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 ';')* transition* '}'

// OOPS I messed this up.   Need to have multiple transitions departing from
// one location....


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*
}}}

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

Example: two threads are generated and go through a barrier:
{{{
int %s[];
fun void %thread(int %id) {
  print "Hello from thread ", %id, "\n";
  when %id==0 %s[0]=1; goto L1;
  
}
}}}