Algorithm
Using our Biological simulator we constructed a toy example.
Important!
species A=1000,B=1000,C,D,E
A + B -> C
C -> D
D -> E
Download : Chemical.plasma
Requirement
And here is the corresponding property which means “Fatally D will be greater than 400 before 2000 step”.
Important!
F<=#2000 D>400
You can chech this property with Montecarlo method and a samplecount parameter of 10000. This will generate 10000 execution traces and check the property on each one of these traces.
As you can see on this property, the Fatally operator is bounded by a variable. This allows you to set a range of bound values for this operator, thus generating and checking a different property for each value of this range.
You can create multiple property and check them at the same time, set the bound variable to range from 1000 to 3000 with an increment of 100.
- F<=#1000 D>400
- F<=#1100 D>400
- …
- F<=#3000 D>400
After Plasma Lab has completed the experiment, you can generate a plot to see how this bound influence your results.
Results plot in Plasma Lab
