diff --git a/spot/tl/hierarchy.cc b/spot/tl/hierarchy.cc index 2e31148d5..47cfb38a4 100644 --- a/spot/tl/hierarchy.cc +++ b/spot/tl/hierarchy.cc @@ -81,51 +81,50 @@ namespace spot } } - static prcheck - algo_to_perform(bool is_persistence, bool aut_given, prcheck algo) + [[noreturn]] static void invalid_spot_pr_check() { - if (algo == prcheck::PR_Auto) - { - // Check environment variable. - static int val_s = []() - { - try - { - auto s = getenv("SPOT_PR_CHECK"); - return s ? std::stoi(s) : 0; - } - catch (const std::exception& e) - { - throw std::runtime_error("invalid value for SPOT_PR_CHECK " - "(should be 1 or 2)"); - } - }(); + throw std::runtime_error("invalid value for SPOT_PR_CHECK " + "(should be 1 or 2)"); + } - if (val_s == 1) + static prcheck + algo_to_perform(bool is_persistence, bool aut_given) + { + static prcheck env_algo = [&]() + { + int val; + try { - return prcheck::PR_via_CoBuchi; + auto s = getenv("SPOT_PR_CHECK"); + val = s ? std::stoi(s) : 0; } - else if (val_s == 2) + catch (const std::exception& e) { - return prcheck::PR_via_Rabin; + invalid_spot_pr_check(); } - else if (!val_s) + if (val == 0) { if (aut_given && !is_persistence) - return prcheck::PR_via_Rabin; + return prcheck::via_Rabin; else if ((aut_given && is_persistence) || !aut_given) - return prcheck::PR_via_CoBuchi; + return prcheck::via_CoBuchi; else SPOT_UNREACHABLE(); } + else if (val == 1) + { + return prcheck::via_CoBuchi; + } + else if (val == 2) + { + return prcheck::via_Rabin; + } else { - throw std::runtime_error("invalid value for SPOT_PR_CHECK " - "(should be 1 or 2)"); + invalid_spot_pr_check(); } - } - else - return algo; + }(); + return env_algo; } bool @@ -134,17 +133,20 @@ namespace spot if (f.is_syntactic_persistence()) return true; - switch (algo_to_perform(true, aut != nullptr, algo)) + if (algo == prcheck::Auto) + algo = algo_to_perform(true, aut != nullptr); + + switch (algo) { - case prcheck::PR_via_CoBuchi: + case prcheck::via_CoBuchi: return cobuchi_realizable(f, aut ? aut : ltl_to_tgba_fm(f, make_bdd_dict(), true)); - case prcheck::PR_via_Rabin: + case prcheck::via_Rabin: return detbuchi_realizable(ltl_to_tgba_fm(formula::Not(f), make_bdd_dict(), true)); - case prcheck::PR_Auto: + case prcheck::Auto: SPOT_UNREACHABLE(); } @@ -157,18 +159,21 @@ namespace spot if (f.is_syntactic_recurrence()) return true; - switch (algo_to_perform(false, aut != nullptr, algo)) + if (algo == prcheck::Auto) + algo = algo_to_perform(true, aut != nullptr); + + switch (algo) { - case prcheck::PR_via_CoBuchi: + case prcheck::via_CoBuchi: return cobuchi_realizable(formula::Not(f), ltl_to_tgba_fm(formula::Not(f), make_bdd_dict(), true)); - case prcheck::PR_via_Rabin: + case prcheck::via_Rabin: return detbuchi_realizable(aut ? aut : ltl_to_tgba_fm(f, make_bdd_dict(), true)); - case prcheck::PR_Auto: + case prcheck::Auto: SPOT_UNREACHABLE(); } @@ -221,11 +226,11 @@ namespace spot case ocheck::via_WDBA: return is_wdba_realizable(f, aut); case ocheck::via_CoBuchi: - return (is_persistence(f, aut, prcheck::PR_via_CoBuchi) - && is_recurrence(f, aut, prcheck::PR_via_CoBuchi)); + return (is_persistence(f, aut, prcheck::via_CoBuchi) + && is_recurrence(f, aut, prcheck::via_CoBuchi)); case ocheck::via_Rabin: - return (is_persistence(f, aut, prcheck::PR_via_Rabin) - && is_recurrence(f, aut, prcheck::PR_via_Rabin)); + return (is_persistence(f, aut, prcheck::via_Rabin) + && is_recurrence(f, aut, prcheck::via_Rabin)); case ocheck::Auto: SPOT_UNREACHABLE(); } diff --git a/spot/tl/hierarchy.hh b/spot/tl/hierarchy.hh index 2f8181624..fbf024fd9 100644 --- a/spot/tl/hierarchy.hh +++ b/spot/tl/hierarchy.hh @@ -42,9 +42,9 @@ namespace spot /// if !f is cobuchi_realizable. enum class prcheck { - PR_Auto, // FIXME: Remove the useless PR_ prefix since - PR_via_CoBuchi, // we already have a prcheck:: prefix. - PR_via_Rabin, + Auto, + via_CoBuchi, + via_Rabin, }; /// \brief Return true if \a f represents a persistence property. @@ -55,7 +55,7 @@ namespace spot SPOT_API bool is_persistence(formula f, twa_graph_ptr aut = nullptr, - prcheck algo = prcheck::PR_Auto); + prcheck algo = prcheck::Auto); /// \brief Return true if \a f represents a recurrence property. /// @@ -67,7 +67,7 @@ namespace spot SPOT_API bool is_recurrence(formula f, twa_graph_ptr aut = nullptr, - prcheck algo = prcheck::PR_Auto); + prcheck algo = prcheck::Auto); /// Enum used to change the behavior of is_obligation(). enum class ocheck diff --git a/tests/core/hierarchy.test b/tests/core/hierarchy.test index 7db4ffb62..a7794c5c9 100755 --- a/tests/core/hierarchy.test +++ b/tests/core/hierarchy.test @@ -66,3 +66,37 @@ diff out expected test B = `ltlfilt --format=%h -f '(Gb R (b xor Gb)) W (a W Xa)'` ltlfilt -q --safety --guarantee -f '(Gb R (b xor Gb)) W (a W Xa)' + +# make sure SPOT_PR_CHECK is read. +randltl -n -1 a b c | ltlfilt -v --syntactic-safety --syntactic-guarantee \ + --syntactic-obligation --syntactic-recurrence --syntactic-persistence \ + -n 100 > res +cat res | SPOT_PR_CHECK=x ltlfilt --recurrence 2>err && exit 1 +cat res | SPOT_PR_CHECK=9 ltlfilt --recurrence 2>err && exit 1 +grep SPOT_PR_CHECK err + +# Testing Recurrence. +cat res | ltlfilt --recurrence > r0 +for i in 1 2; do + cat res | SPOT_PR_CHECK=$i ltlfilt --recurrence > r$i +done +diff r0 r2 +diff r1 r2 +cat res | ltlfilt -o %h.ltl +cat R.ltl O.ltl G.ltl S.ltl B.ltl | sort > rogsb.ltl +sort r2 > r3 +diff r3 rogsb.ltl + +# Testing Persistence. +cat res | ltlfilt --persistence > p0 +for i in 1 2; do + cat res | SPOT_PR_CHECK=$i ltlfilt --persistence > p$i +done +diff p0 p2 +diff p1 p2 +cat res | ltlfilt -o %h.ltl +cat P.ltl O.ltl G.ltl S.ltl B.ltl | sort > pogsb.ltl +sort p2 > p3 +diff p3 pogsb.ltl + +exit 0