source: rtems-central/formal/promela/src/src/modules/promela_yacc/promela/ast.py @ 5d08ea3

Last change on this file since 5d08ea3 was 5d08ea3, checked in by Andrew Butterfield <Andrew.Butterfield@…>, on 01/13/23 at 15:37:36

forked from https://github.com/johnyf/promela,
commit 32d14184a50e920a92201058e4f601329be8c9c7

  • Property mode set to 100644
File size: 29.0 KB
Line 
1"""Abstract syntax tree for Promela."""
2from __future__ import absolute_import
3from __future__ import division
4import logging
5import copy
6import ctypes
7import pprint
8import networkx as nx
9from networkx.utils import misc
10
11
12logger = logging.getLogger(__name__)
13DATATYPES = {
14    'bit': ctypes.c_bool,
15    'bool': ctypes.c_bool,
16    'byte': ctypes.c_ubyte,
17    'pid': ctypes.c_ubyte,
18    'short': ctypes.c_short,
19    'int': ctypes.c_int,
20    'unsigned': None,
21    'chan': None,
22    'mtype': None}
23N = 0
24
25
26def generate_unique_node():
27    """Return a fresh integer to be used as node."""
28    global N
29    N += 1
30    return N
31
32
33def _indent(s, depth=1, skip=0):
34    w = []
35    for i, line in enumerate(s.splitlines()):
36        indent = '' if i < skip else depth * '\t'
37        w.append(indent + line)
38    return '\n'.join(w)
39
40
41def to_str(x):
42    try:
43        return x.to_str()
44    except AttributeError:
45        return str(x)
46
47
48class Proctype(object):
49    def __init__(self, name, body, args=None,
50                 active=None, d_proc=False,
51                 priority=None, provided=None):
52        self.name = name
53        self.body = body
54        self.args = args
55        if active is None:
56            active = 0
57        else:
58            active = int(active.value)
59        if priority is not None:
60            priority = int(priority.value)
61        self.active = active
62        self.priority = priority
63        self.provided = provided
64
65    def __str__(self):
66        return "Proctype('{name}')".format(name=self.name)
67
68    def to_str(self):
69        return (
70            '{active} proctype {name}({args}){{\n'
71            '{body}\n'
72            '}}\n\n').format(
73                active=self._active_str(),
74                name=self.name,
75                args=self._args_str(),
76                body=_indent(to_str(self.body)))
77
78    def _active_str(self):
79        if self.active is None:
80            active = ''
81        else:
82            active = 'active [' + to_str(self.active) + '] '
83        return active
84
85    def _args_str(self):
86        if self.args is None:
87            args = ''
88        else:
89            args = to_str(self.args)
90        return args
91
92    def to_pg(self, syntactic_else=False):
93        """Return program graph of proctype.
94
95        @param syntactic_else: if `True`, then "else"
96            statements in directly nested "if" or "do"
97            take precedence based on syntactic context.
98            The Promela language reference defines
99            "else" semantically, with respect to
100            the program graph.
101        """
102        global N
103        N = 1
104        g = nx.MultiDiGraph(name=self.name)
105        g.locals = set()
106        ine, out = self.body.to_pg(g, syntactic_else=syntactic_else)
107        # root: explicit is better than implicit
108        u = generate_unique_node()
109        g.add_node(u, color='red', context=None)
110        g.root = u
111        for v, d in ine:
112            g.add_edge(u, v, **d)
113        # rm unreachable nodes
114        S = nx.descendants(g, g.root)
115        S.add(g.root)
116        nodes_to_rm = {x for x in g.nodes() if x not in S}
117        [g.remove_node(x) for x in nodes_to_rm]
118        if logger.getEffectiveLevel() == 1:
119            dump_graph(
120                g, 'dbg.pdf', node_label='context',
121                edge_label='stmt', relabel=True)
122        # contract goto edges
123        assert_gotos_are_admissible(g)
124        for u in sorted(g.nodes(), key=str):
125            contract_goto_edges(g, u)
126        h = map_uuid_to_int(g)
127        # other out-edges of each node with an `else`
128        if not syntactic_else:
129            semantic_else(h)
130        return h
131
132
133def contract_goto_edges(g, u):
134    """Identify nodes connected with `goto` edge."""
135    assert u in g
136    assert g.root in g
137    n = g.out_degree(u)
138    if n == 0 or 1 < n:
139        return
140    assert n == 1, n
141    # single outgoing edge: safe to contract
142    _, q, d = next(iter(g.edges(u, data=True)))
143    if d['stmt'] != 'goto':
144        return
145    # goto
146    assert u != q, 'loop of `goto`s detected'
147    # the source node context (atomic or d_step) is overwritten
148    for p, _, d in g.in_edges(u, data=True):
149        g.add_edge(p, q, **d)
150    # but the source node label is preserved
151    u_label = g.node[u].get('labels')
152    if u_label is not None:
153        g.node[q].setdefault('labels', set()).update(u_label)
154    g.remove_node(u)
155    if u == g.root:
156        g.root = q
157
158
159def assert_gotos_are_admissible(g):
160    """Assert no branch node has outgoing `goto`."""
161    # branch node cannot have goto
162    # `goto` and `break` must have transformed to `true`
163    # labels must have raised `Exception`
164    for u in g:
165        if g.out_degree(u) <= 1:
166            continue
167        for _, v, d in g.edges(u, data=True):
168            assert 'stmt' in d
169            stmt = d['stmt']
170            assert stmt != 'goto', stmt
171    for u, d in g.nodes(data=True):
172        assert 'context' in d
173    for u, v, d in g.edges(data=True):
174        assert 'stmt' in d
175
176
177def map_uuid_to_int(g):
178    """Reinplace uuid nodes with integers."""
179    umap = {u: i for i, u in enumerate(sorted(g, key=str))}
180    h = nx.MultiDiGraph(name=g.name)
181    for u, d in g.nodes(data=True):
182        p = umap[u]
183        h.add_node(p, **d)
184    for u, v, key, d in g.edges(keys=True, data=True):
185        p = umap[u]
186        q = umap[v]
187        h.add_edge(p, q, key=key, **d)
188    h.root = umap[g.root]
189    h.locals = g.locals
190    return h
191
192
193def semantic_else(g):
194    """Set `Else.other_guards` to other edges with same source."""
195    for u, v, d in g.edges(data=True):
196        stmt = d['stmt']
197        if not isinstance(stmt, Else):
198            continue
199        # is `Else`
200        stmt.other_guards = [
201            q['stmt'] for _, _, q in g.out_edges(u, data=True)
202            if q['stmt'] != stmt]
203
204
205class NeverClaim(Proctype):
206    """Subclass exists only for semantic purposes."""
207    def to_str(self):
208        name = '' if self.name is None else self.name
209        s = (
210            'never ' + name + '{\n' +
211            _indent(to_str(self.body)) + '\n'
212            '}\n\n')
213        return s
214
215
216class Init(Proctype):
217    def to_str(self):
218        return (
219            'init ' + '{\n' +
220            _indent(to_str(self.body)) + '\n'
221            '}\n\n')
222
223
224class Program(list):
225    def __str__(self):
226        return '\n'.join(to_str(x) for x in self)
227
228    def __repr__(self):
229        c = super(Program, self).__repr__()
230        return 'Program({c})'.format(c=c)
231
232    def to_table(self):
233        """Return global definitions, proctypes, and LTL blocks.
234
235        @rtype: 3-`tuple` of `set`
236        """
237        units = misc.flatten(self)
238        ltl = {x for x in units if isinstance(x, LTL)}
239        proctypes = {x for x in units if isinstance(x, Proctype)}
240        global_defs = {x for x in units
241                       if x not in proctypes and x not in ltl}
242        return global_defs, proctypes, ltl
243
244
245class LTL(object):
246    """Used to mark strings as LTL blocks."""
247
248    def __init__(self, formula):
249        self.formula = formula
250
251    def __repr__(self):
252        return 'LTL({f})'.format(f=repr(self.formula))
253
254    def __str__(self):
255        return 'ltl {' + str(self.formula) + '}'
256
257
258class Sequence(list):
259    def __init__(self, iterable, context=None, is_option=False):
260        super(Sequence, self).__init__(iterable)
261        # "atomic" or "dstep"
262        self.context = context
263        self.is_option = is_option
264
265    def to_str(self):
266        if self.context is None:
267            return '\n'.join(to_str(x) for x in self)
268        else:
269            return (
270                self.context + '{\n' +
271                _indent(to_str(self)) + '\n}\n')
272
273    def __repr__(self):
274        l = super(Sequence, self).__repr__()
275        return 'Sequence({l}, context={c}, is_option={isopt})'.format(
276            l=l, c=self.context, isopt=self.is_option)
277
278    def to_pg(self, g, context=None, option_guard=None, **kw):
279        # set context
280        if context is None:
281            context = self.context
282        c = context
283        assert c in {'atomic', 'd_step', None}
284        # atomic cannot appear inside d_step
285        if context == 'd_step' and c == 'atomic':
286            raise Exception('atomic inside d_step')
287        context = c
288        # find first non-decl
289        # option guard first
290        option_guard = self.is_option or option_guard
291        assert len(self) > 0
292        stmts = iter(self)
293        t = None
294        for stmt in stmts:
295            t = stmt.to_pg(g, context=context,
296                           option_guard=option_guard, **kw)
297            if t is not None:
298                break
299        # no statements ?
300        if t is None:
301            return None
302        e, tail = t
303        # guard can't be a goto or label
304        # (should have been caught below)
305        if option_guard:
306            for u, d in e:
307                assert d.get('stmt') != 'goto', self
308        # other option statements
309        for stmt in stmts:
310            t = stmt.to_pg(g, context=context, option_guard=None, **kw)
311            # decl ?
312            if t is None:
313                continue
314            ine, out = t
315            # connect tail to ine
316            assert ine
317            for v, d in ine:
318                g.add_edge(tail, v, **d)
319            # update tail
320            assert out in g
321            tail = out
322        return e, tail
323
324
325class Node(object):
326    def to_pg(self, g, context=None, **kw):
327        u = generate_unique_node()
328        g.add_node(u, context=context)
329        e = (u, dict(stmt=self))
330        return [e], u
331
332
333class Options(Node):
334    def __init__(self, opt_type, options):
335        self.type = opt_type
336        self.options = options
337
338    def to_str(self):
339        a, b = self.entry_exit
340        c = list()
341        c.append(a)
342        c.append('\n')
343        for option in self.options:
344            option_guard = _indent(to_str(option[0]), skip=1)
345            w = [_indent(to_str(x)) for x in option[1:]]
346            c.append(
347                ':: {option_guard}{tail}\n'.format(
348                    option_guard=option_guard,
349                    tail=(' ->\n' + '\n'.join(w)) if w else ''))
350        c.append(b)
351        c.append(';\n')
352        return ''.join(c)
353
354    @property
355    def entry_exit(self):
356        if self.type == 'if':
357            return ('if', 'fi')
358        elif self.type == 'do':
359            return ('do', 'od')
360
361    def to_pg(self, g, od_exit=None,
362              context=None, option_guard=None,
363              syntactic_else=False, **kw):
364        logger.info('-- start flattening {t}'.format(t=self.type))
365        assert self.options
366        assert self.type in {'if', 'do'}
367        # create target
368        target = generate_unique_node()
369        g.add_node(target, context=context)
370        # target != exit node ?
371        if self.type == 'do':
372            od_exit = generate_unique_node()
373            g.add_node(od_exit, context=context)
374        self_else = None
375        self_has_else = False
376        option_has_else = False
377        edges = list()
378        else_ine = None
379        for option in self.options:
380            logger.debug('option: {opt}'.format(opt=option))
381            t = option.to_pg(g, od_exit=od_exit, context=context, **kw)
382            assert t is not None  # decls filtered by `Sequence`
383            ine, out = t
384            assert out in g
385            # detect `else`
386            has_else = False
387            for u, d in ine:
388                stmt = d.get('stmt')
389                if isinstance(stmt, Else):
390                    has_else = True
391                    self_else = stmt
392                # option cannot start with goto (= contraction)
393                assert stmt != 'goto'
394            # who owns this else ?
395            if has_else:
396                if len(ine) == 1:
397                    assert not self_has_else, option
398                    self_has_else = True
399                    if not syntactic_else:
400                        assert not option_has_else, option
401                elif len(ine) > 1:
402                    option_has_else = True
403                    if not syntactic_else:
404                        assert not self_has_else, option
405                else:
406                    raise Exception('option with no in edges')
407            # collect in edges, except for own `else`
408            if not (has_else and self_has_else):
409                edges.extend(ine)
410            else:
411                else_ine = ine  # keep for later
412            # forward edges
413            # goto from last option node to target node
414            g.add_edge(out, target, stmt='goto')
415            # backward edges
416            if self.type == 'if':
417                continue
418            for u, d in ine:
419                g.add_edge(target, u, **d)
420        # handle else
421        if self_has_else and not option_has_else:
422            self_else.other_guards = [d['stmt'] for v, d in edges]
423            # add back the `else` edge
424            edges.extend(else_ine)
425        # what is the exit node ?
426        if self.type == 'if':
427            out = target
428        elif self.type == 'do':
429            out = od_exit
430        else:
431            raise Exception('Unknown type: {t}'.format(t=out))
432        # is not itself an option guard ?
433        if option_guard:
434            logger.debug('is option guard')
435        if self.type == 'do' and option_guard is None:
436            edge = (target, dict(stmt='goto'))
437            in_edges = [edge]
438        else:
439            in_edges = edges
440        logger.debug('in edges: {ie}, out: {out}\n'.format(
441            ie=in_edges, out=out))
442        logger.info('-- end flattening {t}'.format(t=self.type))
443        assert out in g
444        return in_edges, out
445
446
447class Else(Node):
448    def __init__(self):
449        self.other_guards = None
450
451    def __str__(self):
452        return 'else'
453
454
455class Break(Node):
456    def __str__(self):
457        return 'break'
458
459    def to_pg(self, g, od_exit=None, **kw):
460        if od_exit is None:
461            raise Exception('Break outside repetition construct.')
462        # like goto, but with: v = od_exit
463        # context of od_tail is determined by do loop
464        assert od_exit in g
465        v = od_exit
466        return goto_to_pg(g, v, **kw)
467
468
469class Goto(Node):
470    def __init__(self, label):
471        self.label = label
472
473    def __str__(self):
474        return 'goto {l}'.format(l=self.label)
475
476    def to_pg(self, g, context=None, **kw):
477        v = _format_label(self.label)
478        # ok, because source node context
479        # is overwritten during contraction
480        g.add_node(v, context=context)
481        return goto_to_pg(g, v, context=context, **kw)
482
483
484def goto_to_pg(g, v, option_guard=None, context=None, **kw):
485    assert v in g
486    if option_guard is None:
487        stmt = 'goto'
488    else:
489        stmt = Bool('true')
490    e = (v, dict(stmt=stmt))
491    u = generate_unique_node()
492    g.add_node(u, context=context)
493    return [e], u
494
495
496class Label(Node):
497    def __init__(self, label, body):
498        self.label = label
499        self.body = body
500
501    def to_str(self):
502        return '{l}: {b}'.format(l=self.label, b=to_str(self.body))
503
504    def to_pg(self, g, option_guard=None, context=None, **kw):
505        if option_guard is not None:
506            raise Exception('option guard cannot be labeled')
507        # add label node, with context
508        u = _format_label(self.label)
509        g.add_node(u, context=context, labels={self.label})
510        # flatten body
511        t = self.body.to_pg(g, context=context, **kw)
512        if t is None:
513            raise Exception('Label of variable declaration.')
514        ine, out = t
515        assert out in g
516        # make ine out edges of label node
517        for v, d in ine:
518            g.add_edge(u, v, **d)
519        # appear like a goto (almost)
520        e = (u, dict(stmt='goto'))
521        return [e], out
522
523
524def _format_label(label):
525    return 'label_{l}'.format(l=label)
526
527
528# TODO: check that referenced types exist, before adding typedef
529# to symbol table
530
531class VarDef(Node):
532    def __init__(self, name, vartype, length=None,
533                 visible=None, bitwidth=None,
534                 msg_types=None, initval=None):
535        self.name = name
536        self.type = vartype
537        if length is None:
538            l = None
539        else:
540            l = eval(str(length))
541            assert isinstance(l, int), l
542        self.length = l
543        self.visible = visible
544        if bitwidth is not None:
545            self.bitwidth = int(bitwidth.value)
546        if vartype == 'bool':
547            default_initval = Bool('false')
548        else:
549            default_initval = Integer('0')
550        if initval is None:
551            initval = Expression(default_initval)
552        self.initial_value = initval
553        # TODO message types
554
555    def __repr__(self):
556        return 'VarDef({t}, {v})'.format(t=self.type, v=self.name)
557
558    def to_str(self):
559        s = '{type} {varname}{len}'.format(
560            type=self._type_str(),
561            varname=self.name,
562            len='[{n}]'.format(n=self.len) if self.len else '')
563        return s
564
565    def _type_str(self):
566        return self.type
567
568    def to_pg(self, g, **kw):
569        # var declarations are collected before the process runs
570        # man page: datatypes, p.405
571        g.locals.add(self)
572        return None
573
574    def insert(self, symbol_table, pid):
575        """Insert variable into table of symbols.
576
577        @type symbol_table: L{SymbolTable}
578
579        @type pid: int or None
580        """
581        t = self.type
582        if t == 'chan':
583            v = MessageChannel(self.len)
584            # channels are always available globally
585            # note how this differs from having global scope:
586            # no name conflicts
587            symbol_table.channels.add(v)
588        elif t == 'mtype':
589            raise NotImplementedError
590        elif t in {'bit', 'bool', 'byte', 'pid', 'short', 'int'}:
591            if self.len is None:
592                v = DATATYPES[t]()
593            else:
594                v = [DATATYPES[t]() for i in range(self.len)]
595        elif t == 'unsigned':
596            n = self.bitwidth
597
598            class Unsigned(ctypes.Structure):
599                _fields_ = [('value', ctypes.c_uint, n)]
600
601            if self.len is None:
602                v = Unsigned()
603            else:
604                v = [Unsigned() for i in range(self.len)]
605        else:
606            raise TypeError('unknown type "{t}"'.format(t=t))
607        # global scope ?
608        if pid is None:
609            d = symbol_table.globals
610        else:
611            d = symbol_table.locals[pid]
612        name = self.name
613        if name in d:
614            raise Exception('variable "{name}" is already defined'.format(
615                            name=name))
616        else:
617            d[name] = v
618
619
620class SymbolTable(object):
621    """Variable, user data and message type definitions.
622
623    Attributes:
624
625      - `globals`: `dict` of global vars
626      - `locals`: `dict` of `dicts`, keys of outer `dict` are pids
627      - `channels`: `dict` of global lists for channels
628      - `pids`: map from:
629
630          pid integers
631
632          to:
633
634            - name of proctype (name)
635            - current value of program counter (pc)
636
637      - `types`: `dict` of data types
638
639    pids are non-negative integers.
640    The type name "mtype" corresponds to a message type.
641    """
642
643    def __init__(self):
644        # see Def. 7.6, p.157
645        self.exclusive = None
646        self.handshake = None
647        self.timeout = False
648        self.else_ = False
649        self.stutter = False
650        # tables of variables
651        self.globals = dict()
652        self.channels = set()
653        self.locals = dict()
654        self.pids = dict()
655        self.types = DATATYPES
656
657    def __hash__(self):
658        return hash(repr(self))
659
660    def __eq__(self, other):
661        assert(isinstance(other, SymbolTable))
662        if self.globals != other.globals:
663            return False
664        if self.channels != other.channels:
665            return False
666        if set(self.locals) != set(other.locals):
667            return False
668        for pid, d in self.locals.items():
669            if d != other.locals[pid]:
670                return False
671        if set(self.pids) != set(other.pids):
672            return False
673        for pid, d in self.pids.items():
674            q = other.pids[pid]
675            if d['name'] != q['name']:
676                return False
677            if d['pc'] != q['pc']:
678                return False
679        return True
680
681    def __str__(self):
682        return (
683            'globals: {g}\n'
684            'channels: {c}\n'
685            'pids: {p}\n\n'
686            'types: {t}\n'
687            'locals: {l}\n'
688            'exclusive: {e}\n').format(
689                g=self.globals,
690                l=self.locals,
691                p=pprint.pformat(self.pids, width=15),
692                t=self.types,
693                e=self.exclusive,
694                c=self.channels)
695
696    def copy(self):
697        new = SymbolTable()
698        # auxiliary
699        new.exclusive = self.exclusive
700        new.handshake = self.handshake
701        new.timeout = self.timeout
702        new.else_ = self.else_
703        new.stutter = self.stutter
704        # copy symbols
705        new.globals = copy.deepcopy(self.globals)
706        new.channels = copy.deepcopy(self.channels)
707        new.locals = copy.deepcopy(self.locals)
708        new.pids = {k: {'name': d['name'],
709                        'pc': d['pc']}
710                    for k, d in self.pids.items()}
711        new.types = self.types
712        return new
713
714
715class MessageChannel(object):
716    def __init__(self, nslots):
717        self.nslots = nslots
718        self.contents = list()
719
720    def send(self, x):
721        if len(self.contents) < self.nslots:
722            self.contents.append(x)
723        else:
724            raise Exception('channel {name} is full'.format(
725                            name=self.name))
726
727    def receive(self, x=None, random=False, rm=True):
728        c = self.contents
729        i = 0
730        if x and random:
731            i = c.index(x)
732        m = c[i]
733        if rm:
734            c.pop(i)
735        return m
736
737
738class TypeDef(Node):
739    def __init__(self, name, decls):
740        self.name = name
741        self.decls = decls
742
743    def __str__(self):
744        return 'typedef {name} {\ndecls\n}'.format(
745            name=self.name, decls=to_str(self.decls))
746
747    def exe(self, t):
748        t.types[self.name] = self
749
750
751class MessageType(Node):
752    def __init__(self, values, visible=None):
753        self.values = values
754
755    def __str__(self):
756        return 'mtype {{ {values} }}'.format(values=self.values)
757
758    def exe(self, t):
759        t.types[self.name] = self
760
761
762class Return(Node):
763    def __init__(self, expr):
764        self.expr = expr
765
766    def __str__(self):
767        return to_str(self.expr)
768
769
770class Run(Node):
771    def __init__(self, func, args=None, priority=None):
772        self.func = func
773        self.args = args
774        self.priority = priority
775
776    def __str__(self):
777        return 'run({f})'.format(f=self.func)
778
779
780class Inline(Node):
781    def __init__(self, name, args):
782        self.name = name
783        self.args = args
784
785
786class Call(Node):
787    def __init__(self, func, args):
788        self.func = func
789        self.args = args
790
791
792class Assert(Node):
793    def __init__(self, expr):
794        self.expr = expr
795
796    def __repr__(self):
797        return 'assert({expr})'.format(expr=repr(self.expr))
798
799
800class Expression(Node):
801    def __init__(self, expr):
802        self.expr = expr
803
804    def __repr__(self):
805        return 'Expression({expr})'.format(expr=repr(self.expr))
806
807    def __str__(self):
808        return to_str(self.expr)
809
810    def eval(self, g, l):
811        s = str(self)
812        g = dict(g)
813        for k, v in g.items():
814            if 'ctypes' in str(type(v)):
815                g[k] = int(v.value)
816            elif isinstance(v, list):
817                for x in v:
818                    if 'ctypes' in str(type(x)):
819                        v[v.index(x)] = int(x.value)
820        l = dict(l)
821        for k, v in l.items():
822            if 'ctypes' in str(type(v)):
823                l[k] = int(v.value)
824            elif isinstance(v, list):
825                for x in v:
826                    if 'ctypes' in str(type(x)):
827                        v[v.index(x)] = int(x.value)
828
829        v = eval(s, g, l)
830        return v
831
832
833class Assignment(Node):
834    def __init__(self, var, value):
835        self.var = var
836        self.value = value
837
838    def __repr__(self):
839        return 'Assignment({var}, {val})'.format(
840            var=repr(self.var), val=repr(self.value))
841
842    def __str__(self):
843        return '{var} = {val}'.format(var=self.var, val=self.value)
844
845    def exe(self, g, l):
846        logger.debug('Assign: {var} = {val}'.format(
847                     var=self.var, val=self.value))
848        s = self.to_str()
849        og = g
850        ol = l
851        g = dict(g)
852        for k, v in g.items():
853            if 'ctypes' in str(type(v)):
854                g[k] = int(v.value)
855            elif isinstance(v, list):
856                for x in v:
857                    if 'ctypes' in str(type(x)):
858                        v[v.index(x)] = int(x.value)
859        l = dict(l)
860        for k, v in l.items():
861            if 'ctypes' in str(type(v)):
862                l[k] = int(v.value)
863            elif isinstance(v, list):
864                for x in v:
865                    if 'ctypes' in str(type(x)):
866                        v[v.index(x)] = int(x.value)
867        exec(s, g, l)
868        for k in og:
869            og[k] = g[k]
870        for k in ol:
871            ol[k] = l[k]
872
873
874class Receive(Node):
875    def __init__(self, varref, args=None):
876        self.var = varref
877        self.args = args
878
879    def __str__(self):
880        v = to_str(self.var)
881        return 'Rx({v})'.format(v=v)
882
883
884class Send(Node):
885    def __init__(self, varref, args=None):
886        self.varref = varref
887        self.args = args
888
889    def __str__(self):
890        v = to_str(self.var)
891        return 'Tx({v})'.format(v=v)
892
893
894class Printf(Node):
895    def __init__(self, s, args):
896        self.s = s
897        self.args = args
898
899    def __str__(self):
900        return 'printf()'.format(s=self.s, args=self.args)
901
902
903class Operator(object):
904    def __init__(self, operator, *operands):
905        self.operator = operator
906        self.operands = operands
907
908    def __repr__(self):
909        return 'Operator({op}, {xy})'.format(
910            op=repr(self.operator),
911            xy=', '.join(repr(x) for x in self.operands))
912
913    def __str__(self):
914        return '({op} {xy})'.format(
915            op=self.operator,
916            xy=' '.join(to_str(x) for x in self.operands))
917
918
919class Binary(Operator):
920    def __str__(self):
921        return '({x} {op} {y})'.format(
922            x=to_str(self.operands[0]),
923            op=self.operator,
924            y=to_str(self.operands[1]))
925
926
927class Unary(Operator):
928    pass
929
930
931class Terminal(object):
932    def __init__(self, value):
933        self.value = value
934
935    def __repr__(self):
936        return '{classname}({val})'.format(
937            classname=type(self).__name__,
938            val=repr(self.value))
939
940    def __str__(self):
941        return str(self.value)
942
943
944class VarRef(Terminal):
945    def __init__(self, name, index=None, extension=None):
946        self.name = name
947        if index is None:
948            i = None
949        else:
950            i = index
951        self.index = i
952        self.extension = extension
953        # used by some external methods
954        self.value = name
955
956    def __repr__(self):
957        return 'VarRef({name}, {index}, {ext})'.format(
958            name=repr(self.name),
959            index=repr(self.index),
960            ext=repr(self.extension))
961
962    def __str__(self):
963        if self.index is None:
964            i = ''
965        else:
966            i = '[{i}]'.format(i=to_str(self.index))
967        return '{name}{index}{ext}'.format(
968            name=self.name,
969            index=i,
970            ext='' if self.extension is None else self.extension)
971
972
973class Integer(Terminal):
974    def __bool__(self):
975        return bool(int(self.value))
976
977
978class Bool(Terminal):
979    def __init__(self, val):
980        self.value = val.upper() == 'TRUE'
981
982    def __bool__(self):
983        return self.value
984
985    def __repr__(self):
986        return 'Bool({value})'.format(value=repr(self.value))
987
988    def __str__(self):
989        return str(self.value)
990
991
992class RemoteRef(Terminal):
993    def __init__(self, proctype, label, pid=None):
994        self.proctype = proctype
995        self.label = label
996        self.pid = pid
997
998    def __repr__(self):
999        return 'RemoteRef({proc}, {label}, {pid})'.format(
1000            proc=self.proctype, label=self.label, pid=self.pid)
1001
1002    def __str__(self):
1003        if self.pid is None:
1004            inst = ''
1005        else:
1006            inst = '[{pid}]'.format(pid=self.pid)
1007        return '{proc} {inst} @ {label}'.format(
1008            proc=self.proctype, inst=inst, label=self.label)
1009
1010
1011def dump_graph(g, fname='a.pdf', node_label='label',
1012               edge_label='label', relabel=False):
1013    """Write the program graph, annotated with formulae, to PDF file."""
1014    # map nodes to integers
1015    if relabel:
1016        mapping = {u: i for i, u in enumerate(g)}
1017        g = nx.relabel_nodes(g, mapping)
1018        inv_mapping = {v: k for k, v in mapping.items()}
1019        s = list()
1020        s.append('mapping of nodes:')
1021        for k in sorted(inv_mapping):
1022            v = inv_mapping[k]
1023            s.append('{k}: {v}'.format(k=k, v=v))
1024        print('\n'.join(s))
1025    h = nx.MultiDiGraph()
1026    for u, d in g.nodes(data=True):
1027        label = d.get(node_label, u)
1028        label = '"{label}"'.format(label=label)
1029        h.add_node(u, label=label)
1030    for u, v, d in g.edges(data=True):
1031        label = d.get(edge_label, ' ')
1032        label = '"{label}"'.format(label=label)
1033        h.add_edge(u, v, label=label)
1034    pd = nx.drawing.nx_pydot.to_pydot(h)
1035    pd.write_pdf(fname)
Note: See TracBrowser for help on using the repository browser.