Project

General

Profile

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

Ilya Shchepetkov, 09/19/2019 12:37 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 2 Ilya Shchepetkov
* SMT Solvers, позволяет использовать SMT-решатели для автоматического доказательства.
11
* Atelier B Provers, набор дополнительных инструментов автоматического доказательства.
12 1 Ilya Shchepetkov
13
Для установки плагина SMT Solvers выполните следующие действия:
14
15
# Запустите Rodin и перейдите в раздел Help > Install New Software.
16 3 Ilya Shchepetkov
!http://wiki.event-b.org/images/Install_new_software.png!
17 1 Ilya Shchepetkov
# В выпадающем меню Work with выберите Rodin.
18 3 Ilya Shchepetkov
!http://wiki.event-b.org/images/Select_update_site.png!
19 1 Ilya Shchepetkov
# Появится на выбор несколько категорий с различными плагинами. Разверните категорию Prover Extensions и поставьте галку рядом с SMT Solvers. Нажмите Next.
20 3 Ilya Shchepetkov
!http://wiki.event-b.org/images/Select_smt_feature.png!
21 1 Ilya Shchepetkov
# Проверьте, что все верно, и нажмите Next.
22 3 Ilya Shchepetkov
!http://wiki.event-b.org/images/Review_install_details.png!
23 1 Ilya Shchepetkov
# Прочитайте и примите условия лицензионного соглашения. Затем нажмите кнопку Finish.
24 3 Ilya Shchepetkov
!http://wiki.event-b.org/images/Review_licenses.png!
25 1 Ilya Shchepetkov
# Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажмите OK.
26 3 Ilya Shchepetkov
!http://wiki.event-b.org/images/Security_warning.png!
27 1 Ilya Shchepetkov
# Установка может занять некоторое время. По окончанию нажмите на Restart Now.
28
29
Установка Atelier B Provers почти не отличается от установки SMT Solvers Plug-in. Отличия:
30
* На шаге номер 2 в выпадающем меню Work with нужно выбрать Atelier B Provers.
31
* На шаге номер 3 нужно развернуть категорию Atelier B Provers и поставьте галочку рядом с Atelier B Provers.
32
33
После установки плагинов их нужно настроить. Для этого:
34 2 Ilya Shchepetkov
# Откройте окно настроек Rodin (пункт Window > Preferences в меню, или Rodin Platform > Preferences на macOS).
35
# В выпадающем списке меню выберите Event-B > Sequent Prover > Auto/Post Tactic.
36
# В разделе Auto-Tactics в выпадающем списке Tactic profile to be used for auto-tactics выберите Default Auto Tactic with SMT.
37
# В разделе Post-Tactics уберите галку напротив Enable post-tactic for proving.