Comments 29
Описание ошибки выглядит довольно просто: выводится свойство, которое было нарушено и трасса, которая привела к нарушению свойства.
Вот пример, как это выглядит в IDE:
Ладно, спрошу по другому. После того, как вы увидели, что ошибка есть, вы поняли причину ошибки усилием мысли просматривая код или вывели ее из этого дампа?
То есть вы подали TLC на вход алгоритм и описание свойств, которым вы бы хотели, чтобы он удовлетворял. А TLC проверил алгоритм и сказал вам, действительно ли он им удовлетворяет. И если не удовлетворяет, то отображает конкретный пример, который нарушает как минимум одно из ожидаемых свойств.
После этого вы уже анализируете этот конкретный проблемный пример и (в идеале) понимаете, что вы не учли в алгоритме. Правите алгоритм и повторяете проверку.
Как уже вам успел ответить пользователь alygin, процесс довольно прост:
- Смотрим какие свойства нарушены
- По трассе состояний ищем причину нарушения свойств
- Правим модель
- Запускаем моделирование ещё раз
Во многом похоже на обычную отладку программ, когда просматриваете back-trace при нарушении какого-либо assert'a.
Сначала подробно описывается проблема, алгоритм её решения (с картинками), а потом факир объявляет — теперь нажимаете вот эту красную кнопку, и вуаля — чудо само нашло все ваши ошибки! Вам нужно лишь умело нарисовать некий текст, а далее — просто магия, и вы в шоколаде!
То есть по другому — имея качественное описание проблемы, было бы совсем неплохо дать близкое по качеству описание способа решения. Но вот как раз в этой части автор отсылает читателей в интернет-магазины, где они когда-нибудь смогут купить, дождаться доставки, прочитать, и возможно, что-то понять из того, что автор скрыл за нажатием большой красной кнопки «Сделайте мне красиво!».
На самом деле предложенный подход к решению проблемы вполне известный, базовые принципы довольно простые, поэтому и непонятно — почему эти принципы не озвучены?
И если я прав (а само это сомнение уже явный признак недостаточности информации в статье), то и вы неправильно поняли посыл автора. Точнее, если автор вообще хотел пояснять суть, то это у него не получилось, ну а если не хотел, то ваш результат полностью соответствует отсутствию желания автора.
В других инструментах используются так называемые SAT-solver-ы, которые находят подстановку для логической формулы, при которой формула становится истинной. При этом саму формулу генерируют на основе описания, аналогичного примеру из статьи. То есть все отличия подобных инструментов лишь в обвязке вокруг сольвера, некоторые рисуют диаграммы, другие представляют всё в виде текста. Но ни один из них, естественно, никакие алгоритмы не проверяет. Все они проверяют (при помощи сольвера) можно ли подобрать состояние (а не алгоритм или его ветвь), при котором вылезут противоречия. Поэтому предполагать, что там как-то участвует алгоритм — неправильно, потому что это усложняет (до бесконечности, то есть делает недостижимым) моделирование. Без понимания сути придётся осваивать инструмент методом тыка, примерно как осваивают магию — вот такое заклинание действует вот так, а если изменить в заклинании одно слово — оно перестанет действовать. Почему перестанет? Потому что магия!
В других инструментах используются так называемые SAT-solver-ы, которые находят подстановку для логической формулы, при которой формула становится истинной. При этом саму формулу генерируют на основе описания, аналогичного примеру из статьи. То есть все отличия подобных инструментов лишь в обвязке вокруг сольвера, некоторые рисуют диаграммы, другие представляют всё в виде текста. Но ни один из них, естественно, никакие алгоритмы не проверяет. Все они проверяют (при помощи сольвера) можно ли подобрать состояние (а не алгоритм или его ветвь), при котором вылезут противоречия. Поэтому предполагать, что там как-то участвует алгоритм — неправильно, потому что это усложняет (до бесконечности, то есть делает недостижимым) моделирование. Без понимания сути придётся осваивать инструмент методом тыка, примерно как осваивают магию — вот такое заклинание действует вот так, а если изменить в заклинании одно слово — оно перестанет действовать. Почему перестанет? Потому что магия!
В начале статьи я немного уделил внимание тому, как работает TLC. Там принцип совершенно другой — это просто явный перебор пространства состояний.
В целом, одна из лучших связок инструментов на практике — это Alloy и TLA+/TLC. Alloy — для исследований структур и операций над ними, а TLA+/TLC — для проверки протоколов, интерфейсов взаимодействия, распределённых/параллельных алгоритмов и пр., всего того, что можно моделировать множеством недетерминированных конечных автоматов.
Если будет достаточный интерес читателей, то я могу в следующих статьях подробно расписать, что под капотом у этих инструментов и как они работают внутри. Но у меня сложилось ощущение, что подкапотная логика не так интересна читателям, как примеры использования.
Ну на самом деле на Alloy тоже можно моделировать трейсы, аналогичные тем, что делает TLC (просто ввести некий time в структуру состояния системы с возможностью закольцовывания "суффикса" и наложить ограничения на возможнные переходы — аналог тех самых actions из TLA). Где-то даже статьи были на эту тему со сравнением перфоманса, и там тоже все неоднозначно. Если интересно — могу еще раз найти и кинуть ссылками.
Можно конечно и в Alloy моделировать автоматы и их взаимодействие.
Я даже где-то выкладывал (или собирался выложить) Alloy модуль для работы с NDFA (non-determ. finite automata).
Так как и TLA+/TLC и Alloy делают поиск в пространстве состояний (по-разному, конечно), то понятно, что их области применения частично перекрываются.
Но, если посмотреть с точки зрения удобства использования формализмов для классов задач, то, на мой взгяд, Alloy удобен для исследования/моделирования структур, логики и операций над структурами и отношениями, а TLA+ для моделирования динамики в системах.
Они хорошо взаимодополняют друг-друга.
Тут тяжело всё хорошо и подробно расписать и при этом уложиться в разумный объём статьи.
В предыдущей статье (про Alloy) многие написали, что пример слишком абстрактный и хорошо бы что-нибудь из реальных примеров. Поэтому в этой статье я расписал реальный пример применения TLA+/TLC. Акцент постарался сделать именно на опыте применения TLA+/TLC.
Можно было бы больше уделить внимания особенностям самого TLA+/TLC, но тогда пришлось бы серьёзно сокращать другие части статьи, иначе объём был бы слишком большой, что многих читателей могло бы отпугнуть.
Этот цикл статей изначально задумывался не как обучающий (для тех, кому интереснее будет глубже познакомиться, приведено много ссылок на обучающие и другие материалы), а как ознакомительный, для демонстрации использования современных инструментов в разных прикладных задачах, чтобы показать в первую очередь лёгкость применения современных средств анализа, моделирования и верификации алгоритмов и ПО.
Меня автор фактичски подцепил на TLA своей первой статьей, в качестве тренировки я реализовал (причем в TDD стиле) модель протокола надежной передачи сообщений в сети с возможными потерями, огреб в процессе всяких приколов и уже давно думаю запилить статью-туториал на эту тему, но не хватает мотивации. Если интерес есть — могу попробовать взять себя в руки и все-таки сделать ее.
P.S. Конечная версия "тренировочной" модели на чистом TLA+ и на PCAL есть на гитхабе: https://github.com/skhoroshavin/tla_playground
Возможно, нужно просто создать условия для более глубокого понимания. И начать в таком случае можно с ориентации на массовую аудиторию, из которой хоть кто-то всё же не будет микроскопами гвозди забивать, а займётся более глубоким изучением.
Ну и чисто практически — автор уже предложил пример использования TLA, поэтому возникает вопрос — а чем ваш вариант будет лучше? Можно подробнее расписать нажатия кнопок (обезьяний подход), можно подробнее описать происходящее внутри, ну и можно ещё что-то общее добавить. Вам решать, сможете ли вы (и интересно ли) подать материал как-то по новому.
автор уже предложил пример использования TLA, поэтому возникает вопрос — а чем ваш вариант будет лучше? Можно подробнее расписать нажатия кнопок (обезьяний подход), можно подробнее описать происходящее внутри, ну и можно ещё что-то общее добавит
Скажем так — у автора относительно большая задача, в которую нужно отдельно вникать, что отвлекает от изучения собственно инструмента, почти нет теории, сразу прыжок на абстракцию над TLA+ (т.е. PCAL). Что думал написать я — небольшое введение в принципы, стоящие за TLA+, и дальше очень простой практический пример в TDD стиле (начиная буквально с 3-х строчника на чистом TLA и заканчивая моделью выложенной на гитхаб), в процессе объясняя по мере необходимости как синтаксические конструкции, так и теоретические вещи типа концепций stuttering и weak/strong fairness.
На мой взгляд, это была бы отличная статья для начинающих.
Некоторые тонкие моменты, возможно, я могу потом раскрыть в комментариях или других статьях (по поводу machine-closed спек, некоторые ньюансы временнОй логики, liveness и пр).
В общем — я за.
Было бы здорово, если бы вы написали статью именно как туториал для начинающих, по свежим следам, так сказать.
Мне сложнее писать туториалы для начинающих, так как уже тяжело вспоминать (да и не вспомню многого), как начанал работать с TLA+.
А cli-команда для компиляции есть?
Частью тулбокса является библиотека tla2tools.jar, в которой как раз и содержатся инструменты, с помощью которых можно производить трансляцию, проверку и запуск TLC.
Соответственно, можно запускать это все из командной строки. Есть готовые скрипты, в которые удобно завернуты основные вызовы: tla-bin.
Есть плагин для VS Code, который использует такие же вызовы: TLA+ for Visual Studio Code.
Есть только два нюанса, связанные с тем, что а) Toolbox хранит некоторые настройки в файле *.launch, который сам создает в отдельной поддиректории {имя спека}.toolbox, б) в этой же поддиректории TLC формирует дополнительные файлы во время проверки. Но с этой структурой нужно один раз разобраться и корректно настроить .gitignore, а также флажки для отключения этих файлов. После этого можно работать.
Извиняюсь за задержку с ответом, не сразу заметил.
TLA+ (и PlusCal, как более удобная и привычная программистам обёртка) — это в основном описание взаимодействующих автоматов. Хотя можно и много других вещей выразить в TLA+, но если цель ещё и моделировать, то практически только разновидности автоматов.
Alloy удобен для анализа структур, отношения между элементами которых описываются в реляционной логике первого порядка. Очень близко к описанию отношений между объектами (не в смысле ООП или подобного, а в смысле отражения объектов реального мира) в реляционных БД.
Частично Alloy и TLA+ пересекаются по классу тех систем, что можно ими описать. То есть, можно автоматы и в Alloy моделировать, если явно ввести моменты времени, порядок над ними и отношения между моментами времени и другими структурами системы. Но это будет неудобно и с существенными ограничениями. Ровно как в TLA+ можно описать варианты возможных структур и делать поиск по пространству возможных конфигураций этих структур, но это неудобно и весьма ограниченно.
В целом, первая моя статья описывает весьма характерную задачу для Alloy, а вторая статья — для TLA+
Инженерный подход к разработке ПО. От теории к практике