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

rs_like: fix bug to accept Fin | Fin , Inf & Inf

Browse source 
co-Büchi is now recognized as Streett-like, Büchi as Rabin-like.
Also recognized Inf & Inf & Inf... as Streett-like and
Fin | Fin | Fin... as Rabin-like.

* spot/twa/acc.cc: Fix the bug
* tests/python/rs_like.py: Add some test case
This commit is contained in:
Thomas Medioni 2017-05-23 10:50:54 +02:00
parent acdaaac4f0
commit 4da6a5cde1
2 changed files with 25 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

25
spot/twa/acc.cc
View file

@ -422,6 +422,7 @@ namespace spot
is_rs_like(const acc_cond::acc_code& code, is_rs_like(const acc_cond::acc_code& code,
acc_cond::acc_op highop, acc_cond::acc_op highop,
acc_cond::acc_op lowop, acc_cond::acc_op lowop,
acc_cond::acc_op singleop,
std::vector<acc_cond::rs_pair>& pairs) std::vector<acc_cond::rs_pair>& pairs)
{ {
assert(pairs.empty()); assert(pairs.empty());
@ -430,20 +431,23 @@ namespace spot
if (mainop == acc_cond::acc_op::Fin || mainop == acc_cond::acc_op::Inf) if (mainop == acc_cond::acc_op::Fin || mainop == acc_cond::acc_op::Inf)
{ {
assert(code.size() != 2); assert(code.size() == 2);
auto m = code[0].mark; auto m = code[0].mark;
if (m.count() != 1) if (mainop == singleop && m.count() != 1)
return false; return false;
acc_cond::mark_t fin(0U); acc_cond::mark_t fin(0U);
acc_cond::mark_t inf(0U); acc_cond::mark_t inf(0U);
for (unsigned mark: m.sets())
{
if (mainop == acc_cond::acc_op::Fin) if (mainop == acc_cond::acc_op::Fin)
fin = m; fin = {mark};
else else
inf = m; inf = {mark};
pairs.emplace_back(fin, inf); pairs.emplace_back(fin, inf);
}
return true; return true;
} }
else if (mainop == lowop) // Single pair? else if (mainop == lowop) // Single pair?
@ -468,14 +472,17 @@ namespace spot
acc_cond::mark_t fin(0U); acc_cond::mark_t fin(0U);
acc_cond::mark_t inf(0U); acc_cond::mark_t inf(0U);
if (m.count() != 1) if (op == singleop && m.count() != 1)
return false; return false;
for (unsigned mark: m.sets())
{
if (op == acc_cond::acc_op::Fin) if (op == acc_cond::acc_op::Fin)
fin = m; fin = {mark};
else //fin else //fin
inf = m; inf = {mark};
pairs.emplace_back(fin, inf); pairs.emplace_back(fin, inf);
} }
}
else else
{ {
if (op != lowop || size != 4) if (op != lowop || size != 4)
@ -544,7 +551,7 @@ namespace spot
pairs.emplace_back(0U, 0U); pairs.emplace_back(0U, 0U);
return true; return true;
} }
return is_rs_like(code_, acc_op::And, acc_op::Or, pairs); return is_rs_like(code_, acc_op::And, acc_op::Or, acc_op::Fin, pairs);
} }
bool acc_cond::is_rabin_like(std::vector<rs_pair>& pairs) const bool acc_cond::is_rabin_like(std::vector<rs_pair>& pairs) const
@ -557,7 +564,7 @@ namespace spot
pairs.emplace_back(0U, 0U); pairs.emplace_back(0U, 0U);
return true; return true;
} }
return is_rs_like(code_, acc_op::Or, acc_op::And, pairs); return is_rs_like(code_, acc_op::Or, acc_op::And, acc_op::Inf, pairs);
} }
// PAIRS contains the number of Inf in each pair. // PAIRS contains the number of Inf in each pair.

3
tests/python/rs_like.py
View file

@ -54,6 +54,9 @@ def test_rabin(acc, expected_rabin_like, expected_pairs):
o_acc = spot.acc_cond(acc.get_acceptance().complement()) o_acc = spot.acc_cond(acc.get_acceptance().complement())
test_rs(o_acc, 'streett', expected_rabin_like, switch_pairs(expected_pairs)) test_rs(o_acc, 'streett', expected_rabin_like, switch_pairs(expected_pairs))
acc = spot.acc_cond(spot.acc_code('Fin(0)'))
test_streett(acc, True, [spot.rs_pair(m0, mall)])
acc = spot.acc_cond(spot.acc_code('Fin(0)|Inf(1)')) acc = spot.acc_cond(spot.acc_code('Fin(0)|Inf(1)'))
test_streett(acc, True, [spot.rs_pair(m0, m1)]) test_streett(acc, True, [spot.rs_pair(m0, m1)])