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

fix is_generalized_rabin() and is_generalized_streett()

Browse source 
* spot/twa/acc.cc: Fix detection of single-pairs gen-Rabin and
gen-Streett.
* tests/core/randaut.test: Add test case.
* NEWS: Mention this issue.
This commit is contained in:
Alexandre Duret-Lutz 2020-02-15 10:05:27 +01:00
parent 6a988f6884
commit bf42b19eff
3 changed files with 37 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -99,6 +99,10 @@ New in spot 2.8.5.dev (not yet released)
- Some formulas with Boolean sub-formulas equivalent to true or - Some formulas with Boolean sub-formulas equivalent to true or
false could be translated into automata with false labels. false could be translated into automata with false labels.
- The HOA printer would incorrectly output the condition such
'Fin(1) & Inf(2) & Fin(0)' as 'Fin(0) | Fin(1) & Inf(2)'
due to a bug in the is_generalized_rabin() matching function.
New in spot 2.8.5 (2020-01-04) New in spot 2.8.5 (2020-01-04)
Bugs fixed: Bugs fixed:

18
spot/twa/acc.cc
View file

@ -681,15 +681,21 @@ namespace spot
// generalized Rabin should start with Or, unless // generalized Rabin should start with Or, unless
// it has a single pair. // it has a single pair.
bool singlepair = false;
{ {
auto topop = code_.back().sub.op; auto topop = code_.back().sub.op;
if (topop == acc_op::And) if (topop == acc_op::And)
{
// Probably single-pair generalized-Rabin. Shift the source // Probably single-pair generalized-Rabin. Shift the source
// by one position as if we had an invisible Or in front. // by one position as if we had an invisible Or in front.
++s; ++s;
singlepair = true;
}
else if (topop != acc_op::Or) else if (topop != acc_op::Or)
{
return false; return false;
} }
}
// Each pair 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.
@ -752,7 +758,8 @@ namespace spot
} }
for (auto i: p) for (auto i: p)
pairs.emplace_back(i.second); pairs.emplace_back(i.second);
return (!(seen_fin & seen_inf) return ((!singlepair || pairs.size() == 1)
&& !(seen_fin & seen_inf)
&& (seen_fin | seen_inf) == all_sets()); && (seen_fin | seen_inf) == all_sets());
} }
@ -776,15 +783,21 @@ namespace spot
// generalized Streett should start with And, unless // generalized Streett should start with And, unless
// it has a single pair. // it has a single pair.
bool singlepair = false;
{ {
auto topop = code_.back().sub.op; auto topop = code_.back().sub.op;
if (topop == acc_op::Or) if (topop == acc_op::Or)
{
// Probably single-pair generalized-Streett. Shift the source // Probably single-pair generalized-Streett. Shift the source
// by one position as if we had an invisible And in front. // by one position as if we had an invisible And in front.
++s; ++s;
singlepair = true;
}
else if (topop != acc_op::And) else if (topop != acc_op::And)
{
return false; return false;
} }
}
// Each pairs is the position of a Inf followed // Each pairs is the position of a Inf followed
@ -847,7 +860,8 @@ namespace spot
} }
for (auto i: p) for (auto i: p)
pairs.emplace_back(i.second); pairs.emplace_back(i.second);
return (!(seen_inf & seen_fin) return ((!singlepair || pairs.size() == 1)
&& !(seen_inf & seen_fin)
&& (seen_inf | seen_fin) == all_sets()); && (seen_inf | seen_fin) == all_sets());
} }

10
tests/core/randaut.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et # Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -221,4 +221,12 @@ grep 'randaut:.*end of acceptance.*invalid range' stderr
randaut -Q0 1 2>stderr && exit 1 randaut -Q0 1 2>stderr && exit 1
grep '0 states' stderr grep '0 states' stderr
# This catch a bug where 'Fin(1) & Inf(2) & Fin(0)' was
# incorrectly detected a generalized-Rabin and output a
# 'Fin(0) | Fin(1) & Inf(2)'.
randaut -Q1 -A 'Fin(1) & Inf(2) & Fin(0)' 2 > out.hoa
grep 'Acceptance:' out.hoa > out.acc
echo 'Acceptance: 3 Fin(1) & Inf(2) & Fin(0)' > out.exp
diff out.acc out.exp
: :