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

fix is_generalized_rabin() and is_generalized_streett()

Browse source 
Fixes #325.

* spot/twa/acc.cc: Here.
* tests/core/accsimpl.test: New test case.
* NEWS: Mention the issue.
This commit is contained in:
Alexandre Duret-Lutz 2018-02-16 16:34:08 +01:00
parent 9ec6e9172c
commit 5a2e4f54c5
3 changed files with 36 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -12,6 +12,12 @@ New in spot 2.5.0.dev (not yet released)
- iar() and iar_maybe() properly handle Rabin-like conditions. - iar() and iar_maybe() properly handle Rabin-like conditions.
- is_generalized_rabin() had a typo that caused some non-simplified
acceptance conditions like Fin(0)|(Fin(0)&Inf(1)) to be
incorrectly detecteded as generalized-Rabin 2 0 1 and then output
as Fin(0)|(Fin(1)&Inf(2)) instead. Likewise for
is_generalized_streett
New in spot 2.5 (2018-01-20) New in spot 2.5 (2018-01-20)
Build: Build:

13
spot/twa/acc.cc
View file

@ -666,7 +666,7 @@ namespace spot
auto s = code_.back().sub.size; auto s = code_.back().sub.size;
acc_cond::mark_t seen_fin = 0U; acc_cond::mark_t seen_fin = 0U;
acc_cond::mark_t seen_inf = 0U; acc_cond::mark_t seen_inf = 0U;
// Each pairs is the position of a Fin followed // Each pair is the position of a Fin followed
// by the number of Inf. // by the number of Inf.
std::map<unsigned, unsigned> p; std::map<unsigned, unsigned> p;
while (s) while (s)
@ -697,7 +697,7 @@ namespace spot
unsigned i = m2.count(); unsigned i = m2.count();
// If we have seen this pair already, it must have the // If we have seen this pair already, it must have the
// same size. // same size.
if (p.emplace(m1.max_set(), i).first->second != i) if (p.emplace(m1.max_set() - 1, i).first->second != i)
return false; return false;
assert(i > 0); assert(i > 0);
unsigned j = m1.max_set(); // == n+1 unsigned j = m1.max_set(); // == n+1
@ -705,7 +705,6 @@ namespace spot
if (!m2.has(j++)) if (!m2.has(j++))
return false; return false;
while (--i); while (--i);
seen_fin |= m1; seen_fin |= m1;
seen_inf |= m2; seen_inf |= m2;
} }
@ -715,8 +714,10 @@ namespace spot
for (auto s: m1.sets()) for (auto s: m1.sets())
// If we have seen this pair already, it must have the // If we have seen this pair already, it must have the
// same size. // same size.
if (p.emplace(s, 0U).first->second != 0U) {
return false; if (p.emplace(s, 0U).first->second != 0U)
return false;
}
seen_fin |= m1; seen_fin |= m1;
} }
else else
@ -777,7 +778,7 @@ namespace spot
unsigned i = m2.count(); unsigned i = m2.count();
// If we have seen this pair already, it must have the // If we have seen this pair already, it must have the
// same size. // same size.
if (p.emplace(m1.max_set(), i).first->second != i) if (p.emplace(m1.max_set() - 1, i).first->second != i)
return false; return false;
assert(i > 0); assert(i > 0);
unsigned j = m1.max_set(); // == n+1 unsigned j = m1.max_set(); // == n+1

23
tests/core/accsimpl.test
View file

@ -28,3 +28,26 @@ set -e
ltlcross -f FGa \ ltlcross -f FGa \
'ltl2tgba -G -D %f | autfilt --complement >%O' \ 'ltl2tgba -G -D %f | autfilt --complement >%O' \
'ltl2tgba -G -D %f | autfilt --complement | autfilt --simplify-acceptance >%O' 'ltl2tgba -G -D %f | autfilt --complement | autfilt --simplify-acceptance >%O'
cat >325 <<EOF
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
acc-name: Rabin 3
Acceptance: 6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[!0&!1] 0 {0 4}
[!0&1] 0 {0 3 4}
[0&!1] 0 {2 5}
[0&1] 0 {1 2 5}
--END--
EOF
autfilt --simplify-acceptance 325 > 325s
exp='4 Fin(0) | (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))'
test "$exp" = "`autfilt --stats='%a %g' 325s`"