Warning!
PrerequisiteFor this tutorial we assume that you know how to check a property. If you don’t know how to do that please refer to step 3.
The optimization panel is similar to the experiment panel. Then only new components being
- An optimization variables panel
Optimization panel
This new component allows to define a set of initial states by modifying variables initial values. When launching the experiment, each initial states will be checked as a separate experiment (as you can see on the results panel).
In order to define this set of initial values we use the optimize keyword when editing our property. The complete syntax of the property language, included optimization variables, is described in the BLTL page. We give two examples below.
Important!
To range the variable p1 from 0 to 5 with an increment of 1 we can use the following syntax:
optimize p1:=[0;5;1] end
F<=#5 “eat”
This will generate 6 initial states, one for each value of p1.
Important!
We can also vary the parameters of the properties by using the declare keyword. For instance, instead of using a numerical value for the temporal bound of the property, we can declare a variable K that takes the value 5 and 10 using the following syntax:
declare K:=[5;10;5] end
F<=#(K) “eat”
This will generate 2 properties, one for each value of K. The two syntax can also be combined to optimize both the variables of the model and the parameters of the property.
When we check a property with optimization constraints using the experiment or the optimization panel, several results will be displayed for each instances of the variables.
Results of an experimentation with optimization variables
