Динамическая верификация без VSCode¶

VSCode удобен для разработки модели, медиатора, для разовых проверок трасс. Для запуска динамической верификации в автономном от пользователя режиме VSCode не годится. Чтобы настроить такой режим, нужно:

подготовить окружение
загрузить модель, медиатор и трассы
транслировать модель
транслировать трассы
запустить проверку трасс

Подготовка окружения¶

Нужно установить следующее базовое программное обеспечение:

NodeJS
Python версии не ниже 3.9

Нужно распаковать расширение АНИС для VSCode, так как в нем расположены необходимые инструменты и для работы без VSCode:

unzip eventb-vscode-extension.vsix
cd extension

Загрузка исходных файлов¶

Создать рабочую директорию:
```
mkdir workspace
```
Загрузить модель:
```
mkdir workspace/src
cp .......
```
Загрузить класс-наследник машины и файл conftest.py (при наличии)

Создать виртуальную среду и установить Python-библиотеки АНИС:

cd workspace
mkdir .venv
python3 -m venv .venv
. .venv/bin/activate
pip3 install <wheel-file anis>
pip3 install <wheel-file cli_anis>
cd ..

Загрузить медиатор в рабочую директорию
Загрузить трассы:
```
mkdir workspace/traces
cp .........
```

Трансляция модели¶

Скачать зависимости транслятора модели:
```
scripts/setup_translator.sh
```
Выбрать целевой компонент

Странслировать целевой компонент:

scripts/run_translator.sh workspace/src/<MACHINE>.bm workspace

Транслятор создаст поддиректорию workspace/anis/model и в нее поместит исходные файлы Python.

Трансляция трасс¶

Выбрать адаптер монитора (на данный момент поддерживается всего один)
Скачать зависимости выбранного адаптера монитора:
```
make -C scripts/monitor_adapters -f pytest_json.mk setup
```
Создать файл с форматом трассы
```
vim workspace/trace.json
...
```

Странслировать трассы, все пути должны быть абсолютными, TESTS_DIR должен быть путем внутри workspace:

make -s -C scripts/monitor_adapters -f pytest_json.mk run \
TRACES_DIR=/home/.../workspace/traces \
TRACE_FORMAT=/home/.../workspace/trace.json \
NORMALIZED_TRACES_DIR=/home/.../workspace/traces_normalized \
TESTS_DIR=/home/.../workspace/tests

Проверка трасс¶

cd workspace
pytest -p anis.cli

Если требуется дополнительно собирать покрытие по модели, то надо создать файл workspace/settings.json с тем же содержимым, что и файл .vscode/settings.json.