State Space Visualization - Revision history

Michael Leuschel at 11:59, 6 January 2024

2024-01-06T11:59:06Z

← Older revision		Revision as of 11:59, 6 January 2024
Line 3:		Line 3:
	ProB provides several user-friendly visualization features to help the user to analyze and understand the behavior of his B specification. This feedback is very beneficial to the understanding of the B specification since human perception is good at identifying structural similarities and symmetries. For more information on this particular topic, the reader can refer to <ref name="vispaper">M. Leuschel and E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, LNCS 3455. Springer-Verlag, 2005 https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf</ref> and <ref name="projpaper">L. Ladenberger and M. Leuschel: Mastering the Visualization of Larger State Spaces with Projection Diagrams. ICFEM'2015, LNCS 9407. Springer-Verlag, 2015. https://www3.hhu.de/stups/downloads/pdf/LadenbergerLeuschel_ProjectDiagram.pdf</ref>.		ProB provides several user-friendly visualization features to help the user to analyze and understand the behavior of his B specification. This feedback is very beneficial to the understanding of the B specification since human perception is good at identifying structural similarities and symmetries. For more information on this particular topic, the reader can refer to <ref name="vispaper">M. Leuschel and E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, LNCS 3455. Springer-Verlag, 2005 https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf</ref> and <ref name="projpaper">L. Ladenberger and M. Leuschel: Mastering the Visualization of Larger State Spaces with Projection Diagrams. ICFEM'2015, LNCS 9407. Springer-Verlag, 2015. https://www3.hhu.de/stups/downloads/pdf/LadenbergerLeuschel_ProjectDiagram.pdf</ref>.

	The visualization features of the ~~states pace~~ are in the "Visualize" menu, and comprise the command (visualize) "Statespace" and all the commands of the sub-menu "Statespace Projections". It is important to understand that those commands operate on the state space computed by ProB at the current point during the animation. Each time the user animates the B specification, the state space computed by ProB can be expanded if the selected operations lead to states not already computed by ProB.		In this page we discuss the visualization of the state space of a specification.
			Visualizing individual states can be visualized using [[Graphical_Visualization\|animation functions]], [[Custom_Graph]] definitions or using [[VisB]].

			The visualization features of the state space are in the "Visualize" menu, and comprise the command (visualize) "Statespace" and all the commands of the sub-menu "Statespace Projections". It is important to understand that those commands operate on the state space computed by ProB at the current point during the animation. Each time the user animates the B specification, the state space computed by ProB can be expanded if the selected operations lead to states not already computed by ProB.
	As shown in the following figure, the command (visualize) "Statespace" displays a diagram corresponding to the state space currently explored by the animation in a separate window.		As shown in the following figure, the command (visualize) "Statespace" displays a diagram corresponding to the state space currently explored by the animation in a separate window.

Michael Leuschel: /* Transition Diagram */

2021-11-27T07:23:34Z

Transition Diagram

← Older revision		Revision as of 07:23, 27 November 2021
Line 35:		Line 35:
	==== Transition Diagram ====		==== Transition Diagram ====
	The first command allows you to enter an expression (in B syntax).		The first command allows you to enter an expression (in B syntax).
	The command will then merge all states with the same value for that expression into an equivalence class node. In other words, the state space is projected onto the values of the expression. The generated graph contains only transitions which change the value of that expression.		The command will then merge all states with the same value for that expression into an equivalence class node. In other words, the state space is projected onto the values of the expression. The generated graph contains only transitions which change the value of that expression (unless the DOT_LOOPS preference is set to true).
	The command allows one to project the state space onto a single variable, a subset of variables (by using a tuple (v1,v2,...,vk) as expression). You can increase the projection by using B operators such as card, ran, dom or any other B operator. A more detailed explanation is given in <ref name="projpaper" />.		The command allows one to project the state space onto a single variable, a subset of variables (by using a tuple (v1,v2,...,vk) as expression). You can increase the projection by using B operators such as card, ran, dom or any other B operator. A more detailed explanation is given in <ref name="projpaper" />.
	The command can also be called from probcli using these commands (in conjunction with other commands like <tt>--model-check</tt>):		The command can also be called from probcli using these commands (in conjunction with other commands like <tt>--model-check</tt>):

Michael Leuschel: /* Transition Diagram */

2021-11-27T07:20:51Z

Transition Diagram

← Older revision		Revision as of 07:20, 27 November 2021
Line 45:		Line 45:
	curfloor / 3		curfloor / 3

	[[File:Lift_proj.~~pdf~~\|center]]		[[File:Lift_proj.png\|center]]

	==== Signature and DFA Merge ====		==== Signature and DFA Merge ====

Michael Leuschel: /* Transition Diagram */

2021-11-27T07:18:44Z

Transition Diagram

← Older revision		Revision as of 07:18, 27 November 2021
Line 45:		Line 45:
	curfloor / 3		curfloor / 3

	[[File:~~LiftProj~~.pdf\|center]]		[[File:Lift_proj.pdf\|center]]

	==== Signature and DFA Merge ====		==== Signature and DFA Merge ====

Michael Leuschel at 07:17, 27 November 2021

2021-11-27T07:17:46Z

← Older revision		Revision as of 07:17, 27 November 2021
Line 33:		Line 33:
	* Subgraph for GOAL		* Subgraph for GOAL

			==== Transition Diagram ====
	The first command allows you to enter an expression (in B syntax).		The first command allows you to enter an expression (in B syntax).
	The command will then merge all states with the same value for that expression into an equivalence class node. In other words, the state space is projected onto the values of the expression. The generated graph contains only transitions which change the value of that expression.		The command will then merge all states with the same value for that expression into an equivalence class node. In other words, the state space is projected onto the values of the expression. The generated graph contains only transitions which change the value of that expression.
Line 41:		Line 42:
	dot -Tpdf <DOTFILE >PDFFILE		dot -Tpdf <DOTFILE >PDFFILE

			Here is an example where a faulty lift model has been projected onto the expression
			curfloor / 3

			[[File:LiftProj.pdf\|center]]

			==== Signature and DFA Merge ====

	The two next commands in the menu "View Visited States\|View" provide a means to display a simplified version of the state space. A more detailed explanation is given in <ref name="vispaper" />.		The two next commands in the menu "View Visited States\|View" provide a means to display a simplified version of the state space. A more detailed explanation is given in <ref name="vispaper" />.

	The command "Signature-Merge Reduced Statespace" displays a state space where nodes sharing the same output arcs are collapsed into one node. The command "Reducted Deterministic Automaton of Visited States" removes the non-determinacy of the state space graph. The command "Select Operations & Arguments for Reduction" is used to specify which operations and arguments are affected by the previous transformations.		The command "Signature-Merge Reduced Statespace" displays a state space where nodes sharing the same output arcs are collapsed into one node. The command "Reducted Deterministic Automaton of Visited States" removes the non-determinacy of the state space graph. The command "Select Operations & Arguments for Reduction" is used to specify which operations and arguments are affected by the previous transformations.

			==== Sub Graphs ====

	The two last commands of the "Statespace Projections" sub-menu display subgraphs of the state space. The command "Subgraph for Invariant Violation" displays the subgraph of nodes which violate the invariant, while the command "Subgraph of nodes satisfying GOAL" displays the subgraph where goals (discussed in [[Temporal Model Checking#Specifying Goals and Assertions\|Temporal Model Checking]]) are satisfied.		The two last commands of the "Statespace Projections" sub-menu display subgraphs of the state space. The command "Subgraph for Invariant Violation" displays the subgraph of nodes which violate the invariant, while the command "Subgraph of nodes satisfying GOAL" displays the subgraph where goals (discussed in [[Temporal Model Checking#Specifying Goals and Assertions\|Temporal Model Checking]]) are satisfied.

Michael Leuschel: /* Statespace Projections */

2021-11-27T07:13:37Z

Statespace Projections

← Older revision		Revision as of 07:13, 27 November 2021
Line 36:		Line 36:
	The command will then merge all states with the same value for that expression into an equivalence class node. In other words, the state space is projected onto the values of the expression. The generated graph contains only transitions which change the value of that expression.		The command will then merge all states with the same value for that expression into an equivalence class node. In other words, the state space is projected onto the values of the expression. The generated graph contains only transitions which change the value of that expression.
	The command allows one to project the state space onto a single variable, a subset of variables (by using a tuple (v1,v2,...,vk) as expression). You can increase the projection by using B operators such as card, ran, dom or any other B operator. A more detailed explanation is given in <ref name="projpaper" />.		The command allows one to project the state space onto a single variable, a subset of variables (by using a tuple (v1,v2,...,vk) as expression). You can increase the projection by using B operators such as card, ran, dom or any other B operator. A more detailed explanation is given in <ref name="projpaper" />.
			The command can also be called from probcli using these commands (in conjunction with other commands like <tt>--model-check</tt>):
			probcli -dotexpr transition_diagram EXPR DOTFILE
			The generated dot file can be viewed with a viewer like dotty or can be converted, e.g., to PDF using:
			dot -Tpdf <DOTFILE >PDFFILE


	The two next commands in the menu "View Visited States\|View" provide a means to display a simplified version of the state space. A more detailed explanation is given in <ref name="vispaper" />.		The two next commands in the menu "View Visited States\|View" provide a means to display a simplified version of the state space. A more detailed explanation is given in <ref name="vispaper" />.

Michael Leuschel: /* Graph Nodes */

2021-11-27T07:09:37Z

Graph Nodes

← Older revision		Revision as of 07:09, 27 November 2021
Line 21:		Line 21:
	[[File:Trace_to_invariant_violation.png\|center]]		[[File:Trace_to_invariant_violation.png\|center]]

	Finally, if you have specified a goal predicate (either using a DEFINITION <tt>GOAL == P</tt> or by using a command such as "Find state satisfying predicate...") then those predicates are coloured in orange.		Finally, if you have specified a goal predicate (either using a DEFINITION <tt>GOAL == P</tt> or by using a command such as "Find state satisfying predicate...") then those predicates are coloured in orange. Many of the colours and shapes can be changed by adapting the corresponding preferences. A list of preferences is now shown automatically in ProB Tcl/Tk.

	=== Statespace Projections ===		=== Statespace Projections ===

Michael Leuschel at 07:02, 27 November 2021

2021-11-27T07:02:18Z

← Older revision		Revision as of 07:02, 27 November 2021
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	__NOTOC__		__NOTOC__
	ProB provides several user-friendly visualization features to help the user to analyze and understand the behavior of his B specification. This feedback is very beneficial to the understanding of the B specification since human perception is good at identifying structural similarities and symmetries. For more information on this particular topic, the reader can refer to <ref name="vispaper">M. Leuschel and E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, LNCS 3455. Springer-Verlag, 2005 https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf</ref> and <ref name="projpaper">L. Ladenberger and M. Leuschel: Mastering the Visualization of Larger State Spaces with Projection Diagrams. ICFEM'2015, LNCS 9407. Springer-Verlag, 2015.		ProB provides several user-friendly visualization features to help the user to analyze and understand the behavior of his B specification. This feedback is very beneficial to the understanding of the B specification since human perception is good at identifying structural similarities and symmetries. For more information on this particular topic, the reader can refer to <ref name="vispaper">M. Leuschel and E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, LNCS 3455. Springer-Verlag, 2005 https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf</ref> and <ref name="projpaper">L. Ladenberger and M. Leuschel: Mastering the Visualization of Larger State Spaces with Projection Diagrams. ICFEM'2015, LNCS 9407. Springer-Verlag, 2015. https://www3.hhu.de/stups/downloads/pdf/LadenbergerLeuschel_ProjectDiagram.pdf</ref>.

	The visualization features of the states pace are in the "Visualize" menu, and comprise the command (visualize) "Statespace" and all the commands of the sub-menu "Statespace Projections". It is important to understand that those commands operate on the state space computed by ProB at the current point during the animation. Each time the user animates the B specification, the state space computed by ProB can be expanded if the selected operations lead to states not already computed by ProB.		The visualization features of the states pace are in the "Visualize" menu, and comprise the command (visualize) "Statespace" and all the commands of the sub-menu "Statespace Projections". It is important to understand that those commands operate on the state space computed by ProB at the current point during the animation. Each time the user animates the B specification, the state space computed by ProB can be expanded if the selected operations lead to states not already computed by ProB.

Michael Leuschel at 07:00, 27 November 2021

2021-11-27T07:00:44Z

← Older revision		Revision as of 07:00, 27 November 2021
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	__NOTOC__		__NOTOC__
	ProB provides several user-friendly visualization features to help the user to analyze and understand the behavior of his B specification. This feedback is very beneficial to the understanding of the B specification since human perception is good at identifying structural similarities and symmetries. For more information on this particular topic, the reader can refer to <ref name="vispaper">M. Leuschel and E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, LNCS 3455. Springer-Verlag, 2005 https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf</ref>.		ProB provides several user-friendly visualization features to help the user to analyze and understand the behavior of his B specification. This feedback is very beneficial to the understanding of the B specification since human perception is good at identifying structural similarities and symmetries. For more information on this particular topic, the reader can refer to <ref name="vispaper">M. Leuschel and E.Turner: Visualising larger state spaces in ProB. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, ZB 2005: Formal Specification and Development in Z and B, LNCS 3455. Springer-Verlag, 2005 https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf</ref> and <ref name="projpaper">L. Ladenberger and M. Leuschel: Mastering the Visualization of Larger State Spaces with Projection Diagrams. ICFEM'2015, LNCS 9407. Springer-Verlag, 2015.

	The visualization features of the states pace are in the "Visualize" menu, and comprise the command (visualize) "Statespace" and all the commands of the sub-menu "Statespace Projections". It is important to understand that those commands operate on the state space computed by ProB at the current point during the animation. Each time the user animates the B specification, the state space computed by ProB can be expanded if the selected operations lead to states not already computed by ProB.		The visualization features of the states pace are in the "Visualize" menu, and comprise the command (visualize) "Statespace" and all the commands of the sub-menu "Statespace Projections". It is important to understand that those commands operate on the state space computed by ProB at the current point during the animation. Each time the user animates the B specification, the state space computed by ProB can be expanded if the selected operations lead to states not already computed by ProB.
Line 35:		Line 35:
	The first command allows you to enter an expression (in B syntax).		The first command allows you to enter an expression (in B syntax).
	The command will then merge all states with the same value for that expression into an equivalence class node. In other words, the state space is projected onto the values of the expression. The generated graph contains only transitions which change the value of that expression.		The command will then merge all states with the same value for that expression into an equivalence class node. In other words, the state space is projected onto the values of the expression. The generated graph contains only transitions which change the value of that expression.
	The command allows one to project the state space onto a single variable, a subset of variables (by using a tuple (v1,v2,...,vk) as expression). You can increase the projection by using B operators such as card, ran, dom or any other B operator.		The command allows one to project the state space onto a single variable, a subset of variables (by using a tuple (v1,v2,...,vk) as expression). You can increase the projection by using B operators such as card, ran, dom or any other B operator. A more detailed explanation is given in <ref name="projpaper" />.

	The two next commands in the menu "View Visited States\|View" provide a means to display a simplified version of the state space. A more detailed explanation is given in <ref name="vispaper" />.		The two next commands in the menu "View Visited States\|View" provide a means to display a simplified version of the state space. A more detailed explanation is given in <ref name="vispaper" />.

Michael Leuschel: /* Statespace Projections */

2021-11-27T06:57:47Z

Statespace Projections

← Older revision		Revision as of 06:57, 27 November 2021
Line 27:		Line 27:
	The sub-menu "Statespace Projections" contains several other commands that provide useful views on the state space.		The sub-menu "Statespace Projections" contains several other commands that provide useful views on the state space.

	~~The three next commands in the menu "View Visited States\|View" provide a means to display a simplified version of the state space~~. ~~A more detailed explanation is given in <ref name="vispaper" />~~.		* Transition Diagram for Custom Expression ...
			* Signature-Merge Reduced Statespace...
			* DFA Reduced Statespace
			* Subgraph leading to Invariant Violation
			* Subgraph for GOAL

	The command "~~Reduced~~ Visited States" displays a state space where nodes sharing the same output arcs are collapsed into one node. The command "Reducted Deterministic Automaton of Visited States" removes the non-determinacy of the state space graph. The command "Select Operations & Arguments for Reduction" is used to specify which operations and arguments are affected by the previous transformations.		The first command allows you to enter an expression (in B syntax).
			The command will then merge all states with the same value for that expression into an equivalence class node. In other words, the state space is projected onto the values of the expression. The generated graph contains only transitions which change the value of that expression.
			The command allows one to project the state space onto a single variable, a subset of variables (by using a tuple (v1,v2,...,vk) as expression). You can increase the projection by using B operators such as card, ran, dom or any other B operator.

			The two next commands in the menu "View Visited States\|View" provide a means to display a simplified version of the state space. A more detailed explanation is given in <ref name="vispaper" />.

			The command "Signature-Merge Reduced Statespace" displays a state space where nodes sharing the same output arcs are collapsed into one node. The command "Reducted Deterministic Automaton of Visited States" removes the non-determinacy of the state space graph. The command "Select Operations & Arguments for Reduction" is used to specify which operations and arguments are affected by the previous transformations.

	The two last commands of the "Statespace Projections" sub-menu display subgraphs of the state space. The command "Subgraph for Invariant Violation" displays the subgraph of nodes which violate the invariant, while the command "Subgraph of nodes satisfying GOAL" displays the subgraph where goals (discussed in [[Temporal Model Checking#Specifying Goals and Assertions\|Temporal Model Checking]]) are satisfied.		The two last commands of the "Statespace Projections" sub-menu display subgraphs of the state space. The command "Subgraph for Invariant Violation" displays the subgraph of nodes which violate the invariant, while the command "Subgraph of nodes satisfying GOAL" displays the subgraph where goals (discussed in [[Temporal Model Checking#Specifying Goals and Assertions\|Temporal Model Checking]]) are satisfied.