SMT Solvers Plug-in Developer Support: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Tommy
mNo edit summary
imported>Laurent
Added link to perf application
 
(10 intermediate revisions by 2 users not shown)
Line 2: Line 2:
{{TOCright}}
{{TOCright}}


==Installation from the sources==
== Installation from the sources ==
You will need to:
To start developping the sources of the SMT Solvers plug-in, you will need to:
* Install the Eclipse Platform.
* Install an Eclipse Platform (to be used as the IDE for the developpment of the SMT Solvers plug-in sources).
* Install the Subclipse plug-in to use SVN in Eclipse.
* Clone the Rodin sources and import them into Eclipse or set a Rodin Platform as a ''target platform''.
* Download Rodin sources into Eclipse.
* Clone the SMT plug-in sources and import them into Eclipse.
* Download SMT plug-in sources into Eclipse.
* Optionnally, install custom SMT solvers if you want to use some.
** 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 Eclipse Platform ===
== Installing the Eclipse Platform ==
Download Eclipse Classic (SDK) (around 170 MB) at http://www.eclipse.org/downloads/ . Install it [http://wiki.eclipse.org/FAQ_Where_do_I_get_and_install_Eclipse%3F].
If you don't have an Eclipse development platform for Java and Eclipse plug-ins installed, then :
* Download Eclipse Classic (SDK) or Eclipse for RCP and RAP Developers at http://www.eclipse.org/downloads/ <br/>
* Install it [http://wiki.eclipse.org/FAQ_Where_do_I_get_and_install_Eclipse%3F].


=== Installing the Subclipse plug-in ===
== Get a Rodin host plaform ==
Launch Eclipse and go to ''Help > Install New Software...''.
There are two possibilities:
* OPTION 1: Develop with the latest sources of the platform (developpment branch).
* OPTION 2: Use a target platform.


Click the ''Add'' button and type:
=== Use a Rodin platform running from the Rodin sources ===
Rodin Core sources are available from a Git repository on Sourceforge.


http://subclipse.tigris.org/update_1.6.x
To use these sources, invoke the following command locally :
git clone http://git.code.sf.net/p/rodin-b-sharp/rodincore rodin-b-sharp-rodincore


Name it (ex: SUBCLIPSE 1.6).
Then, from Eclipse, check out all projects of this cloned repository (i.e. use ''File > Import... > Existing projects in workspace'').


Then select the same items as in the following image:
=== Use a Rodin target platfom ===
You can also use a predefined target platform to be used as an host for the SMT Solvers plug-in you will develop.
To get more information about this, please read [http://wiki.event-b.org/index.php/Using_Rodin_as_Target_Platform].


[[Image:Subclipse_selection.png|600px]]


Under Linux, in order to use JNI, you'll need to install the following packages:
=== Downloading the SMT Plug-in Sources ===
    * libsvn-java
    * subversion
    * libsvn1
and to link the installation directory in eclipse.ini, by adding:
 
-Djava.library.path=/usr/lib/jni
 
then restart Eclipse and select ''JavaHL'' in ''Window > Preferences > Team > SVN''.
 
=== Downloading the Rodin Sources ===
Open the ''SVN Repository Exploring'' perspective.
 
Right-clic in the ''SVN Repositories'' view, then ''New > Repository Location''. Enter the following URL : https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp
 
Select all projects in ''trunk > RodinCore'' then right-clic and ''Checkout...''.
 
[[Image:Rodin selection checkout.png|400px]]


''Check out into the workspace as projects'' must be selected. Then click ''Finish''.
SMT plug-in sources are availbable from a Git repository on Sourceforge.


The download might be long (might take around 15min), do not interrupt.
To start your developpement of the SMT plug-in, invoke the following command locally :
{{warning|Once all the sources are downloaded, get back to the ''Java'' perspective. ''org.eventb.core.seqprover'' and ''org.eventb.core.seqprover.tests'' projects might need to be recompiled: select the former and press ''F5''.}}
git clone http://git.code.sf.net/p/rodin-b-sharp/smt rodin-b-sharp-smt
 
=== Downloading the SMT Plug-in Sources ===
Do the same as to dowload Rodin sources, with projects in ''trunk > exploratory > fages'':
* org.eventb.smt.core
* org.eventb.smt.core.tests
* org.eventb.smt.help
* org.eventb.smt.ui
* org.eventb.smt.ui.tests


== Configuration ==
Then, from Eclipse, check out all projects of this cloned repository (i.e. use ''File > Import... > Existing projects in workspace'').
The folling plug-ins are necessary to run the SMT Solvers plug-in:
''org.eventb.smt''
''org.eventb.smt-feature''
''org.eventb.smt.core''
''org.eventb.smt.core.performance''
''org.eventb.smt.core.tests''
''org.eventb.smt.cvc3''
''org.eventb.smt.cvc3.linux''
''org.eventb.smt.cvc3.macosx''
''org.eventb.smt.cvc3.win32''
''org.eventb.smt.help''
''org.eventb.smt.releng''
''org.eventb.smt.ui''
''org.eventb.smt.verit''
''org.eventb.smt.verit.linux''
''org.eventb.smt.verit.macosx''
''org.eventb.smt.verit.win32''


You'll need to:
== Launch configuration ==
To run a Rodin platform, from the sources in the developpment workspace, you'll need to create an Eclipse launch configuration:
* Launch the Rodin platform as to set the default ''Run Configuration''.
* Launch the Rodin platform as to set the default ''Run Configuration''.
* Add the SMT plug-ins to this configuration.
* Add the SMT plug-ins to this configuration.
Line 78: Line 76:
Close the Rodin Platform. Back in the Eclipse Platform, go to the Run Configuration: ''Run > Run Configurations...''.
Close the Rodin Platform. Back in the Eclipse Platform, go to the Run Configuration: ''Run > Run Configurations...''.


Select the ''Rodin.product'' configuration, and go to the ''Plug-ins'' tab. Check all the SMT Plug-ins except ''org.eventb.smt.core.tests'' and ''org.eventb.smt.ui.tests''.
Select the ''Rodin.product'' configuration, and go to the ''Plug-ins'' tab. <br/>
Check all the SMT Plug-ins except :
* ''org.eventb.smt.core.tests'' and
* ''org.eventb.smt.ui.tests''.
 
[[Image:SMT_Solvers_Dev_Plug-ins_to_select.png|600px]]


[[Image:Plug-ins to select.png|525px]]
NB: You actually just need only one project containing the binaries of CVC3 and VeriT.
Hence, you just need to select one project which corresponds to your platform from :
* org.eventb.smt.cvc3.linux,
* org.eventb.smt.cvc3.win32,
* org.eventb.smt.cvc3.macosx.
and one project from :
* org.eventb.smt.verit.linux,
* org.eventb.smt.verit.win32,
* org.eventb.smt.verit.macosx.


Now, you can launch the Rodin platform extended with the SMT plug-in.
Now, you can launch the Rodin platform extended with the SMT plug-in.
Line 86: Line 97:
=== SMT solvers settings ===
=== SMT solvers settings ===
''See [[SMT_Solvers_Plug-in#SMT_solvers_settings]].''
''See [[SMT_Solvers_Plug-in#SMT_solvers_settings]].''
== Measuring Performance ==
There exists an Eclipse Application for measuring the performance of SMT solvers.  Its usage is described at [[SMT Plug-in Performance]].


[[Category:Plugin]]
[[Category:Plugin]]
[[Category:User documentation]]
[[Category:Developer documentation]]

Latest revision as of 14:34, 19 May 2014

For user support, see SMT Solvers Plug-in

Installation from the sources

To start developping the sources of the SMT Solvers plug-in, you will need to:

  • Install an Eclipse Platform (to be used as the IDE for the developpment of the SMT Solvers plug-in sources).
  • Clone the Rodin sources and import them into Eclipse or set a Rodin Platform as a target platform.
  • Clone the SMT plug-in sources and import them into Eclipse.
  • Optionnally, install custom SMT solvers if you want to use some.

Installing the Eclipse Platform

If you don't have an Eclipse development platform for Java and Eclipse plug-ins installed, then :

Get a Rodin host plaform

There are two possibilities:

  • OPTION 1: Develop with the latest sources of the platform (developpment branch).
  • OPTION 2: Use a target platform.

Use a Rodin platform running from the Rodin sources

Rodin Core sources are available from a Git repository on Sourceforge.

To use these sources, invoke the following command locally : git clone http://git.code.sf.net/p/rodin-b-sharp/rodincore rodin-b-sharp-rodincore

Then, from Eclipse, check out all projects of this cloned repository (i.e. use File > Import... > Existing projects in workspace).

Use a Rodin target platfom

You can also use a predefined target platform to be used as an host for the SMT Solvers plug-in you will develop. To get more information about this, please read [2].


Downloading the SMT Plug-in Sources

SMT plug-in sources are availbable from a Git repository on Sourceforge.

To start your developpement of the SMT plug-in, invoke the following command locally : git clone http://git.code.sf.net/p/rodin-b-sharp/smt rodin-b-sharp-smt

Then, from Eclipse, check out all projects of this cloned repository (i.e. use File > Import... > Existing projects in workspace). The folling plug-ins are necessary to run the SMT Solvers plug-in: org.eventb.smt org.eventb.smt-feature org.eventb.smt.core org.eventb.smt.core.performance org.eventb.smt.core.tests org.eventb.smt.cvc3 org.eventb.smt.cvc3.linux org.eventb.smt.cvc3.macosx org.eventb.smt.cvc3.win32 org.eventb.smt.help org.eventb.smt.releng org.eventb.smt.ui org.eventb.smt.verit org.eventb.smt.verit.linux org.eventb.smt.verit.macosx org.eventb.smt.verit.win32

Launch configuration

To run a Rodin platform, from the sources in the developpment workspace, you'll need to create an Eclipse launch configuration:

  • Launch the Rodin platform as to set the default Run Configuration.
  • Add the SMT plug-ins to this configuration.
  • Set the SMT solvers you want to use within Rodin.

Launching the Rodin Platform

Once we have downloaded the Rodin sources, and built it within Eclipse, we can launch the Rodin platform.

Enter the org.rodinp.platform project and right-clic Rodin.product file then choose Run As... > Eclipse Application.

The Rodin platform is launched and ready.

Adding the SMT plug-ins to the Run Configuration

Close the Rodin Platform. Back in the Eclipse Platform, go to the Run Configuration: Run > Run Configurations....

Select the Rodin.product configuration, and go to the Plug-ins tab.
Check all the SMT Plug-ins except :

  • org.eventb.smt.core.tests and
  • org.eventb.smt.ui.tests.

NB: You actually just need only one project containing the binaries of CVC3 and VeriT. Hence, you just need to select one project which corresponds to your platform from :

  • org.eventb.smt.cvc3.linux,
  • org.eventb.smt.cvc3.win32,
  • org.eventb.smt.cvc3.macosx.

and one project from :

  • org.eventb.smt.verit.linux,
  • org.eventb.smt.verit.win32,
  • org.eventb.smt.verit.macosx.

Now, you can launch the Rodin platform extended with the SMT plug-in.

SMT solvers settings

See SMT_Solvers_Plug-in#SMT_solvers_settings.

Measuring Performance

There exists an Eclipse Application for measuring the performance of SMT solvers. Its usage is described at SMT Plug-in Performance.

Retrieved from ‘https://wiki.event-b.org/index.php?title=SMT_Solvers_Plug-in_Developer_Support&oldid=9256’