alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlsynt: fix --global-equiv

Browse source 
Fixes #557.

* spot/tl/apcollect.cc (realizability_simplifier): When detecting
global equivalence such as o1 := i2, the left is always an output, so
it should never be marked as input.
* tests/core/ltlsynt.test: Add test case.
This commit is contained in:
Alexandre Duret-Lutz 2024-01-26 22:31:17 +01:00
parent 690e5a213d
commit dc5a569582
2 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
spot/tl/apcollect.cc
View file

@ -411,9 +411,9 @@ namespace spot
continue; continue;
SPOT_ASSUME(lit != nullptr); SPOT_ASSUME(lit != nullptr);
if (lit.is(spot::op::Not)) if (lit.is(spot::op::Not))
add_to_mapping(lit[0], repr_is_input, not_repr); add_to_mapping(lit[0], false, not_repr);
else else
add_to_mapping(lit, repr_is_input, repr); add_to_mapping(lit, false, repr);
rm_has_new_terms = true; rm_has_new_terms = true;
} }
} }

12
tests/core/ltlsynt.test
View file

@ -1109,4 +1109,14 @@ diff out expected
f1="((G ((p0) <-> (! (p1)))) && (((((F ((b) && (G (F (a))))) ||\ f1="((G ((p0) <-> (! (p1)))) && (((((F ((b) && (G (F (a))))) ||\
(F ((c) && (G (F (! (a))))))) && (F (b))) && (F (c))) <-> (G (F (p0)))))" (F ((c) && (G (F (! (a))))))) && (F (b))) && (F (c))) <-> (G (F (p0)))))"
ltlsynt -f "$f1" --outs="p1, p0" --aiger > /dev/null ltlsynt -f "$f1" --outs="p1, p0" --aiger > /dev/null
# issue #557
ltlsynt -f 'G(in1 <-> out0) & G(in0 <-> out1)' --ins=in1,in0 --verb 2>err >out
grep := err > err2
cat >err2.ex <<EOF
out0 := in1
out1 := in0
EOF
diff err2 err2.ex
grep -F '[!0&!1&!2&!3 | !0&!1&2&3 | 0&1&!2&!3 | 0&1&2&3] 0' out