SVL manual page
Table of Contents

Name

svl - Script Verification Language

Synopsis

svl options [ file[.svl] [script-parameters]]
svl -script options [ file1[.svl] ] [ -output file2 ]
svl -expand [-case] [-indent n] [ file1[.svl] ] [ -output file2 ]
svl -clean [ file[.svl] ]
svl -sweep [ file[.svl] ]
svl -help
svl -version
where the following options are available:
-case, -debug, -ignore, -sh sh-options, -silent.

Description

In the simplest form (first line of the synopsis), SVL takes as input a script file.svl, and produces actions invoking CADP tools.

SVL's input language offers a way to describe (compositional and on-the-fly) verification scenarios, under the form of sequences of statements of several different kinds:

Expressions are built upon the following components:

Moreover, SVL offers a way to invoke Bourne shell commands and to parameterize expressions with respect to particular tools and methods of CADP.

SVL runs a given script through the following steps:

During script execution, several temporary intermediate files may be created, and removed as soon as possible in order to minimize disk space consumption. SVL also maintains a log file named file.log that contains a full diagnostic of the script execution.

Commands

SVL can also be used for alternative actions, using the commands described below:
-script
Stop after generation of the Bourne shell script. If the parameter file2 is specified, then write the generated script to this file. Otherwise display it on the standard output.

-expand
Stop after the expansion phase i.e., after propagating meta-operators inside expressions. If the parameter file2 is specified, then write the expanded SVL program to this file. Otherwise display the expanded program on the standard output.

-clean
Remove the generated shell script and all files created during the latest execution of file.svl. Note that dynamic libraries of BCG files are erased at the same time as the BCG files themselves, and that files created by user written shell commands are not removed. For this command to be effective, both file.log and file.svl must exist in the current directory.

-sweep
Remove temporary files reminiscent of a run in -debug mode (see options below). Note that files created by user written shell commands are not removed. The log file and the output files are not removed either.

-help
Display the available options of SVL.

-version
Display the current version number of SVL.

Note that file.svl (or file1.svl) can be omitted if there exists a unique file with extension .svl in the current directory, in which case this file is considered as the input.

Options

The following options are currently available:
-case
The default behaviour of SVL is to not distinguish lowercase and uppercase characters in identifiers that are not enclosed in double quotes (all characters are turned to uppercase). The -case option forces the distinction.

-debug
Do not erase intermediate files during execution of the generated script, and do not erase the script file after execution. Use command -sweep or -clean to erase these files afterwards.

-ignore
Do not stop execution of the script after an error is issued, continue execution until all instructions of the script are executed (possibly with errors).

-indent n
Set indentation to n blank characters for expanded SVL script display (command -expand). Default value for n is 3.

-sh sh-options
Pass sh-options to the Bourne shell interpreter of the generated script. Note that sh-options must count as a single argument, hence it may be necessary to use quotes to group several options.

-silent
Do not comment actions of the script during execution. This is not a default option.

Syntax of Programs and Expressions

This section describes the syntax of SVL's input language using productions in the Extended Bachus-Naur Form (EBNF).

Terminal symbols are written between double quotes, except for the double quote itself that is written between single quotes. The newline character is written "\n". Non-terminal symbols are written in italic. Optional parts of productions are enclosed between square brackets, and parts that can be iterated zero or more times are written between braces. The following table sums up the non-terminal symbols and their meaning. 

      +--------+--------------------------------------+
      | Symbol |            Description               |
      +--------+--------------------------------------+
      |   P    | program, sequence of statements      |
      |   S    | statement                            |
      |   F    | file                                 |
      |   B    | behaviour expression                 |
      |   SPEC | behaviour specification              |
      |   E    | equivalence relation                 |
      |   M    | verification method                  |
      |   T    | verification tool                    |
      |   LL   | list of labels                       |
      |   L    | label                                |
      |   G    | gate                                 |
      +--------+--------------------------------------+

Programs

A program is a sequence of statements, possibly interleaved with Bourne shell commands. 

    P  ::= <empty>
        |  S 
        |  S ";" P 
        |  "%" shell-line "\n" P

Statements are either assignments, behaviour comparisons, temporal logic verifications, or deadlock/livelock checks.

Comparisons can be parameterized modulo a particular equivalence relation (E), with a particular CADP tool (T), and using a particular exploration method provided by the selected tool (M).

Deadlock/livelock checks can be parameterized with a particular CADP tool. Comparisons, temporal logic verifications, and deadlock/livelock checks may produce diagnostic files.

Assignments produce LTS files. 

    S  ::= F "=" B 
        |  F "=" E "comparison" ["using" M] ["with" T]
                 B ("==" | ">=" | "<=") B 
        |  [F "="] "verify" F ["using" M] "in" B
        |  F "=" "deadlock" ["with" T] "of" B
        |  F "=" "livelock" ["with" T] "of" B
    E  ::= "strong" | "observational" | "branching" 
        |  "tau*.a" | "safety" | "trace" | "weak trace"
        |  "tau-confluence" | "tau-compression" 
        |  "tau-divergence"
 
    M  ::= "std" | "bdd" | "fly" | "bfs" | "dfs"
        |  "acyclic"
    T  ::= "aldebaran" | "bcg_min" | "bisimulator"
        |  "evaluator" | "exhibitor" | "reductor"

Note that fc2tools are no longer supported.

Files are written between double quotes, and must specify a valid extension. Not all extensions are valid in all contexts, as stated more precisely in the sections describing the particular statements and behaviours. 

    F   ::= '"'prefix.EXT'"' | '"'filename'"'
    EXT ::= "aut" | "bcg" | "fc2" | "seq" 
         |  "lnt" | "lotos" | "lot" | "lts" | "exp" 
         |  "hide" | "hid" | "cut" | "rename" | "ren" | "sync" 
         |  "mcl"
A file prefix is any string satisfying the syntax of file names in the current operating system.

Behaviour Expressions

Behaviour expressions are built from elementary systems, that are combined together using the various operators described below. 

    B   ::= SPEC
         |  "stop"
         |  "generation" "of" B
         |  ["leaf" | "root" | "root leaf" | "node" | "smart"]
            ["total" | "partial"]
            [E] ["probabilistic" | "stochastic"]
            "reduction" ["using" M] ["with" T]
            "of" B
         |  ["total" | "partial" | "gate"] "hide" 
            (["all" "but"] [LL] | "using" F) "in" B 
         |  ["total" | "partial" | "gate"] "cut" 
            (["all" "but"] [LL] | "using" F) "in" B 
         |  ["total" | "partial" | "gate"] "prio"
            (["all" "but"] LL (">" ["all" "but"] LL)+)+
            "in" B
         |  ["total" | "single" | "multiple" | "gate"] 
            "rename" (RL | "using" F) "in" B 
         |  ["total" | "partial" | "gate"]  
            ["user"] "abstraction" B
            ["sync" ([LL] | "using" F)] "of" B 
         |  "refined" ["user"] "abstraction" LL
            ["using" B] "of" B
         | "chaos" ( "with" LL 
                   | "with" n "labels" LP 
                   | "using" F )
         | "bag" m ( "with" LL
                   | "with" n "labels" LP "," LP
                   | "using" F )
         | "fifo" m ( "with" LL
                    | "with" n "labels" LP "," LP
                    | "using" F )
         | ["label" | "gate"] "par" ("all" | LD) "in"
           B ("||" B)+
           "end par"
         | ["label" | "gate"] "par" ("all" | LD) "in"
           LL "->" B ("||" LL "->" B)+
           "end par"
         |  B "||" B 
         |  B "|||" B 
         |  B "|[" [LL] "]|" B
         |  B "-||"["?"] B
         |  B "-|||"["?"] B
         |  B "-|[" [LL] "]|"["?"] B
         |  "(" B ")" 
    SPEC ::= F 
          |  [F ":"] L ["[" LL "]"]
    LL ::= L [ "," LL ]
        |  "{"string"}"
    LD ::= L [ "," LD ]
        |  L "#" n [ "," LD ]
        |  "{"string"}"
    RL ::= L "->" L [ "," RL ]
        |  "{"string"}"
    L ::= G | '"'string'"'
    LP ::= '"'string-with-%d'"'
    G, PID ::= lotos-identifier

where n denotes a natural number greater or equal to 2.

A lotos-identifier is a string that starts with a letter and contains letters, digits, and underscores. Underscore can not be the last character of a lotos-identifier.

Precedence and Associativity of Operators

Examples: 

"a.bcg" || "b.bcg" -|| hide G in "c.bcg" ||| "d.bcg"
reads 
"a.bcg" || ("b.bcg" -|| hide G in ("c.bcg" ||| "d.bcg"))

par A#2 in "a.bcg" || reduction of "b.bcg" || "c.bcg" end par
reads 
par A#2 in "a.bcg" || reduction of ("b.bcg" || "c.bcg") end par

Informal Semantics of Behaviour Expressions

The semantics of behaviours is defined as follows:

Behaviour Systems

SPEC may be the name of a file containing a Labelled Transition System (LTS) in one of the AUT (extension .aut), BCG (extension .bcg), FC2 (extension .fc2), or SEQ (extension .seq) file formats. BCG files may define stochastic or probabilistic LTSs as explained in the bcg_min manual page.

SPEC may also be the name of a file containing a network of LTSs in the EXP file format (extension .exp). See a description of the .exp format in the aldebaran manual page

At last, SPEC may also be the name of a LOTOS NT, LOTOS, or FSP file, or an instanciation of a process in a LOTOS NT, LOTOS, or FSP file. In the latter case, the syntax is as follows:
[F ":"] L ["[" LL "]"]
where F is the name of the LOTOS NT (extension .lnt), LOTOS (extension .lotos or .lot), or FSP (extension .lts) file, L is a label denoting the name of the invoked process, and LL is an optional list of labels representing the gate parameters of the process. For an FSP process instanciation, LL must remain empty. Note that L and LL may contain Bourne Shell variables (see Section USING SHELL VARIABLES IN EXPRESSIONS for details).

The filename F is optional. If it is not mentioned, the process will be searched in the default LOTOS NT, LOTOS, or FSP file assigned to the shell variable DEFAULT_PROCESS_FILE on a shell line preceding the expression (see Section SHELL LINES).

Note that SVL relies uniquely on extensions to recognize file formats. All files describing the behaviour of a system must therefore have a valid extension.

Stop

"stop" represents a Labelled Transition System which contains a single state and no transitions.

Hiding

["total" | "partial" | "gate"] "hide" ["all" "but"] [LL] "in" B
["total" | "partial" | "gate"] "hide" "using" F "in" B

will hide the labels found in B using the given hiding rules. These rules can be specified either as a list of labels (first form), or using an external file F (second form).

In the first case, SVL builds a temporary file with extension .hid, filled with the given labels. In the second case, the hide file must be provided by the user, with extension .hide or .hid.

A label can be a gate (possibly followed by experiment offers) or a regular expression denoting a gate (possibly followed by experiment offers). For instance, "G", "G.*", "G !1", "G. !.*" are labels. Among them, only "G" is a gate.

Double quotes around a label can be omitted if and only if the label is a gate (therefore, the syntax of the LOTOS hiding operator is accepted as a particular case of the more general SVL hiding operator). However, for compatibility with LOTOS syntax, gates that are not enclosed between quotes are systematically turned to uppercase, unless the -case option is used. Note that double quotes are mandatory to avoid syntactic ambiguities when a gate has the same name as a reserved SVL keyword (e.g. "reduction", "all", etc.). They are also mandatory to enable the use of shell variables denoting gates or labels as described in Section USING SHELL VARIABLES IN EXPRESSIONS.

The "all but" keywords modify the semantics of the hiding rules: all the labels, except the labels specified in list LL, are hidden in the given behaviour.

The keywords "total", "partial", and "gate" modify the matching mode, that is the way the hiding rules are interpreted, see the caesar_hide_1 manual page. If no matching mode is specified, then the default is "gate", which implements the LOTOS hiding operator (possibly extended by the use of regular expressions on gate names).

For every hiding with "gate" matching, SVL checks whether the gates to be hidden have an appropriate syntax and emit a warning if they appear to contain experiment offers (which is a common mistake for novice users). For instance, 

        hide "G !1"
will trigger a warning message because of the occurence of "!1".

Examples: 

        total hide "G"
hides every label equal to "G", 
        gate hide "G"
hides every label whose gate is G, e.g., "G !1", "G !2", 
        gate hide ".*G.*"
hides every label whose gate contains the character G and 
        partial hide "G"
hides every label whose gate or offers contain the character G.

See the bcg_labels and caesar_hide_1 man pages for more information on the hide file format, and on the semantics of the different matching modes. See the regexp man page for information about the syntax of regular expression.

Cutting

["total" | "partial" | "gate"] "cut" ["all" "but"] [LL] "in" B
["total" | "partial" | "gate"] "cut" "using" F "in" B

will cut the labels found in B using the given cutting rules. These rules can be specified either as a list of labels (first form), or using an external file F (second form).

In the first case, SVL builds a temporary file with extension .cut, filled with the given labels. In the second case, the cut file must be provided by the user, with extension .cut.

A label can be a gate (possibly followed by experiment offers) or a regular expression denoting a gate (possibly followed by experiment offers). For instance, "G", "G.*", "G !1", "G. !.*" are labels. Among them, only "G" is a gate.

Double quotes around a label can be omitted if and only if the label is a gate. However, for compatibility with LOTOS syntax, gates that are not enclosed between quotes are systematically turned to uppercase, unless the -case option is used. Note that double quotes are mandatory to avoid syntactic ambiguities when a gate has the same name as a reserved SVL keyword (e.g. "reduction", "all", etc.). They are also mandatory to enable the use of shell variables denoting gates or labels as described in Section USING SHELL VARIABLES IN EXPRESSIONS.

The "all but" keywords modify the semantics of the cutting rules: all the labels, except the labels specified in list LL, are cut in the given behaviour.

The keywords "total", "partial", and "gate" modify the matching mode, that is the way the cutting rules are interpreted, see the exp.open manual page. If no matching mode is specified, then the default is "gate".

For every cutting with "gate" matching, SVL checks whether the gates to be cut have an appropriate syntax and emit a warning if they appear to contain experiment offers (which is a common mistake for novice users). For instance, 

        cut "G !1"
will trigger a warning message because of the occurence of "!1".

Examples: 

        total cut "G"
cuts every label equal to "G", 
        gate cut "G"
cuts every label whose gate is G, e.g., "G !1", "G !2", 
        gate cut ".*G.*"
cuts every label whose gate contains the character G and 
        partial cut "G"
cuts every label whose gate or offers contain the character G.

See the exp.open man page for more information on the cut file format, and on the semantics of the different matching modes. See the regexp man page for information about the syntax of regular expression.

Priority

["total" | "partial" | "gate"] "prio" (["all" "but"] [LL] (">" ["all" "but"] [LL])+)+ "in" B

sets priorities between the transitions of B. In each state of B, a transition may be executed only if all transitions of higher priority are not ready for execution.

Priorities between transitions (or equivalently, between labels) are defined by a set of priority rules of the form X1 > ... > Xn, where each Xi (for i ranging in 1..n) has the form [all but] LLi and LLi is a list of regular expressions denoting gates or labels. The "all but" keywords that may precede some LLi means all gates or labels but those matching LLi.

Such priority rules define a transitive relation ">>" on labels as follows:

L >> L' means that any transition labeled L has priority over any transition labeled L' or, equivalently, any transition labeled L' yields priority to any transition labeled L.

The relation ">>" must be a strict partial order: B must not contain any label L such that L >> L. If ">>" is not a strict partial order, then the exp.open tool will issue an error message and then exit.

Beware that the rules X > X' and X' > X'' (which are equivalent to X > X' > X'') imply X > X'' only if some label of B matches X'. Therefore, to avoid tricky errors, exp.open checks that every individual regular expression L in LL1, ..., LLn matches some label of B. If not, then exp.open will issue a warning.

The optional "gate", "total", and "partial" keywords define the matching mode, in the same way as for the "hide" and "cut" operators. The matching mode by default is "gate".

See the exp.open manual page for details.

Examples: 

        gate prio
            "A.*" > B > all but "A.*", B
        in
            "f.bcg"
        end prio
defines an LTS in which every transition whose gate starts with the letter "A" has priority over every transition whose gate is "B", which themselves have priority over all other transitions. 
        partial prio
            "A" > all but "A"
        in
            "f.bcg"
        end prio
defines an LTS in which every transition whose label contains the letter "A" has priority over every transition whose label does not contain the letter "A" (including hidden transitions). 
        total prio
            "A" > "B" > "C"
            "D" > "E" > "F"
            "A" > "D"
            "B" > "E"
            "C" > "F"
        in
            "f.bcg"
        end prio
defines an LTS in which:

Note: Strong bisimulation is a congruence for all svl hiding, cutting, renaming, priority, and parallel composition operators operators. However, branching, observational, and safety equivalences are congruences for all svl hiding, cutting, renaming, and parallel composition operators, but not for priority. It should also be noted that tau*.a equivalence is not a congruence for parallel composition.

Renaming

["total" | "single" | "multiple" | "gate"] "rename" RL "in" B
["total" | "single" | "multiple" | "gate"] "rename" "using" F "in" B

will rename the labels of B using the given renaming rules. These rules can be specified either as a list of rules of the form L1 "->" L2, where L1, L2 denote any labels (first form), or using an external file F (second form).

In the first case SVL builds a temporary file with extension .ren, filled with the given substitution rules. In the second case SVL uses the given renaming file, whose extension must be .ren or .rename.

A label can be a gate (possibly followed by experiment offers) or a regular expression denoting a gate (possibly followed by experiment offers). For instance, "G", "G.*", "G !1", "G. !.*" are labels. Among them, only "G" is a gate.

Double quotes around a label can be omitted if and only if the label is a standard LOTOS gate. However, for compatibility with LOTOS syntax, gates which are not enclosed between quotes are systematically turned to uppercase, unless the -case option is used. Note that double quotes are mandatory to avoid syntactic ambiguities when a gate has the same name as a reserved SVL keyword (e.g. "reduction", "all", etc.) and that they enable the use of shell variables denoting gates or labels as described in Section USING SHELL VARIABLES IN EXPRESSIONS.

The keywords "total", "single", "multiple", and "gate" modify the way the left hand sides of the renaming rules are interpreted, see the caesar_rename_1 manual page. If no matching mode is specified, then the default is "gate".

For every renaming with "gate" matching, SVL checks whether the gates to be renamed have an appropriate syntax and emit a warning if they appear to contain experiment offers (which is a common mistake for novice users). For instance, 

        rename "G !1" -> "G !2"
will trigger a warning message because of the occurence of "!1". Note however that 
        rename "G" -> "G !1"
is correct.

Examples: 

        total rename "G" -> "H"
renames to "H" every label equal to "G", 
        gate rename "G" -> "H"
renames to "H" the gate of every label whose gate is G, e.g., "G !1", "G !2", 
        gate rename ".*G.*" -> "H"
renames to "H" the gate of every label whose gate contains a G, 
        single rename "G" -> "H"
replaces the first occurrence of "G" by "H" in every label whose gate or offers contain a G, 
        multiple rename "G" -> "H"
replaces every occurrence of "G" by "H" in every label whose gate or offers contain a G, and 
        total rename "\([A-Z0-9]*\) \(!.*\)" -> "\1 !1 \2"
inserts "!1" between every gate and its first offer.

See the bcg_labels and caesar_rename_1 manual pages for more information on these options and on the format of renaming rules. See also the regexp manual page for more information on regular expressions.

Root Reduction

"root" ["total" | "partial"] [E] ["probabilistic" | "stochastic"] "reduction" ["using" M] ["with" T] "of" B
or more simply
["total" | "partial"] [E] ["probabilistic" | "stochastic"] "reduction" ["using" M] ["with" T] "of" B

will generate the behaviour B (totally or partially) reduced modulo the reduction relation E, and possibly taking into account the probabilistic or stochastic information present in B. The reduction is done with the tool T and using the method M.

T, M, E, "total", "partial", "stochastic", and "probabilistic" are optional:

Example: 

% DEFAULT_REDUCTION_TOOL="reductor"
% DEFAULT_REDUCTION_RELATION="tau*.a"
"a_red.aut" = total reduction of "a.aut"

will induce the total reduction modulo tau*.a of a.aut with reductor, and store the result in file a_red.aut.

When a combination of total/partial reduction, tool, method, and relation is not available, SVL tries to change (at run-time) some parameters to perform a (total or partial) reduction as close as possible to what appears to be expected, trying to preserve the parameters in the following priority order: stochastic or probabilistic reduction, reduction relation, reduction tool, reduction method, and then total or partial reduction.

Moreover, if the reduction fails (for instance because of memory exhaustion) then SVL tries to achieve it another way. For instance, using another tool, or performing a reduction modulo a stronger equivalence relation to reduce the size of the LTS to reducee before re-attempting the weaker reduction. When all attempts fail, then the verification proceeds with the non reduced behaviour.

Note: In some versions of CADP, the aldebaran.old tool, which performs "observational reduction", may be not available. If this is the case, then SVL replaces "observational reduction" by "branching reduction" (performed by the bcg_min tool) and issues a warning message.

Leaf Reduction

"leaf" ["total" | "partial"] [E] ["probabilistic" | "stochastic"] "reduction" ["using" M] ["with" T] "of" B

is a meta-operator that will (totally or partially) reduce the LTSs generated as components of B. As above, T, M, E, the "total" and "partial" keywords and the "probabilistic" and "stochastic" keywords are optional parameters (see ROOT REDUCTION). The final result of a "leaf reduction" is not necessarily as small as that obtained with "root", "root leaf", and "node reduction" since only components of B are reduced.

The expansion rules of "leaf reduction" are the following: 

leaf reduction of B = lRed (B)
lRed (B1 |op| B2) = lRed (B1) |op| lRed (B2)
lRed (Hide (X, B1 |op| B2)) = Hide (X, lRed (B1 |op| B2)) 
lRed (Hide (X, B)) = Red (Hide (X, lRed (B))) 
                     (other cases)
lRed (Cut (X, B1 |op| B2)) = Cut (X, lRed (B1 |op| B2)) 
lRed (Cut (X, B)) = Red (Cut (X, lRed (B))) 
                     (other cases)
lRed (Prio (X, B1 |op| B2)) = Prio (X, lRed (B1 |op| B2))
lRed (Prio (X, B)) = Red (Prio (X, lRed (B))) 
                     (other cases)
lRed (Ren (X, B1 |op| B2)) = Ren (X, lRed (B1) |op| lRed (B2))
lRed (Ren (X, B)) = Red (Ren (X, lRed (B)))
                     (other cases)
lRed (Abs (B1, X, B2)) = Red (Abs (B1, X, lRed(B2)))
lRed (Gen (B)) = Red (Gen (lRed (B)))
lRed (B) = Red (B) otherwise
where Red means reduction, Ren means rename, Abs means abstraction or refined abstraction (its first operand is the interface, and its third operand is the body), Gen means generation, B, B1, B2 denote any behaviour, X denotes either a file or a list of items (labels or renaming rules), and |op| denotes any parallel composition operator.

Note that expansion does not propagate meta-operations across "reduction" operations, nor inside the interface part of the "abstraction" operation.

Note also that, at the end of the expansion phase, the obtained abstract tree is cleaned to optimize execution. Therefore some "reduction" operators inserted by the lRed function are then removed by the cleaning function. For instance, any "reduction" operation inserted at the root of the body of an "abstraction" operation will be systematically deleted to avoid the (useless and expensive) generation of the behaviour to be abstracted. See the CLEANING section below.

Root Leaf Reduction

"root leaf" ["total" | "partial"] [E] ["probabilistic" | "stochastic"] "reduction" ["using" M] ["with" T] "of" B

is a meta-operator, which has the same meaning as "root reduction of leaf reduction of B".

Node Reduction

"node" ["total" | "partial"] [E] ["probabilistic" | "stochastic"] "reduction" ["using" M] ["with" T] "of" B

is a meta-operator that will generate B in a compositional way. The only difference between "root leaf" and "node reduction" is that "node reduction" performs also reduction at each parallel composition node, and that hide and cut operators are propagated as far as possible inside the behaviour expression. As above, T, M, E, the "total" and "partial" keywords and the "probabilistic" and "stochastic" keywords are optional parameters (see ROOT REDUCTION).

The expansion rules of "node reduction" are the following: 

node reduction of B = Red (nRed (B))
nRed (B1 |op| B2) = Red (nRed (B1) |op| nRed (B2))
nRed (Hide (X, B)) = Red (Hide (X, nRed (B)))
nRed (Cut (X, B)) = Red (Cut (X, nRed (B)))
nRed (Prio (X, B)) = Red (Prio (X, nRed (B)))
nRed (Ren (X, B)) = Red (Ren (X, nRed (B)))
nRed (Abs (B1, X, B2)) = Red (Abs (B1, X, lRed (B2)))
nRed (Gen (B)) = Red (Gen (lRed (B)))
nRed (B) = Red (B) otherwise
where Red means reduction, Ren means rename, Abs means abstraction or refined abstraction (its first operand is the interface, and its third operand is the body), Gen means generation, B, B1, B2 denote any behaviour, X denotes either a file or a list of items (labels or renaming rules), and |op| denotes any parallel composition operator.

Note that expansion does not propagate meta-operations across "reduction" operations, nor inside the interface part of the "abstraction" operation. The "node reduction" becomes a "leaf reduction" (lRed) once it has passed through an "abstraction", "refined abstraction", or "generation" operator.

Note also that, at the end of the expansion phase, the obtained abstract tree is cleaned to optimize execution. Therefore some "reduction" operators inserted by the nRed function are then removed by the cleaning function. For instance, any "reduction" operation inserted at the root of the body of an "abstraction" operation will be systematically deleted to avoid the (useless and expensive) generation of the behaviour to be abstracted. See the CLEANING section below.

Smart Reduction

"smart" ["total" | "partial"] [E] ["probabilistic" | "stochastic"] "reduction" ["using" M] ["with" T] "of" B

is an operator that will generate B in a compositional way using a smart heuristic, the aim being to try to avoid generating too large intermediate LTSs.

To do so, B is first turned into a network whose LTSs are minimized. Then, SVL executes the following loop until this network contains only a single LTS:

1
Automatically select several LTSs in the network; this step relies on a heuristic metric (computed by exp2c) that depends on an estimate rate of hidden transitions and an estimate rate of interleaved transitions belonging to the product of selected LTSs.

2
Compose the selected LTSs in parallel.

3
Generate the LTS corresponding to the composition obtained in step 2 and minimize it.

4
Replace in the network the LTSs selected in step 1 by the LTS resulting from step 3; continue in step 1.

The LTS corresponding to the obtained network is finally generated, minimized, and returned as the LTS corresponding to B.

The maximal number of LTSs that can be selected in step 1 is bounded. By default, the limit is set to 4. This limit can be changed by assigning a different value to the variable DEFAULT_SMART_LIMIT.

Note: Unlike other meta-operations, "smart reduction" is not expanded. Indeed, the expansion phase is static, whereas the order in which the LTSs in B are composed by "smart reduction" is determined at run time.

Generation

"generation" "of" B

will force the generation of an explicit LTS representation of B. More precisely, if B is a LOTOS NT, LOTOS, or FSP program, this program will be compiled, and if B has an implicit representation as a network of communicating automata in the EXP format, then an explicit representation of B will be generated.

There are some cases where the "generation" operation is implicit:

Note that, during the expansion phase, meta-operators do not propagate across "generation" operations in the abstract syntax tree.

Parallel Composition

B "||" B
B "|||" B
B "|[" [LL] "]|" B

has the same semantics as the parallel composition in LOTOS: "|||" denotes parallelism with synchronization on termination only, "||" denotes parallelism with synchronization on all gates, and at last "|[" [LL] "]|" denotes parallelism with synchronization on termination and on gates specified in the optional list of labels LL.

Generalized Parallel

["label" | "gate"] "par" ("all" | LD) "in" B ("||" B)+ "end par"
["label" | "gate"] "par" ("all" | LD) "in" LL "->" B ("||" LL "->" B)+ "end par"

are extensions of the E-LOTOS generalized parallel operators. They denote the concurrent execution of behaviours following synchronisation rules expressed using the construct "all" or the synchronisation list "LD", and the label lists preceding the "->" symbols, called synchronisation interfaces.

The first form is equivalent to the second form in which all synchronisation interfaces are empty.

The semantics of synchronisation rules is as follows:

Transition synchronisation is a generalization of LOTOS rendezvous: the transition resulting from the synchronisation of transitions labelled with L is also labelled with L. Transitions whose label does not match any synchronisation rule perform asynchronously.

Note that behaviours always synchronize on labels whose gate is the termination gate and never synchronize on hidden events.

The following syntactic restrictions should hold:

Abstraction

["total" | "partial" | "gate"] ["user"] "abstraction" B "sync" [LL] "of" B
["total" | "partial" | "gate"] ["user"] "abstraction" B "sync" "using" F "of" B
["total" | "partial" | "gate"] ["user"] "abstraction" B "of" B

Abstraction is also called semi-composition. It allows to restrict the rightmost behaviour with respect to its environment i.e., an expression called the interface and a synchronization set.

Interfaces can be either ``exact'' interfaces i.e., parts of the syntactic environment of the sub-expression to be restricted, or ``user-given'' interfaces i.e., expressions that are supposed to correctly approximate this environment. The second case must be expressed with the "user" keyword that involves the generation of some validation predicates in the produced LTS. These predicates are checked afterwards, when the components obtained by user abstractions are recomposed together. SVL issues a warning message if the check fails.

Similarly to hide, cut, and rename operators, the synchronization set can be given explicitly as a list of labels in the abstraction expression, or in a .sync file. See the projector manual page for more information on the sync file format.

A label can be a gate (possibly followed by experiment offers) or a regular expression denoting a gate (possibly followed by experiment offers). For instance, "G", "G.*", "G !1", "G. !.*" are labels. Among them, only "G" is a gate.

Double quotes around a label can be omitted if and only if the label is a gate . However, gates that are not enclosed between quotes are systematically turned to uppercase, unless the -case option is used. Note that double quotes are mandatory to avoid syntactic ambiguities when a gate has the same name as a reserved SVL keyword (e.g. "reduction", "all", etc.). They are also mandatory to enable the use of shell variables denoting gates or labels as described in Section USING SHELL VARIABLES IN EXPRESSIONS.

The "all but" keywords modify the semantics of the synchronization rules: all the labels, except the labels specified in list LL, must be used in the synchronization between the given behaviour and its interface.

The keywords "total", "partial", and "gate" modify the matching mode, that is the way the synchronization rules are interpreted, see the projector manual page. If no matching mode is specified, then the default is "gate".

If no synchronization set is given (no "sync" keyword), the synchronization is done as follows:

For every abstraction with "gate" matching, SVL checks whether the gates to be synchronized have an appropriate syntax and emit a warning if they appear to contain experiment offers (which is a common mistake for novice users). For instance, 

        abstraction ... sync "G !1"
will trigger a warning message because of the occurence of "!1".

Examples: 

        total abstraction ... sync "G"
synchronizes every label equal to "G", 
        gate abstraction ... sync "G"
synchronizes every label whose gate is G, e.g., "G !1", "G !2", 
        gate abstraction ... sync ".*G.*"
synchronizes every label whose gate contains the character G and 
        partial abstraction ... sync "G"
synchronizes every label whose gate or offers contain the character G.

See the projector man page for more information on the sync file format, and on the semantics of the different matching modes. See the regexp man page for information about the syntax of regular expression.

Before doing the semi-composition, SVL does the following to optimize verification efficiency:

Infix Abstraction Operators

B1 "-||" ["?"] B2
B1 "-|||" ["?"] B2
and
B1 "-|[" [LL] "]|" ["?"] B2

are shorthand notations for, respectively,
["user"] "abstraction" B2 "of" B1
["user"] "abstraction" B2 "sync" "of" B1
and
["user"] "abstraction" B2 "sync" [LL] "of" B1
where the "?" symbol has the same meaning as the "user" keyword.

Refined Abstraction

"refined" ["user"] "abstraction" LL ["using" B] "of" B

Refined abstraction allows to restrict the rightmost behaviour expression (the body) with respect to some of its neighbours (specified in the list LL).

The neighbours are those behaviour systems (LTS files, files containing networks of LTSs, LOTOS NT, LOTOS, or FSP files, or processes in LOTOS NT, LOTOS, or FSP files) that are in the environment of (i.e., composed in parallel with) the body. The identifier of a neighbour is either its process name (without offer parameters) in the case of a process, or its filename (with extension and between quotes) in all other cases. Each label in LL must be the identifier of exactly one neighbour (see examples below).

The behaviour expression that follows the "using" keyword, if present, should provide a set of labels, which includes all labels that can be fired by the body. Its states and transitions are simply ignored. These labels allow to compute the possible synchronizations between the body and its environment, without having to generate the LTS corresponding to the body. This expression is required if the body is a LOTOS NT, LOTOS, or FSP file or a process in a LOTOS NT, LOTOS, or FSP file and can be omitted otherwise. If the body is a parallel composition expression (encoded in an EXP file) or an EXP file, this set is computed automatically using the exp.open tool. If the body is neither a LOTOS NT, LOTOS, or FSP file, a process in a LOTOS NT, LOTOS, or FSP file, a parallel composition expression, nor an EXP file, then its LTS is generated and serves as label set.

The "user" keyword should be used when the user cannot guarantee that the label set provided by this expression includes all labels that can be fired by the body. In this case, validation predicates will be generated in the resulting LTS, and warning messages will be issued if the validation predicates are not satisfied.

Refined abstraction executes in two steps: in a first step, an interface and a synchronization set will be generated automatically from the behaviours of neighbours and the environment of the expression, using the exp.open tool; during this step, the LTSs of neighbours in LL are automatically minimized modulo safety equivalence, so as to generate as small an interface as possible; in a second step, the interface and synchronization set obtained during the first step are used to restrict the body, using the projector tool.

Examples:

The following expressions are examples of correct usage of the "refined abstraction" operator: 

"a.bcg" = node strong reduction of
  (
    P
  ||
    (
      (refined abstraction P, "r.bcg" using "q.bcg" of Q)
    ||
      hide A in "r.bcg"
    )
  )

"a.bcg" = generation of
  (
    P
  ||
    (
      refined abstraction P of
        (
          Q
        ||
          (refined abstraction P, Q using "r.bcg" of R)
        )
    )
  )

The following expression is an example of incorrect usage of the "refined abstraction" operator, where Q has two neighbours whose identifier is P, and no neighbour whose identifier is R: 

"a.bcg" = generation of
  (
    P
  ||
    (
      (refined abstraction P, R using "q.bcg" of Q)
    ||
      hide A in P
    )
  )

Chaos Automata

"chaos" "using" F
"chaos" "with" LL
"chaos" "with" n "labels" LP

generate an LTS with a single state and looping transitions, using the bcg_graph tool.

There are several ways to define the transition labels:

See the bcg_graph manual page for more information.

Example:

If "labels" is a file containing three labels A1, A2, and A3, then the following three behaviours denote the same explicit LTS that contains a unique state and three transitions from and to this state, labelled respectively A1, A2, and A3. 


    chaos using "labels"
    chaos with 3 labels "A%d"
    chaos with "A1", "A2", "A3"

Bags and Fifo Buffers

"bag" m "using" F
"bag" m "with" LL
"bag" m "with" n "labels" LP1 "," LP2
"fifo" m "using" F
"fifo" m "with" LL
"fifo" m "with" n "labels" LP1 "," LP2

generate an LTS modeling a communication buffer of size m, which can be either a bag (i.e., a communication buffer in which the ordering of messages is not enforced) or a FIFO (First In/First Out) buffer.

m must be a natural number (sequence of digits), possibly enclosed between double quotes. it can also be defined using shell variables (in which case double quotes are mandatory), such as e.g., "$N" and "${N}0".

Buffers distinguish between two kinds of labels, namely inputs and outputs, modeling respectively the ingoing and outgoing messages. Each input is paired with the corresponding output.

There are several ways to define the labels handled by the buffer:

See the bcg_graph manual page for more information.

Example:

If "labels" is a file containing four labels INPUT1, INPUT2, OUTPUT1, and OUTPUT2, then the following three behaviours denote the same explicit LTS that models a FIFO buffer with 4 places and exchanging 2 different messages. 


    fifo 4 using "labels"
    fifo 4 with 2 labels "INPUT%d", "OUTPUT%d"
    fifo 4 with "INPUT1", "OUTPUT1", "INPUT2", "OUTPUT2"

Cleaning

Since the expansion phase may generate some redundant operations, the tree of the behaviour is always cleaned using the following clean function: 
clean (Gen (Gen (B))) = clean (Gen(B))
clean (Gen (SPEC)) =
        Gen (SPEC) if LOTOS NT, LOTOS, FSP, or EXP
        SPEC       otherwise
clean (Gen (Stop)) = Stop
clean (Gen (Abs (B1, L, B2))) = clean (Abs(B1, L, B2))
clean (Gen (Red (B))) = clean (Red (B))
clean (Gen (B)) = Gen (clean (B))
clean (Hide (L, Hide (L', B)) = clean (Hide (L u L', B))
                          if matching modes are the same
clean (Hide (X, Stop)) = Stop
clean (Hide (X, B)) = Hide (X, clean (B))
clean (Cut (L, Cut (L', B)) = clean (Cut (L u L', B))
                          if matching modes are the same
Clean (Cut (L, Stop)) = Stop
clean (Cut (X, B)) = Cut (X, clean (B))
clean (Prio (X, B)) = Prio (X, clean (B))
clean (B1 |op| B2) = clean (B1) |op| clean (B2)
clean (Abs (Stop, L, B2)) = Stop
clean (Abs (B1, L, B2)) = Abs (clean (B1), L, clean (B2))
clean (Red (Red' (B))) = clean (Red' (B)) if Red' <= Red
clean (Red (Gen (Red (B)))) = clean (Red (Gen (B)))
clean (Red (Abs (B1, L, Red (B2)))) = 
                              clean (Red (Abs (B1, L, B2)))
clean (Red (Hide (L, Red (B)))) = clean (Red (Hide (L, B)))
clean (Red (Cut (L, Red (B)))) = clean (Red (Cut (L, B)))
clean (Red (Ren (X, Red (B)))) = clean (Red (Ren (X, B)))
clean (Red (Stop)) = Stop
clean (Red (B)) = Red (clean (B))
clean (Ren (X, Stop)) = Stop
clean (Ren (X, B)) = Ren (X, clean (B))
clean (B) = B otherwise
where Red <= Red' means Red denotes reduction modulo a weaker (<) or equal (=) reduction relation than this of Red'. The "weaker" (partial order) relation is represented by the diagram below, where an arrow goes from R to R' if R' < R: 
                         strong
                            |
                      +-----+-----+
                      |           |
                      |     tau-divergence
                      |           |
                      |     tau-compression
                      |           |
                      |     tau-confluence
                      |           |
                    trace     branching
                      |           |
                      |      +----+----+
                      |      |         |
                      |   tau*.a  observational
                      |      |         |
                      |      +----+----+
                      |           |
                      |        safety
                      |           |
                      +-----+-----+
                            |
                        weak trace

Informal Semantics of Operations

The semantics of operations is defined as follows:

Assignment

F "=" B

will store in file F the system resulting from the behaviour expression B, with possibly format conversion. F is created in the current directory.

The file format of F can be BCG (extension .bcg), AUT (extension .aut), SEQ (extension .seq), FC2 (extension .fc2), or EXP (extension .exp).

Note that if B is a LOTOS NT, LOTOS, or FSP file, or if B is a network of communicating automata (parallel composition expression) and the format of F is this of an explicit LTS, then SVL issues a warning message since the behaviour B should be generated before being assigned. However, the generation will be performed by SVL.

Assignment to EXP files must be used cautiously, as shows the following example.

Consider the following program, where <B1>, <B2>, and <B3> are any behaviours. 

"a.bcg" = <B1>;
"c.bcg" = <B2>;
"b.exp" = "a.bcg" ||| "c.bcg";
"a.bcg" = <B3>;
"d.bcg" = generation of "b.exp"
It must be clear that the automaton described in "d.bcg" represents the behaviour <B3> ||| <B2> instead of <B1> ||| <B2> since at the time "b.exp" is evaluated, "a.bcg" is bound to <B3>.

On the contrary, in the following program, 

"a.bcg" = <B1>;
"c.bcg" = <B2>;
"b.exp" = (reduction of "a.bcg") ||| "c.bcg";
"a.bcg" = <B3>;
"d.bcg" = generation of "b.exp"
the automaton described in "d.bcg" represents the behaviour (reduction of <B1>) ||| <B2>, since the reduction must be evaluated at the time "b.exp" is created.

Comparison

F "=" E "comparison" ["using" M] ["with" T] B ("==" | "<=" | ">=") B

allows to compare two behaviours. Symbol "==" means "equivalence" whereas "<=" and "=>" denote relation pre-orders. F must have extension .aut, .bcg, .fc2, or .seq. It is created in the current directory, and may contain a diagnostic of the comparison if the result is FALSE.

Some combinations of tool, method, and relation are not available. In this case, SVL tries to change some parameters to perform a reduction as close as possible to what seems to be expected. As much as possible, SVL tries to preserve the parameters in the following priority order: relation, tool, and then method.

The tool T and the method M are optional parameters and similar to those described above for the reductions. The default values may be modified via the variables DEFAULT_COMPARISON_TOOL, and DEFAULT_COMPARISON_METHOD. These variables are initialized with the tool bisimulator and the dfs method.

The equivalence relation E is optional as well; when omitted the default equivalence relation is used (strong). This default value can be modified via the shell variable DEFAULT_COMPARISON_RELATION.

Verification

[F1 "="] "verify" F2 ["using" M] "in" B

allows to evaluate a property on a behaviour, using the EVALUATOR tool using method M. The property must be written in file F2 in the regular alternation-free mu-calculus (see the evaluator manual page) and must have extension .mcl. The method M is optional and may be one of "dfs", "bfs", or "acyclic". See the evaluator manual page for details about these methods. The default value may be modified via the variable DEFAULT_VERIFY_METHOD, initially set to "dfs".

File F1 is optional. If present, it will contain a diagnostic of the verification. It must have extension .aut, .bcg, .fc2, or .seq.

Deadlock and Livelock Checking

F "=" "deadlock" ["with" T] "of" B
F "=" "livelock" ["with" T] "of" B

allows to search deadlocks, respectively livelocks, in a behaviour. F must have extension .aut, .bcg, .fc2, or .seq. It is created in the current directory, and may contain a diagnostic of the search, if available.

The tool T is an optional parameter, similar to those described above for the reductions and comparisons. The default value may be modified via the variable DEFAULT_LOCK_TOOL. This variable is initialized with the tool aldebaran . Other available tools are exhibitor (deadlocks only) and evaluator (livelocks only). Note that fc2tools are no longer supported.

Shell Lines

SVL offers the facility to insert shell lines between statements. Such lines must start with the symbol "%", and finish with the end of the line.

Of course, SVL operates no static control of the validity of inserted shell lines. Hence, erroneous shell scripts may be generated by SVL due to syntax errors made by the user, or to shell lines breaking the consistency of SVL execution.

Comments

Every string delimited by "(*" and "*)" is considered as a comment, and is ignored by SVL. This is the standard syntax of comments in LOTOS.

Note that such comments are not allowed in shell lines (starting with "%"). Shell comments should be used instead.

Using Shell Variables in Expressions

Every string between double quotes may use defined Bourne shell variables ("$"defined-shell-variable). This includes the special Bourne shell variables "$#", "$*", "$@", "$1", "$2", ... which can be used to refer to the script-parameters passed to the generated script.

However, remember that when using filenames, extensions must always be explicitly mentioned, for the following reasons:

Examples: 

% for FNAME in a b c
% do
"reduced-$FNAME.aut" = reduction of "$FNAME.aut"
% done
is correct, but 
% for FNAME in a.aut b.aut c.aut
% do
"reduced-$FNAME" = reduction of "$FNAME"
% done
is not correct (a run-time error is issued) because "$FNAME" is interpreted at compile-time as a process whereas it denotes a file name. However, the following example is correct: 
% DEFAULT_PROCESS_FILE="a.lotos"
% for PNAME in "P1[G1, G2]" P2
% do
"reduced-$PNAME" = reduction of generation of "$PNAME"
% done
This loop reduces in turn the LTSs of processes P1[G1, G2] and P2 found in file "a.lotos".

Shell variables can also be used to denote gates or labels as in the following example: 

% for G in PUT GET
% do
  "P_$G.exp" = 
      "spec.lotos":P ["$G"] 
      |["$G"]|
      "spec.lotos":P ["$G"];
% done
This loop generates in turn two composition expressions stored in EXP files, corresponding to "spec.lotos":P [PUT] |[PUT]| "spec.lotos":P [PUT] and "spec.lotos":P [GET] |[GET]| "spec.lotos":P [GET].

Note also that shell variables and expressions can be used to denote lists of labels, gates, or renaming rules, using the braced notation. A shell expression written between braces will be interpreted as a list of labels instead of a single label, thus differentiating from the quoted notation.

For instance, one may write 

% L1="A,
"f1.bcg" = total hide D, {$L1} in "f2.bcg";
% L2="A, B, C"
"f3.bcg" = "f4.bcg" |[ {$L2} ]| "f5.lotos":P ["D", {$L2}];
% L3="
% L4="C -> A, B -> C"
"f6.bcg" = total rename "D" -> "E", {$L3, $L4} in "f7.bcg";
to express that $A, $B, $C must not be interpreted as single labels or rules (as it would be in "$A", "$B", "$C") but as lists of labels or rules.

Note that the label and rule separator is the coma. However, comas between parentheses are not interpreted as label or rule separators, as long as parentheses are well-balanced.

Local Shell Variables

SVL uses several shell variables. Some of them may be modified (carefully) by the user, in a shell line, as already mentionned. Others should not be used nor modified.

User redefinable variables and their default values are the following: 

+----------------------------+------------+----------------+
|           Variable         |  Default   |  Alternative   |
+----------------------------+------------+----------------+
| DEFAULT_REDUCTION_TOOL     | See section| aldebaran      |
|                            | REDUCTION  | bcg_min        |
|                            | above      | reductor       |
+----------------------------+------------+----------------+
| DEFAULT_COMPARISON_TOOL    | bisimulator| aldebaran      |
+----------------------------+------------+----------------+
| DEFAULT_LOCK_TOOL          | aldebaran  | exhibitor      |
|                            |            | evaluator      |
+----------------------------+------------+----------------+
| DEFAULT_REDUCTION_METHOD   | std        | bdd fly        |
+----------------------------+------------+----------------+
| DEFAULT_COMPARISON_METHOD  | dfs        | std bdd fly    |
|                            |            | bfs dfs        |
+----------------------------+------------+----------------+
| DEFAULT_VERIFY_METHOD      | dfs        | bfs acyclic    |
+----------------------------+------------+----------------+
| DEFAULT_REDUCTION_RELATION | strong     | observational  |
|                            |            | tau*.a         |
|                            |            | branching      |
|                            |            | safety         |
|                            |            | tau-compression|
|                            |            | tau-divergence |
|                            |            | tau-confluence |
|                            |            | trace          |
|                            |            | weak trace     |
+----------------------------+------------+----------------+
| DEFAULT_COMPARISON_RELATION| strong     | observational  |
|                            |            | tau*.a         |
|                            |            | branching      |
|                            |            | safety         |
|                            |            | trace          |
|                            |            | weak trace     |
+----------------------------+------------+----------------+
| DEFAULT_PROCESS_FILE       | not set    |                |
+----------------------------+------------+----------------+
| DEFAULT_SMART_LIMIT        | 4          | any nat > 1    |
+----------------------------+------------+----------------+
Note: Variable DEFAULT_LOTOS_FILE is deprecated. Instead, it is recommended to use DEFAULT_PROCESS_FILE, which can be any file containing a LOTOS (extensions .lot and .lotos), LOTOS NT (extension .lnt), or FSP (extension .lts) program. However, scripts using DEFAULT_LOTOS_FILE should continue to work correctly.

Also, the following variables may be redefined:

ALDEBARAN_OPTIONS, BCG_GRAPH_OPTIONS, BCG_IO_OPTIONS_INPUT, BCG_IO_OPTIONS_OUTPUT, BCG_LABELS_OPTIONS, BCG_MIN_OPTIONS, BCG_OPEN_OPTIONS, BCG_OPEN_CC_OPTIONS, CAESAR_ADT_OPTIONS, CAESAR_OPEN_OPTIONS, CAESAR_OPEN_CC_OPTIONS, CAESAR_OPTIONS, EVALUATOR_OPTIONS, EXHIBITOR_OPTIONS, EXP_OPEN_OPTIONS, EXP_OPEN_CC_OPTIONS, FSP_OPEN_OPTIONS, FSP_OPEN_CC_OPTIONS, GENERATOR_OPTIONS, LNT_OPEN_OPTIONS, LNT_OPEN_CC_OPTIONS, PROJECTOR_OPTIONS, REDUCTOR_OPTIONS, SEQ_OPEN_OPTIONS, SEQ_OPEN_CC_OPTIONS.

They may be assigned options which are passed to tools. They are empty by default. See the different tool manual pages for information about available options.

At last, the following variables may be redefined:

ALDEBARAN_EXECUTABLE, BCG_GRAPH_EXECUTABLE, BCG_IO_EXECUTABLE, BCG_LABELS_EXECUTABLE, BCG_MIN_EXECUTABLE, BCG_OPEN_EXECUTABLE, BISIMULATOR_EXECUTABLE, CAESAR_ADT_EXECUTABLE, CAESAR_EXECUTABLE, CAESAR_OPEN_EXECUTABLE, EVALUATOR_EXECUTABLE, EXHIBITOR_EXECUTABLE, EXP_OPEN_EXECUTABLE, FSP_OPEN_EXECUTABLE, GENERATOR_EXECUTABLE, LNT_OPEN_EXECUTABLE, PROJECTOR_EXECUTABLE, REDUCTOR_EXECUTABLE, SEQ_OPEN_EXECUTABLE.

They may be assigned a path to a different version of the executable file related to a given tool.

Use of variables whose name starts with SVL_ should be avoided. This syntax is reserved to all functions and variables defined internally by SVL.

Environment Variables

The following environment variables are used:
$CADP
Needed. This variable contains the path of directory where CADP is installed.

$CADP/com
This directory should be put in the $PATH variable.

$SVL
Optional. The first action of the generated script is to include the file $CADP/src/svl/standard, containing a list of predefined shell functions and variables. However, if the environment variable SVL is defined, the included file is $SVL/src/svl/standard. Moreover, the kernel program svl_kernel will be searched in $SVL/bin.`arch` instead of $CADP/bin.`arch`.

Files

The following files and extensions are handled by SVL, either as inputs, outputs, or as temporary intermediate files. 
+--------------+-------------------------+-----+-----+-----+
|  Extension   |       Description       | In  | Out | Tmp |
+--------------+-------------------------+-----+-----+-----+
| .svl         | SVL program             |  X  |     |     |
| .lnt         | LOTOS NT program        |  X  |     |     |
| .lotos .lot  | LOTOS program           |  X  |     |     |
| .lts         | FSP program             |  X  |     |     |
| .aut         | LTS in Aldebaran format |  X  |  X  |  X  |
| .bcg         | LTS in BCG format       |  X  |  X  |  X  |
| .fc2         | LTS in FC2 format       |  X  |  X  |  X  |
| .seq         | LTS in sequence format  |  X  |  X  |     |
| .exp         | network of LTSs         |  X  |  X  |  X  |
| .hide .hid   | labels to hide          |  X  |     |  X  |
| .cut         | labels to cut           |  X  |     |  X  |
| .rename .ren | labels to rename        |  X  |     |  X  |
| .sync        | labels to synchronize   |  X  |     |  X  |
| .mcl         | temporal logic formula  |  X  |     |     |
| .log         | log of execution        |     |  X  |     |
+--------------+-------------------------+-----+-----+-----+
Note: SVL generates temporary files in the current directory. To avoid clashes with existing files, file names generated by SVL are prefixed with a string of the form svlxxx_, where xxx is a 3 digits number. Hence it is recommended to avoid naming user files this way.

Exit Status

When the source is erroneous, error messages are issued. Exit status is 0 if everything is alright, 1 otherwise.

Bibliography

Full descriptions of the compositional generation process are given in "$CADP/doc/*/Krimm-Mounier-97.*".

Authors

SVL version 2.0 and later: Hubert Garavel, Frederic Lang, Marc Herbert.

SVL versions 1.0 to 1.6 (kept for internal use and never distributed officially): Mark Jorgensen, Christophe Discours, Hubert Garavel.

The authors owe thanks to Radu Mateescu and Charles Pecheur for their feedback about SVL 1.* and to Laurent Mounier for his useful advices.

See Also

See also the following reference manuals:
aldebaran , bcg_graph bcg_io , bcg_labels , bcg_min , bcg_open , caesar , caesar.adt , caesar.open , caesar_hide_1 , caesar_rename_1 , evaluator , exhibitor , exp.open , generator , projector , reductor , regexp , seq.open

Directives for installation are given in file $CADP/INSTALLATION.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.

Bugs

Please report any bug to cadp@inria.fr

Table of Contents