CIVLite: is an experimental light-weight model checking language and tool. Emphasis on performance and parallelization (using C11 threads?).

Types are: ints, proc, string, and arrays of any type.

Identifiers all start with %.

No boolean type. Instead, int is used. 0 is false, every other int is true (like C).

Parameters have a value that is fixed for the lifetime of the program. They don't go in the state. They can be hard coded into the program, or set on command line, like CIVL's $input variables.

There is a global scope and a local scope for each function. That's it.

No need to "declare" a function before it is used. There is no notion of a function declaration.

Grammar:

constant: INT | 'null'
string: '"' .* '"'
type: 'int' | 'proc' | 'string' | type[]
typedvar: type ID
paramdecl: 'param' typedvar ('=' expr)? ';'
vardecl: typedvar ';'
formallst: typedvar (',' typedvar)*
function: (type | 'void') ID '(' formallst? ')' '{' (typedvar ';')* labelnode* label? '}'
label: ID ':'
labelnode: label? node
node: transition | block
transition: action ('goto' ID)? ';'
block: 'choose' '{' guardedaction+ '}'
guardedaction: (expr | 'else') '->' transition
action : 'noop' |  'begin_atomic' | 'end_atomic' | assign | call | spawn
       | return | wait | assert | print
assign: lval '=' expr
call: (lval '=')? call ID '(' exprlst? ')'
spawn: (lval '=')? 'spawn' ID '(' exprlst? ')'
return: 'return' expr?
wait : 'wait' expr
assert: 'assert' expr
print: 'print' exprlst
exprlst: expr (',' expr)*
lval: ID | lval '[' expr ']' 
binop: 'add' | 'sub' | 'mul' | 'div' | 'mod' | 'eq' | 'neq' | 'lt' | 'lte' | 'and' | 'or'
unop: 'neg' | 'not'
expr: lval | constant | string
  | unop '(' expr ')'
  | binop '(' expr ',' expr ')'
  | 'ite' '(' expr ',' expr ',' expr ')'
  | '(' type ')' 'array' '(' expr ',' expr ')' // (T[])array(length, value)
  | '(' type ')' '{' (expr (',' expr)*)? '}' // (T[]){x1, ..., xn}

program: paramdecl* vardecl* function*

Array example:

int[][] %zero2d(int %n, int %m) {
  int[][] %a;
  %a = (int[][])array(%n, (int[])array(%m, 0));
  return %a;
}

Example:

void %thread(int %tid) {
  print "Hello from thread ", %tid, "\n";
}
void %main() {
  proc %p1;
  proc %p2;
  %p1 = spawn %thread(1);
  %p2 = spawn %thread(2);
  wait %p1;
  wait %p2;
  print "Done.\n";
}

Example (2-thread barrier):

int %s0 = 0;
int %s1 = 0;

void %t0() {
  print "t0 is before the barrier\n";
  %s0 = 1;
  choose {
    %s1 -> %s1 = 0;
  }
  print "t0 is after the barrier\n";
}

void %t1() {
  print "t1 is before the barrier\n";
  choose {
    %s0 -> %s0 = 0;
  }
  %s1 = 1;
  print "t1 is after the barrier\n";
}

void %main() {
  proc %p0;
  proc %p1;
  %p0 = spawn t0();
  %p1 = spawn t1();
  wait %p0;
  wait %p1;
}

Translation of

if (x>0) {
  y=1;
  z=2;
} else {
  y=0;
  z=3;
}

int %x;
int %y;
void %main() {
  choose {
    lt(0,%x) -> noop;
    else -> noop goto @L1;
  }
  %y=1;
  %z=2 goto @L2;
@L1:
  %y=0;
  %z=3;
@L2:
}

Source Information

Source information goes in a separate meta-data file. The tokens correspond 1-1 with the tokens in the code source file. Example:

Code:

%x[%i]=17;
%y=0;

Tokens are:

%x [ %i ] = 17 ; %y = 0 ;

Meta-data file looks something like this:

1:345  1:346  1:347  1:348  1:349  1:440  1:441 1:442 1:443  1:444  1:445

The structure 1:345 indicates "file 1, token 345".