[rtems-central commit] modifications made to promela_yacc
Sebastian Huber
sebh at rtems.org
Wed Jan 18 11:35:17 UTC 2023
Module: rtems-central
Branch: master
Commit: ebe914418c71329ada06430ea33b38533c5ba990
Changeset: http://git.rtems.org/rtems-central/commit/?id=ebe914418c71329ada06430ea33b38533c5ba990
Author: Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie>
Date: Fri Jan 13 15:42:20 2023 +0000
modifications made to promela_yacc
---
.../src/src/modules/promela_yacc/.gitignore | 20 -
.../promela/src/src/modules/promela_yacc/LICENSE | 1 +
.../src/src/modules/promela_yacc/MANIFEST.in | 4 -
formal/promela/src/src/modules/promela_yacc/doc.md | 100 ---
.../src/src/modules/promela_yacc/promela/ast.py | 120 ++--
.../src/src/modules/promela_yacc/promela/lex.py | 18 +-
.../src/src/modules/promela_yacc/promela/yacc.py | 207 ++++--
.../src/modules/promela_yacc/tests/yacc_test.py | 759 ---------------------
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()
More information about the vc
mailing list