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

simplify: fix handling of keep_top_xor

Browse source 
Under that option, !(a ^ b) was converted
to (!a <=> !b) instead of simply (a <=> b).

* spot/tl/simplify.cc (equiv_or_xor): Improve
rewriting.
* tests/core/ltl2tgba2.test, tests/python/simstate.py: Adjust test
cases.
This commit is contained in:
Alexandre Duret-Lutz 2020-07-22 16:23:34 +02:00
parent 2ce84f7889
commit 2c267cac40
4 changed files with 19 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

9
NEWS
View file

@ -1,19 +1,22 @@
New in spot 2.9.3.dev (not yet released)
Nothing yet.
Bugs fixed:
- Handle xor and <-> in a more natural way when translating
LTL formulas to generic acceptancee conditions.
New in spot 2.9.3 (2020-07-22)
Bug fixed:
- Completely fix the ltlcross issue mentionned in previous release.
- Completely fix the ltlcross issue mentioned in previous release.
New in spot 2.9.2 (2020-07-21)
Bugs fixed:
- ltlcross --csv=... --product=N with N>0 could output spurious
diagnosics claiming that words were rejected when evaluating
diagnostics claiming that words were rejected when evaluating
the automaton on state-space.
- spot::scc_info::determine_unknown_acceptance() now also update the

16
spot/tl/simplify.cc
View file

@ -431,12 +431,12 @@ namespace spot
if (equiv)
{
// Rewrite a<=>b as (a&b)|(!a&!b)
auto recurse_f1_true = rec(f1, true);
auto recurse_f2_true = rec(f2, true);
if (!deep && c->options.keep_top_xor)
return formula::Equiv(recurse_f1_true, recurse_f2_true);
auto recurse_f1_false = rec(f1, false);
auto recurse_f2_false = rec(f2, false);
if (!deep && c->options.keep_top_xor)
return formula::Equiv(recurse_f1_false, recurse_f2_false);
auto recurse_f1_true = rec(f1, true);
auto recurse_f2_true = rec(f2, true);
auto left = formula::And({recurse_f1_false, recurse_f2_false});
auto right = formula::And({recurse_f1_true, recurse_f2_true});
return formula::Or({left, right});
@ -444,12 +444,12 @@ namespace spot
else
{
// Rewrite a^b as (a&!b)|(!a&b)
auto recurse_f1_true = rec(f1, true);
auto recurse_f2_true = rec(f2, true);
if (!deep && c->options.keep_top_xor)
return formula::Xor(recurse_f1_true, recurse_f2_true);
auto recurse_f1_false = rec(f1, false);
auto recurse_f2_false = rec(f2, false);
if (!deep && c->options.keep_top_xor)
return formula::Xor(recurse_f1_false, recurse_f2_false);
auto recurse_f1_true = rec(f1, true);
auto recurse_f2_true = rec(f2, true);
auto left = formula::And({recurse_f1_false, recurse_f2_true});
auto right = formula::And({recurse_f1_true, recurse_f2_false});
return formula::Or({left, right});

4
tests/core/ltl2tgba2.test
View file

@ -453,9 +453,9 @@ test 1,3,2 = `ltl2tgba -G -D "(GFp0 | FGp1)" --stats=%s,%e,%a`
# Handling of Xor and <-> by ltl-split and -D -G.
res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) <-> GFe)' --stats='%s %g'`
test "$res" = "17 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))"
res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'`
test "$res" = "17 (Inf(0)&Inf(1)) | (Fin(0) & Fin(1))"
res=`ltl2tgba -D -G 'X((Fa & Fb & Fc & Fd) ^ GFe)' --stats='%s %g'`
test "$res" = "17 (Inf(0) & Fin(1)) | (Fin(0) & Inf(1))"
ltlcross 'ltl2tgba -D -G' 'ltl2tgba -G' -f '(Fa & Fb & Fc & Fd) ^ GFe'
f='G(p1 | G!p0) M Xp1'

6
tests/python/simstate.py
View file

@ -178,13 +178,13 @@ b.copy_state_names_from(a)
assert b.to_str() == """HOA: v1
States: 1
Start: 0
AP: 2 "p1" "p0"
AP: 2 "p0" "p1"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0 "[1,7]"
[!0] 0 {0}
[0] 0
[!1] 0 {0}
[1] 0
--END--"""