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

Types are: ints, proc, 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' | type[]
typedvar: type ID
paramdecl: 'param' typedvar ('=' expr)? ';'
vardecl: typedvar ';'
formallist: typedvar (',' typedvar)*
function: (type | 'void') ID '(' formallist? ')' '{' (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
invocation: ID '(' exprlist? ')'
call: (lval '=')? 'call' invocation
spawn: (lval '=')? 'spawn' invocation
return: 'return' expr?
wait : 'wait' expr
assert: 'assert' expr
print: 'print' exprstrlst
exprstrlst: exprstr (',' exprstr)*
exprstr: expr | string
exprlist: expr (',' expr)*
lval: ID | lval '[' expr ']' 

expr: lval | constant | '(' expr ')' | expr '+' expr | ... // + - * / mod  - == != >= > < <= && || !
  | '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 {
    %x>0 -> noop;
    else -> noop goto @L1;
  }
  %y=1;
  %z=2 goto @L2;
@L1:
  %y=0;
  %z=3;
@L2:
}