Changes between Initial Version and Version 1 of CIVLite

Timestamp:

09/21/23 07:30:59 (3 years ago)

Author:

siegel

Comment:

--

CIVLite

@@ +1 @@
+
+CIVLite: is an experimental light-weight model checking language and tool.
+
+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* '}'
+
+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
+
+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' ';'
+
+exprlist: expr (',' expr)*
+
+lval: ID | lval '[' expr ']' 
+
+expr: lval | constant | '(' expr ')' | expr '+' expr | ...
+ // operators: + - * / mod  - == != >= > < <= && || !
+
+program: paramdecl* vardecl* function*
+
+
+}}}