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

print_hoa: add support for universal branches

Browse source 
* spot/twaalgos/hoa.cc: Implement it.
* tests/python/alternating.py: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2016-11-24 21:13:13 +01:00
parent 6aad559c29
commit 56df459c75
2 changed files with 52 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

43
spot/twaalgos/hoa.cc
View file

@ -426,13 +426,21 @@ namespace spot
}
os << str;
};
// We do not support alternating automata so far, and it's
// probable that nobody cares about the "no-univ-branch"
// properties. The "univ-branch" properties seems more important
// to announce that the automaton might not be parsable by tools
// that do not support alternating automata.
if (verbose)
prop(" no-univ-branch");
// It's probable that nobody cares about the "no-univ-branch"
// property. The "univ-branch" property seems more important to
// announce that the automaton might not be parsable by tools that
// do not support alternating automata.
if (aut->is_alternating())
{
prop(" univ-branch");
}
else if (verbose)
{
if (v1_1)
prop(" !univ-branch");
else
prop(" no-univ-branch");
}
implicit_labels = md.use_implicit_labels;
state_labels = md.use_state_labels;
if (implicit_labels)
@ -539,6 +547,20 @@ namespace spot
}
os << "--BODY--" << nl;
auto print_dst = [&](unsigned dst)
{
bool notfirst = false;
for (unsigned d: aut->univ_dests(dst))
{
if (notfirst)
os << '&';
else
notfirst = true;
os << d;
}
};
auto sn = aut->get_named_prop<std::vector<std::string>>("state-names");
for (unsigned i = 0; i < num_states; ++i)
{
@ -580,7 +602,8 @@ namespace spot
for (auto& t: aut->out(i))
{
os << '[' << md.sup[t.cond] << "] " << t.dst;
os << '[' << md.sup[t.cond] << "] ";
print_dst(t.dst);
if (this_acc == Hoa_Acceptance_Transitions)
md.emit_acc(os, t.acc);
os << nl;
@ -591,7 +614,7 @@ namespace spot
unsigned n = 0;
for (auto& t: aut->out(i))
{
os << t.dst;
print_dst(t.dst);
if (this_acc == Hoa_Acceptance_Transitions)
{
md.emit_acc(os, t.acc);
@ -637,7 +660,7 @@ namespace spot
unsigned n = out.size();
for (unsigned i = 0; i < n;)
{
os << out[i];
print_dst(out[i]);
if (this_acc != Hoa_Acceptance_States)
{
md.emit_acc(os, outm[i]) << nl;

19
tests/python/alternating.py
View file

@ -50,3 +50,22 @@ try:
except RuntimeError:
received = True
assert received
h = aut.to_str('hoa')
print(h)
assert h == """HOA: v1
States: 3
Start: 0
AP: 2 "p1" "p2"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: univ-branch trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0] 1&2 {0}
[1] 0&1
State: 1
[0&1] 0&2&1
State: 2
[0 | 1] 2
--END--"""