Slang: the Script LANGuage
Slang is an interpreted imperative language, with runtime type checking.
Here you can find its grammar.
Assignments, and Mocha context
Slang knows about the objects in the Mocha context, so that for example
if P is a module and you write
Q = P;
then Q becomes the same module as P. There are two assignment
operators in slang: = and :=. The assignment Q =
P gives an error if Q is already defined; the assignment
Q := P does not.
Datatypes and operators
Aside from all the types known to the Mocha context (such as modules, rules,
invariants, etc), slang knows about additional datatypes.
Integers
Slang knows what integers are, and it knows how to do arithmetic operations
(+,,*,/) and comparisons (<,>,==,<=,>=,!=)
between them. Integers are also used to index arrays.
Boolean values are represented as integers; 0 is false, 1 is
true. A test (like if (x) then) passes if the test expression
has nonzero value, similarly in C. The operators &&,,
and ~ stand for and, or, not, respectively; boolean expressions
are evaluated as in java, in fixed lefttoright order between operators
of same precedence, terminating as soon as the value can be decided. For
example, in
if (cat && dog(4) )
the function call dog(4) is executed only if cat is nonzero.
Strings
A string looks like "this". For the moment, there's no way to
embed carriage returns or tabs into strings. If you really want this, then
you could modify the class ASTStringConstant.java.
Arrays
Slang implements singledimensional arrays. They grow dynamically, and
you can set pointblank
duck[5] = "mole"
but watch out: if you later do
b := duck[3]
then Slang will complain that duck[3] has not been initialized.
The predefined function size returns the size of an array; if
the size is n, then the elements are numbered 1,...,n1.
MDDs
Slang allows the manipulation of MDD's for symbolic modelchecking.
MDD's can be generated using the constants oneMdd and zeroMdd,
and the predefined symbolic functions.
Functions
Functions are firstorder objects in slang. You can use them in assignments,
have functions as elements of arrays, etc.
Operator precedence
The precedence of the various operators is the same as in Java.
Comments
Comments can appear at any point, and they are treated like white space.
There are:

Single line comments, introduced by // or ;

Multiline comments, enclosed in a /* ... */ pair.
Such comments cannot be nested.
Commands
The compilation unit of Slang is a command. Commands can be concatenated
by simply writing them one after the other; the command are generally terminated
by a semicolon (see the grammar for the details).
The commands are as follows.
Conditional and iterative commands
Commands for ifthenelse, while, and repeat are available; they work as
usual.
Function definition and call
Functions are defined using the def command, as follows:
def f(x) { print (x+1); }
The function above prints the successor of an integer. To return a value,
you can use the return command. The following example defines
three functions: a function g that increments an integer, a function
apply that applies a function to each element of an array, and
a function f that increments by 1 all the elements of an array.
def g(x) { return(x+1); }
def apply(f,x) {
i = 0;
while (i < size(x)) {
y[i] = f(x[i]);
i := i + 1;
}
return(y);
}
def f(x) { return (apply (g,x)); }
If we define a function with return arguments, as in
def g(x) { print(x+1) ; return(x+1); }
then we can either call the function in an expression, as in
y = g(3);
or we can call it as a command, in which case the return value is lost
(but not the side effects).
g(5);
Note that the return command can be used in any point of a function,
and not only as the last command. As an example, here's a function that
returns 1 if the argument is a prime number, and 0 otherwise.
def isprime(n)
{
if (n < 2) {
return(0);
}
p := 2;
repeat {
q := n / p;
if (n == p * q) return(0); // is not a prime
if (p == 2) p := 3; else p := p + 2;
} while (q > p);
return(1); // is a prime
}
The command return() is equivalent to return(0).
Block command
Any block of code can be enclosed between matching {, }.
Source command
Slang has a command to source (parse) a file. Note that sourcing a file
is different from including it: the sourced file must be a selfenclosed
compilation unit (a command, or a sequence of commands). For example, if
the declaration of the function isprime is in file primecheck.slang,
the following Slang code will source it, and define a function that hunts
for prime numbers:
source("primecheck.slang");
def primehunt(n,m)
{
j = 0;
while (j < m) {
if (isprime(n+j)) print (n+j);
j := j + 1;
}
}
The source command can be used recursively.
Null command
The null command doesn't do anything, and its only purpose is to keep Slang
from complaining when typing extra semicolons.
Scope
Slang maintains a stack of contexts. The top context is the Mocha context,
and each level of recursion in function declaration or call corresponds
to a context below the top one. The current context is hence always the
bottom one. Whenever Slang needs to look up a name in the stack of contexts,
Slang uses the following rules:

If the name appears on the right hand side of an assignment, or in general,
if the name corresponds to something that must be read by Slang
(such as the value of a variable, or a function being called), then Slang
looks up the name in all contexts, starting from the bottom one, and going
upwards until the name is found. For example, the following piece of code
will print out the answer 10:
a = 7;
def f(x) { print (x+a); }
f(3);
In f, the value of a is looked up first in the bottom
context, where it is not found, and then in the top context, where it is
found and where it has associated the value 7.
If the name appears on the left hand side of an assignment, then Slang
looks up the name in the current (bottom) context only. Hence, the following
piece of code will print out 12.
b = 12;
def f(x) { b = 5; }
f(3);
print(b);
Predefined Functions
Slang comes with several predefined functions implementing symbolic operators
for modelchecking. More functions can be defined, as explained below.
General Functions

print is a function that gets a variablelength list of arguments,
and prints them.

size is a function that returns the size of a Slang array.

help is a function that gets a builtin command name as an argument
and returns help information on it.
Operators on Modules
Slang provides the following functions to access syntactic features
of modules:

get_vars takes a module expression P and an integer i in
the range 04 and returns a SlangArray consisting of String names for
variables in the module P. The interpretation is as follows:

If i=0, then get_vars returns a list containing all variables.

If i=1, then get_vars returns a list containing all controlled variables.

If i=2, then get_vars returns a list containing all interface variables.

If i=3, then get_vars returns a list containing all private variables.

If i=4, then get_vars returns a list containing all external variables.
Note that using the function interface of slang, one may define more meaningful
names. For example,
def getControlledVars(M) {
return (get_vars(M,1));
}
may be used as a function to return all controlled variables.
Symbolic Operators
Slang implements symbolic operators on modules to enable MDD based symbolic
model checking. Only the basic operators predecessor, successor, conjunction,
disjunction, set difference, and emptiness check are provided. Using these,
and the control structures provided by Slang, symbolic model checking for
mucalculus is possible. The following functions are available.

and takes two MDD's and returns an MDD representing the conjunction.

or takes two MDD's and returns an MDD representing the disjunction.

not takes an MDD and returns an MDD representing the negation of the MDD.

implies takes two MDD's and returns an MDD representing the disjunction.

diff takes two MDD's m1 and m2 and returns an MDD corresponding
to m1 \ m2.

empty takes an MDD and returns a boolean. empty(m) is true iff
m represents the empty set. This means m = zeroMdd.

incl takes two MDD's and returns a boolean. incl(m1,m2) is true iff the
onset of m1 is a subset of the onset of m2.

equal takes two MDD's and returns a boolean. equal(m1,m2) is true iff m1
and m2 represent the same function.
Besides providing symbolic operators on MDD data structures, Slang provides
essential functions for symbolic model checking of transition systems.

pre takes a ModuleExpression and an MDD and returns the predecessor
MDD of the region represented by the MDD.

post takes a ModuleExpression and an MDD and returns the successor
MDD of the region represented by the MDD.

upre takes a ModuleExpression and an MDD and returns the uncontrollable predecessor MDD of the region represented by the MDD.

init_reg takes a ModuleExpression and returns the initial region
of the ModuleExpression as an MDD.

create_mdd takes a ModuleExpression and a region expression, and
returns an MDD corresponding to the region expression.

get_trans takes a ModuleExpression and returns the transition relation
of the ModuleExpression as an MDD.

pre_reg takes a ModuleExpression and a Mocha Expression and returns
an MDD corresponding to the predecessor of the region represented by the
Expression.

post_reg takes a ModuleExpression and a Mocha Expression and returns
an MDD corresponding to the successor of the region represented by the
Expression.

erase_vars takes a ModuleExpression M and a list of
(primed or unprimed) variables V (as a SlangArray of Strings) and returns
the transition relation of the module with the variables in V erased (quantified).
Thus, it creates an abstraction of the original module. Such abstractions
may then be used to perform abstract model checking.
The following symbolic model checking procedures are available as built
in functions in slang:

inv_check takes a ModuleExpression M and a state invariant expression I,
and performs symbolic forward reachability on the module M to check if
the state invariant I holds at all reachable states.

transinv_check takes a ModuleExpression M and a transition invariant expression
I, and performs symbolic forward reachability on the module M to check
if the transition invariant I holds at all pairs of reachable states.

ref_check takes two ModuleExpressions Spec and Impl and checks if Impl
refines Spec.
The symbolic interface of Slang is very powerful and allows the user to
combine several symbolic analyses efficiently. For example, using the primitive
symbolic operators, one may define the following procedure for getting
the reach set MDD of a module:
def reach(M) {
a := init_reg(M);
b := zeroMdd;
c:= zeroMdd;
while(!incl(a,b)) {
b := a;
c:=post(M,a);
a := or(a, c);
}
return (b);
}
While this may easily be modified to produce an invariant check script,
we recommend using the builtin
inv_check routine for efficiency reasons. Note that the above routine
may be easily changed to produce a routine that computes the backward reachable
states from a region.
However, the power comes at an expense: the user is responsible to ensure
the operations actually make sense. For example, if there are two modules
P and Q with disjoint variable sets, then the MDD for the initial region
of P does not make sense in the context of Q, and any operation involving
this MDD in Q may result in unexpected errors.
Calling Slang on a stream
First, to use Slang you need an instance object of the Slang class; you
can get one by, for example, Slang sl = new Slang();. The Slang
class has two methods to parse a stream: parse and parseIn.
The first method parses any stream; the second method parses standard input.
If you are using the Mocha GUI, then Slang can be instantiated from
the GUI by pressing the Shell button in the Check menu. The shell accepts
all valid input to Slang. To enter multiline input, use a '\' to end each
line.
Use the source command
source("filename");
to read in Slang scripts you may have written.
Extending Slang with New Functions
Slang can be extended with additional functions, to perform verificationrelated
tasks such as computation of Pre, Post, composing modules, computing sets
of reachable states, etc. To add a function to Slang, we must define a
new class that implements the interface SlangCommand. The print
and size functions are implemented by the classes SlangBIPrint
and SlangBISizeOf, look at them to see how they are coded.
As defined in the interface SlangCommand, the eval
method of the classes implementing the SlangCommand interface
is what actually does the job of computing a value (or doing something)
from the arguments. The method eval gets a vector of parameters,
and a stream on which optionally to print output. The vector is a Java
vector containing either objects that are in MochaContext (rules, modules,
invariants, etc) or objects that are instances of the classes SlangInt,
SlangArray, SlangProc, SlangStr, that extend
SlangObject. Two exceptions enable to return a value, and to declare
an error. Throw the latter with a string indicating the error; Slang will
add to the string an indication of where (line and column) the error occurred.
Once a class extending SlangCommand has been defined, to let
Slang know about the new function we must instantiate objects of these
classes, and pass these objects to Slang. If sl is an object of
class Slang, this can be done as follows:
SlangCmnd printFunction = (SlangCmnd) new SlangBIPrint();
SlangCmnd sizeFunction = (SlangCmnd) new SlangBISizeOf();
sl.addCommand("print", 1, printFunction);
sl.addCommand("size", 1, sizeFunction);
For the explanation of the arguments, see Slang.java.
Example
As an example of how Slang may be used in practice, we illustrate a model
checking session using the reactive modules description of the Peterson's
mutual exclusion protocol. The reactive module description is given by
the following code:
/*
* This is an implementation in reactive modules
* of the Peterson mutual exclusion algorithm.
*/
/*
* Type declarations.
*/
type ctype is { outCS, reqCS, inCS } // end of line comment
/*
* Atomic modules.
*/
// First module competing for the critical section.
module P1 /* inline comment */ is
interface x1:bool; pc1:ctype;
external x2:bool; pc2:ctype;
lazy atom A1 controls pc1,x1 reads pc1,pc2,x1,x2 /* comment */
init
[] true > pc1' := outCS; x1' := nondet;
update
[] pc1 = outCS > pc1' := reqCS; x1' := x2;
[] (pc1 = reqCS) & ((pc2 = outCS)  ~(x1 = x2)) > pc1' := inCS;
[] (pc1 = inCS) > pc1' := outCS;
// Second module competeing for the critical section.
module P2 is
interface pc2:ctype; x2:bool;
external pc1:ctype; x1:bool;
lazy atom A2 controls pc2,x2 reads pc1,pc2,x1,x2
init
[] true > pc2':= outCS; x2' := nondet;
update
[] (pc2 = outCS) > pc2':=reqCS; x2':= (x1 ~= true);
[] (pc2 = reqCS) & ((pc1 = outCS)  (x1=x2)) > pc2':=inCS;
[] (pc2 = inCS) > pc2':=outCS;
interface flag:bool;
external pc1:ctype;
atom A3 controls flag reads pc1
init
[] true > flag' := true;
update
[] (pc1 ~= inCS) > flag' := true;
/*
* Composed modules.
*/
module Pete is P1  P2
module Peter is Pete  I
module CPeter is I  Pete
/*
* Invariant declarations.
*/
invariant mutex is ~((pc1 = inCS) & (pc2 = inCS))
invariant request is (pc1 = reqCS)
invariant grant is (pc1 = inCS)
Open the project pete.rm using the Open Project Action in the Files menu.
Open a Shell window using the Shell action in the Check menu.
First we want to check if the state invariant mutex holds. To check
this, we use the slang command:
mocha: inv_check(Pete, mutex);
The invariant checker runs and returns that the invariant is indeed true.
We may also want to check if the
refinement relation Pete < Peter holds. To do this we do
mocha: ref_check(Pete, Peter);
Again, we find that a refinement relation holds.
The other property of interest for the mutual exclusion protocol is
response: a module that wants to get into the critical section can eventually
enter the critical section. This formula is written in LTL as
G( ( pc1 = reqCS ) => F ( pc1 = inCS ) ). While Mocha does not provide
a direct method to model check this property, one may write a Slang script
to compute this condition using the primitive symbolic operators.
This script is provided in the mcscript library in the distribution.
To load the response function, load the script response.slang:
mocha: source("mcscript/response.slang");
(You may need to give the correct path name for slang to find the file).
Now invoke the script using:
mocha: result:= response(Pete, request, grant); print(result);
Mocha prints 1 (for true): the requirement is indeed satisfied for the
module Pete.