Model checking properties

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:

• 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.
• After the time specification there has to be one of the following expressions:
  1. "**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.
  2. "**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_.
• 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.

  1. True "**tt**"
  2. Simple atomic property (see below)
  3. Negation "**!Φ1**"
  4. Conjunction "**AND(Φ1, Φ2)**"
  5. Disjunction "**OR(Φ1, Φ2)**"
  6. _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".
• 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 ">=".

  1. The fluid level of a continuous place compared to a decimal value: "**fluidlevel('id')~x.x**"
  2. The drift of a continuous place compared to a decimal value: "**drift('id')~x.x**"
  3. Check if the upper boundary of a continuous place is reached: "**uboundary('id')**"
  4. Check if the lower boundary of a continuous place is reached: "**lboundary('id')**"
  5. The number of tokens in a discrete place compared to an integer value: "**tokens('id')~x**"
  6. Enabled status of any kind of transition: "**enabled('id')**"
  7. The clock value of a deterministic transition compared to a decimal value: "**clock('id')~x.x**"
  8. The enabling time of a general transition compared to an decimal value: "**enablingtime('id')~x.x**"
  9. Check if the condition of a guard arc is fulfilled "**condition('id')**"