Tutorial LTL Counter-example View - Revision history

Ivaylo Dobrikov: /* Use Case for the LTL Counter-example Viewer */

2015-08-30T08:27:03Z

Use Case for the LTL Counter-example Viewer

← Older revision		Revision as of 08:27, 30 August 2015
Line 80:		Line 80:
	Each state of the counter-example is colored in red since ‘F {p1=crit1}’ does not hold for all states of the path. Additionally, state <math>s_{0}</math> has been highlighted since '''all''' paths starting in <math>s_{0}</math> do not satisfy ‘F {p1=crit1}’ (the semantic of the globally-operator).		Each state of the counter-example is colored in red since ‘F {p1=crit1}’ does not hold for all states of the path. Additionally, state <math>s_{0}</math> has been highlighted since '''all''' paths starting in <math>s_{0}</math> do not satisfy ‘F {p1=crit1}’ (the semantic of the globally-operator).

	To see why the LTL formula ‘F {p1=crit1}’ does not hold in each state of the path in Figure 6 click on one of the nodes in the visualization. As a result, a second box will appear visualizing the counter-example in regard to the LTL formula ‘F {p1=crit1}’. In the second visualization all states are colored in red since ~~‘{p1~~=~~crit1}’~~ does not hold in all states. All states are highlighted as well since ‘F {p1=crit1}’ holds if and only if there is a state in which ''p1'' is equal to ''crit1'' and thus all states are significant for the violation of the formula.		To see why the LTL formula ‘F {p1=crit1}’ does not hold in each state of the path in Figure 6 click on one of the nodes in the visualization. As a result, a second box will appear visualizing the counter-example in regard to the LTL formula ‘F {p1=crit1}’. In the second visualization all states are colored in red since ‘p1=crit1’ does not hold in all states. All states are highlighted as well since ‘F {p1=crit1}’ holds if and only if there is a state in which ''p1'' is equal to ''crit1'' and thus all states are significant for the violation of the formula.

	<br/>[[File:LTLViewVisualisation6.png\|center\|350px]]<br/>		<br/>[[File:LTLViewVisualisation6.png\|center\|350px]]<br/>
Line 88:		Line 88:
	<br/>[[File:LTLViewVisualisation4.png\|center\|350px]]<br/>		<br/>[[File:LTLViewVisualisation4.png\|center\|350px]]<br/>

	In this visualization the crucial state for violating the property ‘G ({p1=wait1} => F {p1=crit1})’ is <math>s_{1}</math> since at this state ~~‘{p1~~=~~wait1}’~~ becomes true. Once a state is encountered where ~~‘{p1~~=~~wait1}’~~ holds, it should be guaranteed that eventually ~~‘{p1~~=~~crit1}’~~ will hold. This is apparently not fulfilled as in all successor states ''p1'' will not become equal to ''crit1''.		In this visualization the crucial state for violating the property ‘G ({p1=wait1} => F {p1=crit1})’ is <math>s_{1}</math> since at this state ‘p1=wait1’ becomes true. Once a state is encountered where ‘p1=wait1’ holds, it should be guaranteed that eventually ‘p1=crit1’ will hold. This is apparently not fulfilled as in all successor states ''p1'' will not become equal to ''crit1''.

	== Literature Sources ==		== Literature Sources ==

Ivaylo Dobrikov: /* Visualization of Counter-examples in Rodin */

2015-08-30T08:21:54Z

Visualization of Counter-examples in Rodin

← Older revision		Revision as of 08:21, 30 August 2015
Line 42:		Line 42:

	''' Obtaining transition and state information'''<br/>		''' Obtaining transition and state information'''<br/>
	A path reported as a counter-example of an LTL formula represents a possible trace of the model being analyzed. In some cases it may be helpful to know which transitions are executed along the path in order to reproduce the erroneous behavior of the model (e.g. by animating the trace). To see which transitions are being executed in the counter-example hold the mouse cursor on the respective edge. A label will ~~come up~~ with the transition name:		A path reported as a counter-example of an LTL formula represents a possible trace of the model being analyzed. In some cases it may be helpful to know which transitions are executed along the path in order to reproduce the erroneous behavior of the model (e.g. by animating the trace). To see which transitions are being executed in the counter-example hold the mouse cursor on the respective edge. A label will appear with the transition name:

	<br/>[[File:LTLViewVisualisation3.png\|center\|250px]]<br/>		<br/>[[File:LTLViewVisualisation3.png\|center\|250px]]<br/>

Ivaylo Dobrikov: /* Visualization of Counter-examples in Rodin */

2015-08-30T08:20:47Z

Visualization of Counter-examples in Rodin

← Older revision		Revision as of 08:20, 30 August 2015
Line 25:		Line 25:
	<br/>[[File:LTLViewVisualisation1.png\|center\|250px]]<br/>		<br/>[[File:LTLViewVisualisation1.png\|center\|250px]]<br/>

	Since the value of the atom ‘{p2=crit2}’ in <math>s_{1}</math> is equal to false the value of the LTL formula ‘X {p2=crit2}’ in <math>s_{0}</math> is also equal to false. Therefore, the first state is colored in red. On the other hand, the value of the formula ‘X {p2=crit2}’ in <math>s_{1}</math> is unknown as there is no successor state of <math>s_{1}</math> in the path ~~showed~~ in Figure 4. Accordingly, the second state in the LTL counter-example viewer will be colored in grey.		Since the value of the atom ‘{p2=crit2}’ in <math>s_{1}</math> is equal to false the value of the LTL formula ‘X {p2=crit2}’ in <math>s_{0}</math> is also equal to false. Therefore, the first state is colored in red. On the other hand, the value of the formula ‘X {p2=crit2}’ in <math>s_{1}</math> is unknown as there is no successor state of <math>s_{1}</math> in the path, as shown in Figure 4. Accordingly, the second state in the LTL counter-example viewer will be colored in grey.
	<br/>[[File:LTLViewFinitePathUnknown.png\|center\|250px]]<br/>		<br/>[[File:LTLViewFinitePathUnknown.png\|center\|250px]]<br/>

Line 48:		Line 48:
	Another way to find out the transitions of the path is to inspect the current trace loaded in the history view.		Another way to find out the transitions of the path is to inspect the current trace loaded in the history view.

	To view a state of a counter-example ~~showed~~ in the LTL counter-example view perform a double-click action on the respective state. After double-clicking a state the relevant information (variables’ evaluation, invariant evaluation, etc.) of the state is displayed in the state view and the trace leading to the double-clicked state is loaded in the history view.		To view a state of a counter-example shown in the LTL counter-example view perform a double-click action on the respective state. After double-clicking a state the relevant information (variables’ evaluation, invariant evaluation, etc.) of the state is displayed in the state view and the trace leading to the double-clicked state is loaded in the history view.

	'''Number of visualizations per LTL formula'''<br/>		'''Number of visualizations per LTL formula'''<br/>

Ivaylo Dobrikov: /* Use Case for the LTL Counter-example Viewer */

2015-03-10T12:56:47Z

Use Case for the LTL Counter-example Viewer

← Older revision		Revision as of 12:56, 10 March 2015
Line 78:		Line 78:
	<br/>[[File:LTLViewVisualisation5.png\|center\|350px]]<br/>		<br/>[[File:LTLViewVisualisation5.png\|center\|350px]]<br/>

	Each state of the counter-example is colored in red since ‘F {p1=crit1}’ does not hold for all states of the path. Additionally, state <math>s_{0}</math> has been highlighted since '''all''' paths starting at <math>s_{0}</math> do not satisfy ‘F {p1=crit1}’ (the semantic of the globally-operator).		Each state of the counter-example is colored in red since ‘F {p1=crit1}’ does not hold for all states of the path. Additionally, state <math>s_{0}</math> has been highlighted since '''all''' paths starting in <math>s_{0}</math> do not satisfy ‘F {p1=crit1}’ (the semantic of the globally-operator).

	To see why the LTL formula ‘F {p1=crit1}’ does not hold in each state of the path in Figure 6 click on one of the nodes in the visualization. As a result, a second box will appear visualizing the counter-example in regard to the LTL formula ‘F {p1=crit1}’. In the second visualization all states are colored in red since ‘{p1=crit1}’ does not hold in all states. All states are highlighted as well since ‘F {p1=crit1}’ holds if and only if there is a state in which ''p1'' is equal to ''crit1'' and thus all states are significant for the violation of the formula.		To see why the LTL formula ‘F {p1=crit1}’ does not hold in each state of the path in Figure 6 click on one of the nodes in the visualization. As a result, a second box will appear visualizing the counter-example in regard to the LTL formula ‘F {p1=crit1}’. In the second visualization all states are colored in red since ‘{p1=crit1}’ does not hold in all states. All states are highlighted as well since ‘F {p1=crit1}’ holds if and only if there is a state in which ''p1'' is equal to ''crit1'' and thus all states are significant for the violation of the formula.

Ivaylo Dobrikov: /* Use Case for the LTL Counter-example Viewer */

2015-03-10T12:54:09Z

Use Case for the LTL Counter-example Viewer

← Older revision		Revision as of 12:54, 10 March 2015
Line 78:		Line 78:
	<br/>[[File:LTLViewVisualisation5.png\|center\|350px]]<br/>		<br/>[[File:LTLViewVisualisation5.png\|center\|350px]]<br/>

	Each state of the counter-example is colored in red since ‘F {p1=crit1}’ does not hold in all states of the path. Additionally, state <math>s_{0}</math> has been highlighted since '''all''' paths starting at <math>s_{0}</math> do not satisfy ‘F {p1=crit1}’ (the semantic of the globally-operator).		Each state of the counter-example is colored in red since ‘F {p1=crit1}’ does not hold for all states of the path. Additionally, state <math>s_{0}</math> has been highlighted since '''all''' paths starting at <math>s_{0}</math> do not satisfy ‘F {p1=crit1}’ (the semantic of the globally-operator).

	To see why the LTL formula ‘F {p1=crit1}’ does not hold in each state of the path in Figure 6 click on one of the nodes in the visualization. As a result, a second box will appear visualizing the counter-example in regard to the LTL formula ‘F {p1=crit1}’. In the second visualization all states are colored in red since ‘{p1=crit1}’ does not hold in all states. All states are highlighted as well since ‘F {p1=crit1}’ holds if and only if there is a state in which ''p1'' is equal to ''crit1'' and thus all states are significant for the violation of the formula.		To see why the LTL formula ‘F {p1=crit1}’ does not hold in each state of the path in Figure 6 click on one of the nodes in the visualization. As a result, a second box will appear visualizing the counter-example in regard to the LTL formula ‘F {p1=crit1}’. In the second visualization all states are colored in red since ‘{p1=crit1}’ does not hold in all states. All states are highlighted as well since ‘F {p1=crit1}’ holds if and only if there is a state in which ''p1'' is equal to ''crit1'' and thus all states are significant for the violation of the formula.

Ivaylo Dobrikov: /* Visualization of Counter-examples in Rodin */

2015-01-28T13:26:32Z

Visualization of Counter-examples in Rodin

← Older revision		Revision as of 13:26, 28 January 2015
Line 25:		Line 25:
	<br/>[[File:LTLViewVisualisation1.png\|center\|250px]]<br/>		<br/>[[File:LTLViewVisualisation1.png\|center\|250px]]<br/>

	Since the value of the atom ‘{p2=crit2}’ in <math>s_{1}</math> is equal to false the value of the LTL formula ‘X {p2=crit2}’ in <math>s_{0}</math> is also equal to false. Therefore the first state is colored in red. On the other hand, the value of the formula ‘X {p2=crit2}’ in <math>s_{1}</math> is unknown as there is no successor state of <math>s_{1}</math> in the path showed in Figure 4. Accordingly, the second state in the LTL counter-example viewer will be colored in grey.		Since the value of the atom ‘{p2=crit2}’ in <math>s_{1}</math> is equal to false the value of the LTL formula ‘X {p2=crit2}’ in <math>s_{0}</math> is also equal to false. Therefore, the first state is colored in red. On the other hand, the value of the formula ‘X {p2=crit2}’ in <math>s_{1}</math> is unknown as there is no successor state of <math>s_{1}</math> in the path showed in Figure 4. Accordingly, the second state in the LTL counter-example viewer will be colored in grey.
	<br/>[[File:LTLViewFinitePathUnknown.png\|center\|250px]]<br/>		<br/>[[File:LTLViewFinitePathUnknown.png\|center\|250px]]<br/>

Ivaylo Dobrikov: /* Use Case for the LTL Counter-example Viewer */

2014-12-03T09:21:09Z

Use Case for the LTL Counter-example Viewer

← Older revision		Revision as of 09:21, 3 December 2014
Line 63:		Line 63:
	<br/>[[File:LTLViewMUTEXEvents.png\|center\|600px]]<br/>		<br/>[[File:LTLViewMUTEXEvents.png\|center\|600px]]<br/>

	Each process <math>P_{i}</math> has three possible states that are denoted by the constants <math>noncrit_{i}</math> (the state in which <math>P_{i} </math> performs noncritical actions), <math>wait_{i}</math> (the state in which <math>P_{i}</math> waits to enter the critical section), and <math>crit_{i}</math> (representing the state in which <math>P_{i}</math> is in the critical section). Both processes share the binary semaphore y where y=1 indicates that the semaphore is free and y=0 that the semaphore is currently processed by one of the processes.		Each process <math>P_{i}</math> has three possible states that are denoted by the constants <math>noncrit_{i}</math> (the state in which <math>P_{i} </math> performs noncritical actions), <math>wait_{i}</math> (the state in which <math>P_{i}</math> waits to enter the critical section), and <math>crit_{i}</math> (representing the state in which <math>P_{i}</math> is in the critical section). Both processes share the binary semaphore y, where y=1 indicates that the semaphore is free and y=0 that the semaphore is currently processed by one of the processes.

	There are several requirements that the mutual exclusion algorithm should satisfy. The most important one is the mutual exclusion property that says ''always at most one process is in its critical section''. This can be simply expressed, for example, as an invariant of the respective Event-B model: ‘not(p1 = crit1 & p2 = crit2)’. However, there are other properties that can be easily expressed by means of LTL formulas and automatically checked on the model. For example, the requirement ''each process will enter infinitely often its critical section'' can be specified by the LTL formula `GF {p1 = crit1} & GF {p2 = crit2}` and the starvation freedom property that states ''each waiting process will eventually enter its critical section'' can be encoded in LTL by means of the formula `G ({p1 = wait1} => F {p1 = crit1}) & G ({p2 = wait2} => F {p2=crit2}) `.		There are several requirements that the mutual exclusion algorithm should satisfy. The most important one is the mutual exclusion property that says ''always at most one process is in its critical section''. This can be simply expressed, for example, as an invariant of the respective Event-B model: ‘not(p1 = crit1 & p2 = crit2)’. However, there are other properties that can be easily expressed by means of LTL formulas and automatically checked on the model. For example, the requirement ''each process will enter infinitely often its critical section'' can be specified by the LTL formula `GF {p1 = crit1} & GF {p2 = crit2}` and the starvation freedom property that states ''each waiting process will eventually enter its critical section'' can be encoded in LTL by means of the formula `G ({p1 = wait1} => F {p1 = crit1}) & G ({p2 = wait2} => F {p2=crit2}) `.

Ivaylo Dobrikov: /* Visualization of Counter-examples in Rodin */

2014-12-03T09:17:34Z

Visualization of Counter-examples in Rodin

← Older revision		Revision as of 09:17, 3 December 2014
Line 36:		Line 36:
	The path in Figure 5 violates ‘{p1=noncrit1} U {p1=crit1}’ since the goal (‘{p1=crit1}’) of the until-formula does not hold in all states of the path. This is illustrated by means of the bottom colored path in the picture above. Both states have been colored with bright red as both are significant for the violation of the until-formula in regard to ‘{p1=crit1}’.		The path in Figure 5 violates ‘{p1=noncrit1} U {p1=crit1}’ since the goal (‘{p1=crit1}’) of the until-formula does not hold in all states of the path. This is illustrated by means of the bottom colored path in the picture above. Both states have been colored with bright red as both are significant for the violation of the until-formula in regard to ‘{p1=crit1}’.

	The upper path in the picture above has been evaluated and colored in regard to the condition (‘{p1=noncrit1}’) of the until-formula. The critical state here is the second one as ‘{p1=noncrit1}’ does not hold in that state and therefore it is highlighted by ~~a brighter color~~. On the other hand, the atom ‘{p1=noncrit1}’ holds in <math>s_{0}</math> and thus the state is colored in green. <math>s_{0}</math> has been grayed out since the evaluation of ‘{p1=noncrit1}’ in that state has no significant meaning for the violation of ‘{p1=noncrit1} U {p1=crit1}’.		The upper path in the picture above has been evaluated and colored in regard to the condition (‘{p1=noncrit1}’) of the until-formula. The critical state here is the second one as ‘{p1=noncrit1}’ does not hold in that state and therefore it is highlighted by bright red. On the other hand, the atom ‘{p1=noncrit1}’ holds in <math>s_{0}</math> and thus the state is colored in green. <math>s_{0}</math> has been grayed out since the evaluation of ‘{p1=noncrit1}’ in that state has no significant meaning for the violation of ‘{p1=noncrit1} U {p1=crit1}’.
	<br/>[[File:LTLViewFinitePathUntil.png\|center\|300px]]<br/>		<br/>[[File:LTLViewFinitePathUntil.png\|center\|300px]]<br/>

Ivaylo Dobrikov: /* Use Case for the LTL Counter-example Viewer */

2014-11-10T18:20:58Z

Use Case for the LTL Counter-example Viewer

← Older revision		Revision as of 18:20, 10 November 2014
Line 84:		Line 84:
	<br/>[[File:LTLViewVisualisation6.png\|center\|350px]]<br/>		<br/>[[File:LTLViewVisualisation6.png\|center\|350px]]<br/>

	For the starvation freedom property (''each waiting process will eventually enter its critical section'') of process P1 three operators are needed for encoding it in LTL: ‘G ({p1=wait1} => F {p1=crit1})’. The mutual exclusion model violates the property because it permits the second process P2 to perform infinitely often consecutively the events Req2, Enter2, Rel2 and thus not allowing process P1 to get access to its critical section. This means that the path in Figure 6 may also be reported as a counter-example for: ‘G ({p1=wait1} => F {p1=crit1})’ by the LTL model checker. As a consequence, the following visualization will be shown in the LTL counter-example view:		For the starvation freedom property (''each waiting process will eventually enter its critical section'') of process P1 three operators are needed for encoding it in LTL: ‘G ({p1=wait1} => F {p1=crit1})’. The mutual exclusion model violates the property because it permits the second process P2 to perform infinitely often consecutively the events Req2, Enter2, Rel2 and thus not allowing process P1 to get access to its critical section. This means that the path in Figure 6 may also be reported as a counter-example for ‘G ({p1=wait1} => F {p1=crit1})’ by the LTL model checker. As a consequence, the following visualization will be shown in the LTL counter-example view:

	<br/>[[File:LTLViewVisualisation4.png\|center\|350px]]<br/>		<br/>[[File:LTLViewVisualisation4.png\|center\|350px]]<br/>

Ivaylo Dobrikov: /* Use Case for the LTL Counter-example Viewer */

2014-11-10T18:17:29Z

Use Case for the LTL Counter-example Viewer

← Older revision		Revision as of 18:17, 10 November 2014
Line 80:		Line 80:
	Each state of the counter-example is colored in red since ‘F {p1=crit1}’ does not hold in all states of the path. Additionally, state <math>s_{0}</math> has been highlighted since '''all''' paths starting at <math>s_{0}</math> do not satisfy ‘F {p1=crit1}’ (the semantic of the globally-operator).		Each state of the counter-example is colored in red since ‘F {p1=crit1}’ does not hold in all states of the path. Additionally, state <math>s_{0}</math> has been highlighted since '''all''' paths starting at <math>s_{0}</math> do not satisfy ‘F {p1=crit1}’ (the semantic of the globally-operator).

	To see why the LTL formula ‘F {p1=crit1}’ does not hold in each state of the path in Figure 6 click on one of the nodes in the visualization. As a ~~consequence~~ a second box will appear visualizing the counter-example in regard to the LTL formula ‘F {p1=crit1}’. In the second visualization all states are colored in red since ‘{p1=crit1}’ does not hold in all states. All states are highlighted as well since ‘F {p1=crit1}’ holds if and only if there is a state in which ''p1'' is equal to ''crit1'' and thus all states are significant for the violation of the formula.		To see why the LTL formula ‘F {p1=crit1}’ does not hold in each state of the path in Figure 6 click on one of the nodes in the visualization. As a result, a second box will appear visualizing the counter-example in regard to the LTL formula ‘F {p1=crit1}’. In the second visualization all states are colored in red since ‘{p1=crit1}’ does not hold in all states. All states are highlighted as well since ‘F {p1=crit1}’ holds if and only if there is a state in which ''p1'' is equal to ''crit1'' and thus all states are significant for the violation of the formula.

	<br/>[[File:LTLViewVisualisation6.png\|center\|350px]]<br/>		<br/>[[File:LTLViewVisualisation6.png\|center\|350px]]<br/>