Tutorial Rodin Parameters: Difference between revisions
m (grammar and punctuation) |
|||
| 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 | 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 | 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 | 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. | ||
Revision as of 12:47, 18 April 2011
Preferences
You can modify the most important parameters of ProB by going to the Rodin preferences.
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):
We explain the most important preferences below.
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. 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 variable in order to know in which range it should be enumerated.
Size of unspecified sets
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.
Some sets are explicitly enumerated, and thus finite. ProB will use this to infer the correct cardinality.
For the other sets, ProB will try to chose a cardinality. If the axioms of a context contain explicit predicates about the cardinality, such as card(S)=4, then this value will be used. You can also use card(S)<n to specify a maximum cardinality, or card(S)>n to specify a minimum cardinality.
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.
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 f : A -->> B, then the cardinality of A must be greater or equal to the cardinality of B. We are working on an automated analysis for detecting the correct cardinalities of the carrier sets automatically.