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

improve translation of ms-phi-h=2..3

Browse source 
* spot/twaalgos/gfguarantee.cc: Rework the history computation to keep
an overapproximation of the history, and a longer one.  Also replay
the history even if there is no initial trivial SCC.  This helps with
translating FG(!a|XXXb) where we need to keep the history of a, but we
were previously unable to do so because some state had both "a" and
"ab" as input.
* spot/twaalgos/translate.cc: Optimize the product of suspendable
automata by removing useless trivial SCCs.
* tests/core/genltl.test, tests/core/satmin.test, NEWS: Adjust
expected results.
This commit is contained in:
Alexandre Duret-Lutz 2018-06-20 17:46:11 +02:00
parent c9131aee72
commit 621fb818e3
5 changed files with 135 additions and 61 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -113,8 +113,8 @@ New in spot 2.5.3.dev (not yet released)
(GFa1 & GFa2) -> GFz 12 1 1 (GFa1 & GFa2) -> GFz 12 1 1
(GFa1 & GFa2 & GFa3) -> GFz 41 1 1 (GFa1 & GFa2 & GFa3) -> GFz 41 1 1
FG(a|b)|FG(!a|Xb) 4 2 2 FG(a|b)|FG(!a|Xb) 4 2 2
FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21 5 4 FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21 4 4
FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170 15 8 FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170 8 8
- print_dot(), used to print automata in GraphViz's format, - print_dot(), used to print automata in GraphViz's format,
underwent several changes: underwent several changes:

138
spot/twaalgos/gfguarantee.cc
View file

@ -27,6 +27,7 @@
#include <spot/twaalgos/minimize.hh> #include <spot/twaalgos/minimize.hh>
#include <spot/twaalgos/dualize.hh> #include <spot/twaalgos/dualize.hh>
#include <spot/twaalgos/isdet.hh> #include <spot/twaalgos/isdet.hh>
// #include <spot/twa/bddprint.hh>
namespace spot namespace spot
{ {
@ -54,6 +55,7 @@ namespace spot
static twa_graph_ptr static twa_graph_ptr
do_g_f_terminal_inplace(scc_info& si, bool state_based) do_g_f_terminal_inplace(scc_info& si, bool state_based)
{ {
bool want_merge_edges = false;
twa_graph_ptr aut = std::const_pointer_cast<twa_graph>(si.get_aut()); twa_graph_ptr aut = std::const_pointer_cast<twa_graph>(si.get_aut());
if (!is_terminal_automaton(aut, &si, true)) if (!is_terminal_automaton(aut, &si, true))
@ -82,56 +84,56 @@ namespace spot
// state. However if some successor of the initial state is // state. However if some successor of the initial state is
// also trivial, we might be able to remove it as well if we // also trivial, we might be able to remove it as well if we
// are able to replay two step from the initial state: this // are able to replay two step from the initial state: this
// can be generalized to more depth and require computing some // can be generalized to more depth and requires computing
// history for each state (i.e., a common suffix to all finite // some history for each state (i.e., a common suffix to all
// words leading to this state). // finite words leading to this state).
//
// We will replay such histories regardless of whether there
// is actually some trivial leading SCCs that could be
// removed, because it reduces the size of cycles in the
// automaton, and this helps getting smaller products when
// combining several automata generated this way.
std::vector<std::vector<bdd>> histories; std::vector<std::vector<bdd>> histories;
bool initial_state_trivial = si.is_trivial(si.initial()); bool initial_state_trivial = si.is_trivial(si.initial());
if (is_det && initial_state_trivial) if (is_det)
{ {
// Compute the max number of steps we want to keep in // Compute the max number of steps we want to keep in
// the history of each state. This is the largest // the history of each state. This is the length of the
// number of trivial SCCs you can chain from the initial // maximal path we can build from the initial state.
// state. unsigned max_histories;
unsigned max_histories = 1;
{ {
std::vector<unsigned> depths(ns, 0U); std::vector<unsigned> depths(ns, 0U);
for (unsigned d: si.succ(ns - 1)) for (unsigned scc = 0; scc < ns; ++scc)
depths[d] = 2;
for (int scc = ns - 2; scc >= 0; --scc)
{ {
if (!si.is_trivial(scc)) unsigned depth = 0;
continue; for (unsigned succ: si.succ(scc))
unsigned sccd = depths[scc]; depth = std::max(depth, depths[succ]);
max_histories = std::max(max_histories, sccd); depths[scc] = depth + si.states_of(scc).size();
++sccd;
for (unsigned d: si.succ(scc))
depths[d] = std::max(depths[d], sccd);
} }
max_histories = depths[ns - 1] - 1;
} }
unsigned numstates = aut->num_states(); unsigned numstates = aut->num_states();
histories.resize(numstates); histories.resize(numstates);
// Compute the one-letter history of each state. If all // Compute the one-letter history of each state. If all
// transition entering a state have the same label, the history // transition entering a state have the same label, the
// is that label. Otherwise set it to bddfalse. // history is that label. Otherwise, we make a
// disjunction of all those labels, so that what we have
// is an over-approximation of the history.
for (auto& e: aut->edges()) for (auto& e: aut->edges())
{ {
std::vector<bdd>& hd = histories[e.dst]; std::vector<bdd>& hd = histories[e.dst];
if (hd.empty()) if (hd.empty())
hd.push_back(e.cond); hd.push_back(e.cond);
else if (hd[0] != e.cond) else
hd[0] = bddfalse; hd[0] |= e.cond;
} }
// remove all bddfalse, and check if there is a chance to build // check if there is a chance to build a larger history.
// a larger history.
bool should_continue = false; bool should_continue = false;
for (auto&h: histories) for (auto&h: histories)
if (h.empty()) if (h.empty())
continue; continue;
else if (h[0] == bddfalse)
h.pop_back();
else else
should_continue = true; should_continue = true;
// Augment those histories with more letters. // Augment those histories with more letters.
@ -152,9 +154,11 @@ namespace spot
else else
hd.push_back(bddfalse); hd.push_back(bddfalse);
} }
else if (hs.size() < historypos else
|| hd[historypos] != hs[historypos - 1])
{ {
if (hs.size() >= historypos)
hd[historypos] |= hs[historypos - 1];
else
hd[historypos] = bddfalse; hd[historypos] = bddfalse;
} }
} }
@ -163,7 +167,6 @@ namespace spot
for (unsigned n = 0; n < numstates; ++n) for (unsigned n = 0; n < numstates; ++n)
{ {
auto& h = histories[n]; auto& h = histories[n];
//for (auto&h: histories)
if (h.size() <= historypos) if (h.size() <= historypos)
continue; continue;
else if (h[historypos] == bddfalse) else if (h[historypos] == bddfalse)
@ -196,10 +199,14 @@ namespace spot
// It will loop // It will loop
if (term[si.scc_of(e.dst)]) if (term[si.scc_of(e.dst)])
{ {
if (!initial_state_trivial
// If the source state is the initial state, we // If the source state is the initial state, we
// should not try to combine it with itself... // should not try to combine it with itself...
|| e.src == init) //
// Also if the automaton is not deterministic
// and there is no trivial initial state, then
// we simply loop back to the initial state.
if (e.src == init
|| (!is_det && !initial_state_trivial))
{ {
e.dst = init; e.dst = init;
e.acc = {0}; e.acc = {0};
@ -224,11 +231,13 @@ namespace spot
// history will get us back the terminal state. In both // history will get us back the terminal state. In both
// cases, we should try again with a smaller history. // cases, we should try again with a smaller history.
unsigned moved_init = init; unsigned moved_init = init;
bdd econd = e.cond;
bool first;
if (is_det) if (is_det)
{ {
auto& h = histories[e.src]; auto& h = histories[e.src];
int hsize = h.size(); int hsize = h.size();
for (int hlen = hsize - 1; hlen > 0; --hlen) for (int hlen = hsize - 1; hlen >= 0; --hlen)
{ {
for (int pos = hlen - 1; pos >= 0; --pos) for (int pos = hlen - 1; pos >= 0; --pos)
{ {
@ -248,16 +257,66 @@ namespace spot
} }
// we have successfully played all history // we have successfully played all history
// to a non-terminal state. // to a non-terminal state.
//
// Combine this edge with any compatible edge from
// the initial state.
first = true;
for (auto& ei: aut->out(moved_init))
{
bdd cond = ei.cond & econd;
if (cond != bddfalse)
{
// We should never reach the terminal state,
// unless the history is empty. In that
// case (ts=true) we have to make a loop to
// the initial state without any
// combination.
bool ts = term[si.scc_of(ei.dst)];
if (ts && hlen > 0)
goto failed;
if (ts)
want_merge_edges = true;
if (first)
{
e.acc = {0};
e.cond = cond;
first = false;
if (!ts)
{
e.dst = ei.dst;
if (new_init == -1U)
new_init = e.src;
}
else
{
new_init = e.dst = init;
}
}
else
{
if (ts)
{
aut->new_edge(e.src, init, cond, {0});
new_init = init;
}
else
{
aut->new_edge(e.src, ei.dst,
cond, {0});
}
}
}
}
break; break;
failed: failed:
moved_init = init; moved_init = init;
continue; continue;
} }
} }
// Combine this edge with any compatible edge from else
// the initial state. {
bdd econd = e.cond; first = true;
bool first = true;
for (auto& ei: aut->out(moved_init)) for (auto& ei: aut->out(moved_init))
{ {
bdd cond = ei.cond & econd; bdd cond = ei.cond & econd;
@ -269,16 +328,15 @@ namespace spot
e.acc = {0}; e.acc = {0};
e.cond = cond; e.cond = cond;
first = false; first = false;
if (new_init == -1U)
new_init = e.src;
} }
else else
{ {
aut->new_edge(e.src, ei.dst, cond, {0}); aut->new_edge(e.src, ei.dst, cond, {0});
} }
} }
} }
}
} }
else else
{ {
@ -315,6 +373,8 @@ namespace spot
} }
aut->purge_unreachable_states(); aut->purge_unreachable_states();
if (want_merge_edges)
aut->merge_edges();
return aut; return aut;
} }
} }

14
spot/twaalgos/translate.cc
View file

@ -27,6 +27,7 @@
#include <spot/twaalgos/gfguarantee.hh> #include <spot/twaalgos/gfguarantee.hh>
#include <spot/twaalgos/isdet.hh> #include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/product.hh> #include <spot/twaalgos/product.hh>
#include <spot/twaalgos/sccinfo.hh>
namespace spot namespace spot
{ {
@ -264,6 +265,19 @@ namespace spot
else else
susp_aut = product_or(susp_aut, one); susp_aut = product_or(susp_aut, one);
} }
if (susp_aut->prop_universal().is_true())
{
// In a deterministic and suspendable automaton, all
// state recognize the same language, so we can move
// the initial state into a bottom accepting SCC.
scc_info si(susp_aut, scc_info_options::NONE);
if (si.is_trivial(si.scc_of(susp_aut->get_init_state_number())))
{
assert(!si.is_trivial(0));
susp_aut->set_init_state(si.one_state_of(0));
susp_aut->purge_unreachable_states();
}
}
if (aut == nullptr) if (aut == nullptr)
aut = susp_aut; aut = susp_aut;
else if (is_and) else if (is_and)

6
tests/core/genltl.test
View file

@ -191,9 +191,9 @@ cat >exp<<EOF
"ms-phi-s=2",1 "ms-phi-s=2",1
"ms-phi-h=0",1 "ms-phi-h=0",1
"ms-phi-h=1",2 "ms-phi-h=1",2
"ms-phi-h=2",5 "ms-phi-h=2",4
"ms-phi-h=3",19 "ms-phi-h=3",8
"ms-phi-h=4",83 "ms-phi-h=4",16
"gf-equiv=0",1 "gf-equiv=0",1
"gf-equiv=1",1 "gf-equiv=1",1
"gf-equiv=2",1 "gf-equiv=2",1

4
tests/core/satmin.test
View file

@ -660,8 +660,8 @@ cat >expected <<'EOF'
"!(G((p0) -> ((p1) U (p2))))","15",3 "!(G((p0) -> ((p1) U (p2))))","15",3
"!(G((p0) -> ((p1) U (p2))))","16",3 "!(G((p0) -> ((p1) U (p2))))","16",3
"!(G((p0) -> ((p1) U (p2))))","17",3 "!(G((p0) -> ((p1) U (p2))))","17",3
"G(F((p0) <-> (X(X(p1)))))","1",6 "G(F((p0) <-> (X(X(p1)))))","1",4
"G(F((p0) <-> (X(X(p1)))))","2",6 "G(F((p0) <-> (X(X(p1)))))","2",4
"G(F((p0) <-> (X(X(p1)))))","3",4 "G(F((p0) <-> (X(X(p1)))))","3",4
"G(F((p0) <-> (X(X(p1)))))","4",4 "G(F((p0) <-> (X(X(p1)))))","4",4
"G(F((p0) <-> (X(X(p1)))))","6",4 "G(F((p0) <-> (X(X(p1)))))","6",4