Project

General

Profile

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

Ilya Shchepetkov, 06/30/2021 11:45 AM

1 1 Ilya Shchepetkov
h1. Инструкция по установке и настройке Rodin
2
3
Для установки Rodin выполните следующие действия:
4
5 6 Ilya Shchepetkov
# Установить @Java Runtime Environment (JRE) 11@ .
6
# Скачать архив с Rodin нужной версии и для нужной ОС, выложенный в данном проекте на вкладке @Files@: https://forge.ispras.ru/projects/spmodeler/files
7
# Распаковать архив в любом месте на жестком диске и запустить исполняемый файл @rodin@.
8 1 Ilya Shchepetkov
9 6 Ilya Shchepetkov
Перед использованием Rodin необходимо установить два плагина:
10
* @SMT Solvers@, позволяет использовать SMT-решатели для автоматического доказательства.
11
* @Atelier B Provers@, набор дополнительных инструментов автоматического доказательства.
12 1 Ilya Shchepetkov
13 6 Ilya Shchepetkov
Для установки плагина @SMT Solvers@ нужно выполнить следующие действия:
14
# Скачать файл с плагином со вкладки @Files@ данного проекта. Например, подойдет следующая версия: https://forge.ispras.ru/attachments/8943.
15
# Запустить Rodin, перейти в раздел @Help > Install New Software@ и нажать @Add@.
16
# В открывшемся окне нужно ввести имя (например, @SMT Solvers ISP RAS@), нажать на кнопку @Archive...@, найти на диске архив с плагином, и затем закрыть окно нажав кнопку @Add@.
17
# Убедиться, что в поле @Work with@ выбран путь до архива с плагином.
18
# После этого необходимо убрать галочку напротив опции @Group items by category@, выбрать для установки плагин @SMT Solvers@ (поставить галочку), и нажать @Next@.
19
# Проверить, что все верно, и нажать @Next@.
20
# Принять условия лицензионного соглашения и нажать @Finish@.
21
# Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажать @OK@.
22
# Установка может занять некоторое время. По окончанию нажать на @Restart Now@.
23 3 Ilya Shchepetkov
24 6 Ilya Shchepetkov
Для установки плагина @Atelier B Provers@ нужно выполнить следующие действия:
25
# Запустить Rodin, перейти в раздел @Help > Install New Software@.
26
# В выпадающем меню @Work with@ выбрать @Atelier B Provers@.
27
# Поставить галочку рядом с @Atelier B Provers@ и нажать @Next@.
28
# Принять условия лицензионного соглашения и нажать @Finish@.
29
# Появится предупреждение о том, что содержимое устанавливаемого плагина не подписано. Нажать @OK@.
30
# Установка может занять некоторое время. По окончанию нажать на @Restart Now@.
31 2 Ilya Shchepetkov
32 6 Ilya Shchepetkov
После установки плагинов их нужно настроить. Для этого нужно:
33
# Открыть окно настроек Rodin (пункт @Window > Preferences@ в меню, или @Rodin Platform > Preferences@ на macOS).
34
# В выпадающем списке меню перейти в @Event-B > Sequent Prover > Auto/Post Tactic@.
35
# В разделе @Auto-Tactics@ в выпадающем списке @Tactic profile to be used for auto-tactics@ выбрать @Default Auto Tactic with SMT@.
36
# В разделе @Interactive-Tactics@ в выпадающем списке @Tactic profile to be used for interactive-tactics@ выбрать @Default Interactive Tactic with SMT@.
37
# В разделе @Post-Tactics@ убрать галочку напротив @Enable post-tactic for proving@.
38 7 Ilya Shchepetkov
39
Также рекомендуется слетать следующее:
40
# Открыть окно настроек Rodin.
41
# В выпадающем списке меню перейти в @General@.
42
# Убрать галочку напротив @Always run in background@.