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

ltl_to_tgba_fm: Build a tgba_digraph instead of a tgba_explicit_formula

Browse source 
The conversion is not complete, because the conversion from SERE to DRA
used for the closure operator is still building a tgba_explicit_formula.

* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh: Return
a tgba_digraph.
* src/priv/acccompl.cc: Simplify.
* src/graph/ngraph.hh: Add a way to iterate over all names.
* src/tgba/tgbagraph.hh (compute_support_conditions): Return something
useful.  It's actually used by the constructor of testing automata.
* src/tgbatest/wdba.test: Adjust to the fact that state are not
labeled by formulas anymore.
* src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc: Do not try to enable
UTF8 on automata anymore.
This commit is contained in:
Alexandre Duret-Lutz 2014-08-06 18:31:18 +02:00
parent 38887f4960
commit 7b23691629
8 changed files with 77 additions and 97 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/bin/ltl2tgba.cc
View file

@ -34,6 +34,7 @@
#include "common_post.hh"
#include "ltlast/formula.hh"
#include "ltlvisit/tostring.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
@ -231,17 +232,6 @@ namespace
s.c_str());
}
if (utf8)
{
spot::tgba* a = const_cast<spot::tgba*>(aut);
if (spot::tgba_explicit_formula* tef =
dynamic_cast<spot::tgba_explicit_formula*>(a))
tef->enable_utf8();
else if (spot::sba_explicit_formula* sef =
dynamic_cast<spot::sba_explicit_formula*>(a))
sef->enable_utf8();
}
switch (format)
{
case Dot:

12
src/bin/ltl2tgta.cc
View file

@ -33,6 +33,7 @@
#include "common_post.hh"
#include "ltlparse/public.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/simplify.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
@ -184,17 +185,6 @@ namespace
s.c_str());
}
if (utf8)
{
spot::tgba* a = const_cast<spot::tgba*>(aut);
if (spot::tgba_explicit_formula* tef =
dynamic_cast<spot::tgba_explicit_formula*>(a))
tef->enable_utf8();
else if (spot::sba_explicit_formula* sef =
dynamic_cast<spot::sba_explicit_formula*>(a))
sef->enable_utf8();
}
bdd ap_set = atomic_prop_collect_as_bdd(f, aut);
if (ta_type != TGTA)

10
src/graph/ngraph.hh
View file

@ -94,6 +94,16 @@ namespace spot
return state_to_name.at(s);
}
bool has_state(name n) const
{
return name_to_state.find(n) != name_to_state.end();
}
state_to_name_t& names()
{
return state_to_name;
}
template <typename... Args>
transition
new_transition(name src, name dst, Args&&... args)

12
src/priv/acccompl.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE)
// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
@ -18,6 +18,7 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "acccompl.hh"
#include <cassert>
namespace spot
{
@ -60,6 +61,8 @@ namespace spot
if (acc == bddtrue)
return all_;
assert(acc != bddfalse);
// Since we never cache a unique positive bdd, we can reuse the
// same cache. In fact the only kind of acc we will receive in
// this method, are a conjunction of positive acceptance
@ -70,12 +73,13 @@ namespace spot
bdd res = all_;
bdd cond = acc;
bdd neg = bddtrue;
while (cond != bddtrue)
{
res &= bdd_nithvar(bdd_var(cond));
neg &= bdd_nithvar(bdd_var(cond));
cond = bdd_high(cond);
}
res &= neg;
cache_[acc] = res;
return res;

7
src/tgba/tgbagraph.hh
View file

@ -360,9 +360,12 @@ namespace spot
return neg_acceptance_conditions_;
}
virtual bdd compute_support_conditions(const state*) const
virtual bdd compute_support_conditions(const state* s) const
{
return bddtrue;
bdd sum = bddfalse;
for (auto& t: out(state_number(s)))
sum |= t.cond;
return sum;
}
/// Iterate over all transitions, and merge those with compatible

93
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -36,7 +36,9 @@
#include "ltl2tgba_fm.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/scc.hh"
#include "tgba/tgbaexplicit.hh"
//#include "tgbaalgos/dotty.hh"
#include "priv/acccompl.hh"
namespace spot
{
@ -403,33 +405,6 @@ namespace spot
return multop::instance(multop::OrRat, v);
}
void
conj_bdd_to_acc(tgba_explicit_formula* a, bdd b,
state_explicit_formula::transition* t)
{
assert(b != bddfalse);
while (b != bddtrue)
{
int var = bdd_var(b);
bdd high = bdd_high(b);
if (high == bddfalse)
{
// Simply ignore negated acceptance variables.
b = bdd_low(b);
}
else
{
const formula* ac = var_to_formula(var);
if (!a->has_acceptance_condition(ac))
a->declare_acceptance_condition(ac->clone());
a->add_acceptance_condition(t, ac);
b = high;
}
assert(b != bddfalse);
}
}
const translated&
ltl_to_bdd(const formula* f, bool mark_all, bool recurring = false);
@ -2048,7 +2023,7 @@ namespace spot
}
tgba_explicit_formula*
tgba_digraph*
ltl_to_tgba_fm(const formula* f, bdd_dict* dict,
bool exprop, bool symb_merge, bool branching_postponement,
bool fair_loop_approx, const atomic_prop_set* unobs,
@ -2128,14 +2103,15 @@ namespace spot
bdd all_events = observable_events | unobservable_events;
tgba_explicit_formula* a = new tgba_explicit_formula(dict);
tgba_digraph* a = new tgba_digraph(dict);
auto namer = a->create_namer<const formula*, formula_ptr_hash>();
// This is in case the initial state is equivalent to true...
if (symb_merge)
f2 = fc.canonize(f2);
formulae_to_translate.insert(f2);
a->set_init_state(f2);
a->set_init_state(namer->new_state(f2));
while (!formulae_to_translate.empty())
{
@ -2273,7 +2249,8 @@ namespace spot
// 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());
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
@ -2296,7 +2273,7 @@ namespace spot
// 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())
if (unobs && now == truef)
cond_for_true = all_events;
else
{
@ -2308,44 +2285,38 @@ namespace spot
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;
if (!namer->has_state(truef))
{
formulae_to_translate.insert(truef);
namer->new_state(truef);
}
namer->new_transition(now, truef, cond_for_true, bddtrue);
}
// 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 = a->has_state(dest);
bool seen = namer->has_state(dest);
if (dest != constant::true_instance())
for (auto& j: i->second)
{
for (prom_map::const_iterator j = i->second.begin();
j != i->second.end(); ++j)
{
bdd cond = j->second - cond_for_true;
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.
if (!reachable && !seen)
namer->new_state(dest);
reachable = true;
namer->new_transition(now, dest, cond, j.first);
}
if (reachable && !seen)
formulae_to_translate.insert(dest);
else
@ -2353,9 +2324,21 @@ namespace spot
}
}
for (auto n: namer->names())
n->destroy();
delete namer;
dict->register_propositions(fc.used_vars(), a);
a->set_acceptance_conditions(d.a_set);
// Turn all promises into real acceptance conditions.
a->complement_all_acceptance_conditions();
acc_compl ac(a->all_acceptance_conditions(),
a->neg_acceptance_conditions());
unsigned ns = a->num_states();
for (unsigned s = 0; s < ns; ++s)
for (auto& t: a->out(s))
t.acc = ac.reverse_complement(t.acc);
if (!simplifier)
// This should not be deleted before we have registered all propositions.

8
src/tgbaalgos/ltl2tgba_fm.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -24,14 +24,14 @@
# define SPOT_TGBAALGOS_LTL2TGBA_FM_HH
#include "ltlast/formula.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgba/tgbagraph.hh"
#include "ltlvisit/apcollect.hh"
#include "ltlvisit/simplify.hh"
namespace spot
{
/// \ingroup tgba_ltl
/// \brief Build a spot::tgba_explicit* from an LTL formula.
/// \brief Build a spot::tgba_digraph* from an LTL formula.
///
/// This is based on the following paper.
/** \verbatim
@ -122,7 +122,7 @@ namespace spot
\endverbatim */
///
/// \return A spot::tgba_explicit that recognizes the language of \a f.
SPOT_API tgba_explicit_formula*
SPOT_API tgba_digraph*
ltl_to_tgba_fm(const ltl::formula* f, bdd_dict* dict,
bool exprop = false, bool symb_merge = true,
bool branching_postponement = false,

16
src/tgbatest/wdba.test
View file

@ -120,14 +120,14 @@ while read f; do
# If the labels of the state have only digits, assume the minimization
# worked.
x=`../ltl2tgba -f -Rm "!($f)" |
grep -v -- '->' |
sed -n 's/.*label="\(..*\)".*/\1/p' |
tr -d '0-9\n'`
case $x in
"") echo "wrongly minimized !($f)"; success=false;;
*) echo "OK !($f)";;
esac
../ltl2tgba -kt -Rm "!($f)" > out1
../ltl2tgba -kt -R3 "!($f)" > out2
if cmp out1 out2; then
echo "OK !($f)";
else
echo "wrongly minimized !($f)";
success=false;
fi
done < non-obligations.txt
$success