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

merge transitions: also merge transitions with same conditions

Browse source 
* src/tgba/tgbagraph.cc (merge_transition): Do it.
* src/tgbatest/readsave.test: Test it.
* src/bin/autfilt.cc: Fix statistics about the original
automaton when using --stats or --name.
This commit is contained in:
Alexandre Duret-Lutz 2014-12-17 09:04:28 +01:00
parent b8a38915e5
commit 8e9c431706
3 changed files with 192 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/bin/autfilt.cc
View file

@ -502,7 +502,11 @@ namespace
spot::stopwatch sw;
sw.start();
auto aut = haut->aut;
// If --stats or --name is used, duplicate the automaton so we
// never modify the original automaton (e.g. with
// merge_transitions()) and the statistics about it make sense.
auto aut = ((format == Stats) || opt_name) ?
spot::make_tgba_digraph(haut->aut) : haut->aut;
// Preprocessing.

43
src/tgba/tgbagraph.cc
View file

@ -80,6 +80,49 @@ namespace spot
if (++out != tend)
trans.resize(out);
tend = out;
out = in = 2;
if (in < tend)
{
typedef graph_t::trans_storage_t tr_t;
g_.sort_transitions_([](const tr_t& lhs, const tr_t& rhs)
{
if (lhs.src < rhs.src)
return true;
if (lhs.src > rhs.src)
return false;
if (lhs.dst < rhs.dst)
return true;
if (lhs.dst > rhs.dst)
return false;
return lhs.cond.id() < rhs.cond.id();
// Do not sort on acceptance, we'll merge
// them.
});
for (; in < tend; ++in)
{
// Merge transitions with the same source, destination,
// and conditions. (We test the source last, for the
// same reason as above.)
if (trans[out].dst == trans[in].dst
&& trans[out].cond.id() == trans[in].cond.id()
&& trans[out].src == trans[in].src)
{
trans[out].acc |= trans[in].acc;
}
else
{
++out;
if (in != out)
trans[out] = trans[in];
}
}
if (++out != tend)
trans.resize(out);
}
g_.chain_transitions_();
}

144
src/tgbatest/readsave.test
View file

@ -126,3 +126,147 @@ cat >expected <<EOF
<Fb U G!a, 3 states>, 7, 1
EOF
diff output expected
cat >input <<EOF
HOA: v1
States: 10
Start: 0
AP: 1 "a"
acc-name: generalized-Buchi 3
Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0 {0}
[!0] 1 {0}
[!0] 2 {0}
[0] 3 {0}
[0] 3 {0 2}
[!0] 2 {0 2}
[!0] 4 {1}
[!0] 5 {1}
[!0] 6 {1}
[!0] 6 {1 2}
[!0] 7 {1}
[!0] 8 {1}
[!0] 9 {1}
[!0] 9 {1 2}
[!0] 4 {0 1}
[!0] 5 {0 1}
[!0] 6 {0 1}
[!0] 6 {0 1 2}
[!0] 7 {0 1}
[!0] 8 {0 1}
[!0] 9 {0 1}
[!0] 9 {0 1 2}
State: 1
[0] 3 {0 2}
State: 2
[!0] 2 {0 2}
[!0] 6 {1 2}
[!0] 9 {1 2}
[!0] 6 {0 1 2}
[!0] 9 {0 1 2}
State: 3
[!0] 1 {0 2}
[!0] 2 {0}
[0] 3 {0 2}
[!0] 2 {0 2}
[!0] 5 {1 2}
[!0] 6 {1}
[!0] 6 {1 2}
[!0] 8 {1 2}
[!0] 9 {1}
[!0] 9 {1 2}
[!0] 5 {0 1 2}
[!0] 6 {0 1}
[!0] 6 {0 1 2}
[!0] 8 {0 1 2}
[!0] 9 {0 1}
[!0] 9 {0 1 2}
State: 4
[!0] 4 {1}
[!0] 5 {1}
[!0] 6 {1}
[!0] 6 {1 2}
[!0] 7
[!0] 8
[!0] 9
[!0] 9 {2}
[!0] 7 {1}
[!0] 8 {1}
[!0] 9 {1}
[!0] 9 {1 2}
State: 5
State: 6
[!0] 6 {1 2}
[!0] 9 {2}
[!0] 9 {1 2}
State: 7
[0] 0 {0}
[0] 3 {0}
[0] 3 {0 2}
State: 8
[0] 3 {0 2}
State: 9
--END--
EOF
cat >expected <<EOF
HOA: v1
name: "63->32 edges, 64->33 transitions"
States: 10
Start: 0
AP: 1 "a"
acc-name: generalized-Buchi 3
Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
properties: trans-labels explicit-labels
--BODY--
State: 0
[t] 0 {0}
[!0] 1 {0}
[!0] 2 {0 2}
[0] 3 {0 2}
[!0] 4 {0 1}
[!0] 5 {0 1}
[!0] 6 {0 1 2}
[!0] 7 {0 1}
[!0] 8 {0 1}
[!0] 9 {0 1 2}
State: 1 {0 2}
[0] 3
State: 2
[!0] 2 {0 2}
[!0] 6 {0 1 2}
[!0] 9 {0 1 2}
State: 3
[!0] 1 {0 2}
[!0] 2 {0 2}
[0] 3 {0 2}
[!0] 5 {0 1 2}
[!0] 6 {0 1 2}
[!0] 8 {0 1 2}
[!0] 9 {0 1 2}
State: 4
[!0] 4 {1}
[!0] 5 {1}
[!0] 6 {1 2}
[!0] 7 {1}
[!0] 8 {1}
[!0] 9 {1 2}
State: 5
State: 6 {1 2}
[!0] 6
[!0] 9
State: 7
[0] 0 {0}
[0] 3 {0 2}
State: 8 {0 2}
[0] 3
State: 9
--END--
EOF
$autfilt --merge -Hm input --name="%E->%e edges, %T->%t transitions" > output
diff output expected