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

Switch from "promises" to "accepting set". Fix the definitions

Browse source 
of these accepting set so that they are really usable.  Provide
a all_accepting_conditions() method for use in the emptyness
check, and a neg_accepting_conditions() for products.
Predeclare TGBA accepting conditions is the i/o.

* src/tgba/bddprint.cc (want_prom): Rename as ...
(want_prom): ... this.
(print_handler): Adjust to display Acc[].
(print_acc_handler, bdd_print_acc): New functions.
* src/tgba/bddprint.hh (print_acc_handler, bdd_print_acc):
New functions.
* src/tgba/succiter.hh (current_promise): Rename as ...
(current_accepting_conditions): ... this.
* src/tgba/succiterconcrete.cc (current_state):
Rename next to now.
(current_promise): Rename as ...
(current_accepting_conditions): ... this, and compute
the accepting conditions.
* src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
src/tgba/succiterconcrete.hh,
src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabddtranslatefactory.cc,
src/tgbaalgos/dotty.cc: Adjust to new names.
* src/tgba/tgba.hh (all_accepting_conditions,
neg_accepting_conditions): New functions.
* src/tgba/tgbabddconcretefactory.cc: Adjust to new
names, and record accepting conditions instead of promises.
* src/tgba/tgbabddcoredata.hh (accepting_conditions,
all_accepting_conditions, negacc_set): New variables.
(notnow_set, notprom_set, declare_promise): Rename as ...
(notnext_set, notacc_set, declare_accepting_condition): ... these.
* src/tgba/tgbaexplicit.hh
(tgba_explicit_succ_iterator::current_promise): Rename as ...
(tgba_explicit_succ_iterator::current_accepting_conditions): ... this.
(tgba_explicit::add_promise): Rename as ...
(tgba_explicit::add_accepting_condition): ... this.
(tgba_explicit::declare_accepting_condition,
tgba_explicit::has_accepting_condition): New variables.
(tgba_explicit::get_promise): Rename as ...
(tgba_explicit::get_accepting_condition): ... this.
(tgba_explicit::all_accepting_conditions,
tgba_explicit::neg_accepting_conditions): Implement them.
(all_accepting_conditions, neg_accepting_conditions,
all_accepting_conditions): New variables.
(tgba_explicit_succ_iterator): Embed all_accepting_conditions_.
* src/tgba/tgbaexplicit.cc: Likewise.
* src/tgba/tgbaproduct.hh
(tgba_product_succ_uterator): Embed left_neg_ and right_neg_.
(tgba_product::all_accepting_conditions,
tgba_product::neg_accepting_conditions): Implement them.
* src/tgba/tgbatranslateproxy.hh:
(tgba_translate_proxy::all_accepting_conditions,
tgba_translate_proxy::neg_accepting_conditions): Implement them.
* src/tgba/tgbatranslateproxy.cc: Likewise.
* src/tgbaalgos/save.cc (save_rec): Call bdd_print
(tgba_save_reachable): Output the `acc =' line.
* src/tgbaparse/tgbaparse.yy: Support the for
accepting conditions definitions using an "acc =" line
at the start.  Later, use has_accepting_condition while
parsing	accepting conditions to ensure they were declared.
Disallow !cond in accepting conditions.
* src/tgbaparse/tgbascan.ll (ACC_DEF): New token.
* src/tgbatest/explicit.cc (main): Declare accepting conditions.
* src/tgbatest/ltl2tgba.cc (main): Add support for the -a, -A,
and -R new options.
* src/tgbatest/tgbaread.cc (main): Really exit on parse error.
* src/tgbatest/explicit.test, src/tgbatest/explprod.test,
src/tgbatest/mixprod.test, src/tgbatest/readsave.test,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Reflect
recent changes.
This commit is contained in:
Alexandre Duret-Lutz 2003-06-23 17:28:26 +00:00
parent fbbfda43f2
commit 25e6cca4b4
37 changed files with 662 additions and 220 deletions
Download patch file Download diff file Expand all files Collapse all files

76
ChangeLog
View file

@ -1,3 +1,79 @@
2003-06-23 Alexandre Duret-Lutz <aduret@src.lip6.fr>
Switch from "promises" to "accepting set". Fix the definitions
of these accepting set so that they are really usable. Provide
a all_accepting_conditions() method for use in the emptyness
check, and a neg_accepting_conditions() for products.
Predeclare TGBA accepting conditions is the i/o.
* src/tgba/bddprint.cc (want_prom): Rename as ...
(want_prom): ... this.
(print_handler): Adjust to display Acc[].
(print_acc_handler, bdd_print_acc): New functions.
* src/tgba/bddprint.hh (print_acc_handler, bdd_print_acc):
New functions.
* src/tgba/succiter.hh (current_promise): Rename as ...
(current_accepting_conditions): ... this.
* src/tgba/succiterconcrete.cc (current_state):
Rename next to now.
(current_promise): Rename as ...
(current_accepting_conditions): ... this, and compute
the accepting conditions.
* src/tgba/dictunion.cc, src/tgba/ltl2tgba.cc,
src/tgba/succiterconcrete.hh,
src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
src/tgba/tgbabdddict.hh, src/tgba/tgbabdddict.cc,
src/tgba/tgbabddtranslatefactory.cc,
src/tgbaalgos/dotty.cc: Adjust to new names.
* src/tgba/tgba.hh (all_accepting_conditions,
neg_accepting_conditions): New functions.
* src/tgba/tgbabddconcretefactory.cc: Adjust to new
names, and record accepting conditions instead of promises.
* src/tgba/tgbabddcoredata.hh (accepting_conditions,
all_accepting_conditions, negacc_set): New variables.
(notnow_set, notprom_set, declare_promise): Rename as ...
(notnext_set, notacc_set, declare_accepting_condition): ... these.
* src/tgba/tgbaexplicit.hh
(tgba_explicit_succ_iterator::current_promise): Rename as ...
(tgba_explicit_succ_iterator::current_accepting_conditions): ... this.
(tgba_explicit::add_promise): Rename as ...
(tgba_explicit::add_accepting_condition): ... this.
(tgba_explicit::declare_accepting_condition,
tgba_explicit::has_accepting_condition): New variables.
(tgba_explicit::get_promise): Rename as ...
(tgba_explicit::get_accepting_condition): ... this.
(tgba_explicit::all_accepting_conditions,
tgba_explicit::neg_accepting_conditions): Implement them.
(all_accepting_conditions, neg_accepting_conditions,
all_accepting_conditions): New variables.
(tgba_explicit_succ_iterator): Embed all_accepting_conditions_.
* src/tgba/tgbaexplicit.cc: Likewise.
* src/tgba/tgbaproduct.hh
(tgba_product_succ_uterator): Embed left_neg_ and right_neg_.
(tgba_product::all_accepting_conditions,
tgba_product::neg_accepting_conditions): Implement them.
* src/tgba/tgbatranslateproxy.hh:
(tgba_translate_proxy::all_accepting_conditions,
tgba_translate_proxy::neg_accepting_conditions): Implement them.
* src/tgba/tgbatranslateproxy.cc: Likewise.
* src/tgbaalgos/save.cc (save_rec): Call bdd_print
(tgba_save_reachable): Output the `acc =' line.
* src/tgbaparse/tgbaparse.yy: Support the for
accepting conditions definitions using an "acc =" line
at the start. Later, use has_accepting_condition while
parsing accepting conditions to ensure they were declared.
Disallow !cond in accepting conditions.
* src/tgbaparse/tgbascan.ll (ACC_DEF): New token.
* src/tgbatest/explicit.cc (main): Declare accepting conditions.
* src/tgbatest/ltl2tgba.cc (main): Add support for the -a, -A,
and -R new options.
* src/tgbatest/tgbaread.cc (main): Really exit on parse error.
* src/tgbatest/explicit.test, src/tgbatest/explprod.test,
src/tgbatest/mixprod.test, src/tgbatest/readsave.test,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Reflect
recent changes.
2003-06-22 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgbatest/tripprod.test, src/tgbatest/explprod.test:

49
src/tgba/bddprint.cc
View file

@ -8,8 +8,8 @@ namespace spot
/// Global dictionary used by print_handler() to lookup variables.
static const tgba_bdd_dict* dict;
/// Global flag to enable Prom[x] output (instead of `x').
static bool want_prom;
/// Global flag to enable Acc[x] output (instead of `x').
static bool want_acc;
/// Stream handler used by Buddy to display BDD variables.
static void
@ -21,12 +21,12 @@ namespace spot
to_string(isi->second, o);
else
{
isi = dict->prom_formula_map.find(var);
if (isi != dict->prom_formula_map.end())
isi = dict->acc_formula_map.find(var);
if (isi != dict->acc_formula_map.end())
{
if (want_prom)
if (want_acc)
{
o << "Prom[";
o << "Acc[";
to_string(isi->second, o) << "]";
}
else
@ -83,9 +83,34 @@ namespace spot
{
dict = &d;
where = &os;
want_prom = false;
assert (bdd_satone(b) == b);
bdd_allsat (b, print_sat_handler);
want_acc = false;
assert(bdd_satone(b) == b);
bdd_allsat(b, print_sat_handler);
return os;
}
static void
print_acc_handler(char* varset, int size)
{
for (int v = 0; v < size; ++v)
{
if (varset[v] < 0)
continue;
if (varset[v] > 0)
{
*where << " ";
print_handler(*where, v);
}
}
}
std::ostream&
bdd_print_acc(std::ostream& os, const tgba_bdd_dict& d, bdd b)
{
dict = &d;
where = &os;
want_acc = false;
bdd_allsat(b, print_acc_handler);
return os;
}
@ -101,7 +126,7 @@ namespace spot
bdd_print_set(std::ostream& os, const tgba_bdd_dict& d, bdd b)
{
dict = &d;
want_prom = true;
want_acc = true;
bdd_strm_hook(print_handler);
os << bddset << b;
bdd_strm_hook(0);
@ -120,7 +145,7 @@ namespace spot
bdd_print_dot(std::ostream& os, const tgba_bdd_dict& d, bdd b)
{
dict = &d;
want_prom = true;
want_acc = true;
bdd_strm_hook(print_handler);
os << bdddot << b;
bdd_strm_hook(0);
@ -131,7 +156,7 @@ namespace spot
bdd_print_table(std::ostream& os, const tgba_bdd_dict& d, bdd b)
{
dict = &d;
want_prom = true;
want_acc = true;
bdd_strm_hook(print_handler);
os << bddtable << b;
bdd_strm_hook(0);

8
src/tgba/bddprint.hh
View file

@ -26,6 +26,14 @@ namespace spot
/// \return The BDD formated as a string.
std::string bdd_format_sat(const tgba_bdd_dict& dict, bdd b);
/// \brief Print a BDD as a list of accepting conditions.
///
/// This is used when saving a TGBA.
/// \param b The BDD to print.
/// \return The BDD formated as a string.
std::ostream& bdd_print_acc(std::ostream& os,
const tgba_bdd_dict& dict, bdd b);
/// \brief Print a BDD as a set.
/// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables.

8
src/tgba/dictunion.cc
View file

@ -29,9 +29,9 @@ namespace spot
var.insert(i->first);
// Merge promises.
for (i = l.prom_map.begin(); i != l.prom_map.end(); ++i)
for (i = l.acc_map.begin(); i != l.acc_map.end(); ++i)
prom.insert(i->first);
for (i = r.prom_map.begin(); i != r.prom_map.end(); ++i)
for (i = r.acc_map.begin(); i != r.acc_map.end(); ++i)
prom.insert(i->first);
// Ensure we have enough BDD variables.
@ -54,8 +54,8 @@ namespace spot
for (f = prom.begin(); f != prom.end(); ++f)
{
clone(*f);
res.prom_map[*f] = v;
res.prom_formula_map[v] = *f;
res.acc_map[*f] = v;
res.acc_formula_map[v] = *f;
++v;
}
for (f = var.begin(); f != var.end(); ++f)

17
src/tgba/ltl2tgba.cc
View file

@ -73,12 +73,13 @@ namespace spot
fact_.add_relation(bdd_apply(now, x | next, bddop_biimp));
/*
`x | next', doesn't actually encode the fact that x
should be fulfilled at eventually. So we declare any
transition going to NEXT without checking X as
"promising x". This promises will be checked by during
the emptiness check.
should be fulfilled at eventually. We ensure
this by creating a new generalized Büchi accepting set,
Acc[x], and leave any transition going to NEXT without
checking X out of this set. Such accepting conditions
are checked for during the emptiness check.
*/
fact_.declare_promise(next & !x, node->child());
fact_.declare_accepting_condition(x | !next, node->child());
res_ = now;
return;
}
@ -145,10 +146,10 @@ namespace spot
/*
The rightmost conjunction, f1 & next, doesn't actually
encode the fact that f2 should be fulfilled eventually.
We declare a promise for this purpose (see the comment
in the unop::F case).
We declare an accepting condition for this purpose (see
the comment in the unop::F case).
*/
fact_.declare_promise(next & !f2, node->second());
fact_.declare_accepting_condition(f2 | !next, node->second());
res_ = now;
return;
}

5
src/tgba/succiter.hh
View file

@ -68,8 +68,9 @@ namespace spot
virtual state* current_state() = 0;
/// \brief Get the condition on the transition leading to this successor.
virtual bdd current_condition() = 0;
/// \brief Get the promise on the transition leading to this successor.
virtual bdd current_promise() = 0;
/// \brief Get the accepting conditions on the transition leading
/// to this successor.
virtual bdd current_accepting_conditions() = 0;
//@}
};

9
src/tgba/succiterconcrete.cc
View file

@ -45,7 +45,9 @@ namespace spot
tgba_succ_iterator_concrete::current_state()
{
assert(!done());
return new state_bdd(bdd_exist(current_, data_.notnow_set));
return new state_bdd(bdd_replace(bdd_exist(current_, data_.notnext_set),
data_.next_to_now));
}
bdd
@ -56,10 +58,11 @@ namespace spot
}
bdd
tgba_succ_iterator_concrete::current_promise()
tgba_succ_iterator_concrete::current_accepting_conditions()
{
assert(!done());
return bdd_exist(current_, data_.notprom_set);
return bdd_exist(bdd_restrict(data_.accepting_conditions, current_),
data_.notacc_set);
}
}

2
src/tgba/succiterconcrete.hh
View file

@ -30,7 +30,7 @@ namespace spot
// inspection
state_bdd* current_state();
bdd current_condition();
bdd current_promise();
bdd current_accepting_conditions();
private:
const tgba_bdd_core_data& data_; ///< Core data of the automata.

22
src/tgba/tgba.hh
View file

@ -77,6 +77,28 @@ namespace spot
/// This formating is the responsability of the automata
/// who owns the state.
virtual std::string format_state(const state* state) const = 0;
/// \brief Return the set of all accepting conditions used
/// by this automaton.
///
/// The goal of the emptiness check is to ensure that
/// a strongly connected component walks through each
/// of these acceptiong conditions. I.e., the union
/// of the acceptiong conditions of all transition in
/// the SCC should be equal to the result of this function.
virtual bdd all_accepting_conditions() const = 0;
/// \brief Return the conjuction of all negated accepting
/// variables.
///
/// For instance if the automaton uses variables \c Acc[a],
/// \c Acc[b] and \c Acc[c] to describe accepting sets,
/// this function should return \c !Acc[a]\&!Acc[b]\&!Acc[c].
///
/// This is useful when making products: each operand conditions
/// set should be augmented with the neg_accepting_conditions() of
/// the other operand.
virtual bdd neg_accepting_conditions() const = 0;
};
}

16
src/tgba/tgbabddconcrete.cc
View file

@ -41,9 +41,7 @@ namespace spot
{
const state_bdd* s = dynamic_cast<const state_bdd*>(state);
assert(s);
bdd succ_set = bdd_replace(bdd_exist(data_.relation & s->as_bdd(),
data_.now_set),
data_.next_to_now);
bdd succ_set = bdd_exist(data_.relation & s->as_bdd(), data_.now_set);
return new tgba_succ_iterator_concrete(data_, succ_set);
}
@ -61,6 +59,18 @@ namespace spot
return dict_;
}
bdd
tgba_bdd_concrete::all_accepting_conditions() const
{
return data_.all_accepting_conditions;
}
bdd
tgba_bdd_concrete::neg_accepting_conditions() const
{
return data_.negacc_set;
}
const tgba_bdd_core_data&
tgba_bdd_concrete::get_core_data() const
{

3
src/tgba/tgbabddconcrete.hh
View file

@ -52,6 +52,9 @@ namespace spot
/// rules, etc.
const tgba_bdd_core_data& get_core_data() const;
virtual bdd all_accepting_conditions() const;
virtual bdd neg_accepting_conditions() const;
protected:
tgba_bdd_core_data data_; ///< Core data associated to the automaton.
tgba_bdd_dict dict_; ///< Dictionary used by the automaton.

60
src/tgba/tgbabddconcretefactory.cc
View file

@ -1,14 +1,13 @@
#include "ltlvisit/clone.hh"
#include "ltlvisit/destroy.hh"
#include "tgbabddconcretefactory.hh"
namespace spot
{
tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory()
{
promise_map_::iterator pi;
for (pi = prom_.begin(); pi != prom_.end(); ++pi)
destroy(pi->first);
acc_map_::iterator ai;
for (ai = acc_.begin(); ai != acc_.end(); ++ai)
destroy(ai->first);
}
int
@ -56,43 +55,50 @@ namespace spot
}
void
tgba_bdd_concrete_factory::declare_promise(bdd b,
const ltl::formula* p)
tgba_bdd_concrete_factory::declare_accepting_condition(bdd b,
const ltl::formula* a)
{
// Maintain a disjunction of BDDs associated to P.
// We will latter (in tgba_bdd_concrete_factory::finish())
// record this disjunction as equivalant to P.
promise_map_::iterator pi = prom_.find(p);
if (pi == prom_.end())
// Maintain a conjunction of BDDs associated to A. We will latter
// (in tgba_bdd_concrete_factory::finish()) associate this
// conjunction to A.
acc_map_::iterator ai = acc_.find(a);
if (ai == acc_.end())
{
p = clone(p);
prom_[p] = b;
a = clone(a);
acc_[a] = b;
}
else
{
pi->second |= b;
ai->second &= b;
}
}
void
tgba_bdd_concrete_factory::finish()
{
promise_map_::iterator pi;
for (pi = prom_.begin(); pi != prom_.end(); ++pi)
acc_map_::iterator ai;
for (ai = acc_.begin(); ai != acc_.end(); ++ai)
{
// Register a BDD variable for this promise.
int p = create_node();
const ltl::formula* f = clone(pi->first); // The promised formula.
dict_.prom_map[f] = p;
dict_.prom_formula_map[p] = f;
// Register a BDD variable for this accepting condition.
int a = create_node();
const ltl::formula* f = clone(ai->first); // The associated formula.
dict_.acc_map[f] = a;
dict_.acc_formula_map[a] = f;
bdd acc = ithvar(a);
// Keep track of all accepting conditions for easy
// existential quantification.
data_.declare_accepting_condition(acc);
}
for (ai = acc_.begin(); ai != acc_.end(); ++ai)
{
bdd acc = ithvar(dict_.acc_map[ai->first]);
bdd prom = ithvar(p);
// Keep track of all promises for easy existential quantification.
data_.declare_promise(prom);
// Complete acc with all the other accepting conditions negated.
acc &= bdd_exist(data_.negacc_set, acc);
// The promise P must hold if we have to verify any of the
// (BDD) formulae registered.
add_relation(bdd_apply(prom, pi->second, bddop_biimp));
// Any state matching the BDD formulae registered is part
// of this accepting set.
data_.accepting_conditions |= ai->second & acc;
}
}

19
src/tgba/tgbabddconcretefactory.hh
View file

@ -34,17 +34,18 @@ namespace spot
/// can be turned into BDD using ithvar().
int create_atomic_prop(const ltl::formula* f);
/// Declare a promise.
///
/// \param b that BDD of the expression that makes a promise
/// \param p the formula promised
/// Declare an accepting condition.
///
/// Formula such as 'f U g' or 'F g' make the promise
/// that 'g' will be fulfilled eventually. So once
/// one of this formula has been translated into a BDD,
/// we use declare_promise() to associate the promise 'g'
/// to this BDD.
void declare_promise(bdd b, const ltl::formula* p);
/// we use declare_accepting_condition() to associate
/// all other states to the accepting set of 'g'.
///
/// \param b a BDD indicating which variables are in the
/// accepting set
/// \param a the formula associated
void declare_accepting_condition(bdd b, const ltl::formula* a);
const tgba_bdd_core_data& get_core_data() const;
const tgba_bdd_dict& get_dict() const;
@ -63,8 +64,8 @@ namespace spot
tgba_bdd_core_data data_; ///< Core data for the new automata.
tgba_bdd_dict dict_; ///< Dictionary for the new automata.
typedef std::map<const ltl::formula*, bdd> promise_map_;
promise_map_ prom_; ///< BDD associated to each promises
typedef std::map<const ltl::formula*, bdd> acc_map_;
acc_map_ acc_; ///< BDD associated to each accepting condition
};
}

35
src/tgba/tgbabddcoredata.cc
View file

@ -3,17 +3,18 @@
namespace spot
{
tgba_bdd_core_data::tgba_bdd_core_data()
: relation(bddtrue),
now_set(bddtrue), negnow_set(bddtrue), notnow_set(bddtrue),
notvar_set(bddtrue), notprom_set(bddtrue), next_to_now(bdd_newpair())
: relation(bddtrue), accepting_conditions(bddfalse),
now_set(bddtrue), negnow_set(bddtrue), notnext_set(bddtrue),
notvar_set(bddtrue), notacc_set(bddtrue), negacc_set(bddtrue),
next_to_now(bdd_newpair())
{
}
tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& copy)
: relation(copy.relation),
: relation(copy.relation), accepting_conditions(copy.accepting_conditions),
now_set(copy.now_set), negnow_set(copy.negnow_set),
notnow_set(copy.notnow_set), notvar_set(copy.notvar_set),
notprom_set(copy.notprom_set),
notnext_set(copy.notnext_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))
{
}
@ -22,11 +23,14 @@ namespace spot
tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& left,
const tgba_bdd_core_data& right)
: relation(left.relation & right.relation),
accepting_conditions(left.accepting_conditions
| 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),
notvar_set(left.notvar_set & right.notvar_set),
notprom_set(left.notprom_set & right.notprom_set),
notacc_set(left.notacc_set & right.notacc_set),
negacc_set(left.negacc_set & right.negacc_set),
next_to_now(bdd_mergepairs(left.next_to_now, right.next_to_now))
{
}
@ -52,23 +56,24 @@ namespace spot
{
now_set &= now;
negnow_set &= !now;
notnow_set &= next;
notnext_set &= now;
bdd both = now & next;
notvar_set &= both;
notprom_set &= both;
notacc_set &= both;
}
void
tgba_bdd_core_data::declare_atomic_prop(bdd var)
{
notnow_set &= var;
notprom_set &= var;
notnext_set &= var;
notacc_set &= var;
}
void
tgba_bdd_core_data::declare_promise(bdd prom)
tgba_bdd_core_data::declare_accepting_condition(bdd acc)
{
notnow_set &= prom;
notvar_set &= prom;
notnext_set &= acc;
notvar_set &= acc;
negacc_set &= !acc;
}
}

65
src/tgba/tgbabddcoredata.hh
View file

@ -10,28 +10,72 @@ namespace spot
{
/// \brief encodes the transition relation of the TGBA.
///
/// \c relation uses four kinds of variables:
/// \c relation uses three kinds of variables:
/// \li "Now" variables, that encode the current state
/// \li "Next" variables, that encode the destination state
/// \li atomic propositions, which are things to verify before going on
/// to the next state
/// \li promises: \c a \c U \c b, or \c F \c b, both imply that \c b
/// should be verified eventually. We encode this with \c Prom[b],
/// and check that promises are fullfilled in the emptyness check.
bdd relation;
/// \brief encodes the accepting conditions
///
/// \c a \c U \c b, or \c F \c b, both imply that \c b
/// should be verified eventually. We encode this with generalized
/// Büchi acceptating conditions. An accepting set, called Acc[b],
/// hold all the state that do not promise to verify \c b eventually.
/// (I.e., all the states that contain \c b, or do not conatain
/// \c a \c U \c b, or \c F \c b.)
///
/// The spot::succ_iter::current_accepting_conditions() method
/// will return the Acc[x] variables of the accepting sets
/// 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
/// 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
/// \c (Acc[a]\&!Acc[b]\&!Acc[c]) \c | \c (!Acc[a]\&Acc[b]\&!Acc[c]).
///
/// Accepting conditions are attributed to transitions and are
/// only concerned by atomic propositions (which label the
/// transitions) and Next variables (the destination). Typically,
/// a transition should bear the variable Acc[b] if it doesn't
/// check for `b' and have a destination of the form \c a \c U \c
/// b, or \c F \c b.
///
/// To summarize, \c accepting_conditions contains three kinds of
/// variables:
/// \li "Next" variables, that encode the destination state,
/// \li atomic propositions, which are things to verify before going on
/// to the next state,
/// \li promise variables.
bdd accepting_conditions;
/// The set of all accepting conditions used by the Automaton.
///
/// The goal of the emptiness check is to ensure that
/// a strongly connected component walks through each
/// of these acceptiong conditions. I.e., the union
/// of the acceptiong conditions of all transition in
/// the SCC should be equal to the result of this function.
bdd all_accepting_conditions;
/// The conjunction of all Now variables, in their positive form.
bdd now_set;
/// 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;
/// not Next variables.
bdd notnext_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 promises.
bdd notprom_set;
/// The (positive) conjunction of all variables which are not
/// accepting conditions.
bdd notacc_set;
/// The negative conjunction of all variables which are accepting
/// conditions.
bdd negacc_set;
/// Record pairings between Next and Now variables.
bddPair* next_to_now;
@ -60,8 +104,9 @@ namespace spot
/// \brief Update the variable sets to take a new automic proposition into
/// account.
void declare_atomic_prop(bdd var);
/// Update the variable sets to take a new promise into account.
void declare_promise(bdd prom);
/// \brief Update the variable sets to take a new accepting condition
/// into account.
void declare_accepting_condition(bdd prom);
};
}

18
src/tgba/tgbabdddict.cc
View file

@ -23,8 +23,8 @@ namespace spot
os << " " << sii->second + 1 << ": Next[";
to_string(sii->first, os) << "]" << std::endl;
}
os << "Promises:" << std::endl;
for (sii = prom_map.begin(); sii != prom_map.end(); ++sii)
os << "Accepting Conditions:" << std::endl;
for (sii = acc_map.begin(); sii != acc_map.end(); ++sii)
{
os << " " << sii->second << ": ";
to_string(sii->first, os) << std::endl;
@ -48,10 +48,10 @@ namespace spot
if (i2 == now_map.end() || i->second != i2->second)
return false;
}
for (i = other.prom_map.begin(); i != other.prom_map.end(); ++i)
for (i = other.acc_map.begin(); i != other.acc_map.end(); ++i)
{
fv_map::const_iterator i2 = prom_map.find(i->first);
if (i2 == prom_map.end() || i->second != i2->second)
fv_map::const_iterator i2 = acc_map.find(i->first);
if (i2 == acc_map.end() || i->second != i2->second)
return false;
}
return true;
@ -66,15 +66,15 @@ namespace spot
now_formula_map(other.now_formula_map),
var_map(other.var_map),
var_formula_map(other.var_formula_map),
prom_map(other.prom_map),
prom_formula_map(other.prom_formula_map)
acc_map(other.acc_map),
acc_formula_map(other.acc_formula_map)
{
fv_map::iterator i;
for (i = now_map.begin(); i != now_map.end(); ++i)
ltl::clone(i->first);
for (i = var_map.begin(); i != var_map.end(); ++i)
ltl::clone(i->first);
for (i = prom_map.begin(); i != prom_map.end(); ++i)
for (i = acc_map.begin(); i != acc_map.end(); ++i)
ltl::clone(i->first);
}
@ -96,7 +96,7 @@ namespace spot
ltl::destroy(i->first);
for (i = var_map.begin(); i != var_map.end(); ++i)
ltl::destroy(i->first);
for (i = prom_map.begin(); i != prom_map.end(); ++i)
for (i = acc_map.begin(); i != acc_map.end(); ++i)
ltl::destroy(i->first);
}

8
src/tgba/tgbabdddict.hh
View file

@ -16,12 +16,12 @@ namespace spot
/// BDD-variable-to-formula maps.
typedef std::map<int, const ltl::formula*> vf_map;
fv_map now_map; ///< Maps formulae to "Now" BDD variables.
vf_map now_formula_map; ///< Maps "Now" BDD variables to formulae.
fv_map now_map; ///< Maps formulae to "Now" BDD variables
vf_map now_formula_map; ///< Maps "Now" BDD variables to formulae
fv_map var_map; ///< Maps atomic propisitions to BDD variables
vf_map var_formula_map; ///< Maps BDD variables to atomic propisitions
fv_map prom_map; ///< Maps promises to BDD variables.
vf_map prom_formula_map; ///< Maps BDD variables to promises.
fv_map acc_map; ///< Maps accepting conditions to BDD variables
vf_map acc_formula_map; ///< Maps BDD variables to accepting conditions
/// \brief Dump all variables for debugging.
/// \param os The output stream.

14
src/tgba/tgbabddtranslatefactory.cc
View file

@ -13,11 +13,12 @@ namespace spot
const tgba_bdd_core_data& in = from.get_core_data();
data_.relation = bdd_replace(in.relation, rewrite);
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_.notprom_set = bdd_replace(in.notprom_set, rewrite);
data_.notacc_set = bdd_replace(in.notacc_set, rewrite);
init_ = bdd_replace(from.get_init_bdd(), rewrite);
@ -40,7 +41,6 @@ namespace spot
{
i_to = dict_.now_map.find(i_from->first);
assert(i_to != dict_.now_map.end());
bdd_setpair(rewrite, i_from->second, i_to->second);
bdd_setpair(rewrite, i_from->second + 1, i_to->second + 1);
bdd_setpair(data_.next_to_now, i_to->second + 1, i_to->second);
@ -51,12 +51,12 @@ namespace spot
assert(i_to != dict_.var_map.end());
bdd_setpair(rewrite, i_from->second, i_to->second);
}
for (i_from = from.prom_map.begin();
i_from != from.prom_map.end();
for (i_from = from.acc_map.begin();
i_from != from.acc_map.end();
++i_from)
{
i_to = dict_.prom_map.find(i_from->first);
assert(i_to != dict_.prom_map.end());
i_to = dict_.acc_map.find(i_from->first);
assert(i_to != dict_.acc_map.end());
bdd_setpair(rewrite, i_from->second, i_to->second);
}
return rewrite;

114
src/tgba/tgbaexplicit.cc
View file

@ -1,4 +1,5 @@
#include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh"
#include "ltlvisit/destroy.hh"
#include "tgbaexplicit.hh"
#include <cassert>
@ -10,8 +11,8 @@ namespace spot
// tgba_explicit_succ_iterator
tgba_explicit_succ_iterator::tgba_explicit_succ_iterator
(const tgba_explicit::state* s)
: s_(s)
(const tgba_explicit::state* s, bdd all_acc)
: s_(s), all_accepting_conditions_(all_acc)
{
}
@ -46,9 +47,9 @@ namespace spot
}
bdd
tgba_explicit_succ_iterator::current_promise()
tgba_explicit_succ_iterator::current_accepting_conditions()
{
return (*i_)->promise;
return (*i_)->accepting_conditions & all_accepting_conditions_;
}
@ -80,7 +81,9 @@ namespace spot
tgba_explicit::tgba_explicit()
: init_(0)
: init_(0), all_accepting_conditions_(bddfalse),
neg_accepting_conditions_(bddtrue),
all_accepting_conditions_computed_(false)
{
}
@ -124,12 +127,13 @@ namespace spot
transition* t = new transition;
t->dest = d;
t->condition = bddtrue;
t->promise = bddtrue;
t->accepting_conditions = bddfalse;
s->push_back(t);
return t;
}
int tgba_explicit::get_condition(ltl::formula* f)
bdd
tgba_explicit::get_condition(ltl::formula* f)
{
assert(dynamic_cast<ltl::atomic_prop*>(f));
tgba_bdd_dict::fv_map::iterator i = dict_.var_map.find(f);
@ -145,45 +149,72 @@ namespace spot
ltl::destroy(f);
v = i->second;
}
return v;
return ithvar(v);
}
void tgba_explicit::add_condition(transition* t, ltl::formula* f)
void
tgba_explicit::add_condition(transition* t, ltl::formula* f)
{
t->condition &= ithvar(get_condition(f));
t->condition &= get_condition(f);
}
void tgba_explicit::add_neg_condition(transition* t, ltl::formula* f)
void
tgba_explicit::add_neg_condition(transition* t, ltl::formula* f)
{
t->condition &= ! ithvar(get_condition(f));
t->condition &= ! get_condition(f);
}
int tgba_explicit::get_promise(ltl::formula* f)
void
tgba_explicit::declare_accepting_condition(ltl::formula* f)
{
tgba_bdd_dict::fv_map::iterator i = dict_.prom_map.find(f);
int v;
if (i == dict_.prom_map.end())
tgba_bdd_dict::fv_map::iterator i = dict_.acc_map.find(f);
if (i == dict_.acc_map.end())
{
int v;
v = create_node();
dict_.prom_map[f] = v;
dict_.prom_formula_map[v] = f;
dict_.acc_map[f] = v;
dict_.acc_formula_map[v] = f;
neg_accepting_conditions_ &= !ithvar(v);
}
else
}
bool
tgba_explicit::has_accepting_condition(ltl::formula* f) const
{
tgba_bdd_dict::fv_map::const_iterator i = dict_.acc_map.find(f);
return i != dict_.acc_map.end();
}
bdd
tgba_explicit::get_accepting_condition(ltl::formula* f)
{
ltl::constant* c = dynamic_cast<ltl::constant*>(f);
if (c)
{
ltl::destroy(f);
v = i->second;
switch (c->val())
{
case ltl::constant::True:
return bddtrue;
case ltl::constant::False:
return bddfalse;
}
/* Unreachable code. */
assert(0);
}
tgba_bdd_dict::fv_map::iterator i = dict_.acc_map.find(f);
assert (i != dict_.acc_map.end());
ltl::destroy(f);
bdd v = ithvar(i->second);
v &= bdd_exist(neg_accepting_conditions_, v);
return v;
}
void tgba_explicit::add_promise(transition* t, ltl::formula* f)
void
tgba_explicit::add_accepting_condition(transition* t, ltl::formula* f)
{
t->promise &= ithvar(get_promise(f));
}
void tgba_explicit::add_neg_promise(transition* t, ltl::formula* f)
{
t->promise &= ! ithvar(get_promise(f));
bdd c = get_accepting_condition(f);
t->accepting_conditions |= c;
}
state*
@ -197,7 +228,8 @@ namespace spot
{
const state_explicit* s = dynamic_cast<const state_explicit*>(state);
assert(s);
return new tgba_explicit_succ_iterator(s->get_state());
return new tgba_explicit_succ_iterator(s->get_state(),
all_accepting_conditions());
}
const tgba_bdd_dict&
@ -216,4 +248,28 @@ namespace spot
return i->second;
}
bdd
tgba_explicit::all_accepting_conditions() const
{
if (!all_accepting_conditions_computed_)
{
bdd all = bddfalse;
tgba_bdd_dict::fv_map::const_iterator i;
for (i = dict_.acc_map.begin(); i != dict_.acc_map.end(); ++i)
{
bdd v = ithvar(i->second);
all |= v & bdd_exist(neg_accepting_conditions_, v);
}
all_accepting_conditions_ = all;
all_accepting_conditions_computed_ = true;
}
return all_accepting_conditions_;
}
bdd
tgba_explicit::neg_accepting_conditions() const
{
return neg_accepting_conditions_;
}
}

22
src/tgba/tgbaexplicit.hh
View file

@ -24,7 +24,7 @@ namespace spot
struct transition
{
bdd condition;
bdd promise;
bdd accepting_conditions;
state* dest;
};
@ -33,8 +33,9 @@ namespace spot
void add_condition(transition* t, ltl::formula* f);
void add_neg_condition(transition* t, ltl::formula* f);
void add_promise(transition* t, ltl::formula* f);
void add_neg_promise(transition* t, ltl::formula* f);
void declare_accepting_condition(ltl::formula* f);
bool has_accepting_condition(ltl::formula* f) const;
void add_accepting_condition(transition* t, ltl::formula* f);
// tgba interface
virtual ~tgba_explicit();
@ -44,10 +45,13 @@ namespace spot
virtual const tgba_bdd_dict& get_dict() const;
virtual std::string format_state(const spot::state* state) const;
virtual bdd all_accepting_conditions() const;
virtual bdd neg_accepting_conditions() const;
protected:
state* add_state(const std::string& name);
int get_condition(ltl::formula* f);
int get_promise(ltl::formula* f);
bdd get_condition(ltl::formula* f);
bdd get_accepting_condition(ltl::formula* f);
typedef std::map<const std::string, tgba_explicit::state*> ns_map;
typedef std::map<const tgba_explicit::state*, std::string> sn_map;
@ -55,6 +59,9 @@ namespace spot
sn_map state_name_map_;
tgba_bdd_dict dict_;
tgba_explicit::state* init_;
mutable bdd all_accepting_conditions_;
bdd neg_accepting_conditions_;
mutable bool all_accepting_conditions_computed_;
};
@ -83,7 +90,7 @@ namespace spot
class tgba_explicit_succ_iterator : public tgba_succ_iterator
{
public:
tgba_explicit_succ_iterator(const tgba_explicit::state* s);
tgba_explicit_succ_iterator(const tgba_explicit::state* s, bdd all_acc);
virtual
~tgba_explicit_succ_iterator()
@ -96,11 +103,12 @@ namespace spot
virtual state_explicit* current_state();
virtual bdd current_condition();
virtual bdd current_promise();
virtual bdd current_accepting_conditions();
private:
const tgba_explicit::state* s_;
tgba_explicit::state::const_iterator i_;
bdd all_accepting_conditions_;
};
}

34
src/tgba/tgbaproduct.cc
View file

@ -43,8 +43,11 @@ namespace spot
// tgba_product_succ_iterator
tgba_product_succ_iterator::tgba_product_succ_iterator
(tgba_succ_iterator* left, tgba_succ_iterator* right)
: left_(left), right_(right)
(tgba_succ_iterator* left, tgba_succ_iterator* right,
bdd left_neg, bdd right_neg)
: left_(left), right_(right),
left_neg_(left_neg),
right_neg_(right_neg)
{
}
@ -131,9 +134,10 @@ namespace spot
return current_cond_;
}
bdd tgba_product_succ_iterator::current_promise()
bdd tgba_product_succ_iterator::current_accepting_conditions()
{
return left_->current_promise() & right_->current_promise();
return ((left_->current_accepting_conditions() & right_neg_)
| (right_->current_accepting_conditions() & left_neg_));
}
////////////////////////////////////////////////////////////
@ -165,6 +169,13 @@ namespace spot
right_ = new tgba_translate_proxy(right, dict_);
right_should_be_freed_ = true;
}
all_accepting_conditions_ = ((left_->all_accepting_conditions()
& right_->neg_accepting_conditions())
| (right_->all_accepting_conditions()
& left_->neg_accepting_conditions()));
neg_accepting_conditions_ = (left_->neg_accepting_conditions()
& right_->neg_accepting_conditions());
}
tgba_product::~tgba_product()
@ -190,7 +201,9 @@ namespace spot
tgba_succ_iterator* li = left_->succ_iter(s->left());
tgba_succ_iterator* ri = right_->succ_iter(s->right());
return new tgba_product_succ_iterator(li, ri);
return new tgba_product_succ_iterator(li, ri,
left_->neg_accepting_conditions(),
right_->neg_accepting_conditions());
}
const tgba_bdd_dict&
@ -209,5 +222,16 @@ namespace spot
+ right_->format_state(s->right()));
}
bdd
tgba_product::all_accepting_conditions() const
{
return all_accepting_conditions_;
}
bdd
tgba_product::neg_accepting_conditions() const
{
return neg_accepting_conditions_;
}
}

12
src/tgba/tgbaproduct.hh
View file

@ -57,7 +57,8 @@ namespace spot
{
public:
tgba_product_succ_iterator(tgba_succ_iterator* left,
tgba_succ_iterator* right);
tgba_succ_iterator* right,
bdd left_neg, bdd right_neg);
virtual ~tgba_product_succ_iterator();
@ -69,7 +70,7 @@ namespace spot
// inspection
state_bdd_product* current_state();
bdd current_condition();
bdd current_promise();
bdd current_accepting_conditions();
private:
//@{
@ -82,6 +83,8 @@ namespace spot
tgba_succ_iterator* left_;
tgba_succ_iterator* right_;
bdd current_cond_;
bdd left_neg_;
bdd right_neg_;
};
/// \brief A lazy product. (States are computed on the fly.)
@ -105,12 +108,17 @@ namespace spot
virtual std::string format_state(const state* state) const;
virtual bdd all_accepting_conditions() const;
virtual bdd neg_accepting_conditions() const;
private:
const tgba* left_;
bool left_should_be_freed_;
const tgba* right_;
bool right_should_be_freed_;
tgba_bdd_dict dict_;
bdd all_accepting_conditions_;
bdd neg_accepting_conditions_;
};
}

26
src/tgba/tgbatranslateproxy.cc
View file

@ -53,9 +53,9 @@ namespace spot
}
bdd
tgba_translate_proxy_succ_iterator::current_promise()
tgba_translate_proxy_succ_iterator::current_accepting_conditions()
{
return bdd_replace(iter_->current_promise(), rewrite_);
return bdd_replace(iter_->current_accepting_conditions(), rewrite_);
}
@ -89,13 +89,18 @@ namespace spot
bdd_setpair(rewrite_to_, i_from->second, i_to->second);
bdd_setpair(rewrite_from_, i_to->second, i_from->second);
}
for (i_from = f.prom_map.begin(); i_from != f.prom_map.end(); ++i_from)
for (i_from = f.acc_map.begin(); i_from != f.acc_map.end(); ++i_from)
{
i_to = to_.prom_map.find(i_from->first);
assert(i_to != to_.prom_map.end());
i_to = to_.acc_map.find(i_from->first);
assert(i_to != to_.acc_map.end());
bdd_setpair(rewrite_to_, i_from->second, i_to->second);
bdd_setpair(rewrite_from_, i_to->second, i_from->second);
}
all_accepting_conditions_ = bdd_replace(from.all_accepting_conditions(),
rewrite_to_);
neg_accepting_conditions_ = bdd_replace(from.neg_accepting_conditions(),
rewrite_to_);
}
tgba_translate_proxy::~tgba_translate_proxy()
@ -140,4 +145,15 @@ namespace spot
return res;
}
bdd
tgba_translate_proxy::all_accepting_conditions() const
{
return all_accepting_conditions_;
}
bdd tgba_translate_proxy::neg_accepting_conditions() const
{
return neg_accepting_conditions_;
}
}

8
src/tgba/tgbatranslateproxy.hh
View file

@ -22,7 +22,7 @@ namespace spot
// inspection
state* current_state();
bdd current_condition();
bdd current_promise();
bdd current_accepting_conditions();
protected:
tgba_succ_iterator* iter_;
bddPair* rewrite_;
@ -51,11 +51,17 @@ namespace spot
virtual std::string format_state(const state* state) const;
virtual bdd all_accepting_conditions() const;
virtual bdd neg_accepting_conditions() const;
private:
const tgba& from_; ///< The spot::tgba to masquerade.
tgba_bdd_dict to_; ///< The new dictionar to use.
bddPair* rewrite_to_; ///< The rewriting pair for from->to.
bddPair* rewrite_from_; ///< The rewriting pair for to->from.
bdd all_accepting_conditions_;
bdd neg_accepting_conditions_;
};
}

4
src/tgbaalgos/dotty.cc
View file

@ -42,8 +42,8 @@ namespace spot
bool recurse = dotty_state(os, g, s, m, node);
os << " " << father << " -> " << node << " [label=\"";
bdd_print_set(os, g.get_dict(), si->current_condition()) << "\\n";
bdd_print_set(os, g.get_dict(), si->current_promise()) << "\"]"
<< std::endl;
bdd_print_set(os, g.get_dict(), si->current_accepting_conditions())
<< "\"]" << std::endl;
if (recurse)
{
dotty_rec(os, g, s, m, node);

17
src/tgbaalgos/save.cc
View file

@ -2,6 +2,7 @@
#include "tgba/tgba.hh"
#include "save.hh"
#include "tgba/bddprint.hh"
#include "ltlvisit/tostring.hh"
namespace spot
{
@ -19,9 +20,9 @@ namespace spot
state* s = si->current_state();
os << "\"" << cur << "\", \"" << g.format_state(s) << "\", ";
bdd_print_sat(os, g.get_dict(), si->current_condition()) << ", ";
bdd_print_sat(os, g.get_dict(), si->current_promise()) << ";"
<< std::endl;
bdd_print_sat(os, g.get_dict(), si->current_condition()) << ",";
bdd_print_acc(os, g.get_dict(), si->current_accepting_conditions())
<< ";" << std::endl;
// Destination already explored?
seen_set::iterator i = m.find(s);
@ -41,6 +42,16 @@ namespace spot
std::ostream&
tgba_save_reachable(std::ostream& os, const tgba& g)
{
const tgba_bdd_dict& d = g.get_dict();
os << "acc =";
for (tgba_bdd_dict::fv_map::const_iterator ai = d.acc_map.begin();
ai != d.acc_map.end(); ++ai)
{
os << " \"";
ltl::to_string(ai->first, os) << "\"";
}
os << ";" << std::endl;
seen_set m;
state* state = g.get_init_state();
save_rec(os, g, state, m);

77
src/tgbaparse/tgbaparse.yy
View file

@ -12,10 +12,14 @@
{
int token;
std::string* str;
std::list<std::pair<bool, spot::ltl::formula*> >* list;
std::list<std::pair<bool, spot::ltl::formula*> >* listp;
std::list<spot::ltl::formula*>* list;
}
%{
#include "ltlast/constant.hh"
#include "ltlvisit/destroy.hh"
/* tgbaparse.hh and parsedecl.hh include each other recursively.
We mut ensure that YYSTYPE is declared (by the above %union)
before parsedecl.hh uses it. */
@ -33,15 +37,20 @@ typedef std::pair<bool, spot::ltl::formula*> pair;
%token <str> STRING
%token <str> IDENT
%type <str> strident
%type <list> prop_list
%type <listp> cond_list
%type <list> acc_list
%token ACC_DEF
%%
tgba: accepting_decl lines | lines;
accepting_decl: ACC_DEF acc_decl ';'
lines:
| lines line
;
line: strident ',' strident ',' prop_list ',' prop_list ';'
line: strident ',' strident ',' cond_list ',' acc_list ';'
{
spot::tgba_explicit::transition* t
= result->create_transition(*$1, *$3);
@ -51,11 +60,9 @@ line: strident ',' strident ',' prop_list ',' prop_list ';'
result->add_neg_condition(t, i->second);
else
result->add_condition(t, i->second);
for (i = $7->begin(); i != $7->end(); ++i)
if (i->first)
result->add_neg_promise(t, i->second);
else
result->add_promise(t, i->second);
std::list<formula*>::iterator i2;
for (i2 = $7->begin(); i2 != $7->end(); ++i2)
result->add_accepting_condition(t, *i2);
delete $1;
delete $3;
delete $5;
@ -65,27 +72,67 @@ line: strident ',' strident ',' prop_list ',' prop_list ';'
strident: STRING | IDENT;
prop_list:
cond_list:
{
$$ = new std::list<pair>;
}
| prop_list strident
| cond_list strident
{
if (*$2 != "")
$1->push_back(pair(false, parse_environment.require(*$2)));
{
$1->push_back(pair(false, parse_environment.require(*$2)));
}
delete $2;
$$ = $1;
}
| prop_list '!' strident
| cond_list '!' strident
{
if (*$3 != "")
$1->push_back(pair(true, parse_environment.require(*$3)));
{
$1->push_back(pair(true, parse_environment.require(*$3)));
}
delete $3;
$$ = $1;
}
;
;
acc_list:
{
$$ = new std::list<formula*>;
}
| acc_list strident
{
if (*$2 == "true")
{
$1->push_back(constant::true_instance());
}
else if (*$2 != "" && *$2 != "false")
{
formula* f = parse_environment.require(*$2);
if (! result->has_accepting_condition(f))
{
error_list.push_back(spot::tgba_parse_error(@2,
"undeclared accepting condition"));
destroy(f);
delete $2;
YYERROR;
}
$1->push_back(f);
}
delete $2;
$$ = $1;
}
;
acc_decl:
| acc_decl strident
{
formula* f = parse_environment.require(*$2);
result->declare_accepting_condition(f);
delete $2;
}
;
%%

2
src/tgbaparse/tgbascan.ll
View file

@ -35,6 +35,8 @@ eol \n|\r|\n\r|\r\n
return STRING;
}
acc[ \t]*= return ACC_DEF;
[a-zA-Z][a-zA-Z0-9_]* {
yylval->str = new std::string(yytext);
return IDENT;

9
src/tgbatest/explicit.cc
View file

@ -18,9 +18,12 @@ main()
a.add_condition(t2, e.require("a"));
a.add_condition(t3, e.require("b"));
a.add_condition(t3, e.require("c"));
a.add_promise(t1, e.require("p"));
a.add_promise(t1, e.require("q"));
a.add_promise(t2, e.require("r"));
a.declare_accepting_condition(e.require("p"));
a.declare_accepting_condition(e.require("q"));
a.declare_accepting_condition(e.require("r"));
a.add_accepting_condition(t1, e.require("p"));
a.add_accepting_condition(t1, e.require("q"));
a.add_accepting_condition(t2, e.require("r"));
spot::dotty_reachable(std::cout, a);
}

6
src/tgbatest/explicit.test
View file

@ -13,10 +13,10 @@ digraph G {
1 [label="state 0"]
0 -> 1
2 [label="state 1"]
1 -> 2 [label="T\n<Prom[p]:1, Prom[q]:1>"]
1 -> 2 [label="T\n<Acc[p]:0, Acc[q]:1, Acc[r]:0><Acc[p]:1, Acc[q]:0, Acc[r]:0>"]
3 [label="state 2"]
2 -> 3 [label="<a:1>\n<Prom[r]:1>"]
3 -> 1 [label="<b:1, c:1>\nT"]
2 -> 3 [label="<a:1>\n<Acc[p]:0, Acc[q]:0, Acc[r]:1>"]
3 -> 1 [label="<b:1, c:1>\nF"]
}
EOF

15
src/tgbatest/explprod.test
View file

@ -5,28 +5,31 @@
set -e
cat >input1 <<EOF
s1, s3, a,;
acc = p1;
s1, s3, a, true;
s1, s2, b, p1;
s2, s1, !a,;
s2, s3, c,;
s2, s1, !a, true;
s2, s3, c, true;
EOF
cat >input2 <<EOF
acc=p2 p3;
s1, s2, b, p2;
s2, s1, a, p3;
EOF
cat >expected <<EOF
"s1 * s1", "s3 * s2", a b, "p2";
acc = "p1" "p2" "p3";
"s1 * s1", "s3 * s2", a b, "p1" "p2";
"s1 * s1", "s2 * s2", b, "p1" "p2";
"s2 * s2", "s3 * s1", a c, "p3";
"s2 * s2", "s3 * s1", a c, "p1" "p3";
EOF
./explprod input1 input2 > stdout
# Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.)
sed 's/c a/a c/g;s/b a/a b/g;s/"p2" "p1"/"p1" "p2"/g' stdout > tmp_ &&
sed 's/c a/a c/g;s/b a/a b/g;s/"p3" "p1"/"p1" "p3"/g;s/"p3" "p2"/"p1" "p3"/g;s/"p2" "p1"/"p1" "p2"/g' stdout > tmp_ &&
mv tmp_ stdout
cat stdout

53
src/tgbatest/ltl2tgba.cc
View file

@ -13,10 +13,14 @@ syntax(char* prog)
{
std::cerr << "Usage: "<< prog << " [-d][-o][-r] formula" << std::endl
<< std::endl
<< " -a display the accepting_conditions BDD, not the reachability graph"
<< " -A same as -a, but as a set" << std::endl
<< " -d turn on traces during parsing" << std::endl
<< " -o re-order BDD variables in the automata" << std::endl
<< std::endl
<< " -r display the relation BDD, not the reachability graph"
<< std::endl;
<< std::endl
<< " -R same as -r, but as a set" << std::endl;
exit(2);
}
@ -27,7 +31,7 @@ main(int argc, char** argv)
bool debug_opt = false;
bool defrag_opt = false;
bool rel_opt = false;
int output = 0;
int formula_index = 0;
for (;;)
@ -37,7 +41,15 @@ main(int argc, char** argv)
++formula_index;
if (!strcmp(argv[formula_index], "-d"))
if (!strcmp(argv[formula_index], "-a"))
{
output = 2;
}
else if (!strcmp(argv[formula_index], "-A"))
{
output = 4;
}
else if (!strcmp(argv[formula_index], "-d"))
{
debug_opt = true;
}
@ -47,7 +59,11 @@ main(int argc, char** argv)
}
else if (!strcmp(argv[formula_index], "-r"))
{
rel_opt = true;
output = 1;
}
else if (!strcmp(argv[formula_index], "-R"))
{
output = 3;
}
else
{
@ -70,11 +86,30 @@ main(int argc, char** argv)
spot::ltl::destroy(f);
if (defrag_opt)
a = spot::defrag(a);
if (rel_opt)
spot::bdd_print_dot(std::cout, a.get_dict(),
a.get_core_data().relation);
else
spot::dotty_reachable(std::cout, a);
switch (output)
{
case 0:
spot::dotty_reachable(std::cout, a);
break;
case 1:
spot::bdd_print_dot(std::cout, a.get_dict(),
a.get_core_data().relation);
break;
case 2:
spot::bdd_print_dot(std::cout, a.get_dict(),
a.get_core_data().accepting_conditions);
break;
case 3:
spot::bdd_print_set(std::cout, a.get_dict(),
a.get_core_data().relation);
break;
case 4:
spot::bdd_print_set(std::cout, a.get_dict(),
a.get_core_data().accepting_conditions);
break;
default:
assert(!"unknown output option");
}
}
else
{

1
src/tgbatest/mixprod.test
View file

@ -8,6 +8,7 @@ set -e
# trigger assertions or I/O errors.
cat >input1 <<EOF
acc = p1;
s1, s3, a,;
s1, s2, b, p1;
s2, s1, !a,;

17
src/tgbatest/readsave.test
View file

@ -5,23 +5,34 @@
set -e
cat >input <<EOF
acc = c d;
s1, "s2", a!b, c d;
"s2", "state 3", a, !c;
"s2", "state 3", a, c;
"state 3", s1,,;
EOF
./readsave input > stdout
cat >expected <<EOF
acc = "c" "d";
"s1", "s2", a !b, "c" "d";
"s2", "state 3", a, !"c";
"state 3", "s1", , ;
"s2", "state 3", a, "c";
"state 3", "s1", ,;
EOF
# Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.)
sed 's/"d" "c"/"c" "d"/g' stdout > tmp_ && mv tmp_ stdout
diff stdout expected
mv stdout input
./readsave input > stdout
# Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.)
sed 's/"d" "c"/"c" "d"/g' stdout > tmp_ && mv tmp_ stdout
diff input stdout
rm input stdout expected

10
src/tgbatest/tgbaread.cc
View file

@ -33,9 +33,9 @@ main(int argc, char** argv)
spot::tgba_parse_error_list pel;
spot::tgba_explicit* a = spot::tgba_parse(argv[filename_index],
pel, env, debug);
exit_code =
spot::format_tgba_parse_errors(std::cerr, pel);
if (spot::format_tgba_parse_errors(std::cerr, pel))
return 2;
if (a)
{
@ -44,7 +44,7 @@ main(int argc, char** argv)
}
else
{
exit_code = 1;
return 1;
}
return exit_code;
return 0;
}

9
src/tgbatest/tgbaread.test
View file

@ -5,8 +5,9 @@
set -e
cat >input <<EOF
acc = c d;
s1, "s2", a!b, c d;
"s2", "state 3", a, !c;
"s2", "state 3", a, c;
"state 3", s1,,;
EOF
@ -19,10 +20,10 @@ digraph G {
1 [label="s1"]
0 -> 1
2 [label="s2"]
1 -> 2 [label="<a:1, b:0>\n<Prom[c]:1, Prom[d]:1>"]
1 -> 2 [label="<a:1, b:0>\n<Acc[c]:0, Acc[d]:1><Acc[c]:1, Acc[d]:0>"]
3 [label="state 3"]
2 -> 3 [label="<a:1>\n<Prom[c]:0>"]
3 -> 1 [label="T\nT"]
2 -> 3 [label="<a:1>\n<Acc[c]:1, Acc[d]:0>"]
3 -> 1 [label="T\nF"]
}
EOF

12
src/tgbatest/tripprod.test
View file

@ -5,18 +5,21 @@
set -e
cat >input1 <<EOF
s1, s3, a,;
acc = p1;
s1, s3, a, true;
s1, s2, b, p1;
s2, s1, !a,;
s2, s1, !a, true;
s2, s3, c,;
EOF
cat >input2 <<EOF
acc = p2 p3;
s1, s2, b, p2;
s2, s1, a, p3;
EOF
cat >input3 <<EOF
acc = p4;
s1, s2, a,;
s1, s3, b,;
s3, s2,, p4;
@ -24,10 +27,11 @@ s2, s3,, p4;
EOF
cat >expected <<EOF
"s1 * s1 * s1", "s3 * s2 * s2", a b, "p2";
acc = "p2" "p3" "p4" "p1";
"s1 * s1 * s1", "s3 * s2 * s2", a b, "p1" "p2";
"s1 * s1 * s1", "s2 * s2 * s2", a b, "p1" "p2";
"s2 * s2 * s2", "s3 * s1 * s3", a c, "p3" "p4";
"s1 * s1 * s1", "s3 * s2 * s3", a b, "p2";
"s1 * s1 * s1", "s3 * s2 * s3", a b, "p1" "p2";
"s1 * s1 * s1", "s2 * s2 * s3", b, "p1" "p2";
"s2 * s2 * s3", "s3 * s1 * s2", a c, "p3" "p4";
EOF