3. Algorithms used in Maria

3.1 The Unification Algorithm

Enabled transition instances are sought in a process called unification.

3.1.1 Concepts

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.

input arc

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

output arc

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

variable

A named and strictly typed entity that may be assigned a value

output variable

A variable occurring only on output arcs of a transition; the value will be picked non-deterministically at the end of the unification process

input variable

A variable occurring on the input arcs of a transition

valuation

binding

A binding of values to variables

expression

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

arc expression

A multi-set valued expression occurring on an input or output arc

gate

gate expression

A condition for the valuation of the input variables; if omitted, it is treated as identically true

token

an entity having a value; moved between places by the firing of transitions

concrete token

a token contained in a place

abstract token

an item of an arc expression

lvalue

Left-hand-side value of an assignment; a data object (in our case, an input variable) that is assigned to

rvalue

Right-hand-side value of an assignment, evaluating to the value that will be assigned to the lvalue

3.1.2 Expanding Quantifications

Arc expressions may contain multi-set sums (see section 1.6 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;
};

3.1.3 Matching Concrete and Formal Tokens

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 3.1.4 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'.

3.1.4 Finding Assignment Candidates

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.

3.1.5 Transition Instance Analysis

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.

3.2 Model Checking Algorithms

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 can be specified with `deadlock' and `reject' conditions (see section 1.3.6.1 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.

3.2.2 Checking Liveness Properties

Currently, the `eval' command (see section 2.2.2.7 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.