|
|
The model checking functions of _libhpng_ require an input of an SMC property definition by the user. The structure and rules for this input are as follows:
|
|
|
The model checking functions of _libhpng_ require an input of a property definition by the user. The structure and rules for this input are according to the _Stochastic Time Logic_ and defined as follows:
|
|
|
|
|
|
<ul style="list-style-type:disc">
|
|
|
<li>The input has to begin with a point in time for which the property should be checked. This time specification has to be of the form "**x.x:**" (for example "3.0:" ). The decimal point has to be included and a colon has to follow.</li>
|
... | ... | @@ -6,7 +6,7 @@ The model checking functions of _libhpng_ require an input of an SMC property de |
|
|
<li>After the time specification there has to be one of the following expressions:<p>
|
|
|
<ol type="1">
|
|
|
<li>"**P=?**" for the calculation of the mean value of all simulations and the corresponding confidence interval. The interval can have a specified width determining the number of runs or the number of runs can be set instead. Furthermore the confidence level has to be specified.</li>
|
|
|
<li>"**P~x.x**" where "~" has to be replaced by "<" or ">=" (for example "P>=0.5" or "P<=0.1"). This expression is used for the sequiential probabilty ratio test.</li></li><p>
|
|
|
<li>"**P~x.x**" where "~" has to be replaced by "<" or ">=" (for example "P>=0.5" or "P<=0.1"). This expression is used for the _Sequential Probability Ratio Test_.</li></li><p>
|
|
|
<li>The expression is followed by a property surrounded by brackets "(" and ")". Brackets can be nested arbitrarily. Allowed types of formulas are as follows, where Φ1 and Φ2 are properties again.
|
|
|
<ol type="1"><p>
|
|
|
<li>True "**tt**"</li>
|
... | ... | @@ -14,7 +14,7 @@ The model checking functions of _libhpng_ require an input of an SMC property de |
|
|
<li>Negation "**!Φ1**"</li>
|
|
|
<li>Conjunction "**AND(Φ1, Φ2)**"</li>
|
|
|
<li>Disjunction "**OR(Φ1, Φ2)**"</li>
|
|
|
<li>_Until_ formula "**U\[t1, t2\](Φ1, Φ2)**" where t1 and t2 are the time bounds that have to be of the form "x.x".</li></li><p>
|
|
|
<li>_Until_ formula "**U\[t1, t2\](Φ1, Φ2)**" where t1 and t2 are the relative time bounds that have to be of the form "x.x".</li></li><p>
|
|
|
<p>
|
|
|
<li>The supported atomic properties are as follows where "id" be the place ID, transition ID or guard arc ID depending on the kind of property and "~" has to be replaced by "<", "<=", "=", ">" or ">=".<ol type="i"><p>
|
|
|
<li>The fluid level of a continuous place compared to a decimal value: "**fluidlevel('id')~x.x**"</li>
|
... | ... | |