я правильно понимаю что под эргономичностью ты имел ввиду пространство состояний которое оно может перебрать по сравнению с TLA+?

В чем преимущества?)

Думаю имеется в виду что TLA уж слишком из мира математиков. А в promela вон говорят синтаксис на C похож

Ну вот как раз suchthat у нас почти нет. Т.е. statefull как работает.. сперва создает пустой state. Потом вызывает твой модуль и говорит "дай мне все возможные команды которые я могу сейчас вызвать над твоей моделью, я сам выберу какую-то из них, проверю precondition, обновлю состояние модели, дерну реальную систему, сравню модель с реальнтй и если всё ок, то уже с обновленным стейтом попробую следующую команду и так далее в цикле" (не совсем так, но упрощенно можго так сказать). И у нас на каждом шагу следующие варианты команд и их аргументов создаются на основе текущего state. Т.е. когда пропер спросит нас "дай мне список возможных команд, вот тебе текущий state модели", мы ему не предложим "удалить Fee" если в state нет ни одной Fee

да. у TLA+ два синтаксиса, и один из них — тупо TeX, а в итоге рендерит он в PDF. В итоге у тебя в голове пять концепций: программа, абстрактная модель, два синтаксиса модели, рендеринг tex-синтаксиса. И надо между по крайней мере тремя или четырьмя из них постоянно переключаться.

Ну можно сказать "сделай мне бинарь в котором первый байт это 1 или 0. Если 0 то остальные байты это unicode строка длиной от 3 до 100 символов; если 1 то дальше должен быть int32 длины и потом любой json. И т.п. Генераторы там довольно выразительные на самом деле.
Но пропер он не пытается именно corner cases целенаправленно искать. У него есть внутренняя переменная size и он га каждом шаге её увеличивает и генерирует всё более длинные/ большие значения. Т.е. если ты ему скажешь "сделай мне список", то он в начале теста сгенерирует пустой список, потом чуть побольше и потом всё боььше и больше (точнее он делает в стиле Length = rand:uniform(0, Size))

Pluscal вам не зашёл?
> Spin provides direct support for the use of embedded C code as part of model specifications. This makes it possible to directly verify implementation level software specifications, using Spin as a driver and as a logic engine to verify high level temporal properties.
звучит довольно интересно

У меня к нему эстетическая контрадикция. Но, может быть, вкусовщина всего лишь.

понятно, кстати пользуясь случаем что говорим про formal methods, у тебя нет на примете хорошой книги или пейпера по классификации методов и введения в тему?

Всем привет. Кто знает? Как из файла модуля можно вызвать функцию f()? В консоли её могу вызывать, в модуле - нет

А зачем вам в моделей  функция f()?

в задании сказано сделать destroy, который будет удалять бд, все методы уже сделал и они работают, только вот не пойму как удалить БД

БД - обычный список

Пока у меня возвращается просто ok.

никак. Как вариант держать все в отдельном процессе и грохать процесс

типа new  - запустили процесс с бесконечным циклом в котором receive, delete - послали туда сообщение что пора закругляться

я еще не на столько хорошо знаю Erlang) Мы его только начали учить :)

там вообще странное задание. "борщик мусора выполнит всю работу за вас" - ну тогда формально решением будет destroy(_Db) -> ok.

Окей. Спасибо!

и кмк list comprehensions для этого задания это читерство. Они хотят явные рекурсии.