Rules-DSL - Revision history

Jan Gruteser: /* Computations */

2025-04-30T17:06:52Z

Computations

← Older revision		Revision as of 17:06, 30 April 2025
Line 75:		Line 75:

	====Computations====		====Computations====
	Computations can be used to define variables. As for rules, their activation can depend on further rules, computations or any other predicate specified as an activation condition. Again, the activation condition is evaluated at initialisation and sets the computation status variable to <code>COMPUTATION_DISABLED</code> if the predicate is false. Furthermore, a <code>DUMMY_VALUE</code> can be set, which initialises the variable with the specified value instead of the empty set before execution of the computation. This mechanism implies that each variable defined by a computation must be a set of type <code>POW(S)</code> for any <code>TYPE</code> <code>S</code>. A computation can be replaced by a previously defined computation if it sets the same variable (of the same type) by using <code>REPLACES</code>. The general syntax for computations is:		Computations can be used to define variables. As for rules, their activation can depend on further rules, computations or any other predicate specified as an activation condition. Again, the activation condition is evaluated at initialisation and sets the computation status variable to <code>COMPUTATION_DISABLED</code> if the predicate is false. Furthermore, a <code>DUMMY_VALUE</code> can be set, which initialises the variable with the specified value instead of the empty set before execution of the computation. This mechanism implies that each variable defined by a computation must be a set of type <code>POW(S)</code> for any <code>TYPE</code> <code>S</code> (note: the <tt>TYPE</tt> section is optional since ProB parser version 2.15.1). A computation can be replaced by a previously defined computation if it sets the same variable (of the same type) by using <code>REPLACES</code>. The general syntax for computations is:
	<pre>		<pre>
	COMPUTATION computation_name		COMPUTATION computation_name

Jan Gruteser: /* Rule Validation with probcli */

2025-04-14T13:45:11Z

Rule Validation with probcli

← Older revision		Revision as of 13:45, 14 April 2025
Line 153:		Line 153:
	The provided file extension is used to determine whether the HTML or the XML version of the report is generated.		The provided file extension is used to determine whether the HTML or the XML version of the report is generated.
	To validate all rules, use this option in combination with <code>-execute_all</code>.		To validate all rules, use this option in combination with <code>-execute_all</code>.
	~~Both report~~ options are also available in ProB Tcl/Tk via the visualization menu.		There is also a dot visualisation command "rule_dependency graph" that can be used to create a graph of the dependencies of rules and computations (including results of the current state); example call:
			<pre>probcli myMch.mch -execute_all -rule_report myReport.html -dot "rule_dependency_graph" myGraph.pdf</pre>
			All three export options are also available in ProB Tcl/Tk via the visualization menu.
	Using the special definition <code>RULE_REPORT_CONTEXT</code> you can include context information about the check in the report (of the type <tt>STRING</tt>), e.g. the file name of a validated XML file.		Using the special definition <code>RULE_REPORT_CONTEXT</code> you can include context information about the check in the report (of the type <tt>STRING</tt>), e.g. the file name of a validated XML file.

Jan Gruteser: /* Rule Validation with probcli */

2025-04-14T13:08:12Z

Rule Validation with probcli

← Older revision		Revision as of 13:08, 14 April 2025
Line 150:		Line 150:

	===Rule Validation with probcli===		===Rule Validation with probcli===
	The probcli recognises the option <code>-rule_report <file></code> which generates the same HTML validation report as in ProB2-UI for the current animation state.		The probcli recognises the option <code>-rule_report <file></code> which generates the same HTML/XML validation report as in ProB2-UI for the current animation state.
			The provided file extension is used to determine whether the HTML or the XML version of the report is generated.
	To validate all rules, use this option in combination with <code>-execute_all</code>.		To validate all rules, use this option in combination with <code>-execute_all</code>.
	~~The HTML~~ report ~~option is~~ also available in ProB Tcl/Tk via the visualization menu.		Both report options are also available in ProB Tcl/Tk via the visualization menu.
	Using the special definition <code>RULE_REPORT_CONTEXT</code> you can include context information about the check in the report (of the type <tt>STRING</tt>), e.g. the file name of a validated XML file.		Using the special definition <code>RULE_REPORT_CONTEXT</code> you can include context information about the check in the report (of the type <tt>STRING</tt>), e.g. the file name of a validated XML file.

Jan Gruteser: /* Rule Validation with probcli */

2025-03-31T10:29:44Z

Rule Validation with probcli

← Older revision		Revision as of 10:29, 31 March 2025
Line 153:		Line 153:
	To validate all rules, use this option in combination with <code>-execute_all</code>.		To validate all rules, use this option in combination with <code>-execute_all</code>.
	The HTML report option is also available in ProB Tcl/Tk via the visualization menu.		The HTML report option is also available in ProB Tcl/Tk via the visualization menu.
	Using the special definition <code>RULE_REPORT_CONTEXT</code> you can include context information about the check in the report, e.g. the file name of a validated XML file.		Using the special definition <code>RULE_REPORT_CONTEXT</code> you can include context information about the check in the report (of the type <tt>STRING</tt>), e.g. the file name of a validated XML file.

	===Use Rules for Data Validation===		===Use Rules for Data Validation===

Jan Gruteser: /* Rule Validation with probcli */

2025-03-31T10:29:18Z

Rule Validation with probcli

← Older revision		Revision as of 10:29, 31 March 2025
Line 153:		Line 153:
	To validate all rules, use this option in combination with <code>-execute_all</code>.		To validate all rules, use this option in combination with <code>-execute_all</code>.
	The HTML report option is also available in ProB Tcl/Tk via the visualization menu.		The HTML report option is also available in ProB Tcl/Tk via the visualization menu.
	Using the special definition <code>RULE_REPORT_CONTEXT</code> you can include context information about the check ~~run~~ in the report, e.g. the file name of a validated XML file.		Using the special definition <code>RULE_REPORT_CONTEXT</code> you can include context information about the check in the report, e.g. the file name of a validated XML file.

	===Use Rules for Data Validation===		===Use Rules for Data Validation===

Jan Gruteser: /* Rule Validation with probcli */

2025-03-31T10:29:04Z

Rule Validation with probcli

← Older revision		Revision as of 10:29, 31 March 2025
Line 153:		Line 153:
	To validate all rules, use this option in combination with <code>-execute_all</code>.		To validate all rules, use this option in combination with <code>-execute_all</code>.
	The HTML report option is also available in ProB Tcl/Tk via the visualization menu.		The HTML report option is also available in ProB Tcl/Tk via the visualization menu.
	Using the special definition <tt>RULE_REPORT_CONTEXT</tt> you can include context information about the check run in the report, e.g. the file name of a validated XML file.		Using the special definition <code>RULE_REPORT_CONTEXT</code> you can include context information about the check run in the report, e.g. the file name of a validated XML file.

	===Use Rules for Data Validation===		===Use Rules for Data Validation===

Jan Gruteser: /* Rule Validation with probcli */

2025-03-31T10:28:52Z

Rule Validation with probcli

← Older revision		Revision as of 10:28, 31 March 2025
Line 153:		Line 153:
	To validate all rules, use this option in combination with <code>-execute_all</code>.		To validate all rules, use this option in combination with <code>-execute_all</code>.
	The HTML report option is also available in ProB Tcl/Tk via the visualization menu.		The HTML report option is also available in ProB Tcl/Tk via the visualization menu.
			Using the special definition <tt>RULE_REPORT_CONTEXT</tt> you can include context information about the check run in the report, e.g. the file name of a validated XML file.

	===Use Rules for Data Validation===		===Use Rules for Data Validation===

Jan Gruteser: /* B-Rules DSL */

2025-03-31T07:33:43Z

B-Rules DSL

← Older revision		Revision as of 07:33, 31 March 2025
Line 148:		Line 148:

	[[File:ProB2 UI Rules View.png\|500px\|ProB2-UI Rules View]]		[[File:ProB2 UI Rules View.png\|500px\|ProB2-UI Rules View]]

			===Rule Validation with probcli===
			The probcli recognises the option <code>-rule_report <file></code> which generates the same HTML validation report as in ProB2-UI for the current animation state.
			To validate all rules, use this option in combination with <code>-execute_all</code>.
			The HTML report option is also available in ProB Tcl/Tk via the visualization menu.

	===Use Rules for Data Validation===		===Use Rules for Data Validation===

Jan Gruteser: /* Rules */

2025-03-31T07:30:17Z

Rules

← Older revision		Revision as of 07:30, 31 March 2025
Line 34:		Line 34:
	There are two constructs for rule bodies that can be used arbitrarily often in the body of a rule.		There are two constructs for rule bodies that can be used arbitrarily often in the body of a rule.
	The following is formulated in a positive way, i.e. the execution of the rule leads to <code>SUCCESS</code> if the conditions in the <code>EXPECT</code>-part are fulfilled.		The following is formulated in a positive way, i.e. the execution of the rule leads to <code>SUCCESS</code> if the conditions in the <code>EXPECT</code>-part are fulfilled.
			In contrast to the <code>RULE_FAIL</code> body (see below), in <code>RULE_FORALL</code> you can obtain success messages (such as counter examples) for successful applications of the rule.
	<pre>		<pre>
	RULE_FORALL		RULE_FORALL
Line 43:		Line 44:
	ERROR_TYPE		ERROR_TYPE
	number encoding error type, must be in range of error types		number encoding error type, must be in range of error types
			ON_SUCCESS
			STRING_FORMAT("errorMessage ~w", identifier from list) or
			```${identifier from list}``` (template string)
	COUNTEREXAMPLE		COUNTEREXAMPLE
	STRING_FORMAT("errorMessage ~w", identifier from list)		STRING_FORMAT("errorMessage ~w", identifier from list) or
			```${identifier from list}``` (template string)
	END		END
	</pre>		</pre>

Jan Gruteser: /* Internal Representation */

2024-02-22T14:55:49Z

Internal Representation

← Older revision		Revision as of 14:55, 22 February 2024
Line 183:		Line 183:
	Consider the following example rule:		Consider the following example rule:
	<pre>		<pre>
			RULE rule1 BODY RULE_FAIL WHEN bfalse COUNTEREXAMPLE "" END END;

			COMPUTATION comp1
			BODY
			DEFINE x
			TYPE POW(INTEGER)
			VALUE 1..10
			END
			END;

	RULE rule2		RULE rule2
	DEPENDS_ON_RULE rule1		DEPENDS_ON_RULE rule1
	DEPENDS_ON_COMPUTATION comp1		// DEPENDS_ON_COMPUTATION comp1
	BODY		BODY
	RULE_FORALL i		RULE_FORALL i
Line 196:		Line 206:
	Its internal representation in classical B is the following:		Its internal representation in classical B is the following:
	<pre>		<pre>
	`$RESULT`,`$COUNTEREXAMPLES` <-- rule2 =		`$RESULT`,`$COUNTEREXAMPLES` <-- rule1 =
			SELECT
			rule1 = "NOT_CHECKED"
			THEN
			rule1,`$RESULT`,`$COUNTEREXAMPLES` := "SUCCESS","SUCCESS",{}
			END;

			comp1 =
			SELECT
			comp1 = "NOT_EXECUTED"
			THEN
			x,comp1 := FORCE(1 .. 10),"EXECUTED"
			END;

			`$RESULT`,`$COUNTEREXAMPLES` <-- rule2 =
	SELECT		SELECT
	rule2 = "NOT_CHECKED"		rule2 = "NOT_CHECKED"
	& ~~comp1~~ = "~~EXECUTED~~"		& rule1 = "SUCCESS"
	& ~~rule1~~ = "~~SUCCESS~~"		& comp1 = "EXECUTED"
	THEN		THEN
	VAR `$ResultTuple`,`$ResultStrings` IN		rule2,`$RESULT`,`$COUNTEREXAMPLES` := "SUCCESS","SUCCESS",{} ;
	`$ResultTuple` := FORCE({i\|i : ~~1 .. 10~~ & not(i > 5)});		VAR `$ResultTuple`,`$ResultStrings`
			IN
			`$ResultTuple` := FORCE({i\|i : x & not(i > 5)}) ;
	`$ResultStrings` := FORCE({`$String`\|`$String` : STRING & #i.(i : `$ResultTuple` & `$String` = FORMAT_TO_STRING("~w <= 5",[TO_STRING(i)]))});		`$ResultStrings` := FORCE({`$String`\|`$String` : STRING & #i.(i : `$ResultTuple` & `$String` = FORMAT_TO_STRING("~w <= 5",[TO_STRING(i)]))});
	rule2_Counterexamples := rule2_Counterexamples \/ {1} * `$ResultStrings`;		rule2_Counterexamples := rule2_Counterexamples \/ {1} * `$ResultStrings` ;
	IF `$ResultTuple` /= {} THEN		IF `$ResultTuple` /= {} THEN
	rule2,`$RESULT`,`$COUNTEREXAMPLES` := "FAIL","FAIL",rule2_Counterexamples		rule2,`$RESULT`,`$COUNTEREXAMPLES` := "FAIL","FAIL",rule2_Counterexamples
	~~END~~		END
	~~END;~~
	~~IF rule2 /= "FAIL" THEN~~
	~~rule2,`$RESULT`,`$COUNTEREXAMPLES` := "SUCCESS","SUCCESS",{}~~
	~~ELSE~~
	~~PRINT(rule2_Counterexamples)~~
	END
	END		END
			END
	</pre>		</pre>
			Observe that the implicit dependency of rule2 on comp1 (rule2 uses its variable x) is detected automatically without explicit declaration.

	===Include Rules Machines into other Projects===		===Include Rules Machines into other Projects===
	Currently, it is not possible to include rules machines directly into any other machines. Instead, use the rules machine at the top of the hierarchy (of the rules project) and save the internal generated machine as <code>.mch</code>-file. After changing the machine name accordingly, the rules can be included and used via this machine.		Currently, it is not possible to include rules machines directly into any other machines. Instead, use the rules machine at the top of the hierarchy (of the rules project) and save the internal generated machine as <code>.mch</code>-file. After changing the machine name accordingly, the rules can be included and used via this machine.
	Note that in this case it is not possible to perform Rules-DSL specific methods of the ProB Java API (like detailed information about rule results).		Note that in this case it is not possible to perform Rules-DSL specific methods of the ProB Java API (like detailed information about rule results).