Commit fd32ab5d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 29e08a1a
Pipeline #4581 passed with stages
in 196 minutes and 4 seconds
......@@ -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
......
......@@ -478,6 +478,7 @@ namespace std {
namespace std {
%template(vector_rs_pair) vector<spot::acc_cond::rs_pair>;
}
%apply std::vector<unsigned> &OUTPUT {std::vector<unsigned>& pairs}
%apply std::vector<spot::acc_cond::rs_pair> &OUTPUT {std::vector<spot::acc_cond::rs_pair>& pairs}
%include <spot/twa/acc.hh>
%template(pair_bool_mark) std::pair<bool, spot::acc_cond::mark_t>;
......
......@@ -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<unsigned, unsigned> 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<unsigned, unsigned> p;
......
......@@ -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"
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment