-
Notifications
You must be signed in to change notification settings - Fork 0
/
spec_parser.py
135 lines (104 loc) · 4.81 KB
/
spec_parser.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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
import re
from itertools import chain
from python_ext import find_all
from structs import SmvModule, PropertySpec, SpecType
# list of all possible system and environment specifications
SPECS = list(chain(*[("ENV_{}".format(spec), "SYS_{}".format(spec)) for spec in SpecType.__members__]))
def get_all_sections(lines, section_name):
inside_section = False
sections = list()
cur_data = None
for l in lines:
if not l.strip():
continue
if is_section_declaration(l) and inside_section:
sections.append(cur_data)
inside_section = False
if inside_section:
cur_data.append(l)
if l.strip() == section_name:
inside_section = True
cur_data = list()
def is_section_declaration(l):
return l.strip() and l.split()[0].strip() in SPECS + ['VAR', 'DEFINE', 'MODULE']
def get_spec_type_for_section(section_declaration: str) -> SpecType:
assert section_declaration.endswith("_SPEC")
assert section_declaration.startswith("SYS_") or section_declaration.startswith("ENV_")
spec_name = section_declaration[4:] # magic
return SpecType[spec_name]
def is_guarantee(section_declaration: str) -> bool:
return section_declaration.startswith("SYS_")
def parse_smv_module(module_lines, base_dir) -> (SmvModule, list, list):
lines_without_spec = []
assumptions = []
guarantees = []
module_name = module_inputs = None
now_parsing = False
is_parsing_guarantees = None
desc = None
for l_raw in module_lines:
l = l_raw.strip()
if not l:
if not now_parsing:
lines_without_spec.append(l_raw)
continue
if l.startswith('--'):
if not now_parsing:
lines_without_spec.append(l_raw)
else:
match = re.fullmatch("(?:--| )*#(?:name|desc):? +([\w_]+).*", l, flags=re.ASCII)
if match:
desc = match.groups()[0]
continue
if is_section_declaration(l):
if l.endswith("_SPEC"):
now_parsing = True
is_parsing_guarantees = is_guarantee(l)
spec_type = get_spec_type_for_section(l)
elif 'MODULE' in l:
# simple parser: assumes all inputs on the same line:
match = re.fullmatch('MODULE *([\w_@\.]+) *(\([\w_@\. ,]*\))? *(?:--.*)*', l)
assert match, 'unknown format\n' + l
assert len(match.groups()) == 2, 'unknown format\n' + l
module_name = match.groups()[0]
inputs_token = match.groups()[1]
module_inputs = re.findall('[\w_\.@]+', inputs_token or '')
else:
now_parsing = False
else:
if now_parsing:
if spec_type == SpecType.AUTOMATON_SPEC:
file_name = re.fullmatch('!? *([\w_\-\.]+\.gff).*', l).groups()[0]
data = PropertySpec(file_name,
not l.startswith('!'),
is_parsing_guarantees,
base_dir + '/' + file_name,
spec_type)
elif spec_type == SpecType.ORE_SPEC:
is_false = l.startswith("!(") and l.endswith(")")
data = PropertySpec(l, not is_false, is_parsing_guarantees,
l if not is_false else l[2:-1], spec_type)
elif spec_type in [SpecType.LTL_SPEC, SpecType.PLTL_SPEC]:
data = PropertySpec(l, True, is_parsing_guarantees, l, spec_type)
else:
assert False, "SpecType " + str(spec_type) + " can not be handled."
if desc:
data.desc = desc
desc = None
(assumptions, guarantees)[is_parsing_guarantees].append(data)
if not now_parsing:
lines_without_spec.append(l_raw)
module = SmvModule(module_name, module_inputs, '', '\n'.join(lines_without_spec), False, False)
return module, assumptions, guarantees
def parse_smv(smv_lines: list, base_dir) -> {str: (SmvModule, list, list)}: # {module_name: Specification}
lines_a_g_by_module_name = dict()
module_start_indices = find_all(lambda l: l.startswith('MODULE'), smv_lines)
for i, start in enumerate(module_start_indices):
if i != len(module_start_indices) - 1:
end = module_start_indices[i + 1]
else:
end = len(smv_lines)
module_without_spec, assumptions, guarantees = \
parse_smv_module(smv_lines[start:end], base_dir)
lines_a_g_by_module_name[module_without_spec.name] = (module_without_spec, assumptions, guarantees)
return lines_a_g_by_module_name