From fd32ab5dd7908fdefc1764f55e6c6446ecc222d6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 8 Nov 2018 11:35:15 +0100 Subject: [PATCH] fix is_generalized_rabin and is_generalized_streett * spot/twa/acc.cc: Recoginize the single-pair case. * python/spot/impl.i: Return the vector instead of taking it by reference. * tests/python/setacc.py: Add test cases. * NEWS: Mention those changes. --- NEWS | 8 ++++++++ python/spot/impl.i | 1 + spot/twa/acc.cc | 35 +++++++++++++++++++++++++++++------ tests/python/setacc.py | 28 ++++++++++++++++++++++++++++ 4 files changed, 66 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index e1cf16b98..5b1009fd7 100644 --- a/NEWS +++ b/NEWS @@ -33,6 +33,10 @@ New in spot 2.6.3.dev (not yet released) spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0') (Note: those extra options are documented in the spot-x(7) man page.) + - spot.is_generalized_rabin() and spot.is_generalized_streett() now return + a tuple (b, v) where b is a Boolean, and v is the vector of the sizes + of each generalized pair. This is a backward incompatible change. + Library: - The LTL parser learned syntactic sugar for nested ranges of X @@ -86,6 +90,10 @@ New in spot 2.6.3.dev (not yet released) Bugs fixed: + - acc_cond::is_generalized_rabin() and + acc_cond::is_generalized_streett() did not recognize the cases + were a single generalized pair is used. + - The pair of acc_cond::mark_t returned by acc_code::used_inf_fin_sets(), and the pair (bool, vector_rs_pairs) by acc_cond::is_rabin_like() and diff --git a/python/spot/impl.i b/python/spot/impl.i index 314305680..1ac93eab0 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -478,6 +478,7 @@ namespace std { namespace std { %template(vector_rs_pair) vector; } +%apply std::vector &OUTPUT {std::vector& pairs} %apply std::vector &OUTPUT {std::vector& pairs} %include %template(pair_bool_mark) std::pair; diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 32ddc058a..d336a948e 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -672,14 +672,25 @@ namespace spot } // "Acceptance: 0 f" is caught by is_generalized_rabin() above. // Therefore is_f() below catches "Acceptance: n f" with n>0. - if (code_.is_f() - || code_.is_t() - || code_.back().sub.op != acc_op::Or) + if (code_.is_f() || code_.is_t()) return false; auto s = code_.back().sub.size; acc_cond::mark_t seen_fin = {}; acc_cond::mark_t seen_inf = {}; + + // generalized Rabin should start with Or, unless + // it has a single pair. + { + 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; + else if (topop != acc_op::Or) + return false; + } + // Each pair is the position of a Fin followed // by the number of Inf. std::map p; @@ -756,14 +767,26 @@ namespace spot } // "Acceptance: 0 t" is caught by is_generalized_buchi() above. // Therefore is_t() below catches "Acceptance: n t" with n>0. - if (code_.is_t() - || code_.is_f() - || code_.back().sub.op != acc_op::And) + if (code_.is_t() || code_.is_f()) return false; auto s = code_.back().sub.size; acc_cond::mark_t seen_fin = {}; acc_cond::mark_t seen_inf = {}; + + // generalized Streett should start with And, unless + // it has a single pair. + { + 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; + else if (topop != acc_op::And) + return false; + } + + // Each pairs is the position of a Inf followed // by the number of Fin. std::map p; diff --git a/tests/python/setacc.py b/tests/python/setacc.py index 90fe492b3..cc09c40c1 100644 --- a/tests/python/setacc.py +++ b/tests/python/setacc.py @@ -54,3 +54,31 @@ assert repr(v) == \ '(spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0]))' v2 = (spot.rs_pair(fin=[0], inf=[1]), spot.rs_pair(fin=[2], inf=[0])) assert v == v2 + +acc = spot.acc_cond("generalized-Rabin 1 2") +(b, v) = acc.is_generalized_rabin() +assert b == True +assert v == (2,) +(b, v) = acc.is_generalized_streett() +assert b == False +assert v == () +(b, v) = acc.is_streett_like() +assert b == True +ve = (spot.rs_pair([0], []), spot.rs_pair([], [1]), spot.rs_pair([], [2])) +assert v == ve +assert acc.name() == "generalized-Rabin 1 2" + +# At the time of writting, acc_cond does not yet recognize +# "generalized-Streett", as there is no definition for that in the HOA format, +# and defining it as follows (dual for gen.Rabin) would prevent Streett from +# being a generalized-Streett. See issue #249. +acc = spot.acc_cond("Inf(0)|Fin(1)|Fin(2)") +(b, v) = acc.is_generalized_streett() +assert b == True +assert v == (2,) +(b, v) = acc.is_generalized_rabin() +assert b == False +assert v == () +# FIXME: We should have a way to disable the following output, as it is not +# part of HOA v1. +assert acc.name() == "generalized-Streett 1 2"