Commit 4ea63f84 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltl2tgba_fm: fix non-deterministic output

The ltl_to_tgba_fm() translation function was using a hash_map of
maps (ugh!) to merge transitions on output.  However recent libstd++
changed the implementation of hash_map (a.k.a. unordered_map) causing
transitions to be output in a different order.  This
implementation-dependent order caused the ltl2ta.test to fail because
the BA->TA transformation can produce TA of different sizes if you
simply change the order of transitions in the input BA! This does not
sound like a nice property for the BA->TA transformation, but Ala Eddine
isn't sure how to fix it yet.  In the meantime, this patch makes sure
ltl_to_tgba_fm() will return the same output regardless of the
implementation of hash_map.

The ltl2ta.test failure has been observed with g++ 4.9.2 on Arch Linux,
and with gcc-snapshot (5.0.0 20141016) on Debian.

* src/tgbaalgos/ltl2tgba_fm.cc: Rewrite the transition merging
using a std::vector and std::sort instead of nested maps tables.
* NEWS: Mention the fix.
parent 27453810
......@@ -20,6 +20,10 @@ New in spot 1.2.5a (not yet released)
version 8.0 of Org-mode. (This was only a problem if you build
from the git repository, or if you want to edit the
documentation.)
- recent to changes to libstd++ (as shipped by g++ 4.9.2) have
demonstrated that the order of transitions output by the
LTL->TGBA translation used to be dependent on the implementation
of the STL. This is now fixed.
New in spot 1.2.5 (2014-08-21)
......
......@@ -33,6 +33,7 @@
#include "ltlvisit/tostring.hh"
#include <cassert>
#include <memory>
#include <algorithm>
#include "ltl2tgba_fm.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/scc.hh"
......@@ -2109,27 +2110,55 @@ namespace spot
}
typedef std::map<bdd, bdd, bdd_less_than> prom_map;
typedef Sgi::hash_map<const formula*, prom_map, formula_ptr_hash> dest_map;
static void
fill_dests(translate_dict& d, dest_map& dests, bdd label, const formula* dest)
namespace
{
bdd conds = bdd_existcomp(label, d.var_set);
bdd promises = bdd_existcomp(label, d.a_set);
struct transition
{
const formula* dest;
bdd prom;
bdd cond;
dest_map::iterator i = dests.find(dest);
if (i == dests.end())
transition(const formula* dest, bdd cond, bdd prom)
: dest(dest), prom(prom), cond(cond)
{
dests[dest][promises] = conds;
}
else
transition(const transition& other)
: dest(other.dest), prom(other.prom), cond(other.cond)
{
i->second[promises] |= conds;
dest->destroy();
}
}
bool operator<(const transition& other) const
{
ltl::formula_ptr_less_than lt;
if (lt(dest, other.dest))
return true;
if (lt(other.dest, dest))
return false;
if (prom.id() < other.prom.id())
return true;
if (prom.id() > other.prom.id())
return false;
return cond.id() < other.cond.id();
}
};
bool postponement_cmp(const transition& lhs, const transition& rhs)
{
if (lhs.prom.id() < rhs.prom.id())
return true;
if (lhs.prom.id() > rhs.prom.id())
return false;
if (lhs.cond.id() < rhs.cond.id())
return true;
if (lhs.cond.id() > rhs.cond.id())
return false;
ltl::formula_ptr_less_than lt;
return lt(lhs.dest, rhs.dest);
}
typedef std::vector<transition> dest_map;
}
tgba_explicit_formula*
ltl_to_tgba_fm(const formula* f, bdd_dict* dict,
......@@ -2220,6 +2249,7 @@ namespace spot
formulae_to_translate.insert(f2);
a->set_init_state(f2);
dest_map dests;
while (!formulae_to_translate.empty())
{
// Pick one formula.
......@@ -2230,6 +2260,9 @@ namespace spot
const translate_dict::translated& t = fc.translate(now);
bdd res = t.symbolic;
if (res == bddfalse)
continue;
// Handle exclusive events.
if (unobs)
{
......@@ -2267,7 +2300,7 @@ namespace spot
//
// In `exprop' mode, considering all possible combinations of
// outgoing propositions generalizes the above trick.
dest_map dests;
dests.clear();
// Compute all outgoing arcs.
......@@ -2288,9 +2321,6 @@ namespace spot
one_prop_set = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= one_prop_set;
typedef std::map<bdd, const formula*, bdd_less_than> succ_map;
succ_map succs;
// Compute prime implicants.
// The reason we use prime implicants and not bdd_satone()
// is that we do not want to get any negation in front of Next
......@@ -2329,38 +2359,36 @@ namespace spot
if (symb_merge)
dest = fc.canonize(dest);
// If we are not postponing the branching, we can
// declare the outgoing transitions immediately.
// Otherwise, we merge transitions with identical
// label, and declare the outgoing transitions in a
// second loop.
if (!branching_postponement)
{
fill_dests(d, dests, label, dest);
}
else
{
succ_map::iterator si = succs.find(label);
if (si == succs.end())
succs[label] = dest;
else
si->second =
multop::instance(multop::Or, si->second, dest);
}
bdd conds = bdd_existcomp(label, d.var_set);
bdd promises = bdd_existcomp(label, d.a_set);
dests.push_back(transition(dest, conds, promises));
}
if (branching_postponement)
for (succ_map::const_iterator si = succs.begin();
si != succs.end(); ++si)
fill_dests(d, dests, si->first, si->second);
}
// Check for an arc going to 1 (True). Register it first, that
// way it will be explored before others during model checking.
dest_map::const_iterator i = dests.find(constant::true_instance());
// COND_FOR_TRUE is the conditions of the True arc, so we
// can remove them from all other arcs. It might sounds that
// this is not needed when exprop is used, but in fact it is
// complementary.
assert(dests.size() > 0);
if (branching_postponement && dests.size() > 1)
{
std::sort(dests.begin(), dests.end(), postponement_cmp);
// Iterate over all dests, and merge the destination of
// transitions with identical labels.
dest_map::iterator out = dests.begin();
dest_map::const_iterator in = out;
do
{
transition t = *in;
while (++in != dests.end()
&& t.cond == in->cond && t.prom == in->prom)
t.dest = multop::instance(multop::Or, t.dest, in->dest);
*out++ = t;
}
while (in != dests.end());
dests.erase(out, dests.end());
}
std::sort(dests.begin(), dests.end());
// If we have some transitions to true, they are the first
// ones. Remove the sum of their conditions from other
// transitions. It might sounds that this is not needed when
// exprop is used, but in fact it is complementary.
//
// Consider
// f = r(X(1) R p) = p.(1 + r(X(1) R p))
......@@ -2373,67 +2401,59 @@ namespace spot
// f ----> 1
//
// because there is no point in looping on f if we can go to 1.
bdd cond_for_true = bddfalse;
if (i != dests.end())
if (dests.front().dest == constant::true_instance())
{
// When translating LTL for an event-based logic with
// unobservable events, the 1 state should accept all events,
// even unobservable events.
if (unobs && now == constant::true_instance())
cond_for_true = all_events;
else
{
// There should be only one transition going to 1 (true) ...
assert(i->second.size() == 1);
prom_map::const_iterator j = i->second.begin();
// ... and it is not expected to make any promises (unless
// fair loop approximations are used).
assert(fair_loop_approx || j->first == bddtrue);
cond_for_true = j->second;
}
if (!a->has_state(constant::true_instance()))
formulae_to_translate.insert(constant::true_instance());
state_explicit_formula::transition* t =
a->create_transition(now, constant::true_instance());
t->condition = cond_for_true;
dest_map::iterator i = dests.begin();
bdd c = bddfalse;
while (i != dests.end() && i->dest == constant::true_instance())
c |= i++->cond;
for (; i != dests.end(); ++i)
i->cond -= c;
}
// Register other transitions.
for (i = dests.begin(); i != dests.end(); ++i)
{
const formula* dest = i->first;
// The cond_for_true optimization can cause some
// transitions to be removed. So we have to remember
// whether a formula is actually reachable.
bool reachable = false;
// Will this be a new state?
bool seen = a->has_state(dest);
if (dest != constant::true_instance())
{
for (prom_map::const_iterator j = i->second.begin();
j != i->second.end(); ++j)
{
bdd cond = j->second - cond_for_true;
if (cond == bddfalse) // Skip false transitions.
continue;
state_explicit_formula::transition* t =
a->create_transition(now, dest);
t->condition = cond;
d.conj_bdd_to_acc(a, j->first, t);
reachable = true;
}
}
else
{
// "1" is reachable.
reachable = true;
}
if (reachable && !seen)
formulae_to_translate.insert(dest);
else
dest->destroy();
}
// Create transitions in the automaton
{
dest_map::const_iterator in = dests.begin();
do
{
// Merge transitions with same destination and
// acceptance.
transition t = *in;
while (++in != dests.end()
&& t.prom == in->prom && t.dest == in->dest)
{
t.cond |= in->cond;
in->dest->destroy();
}
// Actually create the transition
if (t.cond != bddfalse)
{
// When translating LTL for an event-based logic
// with unobservable events, the 1 state should
// accept all events, even unobservable events.
if (unobs
&& t.dest == constant::true_instance()
&& now == constant::true_instance())
t.cond = all_events;
// Will this be a new state?
bool seen = a->has_state(t.dest);
state_explicit_formula::transition* tt =
a->create_transition(now, t.dest);
tt->condition = t.cond;
d.conj_bdd_to_acc(a, t.prom, tt);
if (!seen)
formulae_to_translate.insert(t.dest);
else
t.dest->destroy();
}
else
t.dest->destroy();
}
while (in != dests.end());
}
}
dict->register_propositions(fc.used_vars(), a);
......
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