Project

General

Profile

Инструкция по установке и настройке Rodin » History » Revision 4

Revision 3 (Ilya Shchepetkov, 09/19/2019 12:37 PM) → Revision 4/7 (Ilya Shchepetkov, 12/17/2019 02:04 PM)

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

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

 # Установите Java Runtime Environment (JRE) 8. (JRE). 
 # Скачайте архив с Rodin (на данный момент актуальная версия - 3.4): https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/ 
 # Распакуйте архив в любом месте на жестком диске и запустите исполняемый файл rodin. 

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

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

 # Запустите Rodin и перейдите в раздел Help > Install New Software. 
 !http://wiki.event-b.org/images/Install_new_software.png! 
 # В выпадающем меню Work with выберите Rodin. 
 !http://wiki.event-b.org/images/Select_update_site.png! 
 # Появится на выбор несколько категорий с различными плагинами. Разверните категорию Prover Extensions и поставьте галку рядом с SMT Solvers. Нажмите Next. 
 !http://wiki.event-b.org/images/Select_smt_feature.png! 
 # Проверьте, что все верно, и нажмите Next. 
 !http://wiki.event-b.org/images/Review_install_details.png! 
 # Прочитайте и примите условия лицензионного соглашения. Затем нажмите кнопку Finish. 
 !http://wiki.event-b.org/images/Review_licenses.png! 
 # Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажмите OK. 
 !http://wiki.event-b.org/images/Security_warning.png! 
 # Установка может занять некоторое время. По окончанию нажмите на 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. 
 # В разделе Auto-Tactics в выпадающем списке Tactic profile to be used for auto-tactics выберите Default Auto Tactic with SMT. 
 # В разделе Post-Tactics уберите галку напротив Enable post-tactic for proving.