Also see the following tutorials:
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:
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:
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:
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):
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 (ProB Theory Mapping). The file must have the same name as the theory.
For each annotated operator, the file contains a line of the form
operator Name internal {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):
Axiomatically defined operators are not supported without additional annotations.
An example project with theories: media:theories2.zip
The project contains the following theories:
The operators are annotated such that ProB uses an extra implementation.
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 (ProB Theory Mapping). The file must have the same name as the theory.
For each annotated operator, the file contains a line of the form
operator Name internal {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.
operator "SUM" internal {SIGMA} operator "PRODUCT" internal {PI}
operator "cls" internal {closure1}
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:
ProB now supports FDR and ProBE compatible CSP-M syntax, with the following outstanding issues
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 [| {op1,...,opn} |] Bwhere op1,...,opn are the visible operations defined in the B machine.
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)
lookup!X!2 will match lookup(X) --> 2Note 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.
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.
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:
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:
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:
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:
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.
The following options affect all assertions in the list box.
Other options. The following options have no impact on the assertions in the list box.
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:
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
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:
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
and src+dst=Object as invariant: it generates a check operation encoding the predicate add_preserves_inv with 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_inv into 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).
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:
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
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