Introduce a faster merge_states
merge_states is now hash-based, uses the new edge-sorting with src first and can be executed in parallel. * spot/twa/twagraph.cc: Here * tests/python/mergedge.py: Test
This commit is contained in:
Philipp Schlehuber-Caissier
parent
71c2a7b1a6
commit
d8cc0c5acb
2 changed files with 253 additions and 193 deletions
|
|
@ -372,13 +372,12 @@ namespace spot
|
|||
throw std::runtime_error(
|
||||
"twa_graph::merge_states() does not work on alternating automata");
|
||||
|
||||
const unsigned nthreads = get_nthreads();
|
||||
|
||||
typedef graph_t::edge_storage_t tr_t;
|
||||
g_.sort_edges_([](const tr_t& lhs, const tr_t& rhs)
|
||||
g_.sort_edges_srcfirst_([](const tr_t& lhs, const tr_t& rhs)
|
||||
{
|
||||
if (lhs.src < rhs.src)
|
||||
return true;
|
||||
if (lhs.src > rhs.src)
|
||||
return false;
|
||||
assert(lhs.src == rhs.src);
|
||||
if (lhs.acc < rhs.acc)
|
||||
return true;
|
||||
if (lhs.acc > rhs.acc)
|
||||
|
|
@ -449,7 +448,7 @@ namespace spot
|
|||
// Represents which states share a hash
|
||||
// Head is in the unordered_map,
|
||||
// hash_linked_list is like a linked list structure
|
||||
// of false pointers
|
||||
// of fake pointers
|
||||
|
||||
auto hash_linked_list = std::vector<unsigned>(n_states, -1u);
|
||||
auto s_to_hash = std::vector<size_t>(n_states, 0);
|
||||
|
|
@ -530,8 +529,8 @@ namespace spot
|
|||
};
|
||||
|
||||
|
||||
static auto checked1 = std::vector<char>();
|
||||
static auto checked2 = std::vector<char>();
|
||||
thread_local auto checked1 = std::vector<char>();
|
||||
thread_local auto checked2 = std::vector<char>();
|
||||
|
||||
auto [i1, nsl1, sl1, e1] = e_idx[s1];
|
||||
auto [i2, nsl2, sl2, e2] = e_idx[s2];
|
||||
|
|
@ -585,12 +584,10 @@ namespace spot
|
|||
// More efficient version?
|
||||
// Skip checked edges
|
||||
// Last element serves as break
|
||||
for (; checked1[idx1 - i1]; ++idx1)
|
||||
{
|
||||
}
|
||||
for (; checked2[idx2 - i2]; ++idx2)
|
||||
{
|
||||
}
|
||||
while (checked1[idx1 - i1])
|
||||
++idx1;
|
||||
while (checked2[idx2 - i2])
|
||||
++idx2;
|
||||
// If one is out of bounds, so is the other
|
||||
if (idx1 == e1)
|
||||
{
|
||||
|
|
@ -614,47 +611,107 @@ namespace spot
|
|||
const unsigned nb_states = num_states();
|
||||
std::vector<unsigned> remap(nb_states, -1U);
|
||||
|
||||
for (unsigned i = 0; i != nb_states; ++i)
|
||||
// Check each hash
|
||||
auto check_ix = [&](unsigned ix)
|
||||
{
|
||||
auto j = spe && (*sp)[i] ? player_map.at(s_to_hash[i]).first
|
||||
: env_map.at(s_to_hash[i]).first;
|
||||
for (; j<i; j=hash_linked_list[j])
|
||||
{
|
||||
if (state_equal(j, i))
|
||||
{
|
||||
remap[i] = (remap[j] != -1U) ? remap[j] : j;
|
||||
// Reduce cache miss
|
||||
thread_local auto v = std::vector<unsigned>();
|
||||
v.clear();
|
||||
for (auto i = ix; i != -1U; i = hash_linked_list[i])
|
||||
v.push_back(i);
|
||||
const unsigned N = v.size();
|
||||
|
||||
// Because of the special self-loop tests we use above,
|
||||
// it's possible that i can be mapped to remap[j] even
|
||||
// if j was last compatible states found. Consider the
|
||||
// following cases, taken from an actual test case:
|
||||
// 18 is equal to 5, 35 is equal to 18, but 35 is not
|
||||
// equal to 5.
|
||||
//
|
||||
// State: 5
|
||||
// [0&1&2] 8 {3}
|
||||
// [!0&1&2] 10 {1}
|
||||
// [!0&!1&!2] 18 {1}
|
||||
// [!0&!1&2] 19 {1}
|
||||
// [!0&1&!2] 20 {1}
|
||||
//
|
||||
// State: 18
|
||||
// [0&1&2] 8 {3}
|
||||
// [!0&1&2] 10 {1}
|
||||
// [!0&!1&!2] 18 {1} // self-loop
|
||||
// [!0&!1&2] 19 {1}
|
||||
// [!0&1&!2] 20 {1}
|
||||
//
|
||||
// State: 35
|
||||
// [0&1&2] 8 {3}
|
||||
// [!0&1&2] 10 {1}
|
||||
// [!0&!1&!2] 35 {1} // self-loop
|
||||
// [!0&!1&2] 19 {1}
|
||||
// [!0&1&!2] 20 {1}
|
||||
break;
|
||||
for (unsigned idx = 0; idx < N; ++idx)
|
||||
{
|
||||
auto i = v[idx];
|
||||
for (unsigned jdx = 0; jdx < idx; ++jdx)
|
||||
{
|
||||
auto j = v[jdx];
|
||||
if (state_equal(j, i))
|
||||
{
|
||||
remap[i] = (remap[j] != -1U) ? remap[j] : j;
|
||||
|
||||
// Because of the special self-loop tests we use above,
|
||||
// it's possible that i can be mapped to remap[j] even
|
||||
// if j was last compatible states found. Consider the
|
||||
// following cases, taken from an actual test case:
|
||||
// 18 is equal to 5, 35 is equal to 18, but 35 is not
|
||||
// equal to 5.
|
||||
//
|
||||
// State: 5
|
||||
// [0&1&2] 8 {3}
|
||||
// [!0&1&2] 10 {1}
|
||||
// [!0&!1&!2] 18 {1}
|
||||
// [!0&!1&2] 19 {1}
|
||||
// [!0&1&!2] 20 {1}
|
||||
//
|
||||
// State: 18
|
||||
// [0&1&2] 8 {3}
|
||||
// [!0&1&2] 10 {1}
|
||||
// [!0&!1&!2] 18 {1} // self-loop
|
||||
// [!0&!1&2] 19 {1}
|
||||
// [!0&1&!2] 20 {1}
|
||||
//
|
||||
// State: 35
|
||||
// [0&1&2] 8 {3}
|
||||
// [!0&1&2] 10 {1}
|
||||
// [!0&!1&!2] 35 {1} // self-loop
|
||||
// [!0&!1&2] 19 {1}
|
||||
// [!0&1&!2] 20 {1}
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
auto upd = [](auto& b, const auto&e, unsigned it)
|
||||
{
|
||||
while ((it > 0) & (b != e))
|
||||
{
|
||||
--it;
|
||||
++b;
|
||||
}
|
||||
};
|
||||
|
||||
auto worker = [&upd, check_ix, nthreads](unsigned pid, auto begp, auto endp,
|
||||
auto bege, auto ende)
|
||||
{
|
||||
upd(begp, endp, pid);
|
||||
upd(bege, ende, pid);
|
||||
for (; begp != endp; upd(begp, endp, nthreads))
|
||||
check_ix(begp->second.first);
|
||||
for (; bege != ende; upd(bege, ende, nthreads))
|
||||
check_ix(bege->second.first);
|
||||
};
|
||||
|
||||
{
|
||||
auto begp = player_map.begin();
|
||||
auto endp = player_map.end();
|
||||
auto bege = env_map.begin();
|
||||
auto ende = env_map.end();
|
||||
|
||||
|
||||
if ((nthreads == 1) & (num_states() > 1000)) // Bound?
|
||||
{
|
||||
worker(0, begp, endp, bege, ende);
|
||||
}
|
||||
else
|
||||
{
|
||||
static auto tv = std::vector<std::thread>();
|
||||
assert(tv.empty());
|
||||
tv.resize(nthreads);
|
||||
for (unsigned pid = 0; pid < nthreads; ++pid)
|
||||
tv[pid] = std::thread(
|
||||
[worker, pid, begp, endp, bege, ende]()
|
||||
{
|
||||
worker(pid, begp, endp, bege, ende);
|
||||
return;
|
||||
});
|
||||
for (auto& t : tv)
|
||||
t.join();
|
||||
tv.clear();
|
||||
}
|
||||
}
|
||||
|
||||
for (auto& e: edges())
|
||||
if (remap[e.dst] != -1U)
|
||||
|
|
@ -765,7 +822,7 @@ namespace spot
|
|||
comp_classes_.clear();
|
||||
// get all compatible classes
|
||||
// Candidate classes share a hash
|
||||
// A state is compatible to a class if it is compatble
|
||||
// A state is compatible to a class if it is compatible
|
||||
// to any of its states
|
||||
auto& cand_classes = equiv_class_[hi];
|
||||
unsigned n_c_classes = cand_classes.size();
|
||||
|
|
|
|||
|
|
@ -23,148 +23,151 @@ import spot
|
|||
from unittest import TestCase
|
||||
tc = TestCase()
|
||||
|
||||
aut = spot.automaton("""HOA: v1 States: 1 Start: 0 AP: 1 "a"
|
||||
Acceptance: 1 Inf(0) --BODY-- State: 0 [0] 0 [0] 0 {0} --END--""")
|
||||
tc.assertEqual(aut.num_edges(), 2)
|
||||
aut.merge_edges()
|
||||
tc.assertEqual(aut.num_edges(), 1)
|
||||
for nthread in range(1, 16, 2):
|
||||
spot.set_nthreads(nthread)
|
||||
tc.assertEqual(spot.get_nthreads(), nthread)
|
||||
aut = spot.automaton("""HOA: v1 States: 1 Start: 0 AP: 1 "a"
|
||||
Acceptance: 1 Inf(0) --BODY-- State: 0 [0] 0 [0] 0 {0} --END--""")
|
||||
tc.assertEqual(aut.num_edges(), 2)
|
||||
aut.merge_edges()
|
||||
tc.assertEqual(aut.num_edges(), 1)
|
||||
|
||||
aut = spot.automaton("""
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 2 "p0" "p1"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0] 0 {0}
|
||||
[0] 1 {0}
|
||||
State: 1
|
||||
[!0&!1] 0 {0}
|
||||
[0 | 1] 1
|
||||
[0&!1] 1 {0}
|
||||
--END--""")
|
||||
tc.assertEqual(aut.num_edges(), 5)
|
||||
aut.merge_edges()
|
||||
tc.assertEqual(aut.num_edges(), 5)
|
||||
tc.assertFalse(spot.is_deterministic(aut))
|
||||
aut = spot.split_edges(aut)
|
||||
tc.assertEqual(aut.num_edges(), 9)
|
||||
aut.merge_edges()
|
||||
tc.assertEqual(aut.num_edges(), 5)
|
||||
tc.assertTrue(spot.is_deterministic(aut))
|
||||
aut = spot.automaton("""
|
||||
HOA: v1
|
||||
States: 2
|
||||
Start: 0
|
||||
AP: 2 "p0" "p1"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0] 0 {0}
|
||||
[0] 1 {0}
|
||||
State: 1
|
||||
[!0&!1] 0 {0}
|
||||
[0 | 1] 1
|
||||
[0&!1] 1 {0}
|
||||
--END--""")
|
||||
tc.assertEqual(aut.num_edges(), 5)
|
||||
aut.merge_edges()
|
||||
tc.assertEqual(aut.num_edges(), 5)
|
||||
tc.assertFalse(spot.is_deterministic(aut))
|
||||
aut = spot.split_edges(aut)
|
||||
tc.assertEqual(aut.num_edges(), 9)
|
||||
aut.merge_edges()
|
||||
tc.assertEqual(aut.num_edges(), 5)
|
||||
tc.assertTrue(spot.is_deterministic(aut))
|
||||
|
||||
aut = spot.automaton("""
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0] 1 {0}
|
||||
[0] 2 {0}
|
||||
State: 1
|
||||
[!0] 1 {0}
|
||||
[0] 1
|
||||
State: 2
|
||||
[!0] 2 {0}
|
||||
[0] 1
|
||||
--END--""")
|
||||
aut.merge_states()
|
||||
tc.assertEqual(aut.num_edges(), 4)
|
||||
tc.assertEqual(aut.num_states(), 2)
|
||||
tc.assertTrue(spot.is_deterministic(aut))
|
||||
tc.assertTrue(aut.prop_complete())
|
||||
aut.merge_states()
|
||||
tc.assertEqual(aut.num_edges(), 4)
|
||||
tc.assertEqual(aut.num_states(), 2)
|
||||
tc.assertTrue(spot.is_deterministic(aut))
|
||||
tc.assertTrue(aut.prop_complete())
|
||||
aut = spot.automaton("""
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
AP: 1 "a"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels trans-acc complete
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0] 1 {0}
|
||||
[0] 2 {0}
|
||||
State: 1
|
||||
[!0] 1 {0}
|
||||
[0] 1
|
||||
State: 2
|
||||
[!0] 2 {0}
|
||||
[0] 1
|
||||
--END--""")
|
||||
aut.merge_states()
|
||||
tc.assertEqual(aut.num_edges(), 4)
|
||||
tc.assertEqual(aut.num_states(), 2)
|
||||
tc.assertTrue(spot.is_deterministic(aut))
|
||||
tc.assertTrue(aut.prop_complete())
|
||||
aut.merge_states()
|
||||
tc.assertEqual(aut.num_edges(), 4)
|
||||
tc.assertEqual(aut.num_states(), 2)
|
||||
tc.assertTrue(spot.is_deterministic(aut))
|
||||
tc.assertTrue(aut.prop_complete())
|
||||
|
||||
|
||||
aa = spot.automaton("""
|
||||
HOA: v1 States: 41 Start: 0 AP: 3 "allfinished" "finished_0"
|
||||
"finished_1" acc-name: parity max odd 4 Acceptance: 4 Inf(3) | (Fin(2)
|
||||
& (Inf(1) | Fin(0))) properties: trans-labels explicit-labels
|
||||
trans-acc colored properties: deterministic --BODY-- State: 0
|
||||
[!0&!1&!2] 1 {1} [!0&!1&2] 2 {1} [!0&1&!2] 3 {1} [!0&1&2] 4 {1}
|
||||
[0&!1&!2] 5 {1} [0&!1&2] 6 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} State: 1
|
||||
[!0&!1&!2] 1 {1} [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1}
|
||||
[!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 {1} [0&!1&2] 12 {1}
|
||||
State: 2 [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1}
|
||||
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 13 {1} [!0&1&!2] 14 {1}
|
||||
State: 3 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1}
|
||||
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 15 {1} [!0&!1&2] 16 {1}
|
||||
State: 4 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 {1}
|
||||
[0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17 {1}
|
||||
State: 5 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&!2] 18 {1} [!0&!1&2] 19
|
||||
{1} [!0&1&!2] 20 {1} State: 6 [0&1&2] 8 {1} [!0&1&2] 10 {1} [!0&!1&2]
|
||||
19 {1} [!0&1&!2] 20 {1} [!0&!1&!2] 21 {1} State: 7 [0&1&2] 8 {3}
|
||||
[!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 {1} [!0&!1&!2] 22 {1}
|
||||
State: 8 [!0&!1&!2] 5 {1} [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19
|
||||
{1} [!0&1&!2] 20 {1} State: 9 [0&!1&!2] 5 {1} [0&1&!2] 7 {1} [0&1&2] 8
|
||||
{1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&2] 12 {1} [!0&!1&!2] 23 {1}
|
||||
[!0&!1&2] 24 {1} State: 10 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8
|
||||
{3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {1} [!0&!1&2] 24 {1}
|
||||
[!0&!1&!2] 25 {1} State: 11 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19
|
||||
{1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 12 [0&1&2] 8 {3}
|
||||
[!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 27 {1} [!0&!1&!2] 28 {1}
|
||||
State: 13 [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1}
|
||||
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 13 {1} [!0&1&!2] 14 {1}
|
||||
State: 14 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [!0&1&2] 10 {2}
|
||||
[0&!1&2] 12 {3} [!0&1&!2] 14 {1} [!0&!1&2] 24 {2} [!0&!1&!2] 29 {1}
|
||||
State: 15 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1}
|
||||
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 15 {1} [!0&!1&2] 16 {1}
|
||||
State: 16 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] 11
|
||||
{1} [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17
|
||||
{1} State: 17 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2]
|
||||
11 {1} [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17
|
||||
{1} State: 18 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&!2] 18 {1}
|
||||
[!0&!1&2] 19 {1} [!0&1&!2] 20 {1} State: 19 [0&1&!2] 7 {3} [0&1&2] 8
|
||||
{3} [!0&!1&2] 19 {1} [!0&!1&!2] 30 {1} [!0&1&!2] 31 {1} [!0&1&2] 32
|
||||
{1} State: 20 [0&1&2] 8 {3} [0&!1&2] 12 {1} [!0&1&!2] 20 {1} [!0&1&2]
|
||||
32 {1} [!0&!1&!2] 33 {1} [!0&!1&2] 34 {1} State: 21 [0&1&2] 8 {1}
|
||||
[!0&1&2] 10 {1} [!0&!1&!2] 18 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 {1}
|
||||
State: 22 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20
|
||||
{1} [!0&!1&!2] 35 {1} State: 23 [0&!1&!2] 5 {1} [0&1&!2] 7 {1} [0&1&2]
|
||||
8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&2] 12 {1} [!0&!1&!2] 23
|
||||
{1} [!0&!1&2] 24 {1} State: 24 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2]
|
||||
8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {2} [!0&!1&2] 24
|
||||
{1} [!0&!1&!2] 25 {1} State: 25 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2]
|
||||
8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {2} [!0&!1&2] 24
|
||||
{1} [!0&!1&!2] 25 {1} State: 26 [0&1&2] 8 {3} [!0&1&2] 10 {1}
|
||||
[!0&!1&2] 19 {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 27 [0&1&2]
|
||||
8 {3} [0&!1&2] 12 {3} [!0&1&!2] 27 {1} [!0&1&2] 32 {1} [!0&!1&!2] 36
|
||||
{1} [!0&!1&2] 37 {1} State: 28 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2]
|
||||
19 {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 29 [0&!1&!2] 5 {3}
|
||||
[0&1&!2] 7 {3} [0&1&2] 8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2]
|
||||
14 {1} [!0&!1&2] 24 {2} [!0&!1&!2] 29 {1} State: 30 [0&1&!2] 7 {3}
|
||||
[0&1&2] 8 {3} [!0&!1&2] 19 {1} [!0&!1&!2] 30 {1} [!0&1&!2] 31 {1}
|
||||
[!0&1&2] 32 {1} State: 31 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3}
|
||||
[0&!1&2] 12 {3} [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {2}
|
||||
[!0&!1&!2] 38 {1} State: 32 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8
|
||||
{3} [0&!1&2] 12 {3} [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {1}
|
||||
[!0&!1&!2] 39 {1} State: 33 [0&1&2] 8 {3} [0&!1&2] 12 {1} [!0&1&!2] 20
|
||||
{1} [!0&1&2] 32 {1} [!0&!1&!2] 33 {1} [!0&!1&2] 34 {1} State: 34
|
||||
[0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&!2] 11 {1} [0&!1&2] 12 {1}
|
||||
[!0&1&!2] 31 {1} [!0&1&2] 32 {1} [!0&!1&2] 34 {1} [!0&!1&!2] 40 {1}
|
||||
State: 35 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20
|
||||
{1} [!0&!1&!2] 35 {1} State: 36 [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||
[!0&1&!2] 27 {1} [!0&1&2] 32 {1} [!0&!1&!2] 36 {1} [!0&!1&2] 37 {1}
|
||||
State: 37 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||
[!0&1&!2] 31 {2} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} [!0&!1&!2] 39 {1}
|
||||
State: 38 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||
[!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {2} [!0&!1&!2] 38 {1}
|
||||
State: 39 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||
[!0&1&!2] 31 {2} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} [!0&!1&!2] 39 {1}
|
||||
State: 40 [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&!2] 11 {1} [0&!1&2] 12
|
||||
{1} [!0&1&!2] 31 {1} [!0&1&2] 32 {1} [!0&!1&2] 34 {1} [!0&!1&!2] 40
|
||||
{1} --END--""")
|
||||
aa.merge_states()
|
||||
# This used to cause a segfault reported by Philipp.
|
||||
print(aa.to_str())
|
||||
aa = spot.automaton("""
|
||||
HOA: v1 States: 41 Start: 0 AP: 3 "allfinished" "finished_0"
|
||||
"finished_1" acc-name: parity max odd 4 Acceptance: 4 Inf(3) | (Fin(2)
|
||||
& (Inf(1) | Fin(0))) properties: trans-labels explicit-labels
|
||||
trans-acc colored properties: deterministic --BODY-- State: 0
|
||||
[!0&!1&!2] 1 {1} [!0&!1&2] 2 {1} [!0&1&!2] 3 {1} [!0&1&2] 4 {1}
|
||||
[0&!1&!2] 5 {1} [0&!1&2] 6 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} State: 1
|
||||
[!0&!1&!2] 1 {1} [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1}
|
||||
[!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 {1} [0&!1&2] 12 {1}
|
||||
State: 2 [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1}
|
||||
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 13 {1} [!0&1&!2] 14 {1}
|
||||
State: 3 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1}
|
||||
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 15 {1} [!0&!1&2] 16 {1}
|
||||
State: 4 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] 11 {1}
|
||||
[0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17 {1}
|
||||
State: 5 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&!2] 18 {1} [!0&!1&2] 19
|
||||
{1} [!0&1&!2] 20 {1} State: 6 [0&1&2] 8 {1} [!0&1&2] 10 {1} [!0&!1&2]
|
||||
19 {1} [!0&1&!2] 20 {1} [!0&!1&!2] 21 {1} State: 7 [0&1&2] 8 {3}
|
||||
[!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 {1} [!0&!1&!2] 22 {1}
|
||||
State: 8 [!0&!1&!2] 5 {1} [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19
|
||||
{1} [!0&1&!2] 20 {1} State: 9 [0&!1&!2] 5 {1} [0&1&!2] 7 {1} [0&1&2] 8
|
||||
{1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&2] 12 {1} [!0&!1&!2] 23 {1}
|
||||
[!0&!1&2] 24 {1} State: 10 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8
|
||||
{3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {1} [!0&!1&2] 24 {1}
|
||||
[!0&!1&!2] 25 {1} State: 11 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19
|
||||
{1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 12 [0&1&2] 8 {3}
|
||||
[!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 27 {1} [!0&!1&!2] 28 {1}
|
||||
State: 13 [!0&!1&2] 2 {1} [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1}
|
||||
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 13 {1} [!0&1&!2] 14 {1}
|
||||
State: 14 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [!0&1&2] 10 {2}
|
||||
[0&!1&2] 12 {3} [!0&1&!2] 14 {1} [!0&!1&2] 24 {2} [!0&!1&!2] 29 {1}
|
||||
State: 15 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1}
|
||||
[0&!1&!2] 11 {1} [0&!1&2] 12 {1} [!0&!1&!2] 15 {1} [!0&!1&2] 16 {1}
|
||||
State: 16 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2] 11
|
||||
{1} [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17
|
||||
{1} State: 17 [0&1&!2] 7 {1} [0&1&2] 8 {1} [!0&1&2] 10 {1} [0&!1&!2]
|
||||
11 {1} [0&!1&2] 12 {1} [!0&1&!2] 14 {1} [!0&!1&2] 16 {1} [!0&!1&!2] 17
|
||||
{1} State: 18 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&!2] 18 {1}
|
||||
[!0&!1&2] 19 {1} [!0&1&!2] 20 {1} State: 19 [0&1&!2] 7 {3} [0&1&2] 8
|
||||
{3} [!0&!1&2] 19 {1} [!0&!1&!2] 30 {1} [!0&1&!2] 31 {1} [!0&1&2] 32
|
||||
{1} State: 20 [0&1&2] 8 {3} [0&!1&2] 12 {1} [!0&1&!2] 20 {1} [!0&1&2]
|
||||
32 {1} [!0&!1&!2] 33 {1} [!0&!1&2] 34 {1} State: 21 [0&1&2] 8 {1}
|
||||
[!0&1&2] 10 {1} [!0&!1&!2] 18 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20 {1}
|
||||
State: 22 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20
|
||||
{1} [!0&!1&!2] 35 {1} State: 23 [0&!1&!2] 5 {1} [0&1&!2] 7 {1} [0&1&2]
|
||||
8 {1} [!0&1&!2] 9 {1} [!0&1&2] 10 {1} [0&!1&2] 12 {1} [!0&!1&!2] 23
|
||||
{1} [!0&!1&2] 24 {1} State: 24 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2]
|
||||
8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {2} [!0&!1&2] 24
|
||||
{1} [!0&!1&!2] 25 {1} State: 25 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2]
|
||||
8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2] 14 {2} [!0&!1&2] 24
|
||||
{1} [!0&!1&!2] 25 {1} State: 26 [0&1&2] 8 {3} [!0&1&2] 10 {1}
|
||||
[!0&!1&2] 19 {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 27 [0&1&2]
|
||||
8 {3} [0&!1&2] 12 {3} [!0&1&!2] 27 {1} [!0&1&2] 32 {1} [!0&!1&!2] 36
|
||||
{1} [!0&!1&2] 37 {1} State: 28 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2]
|
||||
19 {1} [!0&!1&!2] 26 {1} [!0&1&!2] 27 {1} State: 29 [0&!1&!2] 5 {3}
|
||||
[0&1&!2] 7 {3} [0&1&2] 8 {3} [!0&1&2] 10 {2} [0&!1&2] 12 {3} [!0&1&!2]
|
||||
14 {1} [!0&!1&2] 24 {2} [!0&!1&!2] 29 {1} State: 30 [0&1&!2] 7 {3}
|
||||
[0&1&2] 8 {3} [!0&!1&2] 19 {1} [!0&!1&!2] 30 {1} [!0&1&!2] 31 {1}
|
||||
[!0&1&2] 32 {1} State: 31 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3}
|
||||
[0&!1&2] 12 {3} [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {2}
|
||||
[!0&!1&!2] 38 {1} State: 32 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8
|
||||
{3} [0&!1&2] 12 {3} [!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {1}
|
||||
[!0&!1&!2] 39 {1} State: 33 [0&1&2] 8 {3} [0&!1&2] 12 {1} [!0&1&!2] 20
|
||||
{1} [!0&1&2] 32 {1} [!0&!1&!2] 33 {1} [!0&!1&2] 34 {1} State: 34
|
||||
[0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&!2] 11 {1} [0&!1&2] 12 {1}
|
||||
[!0&1&!2] 31 {1} [!0&1&2] 32 {1} [!0&!1&2] 34 {1} [!0&!1&!2] 40 {1}
|
||||
State: 35 [0&1&2] 8 {3} [!0&1&2] 10 {1} [!0&!1&2] 19 {1} [!0&1&!2] 20
|
||||
{1} [!0&!1&!2] 35 {1} State: 36 [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||
[!0&1&!2] 27 {1} [!0&1&2] 32 {1} [!0&!1&!2] 36 {1} [!0&!1&2] 37 {1}
|
||||
State: 37 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||
[!0&1&!2] 31 {2} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} [!0&!1&!2] 39 {1}
|
||||
State: 38 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||
[!0&1&!2] 31 {1} [!0&1&2] 32 {2} [!0&!1&2] 37 {2} [!0&!1&!2] 38 {1}
|
||||
State: 39 [0&!1&!2] 5 {3} [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&2] 12 {3}
|
||||
[!0&1&!2] 31 {2} [!0&1&2] 32 {2} [!0&!1&2] 37 {1} [!0&!1&!2] 39 {1}
|
||||
State: 40 [0&1&!2] 7 {3} [0&1&2] 8 {3} [0&!1&!2] 11 {1} [0&!1&2] 12
|
||||
{1} [!0&1&!2] 31 {1} [!0&1&2] 32 {1} [!0&!1&2] 34 {1} [!0&!1&!2] 40
|
||||
{1} --END--""")
|
||||
aa.merge_states()
|
||||
# This used to cause a segfault reported by Philipp.
|
||||
print(aa.to_str())
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue