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.

Grammar:

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

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

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 ';'

exprlist: expr (',' expr)*

lval: ID | lval '[' expr ']' 

expr: lval | constant | '(' expr ')' | expr '+' expr | ...
 // operators: + - * / mod  - == != >= > < <= && || !

program: paramdecl* vardecl* function*