hoa: output acc-name for several acceptance types
So far the HOA output would emit an acc-name only for generalized-Buchi or inferior types (Buchi, all). It now knows about none, co-Buchi, generalized-co-Buchi, Rabin, Streett, and generalized-Rabin as well. * src/twa/acc.cc, src/twa/acc.hh: Add detection code. * src/twaalgos/hoa.cc: Use it. * src/tests/remfin.test, src/tests/maskacc.test, src/tests/complete.test, src/tests/sim3.test, src/tests/ltl2dstar.test: Adjust tests. * src/tests/hoaparse.test: Adjust and add more tests.
This commit is contained in:
Alexandre Duret-Lutz
parent
8e1c846984
commit
d276f73eed
9 changed files with 371 additions and 15 deletions
|
|
@ -64,6 +64,7 @@ HOA: v1
|
|||
States: 3
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
acc-name: co-Buchi
|
||||
Acceptance: 1 Fin(0)
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic
|
||||
|
|
@ -99,6 +100,7 @@ HOA: v1
|
|||
States: 2
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
acc-name: none
|
||||
Acceptance: 0 f
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic
|
||||
|
|
|
|||
|
|
@ -1375,6 +1375,7 @@ HOA: v1
|
|||
States: 2
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: Rabin 2
|
||||
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
--BODY--
|
||||
|
|
@ -1428,6 +1429,7 @@ HOA: v1
|
|||
States: 2
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: Rabin 2
|
||||
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
--BODY--
|
||||
|
|
@ -1731,3 +1733,188 @@ expecterr input <<EOF
|
|||
input:4.8-12: alternation is not yet supported
|
||||
autfilt: failed to read automaton from input
|
||||
EOF
|
||||
|
||||
|
||||
cat >input <<EOF
|
||||
HOA: v1
|
||||
tool: "Rabinizer" "3"
|
||||
name: "DTGRA for (G F a | F G b)"
|
||||
properties: deterministic
|
||||
States: 1
|
||||
Start: 0
|
||||
Acceptance: 4 (Fin(0)&Inf(1)) | (Fin(2)&Inf(3))
|
||||
AP: 2 "a" "b"
|
||||
--BODY--
|
||||
State: 0
|
||||
0 {2} /*{}*/
|
||||
0 {1 2} /*{a}*/
|
||||
0 {3} /*{b}*/
|
||||
0 {3 1} /*{a, b}*/
|
||||
--END--
|
||||
HOA: v1
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
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"
|
||||
Acceptance: 6 Fin(0) | (Fin(1) & Inf(2) & Inf(3)) | (Fin(4) & Inf(5))
|
||||
--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
|
||||
[!0&!1] 0 {0 1}
|
||||
[0&!1] 0 {1}
|
||||
[!0&1] 0 {2}
|
||||
[0&1] 0 {}
|
||||
--END--
|
||||
EOF
|
||||
|
||||
expectok input <<EOF
|
||||
HOA: v1
|
||||
name: "DTGRA for (G F a | F G b)"
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: Rabin 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: 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-co-Buchi 3
|
||||
Acceptance: 3 Fin(0)|Fin(1)|Fin(2)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 0 {0 1}
|
||||
[0&!1] 0 {1}
|
||||
[!0&1] 0 {2}
|
||||
[0&1] 0
|
||||
--END--
|
||||
EOF
|
||||
|
||||
# The complements are Streett and Rabin, but the acceptance set are
|
||||
# not ordered in the way we call "Streett" and "Rabin" in the HOA
|
||||
# specifications.
|
||||
expectok input --complement-acc <<EOF
|
||||
HOA: v1
|
||||
name: "DTGRA for (G F a | F G b)"
|
||||
States: 1
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
Acceptance: 4 (Inf(0) | Fin(1)) & (Inf(2) | Fin(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"
|
||||
Acceptance: 4 (Fin(1) & Inf(0)) | (Fin(3) & Inf(2))
|
||||
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
|
||||
--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
|
||||
properties: deterministic
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!1] 0 {0 1}
|
||||
[0&!1] 0 {1}
|
||||
[!0&1] 0 {2}
|
||||
[0&1] 0
|
||||
--END--
|
||||
EOF
|
||||
|
|
|
|||
|
|
@ -86,6 +86,7 @@ HOA: v1
|
|||
States: 5
|
||||
Start: 3
|
||||
AP: 2 "b" "a"
|
||||
acc-name: Rabin 2
|
||||
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
|
||||
properties: implicit-labels state-acc complete deterministic
|
||||
--BODY--
|
||||
|
|
|
|||
|
|
@ -50,6 +50,7 @@ HOA: v1
|
|||
States: 4
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: co-Buchi
|
||||
Acceptance: 1 Fin(0)
|
||||
properties: trans-labels explicit-labels trans-acc
|
||||
--BODY--
|
||||
|
|
@ -72,6 +73,7 @@ HOA: v1
|
|||
States: 4
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: co-Buchi
|
||||
Acceptance: 1 Fin(0)
|
||||
properties: trans-labels explicit-labels trans-acc
|
||||
--BODY--
|
||||
|
|
|
|||
|
|
@ -235,6 +235,7 @@ HOA: v1
|
|||
States: 1
|
||||
Start: 0
|
||||
AP: 0
|
||||
acc-name: none
|
||||
Acceptance: 0 f
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
--BODY--
|
||||
|
|
|
|||
|
|
@ -26,6 +26,7 @@ HOA: v1
|
|||
States: 7
|
||||
Start: 0
|
||||
AP: 2 "b" "a"
|
||||
acc-name: Rabin 2
|
||||
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
|
||||
properties: implicit-labels state-acc complete deterministic
|
||||
--BODY--
|
||||
|
|
@ -54,6 +55,7 @@ HOA: v1
|
|||
States: 5
|
||||
Start: 0
|
||||
AP: 2 "b" "a"
|
||||
acc-name: Rabin 2
|
||||
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
|
||||
properties: trans-labels explicit-labels state-acc complete
|
||||
properties: deterministic
|
||||
|
|
|
|||
|
|
@ -348,6 +348,103 @@ namespace spot
|
|||
return false;
|
||||
}
|
||||
|
||||
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)
|
||||
return -1;
|
||||
// The size must be a multiple of 5.
|
||||
auto s = code_.back().size;
|
||||
if ((s != code_.size() - 1) || (s % 5))
|
||||
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)
|
||||
return -1;
|
||||
// The size must be a multiple of 5.
|
||||
auto s = code_.back().size;
|
||||
if ((s != code_.size() - 1) || (s % 5))
|
||||
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.
|
||||
bool acc_cond::is_generalized_rabin(std::vector<unsigned>& pairs) const
|
||||
{
|
||||
pairs.clear();
|
||||
if (is_generalized_co_buchi())
|
||||
{
|
||||
pairs.resize(num_);
|
||||
return true;
|
||||
}
|
||||
if (code_.is_true()
|
||||
|| code_.back().op != acc_op::Or)
|
||||
return false;
|
||||
auto s = code_.back().size;
|
||||
unsigned n = 0;
|
||||
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))
|
||||
{
|
||||
m.clear(n);
|
||||
++p;
|
||||
++n;
|
||||
}
|
||||
if (m)
|
||||
return false;
|
||||
pairs.push_back(p);
|
||||
}
|
||||
else if (code_[s].op == acc_op::Fin)
|
||||
{
|
||||
if (code_[--s].mark != acc_cond::mark_t({n++}))
|
||||
return false;
|
||||
pairs.push_back(0);
|
||||
}
|
||||
else
|
||||
{
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
namespace
|
||||
{
|
||||
bdd to_bdd_rec(const acc_cond::acc_word* c, const bdd* map)
|
||||
|
|
|
|||
|
|
@ -501,12 +501,12 @@ namespace spot
|
|||
return res;
|
||||
}
|
||||
|
||||
template<class iterator>
|
||||
static acc_code generalized_rabin(iterator begin, iterator end)
|
||||
template<class Iterator>
|
||||
static acc_code generalized_rabin(Iterator begin, Iterator end)
|
||||
{
|
||||
acc_cond::acc_code res = f();
|
||||
unsigned n = 0;
|
||||
for (iterator i = begin; i != end; ++i)
|
||||
for (Iterator i = begin; i != end; ++i)
|
||||
{
|
||||
acc_cond::acc_code pair = fin({n++});
|
||||
acc_cond::mark_t m = 0U;
|
||||
|
|
@ -854,6 +854,28 @@ namespace spot
|
|||
return uses_fin_acceptance_;
|
||||
}
|
||||
|
||||
bool is_true() const
|
||||
{
|
||||
return code_.is_true();
|
||||
}
|
||||
|
||||
bool is_false() const
|
||||
{
|
||||
return code_.is_false();
|
||||
}
|
||||
|
||||
bool is_buchi() const
|
||||
{
|
||||
unsigned s = code_.size();
|
||||
return num_ == 1 &&
|
||||
s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets();
|
||||
}
|
||||
|
||||
bool is_co_buchi() const
|
||||
{
|
||||
return num_ == 1 && is_generalized_co_buchi();
|
||||
}
|
||||
|
||||
void set_generalized_buchi()
|
||||
{
|
||||
set_acceptance(inf(all_sets()));
|
||||
|
|
@ -866,6 +888,21 @@ namespace spot
|
|||
(s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets());
|
||||
}
|
||||
|
||||
bool is_generalized_co_buchi() const
|
||||
{
|
||||
unsigned s = code_.size();
|
||||
return (s == 2 &&
|
||||
code_[1].op == acc_op::Fin && code_[0].mark == all_sets());
|
||||
}
|
||||
|
||||
// Returns a number of pairs (>=0) if Rabin, or -1 else.
|
||||
int is_rabin() const;
|
||||
// Returns a number of pairs (>=0) if Streett, or -1 else.
|
||||
int is_streett() const;
|
||||
|
||||
// Return the number of Inf in each pair.
|
||||
bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
|
||||
|
||||
static acc_code generalized_buchi(unsigned n)
|
||||
{
|
||||
mark_t m((1U << n) - 1);
|
||||
|
|
@ -874,18 +911,6 @@ namespace spot
|
|||
return acc_code::inf(m);
|
||||
}
|
||||
|
||||
bool is_buchi() const
|
||||
{
|
||||
unsigned s = code_.size();
|
||||
return num_ == 1 &&
|
||||
s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets();
|
||||
}
|
||||
|
||||
bool is_true() const
|
||||
{
|
||||
return code_.is_true();
|
||||
}
|
||||
|
||||
protected:
|
||||
bool check_fin_acceptance() const;
|
||||
|
||||
|
|
|
|||
|
|
@ -292,6 +292,45 @@ namespace spot
|
|||
os << "acc-name: generalized-Buchi " << num_acc;
|
||||
os << nl;
|
||||
}
|
||||
else if (aut->acc().is_generalized_co_buchi())
|
||||
{
|
||||
if (aut->acc().is_false())
|
||||
os << "acc-name: none";
|
||||
else if (aut->acc().is_co_buchi())
|
||||
os << "acc-name: co-Buchi";
|
||||
else
|
||||
os << "acc-name: generalized-co-Buchi " << num_acc;
|
||||
os << nl;
|
||||
}
|
||||
else
|
||||
{
|
||||
int r = aut->acc().is_rabin();
|
||||
assert(r != 0);
|
||||
if (r > 0)
|
||||
{
|
||||
os << "acc-name: Rabin " << r << nl;
|
||||
}
|
||||
else
|
||||
{
|
||||
r = aut->acc().is_streett();
|
||||
assert(r != 0);
|
||||
if (r > 0)
|
||||
{
|
||||
os << "acc-name: Streett " << r << nl;
|
||||
}
|
||||
else
|
||||
{
|
||||
std::vector<unsigned> pairs;
|
||||
if (aut->acc().is_generalized_rabin(pairs))
|
||||
{
|
||||
os << "acc-name: generalized-Rabin " << pairs.size();
|
||||
for (auto p: pairs)
|
||||
os << ' ' << p;
|
||||
os << nl;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
os << "Acceptance: " << num_acc << ' ';
|
||||
os << aut->acc().get_acceptance();
|
||||
os << nl;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue