Franck Pommereau / snakes

Go to a project
Toggle navigation Toggle navigation pinning
Franck Pommereau
25f1cba8 1 parent c678ba6b

fixed CTL* and/or

Inline Side-by-side
Showing 4 changed files with 25 additions and 123 deletions
......@@ -14,8 +14,8 @@ ctl_param: NAME ( '=' '@' STRING+ | ':' NAME )
ctl_formula: ctl_or_formula [ ctl_connector ctl_or_formula ]
ctl_connector: ( '=' '>' | '<=' '>' )
ctl_or_formula: ctl_and_formula [ 'or' ctl_and_formula ]
ctl_and_formula: ctl_not_formula [ 'and' ctl_not_formula ]
ctl_or_formula: ctl_and_formula ('or' ctl_and_formula)*
ctl_and_formula: ctl_not_formula ('and' ctl_not_formula)*
ctl_not_formula: ('not' ctl_not_formula | ctl_binary_formula)
ctl_binary_formula: ctl_unary_formula [ ctl_binary_op ctl_unary_formula ]
ctl_unary_formula: [ ctl_unary_op ] (ctl_atom_formula | '(' ctl_formula ')')
......
......@@ -231,23 +231,35 @@ class Translator (PyTranslator) :
col_offset=st.scol)
def do_ctl_or_formula (self, st, ctx) :
"""ctl_or_formula: ctl_and_formula [ 'or' ctl_and_formula ]
"""ctl_or_formula: ctl_and_formula ('or' ctl_and_formula)*
-> ast.form
<<< True or False
'Spec(atoms=[], properties=[], main=CtlBinary(op=Or(), left=Boolean(val=True), right=Boolean(val=False)))'
<<< True or False or True
'Spec(atoms=[], properties=[], main=CtlBinary(op=Or(), left=CtlBinary(op=Or(), left=Boolean(val=True), right=Boolean(val=False)), right=Boolean(val=True)))'
<<< True or False or False and True and False
'Spec(atoms=[], properties=[], main=CtlBinary(op=Or(), left=CtlBinary(op=Or(), left=Boolean(val=True), right=Boolean(val=False)), right=CtlBinary(op=And(), left=CtlBinary(op=And(), left=Boolean(val=False), right=Boolean(val=True)), right=Boolean(val=False))))'
"""
if len(st) == 1 :
return self.do(st[0], ctx)
else :
op = self._ctl_binary_op[st[1].text](lineno=st[1].srow,
col_offset=st[1].scol)
return self.ST.CtlBinary(lineno=st.srow, col_offset=st.scol,
op=op,
left=self.do(st[0], ctx),
right=self.do(st[2], ctx))
values = [self.do(child, ctx) for child in st[::2]]
ops = [self._ctl_binary_op[child.text](lineno=child.srow,
col_offset=child.scol)
for child in st[1::2]]
while len(values) > 1 :
left = values.pop(0)
right = values.pop(0)
operator = ops.pop(0)
values.insert(0, self.ST.CtlBinary(lineno=st.srow,
col_offset=st.scol,
left=left,
op=operator,
right=right))
return values[0]
def do_ctl_and_formula (self, st, ctx) :
"""ctl_and_formula: ctl_not_formula [ 'and' ctl_not_formula ]
"""ctl_and_formula: ctl_not_formula ('and' ctl_not_formula)*
-> ast.form
<<< True and False
......
......@@ -665,62 +665,7 @@ grammar = ([(256,
-1,
2433]),
0),
([(28, 2), (0, 1)], (29, 28, [2]), 1),
([(27, 3)],
(58,
8,
[2435,
2435,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
2435,
-1,
-1,
-1,
-1,
-1,
2435,
2435,
2435,
2435,
2435,
-1,
-1,
-1,
2435,
-1,
2435,
2435,
-1,
2435,
2435,
2435,
-1,
2435,
-1,
-1,
2435]),
0),
([(0, 3)], (0, 0, []), 1)]),
([(28, 0), (0, 1)], (29, 28, [0]), 1)]),
(265,
'ctl_and_formula',
0,
......@@ -778,62 +723,7 @@ grammar = ([(256,
-1,
2689]),
0),
([(30, 2), (0, 1)], (31, 30, [2]), 1),
([(29, 3)],
(58,
8,
[2691,
2691,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
-1,
2691,
-1,
-1,
-1,
-1,
-1,
2691,
2691,
2691,
2691,
2691,
-1,
-1,
-1,
2691,
-1,
2691,
2691,
-1,
2691,
2691,
2691,
-1,
2691,
-1,
-1,
2691]),
0),
([(0, 3)], (0, 0, []), 1)]),
([(30, 0), (0, 1)], (31, 30, [0]), 1)]),
(266,
'ctl_not_formula',
0,
......
......@@ -105,7 +105,7 @@ class Translator (object) :
if len(st) == 1 :
return self.do(st[0], ctx)
else :
values=[self.do(child, ctx) for child in st[::2]]
values = [self.do(child, ctx) for child in st[::2]]
ops = [(self._binary[child.text], child) for child in st[1::2]]
while len(values) > 1 :
left = values.pop(0)
......