Using ProB with Atelier B: Difference between revisions

 
(62 intermediate revisions by 3 users not shown)
Line 1: Line 1:
[[Category:User Manual]]
== Atelier B Plugin ==
ProB Tcl/Tk can be installed as a plugin for Atelier B, so that ProB can be launched directly from within [http://www.atelierb.eu/ Atelier B] projects.
With this you can animate and model check B machines directly from within the IDE of Atelier-B.
The easiest is to perform the menu command "Install AtelierB 4 Plugin..." in the Help menu of ProB Tcl/Tk. This will create a file called <tt>probtclk.etool</tt> in  an extensions folder next to Atelier B's bbin folder. The extensions folder is created if necessary.
Note: as the layout of Atelier-B's directories has changed, you need to use ProB 1.12.0 or newer for Atelier-B 4.7.1 or newer on macOS.
You can also create the the above file yourself.
Here is a typical <tt>probtclk.etool</tt> file (where PathToProB depends on your location of the ProB installation folder containing the prob and probcli binaries):
<pre>
<externalTool category="component"  name="ProBTclTk" label="&amp;Animate with ProB (Tcl/Tk)">
    <toolParameter name="editor" type="tool" configure="yes"
  default="PathToProB/StartProB.sh" />
    <command>${editor}</command>
    <param>${componentPath}</param>
</externalTool>
</pre>
Note, you can also [[ProB2-UI]] within Atelier-B by creating a suitable file <tt>prob2ui.etool</tt> in this extensions folder. Here is a typical file for macOS; the path needs to be adapted for your location and operating system (we plan to provide an installer within ProB2-UI):
<pre>
<externalTool category="component"  name="ProB2UI" label="&amp;Animate with ProB2-UI">
    <toolParameter name="editor" type="tool" configure="yes"
  default="/Applications/Development/ProB/ProB 2 UI.app/Contents/MacOS/ProB 2 UI" />
    <command>${editor}</command>
    <param>--machine-file</param>
    <param>${componentPath}</param>
</externalTool>
</pre>
After installing the plugins you can launch ProB for selected B machines by right-clicking on a B machine within Atelier B:


[[Category:User Manual]]


[[File:ProB_AtelierB_StartProB_Menu.png|300px|center]]
== ProB as Atelier B Prover==
Atelier B also enables to use ProB as a prover/disprover in the interactive proof window.
For this you need to set the ProB_Path resource to point to probcli (command-line version of ProB). To do this you need to add the following line to the resource file of your project (replacing PATH by the the path on your machine to probcli):
ATB*PR*ProB_Path:PATH/probcli
[[File:ProB_AtelierB_Resource.png|600px|center]]
Then you can type, e.g., the command <tt>prob(1)</tt>in the interactive proof window.
[[File:ProB_AtelierB_Proof.png|600px|center]]


As of version 1.3, ProB contains a much improved parser which tries be compliant with
Two commands are provided within Atelier-B:
Atelier B as much as possible.
* <tt>prob(n)</tt> tries to prove the goal with the selected hypotheses (selected using rp.n as is done for th e pp command of Atelier-B)
* <tt>prob(n|t)</tt> is similar but also limits the execution time of ProB to t seconds


== Atelier B Plugin ==
Atelier-B will call probcli using the commands <tt>-cbc_assertions_tautology_proof</tt> and <tt>-cbc_result_file</tt> after having encoded the proof obligation into the ASSERTIONS clause of a generated B machine.


There is also a [http://www.tools.clearsy.com/index.php5?title=ProB_etool_generation plugin for Atelier B], in order to use the standalone Tcl/Tk Version on [http://www.atelierb.eu/ Atelier B] projects.
The generated machine typically has the form:
<pre>
MACHINE probNr
SETS ...
CONSTANTS ...
PROPERTIES
  << ALL HYPOTHESES >>
ASSERTIONS
  ( <<SELECTED HYPOTHESES >>
  =>
  << PROOF GOAL >>
  )
END
</pre>


== Differences with Atelier B ==
== Differences with Atelier B ==


As of version 1.3, ProB contains a much improved parser which tries be compliant with
Atelier B but provides extra features.


=== Extra Features of ProB ===
=== Extra Features of ProB ===


* Identifiers: ProB also allows identifiers consisting of a single letter.
* Identifiers: ProB also allows identifiers consisting of a single letter. ProB also accepts enumerated set elements to be used as identifiers. Arbitrary identifiers can be used in backquotes (e..g, <tt>`id-1*`</tt>)
 
* Lexing: The Atelier-B parser (<tt>bcomp</tt>) reports a lexical error (<tt>illegal token |-</tt>) if the vertical bar (|) of a lambda abstraction is followed directly by the minus sign.


* Typing:  
* Typing:  
** ProB makes use of a unification-based type inference algorithm. As such, typing information can not only flow from left-to-right inside a formula, but also from left-to-right. For example, <tt>xx<:yy & yy<:NAT</tt> is sufficient to type both <tt>xx</tt> and <tt>yy</tt> in ProB.
** ProB makes use of a unification-based type inference algorithm. As such, typing information can not only flow from left-to-right inside a formula, but also from right-to-left. For example, it is sufficient to type <tt>xx<:yy & yy<:NAT</tt> instead of typing both <tt>xx</tt> and <tt>yy</tt> in ProB.
** Similar to Rodin, ProB extracts typing information from all predicates. As such, <tt>xx/:{1,2}</tt> is sufficient to type <tt>xx</tt>.
** Similar to Rodin, ProB extracts typing information from all predicates. As such, it is sufficient to write <tt>xx/:{1,2}</tt> to assign a type to <tt>xx</tt>.
** the fields of records are normalized (sorted); hence the predicate <tt>rec(a:0,b:1) = rec(b:y,a:x)</tt> is correctly typed for ProB.
** As of version 1.12.1 you can apply prj1 and prj2 without providing the type arguments. For example, you can write <tt>prj2(prj1(1|->2|->3))</tt> instead of <tt>prj2(INTEGER,INTEGER)(prj1(INTEGER*INTEGER,INTEGER)(1|->2|->3))</tt>.


* DEFINITIONS: the definitions and its arguments are type checked by ProB. We believe this to be an important feature for a formal method language. However, as such, every DEFINITION must be either a predicate, an expression or a substitution. You '''cannot''' use, e.g., lists of identifiers as a definition.
* DEFINITIONS: the definitions and its arguments are checked by ProB. We believe this to be an important feature for a formal method language. However, as such, every DEFINITION must be either a predicate, an expression or a substitution. You '''cannot''' use, for example, lists of identifiers as a definition. Also, for the moment, the arguments to DEFINITIONS have to be expressions. Finally, when replacing DEFINITIONS the associativity is not changed. E.g., with <tt>PLUS(x,y) == x+y</tt>, the expression <tt>PLUS(2,3)*10</tt> will evaluate to 50 (and not to 32 as with Atelier-B).


=== Limitations ===
* for a LET substitution, Atelier-B does not allow introduced identifiers to be used in the right-hand side of equations; ProB allows <tt>LET x,y BE x=2 & y=x*x IN ... END</tt> but only if the preference <tt>ALLOW_COMPLEX_LETS</tt> is set to TRUE.
 
* ProB allows WHILE loops and sequential composition in abstract machines
 
* ProB now allows the IF-THEN-ELSE for expressions and predicates: <tt>IF x<0 THEN -x ELSE x END</tt>
 
* ProB now allows LET constructs for expressions and predicates
 
* ProB allows <tt>btrue</tt> and <tt>bfalse</tt> as predicates.
 
* ProB allows to use the Event-B relation operators <tt><<-></tt>,  <tt><->></tt>,  <tt><<->></tt>
 
* ProB allows escape codes (\n, \', \", see above) and supports UTF-8 characters in strings,  and ProB allows multi-line string literals written using three apostrophes (<tt>"''''string''''"</tt>) as well as template strings using three backquotes (e.g., <tt>```1+2=${1+2}```</tt>)


ProB requires all deferred sets to be given a finite cardinality. If no cardinality is specified a default size will be used. Also, mathematical integers will only be enumerated within MININT to MAXINT.
* ProB allows WHILE loops and sequential composition in abstract machines


Other general limitations are:
* Some of the sequence operators can be applied to strings (unless you set the preference STRING_AS_SEQUENCE to FALSE): <tt>size</tt>, <tt>rev</tt>, <tt>^</tt>, <tt>conc</tt>
* closure The transitive and reflexive closure operator of classical B is not supported as defined in the B-Book by Abrial. AtelierB also does not support the operator as defined in the B-Book (as this version cannot be applied in practice). For the reflexive component of closure, ProB will compute the elements in the domain and range of the relation.


Note, however, that the transitive closure operator closure1 is fully supported, and hence one can translate an expression closure(e), where e is a binary relation over some domain d, into the expression closure1(e) \/ id(d).
* As of version 1.12.1 you can write Event-B style set comprehensions with an extra expression like {x•x:1..10|x*x}. You have to use the middle dot, the bullet () or a Unicode dot for this, though.


* fnc, rel These operators are not supported. Also, succ and pred are only supported when applied to numbers (i.e., succ(x) is supported; dom(succ) is not).  
* ProB comes with several libraries of [[External_Functions | external functions]] for string manipulations, mathematical functions, Hilbert's choice operator, etc.


* Trees and binary trees. These onstructs are specific to AtelierB tool and are not supported (the STRING type is now supported);
=== Differences ===
* for ProB the order of fields in a record is not relevant (internally the fields are  sorted), Atelier-B reports a type error if the order of the name of the fields changes


* Definitions Definitions (from the DEFINITIONS clause) with arguments are supported, but in contrast to AtelierB they are type-checked and have to be either an expression, a predicate or a substitution;
* [[Well-Definedness_Checking|Well-definedness]]: ProB will try to check if your predicates are well-defined during animation or model checking, but there is currently no guarantee that all well-definedness errors will be detected. To be on the safe side, you should ensure that your formulas are well-defined according to the  left-to-right definition of well-definedness employed in Rodin for Event-B. ProB now has a [[Well-Definedness_Checking|static checker for well-definedness]] which you can use for this. Note, however, that ProB may re-order conjuncts if this improves well-definedness. For example, for <tt>x:0..3 & y=10/x & x /=0</tt> ProB will not report an error as the conjunct <tt>x/=0</tt> is processed before the division. Indeed, while this predicate is not well-defined according to Rodin's left-to-right rule, it is well-defined according to the more liberal commutative definition of well-definedness.
** There are also limitations wrt refinements. See below;
** VALUES This clause of IMPLEMENTATION machines is not yet supported;


See the page [[Using ProB with Atelier B]] for more details.
=== Limitations ===


=== Multiple Machines and Refinements ===
* Parsing:  ProB will require parentheses around the comma, the relational composition, and parallel product operators. For example, you cannot write <tt>r2=rel;rel</tt>. You need to write <tt>r2=(rel;rel)</tt>. This allows ProB to distinguish the relational composition from the sequential composition (or other uses of the semicolon). You also generally need to put BEGIN and END around the sequential composition operator, e.g., <tt>Op = BEGIN x:=1;y:=2 END</tt>.
* Similarly,  tuples without parentheses are not supported; write (a,b,c) instead of a,b,c


It is possible to use multiple B machines with ProB. However, ProB may not enforce all of the classical B visibility rules (although we try to). As far as the visibility rules are concerned, it is thus a good idea to check the machines in another B tool, such as Atelier B or the B-Toolkit.
* Unsupported Operators:
** Trees and binary trees: most but not all tree operators (mirror, infix) are supported yet. These operators may disappear in future version of Atelier B and may also disappear from ProB.
** <tt>VALUES</tt>: This clause of the <tt>IMPLEMENTATION</tt> machines is not yet fully supported;


While refinements are supported, the preconditions of operations are not propagated down to refinement machines. This means that you should rewrite the preconditions of operations (and reformulate them in terms of the variables of the refinement machine, if necessary). Also, the refinement checker does yet check the gluing invariant.
* There are also some general limitations wrt refinements. See [[Current Limitations#Multiple Machines and Refinements]] for more details.

Latest revision as of 10:02, 23 February 2024


Atelier B Plugin

ProB Tcl/Tk can be installed as a plugin for Atelier B, so that ProB can be launched directly from within Atelier B projects. With this you can animate and model check B machines directly from within the IDE of Atelier-B.

The easiest is to perform the menu command "Install AtelierB 4 Plugin..." in the Help menu of ProB Tcl/Tk. This will create a file called probtclk.etool in an extensions folder next to Atelier B's bbin folder. The extensions folder is created if necessary.

Note: as the layout of Atelier-B's directories has changed, you need to use ProB 1.12.0 or newer for Atelier-B 4.7.1 or newer on macOS. You can also create the the above file yourself.

Here is a typical probtclk.etool file (where PathToProB depends on your location of the ProB installation folder containing the prob and probcli binaries):

<externalTool category="component"   name="ProBTclTk" label="&Animate with ProB (Tcl/Tk)">
    <toolParameter name="editor" type="tool" configure="yes"
   default="PathToProB/StartProB.sh" />
    <command>${editor}</command>
    <param>${componentPath}</param>
 </externalTool>

Note, you can also ProB2-UI within Atelier-B by creating a suitable file prob2ui.etool in this extensions folder. Here is a typical file for macOS; the path needs to be adapted for your location and operating system (we plan to provide an installer within ProB2-UI):

<externalTool category="component"   name="ProB2UI" label="&Animate with ProB2-UI">
    <toolParameter name="editor" type="tool" configure="yes"
   default="/Applications/Development/ProB/ProB 2 UI.app/Contents/MacOS/ProB 2 UI" />
    <command>${editor}</command>
    <param>--machine-file</param>
    <param>${componentPath}</param>
</externalTool>

After installing the plugins you can launch ProB for selected B machines by right-clicking on a B machine within Atelier B:


ProB AtelierB StartProB Menu.png

ProB as Atelier B Prover

Atelier B also enables to use ProB as a prover/disprover in the interactive proof window. For this you need to set the ProB_Path resource to point to probcli (command-line version of ProB). To do this you need to add the following line to the resource file of your project (replacing PATH by the the path on your machine to probcli):

ATB*PR*ProB_Path:PATH/probcli
ProB AtelierB Resource.png

Then you can type, e.g., the command prob(1)in the interactive proof window.

ProB AtelierB Proof.png

Two commands are provided within Atelier-B:

  • prob(n) tries to prove the goal with the selected hypotheses (selected using rp.n as is done for th e pp command of Atelier-B)
  • prob(n|t) is similar but also limits the execution time of ProB to t seconds

Atelier-B will call probcli using the commands -cbc_assertions_tautology_proof and -cbc_result_file after having encoded the proof obligation into the ASSERTIONS clause of a generated B machine.

The generated machine typically has the form:

MACHINE probNr
SETS ...
CONSTANTS ...
PROPERTIES
  << ALL HYPOTHESES >>
ASSERTIONS
  ( <<SELECTED HYPOTHESES >>
   =>
  << PROOF GOAL >>
  )
END

Differences with Atelier B

As of version 1.3, ProB contains a much improved parser which tries be compliant with Atelier B but provides extra features.

Extra Features of ProB

  • Identifiers: ProB also allows identifiers consisting of a single letter. ProB also accepts enumerated set elements to be used as identifiers. Arbitrary identifiers can be used in backquotes (e..g, `id-1*`)
  • Lexing: The Atelier-B parser (bcomp) reports a lexical error (illegal token |-) if the vertical bar (|) of a lambda abstraction is followed directly by the minus sign.
  • Typing:
    • ProB makes use of a unification-based type inference algorithm. As such, typing information can not only flow from left-to-right inside a formula, but also from right-to-left. For example, it is sufficient to type xx<:yy & yy<:NAT instead of typing both xx and yy in ProB.
    • Similar to Rodin, ProB extracts typing information from all predicates. As such, it is sufficient to write xx/:{1,2} to assign a type to xx.
    • the fields of records are normalized (sorted); hence the predicate rec(a:0,b:1) = rec(b:y,a:x) is correctly typed for ProB.
    • As of version 1.12.1 you can apply prj1 and prj2 without providing the type arguments. For example, you can write prj2(prj1(1|->2|->3)) instead of prj2(INTEGER,INTEGER)(prj1(INTEGER*INTEGER,INTEGER)(1|->2|->3)).
  • DEFINITIONS: the definitions and its arguments are checked by ProB. We believe this to be an important feature for a formal method language. However, as such, every DEFINITION must be either a predicate, an expression or a substitution. You cannot use, for example, lists of identifiers as a definition. Also, for the moment, the arguments to DEFINITIONS have to be expressions. Finally, when replacing DEFINITIONS the associativity is not changed. E.g., with PLUS(x,y) == x+y, the expression PLUS(2,3)*10 will evaluate to 50 (and not to 32 as with Atelier-B).
  • for a LET substitution, Atelier-B does not allow introduced identifiers to be used in the right-hand side of equations; ProB allows LET x,y BE x=2 & y=x*x IN ... END but only if the preference ALLOW_COMPLEX_LETS is set to TRUE.
  • ProB allows WHILE loops and sequential composition in abstract machines
  • ProB now allows the IF-THEN-ELSE for expressions and predicates: IF x<0 THEN -x ELSE x END
  • ProB now allows LET constructs for expressions and predicates
  • ProB allows btrue and bfalse as predicates.
  • ProB allows to use the Event-B relation operators <<->, <->>, <<->>
  • ProB allows escape codes (\n, \', \", see above) and supports UTF-8 characters in strings, and ProB allows multi-line string literals written using three apostrophes ("'string'") as well as template strings using three backquotes (e.g., ```1+2=${1+2}```)
  • ProB allows WHILE loops and sequential composition in abstract machines
  • Some of the sequence operators can be applied to strings (unless you set the preference STRING_AS_SEQUENCE to FALSE): size, rev, ^, conc
  • As of version 1.12.1 you can write Event-B style set comprehensions with an extra expression like {x•x:1..10|x*x}. You have to use the middle dot, the bullet (•) or a Unicode dot for this, though.
  • ProB comes with several libraries of external functions for string manipulations, mathematical functions, Hilbert's choice operator, etc.

Differences

  • for ProB the order of fields in a record is not relevant (internally the fields are sorted), Atelier-B reports a type error if the order of the name of the fields changes
  • Well-definedness: ProB will try to check if your predicates are well-defined during animation or model checking, but there is currently no guarantee that all well-definedness errors will be detected. To be on the safe side, you should ensure that your formulas are well-defined according to the left-to-right definition of well-definedness employed in Rodin for Event-B. ProB now has a static checker for well-definedness which you can use for this. Note, however, that ProB may re-order conjuncts if this improves well-definedness. For example, for x:0..3 & y=10/x & x /=0 ProB will not report an error as the conjunct x/=0 is processed before the division. Indeed, while this predicate is not well-defined according to Rodin's left-to-right rule, it is well-defined according to the more liberal commutative definition of well-definedness.

Limitations

  • Parsing: ProB will require parentheses around the comma, the relational composition, and parallel product operators. For example, you cannot write r2=rel;rel. You need to write r2=(rel;rel). This allows ProB to distinguish the relational composition from the sequential composition (or other uses of the semicolon). You also generally need to put BEGIN and END around the sequential composition operator, e.g., Op = BEGIN x:=1;y:=2 END.
  • Similarly, tuples without parentheses are not supported; write (a,b,c) instead of a,b,c
  • Unsupported Operators:
    • Trees and binary trees: most but not all tree operators (mirror, infix) are supported yet. These operators may disappear in future version of Atelier B and may also disappear from ProB.
    • VALUES: This clause of the IMPLEMENTATION machines is not yet fully supported;