Project

General

Profile

Edit History

Wiki » History » Version 1

Ilya Shchepetkov, 02/01/2019 06:56 PM

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





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





    4
    
    
    





    5
    
    
    
# Установите Java Runtime Environment (JRE).





    6
    
    
    
# Скачайте архив с Rodin (на данный момент актуальная версия - 3.4): https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/





    7
    
    
    
# Распакуйте архив в любом месте на жестком диске и запустите исполняемый файл rodin.





    8
    
    
    





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





    10
    
    
    
* SMT Solvers Plug-in, инструкция http://wiki.event-b.org/index.php/SMT_Solvers_Plug-in





    11
    
    
    
* Atelier B Provers, набор инструментов автоматического доказательства





    12
    
    
    





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





    14
    
    
    





    15
    
    
    
# Запустите Rodin и перейдите в раздел Help > Install New Software.





    16
    
    
    
# В выпадающем меню Work with выберите Rodin.





    17
    
    
    
# Появится на выбор несколько категорий с различными плагинами. Разверните категорию Prover Extensions и поставьте галку рядом с SMT Solvers. Нажмите Next.





    18
    
    
    
# Проверьте, что все верно, и нажмите Next.





    19
    
    
    
# Прочитайте и примите условия лицензионного соглашения. Затем нажмите кнопку Finish.





    20
    
    
    
# Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажмите OK.





    21
    
    
    
# Установка может занять некоторое время. По окончанию нажмите на Restart Now.





    22
    
    
    





    23
    
    
    
Установка Atelier B Provers почти не отличается от установки SMT Solvers Plug-in. Отличия:





    24
    
    
    
* На шаге номер 2 в выпадающем меню Work with нужно выбрать Atelier B Provers.





    25
    
    
    
* На шаге номер 3 нужно развернуть категорию Atelier B Provers и поставьте галочку рядом с Atelier B Provers.





    26
    
    
    





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





    28
    
    
    
# Откройте окно настроек Rodin (пункт Preferences в меню)





    29
    
    
    
# В выпадающем списке меню выберите Event-B -> Sequent Prover -> Auto/Post Tactic





    30
    
    
    
# В выпадающем списке Tactic profile to be used for auto-tactics выберите Default Auto Tactic with SMT





    31
    
    
    
# Уберите галку напротив Enable post-tactic for proving