[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
3.1 The Unification Algorithm | Finding enabled transition instances | |
3.2 Model Checking Algorithms | Checking temporal properties |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Enabled transition instances are sought in a process called unification.
3.1.1 Concepts | Concepts related to unification | |
3.1.2 Expanding Quantifications | Expanding multi-set sums | |
3.1.3 Matching Concrete and Formal Tokens | Matching concrete tokens with formal ones | |
3.1.4 Finding Assignment Candidates | Finding assignment candidates | |
3.1.5 Transition Instance Analysis | The core of the unification algorithm |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
There are some concepts related to the unification process that may be somewhat unclear, even though you know the basics of high level Petri Nets.
An arc leading from a place to a transition, labelled with a multi-set expression evaluating to the tokens that are to be removed from the place when the transition fires
An arc leading from a transition to a place, labelled with a multi-set expression evaluating to the tokens that are to be inserted to the place when the transition fires
A named and strictly typed entity that may be assigned a value
A variable occurring only on output arcs of a transition; the value will be picked non-deterministically at the end of the unification process
A variable occurring on the input arcs of a transition
A binding of values to variables
A formula that evaluates to a value; expressions in net descriptions do not contain temporal logic operators or other set operations than multi-set summing
A multi-set valued expression occurring on an input or output arc
A condition for the valuation of the input variables; if omitted, it is treated as identically true
an entity having a value; moved between places by the firing of transitions
a token contained in a place
an item of an arc expression
Left-hand-side value of an assignment; a data object (in our case, an input variable) that is assigned to
Right-hand-side value of an assignment, evaluating to the value that will be assigned to the lvalue
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Arc expressions may contain multi-set sums (see section Operations on Multi-Sets) or universal or existential quantification with fixed or variable bounds. They are expanded at parsing time. Consider the following net description:
place p bool: false, true; place r bool: 2#(2#false, true); trans t in { place p: p; place r: bool s: (s, bool t (p): s && t); }; |
The arc expression is expanded as follows:
trans t in { place p: p; place r: false, true, (p?3:0)#false, (p?1:0)#true; }; |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The Petri Net formalism does not have the concept of assignment as known in programming languages. Also, expressions may not have any side-effects. The only way a Petri system can change its state is through the firing of an enabled transition.
Assignments in the high level Petri Net formalism are implicit. In order for a high-level transition to be enabled, its variables must be bound to suitable values. Values for input variables will be found by matching concrete tokens in places with abstract ones on input arc expressions.
For each abstract token with known multiplicity, all concrete tokens in the input place that have not been associated with other abstract tokens will be considered. If the tokens are compatible (given the valuation generated so far, each component of the abstract token evaluates to the corresponding component of the concrete token or is undefined), a quantity of the concrete token will be associated with the abstract token. For instance, if the place contains ‘3#true,2#false’ and the abstract token is ‘2#x’, the unification algorithm will associate 2 of the 3 ‘true’ tokens or all the ‘false’ tokens with the abstract token.
If the abstract token contains assignment candidates (see section Finding Assignment Candidates), the valuation will be extended. Continuing our example, the variable ‘x’ in the abstract token ‘2#x’ is an lvalue, and it can be assigned the corresponding value of the concrete token, in this case ‘true’ or ‘false’.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Assignment candidates, or left-hand-side values of assignments (lvalues), are expressions that can be assigned to. In Maria, they are variables or array variables indexed by a known index. Lvalues must occur either as such (an abstract token is an lvalue) or in components of structured expressions.
For example, the abstract token ‘42#{x,{y+1,z},+t}’ has two lvalues, the variables ‘x’ and ‘z’. The abstract token ‘x#y’ has one lvalue, ‘y’; the token cannot be matched with a concrete one until the value of ‘x’ is known. The token ‘|x’ does not have any lvalues.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
A preprocessor sorts the input arcs of each transition in such a way that they can be processed in one pass. Static analysis finds out for each input arc the set of variables that are assigned a value based on the token assigned to the arc expression.
Tokens are assigned to input arcs by a depth-first search algorithm. If no variables are unified from an arc, the arc is "constant" under the assignment gathered so far. In this case, the corresponding input place is searched for the token the arc evaluates to. Otherwise, the arc is matched with each token in the input place, one at a time, and the assignment is augmented in such a way that evaluating the arc expression under the augmented (but still incomplete) assignment can yield the token picked from the input place.
In general, the less variables there are in the arc inscriptions and the less tokens in the input places, the faster the instance analysis can be completed.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The on-the-fly model checker in Maria verifies properties expressed in temporal logic by computing a product of a property automaton (which corresponds to a formula) and the reachability graph interpreted as an automaton.
3.2.1 Checking Safety Properties | Safety properties | |
3.2.2 Checking Liveness Properties | Liveness properties |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Safety properties can be specified with ‘deadlock’ and ‘reject’ conditions (see section Verifying Safety Properties), as well as with so-called safe LTL formulae that can be translated to automata on finite words. Also some built-in features of the modelling language, such as capacity constraints, marking-dependent initialization expressions, and checks for expression evaluation errors, can be viewed as safety checking.
While exploring the reachable state space, Maria reports all violations of safety properties and may abort the analysis in case of a fatal violation.
Safety properties can be verified without constructing a reachability graph; it is sufficient to construct the set of reachable states. The command line options ‘-M’, ‘-P’ and ‘-L’ are more efficient than ‘-m’, and the search can be distributed on multiple processors.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Currently, the ‘eval’ command (see section Evaluating Expressions and Formulae) supports LTL formulae on state properties. It is possible to examine counterexamples (paths violating the property being verified), and the algorithm respects both weak and strong fairness conditions.
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by root on December 1, 2016 using texi2html 1.82.