Difference between pages "Rodin Workshop 2020" and "SMT Solvers Plug-in"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Son
 
imported>YGU
m
 
Line 1: Line 1:
−
=The 8th Rodin User and Developer Workshop, June, 2021, Ulm, Germany=
+
''For developer support, see [[SMT Solvers Plug-in Developer Support]]''
 +
{| align="right"
 +
| __TOC__
 +
|}
  
−
[https://abz2020.uni-ulm.de/workshop Rodin Workshop 2020 Website @ ABZ2020]
+
==Introduction==
 +
The SMT plug-in allows users to use SMT solvers within Rodin. It is still in development (See sources [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/_exploratory/fages/]).
  
−
(Due to the situation with Corona-Virus the ABZ2020 conference will be postponed to 2021. Our workshop will be collocated with ABZ2021 around June 2021)
+
==Installation==
 +
You will need to:
 +
* Install the Rodin Platform.
 +
* Install the SMT Solvers Plug-in into Rodin.
 +
** Install veriT if you want to use it (instead of ppTrans) to translate Event-B to SMT-LIB.
 +
* Install the SMT solvers you want to use.
  
−
Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and tool-assisted reasoning, in particular, automated proof. The platform is open source and can be extended with plug-ins. A range of plug-ins are available that can be installed via the built-in extensions mechanism of Eclipse.
+
=== Installing the Rodin Platform ===
 +
Download the Rodin Platform 2.3 (Core) (around 61MB) corresponding to your operating system and install it [http://www.event-b.org/install.html].
  
−
The 8th Rodin workshop will be collocated with the [https://abz2020.uni-ulm.de ABZ2020 Conference].
+
=== Installing the SMT Solvers Plug-in ===
 +
Launch Rodin and go to ''Help > Install New Software...''.
  
−
The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers.
+
[[Image:Install_new_software.png|450px]]
  
−
For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.
 
  
−
If you are interested in giving a presentation at the Rodin workshop or have a plug-in to demonstrate, send a short abstract (1 or 2 pages PDF) to [mailto:rodin@ecs.soton.ac.uk?subject=RodinWorkshop2020%20Contribution rodin@ecs.soton.ac.uk] by '''24 April 2020''' with subject '''[RodinWorkshop2020] Contribution''', indicating whether it is a tool usage or tool development presentation.
+
Select the Rodin Platform Update Site: http://rodin-b-sharp.sourceforge.net/updates.
  
−
We will endeavour to accommodate all submissions that are clearly relevant to Rodin and Event-B.
+
[[Image:Select_update_site.png|450px]]
  
−
The proceedings of the workshop will be available as a technical report at the University of Southampton.
 
  
−
==Organisers==
+
Unfold the ''Prover Extensions'' category, and select the ''SMT Solvers Integration'' feature. Click ''Next''.
  
 +
[[Image:Select_smt_feature.png|450px]]
  
−
Asieh Salehi Fathabadi, University of Southampton
 
  
−
Thai Son Hoang, University of Southampton
+
Review the item to be installed and click ''Next''.
  
−
Colin Snook, University of Southampton
+
[[Image:Review_install_details.png|450px]]
 +
 
 +
 
 +
Read and accept the terms of the license agreement to install the plug-in. Then click ''Finish''.
 +
 
 +
[[Image:Review_licenses.png|450px]]
 +
 
 +
 
 +
A security warning appears because the feature content is unsigned. Click ''Ok''.
 +
 
 +
[[Image:Security_warning.png|450px]]
 +
 
 +
 
 +
Click ''Restart Now''.
 +
 
 +
The SMT Solvers Plug-in is now installed.
 +
 
 +
=== Installing the SMT solvers ===
 +
Currently, the SMT plug-in has been tested with the following solvers:
 +
* Alt-Ergo (INRIA Saclay)
 +
* CVC3 (New York and Iowa Universities)
 +
* veriT (Loria Nancy and UFRN)
 +
* Z3 (Microsoft Research)
 +
 
 +
==== Installing veriT ====
 +
veriT solver can be downloaded at http://www.verit-solver.org/veriT-download.php. Compilation and installation instructions are in the ''INSTALL'' file. You must set off proof production in ''Makefile.config'', because the SMT plug-in needs solvers to check satisfiability only:
 +
PROOF_PRODUCTION = NO
 +
# PROOF_PRODUCTION = YES
 +
 
 +
The following tools are used in the installation process (Debian/Ubuntu platforms):
 +
* gcc, g++: compilers
 +
* make, ar, ranlib: build process
 +
* wget, tar, patch: to fetch GMP and Minisat
 +
* bison, flex, m4: build compilers and preprocessing
 +
 
 +
Do not forget to install the E-prover as well[http://eprover.org/] (''eprover'' package on Ubuntu platforms).
 +
 
 +
==== Installing Alt-Ergo ====
 +
alt-ergo solver can be downloaded at http://alt-ergo.lri.fr/, or installed using the Ubuntu repository: ''alt-ergo'' package.
 +
 
 +
==== Installing CVC3 ====
 +
CVC3 solver can be downloaded at http://cs.nyu.edu/acsys/cvc3/download.html, or installed using the Ubuntu repository: ''cvc3'' package.
 +
 
 +
==== Installing Z3 ====
 +
Z3 solver can be downloaded at http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html.
 +
 
 +
 
 +
== SMT solvers configurations ==
 +
In order to use the plug-in, you must set up some SMT Solvers configuration. We call ''SMT Solver configuration'' a settled configuration of a solver, with ad-hoc properties such as its path, its parameters and the SMT-LIB version of the benchmarks it will execute. For example, such configurations can execute the same solver with different options, or different versions of the same solver, or different solvers.
 +
 
 +
As to reach the SMT solver configurations page, open the ''Preferences'' window: ''Window > Preferences''.
 +
 
 +
[[Image:Preferences_menu.png|450px]]
 +
 
 +
 
 +
Go to the ''SMT-Solvers'' page.
 +
 
 +
[[Image:Smt_solvers_preferences_page.png|450px]]
 +
 
 +
 
 +
Add a new SMT solver configuration into Rodin by clicking the ''Add'' button.
 +
 
 +
[[Image:Solver_configuration.png|450px]]
 +
 
 +
* Fill the ''Solver ID'' with the name you want to give to this configuration.
 +
* Select the solver you want to use in this configuration (if it does not appear in the list, select ''unknown'').
 +
* Click ''Browse'' to fill the solver executable path.
 +
* Fill the ''Solver arguments'' if needed. For now, veriT, Alt-Ergo and Z3 do not need any argument. CVC3 must be used with ''-lang smt'' argument.
 +
* Select which version of SMT-LIB must be used by the plug-in. Currently, version 1.2 is the only one covered by the plug-in).
 +
* Click ''OK''.
 +
 
 +
The selected solver configuration is the blue one. This shows which solver configuration will be used when the SMT tactic will be called. If you want to use another solver configuration, click on the corresponding line in the ''SMT-Solvers configurations'' list, and click ''Select''.
 +
 
 +
[[Image:Selected solver.png|451px]]
 +
 
 +
 
 +
=== SMT-LIB translation settings ===
 +
If you want to use veriT instead of ppTrans to translate Event-B sequents to SMT-LIB benchmarks, you need to fill the veriT path, by clicking the corresponding ''Browse'' button, and selecting the veriT binary.
 +
 
 +
The plug-in may use some temporary files to discharge a sequent. You can choose the directory to use for this purpose, by clicking the corresponding ''Browse'' button, and selecting the target directory.
 +
 
 +
== Usage  ==
 +
 
 +
=== Discharging a sequent ===
 +
We give an example of Event-B model of which proof obligation can be discharge using an SMT solver:
 +
 
 +
[[Image:PrettyPrinted context.png|225px]]
 +
[[Image:Hypothesis and goal.png|225px]]
 +
 
 +
''thm1'' is a theorem which must be proved given axioms ''axm2..axm5''.
 +
 
 +
 
 +
Since we installed SMT Plug-in into the Rodin Platform, the SMT tactic button is now accessible in the ''Proof Control'' bar.
 +
 
 +
[[Image:SMT button.png|450px]]
 +
 
 +
 
 +
Clicking on this button will call the previously selected SMT solver, which will discharge the proof obligation if possible:
 +
 
 +
[[Image:Tactic applied successfully.png|450px]]
 +
 
 +
 
 +
When the tactic is applied successfully, this means that the reasonner created the new proof rule:
 +
 
 +
[[Image:Proof Tree and Rule Details.png|450px]]
 +
 
 +
For now, the proof tree doesn't contain any detail because SMT-LIB 1.2 doesn't implement a proof witnesses system.
 +
 
 +
=== Setting-up an SMT auto tactic ===
 +
One might want to set-up a configuration of SMT solver to be used automatically to discharge Event-b sequents in the Rodin platform. Since version 2.3 of Rodin, it is possible to create new ''tactic combinations'' to be applied automatically (See ''Advanced Profile Customisation'' in [[Rodin_Platform_2.3_Release_Notes]]). A reasonable combination using the SMT tactic is an SMT tactic queued to the default auto tactic combination. We show here how to create such a ''profile''.
 +
 
 +
First, open the ''Preferences'' window of the Rodin platform: ''Window > Preferences''.
 +
 
 +
[[Image:Preferences_menu.png|450px]]
 +
 
 +
 
 +
Open the ''Auto/Post Tactic'' preferences page: ''Event-B > Sequent Prover > Auto/Post Tactic''. Go to the ''Profiles'' tab.
 +
 
 +
[[Image:Duplicating_auto_tactic_profile.png|450px]]
 +
 
 +
Select the default auto tactic profile, and click ''Duplicate'' to duplicate it.
 +
 
 +
Then, select the duplicated profile, and click ''Edit'' to edit it.
 +
 
 +
[[Image:Auto_tactic_profile_duplicated.png|450px]]
 +
 
 +
 
 +
In the tactic profile window, rename the profile, and drag and drop the chosen SMT tactic from the tactics list (in the first column) to the end of the combined tactics (in the second column).
 +
 
 +
[[Image:Adding_smt_tactic_in_profile.png|450px]]
 +
 
 +
Then click ''Finish''.
 +
 
 +
Now a new profile combining the SMT tactic with other tactics is created. To set it on, go to the ''Auto/Post Tactic'' tab.
 +
 
 +
[[Image:Smt auto tactic profile selected.png|450px]]
 +
 
 +
Set the tactic profile to be used for auto-tactics up to the one combining the SMT tactic, by using the drop-down menu.
 +
 
 +
Then click ''Ok''.
 +
 
 +
Now, the combined tactics of your new profile, including the SMT tactic, will be automatically launched when a new proof objective will be opened.
 +
 
 +
== Bugs and features request ==
 +
* SMT-LIB 2.0 support in developpment
 +
* Full set theory support in progress
 +
 
 +
== Releases Notes ==
 +
 
 +
'''Version 0.1.0'''
 +
* Initial beta-release.
 +
* Two approaches for translating Event-B to SMT-LIB 1.2:
 +
** with ppTrans (included in Rodin official releases)
 +
** with veriT (must be installed)
 +
* Integration of solvers successfully tested with: ''(notice that no solver will be included in the plug-in at all)''
 +
** Alt-Ergo 0.93
 +
** Cvc3 2011-07-14
 +
** veriT 201107
 +
** z3 2.19
 +
* Good results in the field of linear integer arithmetic with uninterpreted sort and function symbols
 +
* Good support of basic set theory
 +
* Full set theory support needs to be improved
 +
* No SMT-LIB 2.0 support in this release
 +
 
 +
[[Category:Plugin]]
 +
[[Category:User documentation]]

Revision as of 13:14, 20 October 2011

For developer support, see SMT Solvers Plug-in Developer Support

Introduction

The SMT plug-in allows users to use SMT solvers within Rodin. It is still in development (See sources [1]).

Installation

You will need to:

  • Install the Rodin Platform.
  • Install the SMT Solvers Plug-in into Rodin.
    • Install veriT if you want to use it (instead of ppTrans) to translate Event-B to SMT-LIB.
  • Install the SMT solvers you want to use.

Installing the Rodin Platform

Download the Rodin Platform 2.3 (Core) (around 61MB) corresponding to your operating system and install it [2].

Installing the SMT Solvers Plug-in

Launch Rodin and go to Help > Install New Software....

Install new software.png


Select the Rodin Platform Update Site: http://rodin-b-sharp.sourceforge.net/updates.

Select update site.png


Unfold the Prover Extensions category, and select the SMT Solvers Integration feature. Click Next.

Select smt feature.png


Review the item to be installed and click Next.

Review install details.png


Read and accept the terms of the license agreement to install the plug-in. Then click Finish.

Review licenses.png


A security warning appears because the feature content is unsigned. Click Ok.

Security warning.png


Click Restart Now.

The SMT Solvers Plug-in is now installed.

Installing the SMT solvers

Currently, the SMT plug-in has been tested with the following solvers:

  • Alt-Ergo (INRIA Saclay)
  • CVC3 (New York and Iowa Universities)
  • veriT (Loria Nancy and UFRN)
  • Z3 (Microsoft Research)

Installing veriT

veriT solver can be downloaded at http://www.verit-solver.org/veriT-download.php. Compilation and installation instructions are in the INSTALL file. You must set off proof production in Makefile.config, because the SMT plug-in needs solvers to check satisfiability only: 

PROOF_PRODUCTION = NO
# PROOF_PRODUCTION = YES

The following tools are used in the installation process (Debian/Ubuntu platforms):

  • gcc, g++: compilers
  • make, ar, ranlib: build process
  • wget, tar, patch: to fetch GMP and Minisat
  • bison, flex, m4: build compilers and preprocessing

Do not forget to install the E-prover as well[3] (eprover package on Ubuntu platforms).

Installing Alt-Ergo

alt-ergo solver can be downloaded at http://alt-ergo.lri.fr/, or installed using the Ubuntu repository: alt-ergo package.

Installing CVC3

CVC3 solver can be downloaded at http://cs.nyu.edu/acsys/cvc3/download.html, or installed using the Ubuntu repository: cvc3 package.

Installing Z3

Z3 solver can be downloaded at http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html.


SMT solvers configurations

In order to use the plug-in, you must set up some SMT Solvers configuration. We call SMT Solver configuration a settled configuration of a solver, with ad-hoc properties such as its path, its parameters and the SMT-LIB version of the benchmarks it will execute. For example, such configurations can execute the same solver with different options, or different versions of the same solver, or different solvers.

As to reach the SMT solver configurations page, open the Preferences window: Window > Preferences.

Preferences menu.png


Go to the SMT-Solvers page.

Smt solvers preferences page.png


Add a new SMT solver configuration into Rodin by clicking the Add button.

Solver configuration.png

  • Fill the Solver ID with the name you want to give to this configuration.
  • Select the solver you want to use in this configuration (if it does not appear in the list, select unknown).
  • Click Browse to fill the solver executable path.
  • Fill the Solver arguments if needed. For now, veriT, Alt-Ergo and Z3 do not need any argument. CVC3 must be used with -lang smt argument.
  • Select which version of SMT-LIB must be used by the plug-in. Currently, version 1.2 is the only one covered by the plug-in).
  • Click OK.

The selected solver configuration is the blue one. This shows which solver configuration will be used when the SMT tactic will be called. If you want to use another solver configuration, click on the corresponding line in the SMT-Solvers configurations list, and click Select.

Selected solver.png


SMT-LIB translation settings

If you want to use veriT instead of ppTrans to translate Event-B sequents to SMT-LIB benchmarks, you need to fill the veriT path, by clicking the corresponding Browse button, and selecting the veriT binary.

The plug-in may use some temporary files to discharge a sequent. You can choose the directory to use for this purpose, by clicking the corresponding Browse button, and selecting the target directory.

Usage

Discharging a sequent

We give an example of Event-B model of which proof obligation can be discharge using an SMT solver:

PrettyPrinted context.png Hypothesis and goal.png

thm1 is a theorem which must be proved given axioms axm2..axm5.


Since we installed SMT Plug-in into the Rodin Platform, the SMT tactic button is now accessible in the Proof Control bar.

SMT button.png


Clicking on this button will call the previously selected SMT solver, which will discharge the proof obligation if possible:

Tactic applied successfully.png


When the tactic is applied successfully, this means that the reasonner created the new proof rule:

Proof Tree and Rule Details.png

For now, the proof tree doesn't contain any detail because SMT-LIB 1.2 doesn't implement a proof witnesses system.

Setting-up an SMT auto tactic

One might want to set-up a configuration of SMT solver to be used automatically to discharge Event-b sequents in the Rodin platform. Since version 2.3 of Rodin, it is possible to create new tactic combinations to be applied automatically (See Advanced Profile Customisation in Rodin_Platform_2.3_Release_Notes). A reasonable combination using the SMT tactic is an SMT tactic queued to the default auto tactic combination. We show here how to create such a profile.

First, open the Preferences window of the Rodin platform: Window > Preferences.

Preferences menu.png


Open the Auto/Post Tactic preferences page: Event-B > Sequent Prover > Auto/Post Tactic. Go to the Profiles tab.

Duplicating auto tactic profile.png

Select the default auto tactic profile, and click Duplicate to duplicate it.

Then, select the duplicated profile, and click Edit to edit it.

Auto tactic profile duplicated.png


In the tactic profile window, rename the profile, and drag and drop the chosen SMT tactic from the tactics list (in the first column) to the end of the combined tactics (in the second column).

Adding smt tactic in profile.png

Then click Finish.

Now a new profile combining the SMT tactic with other tactics is created. To set it on, go to the Auto/Post Tactic tab.

Smt auto tactic profile selected.png

Set the tactic profile to be used for auto-tactics up to the one combining the SMT tactic, by using the drop-down menu.

Then click Ok.

Now, the combined tactics of your new profile, including the SMT tactic, will be automatically launched when a new proof objective will be opened.

Bugs and features request

  • SMT-LIB 2.0 support in developpment
  • Full set theory support in progress

Releases Notes

Version 0.1.0

  • Initial beta-release.
  • Two approaches for translating Event-B to SMT-LIB 1.2:
    • with ppTrans (included in Rodin official releases)
    • with veriT (must be installed)
  • Integration of solvers successfully tested with: (notice that no solver will be included in the plug-in at all)
    • Alt-Ergo 0.93
    • Cvc3 2011-07-14
    • veriT 201107
    • z3 2.19
  • Good results in the field of linear integer arithmetic with uninterpreted sort and function symbols
  • Good support of basic set theory
  • Full set theory support needs to be improved
  • No SMT-LIB 2.0 support in this release
Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Workshop_2020&oldid=9166’