Checking CSP Assertions - Revision history

Ivaylo Dobrikov: /* CSP Assertions Viewer */

2016-09-23T09:28:13Z

CSP Assertions Viewer

← Older revision		Revision as of 09:28, 23 September 2016
Line 133:		Line 133:
	** Assertion check interrupted by user. <br/><br/> Note that in case of an LTL and a CTL assertion the check could fail to complete because of a syntax error in the respective formula. If an assertion check fails to complete an error box is popped up displaying an error message, which indicates why the assertion check could not be completed.		** Assertion check interrupted by user. <br/><br/> Note that in case of an LTL and a CTL assertion the check could fail to complete because of a syntax error in the respective formula. If an assertion check fails to complete an error box is popped up displaying an error message, which indicates why the assertion check could not be completed.

	An assertion can be selected by clicking on it with Mouse-1 and checked by double-clicking on it with Mouse-1. Alternatively, selecting an assertion and then pressing the Enter key can start the respective assertion check. When an assertion check is in progress, the assertion will be marked by the clock symbol (⌚). If the assertion check is completed without interrupting it, a new status is assigned to the assertion: tick symbol (✔) indicating that the assertion was completed successfully or cross symbol (✘) indicating that a counterexample was found to the stated property. In case that the status is cross the counterexample can be explored by (second) double-click with Mouse-1 on the assertion or by selecting the assertion and then pressing the Enter key. If the respective assertion is negated, i.e. there is `not` in front of the assertion property, and marked with a cross, then no counterexample can be explored as the proper statement holds.		An assertion can be selected by clicking on it with Mouse-1 and checked by double-clicking on it with Mouse-1. Alternatively, selecting an assertion and then pressing the Enter key can start the respective assertion check. When an assertion check is in progress, the assertion will be marked by the clock symbol (⌚). If the assertion check is completed without interrupting it, a new status is assigned to the assertion: tick symbol (✔) indicating that the assertion was completed successfully or cross symbol (✘) indicating that a counterexample was found for the stated property. In case that the status is cross the counterexample can be explored by (second) double-click with Mouse-1 on the assertion or by selecting the assertion and then pressing the Enter key. If the respective assertion is negated, i.e. there is `not` in front of the assertion property, and marked with a cross, then no counterexample can be explored as the proper statement holds.

	The list box is equipped with a contextual menu (or a pop-up menu), which appears when you right-click on an assertion in the list. Depending on the type and the status of the assertion the contextual menu provides options for checking, debugging, modifying the respective assertion, as well as various other options. Take, for example, the selected assertion on which the contextual menu is popped up in the picture below.		The list box is equipped with a contextual menu (or a pop-up menu), which appears when you right-click on an assertion in the list. Depending on the type and the status of the assertion the contextual menu provides options for checking, debugging, modifying the respective assertion, as well as various other options. Take, for example, the selected assertion on which the contextual menu is popped up in the picture below.

Ivaylo Dobrikov: /* Checking CSP Assertions with `probcli` */

2016-02-22T15:59:19Z

Checking CSP Assertions with `probcli`

← Older revision		Revision as of 15:59, 22 February 2016
Line 225:		Line 225:

	Note that the assertion should be placed between quotes. In addition, when an assertion is checked with the '-csp_assertion' option the keyword '''assert''' should be omitted.		Note that the assertion should be placed between quotes. In addition, when an assertion is checked with the '-csp_assertion' option the keyword '''assert''' should be omitted.

			Notice that for checking LTL and CTL assertions from the command line you need to escape the double quotes (") wrapping the respective LTL/CTL formula by means of a backslash \.
			probcli -csp_assertion "Q \|= LTL: \"F [c]\"" example.csp

	== References and Notes ==		== References and Notes ==
	<references/>		<references/>

Ivaylo Dobrikov: /* Debugging Non-satisfied Assertions */

2016-02-22T13:28:10Z

Debugging Non-satisfied Assertions

Ivaylo Dobrikov: /* Debugging Non-satisfied Assertions */

2015-09-07T08:45:28Z

Debugging Non-satisfied Assertions

← Older revision		Revision as of 08:45, 7 September 2015
Line 191:		Line 191:
	<tt>assert P :[deadlock free [F]]</tt>.		<tt>assert P :[deadlock free [F]]</tt>.

	The check of the assertion will finish by marking the assertion in the list box with a cross symbol. The cross symbol indicates that a counterexample was found for the assertion checks. The counterexample is basically given by the trace <a,b,c> as obviously `P` reaches a deadlock state after performing the trace <a,b,c>. Providing a second double-click on the assertion will open the following debugging window:		The check of the assertion will finish by marking the assertion in the list box with a cross symbol (✘). The cross symbol indicates that a counterexample was found for the assertion checks. The counterexample is basically given by the trace <math>\langle a,b,c \rangle</math> as obviously `P` reaches a deadlock state after performing the trace <math>\langle a,b,c \rangle</math>. Providing a second double-click on the assertion will open the following debugging window:

	[[file: CSP_Deadlock_Trace.png]]		[[file: CSP_Deadlock_Trace.png]]

	Considering the CSP process `Q` and `R` one can see or check that `R` is a trace refinement of `Q` as `R` performs the same set of traces as `Q`. Thus, the assertion check for `Q [T= R` will mark the assertion statement in the list box by a tick symbol. On the other hand, checking the assertion `R [T= Q` will find a counterexample for the refinement check. Performing a second double-click on the item `R [T= Q` will open the following trace debugger window with the counterexample displayed in it:		Considering the CSP process `Q` and `R` one can see or check that `R` is a trace refinement of `Q` as `R` performs the same set of traces as `Q`. Thus, the assertion check for `Q [T= R` will mark the assertion statement in the list box by a tick symbol (✔). On the other hand, checking the assertion `R [T= Q` will find a counterexample for the refinement check. Performing a second double-click on the item `R [T= Q` will open the following trace debugger window with the counterexample displayed in it:

	[[file: CSP_Trace_Debugger.png]]		[[file: CSP_Trace_Debugger.png]]

	A counterexample of a trace-refinement assertion is a trace leading to a state in which the implementation process performs an event that the specification process cannot perform. In the example above both processes `P` and `Q` perform the trace <a> and reach states in which the implementation process can perform an event that is not offered by the specification process. One can easily deduce from the picture above that `Q` performs after `a` the event `c` which is not offered by `R` as `R` can perform only `b` after `a`. In the left most column `Accept` the debugger window lists all possible events that are offered by the specification process after performing the trace given in the `Trace` column next to `Accepts`.		A counterexample of a trace-refinement assertion is a trace leading to a state in which the implementation process performs an event that the specification process cannot perform. In the example above both processes `P` and `Q` perform the trace <math>\langle a \rangle</math> and reach states in which the implementation process can perform an event that is not offered by the specification process ''R''. One can easily deduce from the picture above that `Q` performs after `a` the event `c` which is not offered by `R` as `R` can perform only `b` after `a`. In the left most column `Accept` the debugger window lists all possible events that are offered by the specification process after performing the trace given in the `Trace` column next to `Accepts`.

	As we already mentioned above `R` is a trace-refinement of `Q`. On the other hand, checking whether `R` is a failures-refinement of `Q` will produce a counterexample as `R` refuses the event `c` that is offered by Q after executing `a`. Accordingly, the counterexample will be illustrated within the following trace debugger window:		As we already mentioned above `R` is a trace-refinement of `Q`. On the other hand, checking whether `R` is a failures-refinement of `Q` will produce a counterexample as `R` refuses the event `c` that is offered by Q after executing `a`. Accordingly, the counterexample will be illustrated within the following trace debugger window:

Ivaylo Dobrikov: /* CSP Assertions Viewer */

2015-09-07T08:38:18Z

CSP Assertions Viewer

← Older revision		Revision as of 08:38, 7 September 2015
Line 171:		Line 171:
	* '''Add''': Attaching a new assertion to the list of assertions in the list box. If the entry in one of the selectors is empty no assertion will be added to list box and a warning message will appear informing the user that some of the entries were not specified. If the entered assertion in the tab page is already in the list box, then a warning box appears informing the user that the assertion is already in the list box. If the assertion is present in the list box it will not be added.		* '''Add''': Attaching a new assertion to the list of assertions in the list box. If the entry in one of the selectors is empty no assertion will be added to list box and a warning message will appear informing the user that some of the entries were not specified. If the entered assertion in the tab page is already in the list box, then a warning box appears informing the user that the assertion is already in the list box. If the assertion is present in the list box it will not be added.
	* '''Check''': Attaching a new assertion to the list of assertions in the list box and immediately starting checking the assertion. If the assertion is already in the list box, then the user will be informed that the assertion is already in the list box and in case it is not checked yet its check will be started.		* '''Check''': Attaching a new assertion to the list of assertions in the list box and immediately starting checking the assertion. If the assertion is already in the list box, then the user will be informed that the assertion is already in the list box and in case it is not checked yet its check will be started.
	* '''Cancel/Interrupt''': Closes the window or interrupts an assertion check. In case the “Cancel” command is executed all checks and new assertions will get lost. If an assertion is currently checked, then the button command “Cancel” is replaced by another button command ‘’Interrupt’’, which causes the interruption of the current assertion check when the button is clicked.		* '''Cancel/Interrupt''': Closes the window or interrupts an assertion check. In case the “Cancel” command is executed all checks and new assertions will get lost. If an assertion is currently checked, then the button command “Cancel” is replaced by another button command ‘’Interrupt’’, which causes the interruption of the current assertion check when the button is clicked on.

	== Debugging Non-satisfied Assertions ==		== Debugging Non-satisfied Assertions ==

Ivaylo Dobrikov: /* CSP Assertions Viewer */

2015-09-07T08:37:43Z

CSP Assertions Viewer

Ivaylo Dobrikov: /* CSP Assertions Viewer */

2015-09-07T08:29:02Z

CSP Assertions Viewer

← Older revision		Revision as of 08:29, 7 September 2015
Line 133:		Line 133:
	** Assertion check interrupted by user. <br/><br/> Note that in case of an LTL and a CTL assertion the check could fail to complete because of a syntax error in the respective formula. If an assertion check fails to complete an error box is popped up displaying an error message, which indicates why the assertion check could not be completed.		** Assertion check interrupted by user. <br/><br/> Note that in case of an LTL and a CTL assertion the check could fail to complete because of a syntax error in the respective formula. If an assertion check fails to complete an error box is popped up displaying an error message, which indicates why the assertion check could not be completed.

	An assertion can be selected by clicking on it with Mouse-1 and checked by double-clicking on it with Mouse-1. Alternatively, selecting an assertion and then pressing the Enter key can start the respective assertion check. When an assertion check is in progress, the assertion will be marked by the clock symbol. If the assertion check is completed without interrupting it, a new status is assigned to the assertion: tick symbol indicating that the assertion was completed successfully or cross symbol indicating that a counterexample was found to the stated property. In case that the status is cross the counterexample can be explored by (second) double-click with Mouse-1 on the assertion or by selecting the assertion and then pressing the Enter key. If the respective assertion is negated, i.e. there is `not` in front of the assertion property, and marked with a cross, then no counterexample can be explored as the proper statement holds.		An assertion can be selected by clicking on it with Mouse-1 and checked by double-clicking on it with Mouse-1. Alternatively, selecting an assertion and then pressing the Enter key can start the respective assertion check. When an assertion check is in progress, the assertion will be marked by the clock symbol (⌚). If the assertion check is completed without interrupting it, a new status is assigned to the assertion: tick symbol (✔) indicating that the assertion was completed successfully or cross symbol (✘) indicating that a counterexample was found to the stated property. In case that the status is cross the counterexample can be explored by (second) double-click with Mouse-1 on the assertion or by selecting the assertion and then pressing the Enter key. If the respective assertion is negated, i.e. there is `not` in front of the assertion property, and marked with a cross, then no counterexample can be explored as the proper statement holds.

	The list box is equipped with a contextual menu (or a pop-up menu), which appears when you right-click on an assertion in the list. Depending on the type and the status of the assertion the contextual menu provides options for checking, debugging, modifying the respective assertion, as well as various other options. Take, for example, the selected assertion on which the contextual menu is popped up in the picture below.		The list box is equipped with a contextual menu (or a pop-up menu), which appears when you right-click on an assertion in the list. Depending on the type and the status of the assertion the contextual menu provides options for checking, debugging, modifying the respective assertion, as well as various other options. Take, for example, the selected assertion on which the contextual menu is popped up in the picture below.

Ivaylo Dobrikov: /* CSP Assertions Viewer */

2015-09-07T08:26:32Z

CSP Assertions Viewer

← Older revision		Revision as of 08:26, 7 September 2015
Line 118:		Line 118:
	** ''Check All Assertions'': Selecting this command causes ProB to check of all assertions in the list box that are not checked yet.		** ''Check All Assertions'': Selecting this command causes ProB to check of all assertions in the list box that are not checked yet.
	* '''External Tools'''		* '''External Tools'''
	** ''Open Specification with FDR'': Open the currently loaded CSP-M specification in FDR2. The FDR2 tool is launched with the currently loaded specification in case the FDR2 is installed and the correct path to the `fdr2` command is set for the respective preference `Path to the FDR2 tool`. The value of the `Path to the FDR2 tool` preference can be changed from the “CSP Preferences…” window which can be opened by selecting the `CSP Preferences…` command in `Preferences` menu.		** ''Open Specification with FDR'': Open the currently loaded CSP-M specification in FDR2. The FDR2 tool is launched with the currently loaded specification in case the FDR2 is installed and the correct path to the `fdr2` command is set for the respective preference `Path to the FDR2 tool`. The value of the `Path to the FDR2 tool` preference can be changed from the “CSP Preferences…” window which can be opened by selecting the `CSP Preferences…` command in `Preferences` menu of the main window.
	** ''Evaluate with CSPM-Interpreter'': Selecting this command opens a console in which one can evaluate CSP-M expressions using the CSP-M interpreter. The CSP-M interpreter is an external tool implemented independently from ProB. CSP-M expression can be evaluated if the `cspm` tool is installed and the path to the cspm-command is set for the respective preference `Path to CSPM tool`. The command is obsolete and its removal is considered in future.		** ''Evaluate with CSPM-Interpreter'': Selecting this command opens a console in which one can evaluate CSP-M expressions using the CSP-M interpreter. The CSP-M interpreter is an external tool implemented independently from ProB. CSP-M expression can be evaluated if the `cspm` tool is installed and the path to the cspm-command is set for the respective preference `Path to CSPM tool`. The command is obsolete and its removal is considered in future.

Line 128:		Line 128:
	* ✘ - Assertion check completed, but a counterexample was found to the stated property. The debugger can be used to explore the reason why the property does not hold.		* ✘ - Assertion check completed, but a counterexample was found to the stated property. The debugger can be used to explore the reason why the property does not hold.
	* ⌚ - Assertion is currently checked.		* ⌚ - Assertion is currently checked.
	* ! – The check of the assertion not completed for some reason. Possible causes for the interruption may be:		* ! - The check of the assertion not completed for some reason. Possible causes for the interruption may be:
	** Syntax error in the property was detected;		** Syntax error in the property was detected;
	** Assertion check failed because of missing implementation;		** Assertion check failed because of missing implementation;

Ivaylo Dobrikov: /* CSP Assertions Viewer */

2015-09-07T08:24:54Z

CSP Assertions Viewer

← Older revision		Revision as of 08:24, 7 September 2015
Line 95:		Line 95:
	[[file:CSPAssertionsViewer.png]]		[[file:CSPAssertionsViewer.png]]

	The ''CSP Assertion Viewer'' of ProB has a similar design to the graphical user interface of FDR2. It consists basically of three main components: menu bar, list box and a tab pane. In the following each of the components and ~~its~~ corresponding functionalities are thoroughly described.		The ''CSP Assertion Viewer'' of ProB has a similar design to the graphical user interface of FDR2. It consists basically of three main components: a menu bar, a list box and a tab pane. In the following each of the components and their corresponding functionalities are thoroughly described.

	'''The Menu Bar'''<br/>		'''The Menu Bar'''<br/>
Line 109:		Line 109:
	** ''Size'': Change the font size of the text in the list box. Default font size is 10.		** ''Size'': Change the font size of the text in the list box. Default font size is 10.
	** ''Background'': Change the background color of the list box. Default background color is Gray90.		** ''Background'': Change the background color of the list box. Default background color is Gray90.
	* '''Assertions'''		* '''Assertions'''<br/>The menu provides a list of commands for checking different types of assertions. In case a particular type of assertions is checked the respective command checks only these assertions that are not checked yet.
	** ''Uncheck All Assertions'': Set the status of all assertions in the list box to non-checked.		** ''Uncheck All Assertions'': Set the status of all assertions in the list box to non-checked (`?`).
	** ''Delete All Assertions'': Delete all assertions in the list box.		** ''Delete All Assertions'': Delete all assertions in the list box.
	** ''Check All Refinement…'': The item is a cascading menu and provides commands to check all assertions of one of the following supported refinement types: Traces, Failures, Failures-Divergence, Refusals, and Refusals-Divergence.		** ''Check All Refinement…'': The item is a cascading menu and provides commands to check all assertions of one of the following supported refinement types: Traces, Failures, Failures-Divergence, Refusals, and Refusals-Divergence.

Ivaylo Dobrikov: /* Supported CSP Assertions in ProB */

2015-09-07T07:45:28Z

Supported CSP Assertions in ProB

← Older revision		Revision as of 07:45, 7 September 2015
Line 10:		Line 10:
	<tt>assert P [m= Q</tt>		<tt>assert P [m= Q</tt>

	where m indicates one of the following types of comparison: ‘T’ for traces, ‘F’ for failures, ‘FD’ for failures-divergence, ‘R’ for refusals, and ‘RD’ for ‘refusals-divergence’. Note that the refinement types ‘V’ (revivals) and ‘VD’ (revivals-divergence) that are part of the refinement assertions supported by FDR2 are yet not supported by ProB.		where ‘m’ indicates one of the following types of comparison: ‘T’ for traces, ‘F’ for failures, ‘FD’ for failures-divergence, ‘R’ for refusals, and ‘RD’ for ‘refusals-divergence’. Note that the refinement types ‘V’ (revivals) and ‘VD’ (revivals-divergence) that are part of the refinement assertions supported by FDR2 are yet not supported by ProB.

	'''Deadlock'''<br/>		'''Deadlock'''<br/>
Line 17:		Line 17:
	<tt>assert P :[deadlock free [m]]</tt>		<tt>assert P :[deadlock free [m]]</tt>

	where ''P'' is a process expression and m indicates one of the following models: ‘F’ (failures) and ‘FD’ (failures-divergence).		where ''P'' is a process expression and ‘m’ indicates one of the following models: ‘F’ (failures) and ‘FD’ (failures-divergence).

	'''Determinism'''<br/>		'''Determinism'''<br/>
Line 24:		Line 24:
	<tt>assert P :[deterministic [m]]</tt>		<tt>assert P :[deterministic [m]]</tt>

	where ''P'' is a process expression and m one of the following models: ‘F’ (failures) and ‘FD’ (failures-divergence).		where ''P'' is a process expression and ‘m’ one of the following models: ‘F’ (failures) and ‘FD’ (failures-divergence).

	'''Livelock'''<br/>		'''Livelock'''<br/>
Line 34:		Line 34:

	'''Temporal Properties'''<br/>		'''Temporal Properties'''<br/>
	In ProB it is also possible to make assertions about temporal properties of CSP processes both in LTL and CTL. Basically, one wants to check whether some process ''P'' satisfies a formula ''f'' expressed in temporal logic (denoted by <tt>P \|= f</tt>).		In ProB it is also possible to make assertions about temporal properties of CSP processes both in LTL and CTL. Basically, one wants to check whether some process ''P'' satisfies a formula ''f'' expressed in a temporal logic (denoted by <tt>P \|= f</tt>).

	To check whether a process ''P'' satisfies an LTL formula ''f'' write the following declaration:		To check whether a process ''P'' satisfies an LTL formula ''f'' write the following declaration:
Line 47:		Line 47:
	** To check whether an event `evt` is executed use `[evt]`		** To check whether an event `evt` is executed use `[evt]`
	* Logical operators		* Logical operators
	** true and false		** `true` and `false`
	** `not`: negation		** `not`: negation
	** `&`,`or`,and `=>`: conjunction, disjunction and implication		** `&`,`or` and `=>`: conjunction, disjunction and implication
	* Temporal operators:		* Temporal operators:
	** `G f`: globally		** `G f`: globally
Line 77:		Line 77:
	* State formulae, where f, f1 and f2 are path formulae:		* State formulae, where f, f1 and f2 are path formulae:
	** true \| false \| `not` f \| f1 `&` f2 \| f1 `or` f2 \| f1 `=>` f2,		** true \| false \| `not` f \| f1 `&` f2 \| f1 `or` f2 \| f1 `=>` f2,
	** E f : path quantifier \exists, pronounced `for some path`		** E f : path quantifier `<math>\exists</math>`, pronounced `for some path`
	** A f : path quantifier \forall, pronounced `for all paths`		** A f : path quantifier `<math>\forall</math>`, pronounced `for all paths`
	* Path formulae, where g, g1 and g2 are state formulae:		* Path formulae, where g, g1 and g2 are state formulae:
	** `X g`: next		** `X g`: next

← Older revision		Revision as of 13:28, 22 February 2016
Line 191:		Line 191:
	<tt>assert P :[deadlock free [F]]</tt>.		<tt>assert P :[deadlock free [F]]</tt>.

	The check of the assertion will finish by marking the assertion in the list box with a cross symbol (✘). The cross symbol indicates that a counterexample was found for the assertion ~~checks~~. The counterexample is basically given by the trace <math>\langle a,b,c \rangle</math> as obviously `P` reaches a deadlock state after performing the trace <math>\langle a,b,c \rangle</math>. Providing a second double-click on the assertion will open the following debugging window:		The check of the assertion will finish by marking the assertion in the list box with a cross symbol (✘). The cross symbol indicates that a counterexample was found for the assertion check. The counterexample is basically given by the trace <math>\langle a,b,c \rangle</math> as obviously `P` reaches a deadlock state after performing the trace <math>\langle a,b,c \rangle</math>. Providing a second double-click on the assertion will open the following debugging window:

	[[file: CSP_Deadlock_Trace.png]]		[[file: CSP_Deadlock_Trace.png]]

	Considering the CSP ~~process~~ `Q` and `R` one can see or check that `R` is a trace refinement of `Q` as `R` performs the same set of traces as `Q`. Thus, the assertion check for `Q [T= R` will mark the assertion statement in the list box by a tick symbol (✔). On the other hand, checking the assertion `R [T= Q` will find a counterexample for the refinement check. Performing a second double-click on the item `R [T= Q` will open the following trace debugger window with the counterexample displayed in it:		Considering the CSP processes `Q` and `R` one can see or check that `R` is a trace refinement of `Q` since `R` performs the same set of traces as `Q`. Thus, the assertion check for `Q [T= R` will mark the assertion statement in the list box by a tick symbol (✔). On the other hand, checking the assertion `R [T= Q` will find a counterexample for the refinement check. Performing a second double-click on the item `R [T= Q` will open the following trace debugger window with the counterexample displayed in it:

	[[file: CSP_Trace_Debugger.png]]		[[file: CSP_Trace_Debugger.png]]
Line 201:		Line 201:
	A counterexample of a trace-refinement assertion is a trace leading to a state in which the implementation process performs an event that the specification process cannot perform. In the example above both processes `P` and `Q` perform the trace <math>\langle a \rangle</math> and reach states in which the implementation process can perform an event that is not offered by the specification process ''R''. One can easily deduce from the picture above that `Q` performs after `a` the event `c` which is not offered by `R` as `R` can perform only `b` after `a`. In the left most column `Accept` the debugger window lists all possible events that are offered by the specification process after performing the trace given in the `Trace` column next to `Accepts`.		A counterexample of a trace-refinement assertion is a trace leading to a state in which the implementation process performs an event that the specification process cannot perform. In the example above both processes `P` and `Q` perform the trace <math>\langle a \rangle</math> and reach states in which the implementation process can perform an event that is not offered by the specification process ''R''. One can easily deduce from the picture above that `Q` performs after `a` the event `c` which is not offered by `R` as `R` can perform only `b` after `a`. In the left most column `Accept` the debugger window lists all possible events that are offered by the specification process after performing the trace given in the `Trace` column next to `Accepts`.

	As we already mentioned above `R` is a trace-refinement of `Q`. On the other hand, checking whether `R` is a failures-refinement of `Q` will produce a counterexample as `R` refuses the event `c` that is offered by Q after executing `a`. Accordingly, the counterexample will be illustrated within the following trace debugger window:		As we already mentioned above `R` is a trace-refinement of `Q`. On the other hand, checking whether `R` is a failures-refinement of `Q` will produce a counterexample since `R` refuses the event `c` that is offered by Q after executing `a`. Accordingly, the counterexample will be illustrated within the following trace debugger window:

	[[file: CSP_Failures_Debugger.png]]		[[file: CSP_Failures_Debugger.png]]

	These are basically the three types of debugging windows that will appear when debugging a counterexample for an assertion check in case the respective assertion is not an LTL or a CTL assertion. When a counterexample for an LTL assertion is found it will be explored in the graphical viewer, the same graphical viewer that is used for visualizing the state space ~~of the loaded~~ models in ProB.		These are basically the three types of debugging windows that will appear when debugging a counterexample for an assertion check in case the respective assertion is not an LTL or a CTL assertion. When a counterexample for an LTL assertion is found it will be explored in the graphical viewer, the same graphical viewer that is used for visualizing the state space models in ProB.

	Let us observe again the CSP process `Q` and suppose we want to check whether `Q` satisfies the LTL formula `F [c]`. Then, the respective LTL assertion is declared as follows:		Let us observe again the CSP process `Q` and suppose we want to check whether `Q` satisfies the LTL formula `F [c]`. Then, the respective LTL assertion is declared as follows:
Line 215:		Line 215:
	[[file: CE_LTL_assertion.png]]		[[file: CE_LTL_assertion.png]]

	In the figure above, the nodes and the transitions of the respective counterexample "a -> (b -> a)+" are ~~coloured~~ in red.		In the figure above, the nodes and the transitions of the respective counterexample "a -> (b -> a)+" are colored in red.

	== Checking CSP Assertions with `probcli` ==		== Checking CSP Assertions with `probcli` ==

← Older revision		Revision as of 08:37, 7 September 2015
Line 144:		Line 144:

	The following options affect only the assertion being selected.		The following options affect only the assertion being selected.
	* '''Debug or Show LTL/CTL Counterexample…''': Opens the graphical viewer for exploring the counterexample that was found for the respective LTL assertion check. Option is enabled if the assertion is not negated and its status is cross, or if the assertion is negated and its status is tick. Option appears if the assertion type is an LTL assertion or a CTL assertion.		* '''Debug or Show LTL/CTL Counterexample…''': Opens the graphical viewer for exploring the counterexample that was found for the respective LTL assertion check. Option is enabled if the assertion is not negated and its status is cross (✘), or if the assertion is negated and its status is tick (✔). Option appears if the assertion type is an LTL assertion or a CTL assertion.
	* '''Debug Assertion''': Opens a trace-failure debugger window showing the reason why the corresponding assertion check failed. Option is enabled if the assertion is not negated and its status is cross, or if the assertion is negated and its status is tick. Option available for all types of assertions except for LTL and CTL assertions.		* '''Debug Assertion''': Opens a trace-failure debugger window showing the reason why the corresponding assertion check failed. Option is enabled if the assertion is not negated and its status is cross (✘), or if the assertion is negated and its status is tick (✔). Option available for all types of assertions except for LTL and CTL assertions.
	* '''Check Assertion''': Starts immediately the check of the assertion being selected before right clicking on it.		* '''Check Assertion''': Starts immediately the check of the assertion being selected before right clicking on it.
	* '''Interrupt Assertion Check''': Interrupts the current assertion check.		* '''Interrupt Assertion Check''': Interrupts the current assertion check.
	* '''Uncheck Assertion''': If the assertion was checked and the result of the check is different from question mark, then the status of the assertion will be reset to question mark. Option is enabled only if the assertion result is different from question mark.		* '''Uncheck Assertion''': If the assertion was checked and the result of the check is different from question mark (?), then the status of the assertion will be reset to question mark. Option is enabled only if the assertion result is different from question mark.
	* '''Delete Assertion''': Removes the selected item from the assertion list.		* '''Delete Assertion''': Removes the selected item from the assertion list.
	* '''Negate Assertion''': Negates the respective assertion. ~~In case~~ the result of the (proper) assertion check is cross, then the result of the negated assertion becomes tick. Otherwise, if the result of the (proper) assertion is tick, the negated assertion becomes cross.		* '''Negate Assertion''': Negates the respective assertion. If the result of the (proper) assertion check is cross (✘), then the result of the negated assertion becomes tick (✔). Otherwise, if the result of the (proper) assertion is tick (✔), the negated assertion becomes cross (✘).
	* '''Swap Processes''': Option available only for refinement assertions. Performing the command causes the attachment of a new refinement assertion in which the process expressions on both sides of the refinement operator `[m=` are swapped. If, for example, we execute ‘’Swap Processes’’ on the assertion "<tt>P [T= Q</tt>", the command adds to the list of assertions the assertion "<tt>Q [T= P</tt>".		* '''Swap Processes''': Option available only for refinement assertions. Performing the command causes the attachment of a new refinement assertion in which the process expressions on both sides of the refinement operator `[m=` are swapped. If, for example, we execute ‘’Swap Processes’’ on the assertion "<tt>P [T= Q</tt>", the command adds to the list of assertions the assertion "<tt>Q [T= P</tt>".
	The following options affect all assertions in the list box.		The following options affect all assertions in the list box.
Line 157:		Line 157:
	* '''Delete All Assertions''': All entries in the list box are removed. As a result the message “No assertions were added.” appears in the list box.		* '''Delete All Assertions''': All entries in the list box are removed. As a result the message “No assertions were added.” appears in the list box.
	Other options. The following options have no impact on the assertions in the list box.		Other options. The following options have no impact on the assertions in the list box.
	* '''Summary of the CSP Syntax''': Opens a window in which the summary of the CSP-M syntax and features supported by the ProB tool is ~~detailed~~.		* '''Summary of the CSP Syntax''': Opens a window in which the summary of the CSP-M syntax and features supported by the ProB tool is given.
	* '''Evaluate CSP Expressions''': Opens the Eval console in which CSP expressions can be evaluated.		* '''Evaluate CSP Expressions''': Opens the Eval console in which CSP expressions can be evaluated.
	* '''Open Specification with FDR''': Opens the currently loaded CSP-M specification in FDR2. The FDR2 tool is launched with the currently loaded specification if ~~the~~ FDR2 is installed and the correct path to the `fdr2` command is set for the respective preference `Path to the FDR2 tool`. The value of the `Path to the FDR2 tool` preference can be changed from the “CSP Preferences…” window which can be opened by selecting the `CSP Preferences…` command in `Preferences` menu.		* '''Open Specification with FDR''': Opens the currently loaded CSP-M specification in FDR2. The FDR2 tool is launched with the currently loaded specification if FDR2 is installed and the correct path to the `fdr2` command is set for the respective preference `Path to the FDR2 tool`. The value of the `Path to the FDR2 tool` preference can be changed from the “CSP Preferences…” window which can be opened by selecting the `CSP Preferences…` command in `Preferences` menu of the main window.

	'''The Tab Pane'''<br/>		'''The Tab Pane'''<br/>