Tutorial Rodin Parameters: Difference between revisions

(Created page with 'Category:User Manual == Preferences == You can modify the ProB preferences by selecting the ProB pane inside the Rodin preferences. We explain the most important preferenc…')
 
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.

Revision as of 11:20, 28 July 2010


Preferences

You can modify the ProB preferences by selecting the ProB pane inside the Rodin preferences. We explain the most important preferences below.


ProBRodinPrefs.png


Minint and Maxint

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, to know in which range it should be enumerated.

Size of unspecified sets

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.