# Mec 5.4 user's manual

## Mec 5.4 user's manual

This manual documents Mec 5.4.

The manual, like Mec 5, is in the public domain.

Contributors to this manual are Aymeric Vincent and Farès Chucri.

## 1 Introduction

Mec 5 is a model-checker. Its implementation is based on the well-known data structure called “binary decision diagrams” (BDDs).

Mec 5 is basically a tool which will allow you to compute fixpoints over relations of arbitrary arity. However, it will of course allow you to define relations based on descriptions of models. These models can currently only be given as AltaRica models. Former Mec 4 models can be loaded, synchronized, and displayed but nothing useful can be extracted from them with Mec 5 yet.

## 2 First session

Upon startup, Mec 5 displays a small welcome message and awaits input from the user.


Type :help to get a list of commands.          Mec 5.4

[mec]


At the input prompt, the user can either enter a utilitary command which is prefixed by a semi-colon (<:>) or a formula from the specification language.

A formula of the specification language can extend over several lines. In this case, Mec 5 changes the prompt to indicate that it is waiting for more input from the user. Moreover, every definition of an object triggers the printing of its type. For example:

     [mec] R(x) :=
.        x = true;
R: (bool) -> bool
[mec] cst := false;
cst: bool
[mec]


If Mec 5 was compiled with support for a readline-compatible library, it will allow the user to edit its input and use the history facilities of that library. Please refer to the readline library's documentation for further information.

## 3 Computing relations

The main goal of Mec 5 is to compute relations over finite domains. In every place where it made sense, we tried to stick to the syntax of the AltaRica language, so as to provide a coherent user experience. However, there are a couple of exceptions, see Divergences with the AltaRica language.

### 3.1 Domains

Base domains from the AltaRica language are supported and retain the same syntax. They are: bool, finite integer arrays like [-5, 5]', enumerations like { foo, bar }'.

It is also possible to refer to domains via user-defined names thanks to the domain primitive.

Moreover, the following domains are added: for every AltaRica node n loaded into Mec 5, three domains n!c, n!c, and n!ev are defined, which respectively type configurations, super configurations and event vectors of the node n.

### 3.2 Expressions

Except for the two remarks at the beginning of this section, the syntax of AltaRica expressions is respected to the highest extent in formulas of the specification language; it has been enriched by predicates and first-order quantifiers. We describe here only the extensions specific to the specification language.

Predicates or first-order quantifiers can now be used as any other unary expression.

For first-order quantifiers, the pairs of characters <<>> and <[]> are used to denote respectively existential and universal quantifiers.

Any symbol introduced by such a quantifier can be typed explicitly; it even has to be typed if the subformula doesn't provide enough information for the type to be inferred. For example, <x : D> P(x)' is read \exists x.(x\in\cal D\land P(x)).

Using a predicate is done by enclosing its parameters within parentheses and separating them with commas, like a function call in several languages. This is motivated by the fact that a predicate is a function from the types of its arguments to bool.

### 3.3 Defining new objects

In addition to loading AltaRica nodes, the user can define new domains, constants, and relations. Relations are the objects used as predicates.

#### AltaRica nodes

Loading an AltaRica model n' with :ar-load creates two new domains and two new relations:

n!c
the type of its configurations
n!sc
the type of its super configurations
n!ev
the type of its event vectors
n!t
its transition relation (subset of n!c x n!ev x n!c)
n!st
its super transition relation (subset of n!c x n!ev x n!c)
n!init
its set of initial states (subset of n!c)

Note that the epsilon event is represented by an empty string which can be written as a double double-quote <"">.

Event vectors can be accessed in a structured manner. An event vector is made of a local event name and one event name per leaf subnode. Each component is accessed with a dotted notation, using the instance names of the subnodes to navigate down to the leaf subnodes. To access the local event name, the notation is to suffix the event vector's name with a dot <.>.

Examples of valid expressions are: e. = "on"', e.A.S = "failure"'.

#### Type definitions

Defining a new domain is done with the same syntax as in AltaRica, except that the trailing semi-colon (<;>) is mandatory.

     [mec] domain state = { empty, full };
[mec]


#### Constant definitions

For example, the definition of a new constant is written like this:

     [mec] cst := 25;
cst: integer
[mec]


Please note that the current version of Mec 5 doesn't allow first-order quantifiers nor predicates in the expression defining the constant. All the other operators available in expressions are supported.

#### Relation definitions

A relation can be defined by giving an expression that will constrain its parameters:

     [mec] R(x : [0, 10]) := x = 2 | x = 4;
R: ([ 0, 10 ]) -> bool
[mec] :display R
(4)
(2)
[mec]


It is also possible to define a relation through the use of a least or greatest fixpoint.

Here is an example of a least fixpoint:

     [mec] S(x : [0, 10]) += x = 4 | S(x + 1);
S: ([ 0, 10 ]) -> bool
[mec] :display S
(4)
(3)
(2)
(1)
(0)
[mec]


Systems of equations can also be solved, which gives a way to alternate fixpoints. The integer i that can be embedded within operators encodes the parity associated with the relation being defined. Here is a small table relating operators and parities.

operator parity
+i= 2i+1
-i= 2i

The biggest parity in a play of the induced game determines the winning condition. In the absence of the integer i, it defaults to 1.

In order to avoid cluttering the global name space and to save memory, it is possible to use the local keyword to make a relation local to the given system of equations.

Fixpoint equations are ordered depending on their parities; the order in which they are given doesn't matter.

Here is an example that comes from the Toupie tool:

     [mec] domain vertex = [1, 9];
[mec] g(S : vertex, T : vertex) += (T = S + 1) |
.               (T = S & (S = 2 | S = 4 | S = 6 | S = 8)) |
.               (T = 1 & S = 3);
g: ([ 1, 9 ], [ 1, 9 ]) -> bool
[mec] odd(S : vertex) += <n : [0, 4]>(S = n + n + 1);
odd: ([ 1, 9 ]) -> bool
[mec] begin
. local aux(V : vertex) +1= <W : vertex>(g(V, W) & aux(W)) |
.                           <W : vertex>(g(V, W) & odd(W) & tau(W));
.       tau(U : vertex) -2= aux(U);
. end
tau: ([ 1, 9 ]) -> bool
[mec] :display tau
(3)
(2)
(1)
[mec] gtau(S : vertex, T : vertex) := g(S, T) & tau(S) & tau(T);
gtau: ([ 1, 9 ], [ 1, 9 ]) -> bool
[mec]


In this example, g represents the transition relation of a graph which is basically a line with self loops at every even vertex, and a strongly connected component.

The equation system looks for the strongly connected component which contains at least an odd vertex; it is represented by the set of vertices tau, and the gtau transition relation is the restriction of g to the set of vertices tau.

It is easy to obtain the graphical representation of these graphs with the GraphViz package and with the help of the :graph-print-dot command. See graph-print-dot.

### 3.4 Divergences with the AltaRica language

The specification language of Mec 5 is expected to offer for its expressions a superset of the AltaRica expressions. The major differences are listed here.

#### Operators

Logical operators are not available in their english form, so as to limitate namespace pollution. For example, x or y' is accepted in an AltaRica model but not within a Mec 5 specification; it should be written x | y'.

#### Identifiers

In order to allow primed variables, the quote character <'> can be part of a Mec 5 identifier.

An identifier starts with a letter or an underscore and may contain letters, underscores, the quote character, and the carret <^> character.

Double-quotes <"> should be used to enclose identifiers which contain any other character. However, even these identifiers shall not contain dots <.> nor double-quotes <">.

## 4 Commands

You can use the :help command to see a list of the available commands. This list of commands may vary depending on your precise version of the tool, or on the compilation options.

Each command may be abbreviated to any of its non-ambiguous prefixes. Because such non-ambiguous prefixes depend on the other commands available in Mec, the use of an incomplete command name is strongly discouraged in scripts. Its intended use is for interactive typing.

### 4.1 Commands involving defined relations

#### :display

displays a previously defined constant.

     [mec] cst := false;
cst: bool
[mec] :display cst
false
[mec]


#### :graph-print-dot

outputs in GraphViz format the graph corresponding to the transition relation given as a parameter. The relation is split into two or three components like this: consider the sequence of types forming the type of the relation. The largest prefix which is also a suffix of this sequence constitute together the components of the relation which represent the nodes of the graph. If there are unused components in between, they will constitute the events and be displayed as such.

     [mec] R(s : [0, 4], e : {plus, minus}, t : [0, 4]) :=
.        (e = plus) & ((s + 1 = t) | (s = 4) & (t = 0)) |
.        (e = minus) & ((s - 1 = t) | (s = 0) & (t = 4));
R: ([ 0, 4 ], { plus, minus }, [ 0, 4 ]) -> bool
[mec] :graph-print-dot R > R.dot
[mec]


And you could get a PDF file out of the .dot file with a shell command like:

### 7.1 Prerequisites

Mec 5 needs a C compiler, the flex lexical analyzer generator, and a decent yacc or bison parser generator.

Mec 5 will offer improved functionality if a readline-compatible library with its necessary header files is installed on the system.

Mec 5 has been tested to compile out of the box as long as these prerequisites are fulfilled on Sun Solaris, NetBSD, OpenBSD, Mac OS X, various Linux distributions, and Cygwin under Microsoft Windows.

### 7.2 Default compilation

The first step is to untar the sources with a command like:

     $gzip -cd mec-5.4.tar.gz | tar xf -  This should create a directory called mec-5.4. The compilation script must be launched from the mec-5.4/build/ directory: $ cd mec-5.4/build
$./do-build  Then, when compilation is finished, the mec executable can be found in a subdirectory inside mec-5.4/build/, whose name depends on the machine you compiled Mec 5 on. You should be able to copy this executable wherever you wish. For example: $ cd mec-5.4/build
$./do-build Checking where distribution is... found in ../.. Checking whether make is GNU make... no [...]$ ls
darwin-powerpc  do-build        netbsd-powerpc
$cd netbsd-powerpc$ ./mec

Type :help to get a list of commands.          Mec 5.4

[mec]


### 7.3 The compilation process

The do-build script is very handy to get quickly a mec executable that works. However, if you use Mec 5 from its CVS sources for example, you might want to know what simple steps this script performs.

1. Prepare a directory under the build directory and move to this directory. Nothing outside this directory will be touched.
2. Always from this directory, run the configure script which is located at the root of the Mec 5 sources. This creates a Makefile or GNUmakefile suited to your make tool.
3. You may want to run make clean' to rebuild all the object files from scratch. make clean' will remove only files that should be regenerable automatically. It should not touch any file you put by hand in this directory.
4. You should compute the dependencies between files with make depend' (this step is useless with GNU make).
5. You can now type make' to produce the mec executable.

The whole point of knowing this (classical) procedure is that you can avoid many of the steps when for example only one source file was modified and you want to test the change.

### 7.4 Modifying the compiler flags

The compiler flags are stored in the same directory where mec is compiled. They are either in the file GNUmakefile or Makefile, depending on whether your default make utility is GNU Make or not.

1. Edit this file and locate the line starting with CFLAGS=' near the top of the file.
2. Replace the default by the options you wish
3. Issue a make clean' to ensure every source file is recompiled with the new flags
4. Issue a make' to get a new mec executable compiled with your flags

### 7.5 Compiling a DEBUG version

You may want to get verbose output about what is going on inside Mec 5. For this you need to compile a special version of Mec 5, and change the value of the debug-mask option. See debug-mask.

For this, in the Makefile, you need to uncomment the line

     #CPPFLAGS+=     -DDEBUG


which means to remove the sharp sign at the beginning:

     CPPFLAGS+=      -DDEBUG


You can follow the indications of the previous section to locate the Makefile. See Modifying the compiler flags.

Don't forget to make clean' so that every file will be compiled in DEBUG mode.