Семинар 11

Установка NuSMV

1. Скачайте и распакуйте архив с исходным кодом.
2. Откройте файл NuSMV/README.txt и найдите раздел 3. BUILDING NUSMV FROM SOURCE CODE.
3. Установите требуемые зависимости и следуйте инструкциям по сборке (у меня быстро получилось, но вообще как повезёт...). В результате у вас должен получиться исполняемый файл NuSMV/build/bin/NuSMV.

Использование NuSMV

1. Запустите NuSMV на файле lect10-ex.smv.
2. Добавьте две новые LTL-спецификации и проверьте их.
3. Попытайтесь избавиться от переменной state, обозначающей явное состояние системы. Булевых переменных p, q и r должно быть достаточно для описания модели. Проверьте эквивалентность исходной модели проверкой тех же LTL-спецификаций.
4. Пользуясь решением задачи о волке, козе и капусте, попробуйте сформулировать в терминах системы переходов задачу о людоедах и миссионерах и найти её решение.