-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathexport_dot.py
86 lines (70 loc) · 2.81 KB
/
export_dot.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
from mts import MTS
import logging
from itertools import chain
log = logging.getLogger(__name__)
def modal_to_dot(path, mts: MTS, mc: bool = False, derive_groups: bool = False):
class_text = 'digraph'
states = []
state_mapping = {}
uid = 0
initial_states = list(mts.state_view(lambda x: x['initial'], lambda x: x))
if len(initial_states) != 1:
log.warning(f'Found multiple initial states: {initial_states}')
for state in sorted(mts.states, key=lambda x: 0 if x['initial'] else 1):
state_mapping[state['id']] = uid
states.append(
's{id} [shape="circle" label="{label}"];'.format(id=uid, label=state['id'])
)
uid += 1
red_transitions = 0
def derive_group(transition):
nonlocal red_transitions
if transition['green']:
return 0
elif transition['red']:
red_transitions += 1
return red_transitions
else:
return -1
transitions = []
for transition in mts.transitions:
transitions.append(
gen_mts_transition(state_mapping, transition) if not mc else
gen_mc_transition(state_mapping, transition, **{'group': derive_group(transition)} if derive_groups else {})
)
with open(path, 'wt') as f:
f.write(f'{class_text} g {{\n\n')
for s in states:
f.write('\t' + s + '\n')
f.write('\n')
for t in transitions:
f.write('\t' + t + '\n')
f.write('\n')
f.write('__start0 [label="" shape="none" width="0" height="0"];\n')
f.write('__start0 -> s0;\n')
f.write('}\n')
def gen_mts_transition(state_mapping, transition):
return 's{src} -> s{dest} [modality="{mod}", style="{style}", label="{label}"];'.format(
src=state_mapping[transition["src"]],
dest=state_mapping[transition["dest"]],
mod="MUST" if transition["must"] else "MAY",
style="strict" if transition["must"] else "dashed",
label=transition["label"]
)
def gen_mc_transition(state_mapping, transition, **kwargs):
options = {
'src': state_mapping[transition["src"]],
'dest': state_mapping[transition["dest"]],
'mod': "MUST" if transition["must"] else "MAY",
'style': "strict" if transition["must"] else "dashed",
'label': transition["label"],
'color': 'color="green"' if transition["green"] else
('color="red"' if transition["red"] else ''),
'contract': 'GREEN' if transition["green"] else
('RED' if transition["red"] else 'NONE'),
'group': transition["group"] if "group" in transition else "-1"
}
options.update(kwargs)
return 's{src} -> s{dest} [modality="{mod}", style="{style}", {color} contract="{contract}", group="{group}", label="{label}"];'.format(
**options
)