Difference between pages "D45 Prover Enhancement" and "CamilleX"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Leuschel
 
 
Line 1: Line 1:
= Overview =
+
{{TOCright}}
* Two tasks concerned the prover performance from the core platform: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. While the addition of rewriting and inference rules has always been a regular task to enhance the Rodin integrated prover during DEPLOY lifetime, a new way to manage tactics has been implemented. In fact, the user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations.
+
Return to [[Rodin Plug-ins]]
* The ProB plug-in allows to find and visualize counter examples to the invariant and deadlock preservation proof obligations. ProB has also been used for finding count examples to proof rules of the industrial partner Siemens.
 
* The SMT Solvers plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. {{TODO}} (Laurent Voisin, Yoann Guyot)
 
  
= Motivations =
+
The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.
== New rewriting and inference rules ==
+
Extension to Event-B including the ''machine inclusion'' mechanism is also supported.
In an Event-B development, more than 60% of the time is spent on proofs. It has been a continuous aim to increase the number of automatically discharged proof obligations (POs) by improving the capabilities of the integrated sequent prover through the addition of rewriting and inference rules. These rules were provided through tactics, or existing or newly created. These tactics were automatic, or manual, or sometimes both. Providing new proving rules, even if it sometimes does not increase directly the number of automatically discharged POs aims to help the user to interactively discharge them and spare his time.
 
  
== Advanced Preferences for Auto-tactics ==
+
<br style="clear: both" />
  
The proportion of automatically discharged proof obligations heavily depends on Auto-Tactic configuration.
+
Please have a look also at the [[CamilleX User Guide]].
Sometimes, the automatic prover fails because the tactics are applied in a 'wrong' order - 'wrong' for a given PO - even though all needed tactics are present.
 
Early version of Rodin provided preferences for automatic tactics that enabled to reorder them, but the ordering was lost at each change: one could not record a particular tactic order in order to reuse it later.
 
  
Another issue is to have more than one possibility to combine the tactics. Indeed, the only implicit combination of tactics available consisted in trying to apply them in turn for every open node of a proof. In the proving area, there exists a notion of ''tactic combinators'', also called ''tacticals'', that allow to combine tactics in various specific manners, thus providing a sort of tactic arithmetic.
+
=== Current version ===
 +
The CamilleX version 2.1.0 is available as a separate feature from the main Soton Plug-in update site (under the ''CamilleX'' category).  Notice that the Soton plug-in update site is now included in the composite Rodin Update Site.
  
The advanced preferences for auto-tactics solved these two issues.
+
=== Principles ===
 
+
The CamilleX editors (i.e., XContext and XMachine editors) operate on the separate XContext and XMachine text file and they are compiled to the Rodin files.
== Isabelle Plug-in ==
 
{{TODO}} ''To be completed by Matthias Schmaltz''
 
== ProB Disprover ==
 
 
 
ProB can be used to find counterexamples to invariant preservation and deadlock preservation proof obligations.
 
This feature relies on the constraint solving capabilities of the ProB kernel. It is available from the ProB plugin after loading an Event-B model.
 
 
 
WIthin the context of WP2 (Transportation) ProB has also been used to try and find counterexamples to individual proof rules in the Siemens proof rule database.
 
For this, the ProB command line tool has been extended to load proof rule files (using a Prolog parser to avoid the JVM startup time) and then applies the ProB constraint solver to try and find counter examples to each proof rule.
 
This work has already identified several errors in the Siemens rule database and the work is still ongoing.
 
A current issue is the addition of explicit well-definedness conditions into the proof rules, as well as the fact that some proof rules use substations inside predicates.
 
 
 
 
 
 
 
Mention work using Kodkod here ?
 
 
 
== SMT Solver Integration ==
 
The integration of SMT solvers into the Rodin platform is motivated by two main reasons. On the one hand, the enhancement of its proving capability, especially in the field of arithmetics. On the other hand, the ability of extracting some useful informations from the proofs produced by these solvers, such as unsatisfiable cores, in order to significantly decrease the time necessary to prove a modified model.
 
 
 
= Choices / Decisions =
 
== New rewriting and inference rules ==
 
{{TODO}} ''To be completed by Laurent Voisin''
 
== Advanced Preferences for Auto-tactics ==
 
 
 
Since Rodin 2.1, one can create his own tactic profiles. A tactic profile allows to set and record a particular order of chosen basic tactics. Furthermore, a profile can be applied either globally (as before), or specifically for a given project.
 
 
 
Since Rodin 2.3, tacticals and parameterization have been added to the profiles, thus increasing the potential of such proving feature.
 
A tactic profile may now be composed of tacticals, that combine any number of basic tactics and other profiles.
 
The parameterization allows for example to set a custom timeout on external provers such as AtelierB P1.
 
 
 
== Isabelle Plug-in ==
 
{{TODO}} ''To be completed by Matthias Schmaltz''
 
== ProB Disprover ==
 
 
 
Currently the constraint based invariant and deadlock checker is run from within the ProB plug-in and not from the prover interface on individual proof obligations.
 
Indeed, for invariant preservation the disprover thus checks an event for all invariants, rather than being applied on individual proof obligations related to that event.
 
However, ProB does know which invariants have already been proven to be preserved by that particular event.
 
The rationale for running the invariant preservation checks in this way is that:
 
* the counterexample is a full valuation of the models variables and constants which can be displayed using the ProB interface,
 
* the invariants and guards truth values can be inspected in detail using the ProB interface, make the counter-example intelligible to the user,
 
* ProB can find out which of the axioms are theorems and ignore them. Indeed in the old ProB disprover approach all of the assumptions were fed, and ProB did not know which ones are relevant to find correct values for the constants and variables. In fact, some of the theorems turned out to be very complicated to check, and prevented ProB from finding counterexamples.
 
 
 
Similarly, the constraint-based deadlock checker is run from the ProB plug-in on a loaded model. As Rodin does not currently generate the deadlock freedom proof obligations, this was an obvious choice. Also, it enables the user to type in additional predicates to find "particularly interesting" counter examples (see ICLP'2011 article below).
 
Also, another advantage is that, again, the counter example can be inspected using the ProB interface.
 
 
 
== SMT Solver Integration ==
 
The translation of Event-B language into the SMT-LIB language is the main issue of this integration. Two approaches were developed for this. The more efficient one is based on the translation capabilities of the integrated predicate prover of the Rodin platform (PP). It is completed by translating membership using an uninterpreted predicate symbol, refined with an axiom of the set theory.
 
Technically, the plug-in classes extend the existing XProverCall, XProverInput, XProverReasoner, AbstractLazilyConstrTactic and ITacticParametizer classes which make it easy to integrate new tactics, reasoners and external prover calls.
 
 
 
= Available Documentation =
 
* {{TODO}} Links for New rewriting and inference rules
 
* {{TODO}} Links for Advanced Preferences for Auto-tactics
 
* {{TODO}} Links for Isabelle Plug-in
 
* {{TODO}} Links for ProB Disprover
 
** [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HaLe2011 Constraint-Based Deadlock Checking of High-Level Specifications. In Proceedings ICLP'2011, Cambridge University Press, 2011.]
 
* {{TODO}} Links for SMT Solver Integration
 
 
 
= Status =
 
== New rewriting and inference rules ==
 
{{TODO}} ''To be completed by Laurent Voisin''
 
== Advanced Preferences for Auto-tactics ==
 
 
 
Advanced Preferences for Auto-tactics are functional in Rodin 2.3. This release provides a first set of tacticals and parameterization options.
 
 
 
Further releases may offer additional tacticals and options, according to user feedback.
 
 
 
== Isabelle Plug-in ==
 
{{TODO}} ''To be completed by Matthias Schmaltz''
 
== ProB Disprover ==
 
 
 
The ProB constraint-based invariant and deadlock checkers are available in the current release of ProB for Rodin. The deadlock checker has been applied successfully on a very large industrial model within WP1 (automotive).
 
There is of course always the scope to improve the capabilities of the tool by improving the constraint solving capabilities.
 
In particular, further simplification of existential quantifiers will be important for the deadlock checker to be applied effectively on certain models.
 
 
 
The Siemens proof rule database validation work is still ongoing.
 
This work has already identified several errors in the Siemens rule database.
 
However, a current issue is the addition of explicit well-definedness conditions into the proof rules, as well as the fact that some proof rules use substations inside predicates.
 
 
 
== SMT Solver Integration ==
 
{{TODO}} ''Laurent Voisin & Yoann Guyot''
 
 
 
[[Category:D45 Deliverable]]
 

Latest revision as of 13:09, 19 July 2021

Return to Rodin Plug-ins

The CamilleX feature provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines. Extension to Event-B including the machine inclusion mechanism is also supported.


Please have a look also at the CamilleX User Guide.

Current version

The CamilleX version 2.1.0 is available as a separate feature from the main Soton Plug-in update site (under the CamilleX category). Notice that the Soton plug-in update site is now included in the composite Rodin Update Site.

Principles

The CamilleX editors (i.e., XContext and XMachine editors) operate on the separate XContext and XMachine text file and they are compiled to the Rodin files.