-
Notifications
You must be signed in to change notification settings - Fork 1
/
NodeActionsParse.py
205 lines (174 loc) · 13.2 KB
/
NodeActionsParse.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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
import argparse
from sys import exit as sys_exit
from lxml import etree # https://lxml.de/xpathxslt.html
r'''
The algorithm:
---Required-Definitions---
1) Get UIDs of [], [Act], \E, and \in operators.
2) Check if there is an entry with the operators [][Act], and an operand that is supposedly the formula Next.
3) Check if Next definition exists and if it contains \E X \in Y: Action(X).
4) Check if the set Y is a defined constant.
---Application-Properties---
5) Check if there is an ASSUME Y # {} statement.
6) Check if for every true statement Action(Z) the parameter Z is in the set Y.
'''
DESCRIPTION = '''
A script for analyzing the Node Actions guideline application.
Requires an .xml file generated by the tla2sany.xml.XMLExporter.java class from tla2tools.
'''
OP_EXISTS = '$BoundedExists'
OP_FOR_ALL = '$BoundedForall'
OP_EMPTY_SET = '$SetEnumerate'
OP_NOT_EQUAL = '/='
OP_ALWAYS = '[]'
OP_ACT_SQUARE = '$SquareAct'
OPERATORS_DICT = {OP_EXISTS: '', OP_FOR_ALL: '', OP_EMPTY_SET: '', OP_NOT_EQUAL: '', OP_ALWAYS: '', OP_ACT_SQUARE : ''}
CONSTANT_DECLARATION_KIND = '2'
# Stop the execution of the algorithm.
def stop_algorithm(message):
print(message)
sys_exit('Algorithm stopped.')
# Returns the unique name of a definition with a specified UID.
def get_def_uname(def_uid, xml_root):
return xml_root.xpath('//entry[UID=$uid]/*/uniquename/text()',
uid=def_uid, smart_strings=False)[0]
# Returns the line number(s) of a definition with a specified UID.
def get_def_line_number(def_uid, xml_root):
return xml_root.xpath('concat(//entry[UID=$uid]/*/location/line/begin/text(), \'-\', //entry[UID=$uid]/*/location/line/end/text())',
uid=def_uid, smart_strings=False)
# Find the UIDs of the required operators.
def get_operator_uids(operator_dict, xml_root):
for op_key in operator_dict.keys():
op_uid = xml_root.xpath('//entry[BuiltInKind/uniquename=$operator]/UID/text()',
operator=op_key, smart_strings=False)
if op_uid:
operator_dict[op_key] = op_uid[0]
else:
stop_algorithm(f'Operator {op_key} was not found...')
print(f'Gathered UIDs of required operators: {operator_dict}')
# Find any [][Act] entries and their definition uids.
def get_act_uids(operator_dict, xml_root):
act_uids = xml_root.xpath('//OpApplNode[operator/BuiltInKindRef/UID=$always_uid]/operands/OpApplNode[operator/ \
BuiltInKindRef/UID=$act_square_uid]/operands/OpApplNode[1]/operator/UserDefinedOpKindRef/UID/text()',
always_uid = operator_dict[OP_ALWAYS], act_square_uid = operator_dict[OP_ACT_SQUARE], smart_strings=False)
if not act_uids:
stop_algorithm('Weren\'t able to find any statements of the form [][Act].')
else:
print(f'Found [][Act] statements and possible action Next UIDs: {act_uids}')
return act_uids
# Get a definition of a formula with the specified UID.
def get_def(uid, xml_root):
defElement = xml_root.xpath('//entry[UID=$def_uid]/UserDefinedOpKind', def_uid = uid)
if not defElement:
stop_algorithm(f'Couldn\'t find the definition of the formula with the UID {uid}.')
else:
return defElement[0]
# Return a tuple of a set's UID and an operator's UID that are in an [][Act] entry that complies with all required definitions.
def get_valid_act_uids(act_uids, operator_dict, constant_kind, xml_root):
for act_uid in act_uids:
operator_uids = xml_root.xpath('//entry[UID=$def_uid]/UserDefinedOpKind//OpApplNode[operator/BuiltInKindRef/UID=$exists_id]// \
operands/OpApplNode/operator/UserDefinedOpKindRef/UID/text()',
def_uid=act_uid, exists_id=operator_dict[OP_EXISTS], smart_strings=False)
for operator_uid in operator_uids:
print(f'In the definition of an action {get_def_uname(act_uid, xml_root)} (UID {act_uid}) with ∃, found a defined operator {get_def_uname(operator_uid, xml_root)} with UID {operator_uid}')
print(f'Checking if the operator {get_def_uname(operator_uid, xml_root)} has a parameter...')
operator_param_uid = xml_root.xpath('//entry[UID=$def_uid]/UserDefinedOpKind//OpApplNode[operator/BuiltInKindRef/UID=$exists_id]// \
operands/OpApplNode[operator/UserDefinedOpKindRef/UID=$op_uid]/operands/OpApplNode/operator/ \
FormalParamNodeRef/UID/text()',
def_uid=act_uid, exists_id=operator_dict[OP_EXISTS], op_uid=operator_uid, smart_strings=False)
if operator_param_uid:
operator_param_uid = operator_param_uid[0]
print(f'Found a parameter {get_def_uname(operator_param_uid, xml_root)} with UID {operator_param_uid}.')
print(f'Checking if parameter {get_def_uname(operator_param_uid, xml_root)} is bounded by ∃...')
bounded_param = xml_root.xpath('//entry[UID=$def_uid]/UserDefinedOpKind//OpApplNode[operator/BuiltInKindRef/UID=$exists_id]/ \
boundSymbols[bound/FormalParamNodeRef/UID=$op_param_uid]',
def_uid=act_uid, exists_id=operator_dict[OP_EXISTS], op_param_uid=operator_param_uid)
if bounded_param:
print(f'Parameter {get_def_uname(operator_param_uid, xml_root)} with UID {operator_param_uid} is bounded by ∃.')
print(f'Checking if a constant that is a set is bounded by the same ∃...')
bounded_set_uid = xml_root.xpath('//entry[UID=$def_uid]/UserDefinedOpKind//OpApplNode[operator/BuiltInKindRef/UID=$exists_id]/ \
boundSymbols/bound/OpApplNode/operator/OpDeclNodeRef/UID/text()',
def_uid=act_uid, exists_id=operator_dict[OP_EXISTS], smart_strings=False)
if bounded_set_uid:
bounded_set_uid = bounded_set_uid[0]
print(f'Set {get_def_uname(bounded_set_uid, xml_root)} with UID {bounded_set_uid} is bounded by the same ∃.')
print(f'Checking if the set {get_def_uname(bounded_set_uid, xml_root)} is a defined constant...')
set_constant = xml_root.xpath('//entry[UID=$set_uid]/OpDeclNode[kind=$const_kind]',
set_uid=bounded_set_uid, const_kind=constant_kind)
if set_constant:
print(f'Set {get_def_uname(bounded_set_uid, xml_root)} with UID {bounded_set_uid} is a defined constant.')
print('All required definitions for the Node Actions guideline are present in the TLA+ specification!')
print(f'Set {get_def_uname(bounded_set_uid, xml_root)} with required definitions is defined in line(s) {get_def_line_number(bounded_set_uid, xml_root)}')
print(f'Operator {get_def_uname(operator_uid, xml_root)} with required definitions is defined in line(s) {get_def_line_number(operator_uid, xml_root)}')
print(f'Action {get_def_uname(act_uid, xml_root)} with required definitions is defined in line(s) {get_def_line_number(act_uid, xml_root)}')
return (bounded_set_uid, operator_uid)
else:
print(f'Parameter {get_def_uname(operator_param_uid, xml_root)} with UID {operator_param_uid} is not bounded by ∃.')
else:
print(f'Operator {get_def_uname(operator_uid, xml_root)} with UID {operator_uid} has no parameter...')
stop_algorithm('No [][Act] statement has the required definitions for the Node Actions guideline.')
# Check if there is an ASSUME statement for ensuring a non-empty set for the set with the specified UID.
def check_assume_statement(set_uid, operator_dict, xml_root):
assume_uid = xml_root.xpath('//entry[AssumeNode/body//OpApplNode[operator/BuiltInKindRef/UID=$not_eq_uid]/operands[OpApplNode[1]/operator/OpDeclNodeRef/UID=$set_uid\
and OpApplNode[2]/operator/BuiltInKindRef/UID=$empty_set_uid]]/UID/text()',
not_eq_uid=operator_dict[OP_NOT_EQUAL], set_uid=set_uid, empty_set_uid=operator_dict[OP_EMPTY_SET],smart_strings=False)
if not assume_uid:
stop_algorithm(f'No ASSUME statement for set {get_def_uname(set_uid, filtered_xml_root)} was found in the TLA+ specification. Node Actions guideline not applied correctly.')
else:
print(f'Non-empty {get_def_uname(set_uid, xml_root)} set ASSUME statement found at line(s) {get_def_line_number(assume_uid[0], xml_root)}')
# Check if a valid operator is always used with a parameter that belongs to the specified set.
def check_operator_usage(operator_uid, set_uid, operator_dict, xml_root):
def_uids = xml_root.xpath('//entry[UserDefinedOpKind//OpApplNode//operands/OpApplNode/operator/UserDefinedOpKindRef/UID=$op_uid]/UID/text()',
op_uid=operator_uid, smart_strings=False)
for def_uid in def_uids:
print(f'Found operator {get_def_uname(operator_uid, xml_root)} usage in the formula {get_def_uname(def_uid, xml_root)} defined in line(s) {get_def_line_number(def_uid, xml_root)}.')
print(f'Checking if operator usage complies with Node Actions guideline application properties...')
no_formal_param = xml_root.xpath('//entry[UID=$def_uid]/UserDefinedOpKind//OpApplNode//operands/OpApplNode[operator/UserDefinedOpKindRef/UID=$op_uid \
and not(operands/OpApplNode/operator/FormalParamNodeRef)]/location/line/begin/text()',
def_uid=def_uid, op_uid=operator_uid, smart_strings=False)
if not no_formal_param:
print(f'Operator {get_def_uname(operator_uid, xml_root)} usage in the formula {get_def_uname(def_uid, xml_root)} is bounded by another operator.')
print(f'Checking if bounded parameters are from the set {get_def_uname(set_uid, xml_root)}...')
invalid_bounded_param = xml_root.xpath('//entry[UID=$def_uid]/UserDefinedOpKind//OpApplNode[operator/BuiltInKindRef/UID and \
./operands/OpApplNode[operator/UserDefinedOpKindRef/UID=$op_uid]/operands/OpApplNode/operator/ \
FormalParamNodeRef/UID=boundSymbols/bound/FormalParamNodeRef/UID and ./boundSymbols/bound/OpApplNode/operator/*/UID!=$set_uid] \
/location/line/*/text()',
def_uid=def_uid, op_uid=operator_uid, set_uid=set_uid, smart_strings=False)
if not invalid_bounded_param:
print(f'Node Actions guideline application in formula {get_def_uname(def_uid, xml_root)} in line(s) {get_def_line_number(def_uid, xml_root)} is correct!')
else:
line_numbers = f'{invalid_bounded_param[0]}-{invalid_bounded_param[1]}'
print(f'Node Actions guideline application in formula {get_def_uname(def_uid, xml_root)} is incorrect at line(s) {line_numbers}')
stop_algorithm(f'Node Actions guideline is not applied correctly in the TLA+ specification.')
else:
print(f'Operator {get_def_uname(operator_uid, xml_root)} usage in the formula {get_def_uname(def_uid, xml_root)} invalidates Node Actions guideline application properties in line {no_formal_param[0]}.')
stop_algorithm(f'Node Actions guideline is not applied correctly in the TLA+ specification.')
# Parse command line arguments.
parser = argparse.ArgumentParser(description=DESCRIPTION)
parser.add_argument('xml_file_path', type=str, help='Path to the .xml file generated by the SANY XMLExporter class.')
args = parser.parse_args()
# Get <context> elements.
try:
xml_root = etree.parse(args.xml_file_path)
except OSError as OSerr:
stop_algorithm(OSerr)
# Get operators UIDS.
get_operator_uids(OPERATORS_DICT, xml_root)
# Get .tla file name for filtering entries and filter them.
tla_file_name = xml_root.xpath('//RootModule/text()')
if not tla_file_name:
stop_algorithm('No RootModule tag present in .xml file for getting name of the TLA+ specification.')
tla_file_name = tla_file_name[0]
node_actions_entries = xml_root.xpath('//entry[*/location/filename=$tla_file]', tla_file=tla_file_name, smart_strings=False)
# Create new valid xml tree with entries only from the specified TLA+ file.
filtered_xml_root = etree.Element('root')
for entry in node_actions_entries:
filtered_xml_root.append(entry)
# Get [][Act] entry uids.
act_uids = get_act_uids(OPERATORS_DICT, filtered_xml_root)
# Get valid set and operator uids.
set_uid, operator_uid = get_valid_act_uids(act_uids, OPERATORS_DICT, CONSTANT_DECLARATION_KIND, filtered_xml_root)
# Check for an ASSUME statement and correct valid operator usage.
check_assume_statement(set_uid, OPERATORS_DICT, filtered_xml_root)
check_operator_usage(operator_uid, set_uid, OPERATORS_DICT, filtered_xml_root)
print(f'Node Actions guideline is applied correctly in the {tla_file_name} TLA+ specification!')