Commit 8362bf3a authored by Alexandre Lewkowicz's avatar Alexandre Lewkowicz Committed by Alexandre Duret-Lutz
Browse files

safra: Ensure parity min even acceptance

* src/tests/safra.cc, src/tests/safra.test:  Use HOA format in tests.
* src/twaalgos/safra.cc:  Make sure the number of sets are always odd so
that cycles without any acceptance set are rejected.
parent d0d42f86
......@@ -26,6 +26,7 @@
#include "hoaparse/public.hh"
#include "ltlparse/public.hh"
#include "twaalgos/dotty.hh"
#include "twaalgos/hoa.hh"
int main(int argc, char* argv[])
......@@ -57,5 +58,11 @@ int main(int argc, char* argv[])
}
res->merge_transitions();
spot::dotty_reachable(std::cout, res);
if (argc >= 4 && !strncmp(argv[3], "-H", 2))
{
spot::hoa_reachable(std::cout, res, "t");
std::cout << std::endl;
}
else
spot::dotty_reachable(std::cout, res);
}
......@@ -41,28 +41,31 @@ State: 1
EOF
cat >out.exp << EOF
digraph G {
rankdir=LR
node [shape="circle"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 1 [label="a"]
1 [label="1"]
1 -> 2 [label="a\n{0}"]
1 -> 3 [label="!a & b\n{3}"]
2 [label="2"]
2 -> 1 [label="a"]
2 -> 3 [label="!a & b"]
3 [label="3"]
3 -> 0 [label="a & !b"]
3 -> 2 [label="a & b"]
3 -> 3 [label="!a & b"]
}
HOA: v1
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[0] 1
State: 1
[0] 2 {0}
[!0&1] 3
State: 2
[0] 1
[!0&1] 3
State: 3
[0&!1] 0
[0&1] 2
[!0&1] 3
--END--
EOF
run 0 ../safra --hoa double_a.hoa > out.dot
diff out.dot out.exp
run 0 ../safra --hoa double_a.hoa -H > out.hoa
diff out.hoa out.exp
cat >double_b.hoa << EOF
HOA: v1
......@@ -83,33 +86,36 @@ State: 1
EOF
cat >out.exp << EOF
digraph G {
rankdir=LR
node [shape="circle"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
0 -> 1 [label="a"]
1 [label="1"]
1 -> 1 [label="a & !b"]
1 -> 2 [label="a & b"]
1 -> 3 [label="!a & b\n{0}"]
2 [label="2"]
2 -> 3 [label="!a & b\n{0}"]
2 -> 4 [label="a & !b"]
2 -> 5 [label="a & b"]
3 [label="3"]
3 -> 0 [label="a & !b"]
3 -> 2 [label="a & b"]
3 -> 3 [label="!a & b\n{0}"]
4 [label="4"]
4 -> 1 [label="a\n{0}"]
4 -> 3 [label="!a & b\n{0}"]
5 [label="5"]
5 -> 1 [label="a\n{0}"]
5 -> 3 [label="!a & b\n{0}"]
}
HOA: v1
States: 6
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[0] 1
State: 1
[0&!1] 1
[0&1] 2
[!0&1] 3 {0}
State: 2
[!0&1] 3 {0}
[0&!1] 4
[0&1] 5
State: 3
[0&!1] 0
[0&1] 2
[!0&1] 3 {0}
State: 4
[0] 1 {0}
[!0&1] 3 {0}
State: 5
[0] 1 {0}
[!0&1] 3 {0}
--END--
EOF
run 0 ../safra --hoa double_b.hoa > out.dot
diff out.dot out.exp
run 0 ../safra --hoa double_b.hoa -H > out.hoa
diff out.hoa out.exp
......@@ -26,6 +26,19 @@
namespace spot
{
namespace
{
// Used to remove all acceptance whos value is above max_acc
void remove_dead_acc(twa_graph_ptr& aut, unsigned max_acc)
{
assert(max_acc < 32);
unsigned mask = (1 << max_acc) - 1;
for (auto& t: aut->transitions())
{
t.acc &= mask;
}
}
}
auto
safra_state::compute_succs(const const_twa_graph_ptr& aut,
const std::vector<unsigned>& bddnums,
......@@ -293,10 +306,10 @@ namespace spot
auto res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut);
res->prop_copy(aut,
{ true, // state based
{ false, // state based
true, // inherently_weak
true, // deterministic
false // stutter inv
false, // deterministic
true // stutter inv
});
// Given a safra_state get its associated state in output automata.
......@@ -309,6 +322,7 @@ namespace spot
seen.insert(std::make_pair(init, num));
std::deque<safra_state> todo;
todo.push_back(init);
unsigned sets = 0;
while (!todo.empty())
{
using succs_t = safra_state::succs_t;
......@@ -332,12 +346,22 @@ namespace spot
seen.insert(std::make_pair(s.first, dst_num));
}
if (s.first.color_ != -1U)
res->new_transition(src_num, dst_num, num2bdd[s.second],
{s.first.color_});
{
res->new_transition(src_num, dst_num, num2bdd[s.second],
{s.first.color_});
// We only care about green acc
if (s.first.color_ % 2 == 0)
sets = std::max(s.first.color_ + 1, sets);
}
else
res->new_transition(src_num, dst_num, num2bdd[s.second]);
}
}
//
remove_dead_acc(res, sets);
res->set_acceptance(sets, acc_cond::acc_code::parity(false, false, sets));
res->prop_deterministic(true);
res->prop_state_based_acc(false);
return res;
}
}
Supports Markdown
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