Инструкция по установке и настройке Rodin » History » Revision 6
Revision 5 (Ilya Shchepetkov, 05/25/2021 10:48 AM) → Revision 6/7 (Ilya Shchepetkov, 06/30/2021 11:09 AM)
h1. Инструкция по установке и настройке Rodin Для установки Rodin выполните следующие действия: # Установить @Java Установите Java Runtime Environment (JRE) 11@ . 11. # Скачать Скачайте архив с Rodin нужной версии и для нужной ОС, выложенный в данном проекте на вкладке @Files@: https://forge.ispras.ru/projects/spmodeler/files (на данный момент актуальная версия - 3.6): https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/ # Распаковать Распакуйте архив в любом месте на жестком диске и запустить запустите исполняемый файл @rodin@. rodin. Перед использованием Rodin необходимо желательно установить два плагина: * @SMT Solvers@, SMT Solvers, позволяет использовать SMT-решатели для автоматического доказательства. * @Atelier Atelier B Provers@, Provers, набор дополнительных инструментов автоматического доказательства. Для установки плагина @SMT Solvers@ нужно выполнить SMT Solvers выполните следующие действия: # Скачать файл с плагином со вкладки @Files@ данного проекта. Например, подойдет следующая версия: https://forge.ispras.ru/attachments/8943. # Запустить Rodin, перейти Запустите Rodin и перейдите в раздел @Help Help > Install New Software@ и нажать @Add@. Software. !http://wiki.event-b.org/images/Install_new_software.png! # В открывшемся окне нужно ввести имя (например, @SMT Solvers ISP RAS@), нажать выпадающем меню Work with выберите Rodin. !http://wiki.event-b.org/images/Select_update_site.png! # Появится на кнопку @Archive...@, найти на диске архив выбор несколько категорий с плагином, различными плагинами. Разверните категорию Prover Extensions и затем закрыть окно нажав кнопку @Add@. # Убедиться, что в поле @Work with@ выбран путь до архива поставьте галку рядом с плагином. SMT Solvers. Нажмите Next. # После этого необходимо убрать галочку напротив опции @Group items by category@, выбрать для установки плагин @SMT Solvers@ (поставить галочку), и нажать @Next@. !http://wiki.event-b.org/images/Select_smt_feature.png! # Проверить, Проверьте, что все верно, и нажать @Next@. нажмите Next. !http://wiki.event-b.org/images/Review_install_details.png! # Принять Прочитайте и примите условия лицензионного соглашения и нажать @Finish@. соглашения. Затем нажмите кнопку Finish. !http://wiki.event-b.org/images/Review_licenses.png! # Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажать @OK@. Нажмите OK. !http://wiki.event-b.org/images/Security_warning.png! # Установка может занять некоторое время. По окончанию нажать нажмите на @Restart Now@. Restart Now. Для Установка Atelier B Provers почти не отличается от установки плагина @Atelier B Provers@ нужно выполнить следующие действия: SMT Solvers Plug-in. Отличия: # Запустить Rodin, перейти * На шаге номер 2 в раздел @Help > Install New Software@. # В выпадающем меню @Work with@ Work with нужно выбрать @Atelier Atelier B Provers@. Provers. # Поставить * На шаге номер 3 нужно развернуть категорию Atelier B Provers и поставьте галочку рядом с @Atelier Atelier B Provers@ и нажать @Next@. # Принять условия лицензионного соглашения и нажать @Finish@. # Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажать @OK@. # Установка может занять некоторое время. По окончанию нажать на @Restart Now@. Provers. После установки плагинов их нужно настроить. Для этого нужно: этого: # Открыть Откройте окно настроек Rodin (пункт @Window Window > Preferences@ Preferences в меню, или @Rodin Rodin Platform > Preferences@ Preferences на macOS). # В выпадающем списке меню перейти в @Event-B выберите Event-B > Sequent Prover > Auto/Post Tactic@. Tactic. # В разделе @Auto-Tactics@ Auto-Tactics в выпадающем списке @Tactic Tactic profile to be used for auto-tactics@ выбрать @Default auto-tactics выберите Default Auto Tactic with SMT@. SMT. # В разделе @Interactive-Tactics@ в выпадающем списке @Tactic profile to be used for interactive-tactics@ выбрать @Default Interactive Tactic with SMT@. # В разделе @Post-Tactics@ убрать галочку Post-Tactics уберите галку напротив @Enable Enable post-tactic for proving@. proving.