[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2. Reachability Analysis with Maria

Determining all interesting behaviors of a concurrent system is done by computing a graph of all system states reachable from the initial state. This process is called reachability analysis. Once a (possibly incomplete) reachability graph has been generated, it can be examined, and one can verify temporal properties from it.

It is also possible to verify temporal properties during the generation of the reachability graph (see section Model Checking Algorithms). This can guide the search and speed up the analysis, but verifying another temporal property from the system will usually require the reachability analysis to be performed again.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.1 Invoking Maria

The usual way to invoke Maria is as follows:

 
maria -b model

Here model is the Petri Net file name, which usually ends in ‘.pn’. The base name for reachability graph files (see section The Graph Files) is generated by removing the directory name part and the file name suffix (the last part of the name starting with a period ‘.’) from the Petri Net file name. Three files will be generated using the base name, with the suffixes ‘.rgd’, ‘.rgs’, ‘.rga’ and ‘.rgh’. Thus, ‘maria -b dining.pn’ yields ‘dining.rgd’, ‘dining.rgs’, ‘dining.rga’ and ‘dining.rgh’, and ‘maria -d test/order.pn’ yields ‘order.rgd’, ‘order.rgs’, ‘order.rga’ and ‘order.rgh’, in the current directory.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.1.1 Interrupting the Reachability Analysis

Maria traps the interrupt signal (SIGINT), which is usually bound to C-c. When it catches the signal, it will stop processing new states. After Maria has finished with the state it is currently processing, analyzing all the enabled transition instances and generating the successor states, it will update the reachability graph directory and stop the analysis.

Analyzing and firing enabled transition instances in a state may take a long time. Be patient or issue a SIGQUIT (normally bound to C-\) or a SIGKILL signal to abort the process immediately, leaving the reachability graph files in an inconsistent state.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.1.2 Options

Maria supports both traditional single-letter options and mnemonic long option names (if compiled with ‘getopt_long’, see section Compiling Maria). Long option names are indicated with ‘--’ instead of ‘-’. Abbreviations for option names are allowed as long as they are unique. When a long option takes an argument, like ‘--include’, connect the option name and the argument with ‘=’ or provide the argument in the immediately following command line argument.

The options are interpreted in the order they are entered on the command line. In other words, the options for interpreting a model should be specified before loading the model. For instance, ‘maria -b dbm.pn -DUNUSED’ does not make much sense, while ‘maria -DUNUSED -b dbm.pn’ does.

Here is a list of options that can be used with Maria, alphabetized by short option. It is followed by a cross key alphabetized by long option.

-a limit
--array-limit=limit

Limit the size of array index types to limit possible values. A limit of 0 disables the checks.

-b model
--breadth-first-search=model

Generate the reachability graph of model using breadth-first search. Equivalent to ‘-m model -e breadth’.

-C directory
--compile=directory

Generate C code in directory for evaluating expressions and for the low-level routines of the transition instance analysis algorithm (see section Transition Instance Analysis). In order for this option to work, the program must have been compiled with support for compiled expressions enabled (see section Compiling Maria). Also, the compilation script ‘progname-cso’ must be found in the search path, where ‘progname’ is the name used to invoke the analyzer. It is a good idea to have a look at the compilation script, and to adjust the variable definition INCLUDES, so that the required header files can always be found.

You may also want to adjust the variables DEFINES, CC, CFLAGS, LD and LDFLAGS either in the script or in the environment of the reachability analyzer. For instance, if you are using Bourne shell or one of its descendants, prefixing the command line for invoking Maria with ‘DEFINES="" CFLAGS=""’ disables all compiler optimizations for the model being analyzed. This may be useful if the optimization algorithms of the C compiler would consume too many resources.

Applying this option should not affect the behaviour of the model (i.e. it is a bug if it does). When this option is used, evaluation errors are reported in a slightly different way. The interpreter displays the valuation and expression that caused the first error in a state; the compiled code displays the number of errors. For performance reasons, the generated code does not check for overflow errors when adding items to multi-sets.

-c
--no-compile

The opposite of ‘-C’. Evaluate all expressions in the built-in interpreter. This is the default behavior.

-D symbol
--define=symbol

Define the preprocessor symbol symbol. See section Conditional Processing.

-d model
--depth-first-search=model

Generate the reachability graph of model using depth-first search. Equivalent to ‘-m model -e depth’.

-E interval
--edges=interval

When generating the reachability graph, report the size of the graph after every interval generated edges.

-e string
--execute=string

Execute string. See section The Maria Shell.

-g graphfile
--graph=graphfile

Load a previously generated reachability graph from ‘graphfile.rgh’.

-H h[,f[,t]]
--hashes=h[,f[,t]]

Configure the parameters for lossy verification (‘-P’ or ‘-M’). For ‘-P’, allocate t universal hash functions of f elements and corresponding hash tables of h bits each. For ‘-M’, allocate a f bytes for all h elements of the hash table. The value h (and for ‘-P’, also the value f) will be rounded up to suitable values.

-?
-h
--help

Print a summary of the command-line options to Maria and exit.

-I directory
--include=directory

Append directory to the list of directories searched for include files.

-i columns
--width=columns

Set the right margin of the output to columns. The default is 80.

-j processes
--jobs=processes

When checking safety properties (options ‘-L’, ‘-M’ and ‘-P’), use this many worker processes to speed up the analysis on a multiprocessor computer. See also ‘-k’ and ‘-Z’. Note that on Digital UNIX, this option may not work properly if the model is generating successor states too fast (especially when using the ‘-C’ option).

-k port[/host]
--connect=port[/host]

Distribute safety model checking (options ‘-L’, ‘-M’ and ‘-P’) in a TCP/IP network. For the server, only port is specified as a 16-bit unsigned integer, usually between 1024 and 65535. For the worker processes, port/host specifies the port and the address of the server. See also ‘-j’.

All processes should use the same command line options, except that on the server, the ‘-k’ switch takes only the port argument, and the worker processes exit after executing the ‘breadth’ or ‘depth’ command. To gain best performance, start the server and one client on the fastest computer of the network.

Note that when a computer arranges machine words in the big endian byte order, all computers must be big endian and have the same word length. Little endian computers interoperate regardless of their word lengths.

-L model
--lossless=model

Load model and prepare for analysing it by constructing a set of reachable states in disk files. See also ‘-M’, ‘-P’, ‘-j’ and ‘-k’.

-m model
--model=model

Load model and clear its reachability graph. See also ‘-b’ and ‘-d’.

-M model
--md5-compacted=model

Load model and prepare for analysing it by constructing an overapproximation of the set of reachable states in the main memory by using a technique called hash compaction. See also ‘-P’, ‘-L’, ‘-j’ and ‘-k’.

-N cregexp
--name=cregexp

Specify the names allowed in context c as the extended regular expression regexp; See (grep)Regular Expressions section ‘Regular Expressions’ in GNU GREP Manual. In order for this option to work, the program must have been compiled with the POSIX regular expression library enabled (see section Compiling Maria). The context is identified by the first character of the parameter string; the succeeding characters constitute the regular expression that allowed names must match:

P

place name

T

transition name

t

type name

e

name of enumeration constant

c

name of struct or union component

f

function name

p

function parameter name

v

transition variable name

i

iterator variable name

-n cregexp
--no-name=cregexp

Specify the names not allowed in context c as the extended regular expression regexp.

If both ‘-N’ and and ‘-n’ are specified for a context c, then the allowing match takes precedence. For instance, to require that all user defined type names be terminated with ‘_t’, specify ‘-nt -Nt'_t$'’. The quotes in the latter parameter are required to remove the special meaning from ‘$’ in the command line shell you are probably using to invoke Maria.

-P model
--probabilistic=model

Load model and prepare for analysing it by constructing an overapproximation of the set of reachable states in the main memory by using a technique called bitstate hashing. See also ‘-M’, ‘-L’, ‘-j’ and ‘-k’.

-p command
--property-translator=command

Specify the command to use for translating property automata. The command should read a formula from the standard input and write a corresponding automaton description to the standard output. The translator ‘lbt’ (available separately) is compatible with this option.

-q limit
--quantification-limit=limit

Prevent quantification (multi-set sum) of types having more than limit possible values. A limit of 0 disables the checks.

-R
--modular

Explore the state space in a modular way. See section Defining Subnets for Modular State Space Exploration.

-r
--no-modular

Consider only one state space. This is the default.

-t limit
--tolerance=limit

Abort the analysis when limit non-fatal errors have been reported. A limit of 0, the default, allows an infinite number of errors to occur.

-U symbol
--undefine=symbol

Undefine the preprocessor symbol symbol. See section Conditional Processing.

-u [M][f[outfile]]
--unfold=[M][f[outfile]]

Unfold the net (optionally reducing it by constructing a coverable marking (‘M’)) and write it in format f to outfile. If outfile is not specified, dump the unfolded net to the standard output. Possible formats are ‘m’ (Maria (human-readable), default), ‘l’ (LoLA), ‘p’ (PEP), and ‘r’ (PROD).

When the PROD output is chosen, outfile must be specified and end in ‘.net’. Since PROD has no low-level input format, the transitions in the low-level net are grouped to equivalence classes based on the input and output arc weights. Each equivalence class is folded to a high-level transition. The translation makes use of tables that are written to a separate file. If outfile is ‘out.net’, the tables are written to ‘out.src/tables.c’.

-V
--version

Print the version number of Maria and exit.

-v
--verbose

Display verbose information on different stages of the analysis.

-W
--warnings

Enable warnings about suspicious net constructs. This is the default behavior.

-w
--no-warnings

The opposite of ‘-W’. Disable all warnings.

-x numberbase
--radix=numberbase

Specify the number base for diagnostic output. Allowed values for numberbase are ‘oct’, ‘octal’, ‘8’, ‘hex’, ‘hexadecimal’, ‘16’, ‘dec’, ‘decimal’ and ‘10’. The default is to use decimal numbers.

-Y
--compress-hidden

Reduce the set of reachable states by not storing the successor states of transitions instances for which a ‘hide’ condition holds. The hidden successors are stored to a separate state set. This option may save memory (‘-L’ or ‘-m’) or reduce the probability that states are omitted (‘-M’ or ‘-P’), and it may improve the efficiency of parallel analysis (‘-j’ or ‘-k’), but it may also considerably increase the processor time requirement. The option also works with liveness model checking, but there is no guarantee that the truth values of liveness properties remain unchanged. This option can be combined with ‘-Z’.

-y
--no-compress-hidden

The opposite of ‘-Y’. This is the default behavior.

-Z
--compress-paths

Reduce the set of reachable states by not storing intermediate states that have at most one successor. This option may save memory (‘-L’ or ‘-m’) or reduce the probability that states are omitted (‘-M’ or ‘-P’), and it may improve the efficiency of parallel analysis (‘-j’ or ‘-k’), but it may also considerably increase the processor time requirement. The option also works with liveness model checking, but there is no guarantee that the truth values of liveness properties remain unchanged. This option can be combined with ‘-Y’.

-z
--no-compress-paths

The opposite of ‘-Z’. This is the default behavior.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.1.3 Option Cross Key

Here is a list of options, alphabetized by long option, to help you find the corresponding short option.

 
--array-limit=limit                     -a limit
--breadth-first-search=model            -b model
--compile=directory                     -C directory
--compress-hidden                       -Y
--compress-paths                        -Z
--connect=port[/host]                   -k port[/host]
--define=symbol                         -D symbol
--depth-first-search=model              -d model
--edges=interval                        -E interval
--execute=string                        -e string
--graph=graphfile                       -g graphfile
--hashes=h[,f[,t]]                      -H h[,f[,t]]
--help                                  -h
--include=directory                     -I directory
--jobs=processes                        -j processes
--lossless=model                        -L model
--md5-compacted=model                   -M model
--model=model                           -m model
--modular                               -R
--name=cregexp                          -N cregexp
--no-compile                            -c
--no-compress-hidden                    -y
--no-compress-paths                     -z
--no-modular                            -r
--no-name=cregexp                       -n cregexp
--no-warnings                           -w
--probabilistic=model                   -P model
--property-translator=command           -p command
--quantification-limit=limit            -q limit
--radix=numberbase                      -x numberbase
--tolerance=limit                       -t limit
--undefine=symbol                       -U symbol
--unfold=[M][f[outfile]]                -u [M][f[outfile]]
--verbose                               -v
--version                               -V
--warnings                              -W
--width=columns                         -i columns

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2 The Maria Shell

The Maria shell can be used to interactively examine the reachability graph of a model or to check temporal properties in it.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.1 The Line Editor

The Maria shell has a command-line driven user interface. When support for the GNU Readline library has been enabled at compile time (see section Compiling Maria), using the command line is pretty comfortable. Without Readline, you have to cope with the system’s default line editor, which certainly lacks command line history and completion features.

When invoked, Maria will greet you with the prompt ‘@0$’, where ‘0’ is the number of the current state, or ‘$’ if no model has been loaded. The initial state always has the number zero. Command lines may be split over multiple physical lines. When there is an unbalanced single or double quote or a multi-line (C-style) comment, or when the line ends in a backslash ‘\’, Maria will present the continuation prompt ‘@n>’. In case of a typing mistake, EOF will tell Maria to abort reading continuation lines.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.1.1 Name Completion

This is by no means a complete list of Readline features. See (readline)Command Line Editing section ‘Command Line Editing’ in GNU Readline Library, if you are not familiar with Readline.

One of the nicest features of the Readline library is context-sensitive completion of names. The Maria shell completes names of data types (immediately following the ‘is’ keyword), places (following ‘place’), transitions (‘trans’), and keywords. Let us now assume that you have generated the reachability graph for the dining philosopher example (see section Dining Philosophers (‘dining.pn’)). The following example illustrates how the context-sensitive completion of names works.

 
$graph diningRET
@0$paTAB
@0$path @29 plTAB
@0$path @29 place "fTAB
@0$path @29 place "fork" eqTAB
@0$path @29 place "fork" equals emTAB
@0$path @29 place "fork" equals empty RET
shortest path from condition to @29 (2 nodes):
@74:state (
 state:
  {3,thinking},{1,hungry},{4,hungry},{5,hungry},{2,eating}
)
4 predecessors
1 successor
transition finish->@29
<
 p:2
>
@29:state (
 fork:
  2,3
 state:
  {2,thinking},{3,thinking},{1,hungry},{4,hungry},{5,hungry}
)
4 predecessors
3 successors
@0$exit RET

Unfortunately backslash-quoted names cannot be completed. This is due to a limitation of the Readline library, which will only call the dequoting function if its built-in filename completion function is being used. This is why the keyword completer adds a double quotation mark after keywords that are likely to be followed by a name.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2 The Query Language

Maria uses a script language in which statements are separated by semicolons (‘;’). See section Separating Statements, for other considerations.

There are commands for moving around in the graph and for evaluating formulae in different graph nodes. Maria shell commands are reserved words only in the beginning of a statement: there is no need to quote a place name ‘exit’, for instance.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.1 Loading a Model

 
statement:
        GRAPH name
        |
        MODEL name

The ‘graph’ command loads a previously generated reachability graph. The supplied name must exclude the ‘.rgh’ suffix.

The ‘model’ command loads a Petri net model and initializes its reachability graph. Be careful with this command; it will delete a previously generated reachability graph of the model, if one exists in the current directory.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.2 Displaying a Model

 
statement:
        [ VISUAL ] DUMP

The ‘dump’ command displays the syntax tree of the current model in the modelling language. When the ‘visual’ prefix is present, the Petri net will be displayed graphically (see section Visualizing Graphs and Paths). This command may be useful when trying to find out how Maria expands multi-set summations (see section Operations on Multi-Sets) or quantifications (see section Boolean Logic).


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.3 Unfolding a Model

 
statement:
        UNFOLD [ name ]

The ‘unfold’ command unfolds the currently loaded Petri net model. The argument takes the same format as the command line option ‘-u’ (see section Options).


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.4 Exporting a Labelled State Transition System

 
statement:
        LSTS [ name ]

Maria is able to export the reachability graph or parts thereof as a labelled state transition system. The ‘lsts’ command specifies a file name for an LSTS. When the command is invoked without a file name, any currently open LSTS files are closed and the function cancelled.

The ‘lsts’ command affects exhaustive analysis (see section Exhaustive Analysis), non-visual path queries (see section Shortest Paths) and the representation of counterexample paths of liveness properties (see section Checking Liveness Properties).

In exhaustive analysis, the command should be invoked before any states have been explored, right after the model has been loaded. When using the path commands, the ‘lsts’ command should be issued right before generating the counterexample. These measures are necessary, because for efficiency reasons, the ‘lsts’ command has been implemented so that all generated states and arcs are exported to LSTS files if ones have been opened. The path query commands export results to LSTS if the files are open, and close the files immediately after that. It is impossible to combine several query results into one exported LSTS.

The LSTS output can be controlled by hiding variables or transition instances (see section Transition Definition: ‘trans) and by specifying state propositions (see section Specifying State Propositions for LSTS Output).


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.5 Exporting the Reachability Graph

 
statement:
        [ VISUAL ] DUMPGRAPH

The command ‘dumpgraph’ exports the portion of the reachability graph that has been generated so far. When the ‘visual’ prefix is present, the reachability graph will be displayed graphically (see section Visualizing Graphs and Paths). See section Exhaustive Analysis, for information on generating the reachability graph.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.6 Exhaustive Analysis

 
statement:
        BREADTH [ STATE ]
        |
        DEPTH [ STATE ]

The commands ‘breadth’ and ‘depth’ generate all states that are reachable either from the current state or from a specified state. This exhaustive search will only be performed if the successors of the state have not already been generated.

 
$model "dining.pn"
@0$breadth
"dining.pn": 82 states (3..6 bytes), 265 arcs

At the end of the search, the numbers of generated states and events are reported. The byte range indicates the minimum and maximum lengths of encoded state representations. This number is affected by modelling techniques, such as the use of capacity constraints and invariants (see section Place Definition: ‘place), and by not folding places unnecessarily. For this particular model (see section Dining Philosophers (‘dining.pn’)), the maximum length of encoded states can be reduced from 6 to 4 bytes by splitting the place that holds pairs of philosophers and their states (thinking, hungry, eating) to three places, holding a set of those philosophers that are in the state, and by defining an invariant initialisation expression for the "thinking" place.

The ‘breadth’ and ‘depth’ commands can be also used in purely state-based safety verification (command-line options ‘-L’, ‘-M’ and ‘-P’), without generating a reachability graph. If either command is given a safety LTL formula as an argument, the model contained in the file will be verified against the property. When the command is preceded by a ‘visual’ keyword, any path that violates the formula will be displayed graphically (see section Visualizing Graphs and Paths).

 
statement:
        [ VISUAL ] BREADTH formula
        |
        [ VISUAL ] DEPTH formula

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.7 Evaluating Expressions and Formulae

 
statement:
        [ VISUAL ] [ EVAL ] [ STATE ] formula

Expressions and formulae can be evaluated either in the current state or in a given state.

 
@0$place fork
fork:
 1,2,3,4,5
@0$eval @4 place fork
fork:
 1,2,3,5

When the ‘visual’ keyword is present and a temporal formula is being evaluated, a path violating the formula is displayed graphically (see section Visualizing Graphs and Paths).


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.8 Displaying Markings

With the ‘show’ command it is possible to view the marking of a node in the reachability graph. When a node is not specified, the current node will be shown.

The command can also be used to view the nodes in a strongly connected component (see section Strongly Connected Components). It is possible to specify a Boolean condition to select a subset of the states in the strongly connected component to be displayed.

 
statement:
        [ VISUAL ] SHOW [ STATE ]
        |
        [ VISUAL ] [ SHOW ] COMP [ expr ]
        |
        [ VISUAL ] SHOW STATE STATE ( STATE )*

When the keyword ‘show’ is followed by a sequence of at least two state numbers, Maria displays the sequence of states in the same way as the ‘path’ command does (see section Shortest Paths). This command is most useful with the ‘visual’ prefix, since it can be used for visualizing a previously reported path.

 
@0$show @4
@4:state (
 fork:
  1,2,3,5
 state:
  {1,thinking},{2,thinking},{3,thinking},{5,thinking},{4,hungry}
)
4 predecessors
5 successors

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.9 Excluding Places from Displayed Markings

Petri net models often contain a large number of places whose contents are of less significance when investigating a particular property of the model. The ‘hide’ command controls which places are displayed by the ‘show’ command (see section Displaying Markings) and in the graphical interface (see section Visualizing Graphs and Paths).

 
statement:
        HIDE [ '!' ] [ [ PLACE ] name ( ',' [ PLACE ] name )* ]

When followed by an exclamation point, the command selects places to be shown (instead of to be hidden). An empty list of place names selects all places. Typically, one can issue the command ‘hide’ followed by ‘hide ! placename’ for each place to be shown.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.10 Selecting the Active Subnet

When the model contains subnets (see section Selecting the Active Subnet) and Maria has been told to generate a reachability graph and apply modular analysis (see section Invoking Maria), the ‘subnet’ command can be used for navigating in the state spaces of the modules.

The ‘subnet’ command can be used for navigating in the hierarchy tree in a similar way as the ‘cd’ command navigates in the directory tree. It takes a sequence of subnet identifiers separated by slashes. The string ‘..’ denotes the parent net.

When invoked without parameters, ‘subnet’ selects the root net, which represents the whole system. If the parameter string starts with a slash, the tree is selected relative to the root net. Otherwise, it is selected relative to the currently selected net.

Nets that have been given a name (see section Selecting the Active Subnet) can be referred to by that name. All nets can be referred to by their index number in the parent net. The subnets are numbered starting from zero.

 
statement:
        SUBNET [ [ netid ] ( '/'+ netid )* '/'* ]
netid:  '..' | name | number

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.11 Listing Successor Nodes

The ‘succ’ command lists all successors of a state, or possible events in the state. If no successors have been generated for the state, they will be generated on demand. This makes Maria suitable for simulating or debugging a Petri Net model without generating the complete reachability graph: to create the interesting part of the reachability graph, one can keep listing the successors of the states he is interested in.

The command can also be used to view the successors of a strongly connected component (see section Strongly Connected Components).

 
statement:
        [ VISUAL ] SUCC [ '!' ] [ STATE ]
        |
        [ VISUAL ] SUCC COMP

When the ‘visual’ keyword is present, the successor states or components are displayed graphically (see section Visualizing Graphs and Paths).

When the ‘succ’ keyword is followed by an exclamation point (‘!’), Maria will follow the chain of successor states until a state with several successors is encountered.

 
@0$succ
transition left->@1
<
 p:1
>
transition left->@2
<
 p:2
>
transition left->@3
<
 p:3
>
transition left->@4
<
 p:4
>
transition left->@5
<
 p:5
>

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.12 Listing Predecessor Nodes

The ‘pred’ command lists all the generated predecessors of a state, or all events leading to the state.

The command can also be used to view the predecessors of a strongly connected component (see section Strongly Connected Components).

 
statement:
        [ VISUAL ] PRED [ '!' ] [ STATE ]
        |
        [ VISUAL ] PRED COMP

When the ‘visual’ keyword is present, the predecessor states or components are displayed graphically (see section Visualizing Graphs and Paths).

When the ‘pred’ keyword is followed by an exclamation point (‘!’), Maria will follow the chain of predecessor states until a state with several predecessors is encountered.

 
@0$pred
transition finish<-@20
<
 p:5
>
transition finish<-@18
<
 p:4
>
transition finish<-@15
<
 p:3
>
transition finish<-@11
<
 p:2
>
transition finish<-@6
<
 p:1
>

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.13 Moving in the Graph

Moving from a state to another is as simple as entering the state number. To make scripts more readable, you may also use the ‘go’ keyword.

 
statement:
        [ GO ] STATE
 
@0$@4
@4$go @0
@0$

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.14 Anonymous Transitions

Sometimes, when modelling a complex system, it may be useful to specify a different initial state as a starting point for the analysis. For instance, one might want to slightly modify the marking of an erroneous state to see how the analysis would proceed from there.

In Maria, new states can be computed by entering an anonymous transition that will be evaluated in a specified state, or in the current state if no state is specified. No arcs will be added to the reachability graph. The generated states will be displayed either textually or graphically.

 
statement:
        [ VISUAL ] [ STATE ] TRANS atrans*
atrans:
        '{' [ avar_expr ( delim avar_expr )* [ delim ] ] '}'
        |
        IN trans_places
        |
        OUT trans_places
        |
        GATE expr ( ',' expr )*
avar_expr:
        typereference name
        |
        typereference name '!' [ '(' expr ')' ]
 
@0$trans in { place fork: 1 } out { place fork: 2 }
@82:unprocessed state (
 fork:
  2#2,3,4,5
 state:
  {1,thinking},{2,thinking},{3,thinking},{4,thinking},{5,thinking}
)
@0$

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.15 Defining Functions

All the functions defined in the Petri Net are available in the query tool. It is also possible to define additional functions by using the ‘function’ keyword.

 
statement:
        FUNCTION function
 
@0$function bool assert (bool f) f || fatal
@0$assert (false);
<fatalExpression:
  fatal
>

If there are many function definitions, it is advisable to write them in a Maria command file, e.g. ‘dining’:

 
#!/usr/local/bin/maria
graph dining;
function bool assert (bool f) f || fatal;

The definitions can be loaded in at least three different ways:

 
$maria dining
@0$exit
$./dining #the script must be executable
@0$exit
$maria
$#include "dining"

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.16 Strongly Connected Components

A strongly connected component of a directed graph (e.g. a reachability graph) is a set of nodes that are reachable from each other by following the arcs. If the reachability graph of a model has only one strongly connected component, it is guaranteed to be free of deadlocks, since the initial state is reachable from all states.

A strongly connected component, or a node of a component graph, may be trivial, meaning that it contains only one node of the underlying graph. A terminal component does not have any successors.

Maria computes the strongly connected components by starting from a specified state (by default, the current state) and considering a transitive closure of its generated successors in the reachability graph. It is possible to limit the transitive closure by specifying a condition. States for which the condition does not evaluate to ‘true’ are ignored by the search algorithm.

Once the component graph has been generated, it is possible to list all its non-trivial terminal components, or all components. Also the ‘show’, ‘succ’ and ‘prev’ commands can be used to examine the component graph. The ‘visual’ keyword selects graphical display (see section Visualizing Graphs and Paths).

 
statement:
        STRONG [ STATE ] [ expr ]
        |
        TERMINAL
        |
        [ VISUAL ] COMPONENTS
        |
        [ VISUAL ] [ SHOW ] COMP [ expr ]
        |
        [ VISUAL ] ( SUCC | PRED ) COMP
 
@0$strong
dining: 82 states (3..6 bytes), 265 arcs, 2 components, 1
 terminal component
@0$@@0
terminal trivial strongly connected component @@0: @71
@0$pred @@0
@@1

Maria deploys Tarjan’s algorithm for computing strongly connected components. The algorithm was implemented in Prod by Vesa Hirvisalo and initially ported to Maria by Emil Falck. His port was rewritten by Marko Mäkelä to optimize memory usage. The implementation requires two bits for each node in the reachability graph, and one search stack whose length is limited by the length of the longest cycle or acyclic path in the generated reachability graph. Everything else is managed in disk files.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.17 Shortest Paths

The ‘path’ command lets one to find out the shortest path between a specific state and a set of states.

 
statement:
        [ VISUAL ] PATH ( STATE | COMP | expr ) [ STATE ] [ ',' expr ]
        |
        [ VISUAL ] PATH STATE ( COMP | expr ) [ ',' expr ]

The command takes up to three arguments: the target state, the source state, and an optional condition that all states on the path must fulfill. If the source state is omitted, the command finds out the shortest path to the given target state. Either the source or the target state must be specified; the other end of the path may be identified with a state formula or with a strongly connected component number.

When the ‘visual’ keyword is present, the path is displayed graphically (see section Visualizing Graphs and Paths).

 
@0$path @6
shortest path from @0 to @6 (3 nodes):
@0:state (
 fork:
  1,2,3,4,5
 state:
  {1,thinking},{2,thinking},{3,thinking},{4,thinking},{5,thinking}
)
5 predecessors
5 successors
transition left->@2
<
 p:2
>
@2:state (
 fork:
  1,3,4,5
 state:
  {1,thinking},{3,thinking},{4,thinking},{5,thinking},{2,hungry}
)
4 predecessors
5 successors
transition left->@6
<
 p:1
>
@6:state (
 fork:
  3,4,5
 state:
  {3,thinking},{4,thinking},{5,thinking},{1,hungry},{2,hungry}
)
4 predecessors
4 successors

A third variant of the ‘path’ command finds the shortest path from the current state to a loop. In order to avoid an ambiguity in the grammar, the loop must consist of at least three states.

 
statement:
        [ VISUAL ] PATH STATE STATE STATE ( STATE )* [ ',' expr ]

Maria does not check whether the given states really form a loop; it just finds the shortest path to any of the specified states so that the optional condition holds in all states along the path. When the path enters a state that is not the first (and last) state specified, the loop is shifted. The result is an acyclic path leading to a cycle, resembling the shape of the number 6.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.18 Miscellanous Commands

The ‘help’ command displays a short list of all commands. The ‘stats’ command displays some statistical information of the graph being analyzed. The ‘time’ command displays timing statistics since the last invocation of the ‘time’ command, or since the time when the analyzer was started.

The ‘cd’ command can be used to switch the current directory. Without a parameter, it tries to switch to the directory the environment variable HOME expands to. The ‘translator’ command is used to specify the program for translating temporal logic formulae into property automata. When the command is invoked without arguments, the verification of temporal formulae is disabled.

In order for the ‘compiledir’ command to work, Maria must have been compiled with support for compiled expressions enabled (see section Compiling Maria). This command specifies the directory that will be used for generating executable code from the model. Invoking the command without arguments disables the code generator.

The ‘log’ command allows the textual output of query language commands to be redirected to a file, or to the standard error stream when no file name is specified to the command.

The ‘prompt’ command may be useful when Maria is executed as a subprocess. When the command is invoked with a non-null character constant argument, this character will be echoed on its own line before the command prompt is shown. The plain ‘prompt’ command disables this feature again.

 
        HELP
        |
        STATS
        |
        TIME
        |
        CD [ name ]
        |
        TRANSLATOR [ name ]
        |
        COMPILEDIR [ name ]
        |
        LOG [ name ]
	|
        PROMPT [ 'c' ]
 
@0$stats
dining: 82 states (3..4 bytes), 265 arcs

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.2.19 Exiting

The query tool can be exited either by issuing the command ‘exit’ or by typing the end-of-file character EOF at the command prompt.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.3 Some Quirks with the Query Language

Due to the way the query language and the preprocessor (see section Preprocessor Directives) have been implemented, there are some things that are not obvious for the novice user.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.3.1 Separating Statements

Maria uses a script language in which statements are separated by semicolons (‘;’). The separator is optional at the end of input. In the interactive mode, every logical line is parsed separately and semicolons are only required when issuing multiple commands on one command line. In script files, semicolons are mandatory between the statements. Consider the following example:

 
#!/usr/local/bin/maria
graph dining;
function bool eval () false;
eval;
eval

This example will evaluate the function twice. If the semicolon was omitted, the function would be evaluated only once, since ‘eval’ would be treated as a keyword in that case.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.3.2 Conditional Processing in the Editor

The line editor of Maria performs simple lexical analysis to find out whether the line entered is complete. For instance, if the line contains an unbalanced amount of quotes, a continuation prompt will be presented and further lines will be read until all quotes and multi-line comments are balanced or the entry is aborted by typing EOF at the beginning of a continuation line.

However, preprocessor directives for conditional processing are not detected by the command line interpreter. In case you want to enter conditional statements (which must span several physical lines) interactively, you must enter the physical lines as one logical line by quoting all newline characters but the last one. This can be achieved on many systems by typing C-v C-j.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.4 Visualizing Graphs and Paths

Many commands in the query language can be preceded by the ‘visual’ keyword. When this keyword is present, the results of the command will be displayed in a separate visualization process. The visual variant often displays more information, such as edge attributes (transition names and valuations) in displayed paths.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.4.1 GraphViz, the Graph Visualizer

In order for this option to work, a software package for drawing graphs called Graphviz (http://www.graphviz.org) must be installed. The ‘lefty’ command, belonging to the package, must be in the search path, and the script ‘dotty.lefty’ must be located either in the default ‘lefty’ search path or in a directory specified in LEFTYPATH. Also, the visualization script ‘progname-vis’ must be found in the search path, where ‘progname’ is the name used to invoke the analyzer.

On the Microsoft Windows platform, Maria does not invoke GraphViz as a subprocess. Instead, it writes the visualization data to the file ‘maria-vis.out’ in the current directory. This file must be slightly edited before feeding it to the ‘dotty’ or ‘dot’ programs of GraphViz.

The visualization program reacts to some keyboard and mouse commands. Pressing the left or middle mouse button while the mouse pointer is located on a graph node requests for the successors or predecessors of the node to be generated. Holding down the right mouse button brings up a menu whose contents depends on whether the mouse pointer is located above a node, an edge or somewhere else in the graph. There exist keyboard short-cuts for most menu entries.

The visualization program communicates fully asynchronously with Maria via its standard input and output. It reads commands and graph descriptions from standard input and writes Maria commands to standard output. Maria is ready to read and execute these commands whenever it is sitting in the command prompt waiting for input.

Maria uses two commands of the visualization program. It issues the ‘new();’ command followed by a graph description whenever a query language command is preprended with a ‘visual’ keyword. This command causes a new graph to be displayed. The ‘add();’ command is issued whenever a query language command is prepended with several ‘visual’ keywords. This command causes the visualization program to merge the immediately following graph description with the last graph the user has interacted with. The visualization program always issues query language commands prepended with ‘visual visual’, causing the currently displayed graph to be extended.

If you want to access the visualization commands generated by Maria, you can rename the ‘maria-vis’ script and replace it with something like the following script:

 
#!/bin/sh
tee /tmp/maria-vis.out | exec maria-vis-orig "$@"

In order to print a visualized graph, you can save it to a file by selecting a command in the graphical user interface, and then input this file to the ‘dot’ command. Alternatively, you can use a script like the above one and extract the graph descriptions from the intercepted log file. As the ‘dot’ command does not directly support the DIN A4 paper size, you may want to try out one of the following command lines:

 
dot -Gsize=11.69,8.26 -Gcenter=1 -Gmargin=0 -Grotate=90 -Tps
dot -Gsize=8.26,11.69 -Gcenter=1 -Gmargin=0 -Tps

The former line is for horizontal layouts and the latter is for vertical layouts. You may want to add ‘-Grankdir=LR’ to force left-to-right layouting of the graph instead of the default top-to-bottom. The attributes in the graph file override the command line switches.

Both command lines act as filters, reading the graph description from standard input and writing the Postscript code to standard output. The Postscript can be printed directly as such, or embedded in a document, since it follows the Encapsulated Postscript conventions.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.2.4.2 Known Bugs in the Visualizer

Graphical user interfaces are more challenging to program than plain textual programs. We have avoided most of the problems by choosing an external tool that lays out directed graphs. The GraphViz developer team has been very responsive and nice towards us, even though it has limited resources.

Two bugs that may not be fixed soon concern labels in the graph. Some GraphViz utilities fail if labels are longer than about one thousand characters. You can use the ‘hide’ command (see section Excluding Places from Displayed Markings) to shorten node labels. Also backslash characters in labels may be handled incorrectly.

There are also some known bugs in Maria. Presently, Maria identifies paths only by state numbers. When a path is displayed graphically, Maria displays all transitions between each neighboring state along the path.

This treatment of transitions may be confusing especially when displaying counterexample paths (see section Checking Liveness Properties), since Maria omits the property automaton states from the counterexample. Effectively, it projects the product of the reachability graph and the property automaton on the reachability graph. If there are several enabled actions between two states, or if fairness constraints are present, the presented counterexample path may contain extraneous transitions.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.3 Editing Petri Nets with GNU Emacs

We recommend that you use GNU Emacs for editing Petri Net models. There is an Emacs major mode for editing Maria Petri Nets. Its main features are context-sensitive indentation and syntax highlighting. If you are not familiar with these features of Emacs, it is recommended that you read the Emacs tutorial (press C-h t, that is, first hold down the Control key, press h, then release Control and press t) and learn about these features from the on-line help system of Emacs e.g. with the commands C-h i (M-x info) and C-h a (M-x apropos-command).


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.3.1 Installing the Petri Net mode

The Petri Net mode ‘pn-mode’ has been written for GNU Emacs, versions 20.3 and 21. It does not work in version 19.34, which lacks ‘cc-mode’ and some features of ‘font-lock-mode’ the Petri Net mode requires.

Installing the Petri Net mode is simple. Just add the name of the directory containing ‘pn-mode.el’ to load-path and do ‘(require 'pn-mode)’. To do this, you can add e.g. the following lines to your ‘.emacs’ file.

 
(cond ((>= emacs-major-version 20)
       (let ((pn-lisp-dir (expand-file-name "~/elisp")))
         (cond ((file-readable-p pn-lisp-dir)
                (add-to-list 'load-path pn-lisp-dir))
                (require 'pn-mode)
                (setq pn-font-lock-extra-types
                      '("token" "\\sw+_t")))))))

In this example, we also set the variable pn-font-lock-extra-types so that the word ‘token’ and all words ending in ‘_t’ will be treated as type names.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.3.2 Syntax Highlighting

If you are not familiar with the current syntax highlighting features of Emacs (‘font-lock-mode’), you should read the documentation (using the Info system and maybe also the C-h f and C-h v commands).

Adding the following declarations to your ‘.emacs’ file will enable maximum degree of syntax highlighting in all Emacs modes. You may want to consult the documentation of the variable font-lock-maximum-decoration if you want to limit the degree of highlighting in some modes.

 
(global-font-lock-mode t)
(setq font-lock-maximum-decoration t)
(turn-on-font-lock)

[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

2.3.3 Customizing Emacs

One of the most frequent problems of Emacs newcomers is how to convince Emacs to use 8-bit characters, as in the character set standardized by ISO 8859-1, also known as the Latin-1 alphabet. The default 7-bit character set will suffice for editing Petri Net models. But since this section is about fine-tuning, here is something for your ‘.emacs’ file:

 
(standard-display-european t)
(set-input-mode nil nil 'dummy)
(cond ((< emacs-major-version 20)
       (require 'iso-syntax))
      (t
       (setq default-enable-multibyte-characters nil)
       (set-language-environment "Latin-1")))

In the following you will see some more definitions from my ‘.emacs’ file. Feel free to use any of them. In order for ‘pn-mode’ to automatically register the ‘.pn’ extension with ‘speedbar’, the latter should be loaded first.

 
(setq next-line-add-newlines nil);no accidentally inserted empty lines
(setq make-backup-files nil)     ;unless you like the ‘~’ files
(setq mouse-yank-at-point t)     ;for more accurate yanking (pasting)
(setq inhibit-startup-message t) ;disable the startup message
(if (null window-system)
    (menu-bar-mode -1)           ;hide the menu line in text mode
  (if (>= emacs-major-version 20)
      (speedbar-frame-mode t)))  ;enable speedbar, the navigator
(setq visible-bell t)    ;do not beep---flash instead
(line-number-mode t)     ;show line numbers in the mode line
(column-number-mode t)   ;show column numbers in the mode line
(show-paren-mode t)      ;highlight matching parentheses
(auto-compression-mode t);transparently (de)compress ‘.gz’ files

[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

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