imported>Tommy |
imported>Andy |
| Line 1: |
Line 1: |
| − | ''For developer support, see [[SMT Solvers Plug-in Developer Support]]''
| + | = Generating Code from State-Machine Diagrams = |
| − | {| align="right"
| + | We have introduced the ability to generate code from state-machine diagrams, in version 0.2.3 of the code generation feature plug-in. Implementation code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machines are created, using the existing state-machine plug-in, subject to the limitations described below. |
| − | | __TOC__
| + | == Limitations == |
| − | |}
| + | The current code generation tool is restricted to generating code for a single Event-B machine, which may contain one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines. In principal we should be able to apply decomposition techniques to decompose the single Event-B machine with state-machines into a number of machines, with the state-machines, or the elements of state-machines, distributed between them. |
| | | | |
| − | ==Introduction==
| + | Another limitation is that we do not handle nested state-machines, although this should be feasible. |
| − | 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/]).
| |
| | | | |
| − | ==Installation== | + | == Translations == |
| − | 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 ===
| + | < Diagram here > |
| − | Download the Rodin Platform 2.3 (Core) (around 61MB) corresponding to your operating system and install it [http://www.event-b.org/install.html].
| |
| | | | |
| − | === Installing the SMT Solvers Plug-in ===
| + | The translation of the diagrammatic elements to code has been hard-coded in the code generation plug-in. We have introduced new types to the translator's common language model (IL1). We add case-statements and a container for them, since these are commonly used to implement state-machines. The code generator navigates through each state of a state-machine, generating an internal representation of the state-machine which is used to create the IL1 model. The IL1 model is then used to generate code for the various target languages that may have been implemented. We have also updated the IL1-to-target code generators, to generate case statements in Ada, C and Java. |
| − | Launch Rodin and go to ''Help > Install New Software...''.
| |
| | | | |
| − | [[Image:Install_new_software.png|450px]]
| + | Each state-machine has an Enumerated type whose elements take the names of the states. A state variable is created in the target that keeps track of the current state, and has the type of the enumeration. |
| | | | |
| | + | Each state in the state machine is related to a case statement. For instance, the Ada code for the diagram above, is, |
| | | | |
| − | Select the Rodin Platform Update Site: http://rodin-b-sharp.sourceforge.net/updates.
| + | case sm_state is |
| | + | when A then <body> ; sm_state := B; |
| | + | when B then ... |
| | | | |
| − | [[Image:Select_update_site.png|450px]]
| + | The <body> translation is determined by the number of outgoing transitions and the guards and actions of the elaborated events. In the event that a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. In the event that a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. |
| | | | |
| | + | For example, if we have a machine variable v:INT and events ''ab'' and ''ac'' defined as follows: |
| | | | |
| − | Unfold the ''Prover Extensions'' category, and select the ''SMT Solvers Integration'' feature. Click ''Next''.
| + | ab = when v < 10 then <a1> end; |
| | + | ac = when v >= 10 then <a2> end |
| | | | |
| − | [[Image:Select_smt_feature.png|450px]]
| + | Then this is translated to a branching statement, as in the following Ada statement: |
| | | | |
| | + | if v < 10 then <a1> |
| | + | elsif v >= 10 then <a2> |
| | + | end if; |
| | | | |
| − | Review the item to be installed and click ''Next''.
| + | == Tooling == |
| − | | |
| − | [[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.<br>
| |
| − | 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.<br>
| |
| − | 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.<br>
| |
| − | For example, such configurations can execute the same solver with different options, or different versions of the same solver, or different solvers.<br>
| |
| − | | |
| − | 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.<br>
| |
| − | 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.<br>
| |
| − | 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.<br>
| |
| − | 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]]).<br>
| |
| − | 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]]
| |
Generating Code from State-Machine Diagrams
We have introduced the ability to generate code from state-machine diagrams, in version 0.2.3 of the code generation feature plug-in. Implementation code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machines are created, using the existing state-machine plug-in, subject to the limitations described below.
Limitations
The current code generation tool is restricted to generating code for a single Event-B machine, which may contain one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines. In principal we should be able to apply decomposition techniques to decompose the single Event-B machine with state-machines into a number of machines, with the state-machines, or the elements of state-machines, distributed between them.
Another limitation is that we do not handle nested state-machines, although this should be feasible.
Translations
< Diagram here >
The translation of the diagrammatic elements to code has been hard-coded in the code generation plug-in. We have introduced new types to the translator's common language model (IL1). We add case-statements and a container for them, since these are commonly used to implement state-machines. The code generator navigates through each state of a state-machine, generating an internal representation of the state-machine which is used to create the IL1 model. The IL1 model is then used to generate code for the various target languages that may have been implemented. We have also updated the IL1-to-target code generators, to generate case statements in Ada, C and Java.
Each state-machine has an Enumerated type whose elements take the names of the states. A state variable is created in the target that keeps track of the current state, and has the type of the enumeration.
Each state in the state machine is related to a case statement. For instance, the Ada code for the diagram above, is,
case sm_state is
when A then <body> ; sm_state := B;
when B then ...
The <body> translation is determined by the number of outgoing transitions and the guards and actions of the elaborated events. In the event that a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. In the event that a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete.
For example, if we have a machine variable v:INT and events ab and ac defined as follows:
ab = when v < 10 then <a1> end;
ac = when v >= 10 then <a2> end
Then this is translated to a branching statement, as in the following Ada statement:
if v < 10 then <a1>
elsif v >= 10 then <a2>
end if;
Tooling
