[PATCH 12/18] third party code - promela parser
Andrew.Butterfield at scss.tcd.ie
Andrew.Butterfield at scss.tcd.ie
Thu Dec 22 11:45:27 UTC 2022
forked from https://github.com/johnyf/promela,
commit 32d14184a50e920a92201058e4f601329be8c9c7
---
.../src/src/modules/promela_yacc/.gitignore | 20 +
.../src/src/modules/promela_yacc/.travis.yml | 21 +
.../src/src/modules/promela_yacc/LICENSE | 31 +
.../src/src/modules/promela_yacc/MANIFEST.in | 4 +
.../src/src/modules/promela_yacc/README.md | 27 +
.../src/src/modules/promela_yacc/doc.md | 100 ++
.../modules/promela_yacc/promela/__init__.py | 6 +
.../src/modules/promela_yacc/promela/ast.py | 1035 +++++++++++++++++
.../src/modules/promela_yacc/promela/lex.py | 211 ++++
.../src/modules/promela_yacc/promela/yacc.py | 955 +++++++++++++++
.../src/src/modules/promela_yacc/setup.py | 65 ++
.../modules/promela_yacc/tests/yacc_test.py | 759 ++++++++++++
12 files changed, 3234 insertions(+)
create mode 100644 formal/promela/src/src/modules/promela_yacc/.gitignore
create mode 100644 formal/promela/src/src/modules/promela_yacc/.travis.yml
create mode 100644 formal/promela/src/src/modules/promela_yacc/LICENSE
create mode 100644 formal/promela/src/src/modules/promela_yacc/MANIFEST.in
create mode 100644 formal/promela/src/src/modules/promela_yacc/README.md
create mode 100644 formal/promela/src/src/modules/promela_yacc/doc.md
create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/__init__.py
create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/ast.py
create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/lex.py
create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/yacc.py
create mode 100644 formal/promela/src/src/modules/promela_yacc/setup.py
create mode 100644 formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py
diff --git a/formal/promela/src/src/modules/promela_yacc/.gitignore b/formal/promela/src/src/modules/promela_yacc/.gitignore
new file mode 100644
index 00000000..f4cd3f85
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/.gitignore
@@ -0,0 +1,20 @@
+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/.travis.yml b/formal/promela/src/src/modules/promela_yacc/.travis.yml
new file mode 100644
index 00000000..2fee40c9
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/.travis.yml
@@ -0,0 +1,21 @@
+language: python
+
+python:
+ - 2.7
+ - 3.4
+ - 3.5
+ - 3.6
+
+install:
+ - sudo apt-get update -qq
+ - sudo apt-get install -y graphviz
+ - pip install --upgrade pip setuptools
+ - pip install -r requirements.txt
+ - pip install .
+
+script:
+ - cd tests/
+ - nosetests --with-coverage --cover-package=promela
+
+after_success:
+ - coveralls
diff --git a/formal/promela/src/src/modules/promela_yacc/LICENSE b/formal/promela/src/src/modules/promela_yacc/LICENSE
new file mode 100644
index 00000000..bebe3694
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/LICENSE
@@ -0,0 +1,31 @@
+Copyright (c) 2014-2018 by California Institute of Technology
+Copyright (c) 2014-2018 by Ioannis Filippidis
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the California Institute of Technology nor
+ the names of its contributors may be used to endorse or promote
+ products derived from this software without specific prior
+ written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL CALTECH OR THE
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in b/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
new file mode 100644
index 00000000..bbacf5bf
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
@@ -0,0 +1,4 @@
+include tests/*.py
+include README.md
+include LICENSE
+include doc.md
diff --git a/formal/promela/src/src/modules/promela_yacc/README.md b/formal/promela/src/src/modules/promela_yacc/README.md
new file mode 100644
index 00000000..5340e23b
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/README.md
@@ -0,0 +1,27 @@
+[![Build Status][build_img]][travis]
+[![Coverage Status][coverage]][coveralls]
+
+
+About
+=====
+
+A parser for the Promela modeling language.
+[PLY](https://pypi.python.org/pypi/ply/3.4) (Python `lex`-`yacc`) is used to generate the parser.
+Classes for a Promela abstract tree are included and used for representing the result of parsing.
+A short tutorial can be found in the file `doc.md`.
+To install:
+
+```
+pip install promela
+```
+
+
+License
+=======
+[BSD-3](http://opensource.org/licenses/BSD-3-Clause), see `LICENSE` file.
+
+
+[build_img]: https://travis-ci.org/johnyf/promela.svg?branch=master
+[travis]: https://travis-ci.org/johnyf/promela
+[coverage]: https://coveralls.io/repos/johnyf/promela/badge.svg?branch=master
+[coveralls]: https://coveralls.io/r/johnyf/promela?branch=master
\ No newline at end of file
diff --git a/formal/promela/src/src/modules/promela_yacc/doc.md b/formal/promela/src/src/modules/promela_yacc/doc.md
new file mode 100644
index 00000000..02d73431
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/doc.md
@@ -0,0 +1,100 @@
+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/__init__.py b/formal/promela/src/src/modules/promela_yacc/promela/__init__.py
new file mode 100644
index 00000000..5cb6d2c4
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/promela/__init__.py
@@ -0,0 +1,6 @@
+"""Promela parser and syntax tree."""
+from .yacc import Parser
+try:
+ from ._version import version as __version__
+except:
+ __version__ = None
diff --git a/formal/promela/src/src/modules/promela_yacc/promela/ast.py b/formal/promela/src/src/modules/promela_yacc/promela/ast.py
new file mode 100644
index 00000000..16baaa05
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/promela/ast.py
@@ -0,0 +1,1035 @@
+"""Abstract syntax tree for Promela."""
+from __future__ import absolute_import
+from __future__ import division
+import logging
+import copy
+import ctypes
+import pprint
+import networkx as nx
+from networkx.utils import misc
+
+
+logger = logging.getLogger(__name__)
+DATATYPES = {
+ 'bit': ctypes.c_bool,
+ 'bool': ctypes.c_bool,
+ 'byte': ctypes.c_ubyte,
+ 'pid': ctypes.c_ubyte,
+ 'short': ctypes.c_short,
+ 'int': ctypes.c_int,
+ 'unsigned': None,
+ 'chan': None,
+ 'mtype': None}
+N = 0
+
+
+def generate_unique_node():
+ """Return a fresh integer to be used as node."""
+ global N
+ N += 1
+ return N
+
+
+def _indent(s, depth=1, skip=0):
+ w = []
+ for i, line in enumerate(s.splitlines()):
+ indent = '' if i < skip else depth * '\t'
+ w.append(indent + line)
+ return '\n'.join(w)
+
+
+def to_str(x):
+ try:
+ return x.to_str()
+ except AttributeError:
+ return str(x)
+
+
+class Proctype(object):
+ def __init__(self, name, body, args=None,
+ active=None, d_proc=False,
+ priority=None, provided=None):
+ self.name = name
+ self.body = body
+ self.args = args
+ if active is None:
+ active = 0
+ else:
+ active = int(active.value)
+ if priority is not None:
+ priority = int(priority.value)
+ self.active = active
+ self.priority = priority
+ self.provided = provided
+
+ def __str__(self):
+ return "Proctype('{name}')".format(name=self.name)
+
+ def to_str(self):
+ return (
+ '{active} proctype {name}({args}){{\n'
+ '{body}\n'
+ '}}\n\n').format(
+ active=self._active_str(),
+ name=self.name,
+ args=self._args_str(),
+ body=_indent(to_str(self.body)))
+
+ def _active_str(self):
+ if self.active is None:
+ active = ''
+ else:
+ active = 'active [' + to_str(self.active) + '] '
+ return active
+
+ def _args_str(self):
+ if self.args is None:
+ args = ''
+ else:
+ args = to_str(self.args)
+ return args
+
+ def to_pg(self, syntactic_else=False):
+ """Return program graph of proctype.
+
+ @param syntactic_else: if `True`, then "else"
+ statements in directly nested "if" or "do"
+ take precedence based on syntactic context.
+ The Promela language reference defines
+ "else" semantically, with respect to
+ the program graph.
+ """
+ global N
+ N = 1
+ g = nx.MultiDiGraph(name=self.name)
+ g.locals = set()
+ ine, out = self.body.to_pg(g, syntactic_else=syntactic_else)
+ # root: explicit is better than implicit
+ u = generate_unique_node()
+ g.add_node(u, color='red', context=None)
+ g.root = u
+ for v, d in ine:
+ g.add_edge(u, v, **d)
+ # rm unreachable nodes
+ S = nx.descendants(g, g.root)
+ S.add(g.root)
+ nodes_to_rm = {x for x in g.nodes() if x not in S}
+ [g.remove_node(x) for x in nodes_to_rm]
+ if logger.getEffectiveLevel() == 1:
+ dump_graph(
+ g, 'dbg.pdf', node_label='context',
+ edge_label='stmt', relabel=True)
+ # contract goto edges
+ assert_gotos_are_admissible(g)
+ for u in sorted(g.nodes(), key=str):
+ contract_goto_edges(g, u)
+ h = map_uuid_to_int(g)
+ # other out-edges of each node with an `else`
+ if not syntactic_else:
+ semantic_else(h)
+ return h
+
+
+def contract_goto_edges(g, u):
+ """Identify nodes connected with `goto` edge."""
+ assert u in g
+ assert g.root in g
+ n = g.out_degree(u)
+ if n == 0 or 1 < n:
+ return
+ assert n == 1, n
+ # single outgoing edge: safe to contract
+ _, q, d = next(iter(g.edges(u, data=True)))
+ if d['stmt'] != 'goto':
+ return
+ # goto
+ assert u != q, 'loop of `goto`s detected'
+ # the source node context (atomic or d_step) is overwritten
+ for p, _, d in g.in_edges(u, data=True):
+ g.add_edge(p, q, **d)
+ # but the source node label is preserved
+ u_label = g.node[u].get('labels')
+ if u_label is not None:
+ g.node[q].setdefault('labels', set()).update(u_label)
+ g.remove_node(u)
+ if u == g.root:
+ g.root = q
+
+
+def assert_gotos_are_admissible(g):
+ """Assert no branch node has outgoing `goto`."""
+ # branch node cannot have goto
+ # `goto` and `break` must have transformed to `true`
+ # labels must have raised `Exception`
+ for u in g:
+ if g.out_degree(u) <= 1:
+ continue
+ for _, v, d in g.edges(u, data=True):
+ assert 'stmt' in d
+ stmt = d['stmt']
+ assert stmt != 'goto', stmt
+ for u, d in g.nodes(data=True):
+ assert 'context' in d
+ for u, v, d in g.edges(data=True):
+ assert 'stmt' in d
+
+
+def map_uuid_to_int(g):
+ """Reinplace uuid nodes with integers."""
+ umap = {u: i for i, u in enumerate(sorted(g, key=str))}
+ h = nx.MultiDiGraph(name=g.name)
+ for u, d in g.nodes(data=True):
+ p = umap[u]
+ h.add_node(p, **d)
+ for u, v, key, d in g.edges(keys=True, data=True):
+ p = umap[u]
+ q = umap[v]
+ h.add_edge(p, q, key=key, **d)
+ h.root = umap[g.root]
+ h.locals = g.locals
+ return h
+
+
+def semantic_else(g):
+ """Set `Else.other_guards` to other edges with same source."""
+ for u, v, d in g.edges(data=True):
+ stmt = d['stmt']
+ if not isinstance(stmt, Else):
+ continue
+ # is `Else`
+ stmt.other_guards = [
+ q['stmt'] for _, _, q in g.out_edges(u, data=True)
+ if q['stmt'] != stmt]
+
+
+class NeverClaim(Proctype):
+ """Subclass exists only for semantic purposes."""
+ def to_str(self):
+ name = '' if self.name is None else self.name
+ s = (
+ 'never ' + name + '{\n' +
+ _indent(to_str(self.body)) + '\n'
+ '}\n\n')
+ return s
+
+
+class Init(Proctype):
+ def to_str(self):
+ return (
+ 'init ' + '{\n' +
+ _indent(to_str(self.body)) + '\n'
+ '}\n\n')
+
+
+class Program(list):
+ def __str__(self):
+ return '\n'.join(to_str(x) for x in self)
+
+ def __repr__(self):
+ c = super(Program, self).__repr__()
+ return 'Program({c})'.format(c=c)
+
+ def to_table(self):
+ """Return global definitions, proctypes, and LTL blocks.
+
+ @rtype: 3-`tuple` of `set`
+ """
+ units = misc.flatten(self)
+ ltl = {x for x in units if isinstance(x, LTL)}
+ proctypes = {x for x in units if isinstance(x, Proctype)}
+ global_defs = {x for x in units
+ if x not in proctypes and x not in ltl}
+ return global_defs, proctypes, ltl
+
+
+class LTL(object):
+ """Used to mark strings as LTL blocks."""
+
+ def __init__(self, formula):
+ self.formula = formula
+
+ def __repr__(self):
+ return 'LTL({f})'.format(f=repr(self.formula))
+
+ def __str__(self):
+ return 'ltl {' + str(self.formula) + '}'
+
+
+class Sequence(list):
+ def __init__(self, iterable, context=None, is_option=False):
+ super(Sequence, self).__init__(iterable)
+ # "atomic" or "dstep"
+ self.context = context
+ self.is_option = is_option
+
+ def to_str(self):
+ if self.context is None:
+ return '\n'.join(to_str(x) for x in self)
+ else:
+ return (
+ self.context + '{\n' +
+ _indent(to_str(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)
+
+ 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}
+ # atomic cannot appear inside d_step
+ if context == 'd_step' and c == 'atomic':
+ raise Exception('atomic inside d_step')
+ context = c
+ # find first non-decl
+ # option guard first
+ option_guard = self.is_option or option_guard
+ assert len(self) > 0
+ stmts = iter(self)
+ t = None
+ for stmt in stmts:
+ t = stmt.to_pg(g, context=context,
+ option_guard=option_guard, **kw)
+ if t is not None:
+ break
+ # no statements ?
+ if t is None:
+ return None
+ e, tail = t
+ # guard can't be a goto or label
+ # (should have been caught below)
+ if option_guard:
+ for u, d in e:
+ assert d.get('stmt') != 'goto', self
+ # other option statements
+ for stmt in stmts:
+ t = stmt.to_pg(g, context=context, option_guard=None, **kw)
+ # decl ?
+ if t is None:
+ continue
+ ine, out = t
+ # connect tail to ine
+ assert ine
+ for v, d in ine:
+ g.add_edge(tail, v, **d)
+ # update tail
+ assert out in g
+ tail = out
+ return e, tail
+
+
+class Node(object):
+ def to_pg(self, g, context=None, **kw):
+ u = generate_unique_node()
+ g.add_node(u, context=context)
+ e = (u, dict(stmt=self))
+ return [e], u
+
+
+class Options(Node):
+ def __init__(self, opt_type, options):
+ self.type = opt_type
+ self.options = options
+
+ def to_str(self):
+ a, b = self.entry_exit
+ c = list()
+ c.append(a)
+ c.append('\n')
+ for option in self.options:
+ option_guard = _indent(to_str(option[0]), skip=1)
+ w = [_indent(to_str(x)) for x in option[1:]]
+ c.append(
+ ':: {option_guard}{tail}\n'.format(
+ option_guard=option_guard,
+ tail=(' ->\n' + '\n'.join(w)) if w else ''))
+ c.append(b)
+ c.append(';\n')
+ return ''.join(c)
+
+ @property
+ def entry_exit(self):
+ if self.type == 'if':
+ return ('if', 'fi')
+ elif self.type == 'do':
+ return ('do', 'od')
+
+ def to_pg(self, g, od_exit=None,
+ context=None, option_guard=None,
+ syntactic_else=False, **kw):
+ logger.info('-- start flattening {t}'.format(t=self.type))
+ assert self.options
+ assert self.type in {'if', 'do'}
+ # create target
+ target = generate_unique_node()
+ g.add_node(target, context=context)
+ # target != exit node ?
+ if self.type == 'do':
+ od_exit = generate_unique_node()
+ g.add_node(od_exit, context=context)
+ self_else = None
+ self_has_else = False
+ option_has_else = False
+ edges = list()
+ else_ine = None
+ for option in self.options:
+ logger.debug('option: {opt}'.format(opt=option))
+ t = option.to_pg(g, od_exit=od_exit, context=context, **kw)
+ assert t is not None # decls filtered by `Sequence`
+ ine, out = t
+ assert out in g
+ # detect `else`
+ has_else = False
+ for u, d in ine:
+ stmt = d.get('stmt')
+ if isinstance(stmt, Else):
+ has_else = True
+ self_else = stmt
+ # option cannot start with goto (= contraction)
+ assert stmt != 'goto'
+ # who owns this else ?
+ if has_else:
+ if len(ine) == 1:
+ assert not self_has_else, option
+ self_has_else = True
+ if not syntactic_else:
+ assert not option_has_else, option
+ elif len(ine) > 1:
+ option_has_else = True
+ if not syntactic_else:
+ assert not self_has_else, option
+ else:
+ raise Exception('option with no in edges')
+ # collect in edges, except for own `else`
+ if not (has_else and self_has_else):
+ edges.extend(ine)
+ else:
+ else_ine = ine # keep for later
+ # forward edges
+ # goto from last option node to target node
+ g.add_edge(out, target, stmt='goto')
+ # backward edges
+ if self.type == 'if':
+ continue
+ for u, d in ine:
+ g.add_edge(target, u, **d)
+ # handle else
+ if self_has_else and not option_has_else:
+ self_else.other_guards = [d['stmt'] for v, d in edges]
+ # add back the `else` edge
+ edges.extend(else_ine)
+ # what is the exit node ?
+ if self.type == 'if':
+ out = target
+ elif self.type == 'do':
+ out = od_exit
+ else:
+ raise Exception('Unknown type: {t}'.format(t=out))
+ # is not itself an option guard ?
+ if option_guard:
+ logger.debug('is option guard')
+ if self.type == 'do' and option_guard is None:
+ edge = (target, dict(stmt='goto'))
+ in_edges = [edge]
+ else:
+ in_edges = edges
+ logger.debug('in edges: {ie}, out: {out}\n'.format(
+ ie=in_edges, out=out))
+ logger.info('-- end flattening {t}'.format(t=self.type))
+ assert out in g
+ return in_edges, out
+
+
+class Else(Node):
+ def __init__(self):
+ self.other_guards = None
+
+ def __str__(self):
+ return 'else'
+
+
+class Break(Node):
+ def __str__(self):
+ return 'break'
+
+ def to_pg(self, g, od_exit=None, **kw):
+ if od_exit is None:
+ raise Exception('Break outside repetition construct.')
+ # like goto, but with: v = od_exit
+ # context of od_tail is determined by do loop
+ assert od_exit in g
+ v = od_exit
+ return goto_to_pg(g, v, **kw)
+
+
+class Goto(Node):
+ def __init__(self, label):
+ self.label = label
+
+ def __str__(self):
+ return 'goto {l}'.format(l=self.label)
+
+ def to_pg(self, g, context=None, **kw):
+ v = _format_label(self.label)
+ # ok, because source node context
+ # is overwritten during contraction
+ g.add_node(v, context=context)
+ return goto_to_pg(g, v, context=context, **kw)
+
+
+def goto_to_pg(g, v, option_guard=None, context=None, **kw):
+ assert v in g
+ if option_guard is None:
+ stmt = 'goto'
+ else:
+ stmt = Bool('true')
+ e = (v, dict(stmt=stmt))
+ u = generate_unique_node()
+ g.add_node(u, context=context)
+ return [e], u
+
+
+class Label(Node):
+ def __init__(self, label, body):
+ self.label = label
+ self.body = body
+
+ def to_str(self):
+ return '{l}: {b}'.format(l=self.label, b=to_str(self.body))
+
+ def to_pg(self, g, option_guard=None, context=None, **kw):
+ if option_guard is not None:
+ raise Exception('option guard cannot be labeled')
+ # add label node, with context
+ u = _format_label(self.label)
+ g.add_node(u, context=context, labels={self.label})
+ # flatten body
+ t = self.body.to_pg(g, context=context, **kw)
+ if t is None:
+ raise Exception('Label of variable declaration.')
+ ine, out = t
+ assert out in g
+ # make ine out edges of label node
+ for v, d in ine:
+ g.add_edge(u, v, **d)
+ # appear like a goto (almost)
+ e = (u, dict(stmt='goto'))
+ return [e], out
+
+
+def _format_label(label):
+ return 'label_{l}'.format(l=label)
+
+
+# TODO: check that referenced types exist, before adding typedef
+# to symbol table
+
+class VarDef(Node):
+ def __init__(self, name, vartype, length=None,
+ visible=None, bitwidth=None,
+ msg_types=None, initval=None):
+ self.name = name
+ self.type = vartype
+ if length is None:
+ l = None
+ else:
+ l = eval(str(length))
+ assert isinstance(l, int), l
+ self.length = l
+ self.visible = visible
+ if bitwidth is not None:
+ self.bitwidth = int(bitwidth.value)
+ if vartype == 'bool':
+ default_initval = Bool('false')
+ else:
+ default_initval = Integer('0')
+ if initval is None:
+ initval = Expression(default_initval)
+ self.initial_value = initval
+ # TODO message types
+
+ def __repr__(self):
+ return 'VarDef({t}, {v})'.format(t=self.type, v=self.name)
+
+ def to_str(self):
+ s = '{type} {varname}{len}'.format(
+ type=self._type_str(),
+ varname=self.name,
+ len='[{n}]'.format(n=self.len) if self.len else '')
+ return s
+
+ def _type_str(self):
+ return self.type
+
+ def to_pg(self, g, **kw):
+ # var declarations are collected before the process runs
+ # man page: datatypes, p.405
+ g.locals.add(self)
+ return None
+
+ def insert(self, symbol_table, pid):
+ """Insert variable into table of symbols.
+
+ @type symbol_table: L{SymbolTable}
+
+ @type pid: int or None
+ """
+ t = self.type
+ if t == 'chan':
+ v = MessageChannel(self.len)
+ # channels are always available globally
+ # note how this differs from having global scope:
+ # no name conflicts
+ symbol_table.channels.add(v)
+ elif t == 'mtype':
+ raise NotImplementedError
+ elif t in {'bit', 'bool', 'byte', 'pid', 'short', 'int'}:
+ if self.len is None:
+ v = DATATYPES[t]()
+ else:
+ v = [DATATYPES[t]() for i in range(self.len)]
+ elif t == 'unsigned':
+ n = self.bitwidth
+
+ class Unsigned(ctypes.Structure):
+ _fields_ = [('value', ctypes.c_uint, n)]
+
+ if self.len is None:
+ v = Unsigned()
+ else:
+ v = [Unsigned() for i in range(self.len)]
+ else:
+ raise TypeError('unknown type "{t}"'.format(t=t))
+ # global scope ?
+ if pid is None:
+ d = symbol_table.globals
+ else:
+ d = symbol_table.locals[pid]
+ name = self.name
+ if name in d:
+ raise Exception('variable "{name}" is already defined'.format(
+ name=name))
+ else:
+ d[name] = v
+
+
+class SymbolTable(object):
+ """Variable, user data and message type definitions.
+
+ Attributes:
+
+ - `globals`: `dict` of global vars
+ - `locals`: `dict` of `dicts`, keys of outer `dict` are pids
+ - `channels`: `dict` of global lists for channels
+ - `pids`: map from:
+
+ pid integers
+
+ to:
+
+ - name of proctype (name)
+ - current value of program counter (pc)
+
+ - `types`: `dict` of data types
+
+ pids are non-negative integers.
+ The type name "mtype" corresponds to a message type.
+ """
+
+ def __init__(self):
+ # see Def. 7.6, p.157
+ self.exclusive = None
+ self.handshake = None
+ self.timeout = False
+ self.else_ = False
+ self.stutter = False
+ # tables of variables
+ self.globals = dict()
+ self.channels = set()
+ self.locals = dict()
+ self.pids = dict()
+ self.types = DATATYPES
+
+ def __hash__(self):
+ return hash(repr(self))
+
+ def __eq__(self, other):
+ assert(isinstance(other, SymbolTable))
+ if self.globals != other.globals:
+ return False
+ if self.channels != other.channels:
+ return False
+ if set(self.locals) != set(other.locals):
+ return False
+ for pid, d in self.locals.items():
+ if d != other.locals[pid]:
+ return False
+ if set(self.pids) != set(other.pids):
+ return False
+ for pid, d in self.pids.items():
+ q = other.pids[pid]
+ if d['name'] != q['name']:
+ return False
+ if d['pc'] != q['pc']:
+ return False
+ return True
+
+ def __str__(self):
+ return (
+ 'globals: {g}\n'
+ 'channels: {c}\n'
+ 'pids: {p}\n\n'
+ 'types: {t}\n'
+ 'locals: {l}\n'
+ 'exclusive: {e}\n').format(
+ g=self.globals,
+ l=self.locals,
+ p=pprint.pformat(self.pids, width=15),
+ t=self.types,
+ e=self.exclusive,
+ c=self.channels)
+
+ def copy(self):
+ new = SymbolTable()
+ # auxiliary
+ new.exclusive = self.exclusive
+ new.handshake = self.handshake
+ new.timeout = self.timeout
+ new.else_ = self.else_
+ new.stutter = self.stutter
+ # copy symbols
+ new.globals = copy.deepcopy(self.globals)
+ new.channels = copy.deepcopy(self.channels)
+ new.locals = copy.deepcopy(self.locals)
+ new.pids = {k: {'name': d['name'],
+ 'pc': d['pc']}
+ for k, d in self.pids.items()}
+ new.types = self.types
+ return new
+
+
+class MessageChannel(object):
+ def __init__(self, nslots):
+ self.nslots = nslots
+ self.contents = list()
+
+ def send(self, x):
+ if len(self.contents) < self.nslots:
+ self.contents.append(x)
+ else:
+ raise Exception('channel {name} is full'.format(
+ name=self.name))
+
+ def receive(self, x=None, random=False, rm=True):
+ c = self.contents
+ i = 0
+ if x and random:
+ i = c.index(x)
+ m = c[i]
+ if rm:
+ c.pop(i)
+ return m
+
+
+class TypeDef(Node):
+ def __init__(self, name, decls):
+ self.name = name
+ self.decls = decls
+
+ def __str__(self):
+ return 'typedef {name} {\ndecls\n}'.format(
+ name=self.name, decls=to_str(self.decls))
+
+ def exe(self, t):
+ t.types[self.name] = self
+
+
+class MessageType(Node):
+ def __init__(self, values, visible=None):
+ self.values = values
+
+ def __str__(self):
+ return 'mtype {{ {values} }}'.format(values=self.values)
+
+ def exe(self, t):
+ t.types[self.name] = self
+
+
+class Return(Node):
+ def __init__(self, expr):
+ self.expr = expr
+
+ def __str__(self):
+ return to_str(self.expr)
+
+
+class Run(Node):
+ def __init__(self, func, args=None, priority=None):
+ self.func = func
+ self.args = args
+ self.priority = priority
+
+ def __str__(self):
+ return 'run({f})'.format(f=self.func)
+
+
+class Inline(Node):
+ def __init__(self, name, args):
+ self.name = name
+ self.args = args
+
+
+class Call(Node):
+ def __init__(self, func, args):
+ self.func = func
+ self.args = args
+
+
+class Assert(Node):
+ def __init__(self, expr):
+ self.expr = expr
+
+ def __repr__(self):
+ return 'assert({expr})'.format(expr=repr(self.expr))
+
+
+class Expression(Node):
+ def __init__(self, expr):
+ self.expr = expr
+
+ def __repr__(self):
+ return 'Expression({expr})'.format(expr=repr(self.expr))
+
+ def __str__(self):
+ return to_str(self.expr)
+
+ def eval(self, g, l):
+ s = str(self)
+ g = dict(g)
+ for k, v in g.items():
+ if 'ctypes' in str(type(v)):
+ g[k] = int(v.value)
+ elif isinstance(v, list):
+ for x in v:
+ if 'ctypes' in str(type(x)):
+ v[v.index(x)] = int(x.value)
+ l = dict(l)
+ for k, v in l.items():
+ if 'ctypes' in str(type(v)):
+ l[k] = int(v.value)
+ elif isinstance(v, list):
+ for x in v:
+ if 'ctypes' in str(type(x)):
+ v[v.index(x)] = int(x.value)
+
+ v = eval(s, g, l)
+ return v
+
+
+class Assignment(Node):
+ def __init__(self, var, value):
+ self.var = var
+ self.value = value
+
+ def __repr__(self):
+ return 'Assignment({var}, {val})'.format(
+ var=repr(self.var), val=repr(self.value))
+
+ def __str__(self):
+ return '{var} = {val}'.format(var=self.var, val=self.value)
+
+ def exe(self, g, l):
+ logger.debug('Assign: {var} = {val}'.format(
+ var=self.var, val=self.value))
+ s = self.to_str()
+ og = g
+ ol = l
+ g = dict(g)
+ for k, v in g.items():
+ if 'ctypes' in str(type(v)):
+ g[k] = int(v.value)
+ elif isinstance(v, list):
+ for x in v:
+ if 'ctypes' in str(type(x)):
+ v[v.index(x)] = int(x.value)
+ l = dict(l)
+ for k, v in l.items():
+ if 'ctypes' in str(type(v)):
+ l[k] = int(v.value)
+ elif isinstance(v, list):
+ for x in v:
+ if 'ctypes' in str(type(x)):
+ v[v.index(x)] = int(x.value)
+ exec(s, g, l)
+ for k in og:
+ og[k] = g[k]
+ for k in ol:
+ ol[k] = l[k]
+
+
+class Receive(Node):
+ def __init__(self, varref, args=None):
+ self.var = varref
+ self.args = args
+
+ def __str__(self):
+ v = to_str(self.var)
+ return 'Rx({v})'.format(v=v)
+
+
+class Send(Node):
+ def __init__(self, varref, args=None):
+ self.varref = varref
+ self.args = args
+
+ def __str__(self):
+ v = to_str(self.var)
+ return 'Tx({v})'.format(v=v)
+
+
+class Printf(Node):
+ def __init__(self, s, args):
+ self.s = s
+ self.args = args
+
+ def __str__(self):
+ return 'printf()'.format(s=self.s, args=self.args)
+
+
+class Operator(object):
+ def __init__(self, operator, *operands):
+ self.operator = operator
+ self.operands = operands
+
+ def __repr__(self):
+ return 'Operator({op}, {xy})'.format(
+ op=repr(self.operator),
+ xy=', '.join(repr(x) for x in self.operands))
+
+ def __str__(self):
+ return '({op} {xy})'.format(
+ op=self.operator,
+ xy=' '.join(to_str(x) for x in self.operands))
+
+
+class Binary(Operator):
+ def __str__(self):
+ return '({x} {op} {y})'.format(
+ x=to_str(self.operands[0]),
+ op=self.operator,
+ y=to_str(self.operands[1]))
+
+
+class Unary(Operator):
+ pass
+
+
+class Terminal(object):
+ def __init__(self, value):
+ self.value = value
+
+ def __repr__(self):
+ return '{classname}({val})'.format(
+ classname=type(self).__name__,
+ val=repr(self.value))
+
+ def __str__(self):
+ return str(self.value)
+
+
+class VarRef(Terminal):
+ def __init__(self, name, index=None, extension=None):
+ self.name = name
+ if index is None:
+ i = None
+ else:
+ i = index
+ self.index = i
+ self.extension = extension
+ # used by some external methods
+ self.value = name
+
+ def __repr__(self):
+ return 'VarRef({name}, {index}, {ext})'.format(
+ name=repr(self.name),
+ index=repr(self.index),
+ ext=repr(self.extension))
+
+ def __str__(self):
+ if self.index is None:
+ i = ''
+ else:
+ i = '[{i}]'.format(i=to_str(self.index))
+ return '{name}{index}{ext}'.format(
+ name=self.name,
+ index=i,
+ ext='' if self.extension is None else self.extension)
+
+
+class Integer(Terminal):
+ def __bool__(self):
+ return bool(int(self.value))
+
+
+class Bool(Terminal):
+ def __init__(self, val):
+ self.value = val.upper() == 'TRUE'
+
+ def __bool__(self):
+ return self.value
+
+ def __repr__(self):
+ return 'Bool({value})'.format(value=repr(self.value))
+
+ def __str__(self):
+ return str(self.value)
+
+
+class RemoteRef(Terminal):
+ def __init__(self, proctype, label, pid=None):
+ self.proctype = proctype
+ self.label = label
+ self.pid = pid
+
+ def __repr__(self):
+ return 'RemoteRef({proc}, {label}, {pid})'.format(
+ proc=self.proctype, label=self.label, pid=self.pid)
+
+ def __str__(self):
+ if self.pid is None:
+ inst = ''
+ else:
+ inst = '[{pid}]'.format(pid=self.pid)
+ return '{proc} {inst} @ {label}'.format(
+ proc=self.proctype, inst=inst, label=self.label)
+
+
+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."""
+ # map nodes to integers
+ if relabel:
+ mapping = {u: i for i, u in enumerate(g)}
+ g = nx.relabel_nodes(g, mapping)
+ inv_mapping = {v: k for k, v in mapping.items()}
+ s = list()
+ s.append('mapping of nodes:')
+ for k in sorted(inv_mapping):
+ v = inv_mapping[k]
+ s.append('{k}: {v}'.format(k=k, v=v))
+ print('\n'.join(s))
+ h = nx.MultiDiGraph()
+ for u, d in g.nodes(data=True):
+ label = d.get(node_label, u)
+ label = '"{label}"'.format(label=label)
+ h.add_node(u, label=label)
+ for u, v, d in g.edges(data=True):
+ label = d.get(edge_label, ' ')
+ label = '"{label}"'.format(label=label)
+ h.add_edge(u, v, label=label)
+ pd = nx.drawing.nx_pydot.to_pydot(h)
+ pd.write_pdf(fname)
diff --git a/formal/promela/src/src/modules/promela_yacc/promela/lex.py b/formal/promela/src/src/modules/promela_yacc/promela/lex.py
new file mode 100644
index 00000000..cd3eafe0
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/promela/lex.py
@@ -0,0 +1,211 @@
+"""Lexer for Promela, using Python Lex-Yacc (PLY)."""
+import logging
+import ply.lex
+
+
+logger = logging.getLogger(__name__)
+
+
+class Lexer(object):
+ """Lexer for the Promela modeling language."""
+
+ states = tuple([('ltl', 'inclusive')])
+ reserved = {
+ '_np': 'NONPROGRESS',
+ 'true': 'TRUE',
+ 'false': 'FALSE',
+ 'active': 'ACTIVE',
+ 'assert': 'ASSERT',
+ 'atomic': 'ATOMIC',
+ 'bit': 'BIT',
+ 'bool': 'BOOL',
+ 'break': 'BREAK',
+ 'byte': 'BYTE',
+ 'chan': 'CHAN',
+ 'd_step': 'D_STEP',
+ 'd_proctype': 'D_PROCTYPE',
+ 'do': 'DO',
+ 'else': 'ELSE',
+ 'empty': 'EMPTY',
+ 'enabled': 'ENABLED',
+ 'eval': 'EVAL',
+ 'fi': 'FI',
+ 'full': 'FULL',
+ 'get_priority': 'GET_P',
+ 'goto': 'GOTO',
+ 'hidden': 'HIDDEN',
+ 'if': 'IF',
+ 'init': 'INIT',
+ 'int': 'INT',
+ 'len': 'LEN',
+ 'local': 'ISLOCAL',
+ 'ltl': 'LTL',
+ 'mtype': 'MTYPE',
+ 'nempty': 'NEMPTY',
+ 'never': 'CLAIM',
+ 'nfull': 'NFULL',
+ 'od': 'OD',
+ 'of': 'OF',
+ 'pc_value': 'PC_VAL',
+ 'pid': 'PID',
+ 'printf': 'PRINT',
+ 'priority': 'PRIORITY',
+ 'proctype': 'PROCTYPE',
+ 'provided': 'PROVIDED',
+ 'R': 'RELEASE',
+ 'return': 'RETURN',
+ 'run': 'RUN',
+ 'short': 'SHORT',
+ 'skip': 'TRUE',
+ 'show': 'SHOW',
+ 'timeout': 'TIMEOUT',
+ 'typedef': 'TYPEDEF',
+ 'U': 'UNTIL',
+ 'unless': 'UNLESS',
+ 'unsigned': 'UNSIGNED',
+ 'X': 'NEXT',
+ 'xr': 'XR',
+ 'xs': 'XS',
+ 'W': 'WEAK_UNTIL'}
+ values = {'skip': 'true'}
+ delimiters = ['LPAREN', 'RPAREN', 'LBRACKET', 'RBRACKET',
+ 'LBRACE', 'RBRACE', 'COMMA', 'PERIOD',
+ 'SEMI', 'COLONS', 'COLON', 'ELLIPSIS']
+ # remember to check precedence
+ operators = ['PLUS', 'INCR', 'MINUS', 'DECR', 'TIMES', 'DIVIDE',
+ 'MOD', 'OR', 'AND', 'NOT', 'XOR', 'IMPLIES', 'EQUIV',
+ 'LOR', 'LAND', 'LNOT', 'LT', 'GT',
+ 'LE', 'GE', 'EQ', 'NE',
+ 'RCV', 'R_RCV', 'TX2', 'LSHIFT', 'RSHIFT', 'AT',
+ 'ALWAYS', 'EVENTUALLY']
+ misc = ['EQUALS', 'ARROW', 'STRING', 'NAME', 'INTEGER',
+ 'PREPROC', 'NEWLINE', 'COMMENT']
+
+ def __init__(self, debug=False):
+ self.tokens = (
+ self.delimiters + self.operators +
+ self.misc + list(set(self.reserved.values())))
+ self.build(debug=debug)
+
+ def build(self, debug=False, debuglog=None, **kwargs):
+ """Create a lexer.
+
+ @param kwargs: Same arguments as C{ply.lex.lex}:
+
+ - except for C{module} (fixed to C{self})
+ - C{debuglog} defaults to the module's logger.
+ """
+ if debug and debuglog is None:
+ debuglog = logger
+ self.lexer = ply.lex.lex(
+ module=self,
+ debug=debug,
+ debuglog=debuglog,
+ **kwargs)
+
+ # check for reserved words
+ def t_NAME(self, t):
+ r'[a-zA-Z_][a-zA-Z_0-9]*'
+ t.value = self.values.get(t.value, t.value)
+ t.type = self.reserved.get(t.value, 'NAME')
+ # switch to LTL context
+ if t.value == 'ltl':
+ self.lexer.level = 0
+ self.lexer.begin('ltl')
+ return t
+
+ def t_STRING(self, t):
+ r'"[^"]*"'
+ return t
+
+ # operators
+ t_PLUS = r'\+'
+ t_INCR = r'\+\+'
+ t_MINUS = r'-'
+ t_DECR = r'--'
+ t_TIMES = r'\*'
+ t_DIVIDE = r'/'
+ t_MOD = r'%'
+ t_OR = r'\|'
+ t_AND = r'&'
+ t_NOT = r'~'
+ t_XOR = r'\^'
+ t_LOR = r'\|\|'
+ t_LAND = r'&&'
+ t_LNOT = r'!'
+ t_TX2 = r'!!'
+ t_LT = r'<'
+ t_LSHIFT = r'<<'
+ t_GT = r'>'
+ t_RSHIFT = r'>>'
+ t_LE = r'<='
+ t_GE = r'>='
+ t_EQ = r'=='
+ t_NE = r'!='
+ t_RCV = r'\?'
+ t_R_RCV = r'\?\?'
+ t_AT = r'@'
+ t_EQUIV = r'<->'
+ # assignment
+ t_EQUALS = r'='
+ # temporal operators
+ t_ALWAYS = r'\[\]'
+ t_EVENTUALLY = r'\<\>'
+ # delimeters
+ t_LPAREN = r'\('
+ t_RPAREN = r'\)'
+ t_LBRACKET = r'\['
+ t_RBRACKET = r'\]'
+ t_LBRACE = r'\{'
+ t_RBRACE = r'\}'
+ t_COMMA = r','
+ t_PERIOD = r'\.'
+ t_SEMI = r';'
+ t_COLONS = r'::'
+ t_COLON = r':'
+ t_ELLIPSIS = r'\.\.\.'
+
+ def t_ltl_LBRACE(self, t):
+ r'\{'
+ self.lexer.level += 1
+ return t
+
+ def t_ltl_RBRACE(self, t):
+ r'\}'
+ self.lexer.level -= 1
+ if self.lexer.level == 0:
+ self.lexer.begin('INITIAL')
+ return t
+
+ def t_ltl_ARROW(self, t):
+ r'->'
+ t.type = 'IMPLIES'
+ return t
+
+ t_INITIAL_ARROW = r'->'
+
+ def t_PREPROC(self, t):
+ r'\#.*'
+ pass
+
+ def t_INTEGER(self, t):
+ r'\d+([uU]|[lL]|[uU][lL]|[lL][uU])?'
+ return t
+
+ # t_ignore is reserved by lex to provide
+ # much more efficient internal handling by lex
+ #
+ # A string containing ignored characters (spaces and tabs)
+ t_ignore = ' \t'
+
+ def t_NEWLINE(self, t):
+ r'\n+'
+ t.lexer.lineno += t.value.count('\n')
+
+ def t_COMMENT(self, t):
+ r' /\*(.|\n)*?\*/'
+ t.lineno += t.value.count('\n')
+
+ def t_error(self, t):
+ logger.error('Illegal character "{s}"'.format(s=t.value[0]))
+ t.lexer.skip(1)
diff --git a/formal/promela/src/src/modules/promela_yacc/promela/yacc.py b/formal/promela/src/src/modules/promela_yacc/promela/yacc.py
new file mode 100644
index 00000000..d650c063
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/promela/yacc.py
@@ -0,0 +1,955 @@
+"""Parser for Promela, using Python Lex-Yacc (PLY).
+
+
+References
+==========
+
+Holzmann G.J., The SPIN Model Checker,
+ Addison-Wesley, 2004, pp. 365--368
+ http://spinroot.com/spin/Man/Quick.html
+"""
+from __future__ import absolute_import
+from __future__ import division
+import logging
+import os
+import subprocess
+import warnings
+import ply.yacc
+# inline
+#
+# import promela.ast as promela_ast
+# from promela import lex
+
+
+TABMODULE = 'promela.promela_parsetab'
+logger = logging.getLogger(__name__)
+
+
+class Parser(object):
+ """Production rules for Promela parser."""
+
+ logger = logger
+ tabmodule = TABMODULE
+ start = 'program'
+ # http://spinroot.com/spin/Man/operators.html
+ # spin.y
+ # lowest to highest
+ precedence = (
+ ('right', 'EQUALS'),
+ ('left', 'TX2', 'RCV', 'R_RCV'),
+ ('left', 'IMPLIES', 'EQUIV'),
+ ('left', 'LOR'),
+ ('left', 'LAND'),
+ ('left', 'ALWAYS', 'EVENTUALLY'),
+ ('left', 'UNTIL', 'WEAK_UNTIL', 'RELEASE'),
+ ('right', 'NEXT'),
+ ('left', 'OR'),
+ ('left', 'XOR'),
+ ('left', 'AND'),
+ ('left', 'EQ', 'NE'),
+ ('left', 'LT', 'LE', 'GT', 'GE'),
+ ('left', 'LSHIFT', 'RSHIFT'),
+ ('left', 'PLUS', 'MINUS'),
+ ('left', 'TIMES', 'DIVIDE', 'MOD'),
+ ('left', 'INCR', 'DECR'),
+ ('right', 'LNOT', 'NOT', 'UMINUS', 'NEG'), # LNOT is also SND
+ ('left', 'DOT'),
+ ('left', 'LPAREN', 'RPAREN', 'LBRACKET', 'RBRACKET'))
+
+ def __init__(self, ast=None, lexer=None):
+ if ast is None:
+ import promela.ast as ast
+ if lexer is None:
+ from promela import lex
+ lexer = lex.Lexer()
+ self.lexer = lexer
+ self.ast = ast
+ self.tokens = self.lexer.tokens
+ self.build()
+
+ def build(self, tabmodule=None, outputdir='', write_tables=False,
+ debug=False, debuglog=None, errorlog=None):
+ """Build parser using `ply.yacc`.
+
+ Default table module is `self.tabmodule`.
+ Module logger used as default debug logger.
+ Default error logger is that created by PLY.
+ """
+ if tabmodule is None:
+ tabmodule = self.tabmodule
+ if debug and debuglog is None:
+ debuglog = self.logger
+ self.parser = ply.yacc.yacc(
+ method='LALR',
+ module=self,
+ start=self.start,
+ tabmodule=tabmodule,
+ outputdir=outputdir,
+ write_tables=write_tables,
+ debug=debug,
+ debuglog=debuglog,
+ errorlog=errorlog)
+
+ def parse(self, promela):
+ """Parse string of Promela code."""
+ s = cpp(promela)
+ program = self.parser.parse(
+ s, lexer=self.lexer.lexer, debug=self.logger)
+ return program
+
+ def _iter(self, p):
+ if p[2] is not None:
+ p[1].append(p[2])
+ return p[1]
+
+ def _end(self, p):
+ if p[1] is None:
+ return list()
+ else:
+ return [p[1]]
+
+ # Top-level constructs
+ # ====================
+
+ def p_program(self, p):
+ """program : units"""
+ p[0] = self.ast.Program(p[1])
+
+ def p_units_iter(self, p):
+ """units : units unit"""
+ p[0] = self._iter(p)
+
+ def p_units_end(self, p):
+ """units : unit"""
+ p[0] = self._end(p)
+
+ # TODO: events, c_fcts, ns, error
+ def p_unit_proc(self, p):
+ """unit : proc
+ | init
+ | claim
+ | ltl
+ """
+ p[0] = p[1]
+
+ def p_unit_decl(self, p):
+ """unit : one_decl
+ | utype
+ """
+ p[0] = p[1]
+
+ def p_unit_semi(self, p):
+ """unit : semi"""
+
+ def p_proc(self, p):
+ ("""proc : prefix_proctype NAME"""
+ """ LPAREN decl RPAREN"""
+ """ opt_priority opt_enabler"""
+ """ body
+ """)
+ inst = p[1]
+ name = p[2]
+ args = p[4]
+ priority = p[6]
+ enabler = p[7]
+ body = p[8]
+
+ p[0] = self.ast.Proctype(
+ name, body, args=args, priority=priority,
+ provided=enabler, **inst)
+
+ # instantiator
+ def p_inst(self, p):
+ """prefix_proctype : ACTIVE opt_index proctype"""
+ d = p[3]
+ if p[2] is None:
+ n_active = self.ast.Integer('1')
+ else:
+ n_active = p[2]
+ d['active'] = n_active
+ p[0] = d
+
+ def p_inactive_proctype(self, p):
+ """prefix_proctype : proctype"""
+ p[0] = p[1]
+
+ def p_opt_index(self, p):
+ """opt_index : LBRACKET expr RBRACKET
+ | LBRACKET NAME RBRACKET
+ """
+ p[0] = p[2]
+
+ def p_opt_index_empty(self, p):
+ """opt_index : empty"""
+
+ def p_init(self, p):
+ """init : INIT opt_priority body"""
+ p[0] = self.ast.Init(name='init', body=p[3], priority=p[2])
+
+ def p_claim(self, p):
+ """claim : CLAIM optname body"""
+ name = p[2] if p[2] else 'never'
+ p[0] = self.ast.NeverClaim(name=name, body=p[3])
+
+ # user-defined type
+ def p_utype(self, p):
+ """utype : TYPEDEF NAME LBRACE decl_lst RBRACE"""
+ seq = self.ast.Sequence(p[4])
+ p[0] = self.ast.TypeDef(p[2], seq)
+
+ def p_ltl(self, p):
+ """ltl : LTL LBRACE expr RBRACE"""
+ p[0] = self.ast.LTL(p[3])
+
+ # Declarations
+ # ============
+
+ def p_decl(self, p):
+ """decl : decl_lst"""
+ p[0] = self.ast.Sequence(p[1])
+
+ def p_decl_empty(self, p):
+ """decl : empty"""
+
+ def p_decl_lst_iter(self, p):
+ """decl_lst : one_decl SEMI decl_lst"""
+ p[0] = [p[1]] + p[3]
+
+ def p_decl_lst_end(self, p):
+ """decl_lst : one_decl"""
+ p[0] = [p[1]]
+
+ def p_one_decl_visible(self, p):
+ """one_decl : vis typename var_list
+ | vis NAME var_list
+ """
+ visible = p[1]
+ typ = p[2]
+ var_list = p[3]
+
+ p[0] = self.one_decl(typ, var_list, visible)
+
+ def p_one_decl(self, p):
+ """one_decl : typename var_list
+ | NAME var_list
+ """
+ typ = p[1]
+ var_list = p[2]
+ p[0] = self.one_decl(typ, var_list)
+
+ def one_decl(self, typ, var_list, visible=None):
+ c = list()
+ for d in var_list:
+ v = self.ast.VarDef(vartype=typ, visible=visible, **d)
+ c.append(v)
+ return self.ast.Sequence(c)
+
+ # message type declaration
+ def p_one_decl_mtype_vis(self, p):
+ """one_decl : vis MTYPE asgn LBRACE name_list RBRACE"""
+ p[0] = self.ast.MessageType(p[5], visible=p[1])
+
+ def p_one_decl_mtype(self, p):
+ """one_decl : MTYPE asgn LBRACE name_list RBRACE"""
+ p[0] = self.ast.MessageType(p[3])
+
+ def p_name_list_iter(self, p):
+ """name_list : name_list COMMA NAME"""
+ p[1].append(p[3])
+ p[0] = p[1]
+
+ def p_name_list_end(self, p):
+ """name_list : NAME"""
+ p[0] = [p[1]]
+
+ def p_var_list_iter(self, p):
+ """var_list : ivar COMMA var_list"""
+ p[0] = [p[1]] + p[3]
+
+ def p_var_list_end(self, p):
+ """var_list : ivar"""
+ p[0] = [p[1]]
+
+ # TODO: vardcl asgn LBRACE c_list RBRACE
+
+ # ivar = initialized variable
+ def p_ivar(self, p):
+ """ivar : vardcl"""
+ p[0] = p[1]
+
+ def p_ivar_asgn(self, p):
+ """ivar : vardcl asgn expr"""
+ expr = self.ast.Expression(p[3])
+ p[1]['initval'] = expr
+ p[0] = p[1]
+
+ def p_vardcl(self, p):
+ """vardcl : NAME"""
+ p[0] = {'name': p[1]}
+
+ # p.403, SPIN manual
+ def p_vardcl_unsigned(self, p):
+ """vardcl : NAME COLON const"""
+ p[0] = {'name': p[1], 'bitwidth': p[3]}
+
+ def p_vardcl_array(self, p):
+ """vardcl : NAME LBRACKET const_expr RBRACKET"""
+ p[0] = {'name': p[1], 'length': p[3]}
+
+ def p_vardcl_chan(self, p):
+ """vardcl : vardcl EQUALS ch_init"""
+ p[1].update(p[3])
+ p[0] = p[1]
+
+ def p_typename(self, p):
+ """typename : BIT
+ | BOOL
+ | BYTE
+ | CHAN
+ | INT
+ | PID
+ | SHORT
+ | UNSIGNED
+ | MTYPE
+ """
+ p[0] = p[1]
+
+ def p_ch_init(self, p):
+ ("""ch_init : LBRACKET const_expr RBRACKET """
+ """ OF LBRACE typ_list RBRACE""")
+ p[0] = {'length': p[2], 'msg_types': p[6]}
+
+ def p_typ_list_iter(self, p):
+ """typ_list : typ_list COMMA basetype"""
+ p[1].append(p[3])
+ p[0] = p[1]
+
+ def p_typ_list_end(self, p):
+ """typ_list : basetype"""
+ p[0] = [p[1]]
+
+ # TODO: | UNAME | error
+ def p_basetype(self, p):
+ """basetype : typename"""
+ p[0] = p[1]
+
+ # References
+ # ==========
+
+ def p_varref(self, p):
+ """varref : cmpnd"""
+ p[0] = p[1]
+
+ def p_cmpnd_iter(self, p):
+ """cmpnd : cmpnd PERIOD cmpnd %prec DOT"""
+ p[0] = self.ast.VarRef(extension=p[3], **p[1])
+
+ def p_cmpnd_end(self, p):
+ """cmpnd : pfld"""
+ p[0] = self.ast.VarRef(**p[1])
+
+ # pfld = prefix field
+ def p_pfld_indexed(self, p):
+ """pfld : NAME LBRACKET expr RBRACKET"""
+ p[0] = {'name': p[1], 'index': p[3]}
+
+ def p_pfld(self, p):
+ """pfld : NAME"""
+ p[0] = {'name': p[1]}
+
+ # Attributes
+ # ==========
+
+ def p_opt_priority(self, p):
+ """opt_priority : PRIORITY number"""
+ p[0] = p[2]
+
+ def p_opt_priority_empty(self, p):
+ """opt_priority : empty"""
+
+ def p_opt_enabler(self, p):
+ """opt_enabler : PROVIDED LPAREN expr RPAREN"""
+ p[0] = p[3]
+
+ def p_opt_enabler_empty(self, p):
+ """opt_enabler : empty"""
+
+ def p_body(self, p):
+ """body : LBRACE sequence os RBRACE"""
+ p[0] = p[2]
+
+ # Sequence
+ # ========
+
+ def p_sequence(self, p):
+ """sequence : sequence msemi step"""
+ p[1].append(p[3])
+ p[0] = p[1]
+
+ def p_sequence_ending_with_atomic(self, p):
+ """sequence : seq_block step"""
+ p[1].append(p[2])
+ p[0] = p[1]
+
+ def p_sequence_single(self, p):
+ """sequence : step"""
+ p[0] = self.ast.Sequence([p[1]])
+
+ def p_seq_block(self, p):
+ """seq_block : sequence msemi atomic
+ | sequence msemi dstep
+ """
+ p[1].append(p[3])
+ p[0] = p[1]
+
+ def p_seq_block_iter(self, p):
+ """seq_block : seq_block atomic
+ | seq_block dstep
+ """
+ p[1].append(p[2])
+ p[0] = p[1]
+
+ def p_seq_block_single(self, p):
+ """seq_block : atomic
+ | dstep
+ """
+ p[0] = [p[1]]
+
+ # TODO: XU vref_lst
+ def p_step_1(self, p):
+ """step : one_decl
+ | stmnt
+ """
+ p[0] = p[1]
+
+ def p_step_labeled(self, p):
+ """step : NAME COLON one_decl"""
+ raise Exception(
+ 'label preceding declaration: {s}'.format(s=p[3]))
+
+ def p_step_3(self, p):
+ """step : NAME COLON XR
+ | NAME COLON XS
+ """
+ raise Exception(
+ 'label preceding xr/xs claim')
+
+ def p_step_4(self, p):
+ """step : stmnt UNLESS stmnt"""
+ p[0] = (p[1], 'unless', p[3])
+ self.logger.warning('UNLESS not interpreted yet')
+
+ # Statement
+ # =========
+
+ def p_stmnt(self, p):
+ """stmnt : special
+ | statement
+ """
+ p[0] = p[1]
+
+ # Stmnt in spin.y
+ def p_statement_asgn(self, p):
+ """statement : varref asgn full_expr"""
+ p[0] = self.ast.Assignment(var=p[1], value=p[3])
+
+ def p_statement_incr(self, p):
+ """statement : varref INCR"""
+ one = self.ast.Integer('1')
+ expr = self.ast.Expression(self.ast.Binary('+', p[1], one))
+ p[0] = self.ast.Assignment(p[1], expr)
+
+ def p_statement_decr(self, p):
+ """statement : varref DECR"""
+ one = self.ast.Integer('1')
+ expr = self.ast.Expression(self.ast.Binary('-', p[1], one))
+ p[0] = self.ast.Assignment(p[1], expr)
+
+ def p_statement_assert(self, p):
+ """statement : ASSERT full_expr"""
+ p[0] = self.ast.Assert(p[2])
+
+ def p_statement_fifo_receive(self, p):
+ """statement : varref RCV rargs"""
+ p[0] = self.ast.Receive(p[1], p[3])
+
+ def p_statement_copy_fifo_receive(self, p):
+ """statement : varref RCV LT rargs GT"""
+ p[0] = self.ast.Receive(p[1], p[4])
+
+ def p_statement_random_receive(self, p):
+ """statement : varref R_RCV rargs"""
+ p[0] = self.ast.Receive(p[1], p[3])
+
+ def p_statement_copy_random_receive(self, p):
+ """statement : varref R_RCV LT rargs GT"""
+ p[0] = self.ast.Receive(p[1], p[4])
+
+ def p_statement_tx2(self, p):
+ """statement : varref TX2 margs"""
+ p[0] = self.ast.Send(p[1], p[3])
+
+ def p_statement_full_expr(self, p):
+ """statement : full_expr"""
+ p[0] = p[1]
+
+ def p_statement_else(self, p):
+ """statement : ELSE"""
+ p[0] = self.ast.Else()
+
+ def p_statement_atomic(self, p):
+ """statement : atomic"""
+ p[0] = p[1]
+
+ def p_atomic(self, p):
+ """atomic : ATOMIC LBRACE sequence os RBRACE"""
+ s = p[3]
+ s.context = 'atomic'
+ p[0] = s
+
+ def p_statement_dstep(self, p):
+ """statement : dstep"""
+ p[0] = p[1]
+
+ def p_dstep(self, p):
+ """dstep : D_STEP LBRACE sequence os RBRACE"""
+ s = p[3]
+ s.context = 'd_step'
+ p[0] = s
+
+ def p_statement_braces(self, p):
+ """statement : LBRACE sequence os RBRACE"""
+ p[0] = p[2]
+
+ # the stmt of line 696 in spin.y collects the inline ?
+ def p_statement_call(self, p):
+ """statement : NAME LPAREN args RPAREN"""
+ # NAME = INAME = inline
+ c = self.ast.Inline(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])
+ 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])
+
+ # yet unimplemented for statement:
+ # SET_P l_par two_args r_par
+ # PRINTM l_par varref r_par
+ # PRINTM l_par CONST r_par
+ # ccode
+
+ # Special
+ # =======
+
+ def p_special(self, p):
+ """special : varref RCV"""
+ p[0] = self.ast.Receive(p[1])
+
+ def p_varref_lnot(self, p):
+ """special : varref LNOT margs"""
+ raise NotImplementedError
+
+ def p_break(self, p):
+ """special : BREAK"""
+ p[0] = self.ast.Break()
+
+ def p_goto(self, p):
+ """special : GOTO NAME"""
+ p[0] = self.ast.Goto(p[2])
+
+ def p_labeled_stmt(self, p):
+ """special : NAME COLON stmnt"""
+ p[0] = self.ast.Label(p[1], p[3])
+
+ def p_labeled(self, p):
+ """special : NAME COLON"""
+ p[0] = self.ast.Label(
+ p[1],
+ self.ast.Expression(self.ast.Bool('true')))
+
+ def p_special_if(self, p):
+ """special : IF options FI"""
+ p[0] = self.ast.Options('if', p[2])
+
+ def p_special_do(self, p):
+ """special : DO options OD"""
+ p[0] = self.ast.Options('do', p[2])
+
+ def p_options_end(self, p):
+ """options : option"""
+ p[0] = [p[1]]
+
+ def p_options_iter(self, p):
+ """options : options option"""
+ p[1].append(p[2])
+ p[0] = p[1]
+
+ def p_option(self, p):
+ """option : COLONS sequence os"""
+ s = p[2]
+ s.is_option = True
+ p[0] = s
+
+ # Expressions
+ # ===========
+
+ def p_full_expr(self, p):
+ """full_expr : expr
+ | pexpr
+ """
+ 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
+ | pexpr LAND expr
+ | expr LAND pexpr
+ | pexpr LOR pexpr
+ | pexpr LOR expr
+ | expr LOR pexpr
+ """
+ p[0] = 'pexpr'
+
+ def p_probe(self, p):
+ """probe : FULL LPAREN varref RPAREN
+ | NFULL LPAREN varref RPAREN
+ | EMPTY LPAREN varref RPAREN
+ | NEMPTY LPAREN varref RPAREN
+ """
+ p[0] = 'probe'
+
+ def p_expr_paren(self, p):
+ """expr : LPAREN expr RPAREN"""
+ p[0] = p[2]
+
+ def p_expr_arithmetic(self, p):
+ """expr : expr PLUS expr
+ | expr MINUS expr
+ | expr TIMES expr
+ | expr DIVIDE expr
+ | expr MOD expr
+ """
+ p[0] = self.ast.Binary(p[2], p[1], p[3])
+
+ def p_expr_not(self, p):
+ """expr : NOT expr
+ | MINUS expr %prec UMINUS
+ | LNOT expr %prec NEG
+ """
+ p[0] = self.ast.Unary(p[1], p[2])
+
+ def p_expr_logical(self, p):
+ """expr : expr AND expr
+ | expr OR expr
+ | expr XOR expr
+ | expr LAND expr
+ | expr LOR expr
+ """
+ p[0] = self.ast.Binary(p[2], p[1], p[3])
+
+ # TODO: cexpr
+
+ def p_expr_shift(self, p):
+ """expr : expr LSHIFT expr
+ | expr RSHIFT expr
+ """
+ p[0] = p[1]
+
+ def p_expr_const_varref(self, p):
+ """expr : const
+ | varref
+ """
+ p[0] = p[1]
+
+ def p_expr_varref(self, p):
+ """expr : varref RCV LBRACKET rargs RBRACKET
+ | varref R_RCV LBRACKET rargs RBRACKET
+ """
+ p[0] = p[1]
+ warnings.warn('not implemented')
+
+ def p_expr_other(self, p):
+ """expr : LPAREN expr ARROW expr COLON expr RPAREN
+ | LEN LPAREN varref RPAREN
+ | ENABLED LPAREN expr RPAREN
+ | GET_P LPAREN expr RPAREN
+ """
+ p[0] = p[1]
+ warnings.warn('"{s}" not implemented'.format(s=p[1]))
+
+ def p_expr_run(self, p):
+ """expr : RUN aname LPAREN args RPAREN opt_priority"""
+ p[0] = self.ast.Run(p[2], p[4], p[6])
+
+ def p_expr_other_2(self, p):
+ """expr : TIMEOUT
+ | NONPROGRESS
+ | PC_VAL LPAREN expr RPAREN
+ """
+ raise NotImplementedError()
+
+ def p_expr_remote_ref_proctype_pc(self, p):
+ """expr : NAME AT NAME
+ """
+ p[0] = self.ast.RemoteRef(p[1], p[3])
+
+ def p_expr_remote_ref_pid_pc(self, p):
+ """expr : NAME LBRACKET expr RBRACKET AT NAME"""
+ p[0] = self.ast.RemoteRef(p[1], p[6], pid=p[3])
+
+ def p_expr_remote_ref_var(self, p):
+ """expr : NAME LBRACKET expr RBRACKET COLON pfld"""
+ # | NAME COLON pfld %prec DOT2
+ raise NotImplementedError()
+
+ def p_expr_comparator(self, p):
+ """expr : expr EQ expr
+ | expr NE expr
+ | expr LT expr
+ | expr LE expr
+ | expr GT expr
+ | expr GE expr
+ """
+ p[0] = self.ast.Binary(p[2], p[1], p[3])
+
+ def p_binary_ltl_expr(self, p):
+ """expr : expr UNTIL expr
+ | expr WEAK_UNTIL expr
+ | expr RELEASE expr
+ | expr IMPLIES expr
+ | expr EQUIV expr
+ """
+ p[0] = self.ast.Binary(p[2], p[1], p[3])
+
+ def p_unary_ltl_expr(self, p):
+ """expr : NEXT expr
+ | ALWAYS expr
+ | EVENTUALLY expr
+ """
+ p[0] = self.ast.Unary(p[1], p[2])
+
+ # Constants
+ # =========
+
+ def p_const_expr_const(self, p):
+ """const_expr : const"""
+ p[0] = p[1]
+
+ def p_const_expr_unary(self, p):
+ """const_expr : MINUS const_expr %prec UMINUS"""
+ p[0] = self.ast.Unary(p[1], p[2])
+
+ def p_const_expr_binary(self, p):
+ """const_expr : const_expr PLUS const_expr
+ | const_expr MINUS const_expr
+ | const_expr TIMES const_expr
+ | const_expr DIVIDE const_expr
+ | const_expr MOD const_expr
+ """
+ p[0] = self.ast.Binary(p[2], p[1], p[3])
+
+ def p_const_expr_paren(self, p):
+ """const_expr : LPAREN const_expr RPAREN"""
+ p[0] = p[2]
+
+ def p_const(self, p):
+ """const : boolean
+ | number
+ """
+ # lex maps `skip` to `TRUE`
+ p[0] = p[1]
+
+ def p_bool(self, p):
+ """boolean : TRUE
+ | FALSE
+ """
+ p[0] = self.ast.Bool(p[1])
+
+ def p_number(self, p):
+ """number : INTEGER"""
+ p[0] = self.ast.Integer(p[1])
+
+ # 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
+ | EVAL LPAREN expr RPAREN
+ """
+ p[0] = 'rarg'
+
+ def p_rargs(self, p):
+ """rargs : rarg
+ | rarg COMMA rargs
+ | rarg LPAREN rargs RPAREN
+ | LPAREN rargs RPAREN
+ """
+
+ def p_proctype(self, p):
+ """proctype : PROCTYPE
+ | D_PROCTYPE
+ """
+ if p[1] == 'proctype':
+ p[0] = dict(d_proc=False)
+ else:
+ p[0] = dict(d_proc=True)
+
+ # PNAME
+ def p_aname(self, p):
+ """aname : NAME"""
+ p[0] = p[1]
+
+ # optional name
+ def p_optname(self, p):
+ """optname : NAME"""
+ p[0] = p[1]
+
+ def p_optname_empty(self, p):
+ """optname : empty"""
+
+ # optional semi
+ def p_os(self, p):
+ """os : empty
+ | semi
+ """
+ p[0] = ';'
+
+ # multi-semi
+ def p_msemi(self, p):
+ """msemi : semi
+ | msemi semi
+ """
+ p[0] = ';'
+
+ def p_semi(self, p):
+ """semi : SEMI
+ | ARROW
+ """
+ p[0] = ';'
+
+ def p_asgn(self, p):
+ """asgn : EQUALS
+ | empty
+ """
+ p[0] = None
+
+ def p_visible(self, p):
+ """vis : HIDDEN
+ | SHOW
+ | ISLOCAL
+ """
+ p[0] = {'visible': p[1]}
+
+ def p_empty(self, p):
+ """empty : """
+
+ def p_error(self, p):
+ raise Exception('syntax error at: {p}'.format(p=p))
+
+
+def cpp(s):
+ """Call the C{C} preprocessor with input C{s}."""
+ try:
+ p = subprocess.Popen(['cpp', '-E', '-x', 'c'],
+ stdin=subprocess.PIPE,
+ stdout=subprocess.PIPE,
+ stderr=subprocess.PIPE,
+ universal_newlines=True)
+ except OSError as e:
+ if e.errno == os.errno.ENOENT:
+ raise Exception('C preprocessor (cpp) not found in path.')
+ else:
+ raise
+ logger.debug('cpp input:\n' + s)
+ stdout, stderr = p.communicate(s)
+ logger.debug('cpp returned: {c}'.format(c=p.returncode))
+ logger.debug('cpp stdout:\n {out}'.format(out=stdout))
+ return stdout
+
+
+def rebuild_table(parser, tabmodule):
+ # log details to file
+ h = logging.FileHandler('log.txt', mode='w')
+ debuglog = logging.getLogger()
+ debuglog.addHandler(h)
+ debuglog.setLevel('DEBUG')
+ import os
+ outputdir = './'
+ # rm table files to force rebuild to get debug output
+ tablepy = tabmodule + '.py'
+ tablepyc = tabmodule + '.pyc'
+ try:
+ os.remove(tablepy)
+ except:
+ print('no "{t}" found'.format(t=tablepy))
+ try:
+ os.remove(tablepyc)
+ except:
+ print('no "{t}" found'.format(t=tablepyc))
+ parser.build(tabmodule, outputdir=outputdir,
+ write_tables=True, debug=True,
+ debuglog=debuglog)
+
+
+if __name__ == '__main__':
+ rebuild_table(Parser(), TABMODULE.split('.')[-1])
+
+
+# TODO
+#
+# expr << expr
+# expr >> expr
+# (expr -> expr : expr)
+# run func(args) priority
+# len(varref)
+# enabled(expr)
+# get_p(expr)
+# var ? [rargs]
+# var ?? [rargs]
+# timeout
+# nonprogress
+# pc_val(expr)
+# name[expr] @ name
+# name[expr] : pfld
+# name @ name
+# name : pfld
diff --git a/formal/promela/src/src/modules/promela_yacc/setup.py b/formal/promela/src/src/modules/promela_yacc/setup.py
new file mode 100644
index 00000000..b58de8a0
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/setup.py
@@ -0,0 +1,65 @@
+from setuptools import setup
+# inline:
+# from promela import yacc
+
+
+description = (
+ 'Parser and abstract syntax tree for the Promela modeling language.')
+README = 'README.md'
+VERSION_FILE = 'promela/_version.py'
+MAJOR = 0
+MINOR = 0
+MICRO = 3
+version = '{major}.{minor}.{micro}'.format(
+ major=MAJOR, minor=MINOR, micro=MICRO)
+s = (
+ '# This file was generated from setup.py\n'
+ "version = '{version}'\n").format(version=version)
+install_requires = [
+ 'networkx >= 2.0',
+ 'ply >= 3.4',
+ 'pydot >= 1.1.0']
+classifiers = [
+ 'Development Status :: 2 - Pre-Alpha',
+ 'Intended Audience :: Science/Research',
+ 'License :: OSI Approved :: BSD License',
+ 'Operating System :: OS Independent',
+ 'Programming Language :: Python',
+ 'Programming Language :: Python :: 2.7',
+ 'Programming Language :: Python :: 3',
+ 'Topic :: Scientific/Engineering']
+keywords = [
+ 'promela', 'parser', 'syntax tree', 'ply', 'lex', 'yacc']
+
+
+def build_parser_table():
+ from promela import yacc
+ tabmodule = yacc.TABMODULE.split('.')[-1]
+ outputdir = 'promela/'
+ parser = yacc.Parser()
+ parser.build(tabmodule, outputdir=outputdir, write_tables=True)
+
+
+if __name__ == '__main__':
+ with open(VERSION_FILE, 'w') as f:
+ f.write(s)
+ try:
+ build_parser_table()
+ except ImportError:
+ print('WARNING: `promela` could not cache parser tables '
+ '(ignore this if running only for "egg_info").')
+ setup(
+ name='promela',
+ version=version,
+ description=description,
+ long_description=open(README).read(),
+ author='Ioannis Filippidis',
+ author_email='jfilippidis at gmail.com',
+ url='https://github.com/johnyf/promela',
+ license='BSD',
+ install_requires=install_requires,
+ tests_require=['nose'],
+ packages=['promela'],
+ package_dir={'promela': 'promela'},
+ classifiers=classifiers,
+ keywords=keywords)
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
new file mode 100644
index 00000000..b26d22aa
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py
@@ -0,0 +1,759 @@
+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()
--
2.37.1 (Apple Git-137.1)
More information about the devel
mailing list