Warning!<\/strong><\/p>Prerequisite<\/strong> The optimization panel<\/strong> is similar to the experiment panel. Then only new components being<\/p>\n Optimization panel<\/p><\/div>\n This new component allows to define a set of initial states<\/strong> 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).<\/p>\n In order to define this set of initial values we use the optimize<\/strong> keyword when editing our property. The complete syntax of the property language, included optimization variables, is described in the BLTL page<\/a>. We give two examples below.<\/p>\n Important!<\/strong><\/p><\/p>\n To range the variable p1 from 0 to 5 with an increment of 1 we can use the following syntax:<\/p>\n optimize p1:=[0;5;1] end This will generate 6 initial states, one for each value of p1.<\/p>\n <\/div><\/p>\n Important!<\/strong><\/p><\/p>\n We can also vary the parameters of the properties by using the declare<\/strong> 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:<\/p>\n declare K:=[5;10;5] end 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.<\/p>\n <\/div><\/p>\n 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.<\/p>\n
\nFor 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<\/a>.<\/div><\/p>\n\n
![\"\"](\"http:\/\/plasma-lab.gforge.inria.fr\/plasma_lab_images\/plasma_optimisation.png\")
<\/a>
\nF<=#5 “eat”<\/p>\n
\nF<=#(K) “eat”<\/p>\n
![\"\"](\"http:\/\/plasma-lab.gforge.inria.fr\/plasma_lab_images\/plasma_result_optimisation.png\")
<\/a>