Инструкция по установке и настройке Rodin » History » Revision 2
Revision 1 (Ilya Shchepetkov, 02/01/2019 06:57 PM) → Revision 2/7 (Ilya Shchepetkov, 02/01/2019 07:05 PM)
h1. Инструкция по установке и настройке Rodin Для установки Rodin выполните следующие действия: # Установите Java Runtime Environment (JRE). # Скачайте архив с Rodin (на данный момент актуальная версия - 3.4): https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/ # Распакуйте архив в любом месте на жестком диске и запустите исполняемый файл rodin. Перед использованием Rodin желательно установить два плагина: * SMT Solvers, позволяет использовать SMT-решатели для автоматического доказательства. Solvers Plug-in, инструкция http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in * Atelier B Provers, набор дополнительных инструментов автоматического доказательства. доказательства Для установки плагина SMT Solvers выполните следующие действия: # Запустите Rodin и перейдите в раздел Help > Install New Software. # В выпадающем меню Work with выберите Rodin. # Появится на выбор несколько категорий с различными плагинами. Разверните категорию Prover Extensions и поставьте галку рядом с SMT Solvers. Нажмите Next. # Проверьте, что все верно, и нажмите Next. # Прочитайте и примите условия лицензионного соглашения. Затем нажмите кнопку Finish. # Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажмите OK. # Установка может занять некоторое время. По окончанию нажмите на Restart Now. Установка Atelier B Provers почти не отличается от установки SMT Solvers Plug-in. Отличия: * На шаге номер 2 в выпадающем меню Work with нужно выбрать Atelier B Provers. * На шаге номер 3 нужно развернуть категорию Atelier B Provers и поставьте галочку рядом с Atelier B Provers. После установки плагинов их нужно настроить. Для этого: # Откройте окно настроек Rodin (пункт Window > Preferences в меню, или Rodin Platform > Preferences на macOS). меню) # В выпадающем списке меню выберите Event-B > -> Sequent Prover > -> Auto/Post Tactic. Tactic # В разделе Auto-Tactics в выпадающем списке Tactic profile to be used for auto-tactics выберите Default Auto Tactic with SMT. SMT # В разделе Post-Tactics уберите Уберите галку напротив Enable post-tactic for proving. proving