LTL Model Checking - Revision history

Michael Leuschel: /* Supported Syntax */

2025-09-04T12:15:34Z

Supported Syntax

← Older revision		Revision as of 12:15, 4 September 2025
Line 76:		Line 76:
	*** `changed({BExpr}) ` check if the BExpr is changed by the next transition		*** `changed({BExpr}) ` check if the BExpr is changed by the next transition
	*** `decreasing({BExpr})` check if the BExpr will decrease due to the next transition		*** `decreasing({BExpr})` check if the BExpr will decrease due to the next transition
	***` increasing({BExpr}) ` check if the BExpr will increase due to the next transition		*** `increasing({BExpr})` check if the BExpr will increase due to the next transition
	*** ` BA({BPred}) ` check before-after B predicate BPred on current and next state, where x$0 refers to value in current (before) state, and x to value in next (after) state		*** `BA({BPred})` check before-after B predicate BPred on current and next state, where x$0 refers to value in current (before) state, and x to value in next (after) state
			*** `calls(Op)` check if the next transition calls a (subsidiary) B operation. Note this feature requires the STORE_DETAILED_TRANSITION_INFOS preference to be TRUE. For Op you can use the same syntax as in `[Op]` above.

	* Logical operators		* Logical operators

Michael Leuschel at 12:12, 4 September 2025

2025-09-04T12:12:43Z

@@ Line 170: / Line 170: @@
     ASSERT_LTL1 == "G (e(CruiseBecomesNotAllowed) => e(SetCruiseSpeed))";
     ASSERT_LTL2 == "G (e(CruiseBecomesNotAllowed) => (ObstacleDisappears))"
 '''Storing LTL formulas in CSP-M specifications'''<br/>
@@ Line 185: / Line 188: @@
   assert P |= LTL: "ltl-formula",
   where `P` is an arbitrary process and `ltl-formula` an LTL formula.
 ==LTL Formulae in a Separate File==

Jan Gruteser at 16:10, 13 June 2025

2025-06-13T16:10:21Z

← Older revision		Revision as of 16:10, 13 June 2025
Line 6:		Line 6:
	[[File:ltlviewer.png]]		[[File:ltlviewer.png]]

	All LTL formulas that are given in the "~~DEFINTIONS~~" section of a B machine are displayed in the list box of the LTL/CTL Assertions Viewer. For CSP-M specifications all LTL formulas given in the LTL pragmas of the loaded CSP-M file will be shown in the viewer. (For more detailed information of how LTL/CTL assertions can be stored into B and CSP-M models see Section '''Storing LTL Assertions into a Model''').		All LTL formulas that are given in the "DEFINITIONS" section of a B machine are displayed in the list box of the LTL/CTL Assertions Viewer. For CSP-M specifications all LTL formulas given in the LTL pragmas of the loaded CSP-M file will be shown in the viewer. (For more detailed information of how LTL/CTL assertions can be stored into B and CSP-M models see Section '''Storing LTL Assertions into a Model''').

	A new LTL formula can be entered in the entry below the list box. (We explain the supported syntax below). The typed formula can then be either added to the list box by clicking the "Add" button or directly checked by clicking the "Check" button. Before doing that assure whether you are in the proper frame ("Add LTL Formula") of the bottom part of the LTL viewer.		A new LTL formula can be entered in the entry below the list box. (We explain the supported syntax below). The typed formula can then be either added to the list box by clicking the "Add" button or directly checked by clicking the "Check" button. Before doing that assure whether you are in the proper frame ("Add LTL Formula") of the bottom part of the LTL viewer.

Jan Gruteser: /* Summary of CTL Syntax supported by ProB */

2025-06-13T15:54:43Z

Summary of CTL Syntax supported by ProB

← Older revision		Revision as of 15:54, 13 June 2025
Line 298:		Line 298:

	- atomic propositions:		- atomic propositions:
	{ Pred } to check if a B predicate Pred holds in the current state		{ Pred } to check if a B predicate Pred holds in the current state, e.g. {card(someset) > 1}
	e(op) to check if an operation op is enabled		e(op) to check if an operation op is enabled

Michael Leuschel: /* LTL Preferences */

2023-03-04T14:24:13Z

LTL Preferences

← Older revision		Revision as of 14:24, 4 March 2023
Line 47:		Line 47:
	Download and Install LTL2BA Tool		Download and Install LTL2BA Tool
	from the Help menu.		from the Help menu.
			More details can be found below.

	'''Search Options'''<br/>		'''Search Options'''<br/>

Michael Leuschel: /* Safety Properties */

2023-03-04T14:21:24Z

Safety Properties

← Older revision		Revision as of 14:21, 4 March 2023
Line 106:		Line 106:
	==Safety Properties ==		==Safety Properties ==

	For safety properties ProB uses another checking algorithm, to avoid having to		For safety properties ProB uses another checking algorithm, to avoid having to explore the entire SCC (strongly connected component) of a counter example.
	explore the entire SCC (strongly connected component) of a counter example.		In general this requires installing the LTL2BA tool (see Help menu), but the following patterns are supported directly without LTL2BA:
	In general this requires installing the LTL2BA tool (see Help menu), but
	the following patterns are supported directly without LTL2BA:
	G StateProposition		G StateProposition
	G (StateProposition => X StateProposition)		G (StateProposition => X StateProposition)
	where StateProposition is either an atomic proposition ({Pred}, e(Op), [Op], deadlock,...)		where StateProposition is either an atomic proposition ({Pred}, e(Op), [Op], deadlock,...) or a propositional operators (not, &, =>, or) applied to StatePropositions.
	or a propositional operators (not, &, =>, or) applied to StatePropositions.

	Here are a few example patterns covered by the above:		Here are a few example patterns covered by the above:

Michael Leuschel: /* Safety Properties */

2023-03-04T14:20:57Z

Safety Properties

← Older revision		Revision as of 14:20, 4 March 2023
Line 106:		Line 106:
	==Safety Properties ==		==Safety Properties ==

	For safety properties ProB uses another checking algorithm, to avoid having to		For safety properties ProB uses another checking algorithm, to avoid having to
	explore the entire SCC (strongly connected component) of a counter example.		explore the entire SCC (strongly connected component) of a counter example.
	In general this requires installing the LTL2BA tool (see Help menu), but		In general this requires installing the LTL2BA tool (see Help menu), but
	the following patterns are supported directly without LTL2BA:		the following patterns are supported directly without LTL2BA:
	G StateProposition		G StateProposition
	G (StateProposition => X StateProposition)		G (StateProposition => X StateProposition)
	where StateProposition is either an atomic proposition ({Pred}, e(Op), [Op], deadlock,...)		where StateProposition is either an atomic proposition ({Pred}, e(Op), [Op], deadlock,...)
	or a propositional operators (not, &, =>, or) applied to StatePropositions.		or a propositional operators (not, &, =>, or) applied to StatePropositions.
	Here are a few example patterns covered by the above:
			Here are a few example patterns covered by the above:

	G {Pred} Invariant		G {Pred} Invariant

Michael Leuschel: /* Setting Fairness Constraints */

2023-03-04T14:20:35Z

Setting Fairness Constraints

@@ Line 103: / Line 103: @@
 **  `WEF`: weak fairness for all possible operations
 **  `SEF`: strong fairness for all possible operations
 ==Setting Fairness Constraints==

Michael Leuschel: /* Supported Syntax */

2023-03-04T14:19:14Z

Supported Syntax

← Older revision		Revision as of 14:19, 4 March 2023
Line 69:		Line 69:
	** To check if exactly one operation from a set of operations Op1,Op2,...,Opk is enabled in a state use `controller(Op1,Op2,…,Opk)`.		** To check if exactly one operation from a set of operations Op1,Op2,...,Opk is enabled in a state use `controller(Op1,Op2,…,Opk)`.

	* Transition propositions:~~<br>~~If the next executed operation in the path is `Op`, the expression `[Op]` can be used. Also patter-matching for the arguments of the operation is supported. E.g. `[Op(3,4v)]` checks if the next operation is `Op` and that the first argument is 3 and the third argument is `4v` where `v` is a variable of the machine. <br> Arbitrary B expressions can be used as patterns. Constants and variables of the machine can be used. Variables have the values of the state where the operations starts.		* Transition propositions:
			** If the next executed operation in the path is `Op`, the expression `[Op]` can be used. Also patter-matching for the arguments of the operation is supported. E.g. `[Op(3,4v)]` checks if the next operation is `Op` and that the first argument is 3 and the third argument is `4v` where `v` is a variable of the machine. <br> Arbitrary B expressions can be used as patterns. Constants and variables of the machine can be used. Variables have the values of the state where the operations starts.
			** The following are now also available in ProB 1.12:
			*** `unchanged({BExpr})` check if the B expression BExpr is unchanged compared to the next state
			*** `changed({BExpr}) ` check if the BExpr is changed by the next transition
			*** `decreasing({BExpr})` check if the BExpr will decrease due to the next transition
			***` increasing({BExpr}) ` check if the BExpr will increase due to the next transition
			*** ` BA({BPred}) ` check before-after B predicate BPred on current and next state, where x$0 refers to value in current (before) state, and x to value in next (after) state

	* Logical operators		* Logical operators

Michael Leuschel: /* Summary of CTL Syntax supported by ProB */

2021-06-24T15:57:41Z

Summary of CTL Syntax supported by ProB

← Older revision		Revision as of 15:57, 24 June 2021
Line 265:		Line 265:
	A tutorial of a simple case study, where setting fairness constraints to some of the LTL properties is required, can be found [[Mutual Exclusion (Fairness)\|here]		A tutorial of a simple case study, where setting fairness constraints to some of the LTL properties is required, can be found [[Mutual Exclusion (Fairness)\|here]

	=== Summary of CTL Syntax supported by ProB ===		== Summary of CTL Syntax supported by ProB ==