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

* src/tgba/succiterconcrete.hh (next_succ_set_): Rename as ...

Browse source 
(succ_set_left_): ... this.
(current_base_, current_base_left_): New variables.
* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::first):
Reset current_.
(tgba_succ_iterator_concrete::next): Rewrite.
(tgba_succ_iterator_concrete::current_state): Simplify.
(tgba_succ_iterator_concrete::current_accepting_conditions): Remove
atomic proposition with universal quantification.
* src/tgba/ltl2tgba.cc (ltl_to_tgba): Normalize the formula.
* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state):
Complete the initial state.
(tgba_bdd_concrete::succ_iter): Do not remove Now variable
from the BDD passed to the iterator.
* tgba/tgbabddcoredata.hh (notnow_set, var_set): New variables.
* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust
to update notnow_set and var_set.
This commit is contained in:
Alexandre Duret-Lutz 2003-06-25 15:15:30 +00:00
parent 35be07c472
commit 6d0546c317
8 changed files with 216 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

18
ChangeLog
View file

@ -1,5 +1,23 @@
2003-06-25 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/succiterconcrete.hh (next_succ_set_): Rename as ...
(succ_set_left_): ... this.
(current_base_, current_base_left_): New variables.
* src/tgba/succiterconcrete.cc (tgba_succ_iterator_concrete::first):
Reset current_.
(tgba_succ_iterator_concrete::next): Rewrite.
(tgba_succ_iterator_concrete::current_state): Simplify.
(tgba_succ_iterator_concrete::current_accepting_conditions): Remove
atomic proposition with universal quantification.
* src/tgba/ltl2tgba.cc (ltl_to_tgba): Normalize the formula.
* src/tgba/tgbabddconcrete.cc (tgba_bdd_concrete::set_init_state):
Complete the initial state.
(tgba_bdd_concrete::succ_iter): Do not remove Now variable
from the BDD passed to the iterator.
* tgba/tgbabddcoredata.hh (notnow_set, var_set): New variables.
* tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: Adjust
to update notnow_set and var_set.
* src/tgbatest/ltl2tgba.cc: Support -v.
2003-06-24 Alexandre Duret-Lutz <aduret@src.lip6.fr>

20
src/tgba/ltl2tgba.cc
View file

@ -1,5 +1,8 @@
#include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/lunabbrev.hh"
#include "ltlvisit/nenoform.hh"
#include "ltlvisit/destroy.hh"
#include "tgbabddconcretefactory.hh"
#include <cassert>
@ -211,12 +214,23 @@ namespace spot
tgba_bdd_concrete
ltl_to_tgba(const ltl::formula* f)
{
// Normalize the formula. We want all the negation on
// the atomic proposition. We also suppress logic
// abbreviation such as <=>, =>, or XOR, since they
// would involve negations at the BDD level.
const ltl::formula* f1 = ltl::unabbreviate_logic(f);
const ltl::formula* f2 = ltl::negative_normal_form(f1);
ltl::destroy(f1);
// Traverse the formula and draft the automaton in a factory.
tgba_bdd_concrete_factory fact;
ltl_trad_visitor v(fact);
f->accept(v);
f2->accept(v);
ltl::destroy(f2);
fact.finish();
tgba_bdd_concrete g(fact);
g.set_init_state(v.result());
// Finally setup the resulting automaton.
tgba_bdd_concrete g(fact, v.result());
return g;
}
}

124
src/tgba/succiterconcrete.cc
View file

@ -5,8 +5,12 @@ namespace spot
{
tgba_succ_iterator_concrete::tgba_succ_iterator_concrete
(const tgba_bdd_core_data& d, bdd successors)
: data_(d), succ_set_(successors), next_succ_set_(successors),
current_(bddfalse)
: data_(d),
succ_set_(successors),
succ_set_left_(successors),
current_(bddfalse),
current_base_(bddfalse),
current_base_left_(bddfalse)
{
}
@ -17,7 +21,8 @@ namespace spot
void
tgba_succ_iterator_concrete::first()
{
next_succ_set_ = succ_set_;
succ_set_left_ = succ_set_;
current_ = bddfalse;
if (!done())
next();
}
@ -26,28 +31,117 @@ namespace spot
tgba_succ_iterator_concrete::next()
{
assert(!done());
// succ_set_ is the set of successors we have to explore. it
// contains Now/Next variable and atomic propositions. Each
// satisfaction of succ_set_ represents a transition, and we want
// to compute as little transitions as possible. However one
// important constraint is that all Next variables must appear in
// the satisfaction.
//
// For instance if succ_set_ was
// Now[a] * !Now[b] * (c + d) * (Next[a] + Next[b])
// we'd like to enumerate the following six transitions
// c * Next[a] * Next[b]
// c * Next[a] * !Next[b]
// c * !Next[a] * Next[b]
// d * Next[a] * Next[b]
// d * Next[a] * !Next[b]
// d * !Next[a] * Next[b]
// (We don't really care about the Now variables here.)
//
// Calling bdd_fullsatone on succ_set_ would compute many more
// transitions (twice as much on this example), since all
// atomic propositions would have to appear.
//
// Basically, we want to use bdd_satone for atomic propositions
// and bdd_fullsatone for Next variable. We achieve this as
// follows
// (1) compute a (non-full) satisfaction of succ_set_
// e.g. Now[a] * !Now[b] * c * Next[a]
// (2) retain only the atomic propositions (here: c), and call it
// our current base
// (3) compute a full satisfaction for succ_set_ & current_base_
// Now[a] * !Now[b] * c * d * Next[a] * Next[b]
// (4) retain only the Next variables
// Next[a] * Next[b]
// (5) and finally append them to the current base
// c * Next[a] * Next[b]
// This is the first successor.
//
// This algorithm would compute only one successor. In order to
// iterate over the other ones, we have a couple of variables that
// remember what has been explored so far and what is yet to
// explore.
//
// The next time we compute a successor, we start at (3) and
// compute the *next* full satisfaction matching current_base_. The
// current_base_left_ serves this purpose: holding all the
// current_base_ satisfactions that haven't yet been explored.
//
// Once we've explored all satisfactions of current_base_, we
// start over at (1) and compute the *next* (non-full)
// satisfaction of succ_set_. To that effect, the variable
// next_succ_set hold all these satisfactions that must still be
// explored.
//
// Note: on this example we would not exactly get the six transitions
// mentionned, but maybe something like
// c * Next[a] * Next[b]
// c * Next[a] * !Next[b]
// c * !Next[a] * Next[b]
// d * !c * Next[a] * Next[b]
// d * !c * Next[a] * !Next[b]
// d * !c * !Next[a] * Next[b]
// depending on the BDD order.
// FIXME: Iterating on the successors this way (calling bdd_satone
// and NANDing out the result from the set) requires several descent
// of the BDD. Maybe it would be faster to compute all satisfying
// formula in one operation.
next_succ_set_ &= !current_;
current_ = bdd_satone(next_succ_set_);
// FIXME: It would help to have this half-full half-partial
// satisfaction operation available as one BDD function.
// FIXME: Iterating on the successors this way (calling
// bdd_satone/bdd_fullsetone and NANDing out the result from a
// set) requires several descent of the BDD. Maybe it would be
// faster to compute all satisfying formula in one operation.
do
{
if (current_ == bddfalse)
{
succ_set_left_ &= !current_base_;
if (succ_set_left_ == bddfalse) // No more successors?
return;
// (1) (2)
current_base_ = bdd_exist(bdd_satone(succ_set_left_),
data_.notvar_set);
current_base_left_ = current_base_;
}
// (3) (4) (5)
current_ =
current_base_ & bdd_exist(bdd_fullsatone(succ_set_left_
& current_base_left_),
data_.notnext_set);
current_base_left_ &= !current_;
}
while (// No more successors with the current_base_? Compute
// the next base.
current_ == bddfalse
// The destination state, computed here, should be
// compatible with the transition relation. Otherwise
// it won't have any successor and useless.
|| ((current_state_ = bdd_replace(bdd_exist(current_,
data_.notnext_set),
data_.next_to_now))
& data_.relation) == bddfalse);
}
bool
tgba_succ_iterator_concrete::done()
{
return next_succ_set_ == bddfalse;
return succ_set_left_ == bddfalse;
}
state_bdd*
tgba_succ_iterator_concrete::current_state()
{
assert(!done());
return new state_bdd(bdd_replace(bdd_exist(current_, data_.notnext_set),
data_.next_to_now));
return new state_bdd(current_state_);
}
bdd
@ -61,7 +155,9 @@ namespace spot
tgba_succ_iterator_concrete::current_accepting_conditions()
{
assert(!done());
return bdd_exist(bdd_restrict(data_.accepting_conditions, current_),
return bdd_exist(bdd_forall(bdd_restrict(data_.accepting_conditions,
current_),
data_.var_set),
data_.notacc_set);
}

27
src/tgba/succiterconcrete.hh
View file

@ -13,12 +13,14 @@ namespace spot
public:
/// \brief Build a spot::tgba_succ_iterator_concrete.
///
/// \param successors The set of successors with ingoing conditions
/// and promises, represented as a BDD. The job of this iterator
/// will be to enumerate the satisfactions of that BDD and split
/// them into destination state, conditions, and promises.
/// \param d The core data of the automata. These contains
/// sets of variables useful to split a BDD.
/// \param successors The set of successors with ingoing
/// conditions and accepting conditions, represented as a BDD.
/// The job of this iterator will be to enumerate the
/// satisfactions of that BDD and split them into destination
/// states and conditions, and compute accepting conditions.
/// \param d The core data of the automata.
/// These contains sets of variables useful to split a BDD, and
/// compute accepting conditions.
tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors);
virtual ~tgba_succ_iterator_concrete();
@ -33,10 +35,17 @@ namespace spot
bdd current_accepting_conditions();
private:
const tgba_bdd_core_data& data_; ///< Core data of the automata.
const tgba_bdd_core_data& data_; ///< Core data of the automaton.
bdd succ_set_; ///< The set of successors.
bdd next_succ_set_; ///< Unexplored successors (including current_).
bdd current_; ///< Current successor.
bdd succ_set_left_; ///< Unexplored successors (including current_).
bdd current_; ///< Current successor, as a conjunction of
/// atomic proposition and Next variables.
bdd current_state_; ///< Current successor, as a
/// conjunction of Now variables.
bdd current_base_; ///< Current successor base.
bdd current_base_left_; ///< Used to lists all possible full satisfaction
/// current_base_ which haven't been explored.
};
}

35
src/tgba/tgbabddconcrete.cc
View file

@ -10,8 +10,9 @@ namespace spot
}
tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init)
: data_(fact.get_core_data()), dict_(fact.get_dict()), init_(init)
: data_(fact.get_core_data()), dict_(fact.get_dict())
{
set_init_state(init);
}
tgba_bdd_concrete::~tgba_bdd_concrete()
@ -21,6 +22,36 @@ namespace spot
void
tgba_bdd_concrete::set_init_state(bdd s)
{
// Usually, the ltl2tgba translator will return an
// initial state which does not include all true Now variables,
// even though the truth of some Now variables is garanteed.
//
// For instance, when building the automata for the formula GFa,
// the translator will define the following two equivalences
// Now[Fa] <=> a | (Prom[a] & Next[Fa])
// Now[GFa] <=> Now[Fa] & Next[GFa]
// and return Now[GFa] as initial state.
//
// Starting for state Now[GFa], we could then build
// the following automaton:
// In state Now[GFa]:
// if `a', go to state Now[GFa] & Now[Fa]
// if `!a', go to state Now[GFa] & Now[Fa] with Prom[a]
// In state Now[GFa] & Now[Fa]:
// if `a', go to state Now[GFa] & Now[Fa]
// if `!a', go to state Now[GFa] & Now[Fa] with Prom[a]
//
// As we can see, states Now[GFa] and Now[GFa] & Now[Fa] share
// the same actions. This is no surprise, because
// Now[GFa] <=> Now[GFa] & Now[Fa] according to the equivalences
// defined by the translator.
//
// This happens because we haven't completed the initial
// state with the value of other Now variables. We can
// complete this state with the other equivalant Now variables
// here, but we can't do anything about the remaining unknown
// variables.
s &= bdd_relprod(s, data_.relation, data_.notnow_set);
init_ = s;
}
@ -41,7 +72,7 @@ namespace spot
{
const state_bdd* s = dynamic_cast<const state_bdd*>(state);
assert(s);
bdd succ_set = bdd_exist(data_.relation & s->as_bdd(), data_.now_set);
bdd succ_set = data_.relation & s->as_bdd();
return new tgba_succ_iterator_concrete(data_, succ_set);
}

12
src/tgba/tgbabddcoredata.cc
View file

@ -4,7 +4,8 @@ namespace spot
{
tgba_bdd_core_data::tgba_bdd_core_data()
: relation(bddtrue), accepting_conditions(bddfalse),
now_set(bddtrue), negnow_set(bddtrue), notnext_set(bddtrue),
now_set(bddtrue), negnow_set(bddtrue),
notnow_set(bddtrue), notnext_set(bddtrue), var_set(bddtrue),
notvar_set(bddtrue), notacc_set(bddtrue), negacc_set(bddtrue),
next_to_now(bdd_newpair())
{
@ -13,7 +14,8 @@ namespace spot
tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& copy)
: relation(copy.relation), accepting_conditions(copy.accepting_conditions),
now_set(copy.now_set), negnow_set(copy.negnow_set),
notnext_set(copy.notnext_set), notvar_set(copy.notvar_set),
notnow_set(copy.notnow_set), notnext_set(copy.notnext_set),
var_set(copy.var_set), notvar_set(copy.notvar_set),
notacc_set(copy.notacc_set), negacc_set(copy.negacc_set),
next_to_now(bdd_copypair(copy.next_to_now))
{
@ -27,7 +29,9 @@ namespace spot
| right.accepting_conditions),
now_set(left.now_set & right.now_set),
negnow_set(left.negnow_set & right.negnow_set),
notnow_set(left.notnow_set & right.notnow_set),
notnext_set(left.notnext_set & right.notnext_set),
var_set(left.var_set & right.var_set),
notvar_set(left.notvar_set & right.notvar_set),
notacc_set(left.notacc_set & right.notacc_set),
negacc_set(left.negacc_set & right.negacc_set),
@ -57,6 +61,7 @@ namespace spot
now_set &= now;
negnow_set &= !now;
notnext_set &= now;
notnow_set &= next;
bdd both = now & next;
notvar_set &= both;
notacc_set &= both;
@ -65,13 +70,16 @@ namespace spot
void
tgba_bdd_core_data::declare_atomic_prop(bdd var)
{
notnow_set &= var;
notnext_set &= var;
notacc_set &= var;
var_set &= var;
}
void
tgba_bdd_core_data::declare_accepting_condition(bdd acc)
{
notnow_set &= acc;
notnext_set &= acc;
notvar_set &= acc;
negacc_set &= !acc;

10
src/tgba/tgbabddcoredata.hh
View file

@ -31,9 +31,9 @@ namespace spot
/// in which a transition is. Actually we never return Acc[x]
/// alone, but Acc[x] and all other accepting variables negated.
///
/// So if there is three accepting set \c a, \c b, and \c c, and
/// So if there is three accepting set \c a, \c b, and \c c, and
/// a transition is in set \c a, we'll return \c Acc[a]&!Acc[b]&!Acc[c].
/// If the transition is in both \c a and \c b, we'll return
/// If the transition is in both \c a and \c b, we'll return
/// \c (Acc[a]\&!Acc[b]\&!Acc[c]) \c | \c (!Acc[a]\&Acc[b]\&!Acc[c]).
///
/// Accepting conditions are attributed to transitions and are
@ -65,9 +65,15 @@ namespace spot
/// The conjunction of all Now variables, in their negated form.
bdd negnow_set;
/// \brief The (positive) conjunction of all variables which are
/// not Now variables.
bdd notnow_set;
/// \brief The (positive) conjunction of all variables which are
/// not Next variables.
bdd notnext_set;
/// \brief The (positive) conjunction of all variables which are
/// atomic propositions.
bdd var_set;
/// \brief The (positive) conjunction of all variables which are
/// not atomic propositions.
bdd notvar_set;
/// The (positive) conjunction of all variables which are not

2
src/tgba/tgbabddtranslatefactory.cc
View file

@ -16,8 +16,10 @@ namespace spot
data_.accepting_conditions = bdd_replace(in.accepting_conditions, rewrite);
data_.now_set = bdd_replace(in.now_set, rewrite);
data_.negnow_set = bdd_replace(in.negnow_set, rewrite);
data_.notnow_set = bdd_replace(in.notnow_set, rewrite);
data_.notnext_set = bdd_replace(in.notnext_set, rewrite);
data_.notvar_set = bdd_replace(in.notvar_set, rewrite);
data_.var_set = bdd_replace(in.var_set, rewrite);
data_.notacc_set = bdd_replace(in.notacc_set, rewrite);
init_ = bdd_replace(from.get_init_bdd(), rewrite);