imported>Nicolas: /* Preparing SMT solvers */

2014-06-06T08:48:31Z

Preparing SMT solvers

← Older revision		Revision as of 08:48, 6 June 2014
Line 51:		Line 51:
	=== Preparing SMT solvers ===		=== Preparing SMT solvers ===

	Install the binary files of your SMT ~~solver~~ into the <tt>solvers</tt> directory and ~~for~~ each define at least one configuration in the <tt>preferences</tt> file. A model for the preferences file is available from https://sourceforge.net/p/rodin-b-sharp/smt/ci/master/tree/PerformanceApp/org.eventb.smt.core.perf.app/preferences.model.		Install the binary files of your SMT solvers into the <tt>solvers</tt> directory and make them executable if needed. For each solver, define at least one configuration in the <tt>preferences</tt> file. A model for the preferences file is available from https://sourceforge.net/p/rodin-b-sharp/smt/ci/master/tree/PerformanceApp/org.eventb.smt.core.perf.app/preferences.model.

	== Running Tests ==		== Running Tests ==

imported>Laurent: /* Running Tests */ Add tracing option

2014-05-19T14:51:59Z

Running Tests: Add tracing option

← Older revision		Revision as of 14:51, 19 May 2014
Line 63:		Line 63:

	'''Caution:''' The contents of the <tt>workspace</tt> and <tt>results</tt> directories will be wiped clean before running the tests.		'''Caution:''' The contents of the <tt>workspace</tt> and <tt>results</tt> directories will be wiped clean before running the tests.

			If you want more details on the interaction with the SMT solvers, you can turn on tracing. For this create a file called `options` in the current directory with the contents
			org.eventb.smt.core/debug = true
			org.eventb.smt.core/debug/translator = true
			org.eventb.smt.core/debug/translator_details = true
			and add the two arguments <tt>-debug `pwd`/options</tt> to the command line.

	== Exploiting Test Results ==		== Exploiting Test Results ==

imported>Laurent: Created page with "{{TOCright}} This page describes how to measure the performance of SMT solvers linked to the Rodin platform through the SMT Solvers plug-in. Performance is measured by runnin..."

2014-05-19T14:35:15Z

Created page with "{{TOCright}} This page describes how to measure the performance of SMT solvers linked to the Rodin platform through the SMT Solvers plug-in. Performance is measured by runnin..."

New page

{{TOCright}}
This page describes how to measure the performance of SMT solvers linked to the Rodin platform through the SMT Solvers plug-in.

Performance is measured by running the SMT solvers on a set of proof obligations coming from some Event-B projects. Each solver is run in the exact same conditions (input sequent, timeout, etc.) to avoid introducing any bias.

Moreover, the solvers are not run straight, but integrated within a more general tactic derived from the <tt>Default Auto Tactic</tt> packaged with the Rodin platform. This makes the tests closer to the end-user experience, and therefore more meaningful.

Finally, the SMT solvers are tested side-by-side with the Atelier B provers. This allows to compare their performance relative to the de facto standard automated provers that have always been available with Rodin.

== Required Software ==

To start with, you need a Rodin platform with the Atelier B and SMT solvers plug-ins installed. Proceed as usual to install this software.

Then you need to install the testing application from the zipped update site http://sourceforge.net/projects/rodin-b-sharp/files/Plugin_SMT_Solvers/PerfApp/org.eventb.smt.core.perf.app-1.0.0.201404291022.zip/download.

== Test Layout ==

The tests are organized in a directory as follows:
├─ preferences
├─ projects/
│ ├── ProjectOne/
│ ├── ProjectTwo/
├─ results/
├─ solvers/
├─ workspace/
where<blockquote>
;preferences
:text file describing the SMT configurations to run
;projects
:contains proof obligations to test, organized in Event-B projects
;results
:will contain the detailed results of the tests (that is all proof and proof status files created by the tests)
;solvers
:contains the SMT solvers to run
;workspace
:is a temporary directory used when running tests
</blockquote>

== Preparing tests ==

To prepare the tests, you need some proof obligations and some SMT solvers.

=== Preparing Proof Obligations ===

The easiest way to prepare your proof obligations is to fetch some Rodin project archives, for instance from the [http://deploy-eprints.ecs.soton.ac.uk/view/type/rodin=5Farchive.html Advance/Deploy Repository].

If you want to be sure to start from a clean project, you can import the archive in a running Rodin platform, remove all proof files of the project, clean the project and rebuild it with the automated prover disabled.

In the end, you need to copy all projects containing proof obligations into the <tt>projects</tt> directory.

=== Preparing SMT solvers ===

Install the binary files of your SMT solver into the <tt>solvers</tt> directory and for each define at least one configuration in the <tt>preferences</tt> file. A model for the preferences file is available from https://sourceforge.net/p/rodin-b-sharp/smt/ci/master/tree/PerformanceApp/org.eventb.smt.core.perf.app/preferences.model.

== Running Tests ==

To run the tests, you need to start Rodin from a command line, specifying the test application
rodin -application org.eventb.smt.core.perf.app.main \
-data /path/to/workspace \
-nosplash -consoleLog /path/to/preferences-file

This will test each solver configured in the given preferences file on every projects. The proof and proof status files will be copied into the <tt>results</tt> directory.

'''Caution:''' The contents of the <tt>workspace</tt> and <tt>results</tt> directories will be wiped clean before running the tests.

== Exploiting Test Results ==

While the tests are run, some global statistics are displayed on the console. If you want more detailed statistics you can use [https://sourceforge.net/p/rodin-b-sharp/smt/ci/master/tree/PerformanceApp/org.eventb.smt.core.perf.app/scripts/statocsv.py this script] or even tailor it to you specific needs.

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

SMT Plug-in Performance - Revision history

imported>Nicolas: /* Preparing SMT solvers */

imported>Laurent: /* Running Tests */ Add tracing option

imported>Laurent: Created page with "{{TOCright}} This page describes how to measure the performance of SMT solvers linked to the Rodin platform through the SMT Solvers plug-in. Performance is measured by runnin..."