1. The Net Description Language

Petri Nets are often represented as directed bipartite graphs using a graphical notation. An entirely graphical notation only works for relatively simple nets that can be represented on one sheet of paper. We decided to use a purely textual notation, since it avoids many problems, such as creating an optimal graphical layout for an automatically generated Petri Net model and creating a graphical user interface that works flawlessly on various hardware and software platforms.

1.1 Design Criteria

As an admirer of the programming languages C and C++, I decided to make the net description language resemble C as closely as possible. Users familiar with C should feel comfortable with the way data types are defined and expressions are written in the net description language.

In the following, we will present the grammar of the net description language using regular expressions (see (flex)Patterns section ‘Patterns’ in The Flex Manual) and the Extended Backus-Naur Form (see (bison)Language and Grammar section ‘Languages and Context-Free Grammars’ in The GNU Bison Manual).

1.2 Lexical Conventions

The lexical conventions of the Maria Petri Net description language determine how to format net descriptions in text files, including the mechanisms for embedding explanatory comments.

1.2.1 Formatting

The net description language is not sensitive to the presence or absence of white space between language elements provided that all keywords and identifiers are distinguished. Thus the user has the same degree of freedom that C and C++ allow in formatting code. White space includes these characters: space (‘' '’), newline (‘'\n'’), carriage return (‘'\r'’), form feed (‘'\f'’), horizontal tabulator (‘'\t'’) and vertical tabulator (‘'\v'’).

1.2.2 Comments

Comments are indicated as they are in the C++ programming language. Two contiguous slashes (‘//’) indicate the start of a comment that continues to the end of the current line. A slash immediately followed by an asterisk (‘/*’) indicates a comment that continues until the reverse sequence (‘*/’) is encountered. Comments may not be nested, and comments are interpreted only between language elements (e.g., not inside names enclosed in double quotes).

1.2.3 Lexical Tokens

Lexical tokens are the atomic constituents of the language, consisting of characters or character sequences.

1.2.3.1 Reserved Words

There are quite a few reserved words in the net description language:

In order to use any of these words as an identifier (see section Identifiers), you will have to enclose it in double quotation marks (‘"’).

1.2.3.2 Numeric Constants

Maria has three interchangeable ways of entering integer numeric constants. The constants can be entered using one of three different notations: with decimal numbers (‘[1-9][0-9]*’), octal numbers (‘0[0-7]*’) or hexadecimal numbers (‘0x[0-9a-fA-F]+’). When a numeric constant is too long to fit in the internal representation, the lexical analyzer will detect it and issue a diagnostic message. Decimal numbers are always unsigned, but the hexadecimal and octal representations are translated directly to the system-dependent internal representation, which usually is a 32-bit word interpreted as a signed integer using two’s complement arithmetic.

1.2.3.3 Character Constants

Character constants are just like in the C programming language: a single character enclosed in apostrophes (‘'’). The backslash (‘\’) is used for entering special characters:

‘\a’

alert, bell (BEL)

‘\b’

backspace (BS)

‘\t’

horizontal tabulator (HT)

‘\n’

newline, line feed (LF)

‘\v’

vertical tabulator (VT)

‘\f’

form feed (FF)

‘\r’

carriage return (CR)

‘\[0-7]{1,3}’

octal notation

‘\x[0-9a-fA-F]{1,2}’

hexadecimal notation

‘\c’

character c (c != '\n')

Any other characters than the apostrophe or the backslash can be entered verbatim between the apostrophes.

Any non-special character quoted with the backslash will be entered as such, i.e. the backslash will be ignored. Thus, ‘'\c'’ is equivalent to ‘'c'’. The line break character is a special case. In order to maintain consistence with the quoted identifiers discussed below, a backslash followed by a line break and any amount of white space containing no line breaks will be ignored.

1.2.3.4 Identifiers

Maria uses textual names for identifying places, transitions, data types, variables, enumeration constants and many other things. None of the identifiers become reserved words. For instance, ‘bool’ may be a type name, a place name or the name of a structure component. Anything of the form ‘[A-Za-z_][A-Za-z0-9_]*’ that is not a reserved word is an identifier.

Identifiers can also be enclosed in double quotation marks. As with single-character constants, only the backslash and the quotation mark must be escaped with a backslash, and the backslash notation (see section Character Constants) can be used for entering non-printable characters. Non-printable characters need not be escaped, though. The only character that is not allowed in identifiers is the NUL character.

The backslash character (‘\’) can be used to break up long identifiers. A backslash followed by a line break and any amount of white space containing no line breaks will be ignored in the input. Also, backslashes can be used to quote the following character. For instance, ‘in\ k’ is equivalent to ‘"in k"’.

In double quotes, the newline character is just as significant as any other character. Sometimes one wants to split a long quoted identifier to several lines without the line breaks being significant. This can be achieved by putting a backslash immediately before the line break. The lexical analyzer will ignore the backslash, the line break and the immediately following white space (not line break).

1.2.4 Preprocessor Directives

The language contains a subset of the directives implemented in the C language preprocessor. Conditional compilation and macro definitions are not supported in the current version.

Preprocessor directives are indicated with a number sign (‘#’) located in the first (leftmost) column. The number sign may be followed by any amount of lexical comments and other white space than newline. The line, which must be terminated with a newline, must contain exactly one preprocessor directive.

1.2.4.1 Embedding Other Files: ‘#include’

The ‘#include’ directive works just like in the C preprocessor, except that the file name must be enclosed in double quotes and never in angle brackets (‘<’ and ‘>’). The string in double quotes is interpreted as a quoted identifier (see section Identifier Type).

1.2.4.2 Conditional Processing

The ‘#ifdef’, ‘#ifndef’, ‘#else’ and ‘#endif’ directives work just like in the C preprocessor, expecting an argument of the form ‘[A-Za-z_][A-Za-z0-9_]*’. Note that there is no ‘#if’ directive and that the ‘#define’ directive only takes one argument, the name of the symbol. The preprocessor symbols are not macros; no macro expansion will take place.

Conditional processing can be used to avoid problems with multiple inclusions of a file or to add some parameterization to the net model. Preprocessor symbols can also be defined on the command line.

1.2.4.3 Setting the Line Number: ‘#line’

Code generation tools usually generate ‘#line’ directives for excerpts that are to be embedded verbatim in the generated code. This allows the compiler to refer to the relevant input file of the code generator in its diagnostic messages.

The Maria languages implement the ‘#line’ directive in order to better support the diagnostics of automatically generated net descriptions. The ‘line’ keyword is followed by a numeric constant and a character string constant indicating the line number and the file name of the following line.

1.2.4.4 Preprocessor Comment: ‘#!’

The special preprocessor directive ‘#!’, which causes the rest of the line to be ignored, was added in order to make it possible for Maria input files to also be executable scripts in systems having an appropriate exec system call.

1.3 Constructs for Defining Nets

1.3.1 Type Definitions: ‘typedef’

In the Maria languages, only the predefined data types ‘bool’, ‘int’, ‘unsigned’ and ‘char’ can be used without naming them using the grammatical construct

type:   TYPEDEF typedefinition name

inspired by C. The built-in type names are not reserved words. For instance, any reference to the type ‘int’ following the definition typedef int (-64..63) int; will refer to an integer representable with 7 bits.

For a comprehensive description of the data type system, see Data Types. Here we will only present the syntax, not the semantics.

Some of the syntax for defining data types resembles the C programming language very closely:

typedefinition:
        ENUM '{' enum_item ( delim enum_item )* '}'
        |
        STRUCT '{' comp_list '}'
        |
        UNION '{' comp_list '}'
        |
        typereference

typereference:
        name
enum_item:
        name [ [ '=' ] number ]
comp_list:
        comp (delim comp)* [ delim ]
comp:
        typedefinition name
number:
        expr
delim:
        ','
        |
        ';'

The extra leaf data types include an empty ‘struct’, often used for denoting black tokens, and an identifier type used for identifying e.g. processes or objects. Note that if you intend to compile the model (see section Options), the empty ‘struct’ does not work on all C compilers.

typedefinition:
        STRUCT '{' '}'
        |
        ID '[' number ']'

It is a good idea to define an alias (see section Function Definitions) for the black token, so that its definition can be changed easily:

typedef struct {} token;
// typedef unsigned (0) token;
token token = <token;

The alert reader may have noticed that we have not introduced arrays yet. Arrays in Maria are not necessarily indexed by integers, but by any type having a limited set of possible values. One can also define a finite-capacity buffer that uses either a queue or a stack discipline.

typedefinition:
        typedefinition '[' typedefinition ']'
        |
        typedefinition '[' QUEUE number ']'
        |
        typedefinition '[' STACK number ']'

Last but not least, it is possible to limit the set of possible values for a type by defining constraints, unions of closed or semi-open ranges of constant values.

typedefinition:
        typedefinition constraint
constraint:
        '(' range (delim range)* ')'
range:
        value
        |
        '..' value
        |
        value '..' value
        |
        value '..'
value:
        expr

1.3.2 Function Definitions

Commonly used expressions can be defined as functions, which can be viewed as macros with strictly typed parameters. Functions are defined in the following way:

function:
        typereference name ('='|'()') formula
        |
        typereference name '(' param_list ')' formula
param_list:
        [ param_list_item (delim param_list_item)* ]
param_list_item:
        typereference name

The function name and the optional parameter list are followed by a formula that usually refers to all the function parameters. When the function is “called” (the macro is expanded), each instance of a named parameter will be substituted with the corresponding expression passed as an argument to the function. Parameterless functions are practical for defining constants.

Functions can be defined both in the global scope and in the transition scope. Functions defined in the declaration block of a transition will only be accessible to that transition, and they will temporarily override a global function definition.

1.3.3 Place Definition: ‘place’

All persistent data in Petri Nets is stored in places that can contain a number of tokens, which in the case of Algebraic System Nets have values. When a place is defined, it is given a unique name, and it is assigned a type.

place:
        PLACE name constraint* typedefinition
        [ CONST ] [ ':' marking_list ]

It is possible to define a capacity constraint, a non-negative integer constraint (see section Constraints) that constrains the total number of tokens the place can contain. Note that the constraint does not need to be of the form ‘(0..n)’ for some positive integer n; it can be e.g. ‘(1)’ if the place always contains exactly one token, or ‘(0,2,4)’. Defining constraints has two major advantages. First, they help to catch errors in the model. Second, analysis algorithms may benefit from them, and resources can be saved when maintaining the reachability graph (see section The Graph Files).

Places can be assigned an initial marking, a multi-set valued expression (see section Operations on Multi-Sets) that evaluates to the collection of tokens that will be assigned to the place in the system’s initial state. To parameterise initial markings, you may use the multi-set summation operator.

Sometimes, it is necessary to introduce control places in the model whose contents remains constant. It would be unnecessary to include such places in the representation of model states, or in the unfolding (see section Unfolding a Model) of the model. The keyword ‘const’ in the place definition indicates a constant place.

When the marking of a place is a function of the marking of other places, the place is called a redundant place. Examples of such places include counters and complement places. It is possible to identify such places by writing initialization expressions that make use of the ‘place name’ operation (see section Operations on Multi-Sets). Doing so not only reduces disk space consumption; Maria will also check that such invariant properties hold in all states it generates.

1.3.4 Transition Definition: ‘trans’

The state of a Petri system is changed by firing transitions, removing tokens from their input places and adding tokens to their output places. A transition is enabled if its each input place contains at least the amount of tokens the transition is about to remove. Only enabled transitions may be fired.

transition:
        TRANS [ ':' ] name [ '!' ] trans*
trans:
        '{' [ var_expr (delim var_expr)* [ delim ] ] '}'
        |
        IN trans_places
        |
        OUT trans_places
        |
        GATE expr (',' expr)*

        |
        HIDE expr

        |
        STRONGLY_FAIR expr
        |
        WEAKLY_FAIR expr
        |
        ENABLED expr

        |
        ':' [ TRANS ] name
        |
        NUMBER

var_expr:
        [ HIDE ] typereference name
        |
        [ HIDE ] typereference name '!' [ '(' expr ')' ]
        |
        function

trans_places:
        '{' place_marking (';' place_marking)* '}'
place_marking:
        [ PLACE ] name ':' marking_list

A transition definition is further divided to four different kinds of declarations. The variable declaration block is used for declaring input and output variables and functions. Using the block is optional, since Maria allows implicit variable declarations. When declaring input variables implicitly, you may have to define the type context (see section Type Casting).

The blocks for defining input and output arcs bind the transition with places. Last but not least, the transition may be assigned gate expressions, which are additional Boolean conditions for enabling the transition. All gate expressions associated with a transition must hold in order for an instance of the transition to be enabled.

The gate expressions ‘undefined’ and ‘fatal’ (see section Dynamic Errors) can be used for defining “assertion” transitions. If a transition having such a gate is enabled, an error is reported. As these transitions cannot be fired, it is not meaningful for them to have output arcs.

In order to ease the transition instance analysis, the parser splits all top-level logical conjunctions ‘&&’ in gate expressions. For this reason, gate expressions that rely on short-circuit evaluation should be declared indivisible with the ‘atom’ keyword.

Transitions may be defined in several parts of the input file. There may be any number of ‘in’, ‘out’ and ‘gate’ blocks and variable or function definitions for a transition, and the transition definition may span over several ‘trans’ blocks.

It is possible to define fairness sets of transition instances to guide the on-the-fly model checker. A transition-specific fairness set definition consists of one of the reserved words ‘strongly_fair’ and ‘weakly_fair’ followed by a Boolean condition. The condition identifies the transition instances that are to be treated fairly. All instances fulfilling the condition will be treated as one unique fairness set.

The ‘enabled’ keyword allows the definition of enabledness sets of transition instances. If no transition instances belonging to an enabledness set are enabled, the set will be reported at the end of the analysis. Use the ‘dump’ command (see section Displaying a Model) to see the enabledness set numbers.

See section Defining Fairness Constraints, for fairness and enabledness sets comprising several transitions.

Maria supports a form of transition fusion, which is a key feature to constructing models in a modular way (See also see section Defining Subnets for Modular State Space Exploration). A transition whose name is preceded with a colon (‘trans :callee’) is not an actual transition but it designates a kind of a macro or a function body that can be substituted to other transitions, like this: ‘trans caller:trans callee’. The Maria parser would merge the definitions of ‘trans :callee’ to the definition of ‘trans caller’.

There is a simple priority method in the search algorithm of Maria that works as follows. When computing the successors of a marking, Maria investigates the transitions in the order they were defined in the model, from top to bottom. Whenever a transition having a nonzero priority class is found to be enabled, no further transitions of other priority classes will be analyzed in the marking.

The default priority class is zero. It is worth noting that non-prioritized transitions that are defined before any prioritized transitions are completely independent of other transitions in the model. Any non-prioritized transitions that are defined after prioritized ones will be analyzed only if no prioritized transitions are enabled.

The priority class can be specified by writing a non-negative integer number after the name of the transition. The exclamation point ‘!’ is an alternative mechanism for providing backward compatibility. It assigns a nonzero priority class to the transition from a global counter and then decrements the counter by one, so that the next transitions marked with ‘!’ will be assigned other priority classes.

The ‘hide’ keyword affects the output of labelled state transition systems (see section Exporting a Labelled State Transition System) and the ‘-Y’ command line option for suppressing hidden states (see section Invoking Maria). A transition instance is hidden (renamed to the special "tau" action) if the hiding condition (a truth-valued expression on the transition variables) holds. Transition variables can be omitted from action names by declaring them with the ‘hide’ keyword.

1.3.5 Defining Subnets for Modular State Space Exploration

When a system being modelled consists of a number of loosely synchronised processes, it is often useful to distinguish between the internal actions of these processes and the actions that model the communication or synchronisation of the processes.

In Maria, it is possible to define tree-like hierarchies of high-level nets. In the outer-level net, all transitions are visible, that is, their occurrences directly corresponds to edges in the global reachability graph (synchronisation graph).

In a subnet, defined within a ‘subnet’ block, normal transitions model internal actions, which do not show up in the synchronisation graph. Synchronisation or communication of subnets is modelled with transition fusion (see section Transition Definition: ‘trans’). When a transition in a subnet calls a transition in its parent net, its occurrences will show in the state space of the parent net.

When the model contains subnets, modular analysis should be applied (command line option ‘-R’ or ‘--modular’; see section Invoking Maria).

subnet:
        SUBNET [ name ] '{' net '}'

1.3.6 On-the-Fly Verification

1.3.6.1 Verifying Safety Properties

The ‘reject’ and ‘deadlock’ statements are used in conjunction with Boolean conditions on markings. When these statements are used, the reachability analyzer reports an error whenever

1. a state violating the ‘reject’ formula has been generated
2. the ‘deadlock’ formula holds in a marking where no transitions are enabled

If the formula cannot be evaluated, the analysis will be stopped. Thus, commanding

deadlock fatal;

will cause the analysis to stop when a deadlock is reached. The following construct can be used to stop the analysis when an undesired state is reached:

reject place fork equals empty && fatal;

An alternative mechanism for specifying undesired states is to define “assertion” transitions with ‘undefined’ or ‘fatal’ in their gate expressions (see section Transition Definition: ‘trans’).

verify:
        REJECT expr
        |
        DEADLOCK expr

1.3.6.2 Defining Fairness Constraints

It is possible to define fairness sets of transition instances to guide the on-the-fly model checker. Such sets may contain instances of a single transition (see section Transition Definition: ‘trans’) or of several transitions. The latter case is handled by identifying the transition instances that are to be included to a set using qualifier expressions, which consist of transition names followed by Boolean conditions for transition variables.

A generic fairness set definition consists of one of the reserved words ‘strongly_fair’ and ‘weakly_fair’ followed by a list of qualifier expressions. Each qualifier expression identifies some transition instances that are to be treated fairly. All instances fulfilling a qualifier expression will be treated as one fairness set.

The ‘enabled’ keyword allows the definition of enabledness sets of transition instances. If no transition instances belonging to an enabledness set are enabled, the set will be reported at the end of the analysis. Use the ‘dump’ command (see section Displaying a Model) to see the enabledness set numbers.

fairness:
        STRONGLY_FAIR qual_expr ( ',' qual_expr )*
        |
        WEAKLY_FAIR qual_expr ( ',' qual_expr )*
        |
        ENABLED qual_expr ( ',' qual_expr )*

qual_expr:
        TRANS name [ ':' expr ]
        |
        '(' qual_expr ')'
        |

        '!' qual_expr
        |
        qual_expr '&&' qual_expr
        |
        qual_expr '^^' qual_expr
        |
        qual_expr '||' qual_expr
        |
        qual_expr '<=>' qual_expr
        |
        qual_expr '=>' qual_expr

Qualifier expressions may also be quantified. The semantics of the multi-set summation operation is that each summand is associated with a new fairness set. Universal and existential quantification have their normal semantics, i.e. they are translated into chains of conjunctions or disjunctions.

qual_expr:
        typereference name [ '(' expr ')' ] ':' qual_expr
        |
        typereference name [ '(' expr ')' ] '&&' qual_expr
        |
        typereference name [ '(' expr ')' ] '||' qual_expr

1.3.6.3 Specifying State Propositions for LSTS Output

The labelled state transition systems that Maria is able to output (see section Exporting a Labelled State Transition System) have a notion of state propositions. As they do not have a natural counterpart in a high-level Petri net, a special construct has to be used for specifying them.

proposition:
        PROP name ':' expr

The ‘prop’ definition does not affect anything else except the output of labelled state transition systems and the resolution of identifiers in the query language. The expression must be a truth-valued state formula.

1.4 Data Types

In programming languages, user-defined structural data types became popular in the 1970s with the success of C and other high-level languages. The original Petri Net formalism did not make use of any data types or algebraic sorts, and its high-level variations usually keep the data types pretty simple, often restricted to tuples of integer numbers or enumerated data types.

In order to efficiently analyze the behavior of parallel programs written in a high-level language, there must exist a straightforward translation from the data types in the source formalism to the types supported by the analyzer. Using tuples of integers, one can emulate simple higher-level types, such as a unidimensional array of a leaf type, but anything beyond that is next to impossible.

The data type system in Maria holds the comparison with any high-level programming language. The only thing that is missing is pointers or references, which would entirely break the locality principle of Petri Nets.

1.4.1 Background

The Maria software stores data in two forms: as trees formed by C++ objects, which are easy to manipulate but use up much space, or as compact bit strings. Converting structured values to a fixed-length bit string and vice versa requires that the number of all possible values of a type is known and that there exists a total order among the values.

For supporting iteration through all values of a type, there are successor and predecessor functions and functions for determining the smallest and the largest value of a type. These are in harmony with the conversion functions: the numeric representation of the smallest value of a type is 0, and its successor is 1 (unless the type only has one value), and so on.

1.4.2 Leaf Types

Data types that do not have any further structure are called leaf types. In Maria, all leaf types can be represented using a machine word, an unsigned integer of usually 32 bits.

1.4.2.1 Integer Types

There are two predefined integer types: ‘int’, a signed integer in the range INT_MIN to INT_MAX, as defined by ‘<limits.h>’ in C, and ‘unsigned’, an unsigned integer in the range 0 to UINT_MAX.

Integer literals are numeric constants, given by the regular expressions ‘[1-9][0-9]*’, ‘0[0-7]*’ and ‘0x[0-9a-fA-F]+’. Negative decimal numbers are formed using the unary ‘-’ operator.

The unconstrained built-in integer types have INT_MAX-INT_MIN+1 or UINT_MAX+1 possible values, both usually 2^32. The order among the values is determined by integer arithmetics. All arithmetic operations in the expression evaluator are performed using the unconstrained integer type. Binary operators require their operands to be either both signed or both unsigned.

1.4.2.2 Boolean Type

The Boolean type ‘bool’ is for storing truth values. It has two literals: ‘false’ (the smallest value) and ‘true’.

1.4.2.3 Character Type

Characters internally use the unsigned char type in C++. Analogously with the unsigned integer type, the smallest value is 0 and the largest UCHAR_MAX, and the total number of different values is UCHAR_MAX+1, usually 2^8.

1.4.2.4 Enumerated Type

There are two variants of the enumerated type. A constrained enumerated type acts just like an integer having some named constants. In the following we will concentrate on the unconstrained variant of the enumerated type.

The domain of an unconstrained enumeration ranges from the smallest enumeration constant to the largest one. The order among the enumeration constants is determined by their integer value. Enumeration constants whose value is not explicitly specified in the type definition get their values just like in the C programming language: it is the successor of the value given to the last declared constant. By default, the first constant will get the value 0.

1.4.2.5 Identifier Type

In SDL, there is a data type for process identifiers. Values of this type can only be compared for equality and inequality, and there is an operator for obtaining a new identifier value. SDL assumes an unlimited pool of distinct identifier values: the operator for obtaining a new value will always return something that is different from all previous values. This is impossible for any practical system. The identifier type in Maria has otherwise the same properties as the one in SDL, but one must declare the size of the identifier pool when declaring an identifier type.

Internally, identifier values are unsigned integers ranging up to the size of the identifier pool, exclusive. The operator for obtaining a new identifier value has not been implemented yet, but quantification (see section Operations on Multi-Sets) is possible. In the future, it is intended to implement symmetry reductions of the state space, making use of the properties of the identifier type.

1.4.3 Composite Types

The leaf data types represented in previous section are adequate for representing any kind of data. Composite data types can be viewed as syntactic sugar: by defining structural types, one can group data items together, which can drastically simplify the notation required for referring to the data items.

Composite types in Maria are constructed in a truly recursive way. There are no arbitrary limits. For example, it is entirely possible to define a buffer of buffers containing a union of an array and a structure.

1.4.3.1 Structure

A structure type describes a sequentially allocated set of member objects, each of which has a distinct name and possibly distinct type. The order of structure values is determined in little-endian way: the most significant component is stored last. For instance, the four values of the type ‘struct{bool a;bool b}’ are ordered ‘{false,false}’, ‘{true,false}’, ‘{false,true}’ and ‘{true,true}’.

A structure type that has n members, each member i having c_i possible values, has

c_1 * c_2 * ... * c_n

possible values. An empty structure has only one possible value, ‘{}’.

1.4.3.2 Union

Often there is a need to pass a parameter whose type is determined dynamically. The tagged union type in Maria serves exactly this purpose. It describes an overlapping nonempty set of member objects, each of which have a name and a possibly distinct type. Whenever a union value is initialized, also the union component must be identified.

The union can be viewed as a special kind of structure of two components: the actual value inside the union and the identifier of the component to which the value belongs. For instance, the values of the type ‘union{bool a;struct{} b;}’ are ordered ‘a=false’, ‘a=true’ and ‘b={}’. A union type that has n members, each member i having c_i possible values, has

c_1 + c_2 + ... + c_n

possible values.

1.4.3.3 Array

An array type describes a contiguously allocated nonempty set of objects with a particular member object, called the element type. The members (elements) of an array are accessed by indexing the array with values of the index type of the array. The number of possible values in the index type determines the number of elements in the array.

The order of values in an array type is determined in the little-endian manner. The four values of the type ‘bool[bool]’ are ordered ‘{false,false}’, ‘{true,false}’, ‘{false,true}’ and ‘{true,true}’.

An array whose element type has c_e possible values and index type c_i possible values, has c_e^c_i possible values.

1.4.3.4 Buffer (Queue or Stack)

Communication protocols use queue-like transmission buffers heavily. Many algorithms and the translation of procedural programming languages to Petri Net models require stack-like buffers. The buffer type in Maria has a maximum size, and it has two variants, queue and stack. A buffer is much like an array, but it may contain a variable number of items.

The order of values is determined in the little-endian manner. Shorter buffers come first. For instance, the values of the type ‘bool[queue 2]’ are ordered ‘{}’, ‘{false}’, ‘{true}’, ‘{false,false}’, ‘{true,false}’, ‘{false,true}’ and ‘{true,true}’.

A buffer of at most n elements whose element type has c_e possible values has

possible values.

1.4.4 Constraints

When performing reachability analysis, it is often desirable to limit the analysis in many ways to address the problem known as the state space explosion. One of the ways is to limit the domain of data types. Instead of considering all 32-bit integer numbers, one may restrict the analysis to numbers ranging from 0 to 10, for instance.

In addition to limiting the search, type constraints can act as a valuable aid for detecting errors in system models. The expression evaluator will detect and report constraint violations whenever a subexpression evaluates to an unconstrained value. The successor and predecessor functions will, however, conveniently wrap around, so that the successor of the largest value of a type is the smallest value.

Constraints can be applied to all types whose values can be expressed with constant literals.(1) Not only leaf types can be constrained. For instance, it is possible (while not necessarily sensible) to define a type ‘bool(false)[queue 347](..{false})[int(33101)]’, a single-element array of a buffer having two possible values: ‘{{}}’ and ‘{{false}}’.

The net description language parser computes unions and intersections of value ranges while parsing constraints, which are internally stored as unions of disjoint ranges. In addition, it will combine adjacent constraints and eliminate overlapping constraints. The type ‘int(1..4,3,5)’ is thus equivalent with the types ‘int(1..)(..5)’ and ‘int(1..5)’, the canonical form.

1.5 Expressions and Formulae

Expressions form the core of any language. One of the design goals of the Maria reachability analyzer was to make expressions as rich as possible, to add expressive power to the language and to make the language attractive to people who are familiar with and accustomed to modern high-level programming languages.

Like the data type system, the expression system of Maria has been greatly inspired by that of the programming language C. There are no pointer operations and no expressions with side-effects, and some operators of our language have no direct counterpart in C.

1.5.1 Literals

When an expression is viewed as a tree, the leaves of the tree are called literals. There are three kinds of literals in Maria expressions: constant values, variable names and the reserved words ‘undefined’ and ‘fatal’. Also invocations of functions with zero arguments, also called nullary functions or named constants, could be viewed as literals, but they can expand to more complex expressions or formulae.

1.5.1.1 Constants

The constants in the Maria languages are type-specific. The Boolean type (types derived from the built-in ‘bool’ type) has two constants: ‘false’ and ‘true’. Character types (‘char’) uses single character constants enclosed in single quotes (see section Lexical Tokens), and integer types (‘int’ and ‘unsigned’) use decimal, octal or hexadecimal numbers with a notation familiar from the programming language C.

There are three unary pseudo-operators that deal with type names and yield constant. The number-of-values operator ‘#’ can be used to refer to the number of possible values a type can receive. For instance, ‘#bool’ is equivalent to ‘2’, unless you have redefined the built-in type ‘bool’ to be something else. The operators ‘<’ and ‘>’ refer to the smallest and to the largest value of a type, respectively. For instance, you can use ‘<bool’ interchangeably with ‘false’, unless the type has been redefined.

The constants of enumerated types are written either using numbers, just as with integer types, or using the names of the enumeration symbols. The names do not have global scope, and in the cases when the parser cannot determine the type from the context, you must use the type casting operator (see section Type Casting). If you want an enumeration symbol to have global scope, you can define it as a nullary function or named constant:

typedef enum { a, b, c } enum_t;
enum_t a = is enum_t a;
reject <enum_t != a;

Constants of compound types are written using the respective expressions for creating compound values, restricting the literals in the expressions to constants. The expressions will be evaluated while parsing them and replaced with corresponding constants. This is called constant folding.

1.5.1.2 Variables

Variables make expressions behave dynamically. In high-level Petri Nets, variables make the arc expressions of transitions evaluate in different ways. Each combination of variable–value pairs (usually referred to as valuation) that enables a transition is called an enabled instance for the transition.(2) Enabled transition instances are sought in a process called unification (see section The Unification Algorithm). Variables cannot be explicitly assigned to in the high-level Petri Net formalism.

Variables can be declared either explicitly e.g. in the declaration blocks of transitions, or implicitly in the input arc expressions of transitions.

1.5.1.3 Dynamic Errors

The ‘undefined’ and ‘fatal’ keywords can be used to catch dynamic errors in the model. Both can be seen as type-less nullary operators. When the ‘undefined’ symbol is evaluated while searching for enabled transition instances, the valuation built so far will be marked as erroneous and the instance will not be fired. The ‘fatal’ keyword is similar, but evaluating it will cause the whole analysis to be aborted.

These two keywords are usually used on the right-hand-side of the if-then-else operator or of the logical ‘&&’, ‘||’ or ‘=>’ operators.(3) To improve readability, one could define an ‘assert()’ macro. Unlike its counterpart in the C library, the following macro will return a value.

bool assert (bool expr) expr || fatal;
place p unsigned: 42;
trans t in { place p: p; }
gate assert (p == 42);

The search for enabled transition instances is an iterative process. Because of this, expressions containing ‘undefined’ and ‘fatal’ keywords may be evaluated before the transition instance is complete. If this is not desirable, the expression for catching dynamic errors should be placed on an output arc, perhaps on the right-hand-side of an if-then-else operator.

If you use either keyword in a gate expression as the right-hand-side of the ‘&&’ operator, you’d better declare the expression atomic by enclosing it with ‘atom()’, so that the parser will not split the gate expression into two, which would break the short-circuit evaluation of the ‘&&’ operator.

1.5.2 Operators

The operator precedence in the Maria languages is as follows. Each table row forms a precedence class.

Some operators have several meanings. For instance, there are two variants of the ‘is’ operator, one that performs type conversions, and another that determines whether a union component is active:

expr:
        IS typereference expr
        |
        expr IS name

1.5.2.1 Integer Arithmetic

For performing integer arithmetic, the language contains all the integer operators of C: negation (sign change, unary ‘-’), bitwise complementation (unary ‘~’), basic arithmetics (‘+’, ‘-’, ‘/’, ‘*’, ‘%’) and bit operations (‘&’, ‘|’, ‘^’, ‘<<’, ‘>>’).

Actually there are two sets of integer operators: signed and unsigned operators. Both operands must be either signed or unsigned, and the result is accordingly signed or unsigned. Unsigned arithmetics is a little faster than signed arithmetics. Numeric constants, unsigned by default, are automatically converted to signed integers. For binary integer operators, the type of the first operand determines whether the operation is signed or unsigned.

All integer operators in Maria have been implemented in terms of the corresponding C++ operators, but some error handling has been added. The operators whose result can exceed the limits of the built-in integer type will detect overflows. These operators are negation, addition, subtraction and multiplication. The division and modulus operators will check for division by zero, and the bit shifting operators will ensure that the amount to be shifted does not exceed the size of the integer type in bits. Last but not least, if the result type has a constraint, the result will be checked against it.

1.5.2.2 Successor and Predecessor

The successor and the predecessor are defined for all ordered types. All other types than the identifier type and structural types containing an identifier component are ordered. The successor of the largest value of a type is the smallest value, whose predecessor in turn is the largest value.(4) No errors can occur while computing the successor (unary ‘+’) or predecessor (unary ‘|’).

1.5.2.3 Comparison

The language contains the usual comparison operators (‘==’, ‘!=’, ‘<’, ‘<=’, ‘>=’ and ‘>’). Equality and inequality comparisons are available for all types, while other comparisons are only available for ordered types. The only error that can occur in a comparison is a constraint violation, in case the result type is constrained.(5)

1.5.2.4 Boolean Logic

Boolean logic in Maria has the familiar operators from C: negation (unary ‘!’), conjunction (‘&&’) and disjunction (‘||’). There is also some syntactic sugar: implication (‘a=>b’ is equivalent to ‘!a||b’), logical equivalence (‘a<=>b’ is equivalent to ‘(a&&b)||!(a||b)’) and logical exclusive or (‘a^^b’, equivalent to ‘!(a<=>b)’).

Also, the language supports universal and existential quantification, and translates them to conjunctions and disjunctions:

formula:
        typereference name [ '(' expr ')' ] '&&' formula
        |
        typereference name [ '(' expr ')' ] '||' formula

For instance, the existential quantification

char a (a>='a' && a<='c') || b==a

expands to the formula ‘b=='a'||b=='b'||b=='c'’.

In the quantified formulae, it is possible to refer to quantified variables, variables indexed by a quantifier or the preceding value of a quantifier:

expr:
        '.' name [ name ]
        |
        ':' name [ name ]

For instance, if there is a declaration ‘typedef unsigned (1..3) index_t’, the universal quantification

index_t e && (e == <index_t || :n < .n)

is equivalent to ‘n[1]<n[2]&&n[2]<n[3]’.

The conjunction and disjunction operators use short-circuit evaluation, meaning that the expression is evaluated in depth-first manner from left to right, and if the value of the left-hand-side expression of an operator alone can determine the value of the expression, no matter what the right-hand-side evaluates to, the right-hand-side will not be evaluated.

1.5.2.5 Selection

The ternary ‘?:’ operator of C selects its second or third argument based on its first argument interpreted as a truth value. The ‘?:’ operator in Maria is more generic. It is not a ternary operator but n-ary, with n-1 being the number of possible values for the type of its first argument.

Here is an example of the ‘?:’ operator for a type having three possible values.

typedef int (1..3) i3_t;
place p i3_t: 1;
trans t
in { place p: p; }
out { place p: p ? p : |p : +p; };

The left-hand-side of the ‘?’ on the output arc of transition ‘t’ is the variable ‘p’, which is of type ‘i3_t’ and has three possible values. When the expression has its largest value (in this case ‘3’), the argument immediately following the ‘?’ will be selected. The second largest value (‘2’) will select the third argument (‘|p’), and the smallest value (‘1’) will select the last argument (‘+p’).

In this simple example, the marking of place ‘p’ will alternate between ‘1’ and ‘2’ in two states. It really should be emphasized that it is the number of values of the type that matters, not the number of possible (reachable) values for the left-hand-side expression. Selecting an initial marking ‘3’ for place ‘p’ would yield only one state in the reachability graph.

1.5.2.6 Type Casting

The type casting operator, the prefix ‘is’, has two purposes. First, it can be used to set the context type in case it cannot be determined correctly. The parser is pretty good at guessing the context type, but there is one remarkable case when it cannot do so. Comparison expressions occur in Boolean context, but the arguments to the comparison operator typically are of some other type. If the argument is an enumeration constant or a construction expression for a compound value, the context must be set with the ‘is’ operator:

typedef enum { a, b, c } e3_t;
place p e3_t: a;
trans t
in { place p: p; }
out { place p: b; }
gate p != is e3_t a;

Boolean, integer and character literals will always be detected as such, no matter what the context type is.

The dynamic behavior of type casting is to convert a value of one type to an equivalent value of another type. Type conversion is only allowed if the two types have at least one common value. The only error that can occur during the conversion is a constraint violation.

Also compound values can be converted. Two compound types are considered compatible for the conversion if all their components are compatible. A union-typed value can be converted to the type of one of its components, or vice versa.

1.5.2.7 Atomicity

The parser may perform optimizations on expressions by converting them to equivalent forms. Currently transition gate expressions containing a conjunction in the top level will be split to several gate expressions, and it is likely that the model checker will do something similar to temporal logic formulae.

The transformations of expressions have one disadvantage: they break short-circuit evaluation. If you rely on short-circuit evaluation when writing an expression, it is a good practice to enclose the expression with ‘atom()’, e.g. ‘atom (y==0||x/y>z)’. Short-circuit evaluation takes place with the operators ‘||’, ‘&&’, ‘=>’ and ‘?:’.

1.5.3 Structures

There are two basic operators for structures: for constructing a value of a structure type and for accessing a structure component. Both inherit their syntax and semantics from C.

expr:
        '{' [ [ name ':' ] expr ( ',' [ name ':' ] expr )* ] '}'
        |
        expr '.' name

In the constructor expression, the expressions for individual components may be preceded by the name of the corresponding struct component.

Since Petri nets have no assignment statement, a special operation is needed for modifying a structure component.

expr:
        expr '.' '{' name expr '}'

For instance, ‘a.{b c}’ has otherwise the same value as the structure ‘a’, but with the component ‘b’ equal to ‘c’.

1.5.4 Unions

The union type in Maria is tagged: it is always known which component of the union has been assigned to (or is the active component), and this information can also be enquired by using the infix ‘is’ operator.

expr:
        name '=' expr
        |
        expr IS name
        |
        expr '.' name

The ‘.’ operator can be used to access the value of the active component. If the specified component is not active, a union violation will occur.

Structures and unions are very practical for modeling inherited classes of object-oriented languages. The example file ‘object.pn’ in the Maria distribution shows how a simple class structure can be translated to Maria types and how objects can be converted between a base class and derived classes.

1.5.5 Arrays

Array values are constructed and indexed with a syntax familiar from the C programming language.

expr:
        '{' [ expr ] ( ',' [ expr ] )* '}'
        |
        expr '[' expr ']'

In addition, the contents of an array can be shifted by a given number of items. The amount to be shifted is always reduced to the modulo of number of items in the array. For instance, shifting an array indexed by Boolean values by an even number of items has no effect.

expr:
        expr '<<' expr
        |
        expr '>>' expr

Since Petri nets have no assignment statement, a special operation is needed for modifying an array item.

expr:
        expr '.' '{' '[' expr ']' expr '}'

For instance, ‘a.{[b] c}’ has otherwise the same value as the array ‘a’, but with the item at ‘b’ equal to ‘c’.

1.5.6 Buffers

For ideal buffers, two operations ought to be enough: removing an item for reading, and writing an item. Since there is no well-defined semantics for Petri Nets whose arc expressions have side-effects, reading a buffer has to be split in two separate operations: peeking at an item (‘*’) and removing (‘-’).

Some applications need to access buffers out of order. It is possible to specify the buffer position using an index.

expr:
        expr index '+' expr
        |
        '-' expr index
        |
        expr index '-' expr
        |
        '*' expr index
index:
        [ '[' expr ']' ]

The unary ‘-’ operator removes one item from a buffer. With the binary ‘-’ operator, it is possible to remove several successive items. The second operand indicates the number of items to be removed.

Many applications need to know the remaining or used buffer capacity. That is what the unary operators ‘%’ and ‘/’ are for. It is also possible to construct the whole buffer contents with one expression, just like struct and array values.

expr:
        '{' [ expr ] ( ',' [ expr ] )* '}'
        |
        '/' expr
        |
        '%' expr

1.6 Operations on Multi-Sets

The state of a Petri Net is identified by the distribution of tokens in the places. The contents of the places, also called markings, can be represented as multi-sets, which are sets that can contain several instances of an item, meaning that the multiplicity of an item in the set may be greater than one.

Arc expressions of transitions and initialization expressions of the model typically make use of two multi-set operations. The simpler one, specifying a multiplicity or a token multiplier, makes use of the binary ‘#’ operator.

marking:
        '(' marking_list ')'
        |
        expr '#' marking

For instance, ‘347#33101’ stands for 347 tokens having the value 33101, and ‘4#(3#2,1)’ is another way for expressing ‘12#2,4#1’, which means 12 tokens of the value 2 and four tokens of the value 1.

The other operation, computing a multi-set sum, is called quantification.

marking:
        typereference name [ '(' expr ')' ] ':' marking

The construct will iterate through all the values of the type, binding each value to a named variable. If the condition expression evaluates to true when the variable is bound to a value, the marking expression will be evaluated using that binding, and the resulting items will be added to the quantification result.

In transition expressions, it is possible to define quantified variables, variables indexed by a quantifier:

expr:
        '.' name [ name ]
        |
        ':' name [ name ]

For instance, writing ‘bool b: .a’ is equivalent to writing ‘"a[false]", "a[true]"’. The optional second name refers to a quantifier variable. It is needed in nested quantifications when indexing a variable by something else than the innermost quantifier.

The variant with the colon indexes variables based on the predecessor of the quantifier variable. It is more useful in universal and existential quantification (see section Boolean Logic).

There are two multi-set valued literals: the empty set, which is useful in subset and equality comparisons, and the marking of a place.

In a formula, the marking of a place is a function of the current state. In the output arc of a transition, it is defined as the multi-set of tokens that will be removed from the place by the input arcs of the transition instance. Referring to the contents of a place in an input arc or in a gate expression yields a dynamic error.

marking:
        EMPTY
        |
        PLACE name

Multi-sets can be compared in two ways. Two sets are equal if both contain the same amount of the same items. Multi-set A is subset of multi-set B if for each item in A there are at least as many such items in B.

formula:
        marking SUBSET marking
        |
        marking EQUALS marking

Multi-sets can be combined in three ways. The union of two multi-sets is computed by adding the multiplicities of all items in each set together. The intersection is formed by computing the maximum multiplicity of each item in both sets. Finally, multi-sets can be subtracted from each other. In A-B there are only items that have a greater multiplicity in A than in B. The multiplicity of each item is the difference of the multiplicities in A and in B.

marking:
        marking UNION marking
        |
        marking INTERSECT marking
        |
        marking MINUS marking

As a special case of intersection, it is possible to filter multi-sets based on conditions. A named variable will iterate through all the items in a multi-set, and if the condition expression is true, the item will be included in the resulting set, with its original multiplicity. This construct can be viewed as an intersection with a multi-set whose items have either zero or infinite multiplicity.

marking:
        SUBSET name '{' marking_list '}' expr

For instance, ‘subset t { 3#true, 2#false } !t’ equals ‘2#false’.

There are two mapping operations similar to the filtering operation described above. One operation preserves the cardinality of a multi-set (the number of contained items). It transforms a multi-set of one type to a multi-set of another type by iterating through all the items in the source multi-set with a named variable, and by computing the items for the target multi-set by evaluating a basic expression.

A more generic mapping iterates through a multi-set, assigning the multiplicity and the value of each distinct item to a pair of variables, and mapping the items by evaluating a multi-set valued expression.

marking:
        MAP name '{' marking_list '}' expr
        |
        MAP name '#' name '{' marking_list '}' marking

For instance, ‘map t { 3#true, 2#false } !t’ equals ‘3#false, 2#true’, while the expression ‘map n#t { 3#true, 2#false } (t?1#!t:n#t)’ evaluates to ‘3#false’.

Last but not least, there are operations for determining the minimum or maximum multiplicity of the items belonging to a multi-set, or for computing the cardinality, the sum of the multiplicities. The minimum multiplicity of an empty set is UINT_MAX.

formula:
        MAX marking
        |
        MIN marking
        |
        CARDINALITY marking

1.7 Temporal Logic

The grammar for temporal logic is LTL, Linear Temporal Logic. The operators “eventually”, “henceforth”, and “in the next state” have the digraph representations ‘<>’, ‘[]’ and ‘()’, respectively.

        '<>' formula
        |
        '[]' formula
        |
        '()' formula
        |
        formula UNTIL formula
        |
        formula RELEASE formula

1.8 Non-Determinism in Transitions

Sometimes it is necessary to have non-deterministic transitions, that is, transitions that have several possible outputs for one input. Often such behavior is modeled by adding a ‘const’ place to the net and binding a token from the place to the non-deterministic transition through a bidirectional arc. This approach may disturb partial order reduction algorithms.

The Maria language contains a construct for declaring non-deterministic transition variables, called output variables. (6)

expr:
        typereference [ name ] '!' [ '(' expr ')' ]

The expression will evaluate to the value of the output variable, which will iterate through all the values of the type, or to all values for which the condition expression is true. The output variable can be given a name, and doing so is recommended if the output variable is used in several expressions or if a condition expression is used.

place p bool: true;
trans t in { place p: p } out { place p: bool! };

The default names for unnamed output variables are ‘:0’, ‘:1’, and so on, a colon followed by a hexadecimal number. Those who want to write obfuscated net descriptions can refer to these names using the double-quoted notation.

1.9 Scoping of Identifiers

Even though Petri Nets are a very flat formalism, there is pretty much depth in the scoping of names. In the Petri Net level, there are three name spaces that cannot be overridden: one for place names, one for transition names and one for data type names. Function names can be overridden in the transition level.

In expressions (see section Literals), names can stand for several things. The names will be looked up in the following order:

1. function parameters (in a function definition),
2. iterator variables (multi-set operations, non-determinism)
3. previously declared transition variables
4. nullary functions
5. enumeration constants (in the type context)
6. state propositions (in ‘deadlock’ and ‘reject’ formulae)

If all the look-ups fail for a name, a transition variable will be declared, if a transition definition is being parsed and if the type context is known.

The parser can issue warning messages about names that exist in several name spaces. If you know what you are doing, these warnings can safely be ignored.

This document was generated by root on November 22, 2009 using texi2html 1.82.