acc: better Rabin/Streett detection
* src/twa/acc.cc: Allow duplicate and reordered pairs. Also recognize the single-pair cases. * src/twaalgos/hoa.cc: When Rabin or Streett is detected, canonicalize the Acceptance: line. * src/tests/hoaparse.test, wrap/python/tests/accparse2.py: More tests. * src/tests/sbacc.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
04171207e6
commit
e04b4eb9fb
5 changed files with 280 additions and 50 deletions
|
|
@ -1769,6 +1769,21 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
/* This is Streett, but badly ordered */
|
||||
Acceptance: 4 (Inf(3) | Fin(2)) & (Fin(0) | Inf(1))
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 0 {2}
|
||||
[0&!1] 0 {1 2}
|
||||
[!0&1] 0 {3}
|
||||
[0&1] 0 {1 3}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 6 Fin(0) | (Fin(1) & Inf(2) & Inf(3)) | (Fin(4) & Inf(5))
|
||||
--BODY--
|
||||
State: 0
|
||||
|
|
@ -1781,6 +1796,19 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
/* generalized-Rabin, but badely ordered */
|
||||
Acceptance: 6 (Inf(5) & Fin(4)) | Fin(0) | (Inf(2) & Fin(1) & Inf(3))
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 0 {0 1 4}
|
||||
[0&!1] 0 {2 4}
|
||||
[!0&1] 0 {3 5}
|
||||
[0&1] 0 {1 3}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 3 Fin(0)|Fin(1)|Fin(2)
|
||||
--BODY--
|
||||
State: 0
|
||||
|
|
@ -1875,6 +1903,36 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: Streett 2
|
||||
Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3))
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 0 {2}
|
||||
[0&!1] 0 {1 2}
|
||||
[!0&1] 0 {3}
|
||||
[0&1] 0 {1 3}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: generalized-Rabin 3 0 2 1
|
||||
Acceptance: 6 Fin(0) | (Fin(1) & (Inf(2)&Inf(3))) | (Fin(4) & Inf(5))
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 0 {0 1 4}
|
||||
[0&!1] 0 {2 4}
|
||||
[!0&1] 0 {3 5}
|
||||
[0&1] 0 {1 3}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: generalized-Rabin 3 0 2 1
|
||||
Acceptance: 6 Fin(0) | (Fin(1) & (Inf(2)&Inf(3))) | (Fin(4) & Inf(5))
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
|
|
@ -2000,6 +2058,20 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 4 (Fin(3) & Inf(2)) | (Fin(1) & Inf(0))
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 0 {2}
|
||||
[0&!1] 0 {1 2}
|
||||
[!0&1] 0 {3}
|
||||
[0&1] 0 {1 3}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 6 (Inf(1) | (Fin(2)|Fin(3))) & (Inf(4) | Fin(5)) & Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
|
|
@ -2014,6 +2086,20 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 6 (Inf(4) | Fin(5)) & (Inf(1) | (Fin(2)|Fin(3))) & Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 0 {0 1 4}
|
||||
[0&!1] 0 {2 4}
|
||||
[!0&1] 0 {3 5}
|
||||
[0&1] 0 {1 3}
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: generalized-Buchi 3
|
||||
Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
|
|
|
|||
|
|
@ -85,6 +85,7 @@ HOA: v1
|
|||
States: 3
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
acc-name: Streett 1
|
||||
Acceptance: 2 Fin(0) | Inf(1)
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
--BODY--
|
||||
|
|
|
|||
167
src/twa/acc.cc
167
src/twa/acc.cc
|
|
@ -348,55 +348,92 @@ namespace spot
|
|||
return false;
|
||||
}
|
||||
|
||||
|
||||
namespace
|
||||
{
|
||||
// Is Rabin or Streett, depending on highop and lowop.
|
||||
static bool
|
||||
is_rs(const acc_cond::acc_code& code,
|
||||
acc_cond::acc_op highop,
|
||||
acc_cond::acc_op lowop,
|
||||
acc_cond::mark_t all_sets)
|
||||
{
|
||||
unsigned s = code.back().size;
|
||||
auto mainop = code.back().op;
|
||||
if (mainop == highop)
|
||||
{
|
||||
// The size must be a multiple of 5.
|
||||
if ((s != code.size() - 1) || (s % 5))
|
||||
return false;
|
||||
}
|
||||
else // Single pair?
|
||||
{
|
||||
if (s != 4 || mainop != lowop)
|
||||
return false;
|
||||
// Pretend we where in a unary highop.
|
||||
s = 5;
|
||||
}
|
||||
acc_cond::mark_t seen_fin = 0U;
|
||||
acc_cond::mark_t seen_inf = 0U;
|
||||
while (s)
|
||||
{
|
||||
if (code[--s].op != lowop)
|
||||
return false;
|
||||
auto o1 = code[--s].op;
|
||||
auto m1 = code[--s].mark;
|
||||
auto o2 = code[--s].op;
|
||||
auto m2 = code[--s].mark;
|
||||
|
||||
// We assume
|
||||
// Fin(n) lowop Inf(n+1)
|
||||
// o1 (m1) o2 (m2)
|
||||
// swap if it is the converse
|
||||
if (o2 == acc_cond::acc_op::Fin)
|
||||
{
|
||||
std::swap(o1, o2);
|
||||
std::swap(m1, m2);
|
||||
}
|
||||
if (o1 != acc_cond::acc_op::Fin
|
||||
|| o2 != acc_cond::acc_op::Inf
|
||||
|| m1.count() != 1
|
||||
|| m2.id != (m1.id << 1))
|
||||
return false;
|
||||
seen_fin |= m1;
|
||||
seen_inf |= m2;
|
||||
}
|
||||
|
||||
return (!(seen_fin & seen_inf)
|
||||
&& (seen_fin | seen_inf) == all_sets);
|
||||
}
|
||||
}
|
||||
|
||||
int acc_cond::is_rabin() const
|
||||
{
|
||||
if (code_.is_false())
|
||||
return num_ == 0 ? 0 : -1;
|
||||
if ((num_ & 1)
|
||||
|| code_.is_true()
|
||||
|| code_.back().op != acc_op::Or)
|
||||
if ((num_ & 1) || code_.is_true())
|
||||
return -1;
|
||||
// The size must be a multiple of 5.
|
||||
auto s = code_.back().size;
|
||||
if ((s != code_.size() - 1) || (s % 5))
|
||||
|
||||
if (is_rs(code_, acc_op::Or, acc_op::And, all_sets()))
|
||||
return num_ / 2;
|
||||
else
|
||||
return -1;
|
||||
auto p = s / 5; // number of pairs
|
||||
unsigned n = 0;
|
||||
while (s)
|
||||
if (code_[--s].op != acc_op::And
|
||||
|| code_[--s].op != acc_op::Fin
|
||||
|| code_[--s].mark != acc_cond::mark_t({n++})
|
||||
|| code_[--s].op != acc_op::Inf
|
||||
|| code_[--s].mark != acc_cond::mark_t({n++}))
|
||||
return -1;
|
||||
return p;
|
||||
}
|
||||
|
||||
int acc_cond::is_streett() const
|
||||
{
|
||||
if (code_.is_true())
|
||||
return num_ == 0 ? 0 : -1;
|
||||
if ((num_ & 1)
|
||||
|| code_.is_false()
|
||||
|| code_.back().op != acc_op::And)
|
||||
if ((num_ & 1) || code_.is_false())
|
||||
return -1;
|
||||
// The size must be a multiple of 5.
|
||||
auto s = code_.back().size;
|
||||
if ((s != code_.size() - 1) || (s % 5))
|
||||
|
||||
if (is_rs(code_, acc_op::And, acc_op::Or, all_sets()))
|
||||
return num_ / 2;
|
||||
else
|
||||
return -1;
|
||||
auto p = s / 5; // number of pairs
|
||||
unsigned n = 0;
|
||||
while (s)
|
||||
if (code_[--s].op != acc_op::Or
|
||||
|| code_[--s].op != acc_op::Fin
|
||||
|| code_[--s].mark != acc_cond::mark_t({n++})
|
||||
|| code_[--s].op != acc_op::Inf
|
||||
|| code_[--s].mark != acc_cond::mark_t({n++}))
|
||||
return -1;
|
||||
return p;
|
||||
}
|
||||
|
||||
// Return the number of Inf in each pair.
|
||||
// PAIRS contains the number of Inf in each pair.
|
||||
bool acc_cond::is_generalized_rabin(std::vector<unsigned>& pairs) const
|
||||
{
|
||||
pairs.clear();
|
||||
|
|
@ -408,41 +445,73 @@ namespace spot
|
|||
if (code_.is_true()
|
||||
|| code_.back().op != acc_op::Or)
|
||||
return false;
|
||||
|
||||
auto s = code_.back().size;
|
||||
unsigned n = 0;
|
||||
acc_cond::mark_t seen_fin = 0U;
|
||||
acc_cond::mark_t seen_inf = 0U;
|
||||
// Each pairs is the position of a Fin followed
|
||||
// by the number of Inf.
|
||||
std::map<unsigned, unsigned> p;
|
||||
while (s)
|
||||
{
|
||||
--s;
|
||||
if (code_[s].op == acc_op::And)
|
||||
{
|
||||
if (code_[--s].op != acc_op::Fin
|
||||
|| code_[--s].mark != acc_cond::mark_t({n++})
|
||||
|| code_[--s].op != acc_op::Inf)
|
||||
return false;
|
||||
unsigned p = 0;
|
||||
auto m = code_[--s].mark;
|
||||
while (m.has(n))
|
||||
auto o1 = code_[--s].op;
|
||||
auto m1 = code_[--s].mark;
|
||||
auto o2 = code_[--s].op;
|
||||
auto m2 = code_[--s].mark;
|
||||
|
||||
// We assume
|
||||
// Fin(n) & Inf({n+1,n+2,...,n+i})
|
||||
// o1 (m1) o2 (m2)
|
||||
// swap if it is the converse
|
||||
if (o2 == acc_cond::acc_op::Fin)
|
||||
{
|
||||
m.clear(n);
|
||||
++p;
|
||||
++n;
|
||||
std::swap(o1, o2);
|
||||
std::swap(m1, m2);
|
||||
}
|
||||
if (m)
|
||||
|
||||
if (o1 != acc_cond::acc_op::Fin
|
||||
|| o2 != acc_cond::acc_op::Inf
|
||||
|| m1.count() != 1)
|
||||
return false;
|
||||
pairs.push_back(p);
|
||||
|
||||
unsigned i = m2.count();
|
||||
// If we have seen this pair already, it must have the
|
||||
// same size.
|
||||
if (p.emplace(m1.max_set(), i).first->second != i)
|
||||
return false;
|
||||
assert(i > 0);
|
||||
unsigned j = m1.max_set(); // == n+1
|
||||
do
|
||||
if (!m2.has(j++))
|
||||
return false;
|
||||
while (--i);
|
||||
|
||||
seen_fin |= m1;
|
||||
seen_inf |= m2;
|
||||
}
|
||||
else if (code_[s].op == acc_op::Fin)
|
||||
{
|
||||
if (code_[--s].mark != acc_cond::mark_t({n++}))
|
||||
auto m1 = code_[--s].mark;
|
||||
if (m1.count() != 1)
|
||||
return false;
|
||||
pairs.push_back(0);
|
||||
// If we have seen this pair already, it must have the
|
||||
// same size.
|
||||
if (p.emplace(m1.max_set(), 0U).first->second != 0U)
|
||||
return false;
|
||||
seen_fin |= m1;
|
||||
}
|
||||
else
|
||||
{
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
for (auto i: p)
|
||||
pairs.push_back(i.second);
|
||||
return (!(seen_fin & seen_inf)
|
||||
&& (seen_fin | seen_inf) == all_sets());
|
||||
}
|
||||
|
||||
acc_cond::acc_code
|
||||
|
|
|
|||
|
|
@ -282,6 +282,7 @@ namespace spot
|
|||
os << nl;
|
||||
|
||||
unsigned num_acc = aut->acc().num_sets();
|
||||
acc_cond::acc_code acc_c = aut->acc().get_acceptance();
|
||||
if (aut->acc().is_generalized_buchi())
|
||||
{
|
||||
if (aut->acc().is_true())
|
||||
|
|
@ -309,6 +310,9 @@ namespace spot
|
|||
if (r > 0)
|
||||
{
|
||||
os << "acc-name: Rabin " << r << nl;
|
||||
// Force the acceptance to remove any duplicate sets, and
|
||||
// make sure it is correctly ordered.
|
||||
acc_c = acc_cond::acc_code::rabin(r);
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -317,6 +321,9 @@ namespace spot
|
|||
if (r > 0)
|
||||
{
|
||||
os << "acc-name: Streett " << r << nl;
|
||||
// Force the acceptance to remove any duplicate sets, and
|
||||
// make sure it is correctly ordered.
|
||||
acc_c = acc_cond::acc_code::streett(r);
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -327,6 +334,10 @@ namespace spot
|
|||
for (auto p: pairs)
|
||||
os << ' ' << p;
|
||||
os << nl;
|
||||
// Force the acceptance to remove any duplicate
|
||||
// sets, and make sure it is correctly ordered.
|
||||
acc_c = acc_cond::acc_code::generalized_rabin(pairs.begin(),
|
||||
pairs.end());
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -342,7 +353,7 @@ namespace spot
|
|||
}
|
||||
}
|
||||
os << "Acceptance: " << num_acc << ' ';
|
||||
os << aut->acc().get_acceptance();
|
||||
os << acc_c;
|
||||
os << nl;
|
||||
os << "properties:";
|
||||
// Make sure the property line is not too large,
|
||||
|
|
|
|||
|
|
@ -31,3 +31,66 @@ a.set_acceptance(spot.parse_acc_code(
|
|||
'Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))'))
|
||||
assert(a.is_parity() == [False, False, False])
|
||||
assert(a.is_parity(True) == [True, True, False])
|
||||
|
||||
a = spot.acc_cond(0)
|
||||
a.set_acceptance(spot.parse_acc_code('all'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == 0)
|
||||
a.set_acceptance(spot.parse_acc_code('none'))
|
||||
assert(a.is_rabin() == 0)
|
||||
assert(a.is_streett() == -1)
|
||||
|
||||
a = spot.acc_cond(2)
|
||||
a.set_acceptance(spot.parse_acc_code('(Fin(0)&Inf(1))'))
|
||||
assert(a.is_rabin() == 1)
|
||||
assert(a.is_streett() == -1)
|
||||
a.set_acceptance(spot.parse_acc_code('Inf(1)&Fin(0)'))
|
||||
assert(a.is_rabin() == 1)
|
||||
assert(a.is_streett() == -1)
|
||||
a.set_acceptance(spot.parse_acc_code('(Fin(0)|Inf(1))'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == 1)
|
||||
a.set_acceptance(spot.parse_acc_code('Inf(1)|Fin(0)'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == 1)
|
||||
|
||||
a = spot.acc_cond(4)
|
||||
a.set_acceptance(spot.parse_acc_code('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))'))
|
||||
assert(a.is_rabin() == 2)
|
||||
assert(a.is_streett() == -1)
|
||||
a.set_acceptance(spot.parse_acc_code('(Inf(3)&Fin(2))|(Fin(0)&Inf(1))'))
|
||||
assert(a.is_rabin() == 2)
|
||||
assert(a.is_streett() == -1)
|
||||
a.set_acceptance(spot.parse_acc_code('(Inf(2)&Fin(3))|(Fin(0)&Inf(1))'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == -1)
|
||||
a.set_acceptance(spot.parse_acc_code('(Inf(3)&Fin(2))|(Fin(2)&Inf(1))'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == -1)
|
||||
a.set_acceptance(spot.parse_acc_code('(Inf(1)&Fin(0))|(Fin(0)&Inf(1))'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == -1)
|
||||
r = spot.parse_acc_code('(Fin(0)&Inf(1))|(Inf(1)&Fin(0))|(Inf(3)&Fin(2))')
|
||||
a.set_acceptance(r)
|
||||
assert(a.is_rabin() == 2)
|
||||
assert(a.is_streett() == -1)
|
||||
|
||||
a.set_acceptance(spot.parse_acc_code('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == 2)
|
||||
a.set_acceptance(spot.parse_acc_code('(Inf(3)|Fin(2))&(Fin(0)|Inf(1))'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == 2)
|
||||
a.set_acceptance(spot.parse_acc_code('(Inf(2)|Fin(3))&(Fin(0)|Inf(1))'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == -1)
|
||||
a.set_acceptance(spot.parse_acc_code('(Inf(3)|Fin(2))&(Fin(2)|Inf(1))'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == -1)
|
||||
a.set_acceptance(spot.parse_acc_code('(Inf(1)|Fin(0))&(Fin(0)|Inf(1))'))
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == -1)
|
||||
r = spot.parse_acc_code('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))')
|
||||
a.set_acceptance(r)
|
||||
assert(a.is_rabin() == -1)
|
||||
assert(a.is_streett() == 2)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue