Also see the following tutorials:

- Tutorial Rodin First Step
- Tutorial Rodin Parameters
- Tutorial Rodin Exporting
- Tutorial Symbolic Constants
- Tutorial Disprover
- Tutorial CSP First Step

Since version 1.2.7 of ProB (July 2008) you can also open Promela files with ProB. This mode is still experimental but already very usable and provides source-level highlighting during animation. The main purpose is to debug and animate Promela specifications in a user-friendly way. We do not plan to compete in terms of model checking speed with Spin (Spin compiles Promela to C code, ProB uses a Prolog interpreter). To animate a Promela model, simply open the file with the .pml or .prom extension with the "File->Open..." command. You will have to choose "Other Formalisms" or "All Files" in the filter pop-up-menu to be able to select the file.

You can also use ProB to animate and model check other specification languages by writing your own Prolog interpreter. To do this you should create a Prolog file with the .P extension and which defines three predicates:

- trans/3: this predicate should compute for every state (second argument), the outgoing transitions (first argument), and the resulting new states (third argument)
- prop/2: this predicate should compute the properties for the states of your system
- start/1: this defines the initial states of your system

For example, the following defines a system with two states (a and b) and two transitions (lock and unlock):

start(a). trans(lock,a,b). trans(unlock,b,a). prop(X,X).

These Prolog files can be loaded with ProB's open command (be sure to use the .P extension and to either choose "All files" or "Other Formalisms" in the file filtering menu).

Another simple example for a very basic process algebra is as follows:

% start(PossibleInitialState) start(choice(pref(a,stop),intl(pref(b,pref(c,stop)),pref(d,stop)))). % trans(Event, StateBefore, StateAfter) trans(A,pref(A,P),P). % action prefix trans(A,intl(P,Q),intl(P2,Q)) :- trans(A,P,P2). % interleave trans(A,intl(P,Q),intl(P,Q2)) :- trans(A,Q,Q2). trans(A,par(P,Q),par(P2,Q2)) :- trans(A,P,P2), trans(A,Q,Q2). % parallel composition trans(A,choice(P,Q),P2) :- trans(A,P,P2). % choice trans(A,choice(P,Q),Q2) :- trans(A,Q,Q2). % prop(State, PropertyOfState) prop(pref(A,P),prefix). prop(intl(P,Q),interleave). prop(A,A).

If you have a working interpreter, you can also contact the ProB developers in order for your interpreter to be included in the standard ProB distribution (in the style of the CSP-M or Promela interpreters). With this you can add syntax highlighting, error highlighting in the source code, highlighting during animation, support for new LTL properties,...

Another, slightly more elaborate example, is the following interpreter for regular expressions:

/* A simple animator for regular expressions */ start('|'('.'('*'(a),b) , '.'('*'(b),a))). trans(_,[],_) :- !,fail. trans(X,X,[]) :- atomic(X),!. trans(X,'|'(R1,R2),R) :- trans(X,R1,R) ; trans(X,R2,R). trans(X,'.'(R1,B),R) :- trans(X,R1,R2), gen_concat(R2,B,R). trans(X,'?'(R1),R) :- trans(X,R1,R) ; (X=epsilon,R=[]). trans(epsilon,'*'(_R1),[]). trans(X,'*'(R1),R) :- trans(X,R1,R2), gen_concat(R2,'*'(R1),R). trans(X,'+'(R1),R) :- trans(X,R1,R2), gen_concat(R2,'*'(R1),R). gen_concat(R1,R2,R) :- (R1=[] -> R = R2 ; R = '.'(R1,R2)). prop(X,X).

Finally, a more complex example is an encoding of the Rush Hour puzzle which also includes a graphical visualisation (using the `animation_function_result` predicate recognised by ProB as of version 1.4.0-rc3).

The following can be used to set up an animation image matrix with corresponding actions:

- animation_image(Nr,Path)
- animation_function_result(State,List) where List is a list of terms of the form ((Row,Col),Img) where Img is either a declared animation_image number or another Prolog term
- animation_image_right_click_transition(Row,Col,TransitionTemplate)
- animation_image_click_transition(FromRow,FromCol,ToRow,ToCol,ListOfTransitionTemplates,ImageNr)

In addition to classical B (aka B for software development), ProB also supports Event-B and the Rodin platform. ProB can be installed as a plugin for Rodin. Once installed, one can export contexts and models as *.eventb files and use them within ProB Tcl/Tk and the command-line version probcli.

See the tutorial pages for more information about using ProB for Event-B:

- Starting ProB for Rodin and First Animation Steps
- Important Parameters of ProB for Rodin
- Exporting Rodin Models for ProB Classic
- Using the Symbolic Contants Plugin
- Using the ProB (Dis-)Prover
- Visualization of LTL Counter-examples in Rodin
- Rodin Proof Obligations and Relation to ProB

The Rodin handbook also contains material about ProB:

Currently there are two versions of ProB available for Rodin.

The first one is based on the old Java API and supports Rodin 2.8 and Rodin 3.3. The update site comes built in into Rodin, see the tutorial on installing ProB for Rodin. Nightly releases of this versions are also available on the Download page.

The second, still experimental, one is based on the new ProB Java API (aka ProB 2.0). Because the UI components provided by the ProB Java API are based on web technologies, we were able create a simple plugin for the Rodin 3 tool that provides the user with all of the functionality of ProB within Rodin. The plugin uses views with embedded Eclipse SWT browsers to access the user interface components that are shipped with the ProB Java API library. Details about nightly releases of this versions is also available on the Download page.

There is now also a Multi-Simulation Plug-in available for Rodin. It enables discrete/continuous co-simulation.

This Plug-in is available at the update site http://nightly.cobra.cs.uni-duesseldorf.de/rodin_provereval/ and is capable to evaluate a variety of provers or tactics on a selection of proof obligations.

We also develop the Camille text-editor for Rodin. The update site (https://www3.hhu.de/stups/rodin/camille/nightly/) is preconfigured within Rodin. More information can be found on the Camille site at event-b.org.

ProB supports animation and model-checking for Event-B specifications.

To install the ProB plugin for Rodin, open the "Help" menu in Rodin and click "Install new software".

You see a drop-down list titled "Work with:" at the top of the install dialog. Choose the update site "ProB - ..." and click on "ProB for rodin2" in the field below. Click on the "Next" button at the button on the dialog and proceed with the installation as usual.

Alternativaly, one can use the Tcl/Tk version of ProB but Event-B models must be exported to an .eventb file first (see below).

You can start animation of a model (machine or context) by right-clicking on the model in the Event-B explorer. Choose "Start Animation / Model Checking".

**TODO:** Here we should add more details about the ProB perspective and views.

You can export a model (machine or context) to an .eventb - file by right-clicking on the model in the Event-B explorer. You can find the corresponding menu item right below the animation item.

Such a .eventb file can be opened by the command line and Tcl/Tk version of ProB.

ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):

- recursive datatypes (e.g. the List datatype)
- operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
- special annotated operators (see below)

Axiomatically defined operators are not supported without additional annotations.

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file (**P**roB **T**heory **M**apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form

operatorNameinternal {Tag}

where **Name** is the name of the operator in the theory and **Tag** is a ProB internal name.

The use of these tags is usually for experts only. In the theory file below, some of the theories are annotated.

Currently are the following tags supported:

Tag | Description | Expected type |
---|---|---|

closure1 | the transitive closure | POW(T**T) |

SIGMA | the sum of a set | POW(T**INT) |

PI | the product of a set | POW(T**INT) |

mu | ||

choose | ||

mkinat(op1,op2) |

**TODO**: to be continued...

An example project with theories: media:theories2.zip

**TODO**: A description of the supported parts.

ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):

- recursive datatypes (e.g. the List datatype)
- operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
- special annotated operators like transitive closure (see below)

Axiomatically defined operators are not supported without additional annotations.

An example project with theories: media:theories2.zip

The project contains the following theories:

- SUMandPRODUCT
- Contains two operators SUM and PRODUCT which take a set of the type POW(T**INT) as argument (with T being a type variable) and return the sum (resp.) product of all element's integer value.

The operators are annotated such that ProB uses an extra implementation.

- Seq
- The theory of sequences provides operators for sequences that are defined by direct definitions, thus supported by ProB.
- Real (unsupported)
- A theory of real numbers, currently unsupported by ProB.
- Natural
- A theory of inductive naturals (defined by a constant zero and a successor function).
- The mkinat operator is annotated such that ProB uses an explicit implementation.
- List
- A theory of lists that are either empty or have a head and a tail
- FixPoint (not really supported)
- The theory is defined by direct definitions but they usually get so complex that ProB cannot cope with them.
- closure
- The operator for transitive closure is supported by ProB.
- The operator is annotated such that ProB uses the classical B implementation.
- Card (contains no operators or data types)
- Contains theorem about set cardinalities.
- BoolOps
- Operators on Booleans (e.g. AND, OR) are defined by direct definitions and as such supported by ProB.
- BinaryTree
- Binary Trees are supported by ProB.

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file (**P**roB **T**heory **M**apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form

operatorNameinternal {Tag}

where **Name** is the name of the operator in the theory and **Tag** is a ProB internal name.

Currently are the following tags supported (with T being an arbitrary type):

Tag | Description | Expected type | Return type |
---|---|---|---|

closure1 | the transitive closure | POW(T**T) | POW(T**T) |

SIGMA | the sum of a set | POW(T**INT) | INT |

PI | the product of a set | POW(T**INT) | INT |

mu | returns the element of a singleton set | POW(T) | T |

choose | returns (deterministically) one element of a non-emtpy set | POW(T) | T |

mkinat(zero,succ) | returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) | INT | Inductive Nat |

As of version 1.12 (mid-september 2022) ProB also transparently accepts `POW(INT)` as type for SIGMA and PI.
It now also accepts many of its external functions as tag names, such as the
the functions from LibraryStrings.def or LibraryReals.def.
For example, here we map the operator plus to ProB's external function RADD for adding two reals:

operator "plus" internal {RADD}

If you set the preference ` AUTO_DETECT_THEORY_MAPPING` to TRUE then ProB will work with several standard Rodin theories even without a .ptm file in the workspace.

As of version 1.13 (November 2023) ProB also accepts literals as well as formulas between dollars in the .ptm files. For example, here the operator Rone is defined by the literal 1.0 and the operator RRealPlus by an expression (a set comprehension of the positive reals annotated with the symbolic pragma):

operator "Rone" internal {1.0} operator "RRealPlus" internal {$/*@symbolic*/ {x|x:REAL & x>= 0.0}$}

In case the **.ptm** file is missing, you will get an error message such as the following one:

Axiomatic defined operator "SUM" not recognized.

For reference, here are the contents of some of the **.ptm** files.
In case of an error message, you can copy these files into your Theory Projects (e.g., using Drag & Drop) and then refresh (F5). After that animation with ProB should work.

- SUMandPRODUCT.ptm

operator "SUM" internal {SIGMA} operator "PRODUCT" internal {PI}

- closure.ptm

operator "cls" internal {closure1}

- Natural.ptm

operator "mk_iNAT" internal {mkinat}

Here are the contents for a Reals theory by Guillaume Dupont:

operator "RReal" internal {REAL} operator "Rone" internal {1.0} operator "Rzero" internal {zero} operator "Rtwo" internal {two} operator "plus" internal {RADD} operator "times" internal {RMUL} operator "minus" internal {RSUB} operator "lt" internal {RLT} operator "leq" internal {RLEQ} operator "gt" internal {RGT} operator "geq" internal {RGEQ} operator "uminus" internal {RSUB} operator "inverse" internal {RINV} operator "divide" internal {RDIV} operator "abs" internal {RABS} operator "sqrt" internal {RSQRT} operator "Rmax" internal {RMAXIMUM} operator "Rmin" internal {RMINIMUM} operator "RRealPlus" internal {$/*@symbolic*/ {x|x:REAL & x>= 0.0}$} operator "RRealMinus" internal {$/*@symbolic*/ {x|x:REAL & x<= 0.0}$} operator "RRealStar" internal {$/*@symbolic*/ {x|x:REAL & x /= 0.0}$} operator "RRealPlusStar" internal {$/*@symbolic*/ {x|x:REAL & x> 0.0}$} operator "RRealMinusStar" internal {$/*@symbolic*/ {x|x:REAL & x< 0.0}$}

ProB supports machine readable CSP^{[1]} as supported by FDR and ProBE. CSP files can be animated and model checked on their own simply by opening a file ending with ".csp".

You can also use a CSP file to guide a B machine by first opening the B machine and then using the "Open Special" sub-menu of the File menu:

- use CSP file: uses the CSP file to control the current B machine (see below)
- use default CSP file: trys to use a CSP with the same name as the current B machine to control it

ProB now supports FDR and ProBE compatible CSP-M syntax, with the following outstanding issues

- currying and lambda expressions have only been partially tested
- extensions and productions are not yet supported (but {| |} is)
- the priority of rename compared to external choice is unfortunately different than in FDR; please use parentheses
- mixing of closure with other set operations (especially diff) is not yet fully supported
- input patterns can only contain variables, tuples, integers and constants (ch?(x,1) is ok, ch?(y+1,x) not). Also, for a record, all arguments must be provided (e.g., for datatype r.Val.Val you have to write r?x?y you cannot write r?xy). Finally, for the moment within "ch? x.y:Set" the ":Set" associates only with y; if you want to check that "x.y" is in Set you need to write: "ch?(x.y):Set.
- channel declarations can either use associative dot tuples or non-associative tuples but not yet both. Also, sets of tuples as channel types will not work the same way as in FDR. I.e., for channel a:LinkData you should not use LinkData = {0.0, 0.1, 1.0, 1.1} but rather nametype LinkData = {0,1}.{0,1}.

Also, in the first phase we have striven for compatibility and coverage. We still need to tune the animator and model checker for efficiency (there are few known bottlenecks which will be improved, especially with deeply nested CSP synchronization constructs).

To use this feature of ProB: first open a B Machine, then select "Use CSP File to Guide B..." or "Use Default CSP File" in the "Open Special" submenu of the File menu (you must be in normal user mode to see it).

The CSP file should define a process called "MAIN". This process will be executed in parallel with the B machine. The synchronization between the B machine and the CSP specification is as follows:

- CSP events that have the same name as B Operations will synchronize with B; CSP events that have the same name as a B Variable or Constant can be used to inspect the current value of these, all other CSP events can happen independently of B. In CSP terms the CSP and B are composed as follows:
CSP [| {op1,...,opn} |] B

where op1,...,opn are the visible operations defined in the B machine. - CSP events do not need to provide all arguments of B operations:

add!1 -> will match add(1,1) or add(1,2) or ... (supposing add has 2 parameters in B) add -> will match add(1,2), add(2,1), ...

add!1!2 -> will only match add(1,2)

- B Output arguments are specified at the end
lookup!X!2 will match lookup(X) --> 2

Note however, that for non-deterministic operations you generally should only retrieve the output value using a ? and not match against it using a !. Otherwise, the non-determinism of the B operation will be treated as an external choice for the CSP. So, if lookup is non-deterministic then we should do lookup!X?Res -> Res=2 & Cont rather than lookup!X!2 -> Cont. - If you have a variable called vv, then you can use vv?VAL to get the value of vv. You can also use, for example, vv!X to check that the value is equal to X. If vv is a relation or function, then you can also use two values on the channel to check for particular tuples in the relation. For example, use vv!3?Y to check whether tuples (3,Y) are in the relation vv (there will be one possible synchronisation per such value).
- see the file "bookstore_guide.csp" in the provided Machines directory for an example.

For the syntax definition see CSP-M Syntax

From the command line, you can specify a CSP File that should be used to guide the B machine with

-csp-guide <Filename>

(This feature is included since version 1.3.5-beta7.)

Note: you can use the command "Summary of CSP syntax" in ProB's help menu to get an up-to-date list of the supported syntax, along with current limitations.

- `Process = ProcessExpression`

- `STOP` deadlocking process
- `SKIP` terminating process
- `CHAOS(a)` a: set of channel expressions
- `ch->P` simple action prefix where ch is a channel name possibly followed by a sequence of outputs "!v" and input "?VAR", where v is a value expression and VAR a variable identifier
- `ch?x:v->P` action prefix with set of accepted values
- `P ; Q` sequential composition
- `P ||| Q` interleaving
- `P [] Q` external choice
- `P |~| Q` internal choice
- `P /\ Q` interrupt
- `p [> Q` untimed timeout
- `P [| a |] Q` parallel composition with synchronisation on set of channel expressions a
- `P [ a || a' ] Q` alphabetised parallel
- `P [ c<->c' ] Q` linked parallel
- `P \ a` hiding of channel expressions in c
- `P [[ c<-c' ]]` renaming of channels c into c'
- `if B then P else Q`
- `b & P` guard using a boolean expression b
- `[]x:v@P` replicated external choice (x: variable, v: set value expression)
- `|~|x:v@P` replicated internal choice (x: variable, v: set value expression)
- `|||x:v@P` replicated interleave (x: variable, v: set value expression)
- `;x:s@P` replicated sequential composition (s: sequence expression)
- `||x:v@[a']P` replicated alphabetised parallel
- `[| a |]x:s@P` replicated sharing
- `[c<->c']x:s@P` replicated linked parallel (sequence s must be non empty)
- `let f1=E1 ... fk=Ek within P`

- `true`
- `false`
- `b1 and b2` (`b1 && b2` also accepted but not in CSP-M)
- `b1 or b2` (`b1 || b2` also accepted but not in CSP-M)
- `b1 <=> b2` equivalence
- `b1 => b2` implication
- `not b`
- `v==w` equality of values
- `v!=w` disequality of values
- `v<w,v>w` strict ordering
- `v<=w,v>=w` non-strict ordering (v=<w also accepted)
- `member(v,w)` set membership check
- `empty(a)` set emptiness check
- `null(s)` sequence emptiness check
- `elem(x,s)` sequence member check

- `v+w`, `v-w` addition and subtraction
- `v*w` multiplication
- `v/w` integer division
- `v % w` division remainder
- `bool(b)` convert a boolean expression into a boolean value
- `{v,w,...}` enumerated sets
- `{m..n}` closed range
- `{m..}` open range
- `union(v,w)` set union
- `inter(v,w)` set intersection
- `diff(v,w)` set difference
- `Union(A)` generalized union of a set of sets
- `Inter(A)` generalized intersection
- `card(a)` cardinality of a
- `{x1,...,xn | x<-a,b}`
- `Events` all channel expressions on all declared channels
- `{| ... |}` closure of set of channel expressions
- `Set(a)` all subsets of a
- `<>` empty sequence
- `<v,w,...>` explicit sequence
- `<m..n>` closed range sequence
- `<m..>` open range sequence
- `<....>^s` sequence concatenation (first or last arg has to be an explicit sequence for patterns)
- `#s`, `length(s)`
- `head(s)`
- `tail(s)`
- `concat(s)`
- `set(s)` convert sequence into set

- `-- comment until end of line`
- `{- arbitrary comment -}`

- `transparent f` where f is a unary function which will then on be ignored by ProB
- `{-# assert_ltl "f" "comment" #-}` where
*f*is an LTL-formula and*comment*is an arbitrary comment, which is optional - `{-# assert_ctl "f" "comment" #-}` where
*f*is a CTL-formula and*comment*is an arbitrary comment, which is optional

As of version 1.3.4, ProB provides support for refinement checking and various other assertions (deadlock, divergence, determinism, and LTL/CTL assertions) of CSP-M specifications. In this tutorial we give a short overview of the ProB’s implementations and features for checking CSP assertions. In the Tcl/Tk interface of ProB, CSP assertions can be assembled and checked in the *CSP Assertions Viewer*. A description of the *CSP Assertions Viewer* is also given.

ProB provides support for checking almost all types of CSP-M assertions that can be checked within FDR2. Besides the assertion types that can be checked in FDR2, in ProB one also can check temporal properties on processes expressed by means of LTL and CTL formulae.^{[1]} The following types of assertions are supported in ProB:

**Refinement**

Refinement is one of the fundamental notions for construction and verification of systems specified in CSP. Given two CSP processes *P* and *Q* one can state in ProB the property that process *Q* is an ‘m’ refinement of *P* by the following assertion declaration:

assert P [m= Q

where ‘m’ indicates one of the following types of comparison: ‘T’ for traces, ‘F’ for failures, ‘FD’ for failures-divergence, ‘R’ for refusals, and ‘RD’ for ‘refusals-divergence’. Note that the refinement types ‘V’ (revivals) and ‘VD’ (revivals-divergence) that are part of the refinement assertions supported by FDR2 are yet not supported by ProB.

**Deadlock**

Stating assertions about CSP processes to be deadlock-free is possible by the following assertion declaration:

assert P :[deadlock free [m]]

where *P* is a process expression and ‘m’ indicates one of the following models: ‘F’ (failures) and ‘FD’ (failures-divergence).

**Determinism**

Stating assertions about CSP processes to be deterministic is possible by the following assertion declaration:

assert P :[deterministic [m]]

where *P* is a process expression and ‘m’ one of the following models: ‘F’ (failures) and ‘FD’ (failures-divergence).

**Livelock**

Stating assertions about CSP processes to be livelock-free is possible by the following assertion declaration:

assert P :[livelock free]

where *P* is a process expression.

**Temporal Properties**

In ProB it is also possible to make assertions about temporal properties of CSP processes both in LTL and CTL. Basically, one wants to check whether some process *P* satisfies a formula *f* expressed in a temporal logic (denoted by `P |= f`).

To check whether a process *P* satisfies an LTL formula *f* write the following declaration:

assert P |= LTL: “f”

Note that *f* must be placed between quotes and that the satisfaction relation |= is immediately followed by `LTL:`. ProB supports LTL^{[e]}, an extended version of LTL which provides additionally support for making propositions on transitions. The following LTL^{[e]} syntax for CSP-M specifications can be outlined by the following rules:

- Atomic propositions:
- To check if an event `evt` is enabled in a state use `e(evt)`

- Transition propositions:
- To check whether an event `evt` is executed use `[evt]`

- Logical operators
- `true` and `false`
- `not`: negation
- `&`,`or` and `=>`: conjunction, disjunction and implication

- Temporal operators:
- `G f`: globally
- `F f`: finally
- `X f`: next
- `f U g`: until
- `f W g`: weak-until
- `f R g`: release

- Fairness operators:
- `WF(evt)` or `wf(evt)`: weak fairness, where `evt` is an event
- `SF(evt)` or `sf(evt)`: strong fairness, where `evt` is an event
- `WEF` and `SEF` for checking LTL
^{[e]}formulae on executions that are strongly and weakly fair with respect to all events, respectively

An LTL^{[e]} formula *f* is satisfied by some CSP process *P* if all executions of *P* satisfy *f*. If there is an execution of *P* which violates the property *f*, then the test `P |= f` fails by providing a counterexample. Depending on whether *f* expresses, a safety or liveness property, a finite path or a path in a lasso-form (, i.e. a path leading to a cycle) is returned as a counterexample, respectively.

Note that ProB supports also Past-LTL^{[e]}. Past-LTL^{[e]}, however, may be considered to be inappropriate for LTL assertions since the goal of this type of assertions is usually to check whether all executions starting at the initial states of the process satisfy the respective LTL^{[e]} formula.

To check whether a process *P* satisfies a CTL formula *f* the following assertion should be made:

assert P |= CTL: “f”

As for LTL, CTL formulae should be put in between quotes. The CTL syntax for CSP-M specifications could be summarised as follows:

- Atomic propositions:
- To check if an event `evt` is enabled in a state use `e(evt)`

- Transition propositions:
- To check whether an event `evt` is executed use `[evt]`

- State formulae, where f, f1 and f2 are path formulae:
- true | false | `not` f | f1 `&` f2 | f1 `or` f2 | f1 `=>` f2,
- E f : path quantifier ``, pronounced `for some path`
- A f : path quantifier ``, pronounced `for all paths`

- Path formulae, where g, g1 and g2 are state formulae:
- `X g`: next
- `g1 U g2`: until
- `G g`: globally
- `F g`: finally

- Next executed event:
- `EX [e] true`:

Note that these two types of assertions, the LTL and CTL assertions, are not part of the CSP-M language supported by FDR2. Loading a CSP-M file in FDR2 having assertion declarations of this form will exit with a syntax error. Bear in mind to remove or comment out such LTL/CTL assertions in the CSP-M file before loading it in FDR2.

When a CSP-M specification is loaded one can open the *CSP Assertion Viewer* either from the menu bar of the main window by selecting the `Check CSP-M Assertions` command in the `Verify` menu or from the Refinement button in the ‘’State Properties’’ pane. The viewer looks as follows:

The *CSP Assertion Viewer* of ProB has a similar design to the graphical user interface of FDR2. It consists basically of three main components: a menu bar, a list box and a tab pane. In the following each of the components and their corresponding functionalities are thoroughly described.

**The Menu Bar**

The menu bar is placed at the top of the window. On OS X, it is placed at the top of the screen. The menu bar includes several menus providing commands for adjusting, executing and changing the items in the list box, as well as some (standard) options for re-loading the model, saving the items to an external file or the loaded file, and launching some external tools related with the domain in which the list items are checked. Each menu can be popped up by a click with Mouse-1 (usually the left mouse button). The menu bar consists of the following menus and menu commands:

**File***Reopen File*: Reopening (re-reading and re-loading) the currently loaded file, incorporating any changes that may have been made since the file was last loaded.*Copy new Assertions to File*: All assertions that have been added to the list box since the currently loaded file was last read will be written to the file, i.e. all assertions that are yet not in the file are appended to it.*Save Assertions to External File*: Selecting the option opens a standard Tk dialog box requesting a name of a file in which the assertions and their results in the list box could be saved.*Exit*: Closing the CSP Assertion Viewer. Any assertion check results and any recently added assertions from the Tab Pane will get lost. The user will not be prompted to save these to the source file or an external file.

**Font**

Changing the font settings of the elements in the list box. Each of the items of this menu is a cascading menu that provides a number of options to be selected. The currently selected option in the cascading menu is marked by a tick symbol (✓).*Family-Name*: Change the font family of the text in the list box. There are currently four font families that could be chosen: Arial, Curier, Helvetica, and Times. Default font is Curier.*Size*: Change the font size of the text in the list box. Default font size is 10.*Background*: Change the background color of the list box. Default background color is Gray90.

**Assertions**

The menu provides a list of commands for checking different types of assertions. In case a particular type of assertions is checked the respective command checks only these assertions that are not checked yet.*Uncheck All Assertions*: Set the status of all assertions in the list box to non-checked (`?`).*Delete All Assertions*: Delete all assertions in the list box.*Check All Refinement…*: The item is a cascading menu and provides commands to check all assertions of one of the following supported refinement types: Traces, Failures, Failures-Divergence, Refusals, and Refusals-Divergence.*Check Processes for…*: The item is a cascading menu and provides commands to check all assertions of the following supported types of checks: Deadlock, Determinism and Livelock.*Check All LTL Assertions*: Selecting this command causes ProB to check all LTL assertions in the list box that are not checked yet.*Check All CTL Assertions*: Selecting this command causes ProB to check all CTL assertions in the list box that are not checked yet.*Check All Assertions*: Selecting this command causes ProB to check of all assertions in the list box that are not checked yet.

**External Tools***Open Specification with FDR*: Open the currently loaded CSP-M specification in FDR2. The FDR2 tool is launched with the currently loaded specification in case the FDR2 is installed and the correct path to the `fdr2` command is set for the respective preference `Path to the FDR2 tool`. The value of the `Path to the FDR2 tool` preference can be changed from the “CSP Preferences…” window which can be opened by selecting the `CSP Preferences…` command in `Preferences` menu of the main window.*Evaluate with CSPM-Interpreter*: Selecting this command opens a console in which one can evaluate CSP-M expressions using the CSP-M interpreter. The CSP-M interpreter is an external tool implemented independently from ProB. CSP-M expression can be evaluated if the `cspm` tool is installed and the path to the cspm-command is set for the respective preference `Path to CSPM tool`. The command is obsolete and its removal is considered in future.

**The Assertion List Box**

This part of the viewer lists all assertions stated in the currently loaded CSP-M specification and provides a set of features for checking, manipulating, and debugging of CSP assertions in the list. To each statement in the assertion list box a symbol is assigned, placed on the left side of it, that reveals the current status of the statement in the viewer:

- ? - Assertion not checked yet.
- ✔ - Assertion check completed successfully.
- ✘ - Assertion check completed, but a counterexample was found to the stated property. The debugger can be used to explore the reason why the property does not hold.
- ⌚ - Assertion is currently checked.
- ! - The check of the assertion not completed for some reason. Possible causes for the interruption may be:
- Syntax error in the property was detected;
- Assertion check failed because of missing implementation;
- Assertion check interrupted by user.

Note that in case of an LTL and a CTL assertion the check could fail to complete because of a syntax error in the respective formula. If an assertion check fails to complete an error box is popped up displaying an error message, which indicates why the assertion check could not be completed.

An assertion can be selected by clicking on it with Mouse-1 and checked by double-clicking on it with Mouse-1. Alternatively, selecting an assertion and then pressing the Enter key can start the respective assertion check. When an assertion check is in progress, the assertion will be marked by the clock symbol (⌚). If the assertion check is completed without interrupting it, a new status is assigned to the assertion: tick symbol (✔) indicating that the assertion was completed successfully or cross symbol (✘) indicating that a counterexample was found for the stated property. In case that the status is cross the counterexample can be explored by (second) double-click with Mouse-1 on the assertion or by selecting the assertion and then pressing the Enter key. If the respective assertion is negated, i.e. there is `not` in front of the assertion property, and marked with a cross, then no counterexample can be explored as the proper statement holds.

The list box is equipped with a contextual menu (or a pop-up menu), which appears when you right-click on an assertion in the list. Depending on the type and the status of the assertion the contextual menu provides options for checking, debugging, modifying the respective assertion, as well as various other options. Take, for example, the selected assertion on which the contextual menu is popped up in the picture below.

The assertion "`ASSYSTEM |= LTL: “GF [eats.0]”`" intends to check if the process ASSYSTEM satisfies the LTL formula "`GF [eats.0]`". For the selected assertion above, for example, the options `Show LTL Counterexample` and `Show LTL Counterexample in State Space` are enabled as a counterexample was found for the check. On the other hand, the options `Check Assertion` and `Interrupt Assertion` are disabled as the assertion check was completed.

The contextual menu has in general the following options:

The following options affect only the assertion being selected.

**Debug or Show LTL/CTL Counterexample…**: Opens the graphical viewer for exploring the counterexample that was found for the respective LTL assertion check. Option is enabled if the assertion is not negated and its status is cross (✘), or if the assertion is negated and its status is tick (✔). Option appears if the assertion type is an LTL assertion or a CTL assertion.**Debug Assertion**: Opens a trace-failure debugger window showing the reason why the corresponding assertion check failed. Option is enabled if the assertion is not negated and its status is cross (✘), or if the assertion is negated and its status is tick (✔). Option available for all types of assertions except for LTL and CTL assertions.**Check Assertion**: Starts immediately the check of the assertion being selected before right clicking on it.**Interrupt Assertion Check**: Interrupts the current assertion check.**Uncheck Assertion**: If the assertion was checked and the result of the check is different from question mark (?), then the status of the assertion will be reset to question mark. Option is enabled only if the assertion result is different from question mark.**Delete Assertion**: Removes the selected item from the assertion list.**Negate Assertion**: Negates the respective assertion. If the result of the (proper) assertion check is cross (✘), then the result of the negated assertion becomes tick (✔). Otherwise, if the result of the (proper) assertion is tick (✔), the negated assertion becomes cross (✘).**Swap Processes**: Option available only for refinement assertions. Performing the command causes the attachment of a new refinement assertion in which the process expressions on both sides of the refinement operator `[m=` are swapped. If, for example, we execute ‘’Swap Processes’’ on the assertion "`P [T= Q`", the command adds to the list of assertions the assertion "`Q [T= P`".

The following options affect all assertions in the list box.

**Check All Assertions**: The command causes the check of all assertions in the list box. The assertions that are already checked would not be checked again.**Uncheck All Assertions**: The status of all assertions in the list box is reset to question mark.**Delete All Assertions**: All entries in the list box are removed. As a result the message “No assertions were added.” appears in the list box.

Other options. The following options have no impact on the assertions in the list box.

**Summary of the CSP Syntax**: Opens a window in which the summary of the CSP-M syntax and features supported by the ProB tool is given.**Evaluate CSP Expressions**: Opens the Eval console in which CSP expressions can be evaluated.**Open Specification with FDR**: Opens the currently loaded CSP-M specification in FDR2. The FDR2 tool is launched with the currently loaded specification if FDR2 is installed and the correct path to the `fdr2` command is set for the respective preference `Path to the FDR2 tool`. The value of the `Path to the FDR2 tool` preference can be changed from the “CSP Preferences…” window which can be opened by selecting the `CSP Preferences…` command in `Preferences` menu of the main window.

**The Tab Pane**

The tab pane is placed at the bottom of the window and enables the user to construct and check properties of processes of the currently loaded CSP-M file without adding explicitly assertions to the file.

There are overall six tab pages. Each tab page is used to build up new assertion statements. The tab pages provide selectors, entries and command buttons for assembling, adding and checking new assertions. In each of the selectors all possible processes of the loaded CSP-M file are accessible. It is also possible to specify new process expressions by entering these in the respective entry of the process selector. The tab pages for creating LTL and CTL assertions provide additionally an appropriate entry for specifying the according LTL and CTL formula intended to be checked on the specified process, respectively.

Each tab page is equipped with the following command buttons:

**Add**: Attaching a new assertion to the list of assertions in the list box. If the entry in one of the selectors is empty no assertion will be added to list box and a warning message will appear informing the user that some of the entries were not specified. If the entered assertion in the tab page is already in the list box, then a warning box appears informing the user that the assertion is already in the list box. If the assertion is present in the list box it will not be added.**Check**: Attaching a new assertion to the list of assertions in the list box and immediately starting checking the assertion. If the assertion is already in the list box, then the user will be informed that the assertion is already in the list box and in case it is not checked yet its check will be started.**Cancel/Interrupt**: Closes the window or interrupts an assertion check. In case the “Cancel” command is executed all checks and new assertions will get lost. If an assertion is currently checked, then the button command “Cancel” is replaced by another button command ‘’Interrupt’’, which causes the interruption of the current assertion check when the button is clicked on.

In case an assertion check has failed the user can explore the reason for the assertion violation. If the corresponding assertion is not negated and after finishing the assertion check is marked by cross, then this is an indication that ProB has found a counterexample for the check. The counterexample can be explored by a second double-click with the ‘Mouse-1’ button or by selecting the assertion and then pressing the ‘Enter’ button. Depending on the type of the assertion and the type of the counterexample a corresponding debugging window is opened.

If a CSP process violates an LTL formula or a universally quantified CTL formula, then by performing a second double-click on the respective assertion one can explore the provided counterexample by means of the graphical viewer (Graphical Viewer).

In the following we give an overview of the features for debugging counterexamples being found for different refinement checks. Consider the following CSP processes:

P = a -> b -> c -> STOP

Q = a -> (b -> Q [] c -> Q)

R = a -> b -> R

If we intend to check whether P is deadlock free, then we can state the assertion

`assert P :[deadlock free [F]]`.

The check of the assertion will finish by marking the assertion in the list box with a cross symbol (✘). The cross symbol indicates that a counterexample was found for the assertion check. The counterexample is basically given by the trace as obviously `P` reaches a deadlock state after performing the trace . Providing a second double-click on the assertion will open the following debugging window:

Considering the CSP processes `Q` and `R` one can see or check that `R` is a trace refinement of `Q` since `R` performs the same set of traces as `Q`. Thus, the assertion check for `Q [T= R` will mark the assertion statement in the list box by a tick symbol (✔). On the other hand, checking the assertion `R [T= Q` will find a counterexample for the refinement check. Performing a second double-click on the item `R [T= Q` will open the following trace debugger window with the counterexample displayed in it:

A counterexample of a trace-refinement assertion is a trace leading to a state in which the implementation process performs an event that the specification process cannot perform. In the example above both processes `P` and `Q` perform the trace and reach states in which the implementation process can perform an event that is not offered by the specification process *R*. One can easily deduce from the picture above that `Q` performs after `a` the event `c` which is not offered by `R` as `R` can perform only `b` after `a`. In the left most column `Accept` the debugger window lists all possible events that are offered by the specification process after performing the trace given in the `Trace` column next to `Accepts`.

As we already mentioned above `R` is a trace-refinement of `Q`. On the other hand, checking whether `R` is a failures-refinement of `Q` will produce a counterexample since `R` refuses the event `c` that is offered by Q after executing `a`. Accordingly, the counterexample will be illustrated within the following trace debugger window:

These are basically the three types of debugging windows that will appear when debugging a counterexample for an assertion check in case the respective assertion is not an LTL or a CTL assertion. When a counterexample for an LTL assertion is found it will be explored in the graphical viewer, the same graphical viewer that is used for visualizing the state space models in ProB.

Let us observe again the CSP process `Q` and suppose we want to check whether `Q` satisfies the LTL formula `F [c]`. Then, the respective LTL assertion is declared as follows:

`assert Q |= LTL: “F [c]”`

The assertion check will produce a counterexample as `Q` obviously reaches a cycle “(b -> a)+” that violates the property “F [c]”. Performing a second double-click on the assertion will display the following state space graph in the graphical viewer:

In the figure above, the nodes and the transitions of the respective counterexample "a -> (b -> a)+" are colored in red.

It is also possible to check CSP assertions with the command line version of ProB. The command has the following syntax:

probcli -csp_assertion "A" File

where *A* is a CSP assertion and *File* the path to the CSP file. For example, if we want to check the refinement assertion ``P [T= Q`` on some CSP specification `example.csp`, then we can do this by running the ProB command line version with the following options:

probcli -csp_assertion "P [T= Q" example.csp

Note that the assertion should be placed between quotes. In addition, when an assertion is checked with the '-csp_assertion' option the keyword **assert** should be omitted.

Notice that for checking LTL and CTL assertions from the command line you need to escape the double quotes (") wrapping the respective LTL/CTL formula by means of a backslash \.

probcli -csp_assertion "Q |= LTL: \"F [c]\"" example.csp

- ↑ ProB provides support for LTL and CTL model checking (citations needed).

As of version 1.8 ProB provides support to load Alloy models. The Alloy models are translated to B machines by a Java frontend.

This work and web page is still experimental.

The work is based on a translation of the specification language Alloy to classical B. The translation allows us to load Alloy models into ProB in order to find solutions to the model's constraints. The translation is syntax-directed and closely follows the Alloy grammar. Each Alloy construct is translated into a semantically equivalent component of the B language. In addition to basic Alloy constructs, our approach supports integers and orderings.

Alloy2B is included as of version 1.8.2 of ProB.

You can build Alloy2B yourself:

- Clone or download Alloy2B project on Github.
- Make jar file (gradle build) and
- put resulting alloy2b-*.jar file into ProB's lib folder.

module queens open util/integer sig queen { x:Int, x':Int, y:Int } { x >= 1 y >= 1 x <= #queen y <= #queen x' >=1 x' <= #queen x' = minus[plus[#queen,1],x] } fact { all q:queen, q':(queen-q) { ! q.x = q'.x ! q.y = q'.y ! plus[q.x,q.y] = plus[q'.x,q'.y] ! plus[q.x',q.y] = plus[q'.x',q'.y] }} pred show {} run show for exactly 4 queen, 5 int

This can be loaded in ProB, as shown in the following screenshot. To run the "show" command you have to use "Find Sequence..." command for "run_show" in the "Constraint-Based Checking" submenu of the "Verify" menu.

Internally the Alloy model is translated to the following B model:

MACHINE alloytranslation SETS /* deferred */ queen CONCRETE_CONSTANTS x, x_, y /* PROMOTED OPERATIONS run0 */ PROPERTIES x : queen --> INTEGER & x_ : queen --> INTEGER & y : queen --> INTEGER & !this.(this : queen => x(this) >= 1 & y(this) >= 1 & x(this) <= card(queen) & y(this) <= card(queen) & x_(this) >= 1 & x_(this) <= card(queen) & x_(this) = (card(queen) + 1) - x(this) ) & card(queen) = 4 & !(q,q_).(q_ : queen - {q} => not(x(q) = x(q_)) & not(y(q) = y(q_)) & not(x(q) + y(q) = x( q_) + y(q_)) & not(x_(q) + y(q) = x_(q_) + y(q_))) INITIALISATION skip OPERATIONS run0 = PRE card(queen) = 4 & !(q,q_).(q_ : queen - {q} => not(x(q) = x(q_)) & not(y(q) = y(q_)) & not(x(q) + y(q) = x(q_) + y(q_)) & not(x_(q) + y(q) = x_(q_) + y(q_))) THEN skip END /* DEFINITIONS PREDICATE show; */ END

module river_crossing open util/ordering[State] abstract sig Object { eats: set Object } one sig Farmer, Fox, Chicken, Grain extends Object {} fact { eats = Fox->Chicken + Chicken->Grain} sig State { near, far: set Object } fact { first.near = Object && no first.far } pred crossRiver [from, from', to, to': set Object] { one x: from | { from' = from - x - Farmer - from'.eats to' = to + x + Farmer } } fact { all s: State, s': s.next { Farmer in s.near => crossRiver [s.near, s'.near, s.far, s'.far] else crossRiver [s.far, s'.far, s.near, s'.near] } } run { last.far=Object } for exactly 8 State

This can be loaded in ProB, as shown in the following screenshot. To run the "show" command you have to use "Find Sequence..." command for "run_show" in the "Constraint-Based Checking" submenu of the "Verify" menu (after enabling Kodkod in the Preferences menu).

Internally the Alloy model is translated to the following B model:

/*@ generated */ MACHINE river_crossing SETS Object_ CONSTANTS Farmer_, Fox_, Chicken_, Grain_, eats_Object, near_State, far_State DEFINITIONS crossRiver_(from_,from__,to_,to__) == from_ <: Object_ & from__ <: Object_ & to_ <: Object_ & to__ <: Object_ & (card({x_ | {x_} <: from_ & (((from__ = (((from_ - {x_}) - {Farmer_}) - eats_Object[from__]))) & ((to__ = ((to_ \/ {x_}) \/ {Farmer_}))))}) = 1) ; next_State_(s) == {x|x=s+1 & x:State_} ; nexts_State_(s) == {x|x>s & x:State_} ; prev_State_(s) == {x|x=s-1 & x:State_} ; prevs_State_(s) == {x|x<s & x:State_} ; State_ == 0..7 PROPERTIES {Farmer_} <: Object_ & {Fox_} <: Object_ & {Chicken_} <: Object_ & {Grain_} <: Object_ & ((eats_Object = (({Fox_} * {Chicken_}) \/ ({Chicken_} * {Grain_})))) & (((near_State[{min(State_)}] = Object_) & far_State[{min(State_)}] = {})) & (!(s_, s__).({s_} <: State_ & {s__} <: next_State_(s_) => ((({Farmer_} <: near_State[{s_}]) => crossRiver_(near_State[{s_}], near_State[{s__}], far_State[{s_}], far_State[{s__}])) & (not(({Farmer_} <: near_State[{s_}])) => crossRiver_(far_State[{s_}], far_State[{s__}], near_State[{s_}], near_State[{s__}]))))) & Farmer_ /= Fox_ & Farmer_ /= Chicken_ & Farmer_ /= Grain_ & Fox_ /= Chicken_ & Fox_ /= Grain_ & Chicken_ /= Grain_ & {Farmer_} \/ {Fox_} \/ {Chicken_} \/ {Grain_} = Object_ & eats_Object : Object_ <-> Object_ & near_State : State_ <-> Object_ & far_State : State_ <-> Object_ OPERATIONS run_2 = PRE (far_State[{max(State_)}] = Object_) THEN skip END END

sig Object {} sig Vars { src,dst : Object } pred move (v, v': Vars, n: Object) { v.src+v.dst = Object n in v.src v'.src = v.src - n v'.dst = v.dst + n } assert add_preserves_inv { all v, v': Vars, n: Object | move [v,v',n] implies v'.src+v'.dst = Object } check add_preserves_inv for 3

Note that our translation does not (yet) generate an idiomatic B encoding, with `move` as B operation

andsrc+dst=Objectas invariant: it generates a check operation encoding the predicateadd_preserves_invwith universal quantification.

Below we shoe the B machine we have input into AtelierB. It was obtained by pretty-printing from \prob, and putting the negated guard

of theadd_preserves_invinto an assertion (so that AtelierB generates the desired proof obligation).

MACHINE alloytranslation SETS /* deferred */ Object_; Vars_ CONCRETE_CONSTANTS src_Vars, dst_Vars PROPERTIES src_Vars : Vars_ --> Object_ & dst_Vars : Vars_ --> Object_ ASSERTIONS !(v_,v__,n_).(v_ : Vars_ & v__ : Vars_ & n_ : Object_ => (src_Vars[{v_}] \/ dst_Vars[{v_}] = Object_ & v_ |-> n_ : src_Vars & src_Vars[{v__}] = src_Vars[{v_}] - {n_} & dst_Vars[{v__}] = dst_Vars[{v_}] \/ {n_} => src_Vars[{v__}] \/ dst_Vars[{v__}] = Object_) ) END

The following shows AtelierB proving the above assertion:

Logical predicates: ------------------- P and Q conjunction P or Q disjunction P implies Q implication P iff Q equivalence not P negation Alternative syntax: P && Q conjunction P || Q disjunction P => Q implication P <=> Q equivalence ! P negation Quantifiers: ------------- all DECL | P universal quantification some DECL | P existential quantification one DECL | P existential quantification with exactly one solution lone DECL | P quantification with one or zero solutions where the DECL follow the following form: x : S choose a singleton subset of S (like x : one S) x : one S choose a singleton subset of S x : S choose x to be any subset of S x : some S choose x to be any non-empty subset of S x : lone S choose x to be empty or a singleton subset of S x : Rel where Rel is a cartesian product / relation: see multiplicity declarations x in Rel x,y... : S, v,w,... : T means x:S and y : S and ... v:T and w:T and ... disjoint x,y,... : S means x : S and y : S and ... and x,y,... are all pairwise distinct Set Expressions: ---------------- univ all objects none empty set S + T set union S & T set intersection S - T set difference # S cardinality of set Set Predicates: --------------- no S set S is empty S in T R is subset of S S = T set equality S != T set inequality some S set S is not empty one S S is singleton set lone S S is empty or a singleton {x:S | P} set comprehension {DECL | P} set comprehension, DECL has same format as for quantifiers let s : S | P identifier definition Relation Expressions: ---------------------- R -> S Cartesian product R . S relational join S <: R domain restriction of relation R for unary set S R :> S range restriction of relation R for unary set S R ++ Q override of relation R by relation Q ~R relational inverse ^R transitive closure of binary relation *R reflexive and transitive closure Multiplicity Declarations: --------------------------- The following multiplicity annotations are supported for binary (sub)-relations: f in S -> T f is any relation from S to T (subset of cartesian product) f in S -> lone T f is a partial function from S to T f in S -> one T f is a total function from S to T f in S -> some T f is a total relation from S to T f in S one -> one T f is a total bijection from S to T f in S lone -> lone T f is a partial injection from S to T f in S lone -> one T f is a total injection from S to T f in S some -> lone T f is a partial surjection from S to T f in S some -> one T f is a total surjection from S to T f in S some -> T f is a surjective relation from S to T f in S some -> some T f is a total surjective relation from S to T Ordered Signatures: ------------------- A signature S can be defined to be ordered: open util/ordering [S] as s s/first first element s/last last element s/max returns the largest element in s or the empty set s/min returns the smallest element in s or the empty set s/next[s2] element after s2 s/nexts[s2] all elements after s2 s/prev[s2] element before s2 s/prevs[s2] all elements before s2 s/smaller[e1,e2] return the element with the smaller index s/larger[e1,e2] returns the element with the larger index s/lt[e1,e2] true if index(e1) < index(e2) s/lte[s2] true if index(e1) =< index(e2) s/gt[s2] true if index(e1) > index(e2) s/gte[s2] true if index(e1) >= index(e2) Sequences: ---------- The longest allowed sequence length (maxseq) is set in the scope of a run or check command using the 'seq' keyword. Otherwise, a default value is used. The elements of a sequence s are enumerated from 0 to #s-1. s : seq S ordered and indexed sequence #s the cardinality of s s.isEmpty true if s is empty s.hasDups true if s contains duplicate elements s.first head element s.last last element s.butlast s without its last element s.rest tail of the sequence s.inds the set {0,..,#s-1} if s is not empty, otherwise the empty set s.lastIdx #s-1 if s is not empty, otherwise the empty set s.afterLastIdx #s if s is smaller than maxseq, otherwise the empty set s.idxOf [x] the first index of the occurence of x in s, the empty set if x does not occur in s s.add[x] insert x at index position i s.indsOf[i] the set of indices where x occurs in s, the empty set if x does not occur in s s.delete[i] delete the element at index i s.lastIdxOf[x] the last index of the occurence of x in s, the empty set if x does not occur in s s.append[s2] concatenate s and s2, truncate the result if it contains more than maxseq elements s.insert[i,x] insert x at index position i, remove the last element if #s = maxseq s.setAt[i,x] replace the value at index position i with x s.subseq[i,j] the subsequence of s from indices i to j inclusively [see http://alloy.lcs.mit.edu/alloy/documentation/quickguide/seq.html] Arithmetic Expressions and Predicates: -------------------------------------- You need to open util/integer: plus[X,Y] addition minus[X,Y] subtraction mul[X,Y] multiplication div[X,Y] division rem[X,Y] remainder sum[S] sum of integers of set S X < Y less X = Y integer equality X != Y integer inequality X > Y greater X =< Y less or equal X >= Y greater or equal Structuring: ------------ fact NAME { PRED } fact NAME (x1,...,xk : Set) { PRED } pred NAME { PRED } pred NAME (x1,...,xk : Set) { PRED } assert NAME { PRED } fun NAME : Type { EXPR } Commands: --------- run NAME check NAME run NAME for x global scope of less or equal x run NAME for exactly x1 but x2 S global scope of x1 but less or equal x2 S run NAME for x1 S1,...,xk Sk individual scopes for signatures S1,..,Sk run NAME for x Int specify the integer bitwidth (integer overflows might occur) run NAME for x seq specify the longest allowed sequence length

As of version 1.3.5, ProB supports TLA+.

The latest version of ProB uses the translator TLA2B, which translates the non temporal part of a TLA+ module to a B machine. To use ProB for TLA+ you have to download the TLA tools. They are released as an open source project, under the MIT License. In the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.

When you open a TLA+ module ProB generates the translated B machine in the same folder and loads it in the background. If there is a valid translation you can animate and model check the TLA+ specification. There are many working examples in the 'ProB/Examples/TLA+/'-directory.

There is also an iFM'2012 paper that describes our approach and performs some comparison with TLC. Our online ProB Logic Calculator now also supports TLA syntax and you can experiment with its predicate and expression evaluation capabilities.

The parser and semantic analyzer SANY serves as the front end of TLA2B. SANY was written by Jean-Charles Grégoire and David Jefferson and is also the front end of the model checker TLC. After parsing there is type checking phase, in which types of variables and constants are inferred. So there is no need to especially declare types in a invariant clause (in the manner of the B method). Moreover it checks if a TLA+ module is translatable (see Limitations of Translation).

To tell TLA2B the name of a specification of a TLA+ module you can use a configuration file, just like for TLC. The configuration file must have the same name as the name of the module and the filename extension 'cfg'. The configuration file parser is the same as for TLC so you can look up the syntax in the 'Specifying Systems'-book (Leslie Lamport). If there is no configuration file available TLA2B looks for a TLA+ definition named 'Spec' or alternatively for a 'Init' and a 'Next' definition describing the initial state and the next state relation. Besides that in the configuration file you can give a constant a value but this is not mandatory, in contrast to TLC. Otherwise ProB lets you choose during the animation process a value for the constant which satisfy the assumptions under the ASSUME clause. TLA2B supports furthermore overriding of a constant or definition by another definition in the configuration file.

Logic ----- P /\ Q conjunction P \/ Q disjunction ~ or \lnot or \neg negation => implication <=> or \equiv equivalence TRUE FALSE BOOLEAN set containing TRUE and FALSE \A x \in S : P universal quantification \E x \in S : P existential quantification Equality: ------ e = f equality e # f or e /= f inequality Sets ------ {d, e} set consisting of elements d, e {x \in S : P} set of elements x in S satisfying p {e : x \in S} set of elements e such that x in S e \in S element of e \notin S not element of S \cup T or S \union T set union S \cap T or S \intersect set intersection S \subseteq T equality or subset of S \ t set difference SUBSET S set of subsets of S UNION S union of all elements of S Functions ------ f[e] function application DOMAIN f domain of function f [x \in S |-> e] function f such that f[x] = e for x in S [S -> T] Set of functions f with f[x] in T for x in S [f EXCEPT ![e] = d] the function equal to f except f[e] = d Records ------- r.id the id-field of record r [id_1|->e_1,...,id_n|->e_n] construct a record with given field names and values [id_1:S_1,...,id_n:S_n] set of records with given fields and field types [r EXCEPT !.id = e] the record equal to r except r.id = e Strings and Numbers ------------------- "abc" a string STRING set of a strings 123 a number Miscellaneous constructs ------------------------ IF P THEN e_1 ELSE e_2 CASE P_1 -> e_1 [] ... [] P_n ->e_n CASE P_1 -> e_1 [] ... [] P_n ->e_n [] OTHER -> e LET d_1 == e_1 ... d_n == e_n IN e Action Operators ---------------- v' prime operator (only variables are able to be primed) UNCHANGED v v'=v UNCHANGED <<v_1, v_2>> v_1'=v_1 /\ v_2=v_2 Supported standard modules -------------------------- Naturals -------- x + y addition x - y difference x * y multiplication x \div y division x % y remainder of division x ^ y exponentiation x > y greater than x < y less than x \geq y greater than or equal x \leq y less than or equal x .. y set of numbers from x to y Nat set of natural numbers Integers -------- -x unary minus Int set of integers Reals -------- x / y real division Real set of reals Sequences --------- SubSeq(s,m,n) subsequence of s from component m to n Append(s, e) appending e to sequence s Len(s) length of sequence s Seq(s) set of sequences s_1 \o s_2 or s_1 \circ s_2 concatenation of s_1 and s_2 Head(s) Tail(s) FiniteSets ---------- Cardinality(S) IsFiniteSet(S) (ProB can only handle certain infinite sets as argument) typical structure of a TLA+ module -------------------------- ---- MODULE m ---- EXTENDS m_1, m_2 CONSTANTS c_1, c_2 ASSUME c_1 = ... VARIABLES v_1, v_2 foo == ... Init == ... Next == ... Spec == ... =====================

Temporal formulas and unused definitions are ignored by TLA2B (they are also ignored by the type inference algorithm).

- due to the strict type system of the B method there are several restrictions to TLA+ modules.
- the elements of a set must have the same type (domain and range of a function are sets)
- TLA+ tuples are translated as sequences in B, hence all components of the tuple must have the same type

- TLA2B do not support 2nd-order operators, i.e. operators that take a operator with arguments as argument (e.g.: foo(bar(_),p))

TLA2B divides the next state relation into different actions if a disjunction occurs. IF a existential quantification occurs TLA2B searches for further actions in the predicate of the quantification and adds the bounded variables as arguments to these actions. IF a definition call occurs and the definition has no arguments TLA2B goes into the definition searching for further actions. The displayed actions by ProB are not necessarily identical with the actions determined by TLC.

Corresponding B types to TLA+ data values (let type(e) be the type of the expression e):

TLA+ data B Type -------------------------------------------------- number e.g. 123 INTEGER decimal number e.g. 123.4 REAL string e.g. "abc" STRING bool value e.g. TRUE BOOL set e.g. {e,f} POW(type(e)), type(e) = type(f) function e.g. [x \in S |-> e] POW(type(x)*type(e)), type(S) = POW(type(x)) sequence e.g. <<a,b>> POW(INTEGER*type(a)), type(a) = type(b) record e.g. [id_1|->e_1,...,id_n|->e_n] struct(id_1:type(e_1),...,id_n:type(e_n)) model value ENUM (only definable in config file) Nat POW(INTEGER) Int POW(INTEGER) Real POW(REAL) STRING POW(STRING) BOOLEAN POW(BOOL) SUBSET S POW(type(S))

You can only compare data values with the same type.

Our translator recognises various special definitions which are passed on to ProB.
These definitions for instance can be used to generate VisB visualisations based on SVG graphics.
Some examples can be found in the visb-visualisation-examples repository.
One example is this one, where you can see the special definition ` VISB_SVG_BOX` and the various `VISB_SVG_OBJECTS` definitions to generate SVG graphical elements:

---------------------- MODULE WaterTankReals ---------------------- EXTENDS Naturals, Reals CONSTANTS low_threshold, high_threshold, (*@ unit s *) step_size, (*@ unit m**3 / s *) outflow, inflow ASSUME /\ low_threshold = 20.0 /\ high_threshold = 60.0 /\ outflow = 10.0 /\ inflow = 15.0 /\ step_size = 0.5 VARIABLES pump, level Init == level \in {50.0} /\ pump=FALSE SwitchPump == pump' = IF level < low_threshold THEN TRUE ELSE IF level > high_threshold THEN FALSE ELSE pump UpdateLevel == level' = IF pump THEN level + inflow * step_size - outflow * step_size ELSE level - outflow * step_size Next == SwitchPump /\ UpdateLevel WaterTank == Init /\ [][Next]_{pump} lft == 10.0 \* left offset wid == 30.0 \* width of water tank bot == 120.0 \* bottom of water tank display maxw == high_threshold+inflow \* maximum capacity as shown Invariant == level > 0.0 /\ level <= maxw convy(lvl) == bot-lvl VISB_SVG_BOX == [width |-> wid+4.0*lft, height |-> bot+lft] VISB_SVG_OBJECTS0 == [svg_class |-> "rect", x|->lft, y |-> convy(level), height |-> level, width |-> wid, fill |-> "lightsteelblue"] VISB_SVG_OBJECTS1 == [svg_class |-> "rect", x|->lft, y |-> convy(maxw), height |-> maxw, width |-> wid, fill |-> "none", stroke |-> "black", stroke_width|->1.0] VISB_SVG_OBJECTS2 == [svg_class |-> "line", x1|->lft-0.5, x2|->lft+wid+0.5, y1|->convy(low_threshold), y2|->convy(low_threshold), stroke |-> "red", stroke_width|->1.0] \* line for low_threshold VISB_SVG_OBJECTS3 == [svg_class |-> "line", x1|->lft-0.5, x2|->lft+wid+0.5, y1|->convy(high_threshold), y2|->convy(high_threshold), stroke |-> "red", stroke_width|->1.0] \* line for high_threshold VISB_SVG_OBJECTS4 == [svg_class |-> "rect", x|->lft, y |-> 2.0*lft, height |-> lft, width |-> wid, rx|->5, fill |-> IF pump THEN "mediumseagreen" ELSE "palegoldenrod", stroke |-> "black", stroke_width|->1.0] VISB_SVG_OBJECTS5 == [svg_class |-> "text", x|->lft+5.0, y |-> 2.0*lft-8.0, text|->"Pump:", font_size|->8.0] VISB_SVG_OBJECTS6 == [svg_class |-> "text", x|->lft+9.5, y |-> 2.0*lft+7.2, text|->IF pump THEN "on" ELSE "off", font_size|->8.0] -------------------------------------------------------------- THEOREM WaterTank => []Init ==============================================================

The definitions can also be used to create custom graph visualisations based on GraphViz. For example, this is a TLA+ example making use of the custom graph visualisation feature (and is an adaptation of the B model used in our custom graph manual page):

---- MODULE IceCream_Generic3 ---- EXTENDS Naturals, FiniteSets VARIABLES \* @type: Int -> Bool; ice, \* @type: Int; vans, \* @type: Set(<<Int,Int>>); edge NODES == 1 .. 24 SET_PREF_TIME_OUT == 1500 SET_PREF_SOLVER_STRENGTH == 300 Init == /\ ice \in [NODES -> BOOLEAN] /\ vans \in (0 .. 10) /\ edge \in SUBSET (NODES \times NODES) /\ edge = {<<1, 2>>, <<1, 4>>, <<2, 3>>, <<3, 4>>, <<3, 5>>, <<3, 7>>, <<4, 7>>, <<5, 6>>, <<5, 9>>, <<6, 7>>, <<6, 8>>, <<7, 8>>, <<8, 10>>, <<8, 13>>, <<9, 10>>, <<9, 11>>, <<9, 12>>, <<11, 12>>, <<11, 14>>, <<12, 13>>, <<13, 16>>, <<14, 15>>, <<14, 17>>, <<15, 16>>, <<15, 17>>, <<15, 18>>, <<15, 21>>, <<16, 18>>, <<16, 19>>, <<17, 19>>, <<18, 19>>, <<18, 20>>, <<18, 21>>, <<19, 20>>, <<19, 21>>, <<20, 21>>, <<20, 22>>, <<21, 22>>, <<21, 23>>, <<21, 24>>, <<22, 23>>, <<21, 24>>, <<23, 24>>} /\ (\A x \in NODES : (ice[x] = TRUE \/ (\E nbour \in NODES : (<<nbour,x>> \in edge \/ <<x,nbour>> \in edge) /\ ice[nbour] = TRUE))) /\ vans = Cardinality({x\in NODES : ice[x]=TRUE}) /\ Cardinality({x \in (NODES): ice[x] = TRUE}) =< 6 Next == TRUE /\ UNCHANGED <<ice, vans, edge>> TypeOK == /\ ice \in [NODES -> BOOLEAN] /\ vans \in (0 .. 10) /\ edge \in SUBSET (NODES \times NODES) Invariant == /\ TypeOK /\ Cardinality({x \in (NODES): ice[x] = TRUE})=6 CUSTOM_GRAPH == [layout |-> "dot", rankdir |-> "TB", nodes |-> {[value |-> j, style |-> "filled", fillcolor |-> (IF ice[j] = TRUE THEN "mistyrose" ELSE "white")]: j \in NODES}, edges |-> [color |-> "gray", arrowhead |-> "odot", arrowtail |-> "odot", dir |-> "both", label |-> "edge", edges |-> edge]] ====

ProZ is a extension of the ProB animator and model checker to support Z specifications. It uses the Fuzz Type Checker by Mike Spivey for extracting the formal specification from a LaTeX file. On the website you can also find documentation about the syntax of Z specifications. The iFM'07 article on ProZ contains more details about the implementation.

A Z specification frequently makes use of comprehension sets, which are often introduced by the underlying translation process from Z to B. Normally those comprehension sets should be treated symbolically. To support this, you should set the following in the preferences menu:

Animation Preferences -> - Lazy expansion of lambdas & set comprehensions: True - Convert lazy form back into explicit form for Variables and Constants: False

To identify the components (like state, initialization, operations) of a Z specification, ProZ expects a certain structure of the specification: There must be a schema called "Init". "Init" describes the initialization of the state. "Init" must include exactly one schema in the declaration part. This schema is assumed to be the state schema.

For example, let S be the state schema (= is used for \defs):

S = [ x,y:N ]

There are two supported styles for the initialization:

a) Init = [ S | x=0 /\ y=1] b) Init = [ S'| x'=0 /\ y'=1 ]

If you want to use the logic of other schemas besides the state schema in the initialization, you can do that by including those schemas in the predicate part.

ProZ identifies schemas as operations if they satisfy the following properties:

- All variables of the state and their primed counterpart are declared in the operation. Usually this is done by including "\Delta S" in the operation (with S being the state schema).
- The operation is not referenced by any other schema in the specification

Example: Let S be defined as above:

A = [ \Delta S | x'=x+1 /\ y'=y ] B = [ x,y,x',y':N | x'=x+1 /\ y'=y ] C = [ x,x':N | x'=x+1 ] D = [ y,y':N | y'=y ] E = C /\ D F = [ \Xi S | x=0 ]

Then the schemas A,B and E describe all the same operation. F is also identified as an operation that leaves the state unchanged.

If axiomatic definitions are present, the declared variables are treated like constants. In the first step of the animation, ProB searches for values that satisfy all predicates of the axiomatic definitions are searched. After the first step, the predicates of the axiomatic definitions are ignored. If you want to define functions in an axiomatic definition, consider that ProB can treat lambda expressions and set comprehensions symbolically. Example: The definition of a function "square" could be

a)

| square : Z -> Z |----------------------- | square = (\lambda x:Z @ x*x)

b)

| square : Z -> Z |----------------------- | \forall x:Z @ square x = x*x

When using ProZ, it is preferable to use the method "a" because the lambda expression can be interpreted symbolically. If "b" is used, ProB will try to find a explicit set that will satisfy the given property.

You can add a B-style invariant to the specification by defining a schema "Invariant" that declares a subset of the state variables. In each explored state the invariant will be checked. The model checking feature of ProB will try to find states that violate the invariant.

It is possible to limit the search space of the model checker by adding a schema "Scope" that declares a subset of the state variables. If such a schema is present, each explored state is checked, if it satisfies the predicate. If not, the state is not further explored.

Abbreviation definitions (e.g. Abbr == {1,2,3}) are used like macros by ProZ. A reference to an abbreviation is replaced by its definition in a preprocessor phase. Thereby schemas defined by abbreviation definitions are ignored when ProZ tries to identify components. So, it is recommended to use schema definitions instead of abbreviation definitions (\defs instead of ==) when defining state, initialization, operations, etc.

(**Please note that this functionality is part of the next version. If you want to use graphical animation, please download a version from the Nightly build.**)

Analogous to the graphical animation for B specifications, you can define a function that maps a coordinate to an image. Then ProZ will display the grid of images while animating the specification.

To use this feature, add a schema **Proz_Settings** that contains a variable
**animation\_function**. The animation function should map a coordinate to an image. A coordinate is a pair of numbers or given sets.

The type used for images must be an enumerated set where the names of the elements denote their file names (without the suffix .gif).

Please see the specification **jars.tex** which is bundled with the ProB Tcl/Tk version for Download (inside the examples/Z/GraphicalAnimation/ directory). This is the part of the specification that defines the animation function (actually it defines a pair of animation functions: the default function over which the other function is overlaid; see Graphical_Visualization for more details):

We declare a type for the used images, the names of the elements refer to the file names of the GIF files. \begin{zed} Images ::= Filled | Empty | Void \end{zed} The animation consists of a grid of images that is updated in each new state. The $animation\_function$ maps a coordinate to an image where $(1\mapsto 1)$ is the upper-left corner. \begin{schema}{ProZ\_Settings} Level \\ animation\_function\_default : (\nat \cross Jars) \pfun Images \\ animation\_function : (\nat \cross Jars) \pfun Images \\ \where animation\_function\_default = (1\upto global\_maximum \cross Jars) \cross \{ Void \} \\ animation\_function = \\ \t1 (\{ l:1\upto global\_maximum; c:Jars | l\leq max\_fill~c @ \\ \t2 global\_maximum+1-l\mapsto c\} \cross \{Empty\}) \oplus \\ \t1 (\{ l:1\upto global\_maximum; c:Jars | l\leq level~c @ \\ \t2 global\_maximum+1-l\mapsto c\} \cross \{Filled\}) \end{schema}

Here is how the animation of the specification should look like:

Sometimes it is not desired to check properties of some variables. E.g. ProZ checks if the square function in 2.3.a is a total function by enumerating it (it checks the function only for a limited interval). For more complex definitions the number of entries is often too large to check. When the user is sure that those properties are satisfied (like in our example), a solution is relaxing the declaration from "square : Z -> Z" to "square : Z <-> Z". Sometimes this is not easy to do, for instance if schema types are used which imply other constraints.

ProZ supports an operation \prozignore that instructs ProZ to ignore all constraints on the type and to use just the underlying type. For example, the square function could be defined by:

| square : \prozignore( Z -> Z ) |----------------------- | square = (\lambda x:Z @ x*x)

If you want to use \prozignore, you must first define a TeX command \prozignore:

\newcommand{\prozignore}{ignore_\textsl{\tiny ProZ}}

You can change the definition of the macro as you like because the content is ignored by ProZ. Then you must introduce a generic definition of \prozignore. The definition is ignored by ProB, but Fuzz needs it for type checking.

%%pregen \prozignore \begin{gendef}[X] \prozignore~\_ : \power X \end{gendef}

It is also possible to append these lines to the "fuzzlib" in the fuzz distribution.

You can inspect the result of the translation process with "Show internal representation" in the "Debug" menu. Please note that the shown B machine is normally not syntactically correct because of

- additional constructs like free types
- additional type information of the form "var:type"
- names with primes (') or question marks, etc.
- lack of support from the pretty printer for every construct

- Generic definitions are not supported yet.
- Miscellaneous unsupported constructs
- reflexive-transitive closure
- probably other?

- The error messages are not very helpful yet.

Logical predicates: ------------------- P \land Q conjunction P \lor Q disjunction P \implies Q implication P \iff Q equivalence \lnot P negation Quantifiers: ------------ \forall x:T | P @ Q universal quantification (P => Q) \exists x:T | P @ Q existential quantification (P & Q) \exists_1 x:T | P @ Q exactly one existential quantification Sets: ----- \emptyset empty set \{E,F\} set extension \{~x:S | P~\} set comprehension E \in S element of E \notin S not element of S \cup T union S \cap T intersection S \setminus T set difference \power S power set \# S cardinality S \subseteq T subset predicate S \subset T strict subset \bigcup A generalized union of sets of sets \bigcap A generalized intersection of sets of sets Pairs: ------ E \mapsto F pair S \cross T Cartesian product first E first part of pair second E second part of pair Numbers: -------- \nat Natural numbers \num Integers \nat_1 Positive natural numbers m < n less m \leq n less equal m > n greater m \geq n greater equal m + n addition m - n difference m * n multiplication m \div n division m \mod n modulo** m \upto n m..n min S minimum of a set max S maximum of a set succ n successor of a number **: modulo of negative numbers not supported Functions: ---------- S \rel T relations S \pfun T partial functions from S to T S \fun T total functions from S to T S \pinj T partial injections from S to T S \inj T total injections from S to T S \bij T total bijections from S to T \dom R domain \ran R range \id S identity relation over S S \dres R domain restriction S \ndres R domain anti-restriction R \rres S range restriction R \nrres S range anti-restriction R \oplus Q overriding R \plus transitive closure Sequences: ---------- \langle E,... \rangle explicit sequence \seq S sequences over S \seq_1 S non-empty sequences \iseq S injective sequences over S rev E reverse a sequence head E first element of a sequence last E last element of a sequence tail E sequence with first element removed front E all but the last element E \cat F concatenation of two sequences \dcat ss concatenation of sequences of sequences E \filter F subsequence of elements of sequence E contained in set F E \extract F extract subsequence from F with indexes in set E squash F compaction E \prefix F sequence E is a prefix of F E \suffix F sequence E is a suffix of F E \inseq F E is a sequence occuring in the middle of F (segment relation) \disjoint E family of sets E is disjoint E \partition F family of sets E is a partition of set F Bags: ---------- \bag S bags over S \lbag E,... \rbag explicit bag count B E count of occurences of E in bag B B \bcount E infix version of count E \inbag B bag membership B \subbageq C sub-bag relation B \uplus C bag union B \uminus C bag difference items E bag of items in a sequence n \otimes B bag scaling Other: ----------- \IF P \THEN E \ELSE F if-then-else expression (\LET x == E @ F) Let-expression

The B-Rules domain-specific language (B-Rules DSL) mainly provides operations for data validation. *Rules* allow checking for expected properties, while *computations* can be used to define and compute variables based on the successful execution of certain rules. Furthermore you can use *functions* to compute values multiple times depending on different inputs.

Rules machines are stored in `.rmch`

-files. The general setup for the machine header is:

RULES_MACHINE machine_name REFERENCES list of rules machines

The latter allows the inclusion of other rules machines and ordinary B machines that contain only constants, but not yet any other B machines. Below, `SETS`

, `DEFINITIONS`

, `PROPERTIES`

or `CONSTANTS`

can be used as in a normal B machine. Note that `VARIABLES`

are not allowed as they are set by rule based computations.

Rules can be defined in the `OPERATIONS`

-section of a rules machine. Depending on whether the expectations are met, a rule returns `SUCCESS`

or `FAIL`

. If a rule fails, additionally provided string messages are returned as counterexamples.
In the B Rules-DSL a rule has the following structure:

RULE rule_name // will be the name of the operation and variable storing the result DEPENDS_ON_RULE list of rules DEPENDS_ON_COMPUTATION list of computations ACTIVATION predicate ERROR_TYPES positive number of error types BODY arbitrarily many rule bodys (see below) END

The specified `rule_name`

will be the name of the operation and variable storing the result.
If a rule depends on other rules, it can only be executed if the specified rules have been successfully checked, i.e. their corresponding variables `rule_name`

have the value `SUCCESS`

. In addition, rules can depend on computations. In this case, a rule is enabled when the specified computations have been executed. If a rule uses variables that are defined by computations, the corresponding computations are added implicitly as dependencies and do not have to be declared explicitly. Any other preconditions can be specified as an `ACTIVATION`

predicate. An important note is that the activation predicate is evaluated statically at initialisation and disables the rule if the predicate is false. Activation predicates and dependencies can be omitted if they are not needed.

To use different error types (for example, if a rule has multiple bodies and it is necessary to distinguish between them), the number of error types has to be declared in the rule header. Error types are also optional.

The actual rule conditions are specified within the body of a rule, which contains the name and the preconditions.
A rule succeeds if and only if all rule conditions in its body are satisfied.
There are two constructs for rule bodies that can be used arbitrarily often in the body of a rule.
The following is formulated in a positive way, i.e. the execution of the rule leads to `SUCCESS`

if the conditions in the `EXPECT`

-part are fulfilled.

RULE_FORALL list of identifiers WHERE conditions on identifiers EXPECT conditions that must be fulfilled for this rule ERROR_TYPE number encoding error type, must be in range of error types COUNTEREXAMPLE STRING_FORMAT("errorMessage ~w", identifier from list) END

Alternatively, a negated rule can be formulated. Here the execution of the rule results in `FAIL`

if the conditions in the `WHEN`

-part are fulfilled.

RULE_FAIL list of identifiers WHEN conditions on identifiers for a failing rule ERROR_TYPE number encoding error type, must be in range of error types COUNTEREXAMPLE STRING_FORMAT("errorMessage ~w", identifier from list) END

Counterexamples are of the type `INTEGER <-> STRING`

. The integer contains the error type, while the string contains the message of the counterexample.

Also valid for the rules header are:

RULEID id CLASSIFICATION identifier TAGS identifier

The `CLASSIFICATION`

keyword can be used to group the rules in the HTML validation report according to their classification.

Computations can be used to define variables. As for rules, their activation can depend on further rules, computations or any other predicate specified as an activation condition. Again, the activation condition is evaluated at initialisation and sets the computation status variable to `COMPUTATION_DISABLED`

if the predicate is false. Furthermore, a `DUMMY_VALUE`

can be set, which initialises the variable with the specified value instead of the empty set before execution of the computation. This mechanism implies that each variable defined by a computation must be a set of type `POW(S)`

for any `TYPE`

`S`

. A computation can be replaced by a previously defined computation if it sets the same variable (of the same type) by using `REPLACES`

. The general syntax for computations is:

COMPUTATION computation_name DEPENDS_ON_RULE list of rules DEPENDS_ON_COMPUTATION list of computations ACTIVATION predicate REPLACES identifier of exactly one computation BODY DEFINE variable_name TYPE type of variable DUMMY_VALUE value of variable before execution (initialisation) VALUE value of variable after execution END END

Activation predicates, dependencies, and also the dummy value can be omitted if they are not needed. After the execution of a computation, the value of the corresponding variable `computation_name`

is changed from `NOT_EXECUTED`

to `EXECUTED`

and the variable `variable_name`

has the value \texttt{VALUE}. For related computations, it may be useful to use multiple `DEFINE`

blocks in one computation.
Separated by `;`

, the body of a computation can contain any number of variable definitions.

Functions can be called from any rules machine that references the machine containing the function. Depending on input parameters that must fulfil specified preconditions, the functions returns output value(s) that must fulfil optional postconditions. In the body, any B statement can be used to (sequentially) compute the output value.

FUNCTION output <-- function_name(list of input parameters) PRECONDITION predicate POSTCONDITION predicate BODY some B statements output := ... END

There are some useful predicates available in rules machines that can be used to check the success or failure of rules. It is also possible to check whether a certain error type was returned by a rule. These are:

`SUCCEEDED_RULE(rule1)`

: TRUE, if the check of rule1 succeeded`SUCCEEDED_RULE_ERROR_TYPE(rule1,1)`

: TRUE, if the check of rule1 did not fail with error type 1`GET_RULE_COUNTEREXAMPLES(rule1)`

: set of counterexamples of rule1`FAILED_RULE(rule1)`

: TRUE, if the check of rule1 failed`FAILED_RULE_ERROR_TYPE(rule1,2)`

: TRUE, if check of rule1 failed with error type 2`FAILED_RULE_ALL_ERROR_TYPES(rule1)`

: TRUE, if the check of rule1 failed with all possible error types for rule1`NOT_CHECKED_RULE(rule1)`

: TRUE, if rule1 has not yet been checked`DISABLED_RULE(rule1)`

: TRUE, if rule1 is disabled (its preconditions are not fulfilled)

Another functionality of rules machines are FOR-loops. Their syntax is:

FOR variable(s) IN set DO operation(s) END

An example:

RULE example_rule BODY FOR x,y IN {1 |-> TRUE, 2 |-> FALSE, 3 |-> FALSE} DO RULE_FAIL WHEN y = FALSE COUNTEREXAMPLE STRING_FORMAT("example_rule_fail: ~w", x) END END

This rule always fails and returns `{1 |-> "example_rule_fail: 2", 1 |-> "example_rule_fail: 3"}`

.

Rule validation has been integrated into the ProB2-UI since version 1.2.2 (not yet released). It allows convenient execution of rules and computations together with a graphical representation of the results. Rules are grouped by their classification and can be additionally filtered by their name, ID, or tags. The results can also be exported as an HTML report. In addition, dependencies of rules and computations can be visualised as a graph either for all operations or for just one operation (the HTML report and the dependency graph are generated by the ProB Java API and can also be created without ProB2-UI).

The concept of rule validation can be used to validate data from external sources such as CSV or XML files and load the validated data into ProB by successive computations. For an XML file, this could look as follows:

RULES_MACHINE XML_import DEFINITIONS "LibraryXML.def" CONSTANTS xml_data PROPERTIES xml_data = READ_XML("xml_file.xml", "auto") END

Now some properties can be validated. For example:

RULE is_supported_version_of_type_xyz ERROR_TYPES 2 BODY RULE_FAIL e WHEN 1 : dom(xml_data) & e = data(1)'element & e /= "xyz" ERROR_TYPE 1 // optional: 1 is standard type COUNTEREXAMPLE STRING_FORMAT("Error: could not find element 'xyz', was '"^e^"'") END; RULE_FAIL v WHEN v = xml_data(1)'attributes("version") & v /: supported_versions ERROR_TYPE 2 COUNTEREXAMPLE "xyz of version "^v^" is currently not supported" END END;

Each rules machine is internally translated to an ordinary B machine, which can be accessed as its internal representation. Consider the following example rule:

RULE rule1 BODY RULE_FAIL WHEN bfalse COUNTEREXAMPLE "" END END; COMPUTATION comp1 BODY DEFINE x TYPE POW(INTEGER) VALUE 1..10 END END; RULE rule2 DEPENDS_ON_RULE rule1 // DEPENDS_ON_COMPUTATION comp1 BODY RULE_FORALL i WHERE i : 1..10 EXPECT i > 5 COUNTEREXAMPLE STRING_FORMAT("~w <= 5", i) END END

Its internal representation in classical B is the following:

`$RESULT`,`$COUNTEREXAMPLES` <-- rule1 = SELECT rule1 = "NOT_CHECKED" THEN rule1,`$RESULT`,`$COUNTEREXAMPLES` := "SUCCESS","SUCCESS",{} END; comp1 = SELECT comp1 = "NOT_EXECUTED" THEN x,comp1 := FORCE(1 .. 10),"EXECUTED" END; `$RESULT`,`$COUNTEREXAMPLES` <-- rule2 = SELECT rule2 = "NOT_CHECKED" & rule1 = "SUCCESS" & comp1 = "EXECUTED" THEN rule2,`$RESULT`,`$COUNTEREXAMPLES` := "SUCCESS","SUCCESS",{} ; VAR `$ResultTuple`,`$ResultStrings` IN `$ResultTuple` := FORCE({i|i : x & not(i > 5)}) ; `$ResultStrings` := FORCE({`$String`|`$String` : STRING & #i.(i : `$ResultTuple` & `$String` = FORMAT_TO_STRING("~w <= 5",[TO_STRING(i)]))}); rule2_Counterexamples := rule2_Counterexamples \/ {1} * `$ResultStrings` ; IF `$ResultTuple` /= {} THEN rule2,`$RESULT`,`$COUNTEREXAMPLES` := "FAIL","FAIL",rule2_Counterexamples END END END

Observe that the implicit dependency of rule2 on comp1 (rule2 uses its variable x) is detected automatically without explicit declaration.

Currently, it is not possible to include rules machines directly into any other machines. Instead, use the rules machine at the top of the hierarchy (of the rules project) and save the internal generated machine as `.mch`

-file. After changing the machine name accordingly, the rules can be included and used via this machine.
Note that in this case it is not possible to perform Rules-DSL specific methods of the ProB Java API (like detailed information about rule results).