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 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.

print?

Grammar:

constant: INT | 'null' | '{' (constant (',' constant)*)? '}'

string: '"' .* '"'

type: 'int' | 'proc' | type[]

typedvar: type ID

paramdecl: 'param' typedvar ('=' constant)? ';'

vardecl: 'var' typedvar ';'

formallist: typedvar (',' typedvar)*

function: 'fun' type ID '(' formallist? ')' '{' (typedvar ';')* transition* '}'

transition: (ID ':')? ('when' expr)? action ('goto' ID ';')?
// if label is missing, location will be created anyway with some ID number
// if when is missing, guard is 1 (true)
// if goto is missing, goto the next statement

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*

Example:

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