Slang: the Script LANGuage

Slang is an interpreted imperative language, with run-time 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 non-zero value, similarly in C. The operators &&,||, and ~ stand for and, or, not, respectively; boolean expressions are evaluated as in java, in fixed left-to-right 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 non-zero.

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 single-dimensional arrays. They grow dynamically, and you can set point-blank

 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 pre-defined function size returns the size of an array; if the size is n, then the elements are numbered 1,...,n-1.

MDDs

Slang allows the manipulation of MDD's for symbolic model-checking. MDD's can be generated using the constants oneMdd and zeroMdd, and the predefined symbolic functions.

Functions

Functions are first-order 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 --;
Multi-line 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 if-then-else, 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 self-enclosed 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);

f

a

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 model-checking. More functions can be defined, as explained below.

General Functions

print is a function that gets a variable-length 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 built-in 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 0--4 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.

    def getControlledVars(M) {

        return (get_vars(M,1));

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 mu-calculus 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 verification-related 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.