State space visualization examples - Revision history

Michael Leuschel: /* RushHour */

2015-12-22T16:19:22Z

RushHour

← Older revision		Revision as of 16:19, 22 December 2015
Line 66:		Line 66:
	Here is a visualisation of the full state space of 4782 nodes and 29890 transitions, using the scale option this time:		Here is a visualisation of the full state space of 4782 nodes and 29890 transitions, using the scale option this time:

	[[File:RushHour_full_sfdp.png\|~~1000px~~\|center]]		[[File:RushHour_full_sfdp.png\|707px\|center]]

	== CAN Bus ==		== CAN Bus ==

Michael Leuschel: /* RushHour */

2015-12-22T16:18:55Z

RushHour

← Older revision		Revision as of 16:18, 22 December 2015
Line 58:		Line 58:
	== RushHour ==		== RushHour ==

	This is a visualisation of the [[Rush_Hour_Puzzle Rush Hour puzzle B model]], at the moment that ProB has found a solution.		This is a visualisation of the [[Rush_Hour_Puzzle Rush Hour puzzle B model]], at the moment that ProB has found a solution to the goal predicate (red car moved out of the grid).
	The solution node(s) are marked in orange.		The solution node(s) are marked in orange and the prism option was used.

	[[File:RushHour_sfdp.png\|1000px\|center]]		[[File:RushHour_sfdp.png\|1000px\|center]]


			Here is a visualisation of the full state space of 4782 nodes and 29890 transitions, using the scale option this time:

			[[File:RushHour_full_sfdp.png\|1000px\|center]]

	== CAN Bus ==		== CAN Bus ==

Michael Leuschel at 13:49, 21 December 2015

2015-12-21T13:49:37Z

← Older revision		Revision as of 13:49, 21 December 2015
Line 1:		Line 1:

	~~(This page is under construction)~~
	~~== Alternating Bit Protocol ==~~

	This is a visualisation of 3643 states and 11115 transitions of a TLA+ model of the alternating bit protocol, as distributed with the [http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html TLA+ tools].
	~~This model (MCAlternatingBit.tla) was loaded with [[TLA\|ProB for TLA+]], the model checker run for a few seconds and then the command "State Space Fast Rendering" with options (scale,fast) was used.~~

	~~The goal predicate rBit=1 was used; those states satisfying this predicate are shown in orange.~~

	~~[[File:MCAlternatingBit_sfdp.png\|1000px\|center]]~~

	~~Below is a projection of this state space onto the expression <tt>(rBit,sBit)</tt>, using the "Custom Transition Diagram" feature of ProB:~~

	~~[[File:MCAlternatingBit_projsrBit.png\|400px\|center]]~~

	~~More details about this statespace projection feature can be found in our [http://stups.hhu.de/w/Special:Publication/LadenbergerLeuschel_ICFEM15 ICFEM'15 article].~~

	~~The main file of the model is:~~
	~~<PRE>~~
	~~--------------------------- MODULE MCAlternatingBit -------------------------~~
	~~EXTENDS AlternatingBit, TLC~~

	~~INSTANCE ABCorrectness~~

	~~CONSTANTS msgQLen, ackQLen~~

	~~SeqConstraint == /\ Len(msgQ) \leq msgQLen~~
	~~/\ Len(ackQ) \leq ackQLen~~

	~~SentLeadsToRcvd == \A d \in Data : (sent = d) /\ (sBit # sAck) ~> (rcvd = d)~~
	~~=============================================================================~~

	~~ImpliedAction == [ABCNext]_cvars~~

	~~TNext == WF_msgQ(~ABTypeInv')~~
	~~TProp == \A d \in Data : (sent = d) => [](sent = d)~~

	~~CSpec == ABSpec /\ TNext~~

	~~DataPerm == Permutations(Data)~~
	~~==============================================================~~
	~~</PRE>~~

	~~== MCInnerFIFO ==~~

	~~This is a visualisation of 3866 states and 9661 transitions of a TLA+ model of a FIFO, as distributed with the [http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html TLA+ tools].~~
	This model (MCInnerFIFO) was loaded with [[TLA\|ProB for TLA+]] and the model checker run so that all states with queue size greater than qLen (3) were ignored, i.e., no successor states were computed (this can be set by defining SCOPE==card(q)<=qLen).
	~~The colour indicates the length of the queue variable q of the model (gray=0,blue=1,red=2, green=3, lightgray=4) .~~


	~~[[File:MCInnerFIFO_q3_sfdp.png\|1000px\|center]]~~


	~~Below is a projection of this state space onto the expression <tt>card(q)</tt>, using the "Custom Transition Diagram" feature of ProB:~~

	~~[[File:MCInnerFIFO_proj_cardq.png\|200px\|center]]~~

	~~== RushHour ==~~

	~~This is a visualisation of the [[Rush_Hour_Puzzle Rush Hour puzzle B model]], at the moment that ProB has found a solution.~~
	~~The solution node(s) are marked in orange.~~

	~~[[File:RushHour_sfdp.png\|1000px\|center]]~~

	~~== CAN Bus ==~~

	~~This is a visualisation of the statespace of an Event-B model of a CAN Bus.~~
	~~The colours indicate the size of the BUSwrite variable (gray=0,blue=1,red=2, green=3, lightgray=4).~~

	~~[[File:CANBus_sfdp.png\|1000px\|center]]~~


	~~== Hanoi (6 Discs) ==~~

	~~This is a visualisation of the statespace of a B model of the towers of Hanoi for 6 discs.~~
	~~The state space contains 731 nodes and 2186 nodes.~~

	~~[[File:Hanoi6_sfdp.png\|800px\|center]]~~

	~~One can observe that this figure resembles a Sierpinski triangle.~~
	~~This is [http://www.math.ubc.ca/~cass/courses/m308-02b/projects/touhey/ no coincidence, the state space of Hanoi is one].~~

	~~Below is a projection of this state space onto the expression <tt>card(on(dest)))</tt>, using the "Custom Transition Diagram" feature of ProB:~~

	~~[[File:Hanoi6_proj_cardondest.png\|200px\|center]]~~


	~~== Threads - Partial Order Reduction ==~~

	This is the visualisation of a simple threads model, of two threads with n=51 steps before a synchronisation occurs and threads start again. The state space contains 5410 nodes. One can clearly see two synchronisation points on the left-hand side and right-hand side, and that in between synchronisation the processes simply interleave.

	~~[[File:Threads51_sfdp.png\|600px\|center]]~~

	~~With partial order reduction, the state space is reduced to 208 states:~~
	~~[[File:Threads51_POR_sfdp.png\|400px\|center]]~~

	~~Here is the B source code of the model:~~
	~~<PRE>~~
	~~MACHINE Threads51~~
	~~/* Two simple threads communicating from time to time~~
	~~This kind of situation should happen quite often in controller systems~~
	~~A partial-order reduction can hopefully reduce the interleavings~~
	*/
	~~DEFINITIONS~~
	~~ASSERT_LTL1 == "F deadlock(Step1_p1,Step1_p2)";~~
	~~HEURISTIC_FUNCTION == pc1 // for sfdp colouring~~
	~~CONSTANTS n~~
	~~PROPERTIES n = 51 /* n=51: 208 states with POR (deadlock checking), 5410 without */~~
	~~VARIABLES pc1,pc2, v1,v2~~
	~~INVARIANT~~
	~~pc1 : NATURAL & pc2:NATURAL &~~
	~~v1 : INTEGER & v2:INTEGER~~
	~~INITIALISATION pc1,pc2,v1,v2 := 0,0,0,0~~
	~~OPERATIONS~~
	~~Step1_p1 = PRE pc1<n THEN /* maybe the fact that we have a decreasing variant has an influence on POR ? In Event-B this event would be convergent */~~
	~~pc1 := pc1+1\|\| v1 := v1+1~~
	~~END;~~
	~~Step1_p2 = PRE pc2<n /* & pc1=n manual POR */~~
	~~THEN /* also a convergent event (variant n-pc2) */~~
	~~pc2 := pc2+1 \|\| v2 := v2+1~~
	~~END;~~
	~~Sync = PRE pc1=n & pc2=n THEN~~
	~~pc1, pc2 := 0,0 \|\|~~
	~~v1,v2 := v1 mod 2, v2 mod 2~~
	~~END~~
	~~END~~
	~~</PRE>~~


	~~Below are projections of the above state spaces onto the expression <tt>(bool(pc1=n),bool(pc2=n))</tt>, using the "Custom Transition Diagram" feature of ProB.~~

	(This page is under construction)		(This page is under construction)

Michael Leuschel: /* Threads - Partial Order Reduction */

2015-12-21T13:48:33Z