Tutorial Rodin Parameters - Revision history

Michael Leuschel: /* Size of unspecified sets (carrier sets) */

2019-09-24T12:31:57Z

Size of unspecified sets (carrier sets)

← Older revision		Revision as of 12:31, 24 September 2019
Line 35:		Line 35:
	such as <tt>card(S)=4</tt>, then this value will be used.		such as <tt>card(S)=4</tt>, then this value will be used.
	You can also use <tt>card(S)<n</tt> to specify a maximum cardinality, or <tt>card(S)>n</tt> to specify a minimum cardinality.		You can also use <tt>card(S)<n</tt> to specify a maximum cardinality, or <tt>card(S)>n</tt> to specify a minimum cardinality.
			If no cardinality is specified, ProB will use the default size provided in the preferences dialog (the entry "Size of unspecified deferred sets...").

	=== Using contexts for ProB animation ===		=== Using contexts for ProB animation ===

Michael Leuschel: /* Size of unspecified sets (carrier sets) */

2019-09-23T06:28:13Z

Size of unspecified sets (carrier sets)

← Older revision		Revision as of 06:28, 23 September 2019
Line 53:		Line 53:
	Note that for complicated machines it can be tricky to set up the cardinalities of the carrier sets correctly.		Note that for complicated machines it can be tricky to set up the cardinalities of the carrier sets correctly.
	For example, if you have an axiom <tt>f : A -->> B</tt>, then the cardinality of <tt>A</tt> must be greater or equal to the cardinality of <tt>B</tt>. We are working on an automated analysis for detecting the correct cardinalities of the carrier sets automatically.		For example, if you have an axiom <tt>f : A -->> B</tt>, then the cardinality of <tt>A</tt> must be greater or equal to the cardinality of <tt>B</tt>. We are working on an automated analysis for detecting the correct cardinalities of the carrier sets automatically.

			==== Transforming deferred carrier sets into enumerated sets ====
			Instead of providing a cardinality you can also transform a deferred set into
			an enumerated set, i.e., provided an enumeration of all its elements.
			Here is how you would instantiate S to be a set containing the three elements named a,b,c:

			context c1_prob extends c1
			constants a,b,c
			axioms
			@prob_axm partition(S,{a},{b},{c})
			end

Michael Leuschel: /* Size of unspecified sets (carrier sets) */

2018-02-07T12:05:55Z

Size of unspecified sets (carrier sets)

← Older revision		Revision as of 12:05, 7 February 2018
Line 36:		Line 36:
	You can also use <tt>card(S)<n</tt> to specify a maximum cardinality, or <tt>card(S)>n</tt> to specify a minimum cardinality.		You can also use <tt>card(S)<n</tt> to specify a maximum cardinality, or <tt>card(S)>n</tt> to specify a minimum cardinality.

			=== Using contexts for ProB animation ===
	Note that you can create a new context with those axioms just for animation or model checking with ProB. For this you can simply right-click on the context and use the Rodin command "EXTEND".		Note that you can create a new context with those axioms just for animation or model checking with ProB. For this you can simply right-click on the context and use the Rodin command "EXTEND".
	For example, in Camille syntax such a context could look like:		For example, in Camille syntax such a context could look like:

Michael Leuschel: /* Size of unspecified sets (carrier sets) */

2014-03-26T09:51:32Z

Size of unspecified sets (carrier sets)

← Older revision		Revision as of 09:51, 26 March 2014
Line 44:		Line 44:
	After that you can also refine the model you want to animate by right-clicking on it and using the Rodin command "REFINE", and then add the new context to the seen context list:		After that you can also refine the model you want to animate by right-clicking on it and using the Rodin command "REFINE", and then add the new context to the seen context list:
	machine m0_prob refines m0 sees c0 c1_prob		machine m0_prob refines m0 sees c0 c1_prob

			Here the machine m0_prob and c1_prob play the role of configuration files for the animation.
			You can also add additional axioms in c1_prob to force ProB to use a specific valuation of your constants.

	If ProB cannot infer the size of a carrier set; it will use the default value provided in the "Size of unspecified sets" preference.		If ProB cannot infer the size of a carrier set; it will use the default value provided in the "Size of unspecified sets" preference.

Michael Leuschel at 09:50, 26 March 2014

2014-03-26T09:50:13Z

← Older revision		Revision as of 09:50, 26 March 2014
Line 24:		Line 24:
	variable in order to know in which range it should be enumerated.		variable in order to know in which range it should be enumerated.

	== Size of unspecified sets ==		== Size of unspecified sets (carrier sets) ==

	This is the third entry in the screen shot above.		This is the third entry in the screen shot above.
Line 36:		Line 36:
	You can also use <tt>card(S)<n</tt> to specify a maximum cardinality, or <tt>card(S)>n</tt> to specify a minimum cardinality.		You can also use <tt>card(S)<n</tt> to specify a maximum cardinality, or <tt>card(S)>n</tt> to specify a minimum cardinality.

	Note that you can create a new context with those axioms just for animation or model checking with ProB.		Note that you can create a new context with those axioms just for animation or model checking with ProB. For this you can simply right-click on the context and use the Rodin command "EXTEND".
			For example, in Camille syntax such a context could look like:
			context c1_prob extends c1
			axioms
			@prob_axm card(S) = 3
			end
			After that you can also refine the model you want to animate by right-clicking on it and using the Rodin command "REFINE", and then add the new context to the seen context list:
			machine m0_prob refines m0 sees c0 c1_prob

	If ProB cannot infer the size of a carrier set; it will use the default value provided in the "Size of unspecified sets" preference.		If ProB cannot infer the size of a carrier set; it will use the default value provided in the "Size of unspecified sets" preference.

Joy Clark: grammar and punctuation

2011-04-18T12:47:42Z

grammar and punctuation

← Older revision		Revision as of 12:47, 18 April 2011
Line 22:		Line 22:
	In Rodin, there are only the mathematical integers, and there is no MININT or MAXINT constant.		In Rodin, there are only the mathematical integers, and there is no MININT or MAXINT constant.
	However, this preference will be used by ProB if it cannot determine the value of an integer		However, this preference will be used by ProB if it cannot determine the value of an integer
	variable, to know in which range it should be enumerated.		variable in order to know in which range it should be enumerated.

	== Size of unspecified sets ==		== Size of unspecified sets ==

	This is the third entry in the ~~screenshot~~ above.		This is the third entry in the screen shot above.
	ProB requires all carrier sets to be finite and ProB has to know the cardinality before starting the animation or model checking.		ProB requires all carrier sets to be finite and ProB has to know the cardinality before starting the animation or model checking.

Line 38:		Line 38:
	Note that you can create a new context with those axioms just for animation or model checking with ProB.		Note that you can create a new context with those axioms just for animation or model checking with ProB.

	If ProB cannot infer the size of a carrier set, it will use the default value provided in the "Size of unspecified sets" preference.		If ProB cannot infer the size of a carrier set; it will use the default value provided in the "Size of unspecified sets" preference.

	Note that for complicated machines it can be tricky to set up the cardinalities of the carrier sets correctly.		Note that for complicated machines it can be tricky to set up the cardinalities of the carrier sets correctly.
	For example, if you have an axiom <tt>f : A -->> B</tt>, then the cardinality of <tt>A</tt> must be greater or equal to the cardinality of <tt>B</tt>. We are working on an automated analysis for detecting the correct cardinalities of the carrier sets automatically.		For example, if you have an axiom <tt>f : A -->> B</tt>, then the cardinality of <tt>A</tt> must be greater or equal to the cardinality of <tt>B</tt>. We are working on an automated analysis for detecting the correct cardinalities of the carrier sets automatically.

Michael Leuschel: /* Size of unspecified sets */

2010-07-29T05:31:53Z

Size of unspecified sets

← Older revision		Revision as of 05:31, 29 July 2010
Line 39:		Line 39:

	If ProB cannot infer the size of a carrier set, it will use the default value provided in the "Size of unspecified sets" preference.		If ProB cannot infer the size of a carrier set, it will use the default value provided in the "Size of unspecified sets" preference.

			Note that for complicated machines it can be tricky to set up the cardinalities of the carrier sets correctly.
			For example, if you have an axiom <tt>f : A -->> B</tt>, then the cardinality of <tt>A</tt> must be greater or equal to the cardinality of <tt>B</tt>. We are working on an automated analysis for detecting the correct cardinalities of the carrier sets automatically.

Michael Leuschel: /* Preferences */

2010-07-29T05:20:37Z

Preferences

← Older revision		Revision as of 05:20, 29 July 2010
Line 6:		Line 6:
	You can modify the most important parameters of ProB by going to the Rodin preferences.		You can modify the most important parameters of ProB by going to the Rodin preferences.

	[[file:RodinPrefs.png\|center~~\|\|600px~~]]		[[file:RodinPrefs.png\|center]]

	Now selecting the ProB pane inside the Rodin preferences.		Now selecting the ProB pane inside the Rodin preferences.

Michael Leuschel at 05:20, 29 July 2010

2010-07-29T05:20:04Z

← Older revision		Revision as of 05:20, 29 July 2010
Line 4:		Line 4:
	== Preferences ==		== Preferences ==

	You can modify the ProB preferences by selecting the ProB pane inside the Rodin preferences.		You can modify the most important parameters of ProB by going to the Rodin preferences.
	~~We explain~~ the ~~most important preferences below.~~
			[[file:RodinPrefs.png\|center\|\|600px]]

			Now selecting the ProB pane inside the Rodin preferences.
			You see that a relatively large list of preferences appears (the actual number and denotation depends on the exact version of ProB you have installed):


	[[file:ProBRodinPrefs.png\|center\|\|600px]]		[[file:ProBRodinPrefs.png\|center\|\|600px]]

			We explain the most important preferences below.

	== Minint and Maxint ==		== Minint and Maxint ==

			We first explain the first two entries in the screenshot above.
	Within classical B this provides the range for the implementable integer type.		Within classical B this provides the range for the implementable integer type.
	In Rodin, there are only the mathematical integers, and there is no MININT or MAXINT constant.		In Rodin, there are only the mathematical integers, and there is no MININT or MAXINT constant.
Line 20:		Line 26:
	== Size of unspecified sets ==		== Size of unspecified sets ==

			This is the third entry in the screenshot above.
	ProB requires all carrier sets to be finite and ProB has to know the cardinality before starting the animation or model checking.		ProB requires all carrier sets to be finite and ProB has to know the cardinality before starting the animation or model checking.

Michael Leuschel: /* Size of unspecified sets */

2010-07-28T11:20:25Z

Size of unspecified sets

← Older revision		Revision as of 11:20, 28 July 2010
Line 27:		Line 27:
	If the axioms of a context contain explicit predicates about the cardinality,		If the axioms of a context contain explicit predicates about the cardinality,
	such as <tt>card(S)=4</tt>, then this value will be used.		such as <tt>card(S)=4</tt>, then this value will be used.
	You can also use <tt>card(S)<n</tt> to specify a maximum cardinality, or		You can also use <tt>card(S)<n</tt> to specify a maximum cardinality, or <tt>card(S)>n</tt> to specify a minimum cardinality.
	<tt>card(S)>n</tt> to specify a minimum cardinality.

	Note that you can create a new context with those axioms just for animation or model checking with ProB.		Note that you can create a new context with those axioms just for animation or model checking with ProB.

	If ProB cannot infer the size of a carrier set, it will use the default value provided in the "Size of unspecified sets" preference.		If ProB cannot infer the size of a carrier set, it will use the default value provided in the "Size of unspecified sets" preference.