Инструкция по установке и настройке Rodin¶

Для установки Rodin выполните следующие действия:

1. Установить Java Runtime Environment (JRE) 11 .
2. Скачать архив с Rodin нужной версии и для нужной ОС, выложенный в данном проекте на вкладке Files: https://forge.ispras.ru/projects/spmodeler/files
3. Распаковать архив в любом месте на жестком диске и запустить исполняемый файл rodin.

Перед использованием Rodin необходимо установить два плагина:

• SMT Solvers, позволяет использовать SMT-решатели для автоматического доказательства.
• Atelier B Provers, набор дополнительных инструментов автоматического доказательства.

Для установки плагина SMT Solvers нужно выполнить следующие действия:

1. Скачать файл с плагином со вкладки Files данного проекта. Например, подойдет следующая версия: https://forge.ispras.ru/attachments/8943.
2. Запустить Rodin, перейти в раздел Help > Install New Software и нажать Add.
3. В открывшемся окне нужно ввести имя (например, SMT Solvers ISP RAS), нажать на кнопку Archive..., найти на диске архив с плагином, и затем закрыть окно нажав кнопку Add.
4. Убедиться, что в поле Work with выбран путь до архива с плагином.
5. После этого необходимо убрать галочку напротив опции Group items by category, выбрать для установки плагин SMT Solvers (поставить галочку), и нажать Next.
6. Проверить, что все верно, и нажать Next.
7. Принять условия лицензионного соглашения и нажать Finish.
8. Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажать OK.
9. Установка может занять некоторое время. По окончанию нажать на Restart Now.

Для установки плагина Atelier B Provers нужно выполнить следующие действия:

1. Запустить Rodin, перейти в раздел Help > Install New Software.
2. В выпадающем меню Work with выбрать Atelier B Provers.
3. Поставить галочку рядом с Atelier B Provers и нажать Next.
4. Принять условия лицензионного соглашения и нажать Finish.
5. Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажать OK.
6. Установка может занять некоторое время. По окончанию нажать на Restart Now.

После установки плагинов их нужно настроить. Для этого нужно:

1. Открыть окно настроек Rodin (пункт Window > Preferences в меню, или Rodin Platform > Preferences на macOS).
2. В выпадающем списке меню перейти в Event-B > Sequent Prover > Auto/Post Tactic.
3. В разделе Auto-Tactics в выпадающем списке Tactic profile to be used for auto-tactics выбрать Default Auto Tactic with SMT.
4. В разделе Interactive-Tactics в выпадающем списке Tactic profile to be used for interactive-tactics выбрать Default Interactive Tactic with SMT.
5. В разделе Post-Tactics убрать галочку напротив Enable post-tactic for proving.