Difference between pages "Modularisation Plug-in Tutorial" and "Proof Obligation Commands"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Alexili
(New page: ==Modularisation Plug-in Tutorial== The tutorial illustrates the use of the modularisation plug-in in an Event-B development. The example used is rather small scale but it still demonstra...)
 
imported>Nicolas
 
Line 1: Line 1:
−
==Modularisation Plug-in Tutorial==
+
In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:
  
−
The tutorial illustrates the use of the modularisation plug-in in an Event-B development. The example used is rather small scale but it still demonstrates some basic principles of introducing modules during the development process.
+
[[Image:PO_Commands.png]]
  
−
===Sluice Control Example===
+
These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key).
  
−
The example is a sluice with two doors connecting areas with dramatically different pressures. The pressure difference makes it unsafe to open a door unless the pressure is leveled between the areas connected by the door. The purpose of the system is to adjust the pressure in the sluice area and control the door locks to allow a user to get safely inside to outside. Such system can be deployed, for example, on a submarine to allow divers to get out while submerged.
+
== Retry Auto Provers ==
  
−
The system parts are two doors that can be operated independently of each other and a pressure controller that allows the change of pressure in the sluice area. The following is a schematic depiction of the system.
+
As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).
  
−
[[Image:SluiceController.png]]
+
It may also be used after changing the Auto Prover preferences, in order to check whether the new prover configuration allows to discharge a given (set of) PO(s).
  
−
The system is summarised with the following set of requirements:
+
== Recalculate Auto Status ==
−
# the system allows a user to get inside or outside by leveling pressure between room and a destination
+
 
−
# the system has three locations - ''outside'', ''sluice'' and ''inside''
+
{{TODO}}
−
# the system has two doors - ''door1'', connecting ''outside'' and ''sluice'', and ''door2'', connecting ''sluice'' and ''inside'';
+
 
−
# there is a device to change pressure in ''sluice'';
+
== Proof Replay on Undischarged POs ==
−
# a door may be opened only if the pressures in the locations it connects is equalised;
+
 
−
# at most one door is open at any moment;
+
{{TODO}}
−
# the pressure can only be switched on when the doors are closed.
+
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
 
 +
{{TODO|Category}}

Revision as of 16:56, 4 March 2010

In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:

PO Commands.png

These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key).

Retry Auto Provers

As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).

It may also be used after changing the Auto Prover preferences, in order to check whether the new prover configuration allows to discharge a given (set of) PO(s).

Recalculate Auto Status

TODO

Proof Replay on Undischarged POs

TODO










TODO: Category

Retrieved from ‘https://wiki.event-b.org/index.php?title=Modularisation_Plug-in_Tutorial&oldid=6559’