modifications made to promela_yacc

8 files changed, 228 insertions, 1001 deletions

diff --git a/formal/promela/src/src/modules/promela_yacc/.gitignore b/formal/promela/src/src/modules/promela_yacc/.gitignore
deleted file mode 100644
index f4cd3f85..00000000
--- a/formal/promela/src/src/modules/promela_yacc/.gitignore
+++ /dev/null
@@ -1,20 +0,0 @@
-build/*
-dist/*
-promela/_version.py
-*parsetab.py
-.coverage
-.DS_Store
-Icon?
-
-*.*~
-__pycache__
-*.pyc
-*.swp
-*.pdf
-*.PDF
-*.txt
-*.log
-*.egg-info
-*.html
-*.css
-
diff --git a/formal/promela/src/src/modules/promela_yacc/LICENSE b/formal/promela/src/src/modules/promela_yacc/LICENSE
index bebe3694..40f0a792 100644
--- a/formal/promela/src/src/modules/promela_yacc/LICENSE
+++ b/formal/promela/src/src/modules/promela_yacc/LICENSE
@@ -1,3 +1,4 @@
+Copyright (c) 2019-2021 by Trinity College Dublin, Ireland
 Copyright (c) 2014-2018 by California Institute of Technology
 Copyright (c) 2014-2018 by Ioannis Filippidis
 All rights reserved.
diff --git a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in b/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
deleted file mode 100644
index bbacf5bf..00000000
--- a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
+++ /dev/null
@@ -1,4 +0,0 @@
-include tests/*.py
-include README.md
-include LICENSE
-include doc.md
diff --git a/formal/promela/src/src/modules/promela_yacc/doc.md b/formal/promela/src/src/modules/promela_yacc/doc.md
deleted file mode 100644
index 02d73431..00000000
--- a/formal/promela/src/src/modules/promela_yacc/doc.md
+++ /dev/null
@@ -1,100 +0,0 @@
-This package provides a lexer, parser, and abstract syntax tree (AST) for the [Promela](http://en.wikipedia.org/wiki/Promela) modeling language.
-The lexer and parser are generated using [PLY](https://pypi.python.org/pypi/ply/3.4) (Python `lex`-`yacc`).
-The [grammar](http://spinroot.com/spin/Man/grammar.html) is based on that used in the [SPIN](http://spinroot.com/spin/whatispin.html) model checker (in the files `spin.y` and `spinlex.c` of SPIN's source distribution), with modifications where needed.
-
-To instantiate a Promela parser:
-
-```python
-from promela.yacc import Parser
-parser = Parser()
-```
-
-Then Promela code, as a string, can be parsed by:
-
-```python
-s = '''
-active proctype foo(){
-	int x;
-	do
-	:: x = x + 1;
-	od
-}
-'''
-program = parser.parse(s)
-```
-
-then
-
-```python
->>> print(program)
-active [1]  proctype foo(){
-	int x
-	do
-	:: x = (x + 1)
-	od;
-}
-```
-
-The parser returns the result as an abstract syntax tree using classes from the `promela.ast` module.
-The top production rule returns a `Program` instance, which itself is a `list`.
-The contents of this list
-
-There are two categories of AST classes: those that represent control flow constructs:
-
-- `Proctype`, (`Init`, `NeverClaim`), `Node`, (`Expression`, `Assignment`, `Assert`, `Options` (if, do), `Else`, `Break`, `Goto`, `Label`, `Call`, `Return`, `Run`), `Sequence`
-
-and those that represent only syntax inside an expression:
-
-- `Terminal`, (`VarRef`, `Integer`, `Bool`), `Operator`, (`Binary`, `Unary`)
-
-The classes in parentheses are subclasses of the last class preceding the parentheses.
-Each control flow class has a method `to_pg` that recursively converts the abstract syntax tree to a program graph.
-
-A program graph is a directed graph whose edges are labeled with statements from the program.
-Nodes represent states of the program.
-Note the difference with a control flow graph, whose nodes are program statements and edges are program states.
-AST node classes correspond to nodes of the control flow graph and edges of the program graph (possibly with branching).
-
-For some node classes like `Expression` and `Assignment`, the `to_pg` method returns themselves, a.
-Almost all statements are represented as either an `Expression` or an `Assignment`.
-These label edges in the program graph, using the edge attribute `"stmt"`.
-
-The program graph is represented as a [multi-digraph](http://en.wikipedia.org/wiki/Multigraph) using [`networkx.MultiDiGraph`](https://networkx.github.io/documentation/latest/reference/classes.multidigraph.html).
-A multi-digraph is necessary, because two nodes in the program graph may be connected by two edges, each edge labeled with a different statement.
-For example, this is the case in the code fragment:
-
-```promela
-bit x;
-do
-:: x == 0
-:: x == 1
-od
-```
-
-The above defines a program graph with a single node and two self-loops, one labeled with the statement `x == 0` and another with the statement `x == 1`.
-These two statements here are guards, so they only determine whether the edge can be traversed, without affecting the program's data state (variable values).
-
-Program graph nodes are labeled with a `"context"` attribute that can take the values:
-- `"atomic"`
-- `"d_step"`
-- `None`
-The values `"atomic"` and `"d_step"` signify that the state is inside an atomic or deterministic step block.
-
-Continuing our earlier example:
-
-```python
->>> g = program[0].to_pg()
->>> g.nodes(data=True)
-[(0, {'context': None}), (1, {'context': None})]
->>> g.edges(data=True)
-[(0, 1, {'stmt': Assignment(
-    VarRef('x', None, None),
-    Expression(
-        Operator('+',
-            VarRef('x', None, None),
-            Integer('1'))))}),
- (1, 0, {'stmt': Expression(
-    Operator('==',
-        VarRef('x', None, None),
-        Integer('2')))})]
-```
diff --git a/formal/promela/src/src/modules/promela_yacc/promela/ast.py b/formal/promela/src/src/modules/promela_yacc/promela/ast.py
index 16baaa05..77db1fe9 100644
--- a/formal/promela/src/src/modules/promela_yacc/promela/ast.py
+++ b/formal/promela/src/src/modules/promela_yacc/promela/ast.py
@@ -48,19 +48,20 @@ def to_str(x):
 class Proctype(object):
     def __init__(self, name, body, args=None,
                  active=None, d_proc=False,
-                 priority=None, provided=None):
+                 priority=None, provided=None,
+                 disable_negation=False):
         self.name = name
         self.body = body
         self.args = args
         if active is None:
             active = 0
-        else:
-            active = int(active.value)
+        self.d_proc = d_proc
         if priority is not None:
             priority = int(priority.value)
         self.active = active
         self.priority = priority
         self.provided = provided
+        self.disable_negation = disable_negation
 
     def __str__(self):
         return "Proctype('{name}')".format(name=self.name)
@@ -86,7 +87,7 @@ class Proctype(object):
         if self.args is None:
             args = ''
         else:
-            args = to_str(self.args)
+            args = '; '.join(to_str(xx) for x in self.args for xx in x)
         return args
 
     def to_pg(self, syntactic_else=False):
@@ -223,7 +224,7 @@ class Init(Proctype):
 
 class Program(list):
     def __str__(self):
-        return '\n'.join(to_str(x) for x in self)
+        return '\n'.join(to_str(x) for x, _ in self)
 
     def __repr__(self):
         c = super(Program, self).__repr__()
@@ -245,21 +246,25 @@ class Program(list):
 class LTL(object):
     """Used to mark strings as LTL blocks."""
 
-    def __init__(self, formula):
+    def __init__(self, formula, name = None):
         self.formula = formula
+        self.name = name
 
     def __repr__(self):
         return 'LTL({f})'.format(f=repr(self.formula))
 
     def __str__(self):
-        return 'ltl {' + str(self.formula) + '}'
+        return 'ltl ' + (self.name + ' ' if self.name else '') + '{' + str(self.formula) + '}'
 
 
 class Sequence(list):
-    def __init__(self, iterable, context=None, is_option=False):
+    def __init__(self, iterable, context=None, context_for_var=None, context_for_begin=None, context_for_end=None, is_option=False):
         super(Sequence, self).__init__(iterable)
-        # "atomic" or "dstep"
+        # "for" or "atomic" or "dstep"
         self.context = context
+        self.context_for_var = context_for_var
+        self.context_for_begin = context_for_begin
+        self.context_for_end = context_for_end
         self.is_option = is_option
 
     def to_str(self):
@@ -267,20 +272,22 @@ class Sequence(list):
             return '\n'.join(to_str(x) for x in self)
         else:
             return (
-                self.context + '{\n' +
-                _indent(to_str(self)) + '\n}\n')
+                self.context +
+                (' (' + self.context_for_var + ' : ' + to_str (self.context_for_begin) + ' .. ' + to_str (self.context_for_end) + ') ' if self.context == 'for' else '') +
+                '{\n' +
+                '\n'.join(_indent(to_str(x)) for x in self) + '\n}\n')
 
     def __repr__(self):
         l = super(Sequence, self).__repr__()
-        return 'Sequence({l}, context={c}, is_option={isopt})'.format(
-            l=l, c=self.context, isopt=self.is_option)
+        return 'Sequence({l}, context={c}, context_for_var={cfv}, context_for_begin={cfb}, context_for_end={cfe}, is_option={isopt})'.format(
+            l=l, c=self.context, cfv=self.context_for_var, cfb=self.context_for_begin, cfe=self.context_for_end, isopt=self.is_option)
 
     def to_pg(self, g, context=None, option_guard=None, **kw):
         # set context
         if context is None:
             context = self.context
         c = context
-        assert c in {'atomic', 'd_step', None}
+        assert c in {'atomic', 'd_step', None} # TODO: 'for'
         # atomic cannot appear inside d_step
         if context == 'd_step' and c == 'atomic':
             raise Exception('atomic inside d_step')
@@ -541,12 +548,13 @@ class VarDef(Node):
             assert isinstance(l, int), l
         self.length = l
         self.visible = visible
-        if bitwidth is not None:
-            self.bitwidth = int(bitwidth.value)
+        self.bitwidth = int(bitwidth.value) if bitwidth else None
         if vartype == 'bool':
             default_initval = Bool('false')
         else:
             default_initval = Integer('0')
+        self.msg_types = msg_types
+        self.initial_value0 = initval
         if initval is None:
             initval = Expression(default_initval)
         self.initial_value = initval
@@ -556,10 +564,13 @@ class VarDef(Node):
         return 'VarDef({t}, {v})'.format(t=self.type, v=self.name)
 
     def to_str(self):
-        s = '{type} {varname}{len}'.format(
+        s = '{type} {varname}{bitwidth}{len}{initval}{msg_types}'.format(
             type=self._type_str(),
             varname=self.name,
-            len='[{n}]'.format(n=self.len) if self.len else '')
+            bitwidth=' : {n}'.format(n =self.bitwidth) if self.bitwidth else '',
+            len=' [{n}]'.format(n=self.length) if self.length and not self.msg_types else '',
+            initval=' = {i}'.format(i=self.initial_value0) if self.initial_value0 else '',
+            msg_types=' = [{l}] of {{ {m} }}'.format(l=self.length, m=' , '.join(to_str(x) for x in self.msg_types)) if self.msg_types else '')
         return s
 
     def _type_str(self):
@@ -741,8 +752,8 @@ class TypeDef(Node):
         self.decls = decls
 
     def __str__(self):
-        return 'typedef {name} {\ndecls\n}'.format(
-            name=self.name, decls=to_str(self.decls))
+        return 'typedef {name} {{ {decls} }}'.format(
+            name=self.name, decls='; '.join(to_str(x) for x in self.decls))
 
     def exe(self, t):
         t.types[self.name] = self
@@ -752,8 +763,8 @@ class MessageType(Node):
     def __init__(self, values, visible=None):
         self.values = values
 
-    def __str__(self):
-        return 'mtype {{ {values} }}'.format(values=self.values)
+    def to_str(self):
+        return 'mtype = {{ {values} }}'.format(values=' , '.join(to_str(x) for x in self.values))
 
     def exe(self, t):
         t.types[self.name] = self
@@ -774,27 +785,40 @@ class Run(Node):
         self.priority = priority
 
     def __str__(self):
-        return 'run({f})'.format(f=self.func)
+        return 'run {f} ({args})'.format(f=self.func, args='' if self.args is None else ' , '.join(to_str(x) for x in self.args))
 
 
-class Inline(Node):
-    def __init__(self, name, args):
+class InlineDef(Node):
+    def __init__(self, name, decl, body, disable_negation=False):
         self.name = name
-        self.args = args
+        self.decl = decl
+        self.body = body
+        self.disable_negation = disable_negation
 
+    def __str__(self):
+        return ('inline {name} ({decl}) {{\n'
+                '{body}\n'
+                '}}\n\n').format(
+                    name = self.name,
+                    decl = ', '.join(to_str(x) for x in self.decl) if self.decl else '',
+                    body = _indent(to_str(self.body)))
 
 class Call(Node):
-    def __init__(self, func, args):
-        self.func = func
+    def __init__(self, name, args):
+        self.name = name
         self.args = args
 
+    def __str__(self):
+        return '{name} ({args})'.format(name = self.name, args = ', '.join(to_str(x) for x in self.args) if self.args else '')
+
 
 class Assert(Node):
-    def __init__(self, expr):
+    def __init__(self, expr, pos = None):
         self.expr = expr
+        self.pos = pos
 
-    def __repr__(self):
-        return 'assert({expr})'.format(expr=repr(self.expr))
+    def __str__(self):
+        return 'assert({expr})'.format(expr=to_str(self.expr))
 
 
 class Expression(Node):
@@ -872,32 +896,32 @@ class Assignment(Node):
 
 
 class Receive(Node):
-    def __init__(self, varref, args=None):
+    def __init__(self, varref, args):
         self.var = varref
         self.args = args
 
     def __str__(self):
         v = to_str(self.var)
-        return 'Rx({v})'.format(v=v)
+        return '{v} ? {args}'.format(v=v, args = ' , '.join(to_str(x) for x in self.args))
 
 
 class Send(Node):
-    def __init__(self, varref, args=None):
-        self.varref = varref
+    def __init__(self, varref, args):
+        self.var = varref
         self.args = args
 
     def __str__(self):
         v = to_str(self.var)
-        return 'Tx({v})'.format(v=v)
+        return '{v} ! {args}'.format(v=v, args = ' , '.join(to_str(x) for x in self.args))
 
 
 class Printf(Node):
-    def __init__(self, s, args):
+    def __init__(self, s, args=None):
         self.s = s
         self.args = args
 
     def __str__(self):
-        return 'printf()'.format(s=self.s, args=self.args)
+        return 'printf({s}{args})'.format(s=self.s, args='' if self.args is None else ' , ' + ' , '.join(to_str(x) for x in self.args))
 
 
 class Operator(object):
@@ -927,6 +951,14 @@ class Binary(Operator):
 class Unary(Operator):
     pass
 
+class ReceiveExpr(Node):
+    def __init__(self, varref, args):
+        self.var = varref
+        self.args = args
+
+    def __str__(self):
+        v = to_str(self.var)
+        return '({v} ? [{args}])'.format(v=v, args = ' , '.join(to_str(x) for x in self.args))
 
 class Terminal(object):
     def __init__(self, value):
@@ -967,7 +999,7 @@ class VarRef(Terminal):
         return '{name}{index}{ext}'.format(
             name=self.name,
             index=i,
-            ext='' if self.extension is None else self.extension)
+            ext=('.' + to_str(self.extension)) if self.extension else '' )
 
 
 class Integer(Terminal):
@@ -986,7 +1018,7 @@ class Bool(Terminal):
         return 'Bool({value})'.format(value=repr(self.value))
 
     def __str__(self):
-        return str(self.value)
+        return str('true' if self.value else 'false')
 
 
 class RemoteRef(Terminal):
@@ -1008,6 +1040,14 @@ class RemoteRef(Terminal):
             proc=self.proctype, inst=inst, label=self.label)
 
 
+class Timeout(Node):
+    def __init__(self):
+        return
+
+    def __str__(self):
+        return 'timeout'
+
+
 def dump_graph(g, fname='a.pdf', node_label='label',
                edge_label='label', relabel=False):
     """Write the program graph, annotated with formulae, to PDF file."""
diff --git a/formal/promela/src/src/modules/promela_yacc/promela/lex.py b/formal/promela/src/src/modules/promela_yacc/promela/lex.py
index cd3eafe0..e31a51c0 100644
--- a/formal/promela/src/src/modules/promela_yacc/promela/lex.py
+++ b/formal/promela/src/src/modules/promela_yacc/promela/lex.py
@@ -1,7 +1,7 @@
 """Lexer for Promela, using Python Lex-Yacc (PLY)."""
 import logging
 import ply.lex
-
+import re
 
 logger = logging.getLogger(__name__)
 
@@ -30,12 +30,14 @@ class Lexer(object):
         'enabled': 'ENABLED',
         'eval': 'EVAL',
         'fi': 'FI',
+        'for': 'FOR',
         'full': 'FULL',
         'get_priority': 'GET_P',
         'goto': 'GOTO',
         'hidden': 'HIDDEN',
         'if': 'IF',
         'init': 'INIT',
+        'inline': 'INLINE',
         'int': 'INT',
         'len': 'LEN',
         'local': 'ISLOCAL',
@@ -56,7 +58,7 @@ class Lexer(object):
         'return': 'RETURN',
         'run': 'RUN',
         'short': 'SHORT',
-        'skip': 'TRUE',
+        'skip': 'SKIP',
         'show': 'SHOW',
         'timeout': 'TIMEOUT',
         'typedef': 'TYPEDEF',
@@ -67,9 +69,9 @@ class Lexer(object):
         'xr': 'XR',
         'xs': 'XS',
         'W': 'WEAK_UNTIL'}
-    values = {'skip': 'true'}
+    values = {'': ''}
     delimiters = ['LPAREN', 'RPAREN', 'LBRACKET', 'RBRACKET',
-                  'LBRACE', 'RBRACE', 'COMMA', 'PERIOD',
+                  'LBRACE', 'RBRACE', 'COMMA', 'PERIODS', 'PERIOD',
                   'SEMI', 'COLONS', 'COLON', 'ELLIPSIS']
     # remember to check precedence
     operators = ['PLUS', 'INCR', 'MINUS', 'DECR', 'TIMES', 'DIVIDE',
@@ -159,6 +161,7 @@ class Lexer(object):
     t_LBRACE = r'\{'
     t_RBRACE = r'\}'
     t_COMMA = r','
+    t_PERIODS = r'\.\.'
     t_PERIOD = r'\.'
     t_SEMI = r';'
     t_COLONS = r'::'
@@ -184,6 +187,11 @@ class Lexer(object):
 
     t_INITIAL_ARROW = r'->'
 
+    def t_PREPROC_stdin(self, t):
+        r'\# .+ "<stdin>"[0-9 ]*' # WARNING: using '\d+' instead of '.+' does not necessarily result in the same matching
+        t.lexer.lineno = int (re.search (r'\# (\d+) "<stdin>"', t.value).group (1)) - 1
+        pass
+
     def t_PREPROC(self, t):
         r'\#.*'
         pass
@@ -204,7 +212,7 @@ class Lexer(object):
 
     def t_COMMENT(self, t):
         r' /\*(.|\n)*?\*/'
-        t.lineno += t.value.count('\n')
+        t.lexer.lineno += t.value.count('\n')
 
     def t_error(self, t):
         logger.error('Illegal character "{s}"'.format(s=t.value[0]))
diff --git a/formal/promela/src/src/modules/promela_yacc/promela/yacc.py b/formal/promela/src/src/modules/promela_yacc/promela/yacc.py
index d650c063..af96dc99 100644
--- a/formal/promela/src/src/modules/promela_yacc/promela/yacc.py
+++ b/formal/promela/src/src/modules/promela_yacc/promela/yacc.py
@@ -15,6 +15,7 @@ import os
 import subprocess
 import warnings
 import ply.yacc
+from sys import platform as _platform
 # inline
 #
 # import promela.ast as promela_ast
@@ -90,11 +91,11 @@ class Parser(object):
             debuglog=debuglog,
             errorlog=errorlog)
 
-    def parse(self, promela):
+    def parse(self, promela, fic):
         """Parse string of Promela code."""
-        s = cpp(promela)
+        s = cpp(promela, fic)
         program = self.parser.parse(
-            s, lexer=self.lexer.lexer, debug=self.logger)
+            s, lexer=self.lexer.lexer, debug=self.logger, tracking=True)
         return program
 
     def _iter(self, p):
@@ -115,6 +116,10 @@ class Parser(object):
         """program : units"""
         p[0] = self.ast.Program(p[1])
 
+    def p_program_empty(self, p):
+        """program : empty"""
+        p[0] = self.ast.Program([])
+
     def p_units_iter(self, p):
         """units : units unit"""
         p[0] = self._iter(p)
@@ -126,17 +131,18 @@ class Parser(object):
     # TODO: events, c_fcts, ns, error
     def p_unit_proc(self, p):
         """unit : proc
+                | inline
                 | init
                 | claim
                 | ltl
         """
-        p[0] = p[1]
+        p[0] = (p[1], p.lineno(1))
 
     def p_unit_decl(self, p):
         """unit : one_decl
                 | utype
         """
-        p[0] = p[1]
+        p[0] = (p[1], p.lineno(1))
 
     def p_unit_semi(self, p):
         """unit : semi"""
@@ -158,6 +164,13 @@ class Parser(object):
             name, body, args=args, priority=priority,
             provided=enabler, **inst)
 
+    def p_inline(self, p):
+        ("""inline : INLINE NAME"""
+         """         LPAREN var_list0 RPAREN"""
+         """         body
+         """)
+        p[0] = self.ast.InlineDef(name = p[2], decl = p[4], body = p[6])
+
     # instantiator
     def p_inst(self, p):
         """prefix_proctype : ACTIVE opt_index proctype"""
@@ -166,7 +179,7 @@ class Parser(object):
             n_active = self.ast.Integer('1')
         else:
             n_active = p[2]
-        d['active'] = n_active
+        d['active'] = int(n_active.value)
         p[0] = d
 
     def p_inactive_proctype(self, p):
@@ -197,7 +210,11 @@ class Parser(object):
         seq = self.ast.Sequence(p[4])
         p[0] = self.ast.TypeDef(p[2], seq)
 
-    def p_ltl(self, p):
+    def p_ltl1(self, p):
+        """ltl : LTL NAME LBRACE expr RBRACE"""
+        p[0] = self.ast.LTL(p[4], name = p[2])
+
+    def p_ltl2(self, p):
         """ltl : LTL LBRACE expr RBRACE"""
         p[0] = self.ast.LTL(p[3])
 
@@ -219,6 +236,21 @@ class Parser(object):
         """decl_lst : one_decl"""
         p[0] = [p[1]]
 
+    def p_decl0(self, p):
+        """decl0 : decl_lst0"""
+        p[0] = self.ast.Sequence(p[1])
+
+    def p_decl_empty0(self, p):
+        """decl0 : empty"""
+
+    def p_decl_lst_iter0(self, p):
+        """decl_lst0 : expr COMMA decl_lst0"""
+        p[0] = [p[1]] + p[3]
+
+    def p_decl_lst_end0(self, p):
+        """decl_lst0 : expr"""
+        p[0] = [p[1]]
+
     def p_one_decl_visible(self, p):
         """one_decl : vis typename var_list
                     | vis NAME var_list
@@ -251,7 +283,7 @@ class Parser(object):
 
     def p_one_decl_mtype(self, p):
         """one_decl : MTYPE asgn LBRACE name_list RBRACE"""
-        p[0] = self.ast.MessageType(p[3])
+        p[0] = self.ast.MessageType(p[4])
 
     def p_name_list_iter(self, p):
         """name_list : name_list COMMA NAME"""
@@ -270,8 +302,28 @@ class Parser(object):
         """var_list : ivar"""
         p[0] = [p[1]]
 
+    def p_var_list00_iter(self, p):
+        """var_list00 : ivar0 COMMA var_list00"""
+        p[0] = [p[1]] + p[3]
+
+    def p_var_list00_end(self, p):
+        """var_list00 : ivar0"""
+        p[0] = [p[1]]
+
+    def p_var_list0(self, p):
+        """var_list0 : var_list00"""
+        p[0] = p[1]
+
+    def p_var_list0_empty(self, p):
+        """var_list0 : empty"""
+        p[0] = []
+
     # TODO: vardcl asgn LBRACE c_list RBRACE
 
+    def p_ivar0(self, p):
+        """ivar0 : NAME"""
+        p[0] = p[1]
+
     # ivar = initialized variable
     def p_ivar(self, p):
         """ivar : vardcl"""
@@ -342,7 +394,7 @@ class Parser(object):
 
     def p_cmpnd_iter(self, p):
         """cmpnd : cmpnd PERIOD cmpnd %prec DOT"""
-        p[0] = self.ast.VarRef(extension=p[3], **p[1])
+        p[0] = self.ast.VarRef(extension=p[3], name = p[1].name, index = p[1].index)
 
     def p_cmpnd_end(self, p):
         """cmpnd : pfld"""
@@ -467,7 +519,7 @@ class Parser(object):
 
     def p_statement_assert(self, p):
         """statement : ASSERT full_expr"""
-        p[0] = self.ast.Assert(p[2])
+        p[0] = self.ast.Assert(p[2], pos = p.lineno(1))
 
     def p_statement_fifo_receive(self, p):
         """statement : varref RCV rargs"""
@@ -486,7 +538,7 @@ class Parser(object):
         p[0] = self.ast.Receive(p[1], p[4])
 
     def p_statement_tx2(self, p):
-        """statement : varref TX2 margs"""
+        """statement : varref TX2 rargs"""
         p[0] = self.ast.Send(p[1], p[3])
 
     def p_statement_full_expr(self, p):
@@ -497,6 +549,19 @@ class Parser(object):
         """statement : ELSE"""
         p[0] = self.ast.Else()
 
+    def p_statement_for(self, p):
+        """statement : for"""
+        p[0] = p[1]
+
+    def p_for(self, p):
+        """for : FOR LPAREN NAME COLON full_expr PERIODS full_expr RPAREN LBRACE sequence os RBRACE"""
+        s = p[10]
+        s.context = 'for'
+        s.context_for_var = p[3]
+        s.context_for_begin = p[5]
+        s.context_for_end = p[7]
+        p[0] = s
+
     def p_statement_atomic(self, p):
         """statement : atomic"""
         p[0] = p[1]
@@ -523,23 +588,27 @@ class Parser(object):
 
     # the stmt of line 696 in spin.y collects the inline ?
     def p_statement_call(self, p):
-        """statement : NAME LPAREN args RPAREN"""
+        """statement : NAME LPAREN decl0 RPAREN"""
         # NAME = INAME = inline
-        c = self.ast.Inline(p[1], p[3])
+        c = self.ast.Call(p[1], p[3])
         p[0] = self.ast.Sequence([c])
 
     def p_statement_assgn_call(self, p):
-        """statement : varref asgn NAME LPAREN args RPAREN statement"""
-        inline = self.ast.Inline(p[3], p[5])
+        """statement : varref asgn NAME LPAREN decl0 RPAREN statement"""
+        inline = self.ast.Call(p[3], p[5])
         p[0] = self.ast.Assignment(p[1], inline)
 
     def p_statement_return(self, p):
         """statement : RETURN full_expr"""
         p[0] = self.ast.Return(p[2])
 
-    def p_printf(self, p):
-        """statement : PRINT LPAREN STRING prargs RPAREN"""
-        p[0] = self.ast.Printf(p[3], p[4])
+    def p_printf1(self, p):
+        """statement : PRINT LPAREN STRING RPAREN"""
+        p[0] = self.ast.Printf(p[3])
+
+    def p_printf2(self, p):
+        """statement : PRINT LPAREN STRING COMMA decl0 RPAREN"""
+        p[0] = self.ast.Printf(p[3], p[5])
 
     # yet unimplemented for statement:
         # SET_P l_par two_args r_par
@@ -555,8 +624,8 @@ class Parser(object):
         p[0] = self.ast.Receive(p[1])
 
     def p_varref_lnot(self, p):
-        """special : varref LNOT margs"""
-        raise NotImplementedError
+        """special : varref LNOT rargs"""
+        p[0] = self.ast.Send(p[1], p[3])
 
     def p_break(self, p):
         """special : BREAK"""
@@ -609,17 +678,23 @@ class Parser(object):
         p[0] = self.ast.Expression(p[1])
 
     # probe expr = no negation allowed (positive)
-    def p_pexpr(self, p):
-        """pexpr : probe
-                 | LPAREN pexpr RPAREN
-                 | pexpr LAND pexpr
+    def p_pexpr_probe(self, p):
+        """pexpr : probe"""
+        p[0] = p[1]
+
+    def p_pexpr_paren(self, p):
+        """pexpr : LPAREN pexpr RPAREN"""
+        p[0] = p[2]
+
+    def p_pexpr_logical(self, p):
+        """pexpr : pexpr LAND pexpr
                  | pexpr LAND expr
                  | expr LAND pexpr
                  | pexpr LOR pexpr
                  | pexpr LOR expr
                  | expr LOR pexpr
         """
-        p[0] = 'pexpr'
+        p[0] = self.ast.Binary(p[2], p[1], p[3])
 
     def p_probe(self, p):
         """probe : FULL LPAREN varref RPAREN
@@ -627,7 +702,7 @@ class Parser(object):
                  | EMPTY LPAREN varref RPAREN
                  | NEMPTY LPAREN varref RPAREN
         """
-        p[0] = 'probe'
+        p[0] = self.ast.Call(p[1], self.ast.Sequence([p[3]]))
 
     def p_expr_paren(self, p):
         """expr : LPAREN expr RPAREN"""
@@ -676,8 +751,7 @@ class Parser(object):
         """expr : varref RCV LBRACKET rargs RBRACKET
                 | varref R_RCV LBRACKET rargs RBRACKET
         """
-        p[0] = p[1]
-        warnings.warn('not implemented')
+        p[0] = self.ast.ReceiveExpr(p[1], p[4])
 
     def p_expr_other(self, p):
         """expr : LPAREN expr ARROW expr COLON expr RPAREN
@@ -689,12 +763,15 @@ class Parser(object):
         warnings.warn('"{s}" not implemented'.format(s=p[1]))
 
     def p_expr_run(self, p):
-        """expr : RUN aname LPAREN args RPAREN opt_priority"""
+        """expr : RUN aname LPAREN decl0 RPAREN opt_priority"""
         p[0] = self.ast.Run(p[2], p[4], p[6])
 
+    def p_expr_other_1(self, p):
+        """expr : TIMEOUT"""
+        p[0] = self.ast.Timeout()
+
     def p_expr_other_2(self, p):
-        """expr : TIMEOUT
-                | NONPROGRESS
+        """expr : NONPROGRESS
                 | PC_VAL LPAREN expr RPAREN
         """
         raise NotImplementedError()
@@ -764,10 +841,10 @@ class Parser(object):
         p[0] = p[2]
 
     def p_const(self, p):
-        """const : boolean
+        """const : SKIP
+                 | boolean
                  | number
         """
-        # lex maps `skip` to `TRUE`
         p[0] = p[1]
 
     def p_bool(self, p):
@@ -783,47 +860,24 @@ class Parser(object):
     # Auxiliary
     # =========
 
-    def p_two_args(self, p):
-        """two_args : expr COMMA expr"""
-
-    def p_args(self, p):
-        """args : arg"""
-        p[0] = p[1]
-
-    def p_prargs(self, p):
-        """prargs : COMMA arg"""
-        p[0] = p[2]
-
-    def p_prargs_empty(self, p):
-        """prargs : empty"""
-
-    def p_args_empty(self, p):
-        """args : empty"""
-
-    def p_margs(self, p):
-        """margs : arg
-                 | expr LPAREN arg RPAREN
-        """
-
-    def p_arg(self, p):
-        """arg : expr
-               | expr COMMA arg
-        """
-        p[0] = 'arg'
-
     # TODO: CONST, MINUS CONST %prec UMIN
     def p_rarg(self, p):
-        """rarg : varref
+        """rarg : const
+                | varref
                 | EVAL LPAREN expr RPAREN
         """
-        p[0] = 'rarg'
+        # todo: support all cases
+        #       | rarg LPAREN rargs RPAREN
+        #       | LPAREN rargs RPAREN
+        p[0] = p[1]
 
-    def p_rargs(self, p):
-        """rargs : rarg
-                 | rarg COMMA rargs
-                 | rarg LPAREN rargs RPAREN
-                 | LPAREN rargs RPAREN
-        """
+    def p_rargs_iter(self, p):
+        """rargs : rarg COMMA rargs"""
+        p[0] = [p[1]] + p[3]
+
+    def p_rargs_end(self, p):
+        """rargs : rarg"""
+        p[0] = [p[1]]
 
     def p_proctype(self, p):
         """proctype : PROCTYPE
@@ -887,10 +941,14 @@ class Parser(object):
         raise Exception('syntax error at: {p}'.format(p=p))
 
 
-def cpp(s):
+def cpp(code, fic):
     """Call the C{C} preprocessor with input C{s}."""
     try:
-        p = subprocess.Popen(['cpp', '-E', '-x', 'c'],
+        if _platform == "darwin":
+            cppprog = 'clang'
+        else:
+            cppprog = 'cpp'
+        p = subprocess.Popen([cppprog, '-E', '-x', 'c', '-' if code is not None else fic], # NOTE: if code is empty, then '-' must be returned as well
                              stdin=subprocess.PIPE,
                              stdout=subprocess.PIPE,
                              stderr=subprocess.PIPE,
@@ -900,10 +958,13 @@ def cpp(s):
             raise Exception('C preprocessor (cpp) not found in path.')
         else:
             raise
-    logger.debug('cpp input:\n' + s)
-    stdout, stderr = p.communicate(s)
+    if code:
+        logger.debug('cpp input:\n' + code)
+    stdout, stderr = p.communicate(code)
     logger.debug('cpp returned: {c}'.format(c=p.returncode))
     logger.debug('cpp stdout:\n {out}'.format(out=stdout))
+    if p.returncode != 0:
+        raise Exception('C preprocessor return code: {returncode}'.format(returncode=p.returncode))
     return stdout
 
 
diff --git a/formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py b/formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py
deleted file mode 100644
index b26d22aa..00000000
--- a/formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py
+++ /dev/null
@@ -1,759 +0,0 @@
-import logging
-import networkx as nx
-import networkx.algorithms.isomorphism as iso
-from nose.tools import assert_raises
-from promela import ast, yacc
-
-
-logger = logging.getLogger(__name__)
-logger.setLevel('WARNING')
-log = logging.getLogger('promela.yacc')
-log.setLevel(logging.ERROR)
-h = logging.StreamHandler()
-log = logging.getLogger('promela.ast')
-log.setLevel('WARNING')
-log.addHandler(h)
-
-
-parser = yacc.Parser()
-
-
-def parse_proctype_test():
-    s = '''
-    active [3] proctype main(){
-        int x;
-    }
-    '''
-    tree = parser.parse(s)
-    assert isinstance(tree, ast.Program)
-    assert len(tree) == 1
-    p = tree[0]
-    assert isinstance(p, ast.Proctype)
-    assert p.name == 'main'
-    assert isinstance(p.body, ast.Sequence)
-    assert p.active == 3, type(p.active)
-    assert p.args is None
-    assert p.priority is None
-    assert p.provided is None
-
-
-def parse_if_test():
-    s = '''
-    proctype p (){
-        if
-        :: skip
-        fi
-    }
-    '''
-    tree = parser.parse(s)
-    assert isinstance(tree, ast.Program)
-    assert len(tree) == 1
-    proc = tree[0]
-    assert isinstance(proc, ast.Proctype)
-    assert isinstance(proc.body, ast.Sequence)
-    assert len(proc.body) == 1
-    if_block = proc.body[0]
-    assert isinstance(if_block, ast.Options)
-    assert if_block.type == 'if'
-    options = if_block.options
-    assert isinstance(options, list)
-    assert len(options) == 1
-    opt0 = options[0]
-    assert isinstance(opt0, ast.Sequence)
-    assert len(opt0) == 1
-    assert isinstance(opt0[0], ast.Expression)
-    e = opt0[0].expr
-    assert isinstance(e, ast.Bool)
-    assert e.value, e
-
-
-def parse_do_multiple_options_test():
-    s = '''
-    proctype p (){
-        do
-        :: x -> x = x + 1;
-        :: (y == 0) -> y = x; y == 1;
-        od
-    }
-    '''
-    tree = parser.parse(s)
-    assert isinstance(tree, ast.Program)
-    assert len(tree) == 1
-    proc = tree[0]
-    assert isinstance(proc, ast.Proctype)
-    assert isinstance(proc.body, ast.Sequence)
-    assert len(proc.body) == 1
-    do_block = proc.body[0]
-    assert isinstance(do_block, ast.Options)
-    assert do_block.type == 'do'
-    options = do_block.options
-    assert isinstance(options, list)
-    assert len(options) == 2
-    opt = options[0]
-    assert isinstance(opt, ast.Sequence)
-    assert len(opt) == 2
-    assert isinstance(opt[0], ast.Expression)
-    assert isinstance(opt[1], ast.Assignment)
-
-    opt = options[1]
-    assert isinstance(opt, ast.Sequence)
-    assert len(opt) == 3
-    assert isinstance(opt[0], ast.Expression)
-    assert isinstance(opt[1], ast.Assignment)
-    assert isinstance(opt[2], ast.Expression)
-
-
-def if_one_option_pg_test():
-    s = '''
-    proctype p (){
-        if
-        :: skip
-        fi
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1)])
-    assert nx.is_isomorphic(g, h)
-
-
-def if_two_options_pg_test():
-    s = '''
-    proctype p(){
-        if
-        :: true
-        :: false
-        fi
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1), (0, 1)])
-    assert nx.is_isomorphic(g, h)
-
-
-def do_one_option_pg_test():
-    s = '''
-    proctype p(){
-        do
-        :: skip
-        od
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 0)])
-    assert nx.is_isomorphic(g, h)
-
-
-def do_two_options_pg_test():
-    s = '''
-    proctype p(){
-        do
-        :: true
-        :: false
-        od
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 0), (0, 0)])
-    assert nx.is_isomorphic(g, h)
-
-
-def nested_if_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        if
-        :: if
-           :: true
-           :: false
-           fi
-        :: x
-        fi
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1), (0, 1), (0, 1)])
-    assert nx.is_isomorphic(g, h)
-
-
-def nested_if_not_guard_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        if
-        :: true;
-           if
-           :: true
-           :: false
-           fi
-        :: x
-        fi
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1), (0, 2), (2, 1), (2, 1)])
-    assert nx.is_isomorphic(g, h)
-
-
-def doubly_nested_if_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        if
-        :: if
-           :: true
-           :: if
-              :: true
-              :: skip
-              fi
-           :: false
-           fi
-        :: if
-           :: if
-              :: true
-              :: false
-              fi
-           fi
-        fi
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    for i in range(6):
-        h.add_edge(0, 1)
-    assert nx.is_isomorphic(g, h)
-
-
-def nested_do_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        if
-        :: do
-           :: true
-           :: false
-           od
-        :: x
-        fi
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1), (0, 2), (0, 2), (2, 2), (2, 2)])
-    assert nx.is_isomorphic(g, h)
-
-
-def nested_do_not_guard_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        if
-        :: true;
-           do
-           :: true
-           :: false
-           od
-        :: x
-        fi
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1), (0, 2), (2, 2), (2, 2)])
-    assert nx.is_isomorphic(g, h)
-
-
-def combined_if_do_program_graph_test():
-    s = '''
-    active proctype p(){
-        int x, y, z;
-        if /* 0 */
-        ::  do
-            :: x = 1; /* 2 */
-               y == 5 /* 1 */
-
-            :: z = 3; /* 3 */
-               skip /* 1 */
-
-            ::  if
-                :: z = (3 - x) * y; /* 4 */
-                   true; /* 5 */
-                   y = 3 /* 1 */
-
-                :: true /* 1 */
-                fi
-            od
-          /* 1 */
-
-        :: true; /* 6 */
-           if
-           :: true /* 7 */
-
-           :: true -> /* 8 */
-              x = y /* 7 */
-
-           fi
-        fi
-        /* 7 */
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([
-        (0, 2), (0, 3), (0, 4), (0, 1),
-        (2, 1), (3, 1), (5, 1),
-        (1, 2), (1, 3), (1, 4), (1, 1),
-        (4, 5),
-        # false; if ...
-        (0, 6),
-        (6, 7), (6, 8), (8, 7)])
-    dump(g, node_label=None)
-    assert iso.is_isomorphic(g, h)
-
-
-def invalid_label_pg_test():
-    s = '''
-    proctype p(){
-        do
-        :: S0: x = 1;
-        od
-    }
-    '''
-    tree = parser.parse(s)
-    with assert_raises(Exception):
-        tree[0].to_pg()
-
-
-def goto_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        x = 1;
-        goto S0;
-        x = 2;
-        S0: x = 3;
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1), (1, 2)])
-    assert nx.is_isomorphic(g, h)
-
-
-def double_goto_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        x = 1;
-        goto S0;
-        x = 2;
-        S0: goto S1;
-        x = 3;
-        S1: skip
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1), (1, 2)])
-    assert nx.is_isomorphic(g, h)
-
-
-def goto_inside_if_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        if
-        :: true; goto S0; x = 1;
-        :: x = 3; false
-        fi;
-        S0: skip
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1), (0, 2), (2, 1), (1, 3)])
-    assert nx.is_isomorphic(g, h)
-
-
-def goto_loop_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        S0: if
-        :: true; goto S0; x = 1;
-        :: x = 3;
-        fi;
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1), (0, 0)])
-    assert nx.is_isomorphic(g, h)
-
-
-def goto_self_loop_pg_test():
-    s = '''
-    proctype p(){
-        S0: goto S1;
-        S1: goto S0
-    }
-    '''
-    tree = parser.parse(s)
-    with assert_raises(AssertionError):
-        tree[0].to_pg()
-
-
-def break_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        do
-        :: true; x = 1;
-        :: break; x = 3;
-        od
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 1), (1, 0), (0, 2)])
-    assert nx.is_isomorphic(g, h)
-
-
-def nested_break_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        /* 0 */
-        do
-        :: true; /* 2 */
-           x == 1; /* 0 */
-
-        :: do
-           :: x == 2;
-              break /* 0 */
-
-           :: false; /* 4 */
-              x == 3 /* 5 */
-
-           od
-           /* 5 */
-
-        :: break; /* 1 */
-           x == 4;
-
-        od
-        /* 1 */
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([
-        (0, 1),
-        (0, 2), (2, 0),
-        (0, 0),
-        (0, 4), (4, 5),
-        (5, 4), (5, 0)])
-    assert nx.is_isomorphic(g, h)
-
-
-def atomic_pg_test():
-    s = '''
-    proctype p(){
-        bit x;
-        x = 1;
-        atomic { x = 2; }
-        x = 3;
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_node(0, context=None)
-    h.add_node(1, context=None)
-    h.add_node(2, context='atomic')
-    h.add_node(3, context=None)
-    h.add_edges_from([(0, 1), (1, 2), (2, 3)])
-    nm = lambda x, y: x['context'] == y['context']
-    gm = iso.GraphMatcher(g, h, node_match=nm)
-    assert gm.is_isomorphic()
-
-
-def do_atomic_dissapears_pg_test():
-    s = '''
-    proctype p(){
-        bit x, y;
-        /* 0 */
-        do
-        :: true; /* 3 */
-           atomic { x = 2; goto S0; /* 1 */ y = 1}
-        :: x == 1; /* 4 */ y == 2; /* 0 */
-        od;
-        x = 3;
-        /* 1 */
-        S0: skip
-        /* 2 */
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([
-        (0, 3), (3, 1), (1, 2),
-        (0, 4), (4, 0)])
-    for u in h:
-        h.add_node(u, context=None)
-    nm = lambda x, y: x['context'] == y['context']
-    gm = iso.GraphMatcher(g, h, node_match=nm)
-    assert gm.is_isomorphic()
-
-
-def do_atomic_pg_test():
-    s = '''
-    proctype p(){
-        bit x, y;
-        /* 0 */
-        do
-        :: true; /* 1 */
-           atomic { x = 2; /* 2 */
-           y = 1; goto S0; } /* 3 */
-        :: x == 1; /* 4 */ y == 2; /* 0 */
-        od;
-        x = 3;
-        /* 3 */
-        S0: skip
-        /* 5 */
-    }
-    '''
-    tree = parser.parse(s)
-    g = tree[0].to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([
-        (0, 1), (1, 2), (2, 3),
-        (3, 5), (0, 4), (4, 0)])
-    for u in h:
-        h.add_node(u, context=None)
-    h.add_node(2, context='atomic')
-    nm = lambda x, y: x['context'] == y['context']
-    gm = iso.GraphMatcher(g, h, node_match=nm)
-    assert gm.is_isomorphic()
-
-
-def ltl_block_test():
-    s = '''
-    bit x, y, c;
-
-    proctype p(){
-        if
-        :: x;
-        fi
-    }
-
-    ltl { (x == 1) && []<>(y != 2) && <>[](c == 1) && (x U y) }
-    '''
-    tree = parser.parse(s)
-    assert len(tree) == 3, repr(tree)
-    decl, p, ltl = tree
-    assert isinstance(p, ast.Proctype)
-    assert isinstance(ltl, ast.LTL)
-    s = str(ltl.formula)
-    assert s == (
-        '((((x == 1) && ([] (<> (y != 2)))) && '
-        '(<> ([] (c == 1)))) && (x U y))'), s
-
-
-def test_else():
-    s = '''
-    proctype p(){
-        byte x;
-        do
-        :: x == 0
-        :: x == 1
-        :: else
-        od
-    }
-    '''
-    (proc,) = parser.parse(s)
-    g = proc.to_pg()
-    dump(g)
-    for u, v, d in g.edges(data=True):
-        c = d['stmt']
-        if isinstance(c, ast.Else):
-            print(c.other_guards)
-
-
-def test_nested_else():
-    s = '''
-    proctype p(){
-        byte x;
-        do
-        ::
-            if
-            :: false
-            :: else
-            fi
-        od
-    }
-    '''
-    (proc,) = parser.parse(s)
-    g = proc.to_pg()
-    dump(g)
-    h = nx.MultiDiGraph()
-    h.add_edges_from([(0, 0), (0, 0)])
-    for u in h:
-        h.add_node(u, context=None)
-    nm = lambda x, y: x['context'] == y['context']
-    gm = iso.GraphMatcher(g, h, node_match=nm)
-    assert gm.is_isomorphic()
-
-
-def test_double_else():
-    s = '''
-    proctype foo(){
-        bit x;
-        do
-        ::
-            if
-            :: x
-            :: else
-            fi
-        :: else
-        od
-    }
-    '''
-    # syntactic else = Promela language definition
-    (proc,) = parser.parse(s)
-    with assert_raises(AssertionError):
-        proc.to_pg()
-    # different from Promela language definition
-    g = proc.to_pg(syntactic_else=True)
-    active_else = 0
-    off_else = 0
-    for u, v, d in g.edges(data=True):
-        stmt = d['stmt']
-        if isinstance(stmt, ast.Else):
-            other = stmt.other_guards
-            if other is None:
-                off_else += 1
-            else:
-                active_else += 1
-                assert len(other) == 1, other
-                (other_stmt,) = other
-                s = str(other_stmt)
-                assert s == 'x', s
-    assert active_else == 1, active_else
-    assert off_else == 1, off_else
-
-
-def test_pg_node_order():
-    s = '''
-    proctype foo(){
-        bit x;
-        if
-        ::
-            do
-            :: x > 2; x = 1
-            :: else; break
-            od;
-            x = 1
-        :: x = 2
-        fi
-    }
-    '''
-    (proc,) = parser.parse(s)
-    g = proc.to_pg()
-    dump(g)
-    # Final indexing depends on the
-    # aux goto nodes created and the contraction order.
-    # The latter depend on the intermediate indexing,
-    # which is fixed syntactically
-    # (see `generate_unique_node`).
-    edges = {(0, 1), (0, 3), (0, 4), (2, 3),
-             (2, 4), (3, 1), (4, 2)}
-    assert set(g) == set(range(5)), g.nodes()
-    assert set(g.edges()) == edges, g.edges()
-
-
-def test_labels():
-    s = '''
-    active proctype foo(){
-        progress:
-        do
-        :: true
-        od
-    }
-    '''
-    (proc,) = parser.parse(s)
-    g = proc.to_pg()
-    for u, d in g.nodes(data=True):
-        print(d.get('label'))
-
-
-def test_remote_ref():
-    s = '''
-    proctype foo(){
-        bar @ critical
-    }
-    '''
-    (proc,) = parser.parse(s)
-    g = proc.to_pg()
-    (e,) = g.edges(data=True)
-    u, v, d = e
-    s = d['stmt']
-    assert isinstance(s, ast.Expression), s
-    ref = s.expr
-    assert isinstance(ref, ast.RemoteRef), ref
-    assert ref.proctype == 'bar', ref.proctype
-    assert ref.label == 'critical', ref.label
-    assert ref.pid is None, ref.pid
-
-
-def dump(g, fname='g.pdf', node_label='context'):
-    if logger.getEffectiveLevel() >= logging.DEBUG:
-        return
-    # map nodes to integers
-    ast.dump_graph(
-        g, fname, node_label=node_label, edge_label='stmt')
-
-
-if __name__ == '__main__':
-    test_labels()