diff --git a/NEWS b/NEWS index 76f850ac8..e8485acee 100644 --- a/NEWS +++ b/NEWS @@ -99,6 +99,10 @@ New in spot 2.8.5.dev (not yet released) - Some formulas with Boolean sub-formulas equivalent to true or 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) Bugs fixed: diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 3ef185403..9b946f48a 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -681,14 +681,20 @@ namespace spot // generalized Rabin should start with Or, unless // it has a single pair. + bool singlepair = false; { auto topop = code_.back().sub.op; if (topop == acc_op::And) - // Probably single-pair generalized-Rabin. Shift the source - // by one position as if we had an invisible Or in front. - ++s; + { + // Probably single-pair generalized-Rabin. Shift the source + // by one position as if we had an invisible Or in front. + ++s; + singlepair = true; + } else if (topop != acc_op::Or) - return false; + { + return false; + } } // Each pair is the position of a Fin followed @@ -752,7 +758,8 @@ namespace spot } for (auto i: p) 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()); } @@ -776,14 +783,20 @@ namespace spot // generalized Streett should start with And, unless // it has a single pair. + bool singlepair = false; { auto topop = code_.back().sub.op; if (topop == acc_op::Or) - // Probably single-pair generalized-Streett. Shift the source - // by one position as if we had an invisible And in front. - ++s; + { + // Probably single-pair generalized-Streett. Shift the source + // by one position as if we had an invisible And in front. + ++s; + singlepair = true; + } else if (topop != acc_op::And) - return false; + { + return false; + } } @@ -847,7 +860,8 @@ namespace spot } for (auto i: p) 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()); } diff --git a/tests/core/randaut.test b/tests/core/randaut.test index 6707eb050..ea432ec3f 100755 --- a/tests/core/randaut.test +++ b/tests/core/randaut.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- 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). # # 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 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 + :