(22 intermediate revisions by 4 users not shown) | |||
Line 1: | Line 1: | ||
As of version 1.3.5, ProB supports [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+]. | As of version 1.3.5, ProB supports [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+]. | ||
= Using ProB for Animation and Model Checking of TLA+ specifications = | = Using ProB for Animation and Model Checking of TLA+ specifications = | ||
The [ | The [[Download|latest version of ProB]] uses the translator TLA2B, which translates the non temporal part of a [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+] module to a B machine. | ||
To use ProB for TLA you have to download the | To use ProB for TLA+ you have to download the TLA tools. They are released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html 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 | [[File:Download_TLA_Tools.png|400px|center]] | ||
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. | 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 are many working examples in the 'ProB/Examples/TLA+/'-directory. | ||
There is also an [https://www3.hhu.de/stups/downloads/pdf/HansenLeuschelTLA2012.pdf iFM'2012 paper] that describes our approach and performs some comparison with TLC. | |||
Our [[ProB_Logic_Calculator|online ProB Logic Calculator]] now also supports TLA syntax and you can experiment with its predicate and expression evaluation capabilities. | |||
= TLA2B = | = TLA2B = | ||
Line 117: | Line 123: | ||
-x unary minus | -x unary minus | ||
Int set of integers | Int set of integers | ||
Reals | |||
-------- | |||
x / y real division | |||
Real set of reals | |||
Sequences | Sequences | ||
Line 155: | Line 166: | ||
* due to the strict type system of the B method there are several restrictions to TLA+ modules. | * 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) | ** the elements of a set must have the same type (domain and range of a function are sets) | ||
** TLA+ | ** 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 do not support 2nd-order operators, i.e. operators that take a operator with arguments as argument (e.g.: foo(bar(_),p)) | ||
Line 173: | Line 184: | ||
TLA+ data B Type | TLA+ data B Type | ||
-------------------------------------------------- | -------------------------------------------------- | ||
number | number e.g. 123 INTEGER | ||
string | decimal number e.g. 123.4 REAL | ||
bool value | string e.g. "abc" STRING | ||
set | bool value e.g. TRUE BOOL | ||
function | set e.g. {e,f} POW(type(e)), type(e) = type(f) | ||
sequence | function e.g. [x \in S |-> e] POW(type(x)*type(e)), type(S) = POW(type(x)) | ||
record | 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 | model value ENUM | ||
(only definable in config file) | |||
Nat POW(INTEGER) | Nat POW(INTEGER) | ||
Int POW(INTEGER) | Int POW(INTEGER) | ||
Real POW(REAL) | |||
STRING POW(STRING) | STRING POW(STRING) | ||
BOOLEAN POW(BOOL) | BOOLEAN POW(BOOL) | ||
Line 190: | Line 203: | ||
</pre> | </pre> | ||
You can only compare data values with the same type. | You can only compare data values with the same type. | ||
= Visualisation = | |||
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 [https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples visb-visualisation-examples] repository. | |||
One example is this one, where you can see the special definition <tt> VISB_SVG_BOX</tt> and the various <tt>VISB_SVG_OBJECTS</tt> definitions to generate SVG graphical elements: | |||
<pre> | |||
---------------------- 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 | |||
============================================================== | |||
</pre> | |||
The definitions can also be used to create [[Custom_Graph|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|custom graph manual page]]): | |||
<pre> | |||
---- 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]] | |||
==== | |||
</pre> |
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]] ====