{"id":565,"date":"2013-01-10T10:08:56","date_gmt":"2013-01-10T09:08:56","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=565"},"modified":"2015-03-17T17:50:16","modified_gmt":"2015-03-17T16:50:16","slug":"chemical","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/examples\/chemical\/","title":{"rendered":"Chemical"},"content":{"rendered":"

<\/p>\n

Algorithm<\/h3>\n

Using our Biological simulator we constructed a toy example.<\/p>\n

Important!<\/strong><\/p><\/p>\n

species A=1000,B=1000,C,D,E<\/p>\n

A + B -> C
\nC -> D
\nD -> E<\/p>\n

<\/div>\n

Download : Chemical.plasma<\/a><\/strong><\/p>\n

\n

<\/h3>\n

Requirement<\/h3>\n

And here is the corresponding property which means “Fatally D will be greater than 400 before 2000 step”<\/em>.<\/p>\n

Important!<\/strong><\/p><\/p>\n

F<=#2000 D>400<\/p>\n

<\/div>\n

You can chech this property with Montecarlo method<\/strong> and a samplecount parameter of 10000<\/strong>. This will generate 10000 execution traces and check the property on each one of these traces.<\/p>\n

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.<\/p>\n

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<\/strong>.<\/p>\n