Инструкция по установке и настройке Rodin » History » Version 5
Ilya Shchepetkov, 05/25/2021 10:48 AM
| 1 | 1 | Ilya Shchepetkov | h1. Инструкция по установке и настройке Rodin |
|---|---|---|---|
| 2 | |||
| 3 | Для установки Rodin выполните следующие действия: |
||
| 4 | |||
| 5 | 5 | Ilya Shchepetkov | # Установите Java Runtime Environment (JRE) 11. |
| 6 | # Скачайте архив с Rodin (на данный момент актуальная версия - 3.6): https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/ |
||
| 7 | 1 | Ilya Shchepetkov | # Распакуйте архив в любом месте на жестком диске и запустите исполняемый файл 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. |