[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
2.1 Invoking Maria | Starting the reachability analysis | |
2.1.1 Interrupting the Reachability Analysis | Interrupting the reachability analysis | |
2.2 The Maria Shell | Examining the reachability graph interactively | |
2.3 Editing Petri Nets with GNU Emacs |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
2.1.1 Interrupting the Reachability Analysis | Interrupting the reachability analysis | |
2.1.2 Options | All the options described in detail, in alphabetical order by short options. | |
2.1.3 Option Cross Key | Alphabetical list of long options. |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
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.
Limit the size of array index types to limit possible values. A limit of 0 disables the checks.
Generate the reachability graph of model using breadth-first search. Equivalent to ‘-m model -e breadth’.
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.
The opposite of ‘-C’. Evaluate all expressions in the built-in interpreter. This is the default behavior.
Define the preprocessor symbol symbol. See section Conditional Processing.
Generate the reachability graph of model using depth-first search. Equivalent to ‘-m model -e depth’.
When generating the reachability graph, report the size of the graph after every interval generated edges.
Execute string. See section The Maria Shell.
Load a previously generated reachability graph from ‘graphfile.rgh’.
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.
Print a summary of the command-line options to Maria and exit.
Append directory to the list of directories searched for include files.
Set the right margin of the output to columns. The default is 80.
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).
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.
Load model and prepare for analysing it by constructing a set of reachable states in disk files. See also ‘-M’, ‘-P’, ‘-j’ and ‘-k’.
Load model and clear its reachability graph. See also ‘-b’ and ‘-d’.
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’.
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:
place name
transition name
type name
name of enumeration constant
name of struct or union component
function name
function parameter name
transition variable name
iterator variable name
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.
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’.
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.
Prevent quantification (multi-set sum) of types having more than limit possible values. A limit of 0 disables the checks.
Explore the state space in a modular way. See section Defining Subnets for Modular State Space Exploration.
Consider only one state space. This is the default.
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.
Undefine the preprocessor symbol symbol. See section Conditional Processing.
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’.
Print the version number of Maria and exit.
Display verbose information on different stages of the analysis.
Enable warnings about suspicious net constructs. This is the default behavior.
The opposite of ‘-W’. Disable all warnings.
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.
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’.
The opposite of ‘-Y’. This is the default behavior.
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’.
The opposite of ‘-Z’. This is the default behavior.
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
The Maria shell can be used to interactively examine the reachability graph of a model or to check temporal properties in it.
2.2.1 The Line Editor | The command line editor | |
2.2.2 The Query Language | The query language | |
2.2.3 Some Quirks with the Query Language | Some considerations on the preprocessor | |
2.2.4 Visualizing Graphs and Paths | Visualizing the results |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
2.2.1.1 Name Completion | Features of the Readline library |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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.
2.2.3.1 Separating Statements | Why is a semicolon mandatory here? | |
2.2.3.2 Conditional Processing in the Editor | Using #ifdef on the command line |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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.
2.2.4.1 GraphViz, the Graph Visualizer | The interface to the graph visualizer | |
2.2.4.2 Known Bugs in the Visualizer | Exceptional situations in visualization |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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).
2.3.1 Installing the Petri Net mode | ||
2.3.2 Syntax Highlighting | Syntax highlighting | |
2.3.3 Customizing Emacs | Other things to customize in Emacs |
[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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] | [ ? ] |
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] | [ ? ] |
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 December 1, 2016 using texi2html 1.82.