Проверка формул линейной темпоральной логики (LTL) на заданных последовательностях событий с помощью SPIN. Формула, последовательности и ожидаемые результаты описываются в JSON. Для каждого теста скрипт строит модель Promela, запускает верификатор и сохраняет отчёт с контрпримером, если формула нарушена.
В tasks/ собраны учебные задачи с одним и двумя предикатами: количество событий, порядок их появления, чередование и стабилизация.
Запуск · Свои последовательности · Параметры · Результаты и артефакты · Отчёт · Устройство проекта
- Python 3.8+. Используется только стандартная библиотека; устанавливать пакеты через
pipне требуется. - SPIN 6 с поддержкой оператора
X(next). Для этого SPIN должен быть собран с-DNXT; скрипт проверяет поддержку при запуске. См. установку SPIN и документацию LTL. - GCC для компиляции верификатора. В Windows можно использовать GCC из MSYS2 UCRT64.
git clone https://github.com/DafterT/LTL_checker.git
cd LTL_checkerУкажите пути к SPIN и GCC в config.json. В репозитории задана конфигурация для Windows:
{
"spin": "%LOCALAPPDATA%/Programs/Spin/spin.exe",
"cc": "C:/msys64/ucrt64/bin/gcc.exe"
}Если инструменты доступны в PATH, достаточно "spin": "spin" и "cc": "gcc". В путях Windows используйте / или экранируйте обратные слеши: \\. Каталоги инструментов из абсолютных путей автоматически добавляются в PATH процесса.
Запустите все задания из корня проекта:
python run.pyРезультаты выводятся в консоль, полный отчёт сохраняется в build/<запуск>/report.txt. Каждый запуск создаёт отдельную папку. Для быстрой проверки одного сценария:
python run.py --test "3.1 next_not_a/periodic_reset"Создайте tasks/my_sequence.json. Один файл задаёт одну формулу и набор тестов для неё. В этом примере после каждого события a в следующий момент должно выполняться !a:
{
"predicates": ["a"],
"formula": "[] (a -> X !a)",
"tests": [
{
"name": "single_event",
"prefix": [{"a": 0}, {"a": 1}],
"expected": true
},
{
"name": "periodic_events",
"prefix": [{"a": 0}],
"loop": [{"a": 1}, {"a": 0}],
"expected": true
},
{
"name": "adjacent_events",
"note": "Два события подряд нарушают требование сброса.",
"prefix": [{"a": 0}, {"a": 1}, {"a": 1}],
"expected": false
}
]
}Запуск всех тестов этого файла:
python run.py --test "my_sequence/*"| Поле | Назначение |
|---|---|
predicates |
Непустой список уникальных имён предикатов. |
formula |
LTL-формула в синтаксисе SPIN, общая для всех тестов файла. |
tests |
Непустой список тестов. |
tests[].name |
Имя теста, уникальное внутри файла. Латинские буквы, цифры, _ и -. |
tests[].prefix |
Непустая последовательность состояний; первый элемент — состояние в момент t=0. |
tests[].loop |
Необязательный непустой цикл, повторяемый после prefix бесконечно. |
tests[].expected |
true, если формула должна выполняться, или false, если ожидается нарушение. |
tests[].note |
Необязательное пояснение к тесту, включаемое в отчёт. |
Имена предикатов должны соответствовать [a-z][a-z0-9_]* и не совпадать с зарезервированными словами Promela. Каждое состояние содержит все и только объявленные предикаты со значениями 0, 1, false или true. Например, для "predicates": ["a", "b"] состояние записывается как {"a": 1, "b": 0}.
В формулах доступны [] (всегда), <> (когда-нибудь), X (в следующий момент), U (до), а также логические связки !, &&, ||, ->. Полный синтаксис описан в справочнике SPIN.
LTL проверяется на бесконечной последовательности. prefix выполняется один раз, после чего бесконечно повторяется loop. Если loop отсутствует, все предикаты становятся равными нулю и остаются такими навсегда. Последнее состояние prefix автоматически не продлевается.
Для примера выше:
single_event: 0 → 1 → 0 → 0 → 0 → … expected: true
periodic_events: 0 → [1 → 0] → [1 → 0] → … expected: true
adjacent_events: 0 → 1 → 1 → 0 → 0 → … expected: false
Для постоянного ненулевого продолжения укажите его явно: "loop": [{"a": 1}]. Соседние одинаковые состояния — отдельные моменты времени: 0 → 1 → 1 → 0 и 0 → 1 → 0 могут давать разные результаты для формул с X.
python run.py [--tasks PATH] [--test PATTERN] [--timeout SECONDS] [--depth N]
python run.py --replay PATH [--timeout SECONDS]
| Параметр | По умолчанию | Назначение |
|---|---|---|
--tasks PATH |
tasks/ рядом с run.py |
Папка с заданиями. Читаются только файлы *.json непосредственно в ней. |
--test PATTERN |
* |
Фильтр вида <имя файла без .json>/<имя теста>. Поддерживает *, ? и наборы символов [...]; регистр учитывается. |
--timeout SECONDS |
30 |
Лимит времени одной внешней команды в секундах, а не всего запуска. |
--depth N |
10000 |
Максимальная глубина поиска SPIN. |
--replay PATH |
— | Воспроизведение контрпримера из папки ранее выполненного теста. Новая проверка не запускается. |
-h, --help |
— | Справка. |
--timeout и --depth должны быть положительными. Относительные пути в аргументах отсчитываются от текущего каталога. Настройки инструментов всегда читаются из config.json рядом с run.py.
# Все тесты одного задания
python run.py --test "2.1 both_reset/*"
# Один тест
python run.py --test "2.1 both_reset/late_reset"
# Задания из другой папки с увеличенными лимитами
python run.py --tasks "my_tasks" --timeout 60 --depth 50000| Статус | Значение |
|---|---|
PASS |
Результат проверки совпал с expected. |
FAIL |
Результат проверки отличается от expected. |
ERROR |
Проверка не завершена корректно: ошибка входных данных, инструмента, тайм-аут или ограничение ресурсов. |
PASS не обязательно означает, что формула выполняется. Если expected равен false и SPIN нашёл нарушение, тест успешно пройден. Коды завершения: 0 — все тесты прошли; 1 — есть FAIL; 2 — есть техническая ошибка. При сочетании FAIL и ERROR возвращается 2.
build/<запуск>/
├── report.txt # Общий отчёт: формулы, ожидания, результаты и трассы
├── environment.log # Версия SPIN
├── next_support.log # Проверка поддержки X
└── <задание>/<тест>/
├── case.json # Снимок входных данных
├── model.pml # Сгенерированная модель Promela
├── pan.* # Исходники и исполняемый файл верификатора
├── generate.log # Генерация модели проверки
├── compile.log # Компиляция верификатора
├── verify.log # Полный вывод проверки SPIN
├── model.pml.trail # Контрпример при нарушении формулы
├── replay.log # Подробное воспроизведение контрпримера
└── trace.txt # Краткая трасса состояний
При ошибке сохраняются файлы выполненных этапов. Контрпример и его воспроизведение создаются при нарушении формулы, в том числе для тестов со статусом PASS. Если ожидалось нарушение, но формула выполняется, контрпримера нет.
Чтобы повторно посмотреть сохранённый контрпример, подставьте путь из строки Файлы: в отчёте:
python run.py --replay "build/<запуск>/2.1 both_reset/late_reset"Команда выводит трассу в консоль и обновляет replay.log и trace.txt в папке теста. Для нарушений свойств живости трасса может содержать отметку начала повторяемого цикла.
FAIL— сравнитеexpected, формулу и последовательность вreport.txt; при наличии контрпримера откройтеtrace.txt.- Ошибка запуска или компиляции — проверьте пути в
config.jsonи соответствующий файл*.log. - SPIN не поддерживает
X— используйте сборку SPIN с-DNXT. - Превышение глубины или времени — увеличьте
--depthили--timeout. Незавершённый поиск считаетсяERROR.
Ошибка формата JSON останавливает запуск до проверки тестов. Ошибка генерации, компиляции или проверки отдельного теста не мешает выполнить остальные.
| Путь | Назначение |
|---|---|
| run.py | Чтение заданий, запуск инструментов и формирование отчётов. |
| config.json | Пути к SPIN и GCC. |
| template.pml | Шаблон модели Promela. |
| tasks/ | Формулы и тестовые последовательности. |
| report/ | Отчёт по лабораторной работе в форматах Word и PDF. |
build/ |
Артефакты запусков; каталог исключён из Git. |
Начальное состояние задаётся в объявлениях переменных Promela. Каждый следующий момент выполняется одним d_step, поэтому все предикаты обновляются одновременно. Бесконечное продолжение задаётся явным циклом.
Для каждого теста выполняется цепочка:
spin -o3 -a model.pml
gcc -O2 -DNOREDUCE -o pan.exe pan.c
pan.exe -a -b -m10000 -w18
В Unix исполняемый файл называется pan. Параметр -o3 отключает объединение операторов, а -DNOREDUCE — сокращение частичных порядков; это сохраняет последовательность моментов для формул с X. -a включает поиск принимающих циклов, -b позволяет выявить превышение глубины. Все команды и их вывод сохраняются в логах.