TLA - Revision history

Michael Leuschel at 10:44, 1 August 2025

2025-08-01T10:44:21Z

← Older revision		Revision as of 10:44, 1 August 2025
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+].
			It translates a TLA+ model to a B machine and provides features such as interactive animation, constraint solving, visualization.
			It is complementary to tools such as TLC or Apalache for TLA+

	= Comparison with TLC and Apalache =		= Comparison with TLC and Apalache =

Michael Leuschel at 08:02, 1 August 2025

2025-08-01T08:02:33Z

← Older revision		Revision as of 08:02, 1 August 2025
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+].

	= Comparison with TLC and Apalache		= Comparison with TLC and Apalache =

	== Why you may want to use ProB for TLA+		== Why you may want to use ProB for TLA+ ==
	* Interactive animation with backtracking and freely navigating the state space		* Interactive animation with backtracking and freely navigating the state space
	* Constraint solving capabilities		* Constraint solving capabilities
Line 12:		Line 12:
	* No risk of unsoundness due to hash collisions (ProB keeps the state space in memory and safely detects hash collisions)		* No risk of unsoundness due to hash collisions (ProB keeps the state space in memory and safely detects hash collisions)

	== Why you may not want to use ProB for TLA+		== Why you may not want to use ProB for TLA+ ==
	* Model checking can be much slower than with TLC (ProB keeps the state space in memory, is much slower for low-level models that do not require constraint solving to effectively compute the next state action or invariants)		* Model checking can be much slower than with TLC (ProB keeps the state space in memory, is much slower for low-level models that do not require constraint solving to effectively compute the next state action or invariants)
	* Only typed specifications are accepted		* Only typed specifications are accepted

Michael Leuschel at 08:02, 1 August 2025

2025-08-01T08:02:11Z

← Older revision		Revision as of 08:02, 1 August 2025
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+].

			= Comparison with TLC and Apalache

			== Why you may want to use ProB for TLA+
			* Interactive animation with backtracking and freely navigating the state space
			* Constraint solving capabilities
			* Visualisation: state space projection, individual states using GraphViz, SVG-based interactive visualisation (VisB)
			* Storing & replaying traces, validation obligation manager
			* Model checking: other algorithms available: operation caching, partial order reduction, …
			* Unbounded integers (compared to TLC's 32-bit integers, ProB uses Prolog's tagged 64-bit representation, resulting in 60 bit integers and transparently switching to unlimited big integers; the CLP(FD) solver cannot use big integers though, but can be turned off)
			* No risk of unsoundness due to hash collisions (ProB keeps the state space in memory and safely detects hash collisions)

			== Why you may not want to use ProB for TLA+
			* Model checking can be much slower than with TLC (ProB keeps the state space in memory, is much slower for low-level models that do not require constraint solving to effectively compute the next state action or invariants)
			* Only typed specifications are accepted
			* Not all features of TLA+ supported
			* ProB may show B formulas (even though use of Unicode overcomes part of the hurdle)

	= Using ProB for Animation and Model Checking of TLA+ specifications =		= Using ProB for Animation and Model Checking of TLA+ specifications =

Michael Leuschel: /* Visualisation */

2024-09-12T07:16:45Z

Visualisation

← Older revision		Revision as of 07:16, 12 September 2024
Line 209:		Line 209:
	These definitions for instance can be used to generate [[VisB]] visualisations based on SVG graphics.		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.		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>		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:
	and the various <tt>VISB_SVG_OBJECTS</tt> definitions to generate SVG graphical elements:
	<pre>		<pre>
	---------------------- MODULE WaterTankReals ----------------------		---------------------- MODULE WaterTankReals ----------------------

Michael Leuschel: /* Visualisation */

2024-09-12T07:16:30Z

Visualisation

@@ Line 209: / Line 209: @@
 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.
 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]]):

Michael Leuschel: /* Visualisation */

2024-09-12T07:14:06Z

Visualisation

← Older revision		Revision as of 07:14, 12 September 2024
Line 210:		Line 210:
	Some examples can be found in the [https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples visb-visualisation-examples] repository.		Some examples can be found in the [https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples visb-visualisation-examples] repository.

	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:		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>		<pre>
	---- MODULE IceCream_Generic3 ----		---- MODULE IceCream_Generic3 ----
Line 224:		Line 224:

	SET_PREF_TIME_OUT == 1500		SET_PREF_TIME_OUT == 1500
	~~\*SET_PREF_SMT == TRUE~~
	~~\*SET_PREF_SOLVER_FOR_PROPERTIES == "sat"~~
	SET_PREF_SOLVER_STRENGTH == 300		SET_PREF_SOLVER_STRENGTH == 300

Michael Leuschel: /* Visualisation */

2024-09-12T07:11:31Z

Visualisation

← Older revision		Revision as of 07:11, 12 September 2024
Line 210:		Line 210:
	Some examples can be found in the [https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples visb-visualisation-examples] repository.		Some examples can be found in the [https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples visb-visualisation-examples] repository.

	The definitions can also be used to create [[Custom_Graph\|custom graph visualisations]] based on GraphViz.		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:
			<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_SMT == TRUE
			\*SET_PREF_SOLVER_FOR_PROPERTIES == "sat"
			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>

Michael Leuschel: /* Visualisation */

2024-09-12T07:08:09Z

Visualisation

← Older revision		Revision as of 07:08, 12 September 2024
Line 210:		Line 210:
	Some examples can be found in the [https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples visb-visualisation-examples] repository.		Some examples can be found in the [https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples visb-visualisation-examples] repository.

	The definitions can also be used to create custom graph visualisations based on GraphViz.		The definitions can also be used to create [[Custom_Graph\|custom graph visualisations]] based on GraphViz.

Michael Leuschel: /* Visualisation */

2024-09-12T07:07:04Z

Visualisation

← Older revision		Revision as of 07:07, 12 September 2024
Line 207:		Line 207:

	Our translator recognises various special definitions which are passed on to ProB.		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.		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.		Some examples can be found in the [https://gitlab.cs.uni-duesseldorf.de/general/stups/visb-visualisation-examples visb-visualisation-examples] repository.

	The definitions can also be used to create custom graph visualisations based on GraphViz.		The definitions can also be used to create custom graph visualisations based on GraphViz.

Michael Leuschel at 06:59, 12 September 2024

2024-09-12T06:59:33Z

← Older revision		Revision as of 06:59, 12 September 2024
Line 203:		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.

			The definitions can also be used to create custom graph visualisations based on GraphViz.