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' | '{' (constant (',' constant)*)? '}'
string: '"' .* '"'
type: 'int' | 'proc' | type[] | 'void'
typedvar: type ID
paramdecl: 'param' typedvar ('=' constant)? ';'
vardecl: 'var' typedvar ';'
formallist: typedvar (',' typedvar)*
function: 'fun' type ID '(' formallist? ')' '{' (typedvar ';')* labelnode* '}'
labelnode: (ID ':')? node
node: transition ('or' transition)* // multiple transitions may depart a node
transition: ((expr | 'else') '->')? action ('goto' ID ';')?
// if guard is missing, guard is 1 (true)
// else guard holds when all other guards are false
// if goto is missing, goto the next location
action: assignment call spawn noop return wait begin_atomic end_atomic assertion print
assignment: lval '=' expr ';'
invocation: ID '(' exprlist? ')'
call: (lval '=')? 'call' invocation ';'
spawn: (lval '=')? 'spawn' invocation ';'
noop: ';'
return: 'return' expr? ';'
wait : 'wait' expr ';'
begin_atomic: 'begin_atomic' ';'
end_atomic: 'end_atomic' ';'
assertion: '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  - == != >= > < <= && || !
  | 'array' '(' type ',' expr ',' expr ')' // array(element-type, length, value)

program: paramdecl* vardecl* function*

Array example:

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

Example:

fun void %thread(int %tid) {
  print "Hello from thread ", %tid, "\n";
}
fun 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;

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

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

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