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:

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:

Predefined Functions

Slang comes with several predefined functions implementing symbolic operators for model-checking. More functions can be defined, as explained below.

General Functions

Operators on Modules

Slang provides the following functions to access syntactic features of modules:

 

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.

Besides providing symbolic operators on MDD data structures, Slang provides essential functions for symbolic model checking of transition systems. The following symbolic model checking procedures are available as built in functions in slang: 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: 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: 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.