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

simulation: Fix co-simulation and iterated simulations of BA automata

Browse source 
* src/tgbaalgos/simulation.hh, src/tgbaalgos/simulation.cc
(simulation_sba, cosimulation_sba, iterated_simulations_sba): New
function.  Also speedup the existing functions by avoiding
add_acceptince_conditions() and add_conditions().  Finally, use
scc_filter_states() when dealing with degeneralized automata.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh (do_ba_simul):
New method.  Use it after degeneralization.
* src/tgba/tgbaexplicit.hh (get_transition, get_state): New methods.
* src/tgbatest/basimul.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add it.
* NEWS: Introduce the new function and summarize the bug.
This commit is contained in:
Alexandre Duret-Lutz 2013-05-12 17:49:20 +02:00
parent 372790a489
commit 0c7c933805
8 changed files with 303 additions and 110 deletions
Download patch file Download diff file Expand all files Collapse all files

17
NEWS
View file

@ -30,6 +30,15 @@ New in spot 1.1a (not yet released):
the automaton. scc_filter_state() should be used when
post-processing TGBAs that actually represent BAs.
- simulation_sba(), cosimulation_sba(), and
iterated_simulations_sba() are new functions that apply to TGBAs
that actually represent BAs. They preserve the imporant
property that if a state of the BA is is accepting, the outgoing
transitions of that state are all accepting in the TGBA that
represent the BA. This is something that was not preserved by
functions cosimultion() and iterated_simulations() as mentionned
in the bug fixes below.
- ltlcross has a new option --seed, that makes it possible to
change the seed used by the random graph generator.
@ -40,6 +49,14 @@ New in spot 1.1a (not yet released):
- ltlfilt --stutter-invariant would trigger an assert on PSL formulas.
- ltl2tgba, ltl2tgta, ltlcross, and ltlfilt, would all choke on empty
lines in a file of formulas. They now ignore empty lines.
- The iterated simulation applied on degeneralized TGBA was bogus
for two reasons: one was that cosimulation was applied using the
generic cosimulation for TGBA, and the second is that
SCC-filtering, performed between iterations, was also a
TGBA-based algorithm. Both of these algorithms could lose the
property that if a TGBA represents a BA, all the outgoing
transitions of a state should be accepting. As a consequence, some
formulas where translated to incorrect Büchi automata.
New in spot 1.1 (2013-04-28):

27
src/tgba/tgbaexplicit.hh
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita.
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
// et Développement de l'Epita.
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
@ -318,6 +318,15 @@ namespace spot
return const_cast<transition*>(&(*(si->get_iterator())));
}
transition*
get_transition(const tgba_succ_iterator* si)
{
const tgba_explicit_succ_iterator<State>* tmp
= down_cast<const tgba_explicit_succ_iterator<State>*>(si);
assert(tmp);
return get_transition(tmp);
}
void add_condition(transition* t, const ltl::formula* f)
{
t->condition &= formula_to_bdd(f, dict_, this);
@ -336,12 +345,24 @@ namespace spot
return dict_->is_registered_acceptance_variable(f, this);
}
//old tgba explicit labelled interface
//old tgba explicit labeled interface
bool has_state(const label_t& name)
{
return ls_.find(name) != ls_.end();
}
/// \brief Return the state associated to a given label.
///
/// This is similar to add_state(), except that it returns 0 if
/// the state does not exist.
const State* get_state(const label_t& name)
{
typename ls_map::const_iterator i = ls_.find(name);
if (i == ls_.end())
return 0;
return &i->second;
}
const label_t& get_label(const State* s) const
{
typename sl_map::const_iterator i = sl_.find(s);

19
src/tgbaalgos/postproc.cc
View file

@ -80,6 +80,23 @@ namespace spot
}
}
const tgba* postprocessor::do_ba_simul(const tgba* a, int opt)
{
switch (opt)
{
case 0:
return a;
case 1:
return simulation_sba(a);
case 2:
return cosimulation_sba(a);
case 3:
default:
return iterated_simulations_sba(a);
}
}
const tgba* postprocessor::do_degen(const tgba* a)
{
const tgba* d = degeneralize(a,
@ -90,7 +107,7 @@ namespace spot
if (ba_simul_ <= 0)
return d;
const tgba* s = do_simul(d, ba_simul_);
const tgba* s = do_ba_simul(d, ba_simul_);
if (s != d)
delete d;

1
src/tgbaalgos/postproc.hh
View file

@ -91,6 +91,7 @@ namespace spot
protected:
const tgba* do_simul(const tgba* input, int opt);
const tgba* do_ba_simul(const tgba* input, int opt);
const tgba* do_degen(const tgba* input);
output_type type_;

210
src/tgbaalgos/simulation.cc
View file

@ -212,7 +212,6 @@ namespace spot
return false;
}
int transitions;
int states;
};
@ -223,7 +222,7 @@ namespace spot
// automaton is similar to the old one, except that the acceptance
// condition on the transitions are complemented.
// There is a specialization below.
template <bool Cosimulation, bool ReverseComplement = false>
template <bool Cosimulation, bool Sba>
class acc_compl_automaton:
public tgba_reachable_iterator_depth_first
{
@ -243,16 +242,10 @@ namespace spot
const state*, int,
const tgba_succ_iterator* si)
{
bdd acc = ReverseComplement
? ac_.reverse_complement(si->current_acceptance_conditions())
: ac_.complement(si->current_acceptance_conditions());
const tgba_explicit_succ_iterator<state_explicit_number>* tmpit =
down_cast<const tgba_explicit_succ_iterator
<state_explicit_number>*>(si);
bdd acc = ac_.complement(si->current_acceptance_conditions());
typename tgba_explicit_number::transition* t =
ea_->get_transition(tmpit);
ea_->get_transition(si);
t->acceptance_conditions = acc;
}
@ -281,10 +274,10 @@ namespace spot
acc_compl ac_;
};
// The specialization for Cosimulation equals to true: We need to
// copy.
template <>
class acc_compl_automaton<true>:
// The specialization for Cosimulation equals to true: We copy the
// automaton and transpose it at the same time.
template <bool Sba>
class acc_compl_automaton<true, Sba>:
public tgba_reachable_iterator_depth_first
{
public:
@ -292,13 +285,16 @@ namespace spot
: tgba_reachable_iterator_depth_first(a),
size(0),
out_(new tgba_explicit_number(a->get_dict())),
ea_(a),
ac_(ea_->all_acceptance_conditions(),
ea_->neg_acceptance_conditions()),
ac_(a->all_acceptance_conditions(),
a->neg_acceptance_conditions()),
current_max(0)
{
init_ = ea_->get_init_state();
a->get_dict()->register_all_variables_of(a, out_);
out_->set_acceptance_conditions(a->all_acceptance_conditions());
const state* init_ = a->get_init_state();
out_->set_init_state(get_state(init_));
init_->destroy();
}
inline unsigned
@ -325,19 +321,32 @@ namespace spot
unsigned src = get_state(in_s);
unsigned dst = get_state(out_s);
// In the case of the cosimulation, we want to have all the
// ingoing transition, and to keep the rest of the code
// similar, we just create equivalent transition in the other
// direction. Since we do not have to run through the
// automaton to get the signature, this is correct.
std::swap(src, dst);
bdd acc = ac_.complement(si->current_acceptance_conditions());
// Note the order of src and dst: the transition is reversed.
tgba_explicit_number::transition* t
= out_->create_transition(src, dst);
= out_->create_transition(dst, src);
out_->add_acceptance_conditions(t, acc);
out_->add_conditions(t, si->current_condition());
t->condition = si->current_condition();
if (!Sba)
{
bdd acc = ac_.complement(si->current_acceptance_conditions());
t->acceptance_conditions = acc;
}
else
{
// If the acceptance is interpreted as state-based, to
// apply the reverse simulation on a SBA, we should pull
// the acceptance of the destination state on its incoming
// arcs (which now become outgoing args after
// transposition).
tgba_succ_iterator* it = out_->succ_iter(out_s);
it->first();
if (!it->done())
{
bdd acc = ac_.complement(it->current_acceptance_conditions());
t->acceptance_conditions = acc;
}
delete it;
}
}
void process_state(const state*, int, tgba_succ_iterator*)
@ -347,8 +356,6 @@ namespace spot
~acc_compl_automaton()
{
// Because we don't know what get_init_state returns...
init_->destroy();
}
public:
@ -359,16 +366,14 @@ namespace spot
map_state_state old_name_;
private:
const state* init_;
const tgba* ea_;
acc_compl ac_;
map_state_unsigned state2int;
unsigned current_max;
};
// The direct_simulation. If Cosimulation is true, we are doing a
// cosimulation. Seems obvious, but it's better to be clear.
template <bool Cosimulation>
// cosimulation.
template <bool Cosimulation, bool Sba>
class direct_simulation
{
protected:
@ -393,7 +398,7 @@ namespace spot
scc_map_->build_map();
old_a_ = a_;
acc_compl_automaton<Cosimulation> acc_compl(a_);
acc_compl_automaton<Cosimulation, Sba> acc_compl(a_);
// We'll start our work by replacing all the acceptance
// conditions by their complement.
@ -401,7 +406,7 @@ namespace spot
// Contains the relation between the names of the states in
// the automaton returned by the complementation and the one
// get in argument to the constructor of acc_compl.
// passed to the constructor of acc_compl.
std::swap(old_name_, acc_compl.old_name_);
a_ = acc_compl.out_;
@ -417,9 +422,10 @@ namespace spot
// class. We register one bdd by state, because in the worst
// case, |Class| == |State|.
unsigned set_num = a_->get_dict()
->register_anonymous_variables(size_a_ + 1, a_);
->register_anonymous_variables(size_a_ + 1, this);
all_proms_ = bdd_support(a_->all_acceptance_conditions());
all_acceptance_conditions_ = a_->all_acceptance_conditions();
all_proms_ = bdd_support(all_acceptance_conditions_);
bdd_initial = bdd_ithvar(set_num++);
bdd init = bdd_ithvar(set_num++);
@ -451,7 +457,6 @@ namespace spot
relation_[init] = init;
std::swap(order_, acc_compl.order_);
all_acceptance_conditions_ = a_->all_acceptance_conditions();
}
@ -460,16 +465,17 @@ namespace spot
// function simulation.
virtual ~direct_simulation()
{
a_->get_dict()->unregister_all_my_variables(this);
delete scc_map_;
if (!dont_delete_old_)
delete old_a_;
// Since a_ is a new automaton only if we are doing a
// cosimulation.
// a_ is a new automaton only if we are doing a cosimulation.
if (Cosimulation)
delete a_;
}
// We update the name of the classes.
// Update the name of the classes.
void update_previous_class()
{
std::list<bdd>::iterator it_bdd = used_var_.begin();
@ -535,10 +541,12 @@ namespace spot
{
const state* dst = sit->current_state();
bdd acc = bddtrue;
map_constraint::const_iterator it;
// We are using new_original_[old_name_[...]] because we
// give the constraints in the original automaton, so we
// need to use this heavy computation.
// We are using new_original_[old_name_[...]] because
// we have the constraints in the original automaton
// which has been duplicated twice to get the current
// automaton.
if (map_cst_
&& ((it = map_cst_
->find(std::make_pair(new_original_[old_name_[src]],
@ -563,7 +571,7 @@ namespace spot
}
// When we Cosimulate, we add a special flag to differentiate
// initial state.
// the initial state from the other.
if (Cosimulation && initial_state == src)
res |= bdd_initial;
@ -728,10 +736,10 @@ namespace spot
acc_compl reverser(all_acceptance_conditions_,
a_->neg_acceptance_conditions());
tgba_explicit_number* res
= new tgba_explicit_number(a_->get_dict());
res->set_acceptance_conditions
(all_acceptance_conditions_);
bdd_dict* d = a_->get_dict();
tgba_explicit_number* res = new tgba_explicit_number(d);
d->register_all_variables_of(a_, res);
res->set_acceptance_conditions(all_acceptance_conditions_);
bdd sup_all_acc = bdd_support(all_acceptance_conditions_);
// Non atomic propositions variables (= acc and class)
@ -746,11 +754,16 @@ namespace spot
// The difference between the two next lines is:
// the first says "if you see A", the second "if you
// see A and all the class implied by it".
// see A and all the classes implied by it".
bdd2state[part] = current_max;
bdd2state[relation_[part]] = current_max;
}
// Acceptance of states. Only used if Sba && Cosimulation.
std::vector<bdd> accst;
if (Sba && Cosimulation)
accst.resize(current_max + 1, bddfalse);
stat.states = bdd_lstate_.size();
stat.transitions = 0;
@ -788,7 +801,7 @@ namespace spot
bddtrue);
all_atomic_prop -= one;
// For each possible valuation, iterator over all possible
// For each possible valuation, iterate over all possible
// destination classes. We use minato_isop here, because
// if the same valuation of atomic properties can go
// to two different classes C1 and C2, iterating on
@ -820,8 +833,8 @@ namespace spot
sup_all_atomic_prop);
// Because we have complemented all the acceptance
// condition on the input automaton, we must re
// invert them to create a new transition.
// conditions on the input automaton, we must
// revert them to create a new transition.
acc = reverser.reverse_complement(acc);
// Take the id of the source and destination. To
@ -843,8 +856,11 @@ namespace spot
// acceptance condition.
tgba_explicit_number::transition* t
= res->create_transition(src, dst);
res->add_conditions(t, cond);
res->add_acceptance_conditions(t, acc);
t->condition = cond;
if (Sba && Cosimulation)
accst[dst] = acc;
else
t->acceptance_conditions = acc;
}
}
}
@ -854,6 +870,23 @@ namespace spot
res->merge_transitions();
// Mark all accepting state in a second pass, when
// dealing with SBA in cosimulation.
if (Sba && Cosimulation)
for (unsigned snum = current_max; snum > 0; --snum)
{
const state* s = res->get_state(snum);
tgba_succ_iterator* it = res->succ_iter(s);
bdd acc = accst[snum];
for (it->first(); !it->done(); it->next())
{
tgba_explicit_number::transition* t =
res->get_transition(it);
t->acceptance_conditions = acc;
}
delete it;
}
res_is_deterministic = nb_minato == nb_satoneset;
return res;
@ -968,7 +1001,7 @@ namespace spot
};
// For now, we don't try to handle cosimulation.
class direct_simulation_dont_care: public direct_simulation<false>
class direct_simulation_dont_care: public direct_simulation<false, false>
{
typedef std::vector<std::list<constraint> > constraints;
typedef std::map<bdd, // Source Class.
@ -981,11 +1014,11 @@ namespace spot
public:
direct_simulation_dont_care(const tgba* t)
: direct_simulation<false>(t)
: direct_simulation(t)
{
// This variable is used in the new signature.
on_cycle_ =
bdd_ithvar(a_->get_dict()->register_anonymous_variables(1, a_));
bdd_ithvar(a_->get_dict()->register_anonymous_variables(1, this));
// This one is used for the iteration on all the
// possibilities. Avoid computing two times "no constraints".
@ -1000,7 +1033,6 @@ namespace spot
& all_class_var_ & on_cycle_);
}
// This function computes the don't care signature of the state
// src. This signature is similar to the classic one, excepts
// that if the transition is on a SCC, we add a on_cycle_ on it,
@ -1481,7 +1513,7 @@ namespace spot
else if (cstr.empty())
empty_seen_ = true;
direct_simulation<false> dir_sim(original_, &cstr);
direct_simulation<false, false> dir_sim(original_, &cstr);
tgba* tmp = dir_sim.run();
automaton_size cur_size = dir_sim.get_stat();
if (*min == 0 || min_size_ > cur_size)
@ -1529,21 +1561,35 @@ namespace spot
tgba*
simulation(const tgba* t)
{
direct_simulation<false> simul(t);
direct_simulation<false, false> simul(t);
return simul.run();
}
tgba*
simulation_sba(const tgba* t)
{
direct_simulation<false, true> simul(t);
return simul.run();
}
tgba*
cosimulation(const tgba* t)
{
direct_simulation<true> simul(t);
direct_simulation<true, false> simul(t);
return simul.run();
}
tgba*
iterated_simulations(const tgba* t)
cosimulation_sba(const tgba* t)
{
direct_simulation<true, true> simul(t);
return simul.run();
}
template<bool Sba>
tgba*
iterated_simulations_(const tgba* t)
{
tgba* res = const_cast<tgba*> (t);
automaton_size prev;
@ -1552,8 +1598,7 @@ namespace spot
do
{
prev = next;
direct_simulation<false> simul(res);
direct_simulation<false, Sba> simul(res);
tgba* maybe_res = simul.run();
if (res != t)
@ -1566,24 +1611,34 @@ namespace spot
}
unique_ptr<tgba> after_simulation(maybe_res);
direct_simulation<true> cosimul(after_simulation);
direct_simulation<true, Sba> cosimul(after_simulation);
unique_ptr<tgba> after_cosimulation(cosimul.run());
next = cosimul.get_stat();
if (Sba)
res = scc_filter_states(after_cosimulation);
else
res = scc_filter(after_cosimulation, false);
}
while (prev != next);
return res;
}
tgba*
iterated_simulations(const tgba* t)
{
return iterated_simulations_<false>(t);
}
tgba*
iterated_simulations_sba(const tgba* t)
{
return iterated_simulations_<true>(t);
}
tgba*
dont_care_simulation(const tgba* t, int limit)
{
direct_simulation<false> sim(t);
direct_simulation<false, false> sim(t);
tgba* tmp = sim.run();
direct_simulation_dont_care s(tmp);
@ -1613,12 +1668,9 @@ namespace spot
if (res != t)
delete res;
direct_simulation<true> cosimul(after_simulation);
direct_simulation<true, false> cosimul(after_simulation);
unique_ptr<tgba> after_cosimulation(cosimul.run());
next = cosimul.get_stat();
res = scc_filter(after_cosimulation, true);
}
while (prev != next);

12
src/tgbaalgos/simulation.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -20,7 +20,6 @@
#ifndef SPOT_TGBAALGOS_SIMULATION_HH
# define SPOT_TGBAALGOS_SIMULATION_HH
namespace spot
{
class tgba;
@ -28,6 +27,7 @@ namespace spot
/// \addtogroup tgba_reduction
/// @{
/// @{
/// \brief Attempt to reduce the automaton by direct simulation.
///
/// When the suffixes (letter and acceptance conditions) reachable
@ -68,7 +68,10 @@ namespace spot
/// \return a new automaton which is at worst a copy of the received
/// one
tgba* simulation(const tgba* automaton);
tgba* simulation_sba(const tgba* automaton);
/// @}
/// @{
/// \brief Attempt to reduce the automaton by reverse simulation.
///
/// When the prefixes (letter and acceptance conditions) leading to
@ -116,7 +119,10 @@ namespace spot
/// \return a new automaton which is at worst a copy of the received
/// one
tgba* cosimulation(const tgba* automaton);
tgba* cosimulation_sba(const tgba* automaton);
/// @}
/// @{
/// \brief Iterate simulation() and cosimulation().
///
/// Runs simulation(), cosimulation(), and scc_filter() in a loop,
@ -132,6 +138,8 @@ namespace spot
/// \return a new automaton which is at worst a copy of the received
/// one
tgba* iterated_simulations(const tgba* automaton);
tgba* iterated_simulations_sba(const tgba* automaton);
/// @}
tgba* dont_care_simulation(const tgba* t, int limit = -1);

1
src/tgbatest/Makefile.am
View file

@ -110,6 +110,7 @@ TESTS = \
dfs.test \
emptchkr.test \
ltlcounter.test \
basimul.test \
spotlbtt.test \
ltlcross.test \
spotlbtt2.test \

76
src/tgbatest/basimul.test Executable file
View file

@ -0,0 +1,76 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program. If not, see <http://www.gnu.org/licenses/>.
. ./defs
set -e
ltl2tgba=../../bin/ltl2tgba
# This bug was found while working on the state-based acceptance
# output for the LBTT format. Using ba-simul=2 causes reverse
# simulation to be applied to the BA automaton obtained after
# degeneralization. Unfortunately in Spot 1.1, reverse simulation is
# only implemented on TGBA, and when applied to a TGBA that is a BA,
# it may merge one state that is accepting with one state that is not
# accepting, just because they have the same incoming transitions.
# (Applying direct simulation on a TGBA that is a BA is not a problem,
# since an accepting state will never have the same outgoing
# transitions as a BA.)
# In previous tests, we did not notice the bug because the --lbtt
# output was always using transition-based acceptance (the equivalent
# of --lbtt=t today), so the result of the reverse-simulation on the
# BA was output as a TGBA with a single acceptance set, and some state
# had both accepting and non-accepting transitions because of the
# merge. Unfortunately, this is not a Büchi automaton. Using the
# --spin output, or the new (state-based) --lbtt output highlights the
# bug.
# In the cases below, the following configurations used to fail
# cross-comparison with the other "sane" configurations, at least
# with the first formula. (The other three formulas were added because
# they also triggered related issues while debugging the first one.)
# --lbtt -x ba-simul=2
# --lbtt -x ba-simul=3
# --spin -x ba-simul=2
# --spin -x ba-simul=3
for seed in 1 2 3; do
../../bin/ltlcross --seed=$seed --density=0.$seed \
-f 'X((F(Xa | b) W c) U (Xc W (a & d)))' \
-f '((<> p5 V ((p0 U p1) <-> (p5 \/ p1))) -> ((<> p4 V p2) M p2))' \
-f '!p2 & (Fp5 R (((p0 U p1) & (p5 | p1)) | (!p5 & (!p0 R !p1))))' \
-f '! ((p0 /\ p4) <-> ! ((! p0 U (p0 W p4)) /\ (X p5 -> ([] p3 /\ p5))))' \
"$ltl2tgba --ba --high --lbtt=t -x ba-simul=0 %f >%T" \
"$ltl2tgba --ba --high --lbtt=t -x ba-simul=1 %f >%T" \
"$ltl2tgba --ba --high --lbtt=t -x ba-simul=2 %f >%T" \
"$ltl2tgba --ba --high --lbtt=t -x ba-simul=3 %f >%T" \
"$ltl2tgba --ba --high --lbtt -x ba-simul=0 %f >%T" \
"$ltl2tgba --ba --high --lbtt -x ba-simul=1 %f >%T" \
"$ltl2tgba --ba --high --lbtt -x ba-simul=2 %f >%T" \
"$ltl2tgba --ba --high --lbtt -x ba-simul=3 %f >%T" \
"$ltl2tgba --ba --high --spin -x ba-simul=0 %f >%N" \
"$ltl2tgba --ba --high --spin -x ba-simul=1 %f >%N" \
"$ltl2tgba --ba --high --spin -x ba-simul=2 %f >%N" \
"$ltl2tgba --ba --high --spin -x ba-simul=3 %f >%N"
done