Difference between pages "ADVANCE D3.3 Model Checking" and "B2Latex"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Ladenberger
 
imported>Tommy
 
Line 1: Line 1:
−
= Overview =
+
B2Latex is a plug-in for Rodin that allows you to export Event-B contexts and machines in Latex files that can then be further rendered.
−
We think that animation and model checking are important tools when building a model. Animation allows the user to validate if the model corresponds to the user's intentions. Model checking allows to check if the model contains errors and provides counter-examples that help to understand the problem beforehand. Moreover, it allows to reason with domains (like physical units) and verify some properties (like temporal logic ones), that have currently no matching proof support.
 
−
The following activities were pursued within the project:
 
−
* The constraint solving capabilities of ProB have been continuously improved along with scalability improvements.
 
−
* Previously we implemented a TLA to B compiler to use ProB on TLA<sup>+</sup> specifications. We now also support the direction from B to TLA<sup>+</sup>. This allows to use the TCL model checker on B specifications.
 
−
* There is work in progress towards support of the upcoming 2.0 version of the Theory plug-in.
 
−
* We are working on a secondary independent toolchain for animation.
 
−
* We finalized and released the of physical units plug-in.
 
  
−
Outside ADVANCE we improved the model checker by adding support for distributed model checking, partial order reduction and partial guard evaluation. We think that these improvements are also valuable within the ADVANCE project.
+
Current Version : 0.5.3
  
−
= Motivations / Decisions =
+
== Installation/Upgrade ==
 +
The B2latex plugin or "Event-B to Latex exporter" is available from the Main Rodin update site.
 +
Select the main Rodin Update site from the "work with:" field in the Help > Install New Software menu in Rodin.
  
 +
== How to use B2Latex? ==
 +
Righ click on a machine or a context directly from the project explorer and select 'Generate Latex Document' command to produce latex documents.
 +
The latex docs are generated in the 'latex' folder in your Event-B project directory (i.e. ...\workspaceName\projectName\latex\*.tex) together
 +
with a style file named ''b2latex.sty''. bsymb.sty and b2latex.sty are required to process the latex.
 +
You can then run Latex on the source files using your own latex installation.
  
−
'''Secondary toolchain'''
+
bsymb.sty can be dowloaded from http://www.event-b.org or https://sourceforge.net/projects/rodin-b-sharp/files/Doc_%20Event%20B%20LaTeX%20style/1.9/
 +
== News? ==
 +
The B2Latex 0.5.3 is now available from the Rodin update site. It is compatible with Rodin 2.4 and Rodin 2.5.
 +
Since B2Latex 0.5.1, the command to export files has been moved to the Event-B project explorer. Users can select a machine or a context to produce latex documents directly from
 +
the project explorer by pressing right click and then select menu 'Generate Latex Document' on the component of their choice. The latex documents are generated in the 'latex' folder like it was done in other previous releases.
  
−
Independently of ProB we completed the development of a tool, which is able read solutions (constant and variable-values) generated by ProB and evaluate predicates like the properties or the invariant of a B model. Also it is possible to evaluate expression in an interactive mode or animate B machines. The tool is (with the exception of the parser) a complete new implementation of a predicate/expression B-evaluator and animator in python. The goal of the reimplementation is to establish a second independent toolchain to crosscheck results of ProB. The python tool has been successfully tested with industrial B Models from the railway domain. The tool is available from [https://github.com/hhu-stups/pyB http://github.com/hhu-stups/pyB]
+
== Tips ==
  
−
'''B to TLA<sup>+</sup>'''
+
- If you wish to have math formulas or B code in a comment, you need to put them in $..$.
  
−
We developed a transcompiler from B to TLA<sup>+</sup> (Temporal Logic of Actions) to verify B specifications with TLC. TLC is an explicit state model checker for TLA<sup>+</sup> with an efficient disk-based algorithm and support for temporal formulas and fairness.Our translator is full automatic and supports a large subset of B.
+
- The file ''b2latex.sty'' which is generated in the ''latex'' directory can be modified to change the style of the documentation.
−
Moreover it uses static analyses to verify the correctness of the B specification (e.g. type checking and scope checking) and creates an optimized translation for the validation with TLC.
 
−
Error traces (e.g. leading to deadlocks or invariant violations) detected by TLC are translated back to B and can be verified by ProB.
 
  
−
{{TODO}} ''' Kodkod'''
+
- To avoid copying ''bsymb.sty'' to every folder where it is used, please follow the procedure below:
−
''Currently the translation to Kodkod is only applied to axioms when trying to find values for the constants and during the constraint based deadlock check. We plan to restructure ProB's internal programming interfaces in a way that allows to apply Kodkod more easily and make it available for other checks (e.g. constraint-based invariant check, assertion checks).
+
  (If you have used MikTex)
−
We will evaluate how we can employ more SMT based techniques in ProB.''
+
  (1) copy the bsmb.sty file into the MikTex directory
 +
      (somewhere like C:\Program Files\MiKTeX 2.7\tex\latex),
 +
  (2) select start -> program -> MikTex 2.x -> setting.
 +
      You will see a dialog box "MikTeX Options".
 +
  (3) Select "General" tab and then click "Refresh FNDB" to update to the miktex database.
 +
 
 +
  This process makes the bsymb.sty can be used everywhere without copying to any folders.
  
−
{{TODO}}'''  Constraint Solver Improvements '''
+
== Old releases ==
−
''During the further development of ProB's constraint solving it became apparent that it would be helpful to represent the cardinality of a set by a CLP(FD) variable. We plan to change ProB's internal representation of sets in a way that its cardinality can be accessed in this way.
+
B2Latex 0.5.1, is now available from the Rodin update site.
−
To allow a translation from ProB to Kodkod, we implemented an integer interval analysis. We plan to adapt the analysis to set up sizes of deferred sets. This is necessary because ProB chooses a fixed size for a deferred set and sometimes a model has only solutions for a certain size. Currently a user must supply a size manually.''
+
This release is for the Rodin 2.4.x or higher
  
−
'''Theory Plug-in support'''
+
B2Latex 0.5.0, is now available from the Rodin update site.
 +
This release is for the Rodin 0.9.2.x or higher.
  
−
We adapted ProB to the changes that had been made to the Theory Plug-in in preperation of the upcoming release. We implemented support for the theory of transitive closures.
+
B2Latex 0.4.1 is required for the Rodin 0.9.1.  
−
From the current set of standard theories, ProB supports animation of models that use operators of the theories "BoolOps", "FixPoint", "Seq", "SUMandPRODUCT" and "closure".
+
If you want to use the Rodin 0.8.x, you need to install the release 0.3.0 instead.
−
Still unsupported are the operators of the remaining standard theories "BinaryTree" and "List" which use recursively defined operators. We plan to implement support for them for the next release.
 
  
−
''' LTL Fairness'''  
+
''How to use old versions?''
 +
After installation, releases 0.3.x up to 0.5.0, you will see an LX entry in the context menu in the Event-B perspective.
 +
Select the Machine or Context you want to translate to Latex and then press the LX button.
 +
A latex source file will be generated in a folder named ''latex''
 +
in your Event-B project directory (i.e. ...\workspaceName\projectName\latex\*.tex) together
 +
with a style file named ''b2latex.sty''. bsymb.sty and b2latex.sty are required to process the latex.
 +
Run latex on the source files using your own latex installation.
  
−
We currently explore ways to implement Fairness into ProB's LTL model checker. However, it is already possible to use fairness by using the B to TLA translator and running TLC.
+
bsymb.sty can be dowloaded from http://www.event-b.org or http://sourceforge.net/projects/rodin-b-sharp/
  
−
''' Physical Units'''
 
  
−
The work on physical unit support has been completed and is available as an optional plug-in available from the ProB update site.
+
[[Category:User documentation]]
−
 
+
[[Category:Plugin]]
−
'''  BMotion Studio '''
 
−
 
 
−
[[File:d33_bms2_prototype.png|125px|thumb|right|BMotion Studio 2 Prototype]]
 
−
 
 
−
BMotion Studio provides an easy and fast way to create a visualization for a formal model. It comes with a set of predefined widgets and observer which are sufficient for most visualizations. However, it is still cumbersome to add custom widgets and observer to BMotion Studio, since the user needs programming skills in Java and Eclipse Plugin Development. As a consequence we decided to replace the rendering-engine of BMotion Studio with HTML. This has the benefit that we can use the entire HTML functionality. For instance, HTML elements like tables, buttons and images as well as features like CSS (Cascading Style Sheets) and SVG (Scalable Vector Graphics). In addition, the user can reuse all HTML snippets which can be found in the WWW for his own visualization.
 
−
While the user can create visualizations by writing HTML or SVG, we will also provide a way to create visualizations as in the ''old'' BMotion Studio, i.e. via a visual editor with easy to use dialogues and wizards. The screenshot shows a first prototype of the new BMotion Studio visualising a model of a simple lift.
 
−
 
 
−
= Available Documentation =
 
−
 
 
−
'''ProB'''<br>
 
−
The ProB Website<ref>http://www.stups.uni-duesseldorf.de/ProB</ref> is the place where we collect information on the ProB toolset. There are several tutorials on ProB available in the User manual section. We also supply documentation on extending ProB for developers.
 
−
 
 
−
In addition we run a bug tracking system<ref>http://jira.cobra.cs.uni-duesseldorf.de/</ref> to document known bugs, workarounds and feature requests.
 
−
 
 
−
'''BMotion Studio'''<br>
 
−
A developer-, user documentation, tutorial and examples are available from a dedicated webpage<ref>http://www.stups.uni-duesseldorf.de/bmotionstudio</ref> hosted by the University of Duesseldorf.
 
−
 
 
−
= Planning =
 
−
{{TODO}}
 
−
 
 
−
= References =
 
−
<references/>
 
−
 
 
−
[[Category:ADVANCE D3.3 Deliverable]]
 

Revision as of 15:57, 23 April 2012

B2Latex is a plug-in for Rodin that allows you to export Event-B contexts and machines in Latex files that can then be further rendered.

Current Version : 0.5.3

Installation/Upgrade

The B2latex plugin or "Event-B to Latex exporter" is available from the Main Rodin update site. Select the main Rodin Update site from the "work with:" field in the Help > Install New Software menu in Rodin.

How to use B2Latex?

Righ click on a machine or a context directly from the project explorer and select 'Generate Latex Document' command to produce latex documents. The latex docs are generated in the 'latex' folder in your Event-B project directory (i.e. ...\workspaceName\projectName\latex\*.tex) together with a style file named b2latex.sty. bsymb.sty and b2latex.sty are required to process the latex. You can then run Latex on the source files using your own latex installation.

bsymb.sty can be dowloaded from http://www.event-b.org or https://sourceforge.net/projects/rodin-b-sharp/files/Doc_%20Event%20B%20LaTeX%20style/1.9/

News?

The B2Latex 0.5.3 is now available from the Rodin update site. It is compatible with Rodin 2.4 and Rodin 2.5. Since B2Latex 0.5.1, the command to export files has been moved to the Event-B project explorer. Users can select a machine or a context to produce latex documents directly from the project explorer by pressing right click and then select menu 'Generate Latex Document' on the component of their choice. The latex documents are generated in the 'latex' folder like it was done in other previous releases.

Tips

- If you wish to have math formulas or B code in a comment, you need to put them in $..$.

- The file b2latex.sty which is generated in the latex directory can be modified to change the style of the documentation.

- To avoid copying bsymb.sty to every folder where it is used, please follow the procedure below: 

 (If you have used MikTex) 
  (1) copy the bsmb.sty file into the MikTex directory
     (somewhere like C:\Program Files\MiKTeX 2.7\tex\latex),
  (2) select start -> program -> MikTex 2.x -> setting. 
      You will see a dialog box "MikTeX Options".
  (3) Select "General" tab and then click "Refresh FNDB" to update to the miktex database.
  
 This process makes the bsymb.sty can be used everywhere without copying to any folders.

Old releases

B2Latex 0.5.1, is now available from the Rodin update site. This release is for the Rodin 2.4.x or higher

B2Latex 0.5.0, is now available from the Rodin update site. This release is for the Rodin 0.9.2.x or higher.

B2Latex 0.4.1 is required for the Rodin 0.9.1. If you want to use the Rodin 0.8.x, you need to install the release 0.3.0 instead.

How to use old versions? After installation, releases 0.3.x up to 0.5.0, you will see an LX entry in the context menu in the Event-B perspective. Select the Machine or Context you want to translate to Latex and then press the LX button. A latex source file will be generated in a folder named latex in your Event-B project directory (i.e. ...\workspaceName\projectName\latex\*.tex) together with a style file named b2latex.sty. bsymb.sty and b2latex.sty are required to process the latex. Run latex on the source files using your own latex installation.

bsymb.sty can be dowloaded from http://www.event-b.org or http://sourceforge.net/projects/rodin-b-sharp/

Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.3_Model_Checking&oldid=953’