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

ltl2tgba_fm: fix non-deterministic output

Browse source 
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.
* src/tgbatest/ltl2ta.test: Adjust sizes to the new order.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2014-11-13 18:03:15 +01:00
parent 63da386a66
commit 11aa708a81
3 changed files with 151 additions and 121 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -157,6 +157,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)

222
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -34,6 +34,7 @@
#include <cassert>
#include <memory>
#include <utility>
#include <algorithm>
#include "ltl2tgba_fm.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/sccinfo.hh"
@ -2093,28 +2094,56 @@ namespace spot
}
typedef std::map<bdd, bdd, bdd_less_than> prom_map;
typedef std::unordered_map<const formula*, prom_map> 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_digraph_ptr
ltl_to_tgba_fm(const formula* f, const bdd_dict_ptr& dict,
bool exprop, bool symb_merge, bool branching_postponement,
@ -2206,6 +2235,7 @@ namespace spot
formulae_to_translate.insert(f2);
a->set_init_state(namer->new_state(f2));
dest_map dests;
while (!formulae_to_translate.empty())
{
// Pick one formula.
@ -2216,6 +2246,9 @@ namespace spot
const translate_dict::translated& t = fc.translate(now);
bdd res = t.symbolic;
if (res == bddfalse)
continue;
// Handle exclusive events.
if (unobs)
{
@ -2253,7 +2286,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.
@ -2274,9 +2307,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
@ -2315,39 +2345,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.
auto truef = constant::true_instance();
dest_map::const_iterator i = dests.find(truef);
// 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))
@ -2360,61 +2387,60 @@ 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 == truef)
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 (!namer->has_state(truef))
{
formulae_to_translate.insert(truef);
namer->new_state(truef);
}
namer->new_transition(now, truef, cond_for_true, 0U);
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;
if (dest == truef)
continue;
// 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 = namer->has_state(dest);
// 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;
for (auto& j: i->second)
{
bdd cond = j.second - cond_for_true;
if (cond == bddfalse) // Skip false transitions.
continue;
if (!reachable && !seen)
namer->new_state(dest);
reachable = true;
namer->new_transition(now, dest, cond, d.bdd_to_mark(j.first));
}
// Will this be a new state?
bool seen = namer->has_state(t.dest);
if (reachable && !seen)
formulae_to_translate.insert(dest);
else
dest->destroy();
}
if (!seen)
{
formulae_to_translate.insert(t.dest);
namer->new_state(t.dest);
}
namer->new_transition(now, t.dest, t.cond,
d.bdd_to_mark(t.prom));
if (seen)
t.dest->destroy();
}
else
t.dest->destroy();
}
while (in != dests.end());
}
}
for (auto n: namer->names())

46
src/tgbatest/ltl2ta.test
View file

@ -169,12 +169,12 @@ in: Fa & b & GFc & Gd
-TA -DS -RT | 12 | 126 | 8
-TA -DS -lv | 29 | 315 | 17
-TA -DS -lv -RT | 13 | 140 | 8
-TA -DS -sp | 28 | 306 | 16
-TA -DS -sp -RT | 12 | 134 | 7
-TA -DS -sp | 28 | 309 | 16
-TA -DS -sp -RT | 12 | 137 | 7
-TA -DS -lv -sp | 29 | 315 | 17
-TA -DS -lv -sp -RT | 13 | 140 | 8
-x -TA -DS -in | 29 | 240 | 13
-x -TA -DS -in -RT | 12 | 93 | 7
-x -TA -DS -in | 29 | 254 | 13
-x -TA -DS -in -RT | 12 | 96 | 7
in: Fa & a & GFc & Gc
-TGTA | 4 | 8 | XXX
-TGTA -RT | 3 | 6 | XXX
@ -326,13 +326,13 @@ in: # Make sure '(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))'
in: # has 21 states and 96 transitions before minimization, and
in: # has 20 states and 89 transitions, after minimization.
in: (G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))
-TGTA | 21 | 129 | XXX
-TGTA | 21 | 127 | XXX
-TGTA -RT | 17 | 93 | XXX
-TA | 20 | 92 | 12
-TA -RT | 15 | 57 | 9
-TA -lv | 21 | 104 | 6
-TA -lv -RT | 17 | 75 | 4
-TA -sp | 20 | 102 | 5
-TA -sp | 20 | 100 | 5
-TA -sp -RT | 16 | 70 | 3
-TA -lv -sp | 21 | 104 | 6
-TA -lv -sp -RT | 17 | 75 | 4
@ -340,8 +340,8 @@ in: (G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))
-TA -DS -RT | 18 | 81 | 13
-TA -DS -lv | 21 | 104 | 11
-TA -DS -lv -RT | 20 | 99 | 11
-TA -DS -sp | 20 | 102 | 10
-TA -DS -sp -RT | 19 | 97 | 10
-TA -DS -sp | 20 | 100 | 10
-TA -DS -sp -RT | 19 | 95 | 10
-TA -DS -lv -sp | 21 | 104 | 11
-TA -DS -lv -sp -RT | 20 | 99 | 11
-x -TA -DS -in | 19 | 66 | 9
@ -389,26 +389,26 @@ in: Gq|Gr|(G(q|FGp)&G(r|FG!p))
-x -TA -DS -in | 33 | 152 | 25
-x -TA -DS -in -RT | 21 | 112 | 17
in: FG((WaitRight4 M (HasRight1 W GWaitLeft0)) M HasLeft4)
-TGTA | 45 | 717 | XXX
-TGTA | 45 | 730 | XXX
-TGTA -RT | 35 | 598 | XXX
-TA | 44 | 602 | 16
-TA -RT | 33 | 482 | 9
-TA -lv | 45 | 676 | 9
-TA -lv -RT | 35 | 566 | 4
-TA -sp | 44 | 654 | 8
-TA -sp | 44 | 667 | 8
-TA -sp -RT | 34 | 545 | 3
-TA -lv -sp | 45 | 676 | 9
-TA -lv -sp -RT | 35 | 566 | 4
-TA -DS | 54 | 722 | 26
-TA -DS -RT | 38 | 534 | 17
-TA -DS -RT | 42 | 600 | 19
-TA -DS -lv | 55 | 800 | 19
-TA -DS -lv -RT | 39 | 608 | 11
-TA -DS -sp | 54 | 776 | 18
-TA -DS -sp -RT | 38 | 586 | 10
-TA -DS -lv -RT | 44 | 694 | 13
-TA -DS -sp | 54 | 797 | 18
-TA -DS -sp -RT | 43 | 683 | 12
-TA -DS -lv -sp | 55 | 800 | 19
-TA -DS -lv -sp -RT | 39 | 608 | 11
-x -TA -DS -in | 55 | 696 | 11
-x -TA -DS -in -RT | 42 | 603 | 8
-TA -DS -lv -sp -RT | 44 | 694 | 13
-x -TA -DS -in | 55 | 700 | 11
-x -TA -DS -in -RT | 39 | 566 | 8
in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))
-TGTA | 69 | 1539 | XXX
-TGTA -RT | 49 | 935 | XXX
@ -421,15 +421,15 @@ in: G(F(GWaitLeft7 U Idle4) U (WaitLeft2 M IsEating2))
-TA -lv -sp | 68 | 1443 | 16
-TA -lv -sp -RT | 56 | 1179 | 15
-TA -DS | 124 | 2964 | 44
-TA -DS -RT | 96 | 2099 | 42
-TA -DS -RT | 100 | 2285 | 42
-TA -DS -lv | 125 | 3028 | 42
-TA -DS -lv -RT | 97 | 2149 | 40
-TA -DS -sp | 124 | 3008 | 41
-TA -DS -sp -RT | 96 | 2129 | 39
-TA -DS -lv -RT | 101 | 2339 | 40
-TA -DS -sp | 124 | 3012 | 41
-TA -DS -sp -RT | 100 | 2324 | 39
-TA -DS -lv -sp | 125 | 3028 | 42
-TA -DS -lv -sp -RT | 97 | 2149 | 40
-TA -DS -lv -sp -RT | 101 | 2339 | 40
-x -TA -DS -in | 125 | 1838 | 25
-x -TA -DS -in -RT | 90 | 1368 | 25
-x -TA -DS -in -RT | 89 | 1344 | 25
EOF
sed -n 's/in: \(.*\)/\1/p' checkta.txt > input.txt