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

Remove the old broken game-theory-based simulation reductions.

Browse source 
This implementation of direct simulation was only working on
degeneralized automata, and produce automata that are inferiors to
those output by the new direct simulation implementation (in
tgba/simulation.hh) which can also work on TGBA.  The delayed
simulation has never been reliable.  It's time for some spring
cleaning.

* src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc: Delete.
* src/tgba/Makefile.am: Adjust.
* src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh:
Remove all code, and keep only a deprecated replacement
from reduc_tgba_sim().
* src/tgbaalgos/reductgba_sim_del.cc: Delete.
* src/tgbaalgos/Makefile.am: Adjust.
* src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc,
src/tgbatest/reductgba.test: Delete.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc: Undocument options -R1s, -R1t,
-R2s, -R2t, and implement them using the new direct simulation.
Remove options -Rd and -RD.
* src/tgbatest/spotlbtt.test: Remove entry using these old options.
* wrap/python/spot.i: Do not process tgbaalgos/reductgba_sim.cc.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-27 17:11:53 +02:00
parent 7ba4ab7931
commit 7e5875845a
14 changed files with 69 additions and 2713 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tgba/Makefile.am
View file

@ -48,7 +48,6 @@ tgba_HEADERS = \
tgbakvcomplement.hh \
tgbascc.hh \
tgbaproduct.hh \
tgbareduc.hh \
tgbasgba.hh \
tgbasafracomplement.hh \
tgbatba.hh \
@ -72,7 +71,6 @@ libtgba_la_SOURCES = \
tgbaexplicit.cc \
tgbakvcomplement.cc \
tgbaproduct.cc \
tgbareduc.cc \
tgbasafracomplement.cc \
tgbascc.cc \
tgbasgba.cc \

443
src/tgba/tgbareduc.cc
View file

@ -1,443 +0,0 @@
// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "tgbareduc.hh"
#include <sstream>
namespace spot
{
namespace
{
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
}
tgba_reduc::tgba_reduc(const tgba* a)
: tgba_explicit_string(a->get_dict()),
tgba_reachable_iterator_breadth_first(a)
{
dict_->register_all_variables_of(a, this);
run();
all_acceptance_conditions_ = a->all_acceptance_conditions();
all_acceptance_conditions_computed_ = true;
}
tgba_reduc::~tgba_reduc()
{
sp_map::iterator i;
for (i = state_predecessor_map_.begin();
i!= state_predecessor_map_.end(); ++i)
{
delete i->second;
}
}
void
tgba_reduc::quotient_state(direct_simulation_relation* rel)
{
// Remember that for each state couple
// (*i)->second simulate (*i)->first.
for (direct_simulation_relation::iterator i = rel->begin();
i != rel->end(); ++i)
{
// All state simulate himself.
if (((*i)->first)->compare((*i)->second) == 0)
continue;
// We check if the two state are co-simulate.
bool recip = false;
for (direct_simulation_relation::iterator j = i;
j != rel->end(); ++j)
if ((((*i)->first)->compare((*j)->second) == 0) &&
(((*j)->first)->compare((*i)->second) == 0))
recip = true;
if (recip)
//this->redirect_transition((*i)->first, (*i)->second);
this->merge_state((*i)->first, (*i)->second);
}
this->merge_transitions();
}
void
tgba_reduc::quotient_state(delayed_simulation_relation* rel)
{
if (nb_set_acc_cond() > 1)
return;
//this->quotient_state(rel);
for (delayed_simulation_relation::iterator i = rel->begin();
i != rel->end(); ++i)
{
// All state simulate himself.
if (((*i)->first)->compare((*i)->second) == 0)
continue;
// We check if the two state are co-simulate.
bool recip = false;
for (delayed_simulation_relation::iterator j = i;
j != rel->end(); ++j)
if ((((*i)->first)->compare((*j)->second) == 0) &&
(((*j)->first)->compare((*i)->second) == 0))
recip = true;
if (recip)
this->merge_state((*i)->first, (*i)->second);
}
this->merge_transitions();
}
void
tgba_reduc::delete_transitions(simulation_relation* rel)
{
for (simulation_relation::iterator i = rel->begin();
i != rel->end(); ++i)
{
if (((*i)->first)->compare((*i)->second) == 0)
continue;
this->redirect_transition((*i)->first, (*i)->second);
}
this->merge_transitions();
}
////////////////////////////////////////////
// for build tgba_reduc
void
tgba_reduc::process_state(const spot::state* s, int, tgba_succ_iterator* si)
{
spot::state* init = aut_->get_init_state();
if (init->compare(s) == 0)
this->set_init_state(aut_->format_state(s));
init->destroy();
transition* t;
for (si->first(); !si->done(); si->next())
{
init = si->current_state();
t = this->create_transition(s, init);
this->add_conditions(t, si->current_condition());
this->add_acceptance_conditions(t, si->current_acceptance_conditions());
init->destroy();
}
}
tgba_explicit_string::transition*
tgba_reduc::create_transition(const spot::state* source,
const spot::state* dest)
{
const std::string ss = aut_->format_state(source);
const std::string sd = aut_->format_state(dest);
state_explicit_string* s = tgba_explicit_string::add_state(ss);
state_explicit_string* d = tgba_explicit_string::add_state(sd);
transition t;
t.dest = d;
sp_map::iterator i = state_predecessor_map_.find(d);
if (i == state_predecessor_map_.end())
{
std::list<state*>* pred = new std::list<state*>;
pred->push_back(s);
state_predecessor_map_[d] = pred;
}
else
{
(i->second)->push_back(s);
}
t.condition = bddtrue;
t.acceptance_conditions = bddfalse;
state_explicit_string::transitions_t::iterator is
= s->successors.insert(s->successors.end(), t);
return &*is;
}
///////////////////////////////////////////////////
void
tgba_reduc::redirect_transition(const spot::state* s,
const spot::state* simul)
{
bool belong = false;
bdd cond_simul;
bdd acc_simul;
std::list<state*> ltmp;
const state_explicit_string* s1 =
&(ls_[tgba_explicit_string::format_state(s)]);
const state_explicit_string* s2 =
&(ls_[tgba_explicit_string::format_state(simul)]);
sp_map::iterator i = state_predecessor_map_.find(s1);
if (i == state_predecessor_map_.end()) // 0 predecessor
return;
// for all predecessor of s.
for (std::list<state*>::iterator p = (i->second)->begin();
p != (i->second)->end(); ++p)
{
// We check if simul belong to the successor of p,
// as s belong too.
for (state_explicit_string::transitions_t::iterator
j = (*p)->successors.begin();
j != (*p)->successors.end(); ++j)
if (j->dest == s2) // simul belong to the successor of p.
{
belong = true;
cond_simul = j->condition;
acc_simul = j->acceptance_conditions;
break;
}
// If not, we check for another predecessor of s.
if (!belong)
continue;
// for all successor of p, a predecessor of s and simul.
for (state_explicit_string::transitions_t::iterator
j = (*p)->successors.begin();
j != (*p)->successors.end(); ++j)
{
// if the transition lead to s.
if ((j->dest == s1) &&
// if the label of the transition whose lead to s implies
// this leading to simul.
(((!j->condition | cond_simul) == bddtrue) &&
((!j->acceptance_conditions) | acc_simul) == bddtrue))
{
// We can redirect transition leading to s on simul.
j->dest = const_cast<state_explicit_string*>(s2);
// We memorize that we have to remove p
// of the predecessor of s.
ltmp.push_back(*p);
}
}
belong = false;
}
// We remove all the predecessor of s than we have memorized.
std::list<state*>::iterator k;
for (k = ltmp.begin();
k != ltmp.end(); ++k)
this->remove_predecessor_state(i->first, *k);
}
void
tgba_reduc::remove_predecessor_state(const state* s, const state* p)
{
sp_map::iterator i = state_predecessor_map_.find(s);
if (i == state_predecessor_map_.end()) // 0 predecessor
return;
// for all predecessor of s we remove p.
for (std::list<state*>::iterator j = (i->second)->begin();
j != (i->second)->end();)
if (p == *j)
j = (i->second)->erase(j);
else
++j;
}
void
tgba_reduc::remove_state(const spot::state* s)
{
// We suppose that the state is not reachable when called by
// merge_state => NO PREDECESSOR. But it can be have some
// predecessor in state_predecessor_map_.
ls_map::iterator k =
ls_.find(tgba_explicit_string::format_state(s));
if (k == ls_.end()) // 0 predecessor
return;
state_explicit_string* st =
&(ls_[tgba_explicit_string::format_state(s)]);
// for all successor q of s, we remove s of the predecessor of q.
// Note that the initial node can't be removed.
for (state_explicit_string::transitions_t::iterator j =
st->successors.begin(); j != st->successors.end(); ++j)
this->remove_predecessor_state(down_cast<const state_explicit_string*>
(j->dest), st);
sp_map::iterator i = state_predecessor_map_.find(st);
if (i == state_predecessor_map_.end()) // 0 predecessor
return;
// for all predecessor of s (none when called by merge_state)
for (std::list<state*>::iterator p = (i->second)->begin();
p != (i->second)->end(); ++p)
{
// for all transition of p, a predecessor of s.
for (state_explicit_string::transitions_t::iterator
j = (*p)->successors.begin();
j != (*p)->successors.end();)
{
if (j->dest == st)
{
// Remove the transition
j = (*p)->successors.erase(j);
++j;
}
else
++j;
}
}
// DESTROY THE STATE !? USELESS
// it will be destroyed when the automaton is deleted
// name_state_map_::iterator = name_state_map_[st];
// const tgba_explicit::state* st = name_state_map_[this->format_state(s)];
}
void
tgba_reduc::merge_state(const spot::state* sim1, const spot::state* sim2)
{
const state_explicit_string* s1 =
&(ls_[tgba_explicit_string::format_state(sim1)]);
const state_explicit_string* s2 =
&(ls_[tgba_explicit_string::format_state(sim2)]);
const state_explicit_string* stmp = s1;
const spot::state* simtmp = sim1;
// if sim1 is the init state, we remove sim2.
spot::state* init = this->get_init_state();
if (sim1->compare(init) == 0)
{
s1 = s2;
s2 = stmp;
sim1 = sim2;
sim2 = simtmp;
}
init->destroy();
sp_map::iterator i = state_predecessor_map_.find(s1);
if (i == state_predecessor_map_.end()) // 0 predecessor
{
// We can remove s1 safely, without changing the language
// of the automaton.
this->remove_state(sim1);
return;
}
// for all predecessor of s1, not the initial state,
// we redirect to s2 the transitions that lead to s1.
for (std::list<state*>::iterator p = (i->second)->begin();
p != (i->second)->end(); ++p)
{
// for all successor of p, a predecessor of s1.
for (state_explicit_string::transitions_t::iterator
j = (*p)->successors.begin();
j != (*p)->successors.end(); ++j)
{
// if the successor was s1...
if (j->dest == s1)
{
// ... make it s2.
j->dest = const_cast<state_explicit_string*>(s2);
}
}
}
// FIXME: The following justification sounds really dubious.
//
// We have to stock on s2 the acceptance condition of the arc
// leaving s1 (possible when the simulation is delayed). Since s2
// simulates s1, s2 has some labels that imply these of s1, so we
// can put the acceptance conditions on its arcs.
for (state_explicit_string::transitions_t::const_iterator
j = s1->successors.begin();
j != s1->successors.end(); ++j)
{
transition t;
t.dest = j->dest;
t.condition = j->condition;
t.acceptance_conditions = j->acceptance_conditions;
const_cast<state_explicit_string*>(s2)->successors.push_back(t);
}
// We remove all the predecessor of s1.
(i->second)->clear();
// then we can remove s1 safely, without changing the language
// of the automaton.
this->remove_state(sim1);
}
void
tgba_reduc::merge_state_delayed(const spot::state*,
const spot::state*)
{
// TO DO
}
int
tgba_reduc::nb_set_acc_cond() const
{
bdd acc, all;
acc = all = this->all_acceptance_conditions();
int count = 0;
while (all != bddfalse)
{
all -= bdd_satone(all);
++count;
}
return count;
}
//////// JUST FOR DEBUG //////////
void
tgba_reduc::display_rel_sim(simulation_relation* rel,
std::ostream& os)
{
int n = 0;
simulation_relation::iterator i;
for (i = rel->begin(); i != rel->end(); ++i)
{
if (((*i)->first)->compare((*i)->second) == 0)
continue;
++n;
os << "couple " << n
<< std::endl
<< " " << " [label=\""
<< this->format_state((*i)->first) << "\"]"
<< std::endl
<< " " << " [label=\""
<< this->format_state((*i)->second) << "\"]"
<< std::endl
<< std::endl;
}
}
}

167
src/tgba/tgbareduc.hh
View file

@ -1,167 +0,0 @@
// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_TGBA_TGBAREDUC_HH
# define SPOT_TGBA_TGBAREDUC_HH
#include "tgbaexplicit.hh"
#include "tgbaalgos/reachiter.hh"
#include <list>
#include <vector>
namespace spot
{
typedef std::pair<const spot::state*, const spot::state*> state_couple;
typedef std::vector<state_couple*> simulation_relation;
/*
typedef std::vector<state_couple*> direct_simulation_relation;
typedef std::vector<state_couple*> delayed_simulation_relation;
*/
class direct_simulation_relation: public simulation_relation
{
};
class delayed_simulation_relation: public simulation_relation
{
};
/// Explicit automata used in reductions.
/// \ingroup tgba_representation
class tgba_reduc:
public tgba_explicit_string, public tgba_reachable_iterator_breadth_first
{
public:
tgba_reduc(const tgba* a);
~tgba_reduc();
/// Reduce the automata using a relation simulation
/// Do not call this method with a delayed simulation relation.
void quotient_state(direct_simulation_relation* rel);
/// Build the quotient automata. Call this method
/// when use to a delayed simulation relation.
void quotient_state(delayed_simulation_relation* rel);
/// \brief Delete some transitions with help of a simulation
/// relation.
void delete_transitions(simulation_relation* rel);
// For Debug
void display_rel_sim(simulation_relation* rel, std::ostream& os);
void display_scc(std::ostream& os);
protected:
typedef Sgi::hash_map<const state_explicit_string*,
std::list<state*>*,
ptr_hash<state_explicit_string> > sp_map;
sp_map state_predecessor_map_;
// Interface of tgba_reachable_iterator_breadth_first
void process_state(const spot::state* s, int n, tgba_succ_iterator* si);
/// Create a transition using two state of a TGBA.
transition* create_transition(const spot::state* source,
const spot::state* dest);
/// Remove all the transition from the state q, predecessor
/// of both \a s and \a simul, which can be removed.
void redirect_transition(const spot::state* s,
const spot::state* simul);
/// Remove p of the predecessor of s.
void remove_predecessor_state(const state* s, const state* p);
/// Remove all the transition leading to s.
/// s is then unreachable and can be consider as remove.
void remove_state(const spot::state* s);
/// Redirect all transition leading to s1 to s2.
/// Note that we can do the reverse because
/// s1 and s2 belong to a co-simulate relation.
void merge_state(const spot::state* s1,
const spot::state* s2);
/// Redirect all transition leading to s1 to s2.
/// Note that we can do the reverse because
/// s1 and s2 belong to a co-simulate relation.
void merge_state_delayed(const spot::state* s1,
const spot::state* s2);
/// Remove all the scc which are terminal and doesn't
/// contains all the acceptance conditions.
void delete_scc();
/// Return true if the scc which contains \a s
/// is an fixed-formula alpha-ball.
/// this is explain in
/// \verbatim
/// @InProceedings{ etessami.00.concur,
/// author = {Kousha Etessami and Gerard J. Holzmann},
/// title = {Optimizing {B\"u}chi Automata},
/// booktitle = {Proceedings of the 11th International Conference on
/// Concurrency Theory (Concur'2000)},
/// pages = {153--167},
/// year = {2000},
/// editor = {C. Palamidessi},
/// volume = {1877},
/// series = {Lecture Notes in Computer Science},
/// publisher = {Springer-Verlag}
/// }
/// \endverbatim
// bool is_alpha_ball(const spot::state* s,
// bdd label = bddfalse,
// int n = -1);
// Return true if we can't reach a state with
// an other value of scc.
bool is_terminal(const spot::state* s,
int n = -1);
// Return false if the scc contains all the acceptance conditions.
bool is_not_accepting(const spot::state* s,
int n = -1);
/// If a scc maximal do not contains all the acceptance conditions
/// we can remove all the acceptance conditions in this scc.
void remove_acc(const spot::state* s);
/// Remove all the state which belong to the same scc that s.
void remove_scc(spot::state* s);
/// Same as remove_scc but more efficient.
// void remove_scc_depth_first(spot::state* s, int n = -1);
/// For compute_scc.
void remove_component(const spot::state* from);
int nb_set_acc_cond() const;
};
}
#endif // SPOT_TGBA_TGBAREDUC_HH

10
src/tgbaalgos/Makefile.am
View file

@ -1,8 +1,9 @@
## Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
## -*- coding: utf-8 -*-
## Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
## et Développement de l'Epita (LRDE).
## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
## Université Pierre et Marie Curie.
## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
## Université Pierre et Marie Curie.
##
## This file is part of Spot, a model checking library.
##
@ -99,7 +100,6 @@ libtgbaalgos_la_SOURCES = \
tau03.cc \
tau03opt.cc \
reductgba_sim.cc \
reductgba_sim_del.cc \
weight.cc
libtgbaalgos_la_LIBADD = gtec/libgtec.la

664
src/tgbaalgos/reductgba_sim.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -22,633 +22,12 @@
// 02111-1307, USA.
#include "reductgba_sim.hh"
#include "tgba/bddprint.hh"
#include "sccfilter.hh"
#include "simulation.hh"
#include "dupexp.hh"
namespace spot
{
///////////////////////////////////////////////////////////////////////
// spoiler_node
spoiler_node::spoiler_node(const state* d_node,
const state* s_node,
int num)
{
num_ = num;
sc_ = new state_couple(d_node, s_node);
lnode_succ = new sn_v;
lnode_pred = new sn_v;
not_win = false;
}
spoiler_node::~spoiler_node()
{
lnode_succ->clear();
lnode_pred->clear();
delete lnode_succ;
delete lnode_pred;
delete sc_;
}
bool
spoiler_node::add_succ(spoiler_node* n)
{
bool exist = false;
for (sn_v::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i)
if ((*i == n) ||
((*i)->compare(n) == true))
exist = true;
if (exist)
return false;
lnode_succ->push_back(n);
n->add_pred(this);
return true;
}
void
spoiler_node::del_succ(spoiler_node* n)
{
for (sn_v::iterator i = lnode_succ->begin();
i != lnode_succ->end();)
{
if (*i == n)
{
i = lnode_succ->erase(i);
}
else
++i;
}
}
void
spoiler_node::add_pred(spoiler_node* n)
{
lnode_pred->push_back(n);
}
void
spoiler_node::del_pred()
{
for (sn_v::iterator i = lnode_pred->begin();
i != lnode_pred->end(); ++i)
(*i)->del_succ(this);
}
bool
spoiler_node::set_win()
{
bool change = not_win;
for (std::vector<spoiler_node*>::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i)
{
not_win |= (*i)->not_win;
}
if (change != not_win)
for (std::vector<spoiler_node*>::iterator i = lnode_pred->begin();
i != lnode_pred->end(); ++i)
(*i)->set_win();
return change != not_win;
}
std::string
spoiler_node::to_string(const tgba* a)
{
std::ostringstream os;
os << num_
<< " [shape=box, label=\"("
<< a->format_state(sc_->first)
<< ", "
<< a->format_state(sc_->second)
<< ")\"]"
<< std::endl;
return os.str();
}
std::string
spoiler_node::succ_to_string()
{
std::ostringstream os;
sn_v::iterator i;
for (i = lnode_succ->begin(); i != lnode_succ->end(); ++i)
{
os << num_ << " -> " << (*i)->num_ << std::endl;
}
return os.str();
}
bool
spoiler_node::compare(spoiler_node* n)
{
return (((sc_->first)->compare((n->get_pair())->first) == 0) &&
((sc_->second)->compare((n->get_pair())->second) == 0));
}
int
spoiler_node::get_nb_succ()
{
return lnode_succ->size();
}
const state*
spoiler_node::get_spoiler_node()
{
return sc_->first;
}
const state*
spoiler_node::get_duplicator_node()
{
return sc_->second;
}
state_couple*
spoiler_node::get_pair()
{
return sc_;
}
///////////////////////////////////////////////////////////////////////
// duplicator_node
duplicator_node::duplicator_node(const state* d_node,
const state* s_node,
bdd l,
bdd a,
int num)
: spoiler_node(d_node, s_node, num),
label_(l),
acc_(a)
{
}
duplicator_node::~duplicator_node()
{
}
bool
duplicator_node::set_win()
{
bool change = not_win;
if (!this->get_nb_succ())
not_win = true;
else
{
not_win = true;
for (std::vector<spoiler_node*>::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i)
{
not_win &= (*i)->not_win;
}
}
if (change != not_win)
for (std::vector<spoiler_node*>::iterator i = lnode_pred->begin();
i != lnode_pred->end(); ++i)
(*i)->set_win();
return change != not_win;
}
std::string
duplicator_node::to_string(const tgba* a)
{
std::ostringstream os;
os << num_
<< " [shape=box, label=\"("
<< a->format_state(sc_->first)
<< ", "
<< a->format_state(sc_->second)
<< ", ";
bdd_print_acc(os, a->get_dict(), label_);
os << ", ";
bdd_print_acc(os, a->get_dict(), acc_);
os << ")\"]"
<< std::endl;
return os.str();
}
bool
duplicator_node::compare(spoiler_node* n)
{
return (this->spoiler_node::compare(n) &&
(label_ == static_cast<duplicator_node*>(n)->get_label()) &&
(acc_ == static_cast<duplicator_node*>(n)->get_acc()));
}
bdd
duplicator_node::get_label() const
{
return label_;
}
bdd
duplicator_node::get_acc() const
{
return acc_;
}
bool
duplicator_node::match(bdd l, bdd a)
{
return ((l == label_) && (a == acc_));
}
bool
duplicator_node::implies(bdd l, bdd a)
{
// if (a | !b) == true then (a => b).
return (((l | !label_) == bddtrue) &&
((a | !acc_) == bddtrue));
}
///////////////////////////////////////////////////////////////////////
// parity_game_graph
void
parity_game_graph::process_state(const state* s,
int,
tgba_succ_iterator*)
{
tgba_state_.push_back(s);
}
void
parity_game_graph::print(std::ostream& os)
{
std::vector<spoiler_node*>::iterator i1;
std::vector<duplicator_node*>::iterator i2;
int n = 0;
os << "digraph G {" << std::endl;
os << "{" << std::endl
<< "rank = same;" << std::endl
<< "node [color=red];" << std::endl;
for (i1 = spoiler_vertice_.begin();
i1 != spoiler_vertice_.end(); ++i1)
{
os << (*i1)->to_string(aut_);
++n;
if (n > 20)
{
n = 0;
os << "}" << std::endl << std::endl
<< "{" << std::endl
<< "rank = same" << std::endl
<< "node [color=red];" << std::endl;
}
}
os << "}" << std::endl;
n = 0;
os << "{" << std::endl
<< "rank = same;" << std::endl
<< "node [color=green];" << std::endl;
for (i2 = duplicator_vertice_.begin();
i2 != duplicator_vertice_.end(); ++i2)
{
os << (*i2)->to_string(aut_);
++n;
if (n > 20)
{
n = 0;
os << "}" << std::endl << std::endl
<< "{" << std::endl
<< "rank = same" << std::endl
<< "node [color=green];" << std::endl;
}
}
os << "}" << std::endl << std::endl;
os << "edge [color=red];" << std::endl;
for (i1 = spoiler_vertice_.begin();
i1 != spoiler_vertice_.end(); ++i1)
{
os << (*i1)->succ_to_string();
}
os << std::endl
<< "edge [color=green];" << std::endl;
for (i2 = duplicator_vertice_.begin();
i2 != duplicator_vertice_.end(); ++i2)
{
os << (*i2)->succ_to_string();
}
os << "}" << std::endl;
}
parity_game_graph::~parity_game_graph()
{
std::vector<spoiler_node*>::iterator i1;
std::vector<duplicator_node*>::iterator i2;
for (i1 = spoiler_vertice_.begin();
i1 != spoiler_vertice_.end(); ++i1)
{
delete *i1;
}
for (i2 = duplicator_vertice_.begin();
i2 != duplicator_vertice_.end(); ++i2)
{
delete *i2;
}
spoiler_vertice_.clear();
duplicator_vertice_.clear();
}
parity_game_graph::parity_game_graph(const tgba* a)
: tgba_reachable_iterator_breadth_first(a)
{
this->run();
nb_node_parity_game = 0;
}
///////////////////////////////////////////////////////////////////////
// parity_game_graph_direct
void
parity_game_graph_direct::build_graph()
{
tgba_succ_iterator* si = 0;
typedef std::pair<bdd, bdd> couple_bdd;
couple_bdd *p = 0;
std::vector<couple_bdd*>* trans = 0;
bool exist = false;
spot::state* s = 0;
for (std::vector<const state*>::iterator i = tgba_state_.begin();
i != tgba_state_.end(); ++i)
{
// spoiler node are all state couple (i,j)
for (std::vector<const state*>::iterator j = tgba_state_.begin();
j != tgba_state_.end(); ++j)
{
spoiler_node* n1 = new spoiler_node(*i,
*j,
nb_node_parity_game++);
spoiler_vertice_.push_back(n1);
}
// duplicator node are all state couple where
// the first state i are reachable.
trans = new std::vector<couple_bdd*>;
for (std::vector<const state*>::iterator j = tgba_state_.begin();
j != tgba_state_.end(); ++j)
{
si = aut_->succ_iter(*j);
for (si->first(); !si->done(); si->next())
{
// if there exist a predecessor of i named j
s = si->current_state();
if (s->compare(*i) == 0)
{
// p is the label of the transition j->i
p = new couple_bdd(si->current_condition(),
si->current_acceptance_conditions());
// If an other predecessor of i has the same label p
// to reach i, then we don't compute the duplicator node.
exist = false;
for (std::vector<couple_bdd*>::iterator v
= trans->begin();
v != trans->end(); ++v)
{
if ((si->current_condition() == (*v)->first) &&
(si->current_acceptance_conditions()
== (*v)->second))
exist = true;
}
if (!exist)
{
// We build all the state couple with the label p.
trans->push_back(p);
for (std::vector<const state*>::iterator s
= tgba_state_.begin();
s != tgba_state_.end(); ++s)
{
duplicator_node* n2
= new
duplicator_node(*i,
*s,
si->current_condition(),
si
->current_acceptance_conditions(),
nb_node_parity_game++);
duplicator_vertice_.push_back(n2);
}
}
else
delete p;
}
s->destroy();
}
delete si;
}
std::vector<couple_bdd*>::iterator i2;
for (i2 = trans->begin(); i2 != trans->end(); ++i2)
{
delete *i2;
}
delete trans;
}
}
void
parity_game_graph_direct::build_link()
{
int nb_ds = 0;
int nb_sd = 0;
spot::state* s = 0;
// for each couple of (spoiler, duplicator)
for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i)
{
for (std::vector<duplicator_node*>::iterator j
= duplicator_vertice_.begin();
j != duplicator_vertice_.end(); ++j)
{
// We add a link between a duplicator and a spoiler.
if ((*j)->get_spoiler_node()
->compare((*i)->get_spoiler_node()) == 0)
{
tgba_succ_iterator* si
= aut_->succ_iter((*j)->get_duplicator_node());
for (si->first(); !si->done(); si->next())
{
s = si->current_state();
if ((s->compare((*i)->get_duplicator_node()) == 0) &&
(*j)->implies(si->current_condition(),
si->current_acceptance_conditions()))
{
(*j)->add_succ(*i);
++nb_ds;
}
s->destroy();
}
delete si;
}
// We add a link between a spoiler and a duplicator.
if ((*j)->get_duplicator_node()
->compare((*i)->get_duplicator_node()) == 0)
{
tgba_succ_iterator* si
= aut_->succ_iter((*i)->get_spoiler_node());
for (si->first(); !si->done(); si->next())
{
s = si->current_state();
if ((s->compare((*j)->get_spoiler_node()) == 0) &&
(*j)->match(si->current_condition(),
si->current_acceptance_conditions()))
{
(*i)->add_succ(*j);
++nb_sd;
}
s->destroy();
}
delete si;
}
}
}
}
void
parity_game_graph_direct::lift()
{
bool change = true;
while (change)
{
change = false;
for (std::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin();
i != duplicator_vertice_.end(); ++i)
{
change |= (*i)->set_win();
}
for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i)
{
change |= (*i)->set_win();
}
}
}
direct_simulation_relation*
parity_game_graph_direct::get_relation()
{
direct_simulation_relation* rel = new direct_simulation_relation;
state_couple* p = 0;
seen_map::iterator j;
for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i)
{
if (!(*i)->not_win)
{
p = new state_couple((*i)->get_spoiler_node(),
(*i)->get_duplicator_node());
rel->push_back(p);
// We remove the state in rel from seen
// because the destructor of
// tgba_reachable_iterator_breadth_first
// delete all instance of state.
if ((j = seen.find(p->first)) != seen.end())
seen.erase(j);
if ((j = seen.find(p->second)) != seen.end())
seen.erase(j);
}
}
return rel;
}
parity_game_graph_direct::~parity_game_graph_direct()
{
}
parity_game_graph_direct::parity_game_graph_direct(const tgba* a)
: parity_game_graph(a)
{
this->build_graph();
this->build_link();
this->lift();
}
///////////////////////////////////////////////////////////////////////
direct_simulation_relation*
get_direct_relation_simulation(const tgba* f,
std::ostream& os,
int opt)
{
parity_game_graph_direct* G = new parity_game_graph_direct(f);
direct_simulation_relation* rel = G->get_relation();
if (opt == 1)
G->print(os);
delete G;
return rel;
}
void
free_relation_simulation(direct_simulation_relation* rel)
{
if (rel == 0)
return;
Sgi::hash_map<const spot::state*, int,
state_ptr_hash, state_ptr_equal> seen;
Sgi::hash_map<const spot::state*, int,
state_ptr_hash, state_ptr_equal>::iterator j;
simulation_relation::iterator i;
for (i = rel->begin(); i != rel->end(); ++i)
{
if ((j = seen.find((*i)->first)) == seen.end())
seen[(*i)->first] = 0;
if ((j = seen.find((*i)->second)) == seen.end())
seen[(*i)->second] = 0;
delete *i;
}
delete rel;
rel = 0;
for (j = seen.begin(); j != seen.end();)
{
const state* ptr = j->first;
++j;
ptr->destroy();
}
}
bool
is_include(const tgba*, const tgba*)
{
return false;
}
const tgba*
reduc_tgba_sim(const tgba* f, int opt)
{
@ -661,41 +40,18 @@ namespace spot
return f;
}
spot::tgba_reduc* automatareduc = new spot::tgba_reduc(f);
// Destroy the automaton created by scc_filter.
if (opt & Reduce_Scc)
delete f;
if (opt & (Reduce_quotient_Dir_Sim | Reduce_transition_Dir_Sim))
if (opt & (Reduce_quotient_Dir_Sim | Reduce_transition_Dir_Sim
| Reduce_quotient_Del_Sim | Reduce_transition_Del_Sim))
{
direct_simulation_relation* rel
= get_direct_relation_simulation(automatareduc, std::cout);
tgba* res = simulation(f);
assert(rel);
if (opt & Reduce_Scc)
delete f;
automatareduc->display_rel_sim(rel, std::cout);
automatareduc->quotient_state(rel);
automatareduc->delete_transitions(rel);
free_relation_simulation(rel);
return res;
}
else
if (opt & (Reduce_quotient_Del_Sim | Reduce_transition_Del_Sim))
{
delayed_simulation_relation* rel
= get_delayed_relation_simulation(automatareduc, std::cout);
assert(rel);
automatareduc->display_rel_sim(rel, std::cout);
automatareduc->quotient_state(rel);
automatareduc->delete_transitions(rel);
free_relation_simulation(rel);
}
return automatareduc;
return tgba_dupexp_dfs(f);
}
}

305
src/tgbaalgos/reductgba_sim.hh
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -25,14 +25,9 @@
#ifndef SPOT_TGBAALGOS_REDUCTGBA_SIM_HH
#define SPOT_TGBAALGOS_REDUCTGBA_SIM_HH
#include "tgba/tgbareduc.hh"
#include "tgbaalgos/reachiter.hh"
#include <vector>
#include <list>
#include <sstream>
namespace spot
{
class tgba;
/// \addtogroup tgba_reduction
/// @{
@ -62,280 +57,34 @@ namespace spot
#endif
};
/// \brief Remove some node of the automata using a simulation
/// relation.
#if __GNUC__
/// \brief Simplify the automaton using a simulation relation.
///
/// \param a the automata to reduce.
/// Do not use this obsolete function.
///
/// \param a the automata to reduce
/// \param opt a conjonction of spot::reduce_tgba_options specifying
/// which optimizations to apply.
/// \return the reduced automata.
/// which optimizations to apply. Actually any
/// simulation-related flag will cause direct simulation
/// to be applied.
/// \return the reduced automaton
/// \deprecated Use scc_filter(), minimize_wdba(), or simulation().
const tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All)
__attribute__ ((deprecated));
#else
/// \brief Simplify the automaton using a simulation relation.
///
/// Do not use this obsolete function.
///
/// \param a the automata to reduce
/// \param opt a conjonction of spot::reduce_tgba_options specifying
/// which optimizations to apply. Actually any
/// simulation-related flag will cause direct simulation
/// to be applied.
/// \return the reduced automaton
/// \deprecated Use scc_filter(), minimize_wdba(), or simulation().
const tgba* reduc_tgba_sim(const tgba* a, int opt = Reduce_All);
#ifndef SWIG
/// \brief Compute a direct simulation relation on state of tgba \a f.
direct_simulation_relation* get_direct_relation_simulation(const tgba* a,
std::ostream& os,
int opt = -1);
/// Compute a delayed simulation relation on state of tgba \a f.
/// \bug Does not work for generalized automata.
delayed_simulation_relation* get_delayed_relation_simulation(const tgba* a,
std::ostream& os,
int opt = -1);
/// To free a simulation relation.
void free_relation_simulation(direct_simulation_relation* rel);
/// To free a simulation relation.
void free_relation_simulation(delayed_simulation_relation* rel);
///////////////////////////////////////////////////////////////////////
// simulation.
class spoiler_node;
class duplicator_node;
typedef std::vector<spoiler_node*> sn_v;
typedef std::vector<duplicator_node*> dn_v;
typedef std::vector<const state*> s_v;
/// \brief Parity game graph which compute a simulation relation.
class parity_game_graph : public tgba_reachable_iterator_breadth_first
{
public:
parity_game_graph(const tgba* a);
virtual ~parity_game_graph();
virtual simulation_relation* get_relation() = 0;
void print(std::ostream& os);
protected:
sn_v spoiler_vertice_;
dn_v duplicator_vertice_;
s_v tgba_state_;
int nb_node_parity_game;
void process_state(const state* s, int n, tgba_succ_iterator* si);
/// \brief Compute each node of the graph.
virtual void build_graph() = 0;
/// \brief Remove edge from spoiler to duplicator that make
/// duplicator loose.
/// Spoiler node whose still have some link, reveal
/// a direct simulation relation.
virtual void lift() = 0;
};
///////////////////////////////////////////////////////////////////////
// Direct simulation.
/// Spoiler node of parity game graph.
class spoiler_node
{
public:
spoiler_node(const state* d_node,
const state* s_node,
int num);
virtual ~spoiler_node();
/// \brief Add a successor.
/// Return true if \a n wasn't yet in the list of successor,
/// false eitherwise.
bool add_succ(spoiler_node* n);
void del_succ(spoiler_node* n);
virtual void add_pred(spoiler_node* n);
virtual void del_pred();
int get_nb_succ();
bool prune();
virtual bool set_win();
virtual std::string to_string(const tgba* a);
virtual std::string succ_to_string();
virtual bool compare(spoiler_node* n);
const state* get_spoiler_node();
const state* get_duplicator_node();
state_couple* get_pair();
bool not_win;
int num_; // for the dot display.
protected:
sn_v* lnode_succ;
sn_v* lnode_pred;
state_couple* sc_;
};
/// Duplicator node of parity game graph.
class duplicator_node : public spoiler_node
{
public:
duplicator_node(const state* d_node,
const state* s_node,
bdd l,
bdd a,
int num);
virtual ~duplicator_node();
virtual bool set_win();
virtual std::string to_string(const tgba* a);
virtual bool compare(spoiler_node* n);
bool match(bdd l, bdd a);
bool implies(bdd l, bdd a);
bdd get_label() const;
bdd get_acc() const;
protected:
bdd label_;
bdd acc_;
};
/// Parity game graph which compute the direct simulation relation.
class parity_game_graph_direct : public parity_game_graph
{
public:
parity_game_graph_direct(const tgba* a);
~parity_game_graph_direct();
virtual direct_simulation_relation* get_relation();
protected:
virtual void build_graph();
virtual void lift();
void build_link();
};
///////////////////////////////////////////////////////////////////////
// Delayed simulation.
/// Spoiler node of parity game graph for delayed simulation.
class spoiler_node_delayed : public spoiler_node
{
public:
spoiler_node_delayed(const state* d_node,
const state* s_node,
bdd a,
int num);
~spoiler_node_delayed();
/// Return true if the progress_measure has changed.
bool set_win();
bdd get_acceptance_condition_visited() const;
virtual bool compare(spoiler_node* n);
virtual std::string to_string(const tgba* a);
int get_progress_measure() const;
bool get_lead_2_acc_all();
bool set_lead_2_acc_all(bdd acc = bddfalse);
//
bool seen_;
protected:
/// a Bdd for retain all the acceptance condition
/// that a node has visited.
bdd acceptance_condition_visited_;
int progress_measure_;
bool lead_2_acc_all_;
};
/// Duplicator node of parity game graph for delayed simulation.
class duplicator_node_delayed : public duplicator_node
{
public:
duplicator_node_delayed(const state* d_node,
const state* s_node,
bdd l,
bdd a,
int num);
~duplicator_node_delayed();
/// Return true if the progress_measure has changed.
bool set_win();
virtual std::string to_string(const tgba* a);
bool implies_label(bdd l);
bool implies_acc(bdd a);
int get_progress_measure();
bool get_lead_2_acc_all();
bool set_lead_2_acc_all(bdd acc = bddfalse);
//
bool seen_;
protected:
int progress_measure_;
bool lead_2_acc_all_;
};
/// Parity game graph which computes the delayed simulation relation
/// as explained in
/// \verbatim
/// @InProceedings{etessami.01.alp,
/// author = {Kousha Etessami and Thomas Wilke and Rebecca A. Schuller},
/// title = {Fair Simulation Relations, Parity Games, and State Space
/// Reduction for Buchi Automata},
/// booktitle = {Proceedings of the 28th international colloquium on
/// Automata, Languages and Programming},
/// pages = {694--707},
/// year = {2001},
/// editor = {Fernando Orejas and Paul G. Spirakis and Jan van Leeuwen},
/// volume = {2076},
/// series = {Lecture Notes in Computer Science},
/// address = {Crete, Greece},
/// month = {July},
/// publisher = {Springer-Verlag}
/// }
/// \endverbatim
class parity_game_graph_delayed: public parity_game_graph
{
public:
parity_game_graph_delayed(const tgba* a);
~parity_game_graph_delayed();
virtual delayed_simulation_relation* get_relation();
private:
/// Vector which contain all the sub-set of the set
/// of acceptance condition.
typedef std::vector<bdd> bdd_v;
bdd_v sub_set_acc_cond_;
/// Return the number of acceptance condition.
int nb_set_acc_cond();
///
duplicator_node_delayed* add_duplicator_node_delayed(const spot::state* sn,
const spot::state* dn,
bdd acc,
bdd label,
int nb);
///
spoiler_node_delayed* add_spoiler_node_delayed(const spot::state* sn,
const spot::state* dn,
bdd acc,
int nb);
void build_recurse_successor_spoiler(spoiler_node* sn,
std::ostringstream& os);
void build_recurse_successor_duplicator(duplicator_node* dn,
spoiler_node* sn,
std::ostringstream& os);
/// \brief Compute the couple as for direct simulation,
virtual void build_graph();
/// \brief The Jurdzinski's lifting algorithm.
virtual void lift();
};
#endif // SWIG
#endif
/// @}
}

675
src/tgbaalgos/reductgba_sim_del.cc
View file

@ -1,675 +0,0 @@
// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "reductgba_sim.hh"
#include "tgba/bddprint.hh"
namespace spot
{
/// Number of spoiler node with a one priority (see icalp2001).
/// The one priority is represent by a \a acceptance_condition_visited_
/// which differ of bddfalse.
/// This spoiler node are looser for the duplicator.
/// FIXME: get rid of these ugly globals
static int nb_spoiler_loose_;
static int nb_spoiler;
static int nb_duplicator;
static bdd all_acc_cond = bddfalse;
static std::vector<bool*> bool_v;
//static int nb_node = 0;
//seen_map_node seen_node_;
///////////////////////////////////////////////////////////////////////
// spoiler_node_delayed
spoiler_node_delayed::spoiler_node_delayed(const state* d_node,
const state* s_node,
bdd a,
int num)
: spoiler_node(d_node, s_node, num),
acceptance_condition_visited_(a)
{
++nb_spoiler;
progress_measure_ = 0;
if (acceptance_condition_visited_ != bddfalse)
++nb_spoiler_loose_;
lead_2_acc_all_ = false;
seen_ = false;
}
spoiler_node_delayed::~spoiler_node_delayed()
{
if (acceptance_condition_visited_ != bddfalse)
--nb_spoiler_loose_;
}
bool
spoiler_node_delayed::set_win()
{
// We take the max of the progress measure of the successor node
// because we are on a spoiler.
if (lnode_succ->empty())
progress_measure_ = nb_spoiler_loose_ + 1;
if (progress_measure_ >= nb_spoiler_loose_ + 1)
return false;
bool change;
int tmpmax = 0;
int tmp = 0;
int tmpmaxwin = -1;
sn_v::iterator i = lnode_succ->begin();
if (i != lnode_succ->end())
{
tmpmax =
static_cast<duplicator_node_delayed*>(*i)->get_progress_measure();
if (static_cast<duplicator_node_delayed*>(*i)->get_lead_2_acc_all())
tmpmaxwin = tmpmax;
++i;
}
for (; i != lnode_succ->end(); ++i)
{
tmp =
static_cast<duplicator_node_delayed*>(*i)->get_progress_measure();
if (tmp > tmpmax)
tmpmax = tmp;
if (static_cast<duplicator_node_delayed*>(*i)->get_lead_2_acc_all() &&
(tmp > tmpmaxwin))
tmpmaxwin = tmp;
}
if (tmpmaxwin != -1)
tmpmax = tmpmaxwin;
// If the priority of the node is 1
// acceptance_condition_visited_ != bddfalse
// then we increment the progress measure of 1.
if ((acceptance_condition_visited_ != bddfalse) &&
(tmpmax < (nb_spoiler_loose_ + 1)))
++tmpmax;
change = (progress_measure_ < tmpmax);
progress_measure_ = tmpmax;
return change;
}
bool
spoiler_node_delayed::compare(spoiler_node* n)
{
return (this->spoiler_node::compare(n) &&
(acceptance_condition_visited_ ==
static_cast<spoiler_node_delayed*>(n)->
get_acceptance_condition_visited()));
}
std::string
spoiler_node_delayed::to_string(const tgba* a)
{
std::ostringstream os;
// print the node.
os << num_
<< " [shape=box, label=\"("
<< a->format_state(sc_->first)
<< ", "
<< a->format_state(sc_->second)
<< ", ";
//bdd_print_acc(os, a->get_dict(), acceptance_condition_visited_);
if (acceptance_condition_visited_ == bddfalse)
{
os << "false";
}
else
{
os << "ACC";
}
os << ")"
<< " pm = " << progress_measure_;
if (lead_2_acc_all_)
os << ", 1\"]";
else
os << ", 0\"]";
os << std::endl;
return os.str();
}
bdd
spoiler_node_delayed::get_acceptance_condition_visited() const
{
return acceptance_condition_visited_;
}
int
spoiler_node_delayed::get_progress_measure() const
{
if ((acceptance_condition_visited_ == bddfalse) &&
(progress_measure_ != (nb_spoiler_loose_ + 1)))
return 0;
else
return progress_measure_;
}
bool
spoiler_node_delayed::get_lead_2_acc_all()
{
return lead_2_acc_all_;
}
bool
spoiler_node_delayed::set_lead_2_acc_all(bdd acc)
{
if (!seen_)
{
seen_ = true;
for (sn_v::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i)
static_cast<duplicator_node_delayed*>(*i)->set_lead_2_acc_all(acc);
}
else
{
if (acc == all_acc_cond)
lead_2_acc_all_ = true;
}
return lead_2_acc_all_;
}
///////////////////////////////////////////////////////////////////////
// duplicator_node_delayed
duplicator_node_delayed::duplicator_node_delayed(const state* d_node,
const state* s_node,
bdd l,
bdd a,
int num)
: duplicator_node(d_node, s_node, l, a, num)
{
++nb_duplicator;
progress_measure_ = 0;
all_acc_cond |= a;
lead_2_acc_all_ = false;
seen_ = false;
}
duplicator_node_delayed::~duplicator_node_delayed()
{
}
bool
duplicator_node_delayed::set_win()
{
// We take the min of the progress measure of the successor node
// because we are on a duplicator.
if (lnode_succ->empty())
progress_measure_ = nb_spoiler_loose_ + 1;
if (progress_measure_ >= nb_spoiler_loose_ + 1)
return false;
bool change;
int tmpmin = 0;
int tmp = 0;
int tmpminwin = -1;
sn_v::iterator i = lnode_succ->begin();
if (i != lnode_succ->end())
{
tmpmin =
static_cast<spoiler_node_delayed*>(*i)->get_progress_measure();
if (static_cast<spoiler_node_delayed*>(*i)->get_lead_2_acc_all())
tmpminwin = tmpmin;
++i;
}
for (; i != lnode_succ->end(); ++i)
{
tmp = static_cast<spoiler_node_delayed*>(*i)->get_progress_measure();
if (tmp < tmpmin)
tmpmin = tmp;
if (static_cast<spoiler_node_delayed*>(*i)->get_lead_2_acc_all() &&
(tmp > tmpminwin))
tmpminwin = tmp;
}
if (tmpminwin != -1)
tmpmin = tmpminwin;
change = (progress_measure_ < tmpmin);
progress_measure_ = tmpmin;
return change;
}
std::string
duplicator_node_delayed::to_string(const tgba* a)
{
std::ostringstream os;
// print the node.
os << num_
<< " [shape=box, label=\"("
<< a->format_state(sc_->first)
<< ", "
<< a->format_state(sc_->second)
<< ", ";
if (label_ == bddfalse)
os << "0";
else if (label_ == bddtrue)
os << "1";
else
bdd_print_acc(os, a->get_dict(), label_);
//<< ", ";
//bdd_print_acc(os, a->get_dict(), acc_);
os << ")"
<< " pm = " << progress_measure_;
if (lead_2_acc_all_)
os << ", 1\"]";
else
os << ", 0\"]";
os << std::endl;
return os.str();
}
bool
duplicator_node_delayed::implies_label(bdd l)
{
return ((l | !label_) == bddtrue);
}
bool
duplicator_node_delayed::implies_acc(bdd a)
{
return ((a | !acc_) == bddtrue);
}
int
duplicator_node_delayed::get_progress_measure()
{
return progress_measure_;
}
bool
duplicator_node_delayed::get_lead_2_acc_all()
{
return lead_2_acc_all_;
}
bool
duplicator_node_delayed::set_lead_2_acc_all(bdd acc)
{
acc |= acc_;
if (!seen_)
{
seen_ = true;
for (sn_v::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i)
lead_2_acc_all_
|= static_cast<spoiler_node_delayed*>(*i)->set_lead_2_acc_all(acc);
}
return lead_2_acc_all_;
}
///////////////////////////////////////////////////////////////////////
// parity_game_graph_delayed
int
parity_game_graph_delayed::nb_set_acc_cond()
{
return aut_->number_of_acceptance_conditions();
}
// We build only node which are reachable
void
parity_game_graph_delayed::build_graph()
{
// We build only some "basic" spoiler node.
sn_v tab_temp;
s_v::iterator i1;
for (i1 = tgba_state_.begin(); i1 != tgba_state_.end(); ++i1)
{
// spoiler node are all state couple (i,j)
s_v::iterator i2;
for (i2 = tgba_state_.begin();
i2 != tgba_state_.end(); ++i2)
{
//std::cout << "add spoiler node" << std::endl;
++nb_spoiler;
spoiler_node_delayed* n1
= new spoiler_node_delayed(*i1, *i2,
bddfalse,
nb_node_parity_game++);
spoiler_vertice_.push_back(n1);
tab_temp.push_back(n1);
}
}
sn_v::iterator j;
std::ostringstream os;
for (j = tab_temp.begin(); j != tab_temp.end(); ++j)
{
// We add a link between a spoiler and a (new) duplicator.
// The acc of the duplicator must contains the
// acceptance_condition_visited_ of the spoiler.
//std::cout << "build_link : iter " << ++n << std::endl;
build_recurse_successor_spoiler(*j, os);
}
}
void
parity_game_graph_delayed::
build_recurse_successor_spoiler(spoiler_node* sn,
std::ostringstream& os)
{
assert(sn);
tgba_succ_iterator* si = aut_->succ_iter(sn->get_spoiler_node());
for (si->first(); !si->done(); si->next())
{
bdd btmp = si->current_acceptance_conditions() |
static_cast<spoiler_node_delayed*>(sn)->
get_acceptance_condition_visited();
s_v::iterator i1;
state* s;
for (i1 = tgba_state_.begin();
i1 != tgba_state_.end(); ++i1)
{
s = si->current_state();
if (s->compare(*i1) == 0)
{
s->destroy();
duplicator_node_delayed* dn
= add_duplicator_node_delayed(*i1,
sn->get_duplicator_node(),
si->current_condition(),
btmp,
nb_node_parity_game++);
if (!(sn->add_succ(dn)))
continue;
std::ostringstream os2;
os2 << os.str() << " ";
build_recurse_successor_duplicator(dn, sn, os2);
}
else
s->destroy();
}
}
delete si;
}
void
parity_game_graph_delayed::
build_recurse_successor_duplicator(duplicator_node* dn,
spoiler_node* ,
std::ostringstream& os)
{
tgba_succ_iterator* si = aut_->succ_iter(dn->get_duplicator_node());
for (si->first(); !si->done(); si->next())
{
// if si->current_condition() doesn't implies dn->get_label()
// then duplicator can't play.
if ((si->current_condition() | !dn->get_label()) != bddtrue)
{
continue;
}
bdd btmp = dn->get_acc() -
(dn->get_acc() & si->current_acceptance_conditions());
s_v::iterator i1;
state* s;
for (i1 = tgba_state_.begin();
i1 != tgba_state_.end(); ++i1)
{
s = si->current_state();
if (s->compare(*i1) == 0)
{
s->destroy();
spoiler_node_delayed* sn_n
= add_spoiler_node_delayed(dn->get_spoiler_node(),
*i1,
btmp,
nb_node_parity_game++);
if (!(dn->add_succ(sn_n)))
continue;
std::ostringstream os2;
os2 << os.str() << " ";
build_recurse_successor_spoiler(sn_n, os2);
}
else
s->destroy();
}
}
delete si;
}
duplicator_node_delayed*
parity_game_graph_delayed::add_duplicator_node_delayed(const spot::state* sn,
const spot::state* dn,
bdd acc,
bdd label,
int nb)
{
bool exist = false;
duplicator_node_delayed* dn_n
= new duplicator_node_delayed(sn, dn, acc, label, nb);
for (std::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin();
i != duplicator_vertice_.end(); ++i)
{
if (dn_n->compare(*i))
{
exist = true;
delete dn_n;
dn_n = static_cast<duplicator_node_delayed*>(*i);
break;
}
}
if (!exist)
duplicator_vertice_.push_back(dn_n);
return dn_n;
}
spoiler_node_delayed*
parity_game_graph_delayed::add_spoiler_node_delayed(const spot::state* sn,
const spot::state* dn,
bdd acc,
int nb)
{
bool exist = false;
//bool l2a = (acc != aut_->all_acceptance_conditions());
spoiler_node_delayed* sn_n
= new spoiler_node_delayed(sn, dn, acc, nb);
for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i)
{
if (sn_n->compare(*i))
{
exist = true;
delete sn_n;
sn_n = static_cast<spoiler_node_delayed*>(*i);
break;
}
}
if (!exist)
spoiler_vertice_.push_back(sn_n);
return sn_n;
}
void
parity_game_graph_delayed::lift()
{
// Jurdzinski's algorithm
bool change = true;
while (change)
{
//std::cout << "lift::change = true" << std::endl;
change = false;
for (std::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin();
i != duplicator_vertice_.end(); ++i)
{
change |= (*i)->set_win();
}
for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i)
{
change |= (*i)->set_win();
}
}
//std::cout << "lift::change = false" << std::endl;
}
delayed_simulation_relation*
parity_game_graph_delayed::get_relation()
{
delayed_simulation_relation* rel = new delayed_simulation_relation;
state_couple* p = 0;
seen_map::iterator j;
// This does not work for generalized automata. A tarjan-like
// algorithm is required to tell whether a state can lead to an
// acceptance cycle.
if (this->nb_set_acc_cond() > 1)
return rel;
for (std::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i)
{
if ((static_cast<spoiler_node_delayed*>(*i)->get_progress_measure()
< nb_spoiler_loose_ + 1) &&
(static_cast<spoiler_node_delayed*>(*i)
->get_acceptance_condition_visited() == bddfalse))
{
p = new state_couple((*i)->get_spoiler_node(),
(*i)->get_duplicator_node());
rel->push_back(p);
// We remove the state in rel from seen
// because the destructor of
// tgba_reachable_iterator_breadth_first
// delete all the state.
if ((j = seen.find(p->first)) != seen.end())
seen.erase(j);
if ((j = seen.find(p->second)) != seen.end())
seen.erase(j);
}
}
return rel;
}
parity_game_graph_delayed::~parity_game_graph_delayed()
{
}
parity_game_graph_delayed::parity_game_graph_delayed(const tgba* a)
: parity_game_graph(a)
{
nb_spoiler_loose_ = 0;
this->build_graph();
this->lift();
}
///////////////////////////////////////////
delayed_simulation_relation*
get_delayed_relation_simulation(const tgba* f, std::ostream& os, int opt)
{
parity_game_graph_delayed* G = new parity_game_graph_delayed(f);
delayed_simulation_relation* rel = G->get_relation();
if (opt == 1)
G->print(os);
delete G;
return rel;
}
void
free_relation_simulation(delayed_simulation_relation* rel)
{
if (rel == 0)
return;
Sgi::hash_map<const spot::state*, int,
state_ptr_hash, state_ptr_equal> seen;
Sgi::hash_map<const spot::state*, int,
state_ptr_hash, state_ptr_equal>::iterator j;
delayed_simulation_relation::iterator i;
for (i = rel->begin(); i != rel->end(); ++i)
{
if ((j = seen.find((*i)->first)) == seen.end())
seen[(*i)->first] = 0;
if ((j = seen.find((*i)->second)) == seen.end())
seen[(*i)->second] = 0;
delete *i;
}
delete rel;
rel = 0;
for (j = seen.begin(); j != seen.end();)
{
const state* ptr = j->first;
++j;
ptr->destroy();
}
}
}

7
src/tgbatest/Makefile.am
View file

@ -43,8 +43,6 @@ check_PROGRAMS = \
ltlprod \
mixprod \
powerset \
reductgba \
reduccmp \
taatgba \
tgbaread \
tripprod
@ -65,9 +63,6 @@ ltlprod_SOURCES = ltlprod.cc
mixprod_SOURCES = mixprod.cc
powerset_SOURCES = powerset.cc
randtgba_SOURCES = randtgba.cc
reductgba_SOURCES = reductgba.cc
reduccmp_SOURCES = reductgba.cc
reduccmp_CXXFLAGS = -DREDUCCMP
taatgba_SOURCES = taatgba.cc
tgbaread_SOURCES = tgbaread.cc
tripprod_SOURCES = tripprod.cc
@ -97,8 +92,6 @@ TESTS = \
degendet.test \
degenid.test \
kv.test \
reduccmp.test \
reductgba.test \
scc.test \
sccsimpl.test \
obligation.test \

134
src/tgbatest/ltl2tgba.cc
View file

@ -1,8 +1,9 @@
// Copyright (C) 2007, 2008, 2009, 2010, 2011 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// -*- coding: utf-8 -*-
// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis
// Coopératifs (SRC), Université Pierre et Marie Curie.
// Paris 6 (LIP6), département Systèmes Répartis
// Coopératifs (SRC), Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -49,7 +50,6 @@
#include "tgbaalgos/dupexp.hh"
#include "tgbaalgos/minimize.hh"
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/reductgba_sim.hh"
#include "tgbaalgos/replayrun.hh"
#include "tgbaalgos/rundotdec.hh"
#include "tgbaalgos/sccfilter.hh"
@ -196,22 +196,11 @@ syntax(char* prog)
<< "Automaton simplifications (after translation):"
<< std::endl
<< " -R1q merge states using direct simulation "
<< "(use -L for more reduction)"
<< std::endl
<< " -R1t remove transitions using direct simulation "
<< "(use -L for more reduction)"
<< std::endl
<< " -R2q merge states using delayed simulation" << std::endl
<< " -R2t remove transitions using delayed simulation"
<< std::endl
<< " -R3 use SCC to reduce the automata" << std::endl
<< " -R3f clean more acceptance conditions than -R3" << std::endl
<< " "
<< "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
<< std::endl
<< " -Rd display the simulation relation" << std::endl
<< " -RD display the parity game (dot format)" << std::endl
<< " -Rm attempt to minimize the automata" << std::endl
<< std::endl
@ -314,13 +303,11 @@ main(int argc, char** argv)
bool accepting_run_replay = false;
bool from_file = false;
bool read_neverclaim = false;
int reduc_aut = spot::Reduce_None;
int redopt = spot::ltl::Reduce_None;
bool scc_filter = false;
bool scc_filter_all = false;
bool symbolic_scc_pruning = false;
bool display_reduce_form = false;
bool display_rel_sim = false;
bool display_parity_game = false;
bool post_branching = false;
bool fair_loop_approx = false;
bool graph_run_opt = false;
@ -621,33 +608,22 @@ main(int argc, char** argv)
{
output = 3;
}
else if (!strcmp(argv[formula_index], "-R1q"))
else if (!strcmp(argv[formula_index], "-R1q")
|| !strcmp(argv[formula_index], "-R1t")
|| !strcmp(argv[formula_index], "-R2q")
|| !strcmp(argv[formula_index], "-R2t"))
{
reduc_aut |= spot::Reduce_quotient_Dir_Sim;
}
else if (!strcmp(argv[formula_index], "-RSD"))
{
reduction_dir_sim = true;
}
else if (!strcmp(argv[formula_index], "-R1t"))
{
reduc_aut |= spot::Reduce_transition_Dir_Sim;
}
else if (!strcmp(argv[formula_index], "-R2q"))
{
reduc_aut |= spot::Reduce_quotient_Del_Sim;
}
else if (!strcmp(argv[formula_index], "-R2t"))
{
reduc_aut |= spot::Reduce_transition_Del_Sim;
// For backward compatibility, make all these options
// equal to -RSD.
reduction_dir_sim = true;
}
else if (!strcmp(argv[formula_index], "-R3"))
{
reduc_aut |= spot::Reduce_Scc;
scc_filter = true;
}
else if (!strcmp(argv[formula_index], "-R3f"))
{
reduc_aut |= spot::Reduce_Scc;
scc_filter = true;
scc_filter_all = true;
}
else if (!strcmp(argv[formula_index], "-R3b"))
@ -658,18 +634,14 @@ main(int argc, char** argv)
{
display_reduce_form = true;
}
else if (!strcmp(argv[formula_index], "-Rd"))
{
display_rel_sim = true;
}
else if (!strcmp(argv[formula_index], "-RD"))
{
display_parity_game = true;
}
else if (!strcmp(argv[formula_index], "-Rm"))
{
opt_minimize = true;
}
else if (!strcmp(argv[formula_index], "-RSD"))
{
reduction_dir_sim = true;
}
else if (!strcmp(argv[formula_index], "-M"))
{
opt_monitor = true;
@ -898,12 +870,12 @@ main(int argc, char** argv)
to_free = a;
}
if (opt_monitor && ((reduc_aut & spot::Reduce_Scc) == 0))
if (opt_monitor && !scc_filter)
{
if (dynamic_cast<const spot::tgba_bdd_concrete*>(a))
symbolic_scc_pruning = true;
else
reduc_aut |= spot::Reduce_Scc;
scc_filter = true;
}
if (symbolic_scc_pruning)
@ -932,7 +904,7 @@ main(int argc, char** argv)
// Remove dead SCCs and useless acceptance conditions before
// degeneralization.
const spot::tgba* aut_scc = 0;
if (reduc_aut & spot::Reduce_Scc)
if (scc_filter)
{
tm.start("reducing A_f w/ SCC");
a = aut_scc = spot::scc_filter(a, scc_filter_all);
@ -1019,67 +991,6 @@ main(int argc, char** argv)
// pointless.
}
spot::tgba_reduc* aut_red = 0;
if (reduc_aut != spot::Reduce_None)
{
if (reduc_aut & ~spot::Reduce_Scc)
{
tm.start("reducing A_f w/ sim.");
a = aut_red = new spot::tgba_reduc(a);
if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
spot::Reduce_transition_Dir_Sim |
spot::Reduce_quotient_Del_Sim |
spot::Reduce_transition_Del_Sim))
{
spot::direct_simulation_relation* rel_dir = 0;
spot::delayed_simulation_relation* rel_del = 0;
if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
spot::Reduce_transition_Dir_Sim))
{
rel_dir =
spot::get_direct_relation_simulation
(a, std::cout, display_parity_game);
assert(rel_dir);
}
if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
spot::Reduce_transition_Del_Sim))
{
rel_del =
spot::get_delayed_relation_simulation
(a, std::cout, display_parity_game);
assert(rel_del);
}
if (display_rel_sim)
{
if (rel_dir)
aut_red->display_rel_sim(rel_dir, std::cout);
if (rel_del)
aut_red->display_rel_sim(rel_del, std::cout);
}
if (reduc_aut & spot::Reduce_quotient_Dir_Sim)
aut_red->quotient_state(rel_dir);
if (reduc_aut & spot::Reduce_transition_Dir_Sim)
aut_red->delete_transitions(rel_dir);
if (reduc_aut & spot::Reduce_quotient_Del_Sim)
aut_red->quotient_state(rel_del);
if (reduc_aut & spot::Reduce_transition_Del_Sim)
aut_red->delete_transitions(rel_del);
if (rel_dir)
spot::free_relation_simulation(rel_dir);
if (rel_del)
spot::free_relation_simulation(rel_del);
}
tm.stop("reducing A_f w/ sim.");
}
}
const spot::tgba_explicit_string* expl = 0;
switch (dupexp)
{
@ -1394,7 +1305,6 @@ main(int argc, char** argv)
delete product_to_free;
delete system;
delete expl;
delete aut_red;
delete minimized;
delete degeneralized;
delete aut_scc;

59
src/tgbatest/reduccmp.test
View file

@ -1,59 +0,0 @@
#!/bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
# 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 2 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 Spot; see the file COPYING. If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.
. ./defs
set -e
# FIXME
exit 0
cat >input <<EOF
acc = c;
s1, "s2", "a", c;
"s2", "s3", "a",;
"3", s2, "a",;
EOF
run 0 ../reduccmp 0 input
run 0 ../reduccmp 0 input > stdout
cat >expected <<EOF
digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="s1, SCC -1"]
}
EOF
rm input stdout expected
# Sort out some possible inversions in the output.
# (The order is not guaranteed by SPOT.)
sed 's/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout
diff stdout expected
# FIXME
exit 0

180
src/tgbatest/reductgba.cc
View file

@ -1,180 +0,0 @@
// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// 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.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <cstdlib>
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/reductgba_sim.hh"
#include "tgba/tgbareduc.hh"
#include "ltlvisit/reduce.hh"
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
#include "tgbaalgos/ltl2tgba_lacim.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgba/tgbatba.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
#include "tgbaparse/public.hh"
#include "tgbaalgos/dupexp.hh"
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/sccfilter.hh"
#include "misc/escape.hh"
void
syntax(char* prog)
{
#ifdef REDUCCMP
std::cerr << prog << " option file" << std::endl;
#else
std::cerr << prog << " option formula" << std::endl;
#endif
exit(2);
}
int
main(int argc, char** argv)
{
if (argc < 3)
syntax(argv[0]);
int o = spot::ltl::Reduce_None;
switch (atoi(argv[1]))
{
case 0:
o = spot::Reduce_Scc;
break;
case 1:
o = spot::Reduce_quotient_Dir_Sim;
break;
case 2:
o = spot::Reduce_transition_Dir_Sim;
break;
case 3:
o = spot::Reduce_quotient_Del_Sim;
break;
case 4:
o = spot::Reduce_transition_Del_Sim;
break;
case 5:
o = spot::Reduce_quotient_Dir_Sim |
spot::Reduce_transition_Dir_Sim |
spot::Reduce_Scc;
break;
case 6:
o = spot::Reduce_quotient_Del_Sim |
spot::Reduce_transition_Del_Sim |
spot::Reduce_Scc;
break;
case 7:
// No Reduction
break;
default:
return 2;
}
int exit_code = 0;
spot::direct_simulation_relation* rel_dir = 0;
spot::delayed_simulation_relation* rel_del = 0;
spot::tgba* automata = 0;
spot::tgba_reduc* automatareduc = 0;
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::bdd_dict* dict = new spot::bdd_dict();
#ifdef REDUCCMP
spot::tgba_parse_error_list pel;
automata = spot::tgba_parse(argv[2], pel, dict, env, env, false);
if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel))
return 2;
#else
spot::ltl::parse_error_list p1;
spot::ltl::formula* f = spot::ltl::parse(argv[2], p1, env);
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
return 2;
automata = spot::ltl_to_tgba_fm(f, dict,
false, true,
false, true);
#endif
spot::dotty_reachable(std::cout, automata);
automatareduc = new spot::tgba_reduc(automata);
if (o & spot::Reduce_quotient_Dir_Sim)
{
rel_dir = spot::get_direct_relation_simulation(automatareduc, std::cout);
automatareduc->quotient_state(rel_dir);
}
else if (o & spot::Reduce_quotient_Del_Sim)
{
std::cout << "get delayed" << std::endl;
rel_del = spot::get_delayed_relation_simulation(automatareduc, std::cout);
std::cout << "quotient state" << std::endl;
automatareduc->quotient_state(rel_del);
std::cout << "end" << std::endl;
}
if (rel_dir != 0)
{
automatareduc->display_rel_sim(rel_dir, std::cout);
spot::free_relation_simulation(rel_dir);
}
if (rel_del != 0)
{
automatareduc->display_rel_sim(rel_del, std::cout);
spot::free_relation_simulation(rel_del);
}
spot::tgba* res = automatareduc;
if (o & spot::Reduce_Scc)
{
res = spot::scc_filter(automatareduc);
delete automatareduc;
}
spot::dotty_reachable(std::cout, res);
delete res;
delete automata;
#ifndef REDUCCMP
if (f != 0)
f->destroy();
#endif
assert(spot::ltl::atomic_prop::instance_count() == 0);
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
if (dict != 0)
delete dict;
return exit_code;
}

92
src/tgbatest/reductgba.test
View file

@ -1,92 +0,0 @@
#!/bin/sh
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
# 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 2 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 Spot; see the file COPYING. If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.
. ./defs
set -e
check()
{
#run 0 ../reductgba "$1" "$2"
../reductgba "$1" "$2"
}
# We don't check the output, but just running these might be enough to
# trigger assertions.
check 0 a
check 0 'a U b'
check 0 'a U Fb'
check 0 'X a'
check 0 'a & b & c'
check 0 'a | b | (c U (d & (g U (h ^ i))))'
check 0 'Xa & (b U !a) & (b U !a)'
check 0 'Fa & Xb & GFc & Gd'
check 0 'Fa & Xa & GFc & Gc'
check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 0 'a R (b R c)'
check 0 '(a U b) U (c U d)'
check 0 '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
check 0 '((p3 | Xp3 | Xp2) & (X!p3 | (!p3 & X!p2))) R F(0)'
check 1 a
check 1 'a U b'
check 1 'X a'
check 1 'a & b & c'
check 1 'a | b | (c U (d & (g U (h ^ i))))'
check 1 'Xa & (b U !a) & (b U !a)'
check 1 'Fa & Xb & GFc & Gd'
check 1 'Fa & Xa & GFc & Gc'
check 1 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 1 'a R (b R c)'
check 1 '(a U b) U (c U d)'
check 1 '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
check 2 a
check 2 'a U b'
check 2 'X a'
check 2 'a & b & c'
check 2 'a | b | (c U (d & (g U (h ^ i))))'
check 2 'Xa & (b U !a) & (b U !a)'
check 2 'Fa & Xb & GFc & Gd'
check 2 'Fa & Xa & GFc & Gc'
check 2 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 2 'a R (b R c)'
check 2 '(a U b) U (c U d)'
check 2 '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
check 3 a
check 3 'a U b'
check 3 'a U Fb'
check 3 'X a'
check 3 'a & b & c'
check 3 'a | b | (c U (d & (g U (h ^ i))))'
check 3 'Xa & (b U !a) & (b U !a)'
check 3 'Fa & Xb & GFc & Gd'
check 3 'Fa & Xa & GFc & Gc'
check 3 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 3 'a R (b R c)'
check 3 '(a U b) U (c U d)'
check 3 '((Xp2)U(X(1)))&(p1 R(p2 R p0))'

41
src/tgbatest/spotlbtt.test
View file

@ -1,9 +1,10 @@
#!/bin/sh
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# -*- coding: utf-8 -*-
# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire
# d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
# Coopératifs (SRC), Université Pierre et Marie Curie.
# d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
# Coopératifs (SRC), Université Pierre et Marie Curie.
#
# This file is part of Spot, a model checking library.
#
@ -150,22 +151,6 @@ Algorithm
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM), post reduction with direct simulation"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -R1q -R1t -R3 -r4 -F -f -t'"
Enabled = yes
}
Algorithm
{
Name = "Spot (Couvreur -- FM), post reduction with delayed simulation"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -R2q -R2t -F -f -t'"
Enabled = yes
}
Algorithm
{
Name = "Spot (Couvreur -- FM), post reduction with scc"
@ -174,14 +159,6 @@ Algorithm
Enabled = yes
}
Algorithm
{
Name = "Spot (Couvreur -- FM), pre + post reduction"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -r4 -R1q -R1t -R3 -F -f -t'"
Enabled = yes
}
Algorithm
{
Name = "Spot (Couvreur -- FM), +pre +WDBA"
@ -198,14 +175,6 @@ Algorithm
Enabled = yes
}
Algorithm
{
Name = "Spot (Couvreur -- FM), pre + allpost reduction"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -r4 -R1q -R1t -R2q -R2t -R3 -F -f -t'"
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM), without symb_merge"

3
wrap/python/spot.i
View file

@ -96,7 +96,6 @@
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/minimize.hh"
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/reductgba_sim.hh"
#include "tgbaalgos/rundotdec.hh"
#include "tgbaalgos/save.hh"
#include "tgbaalgos/sccfilter.hh"
@ -180,7 +179,6 @@ using namespace spot;
%feature("new") spot::ltl_to_tgba_lacim;
%feature("new") spot::minimize_wdba;
%feature("new") spot::minimize_monitor;
%feature("new") spot::reduc_tgba_sim;
%feature("new") spot::scc_filter;
%feature("new") spot::tgba_dupexp_bfs;
%feature("new") spot::tgba_dupexp_dfs;
@ -226,7 +224,6 @@ using namespace spot;
%include "tgbaalgos/magic.hh"
%include "tgbaalgos/minimize.hh"
%include "tgbaalgos/neverclaim.hh"
%include "tgbaalgos/reductgba_sim.hh"
%include "tgbaalgos/rundotdec.hh"
%include "tgbaalgos/save.hh"
%include "tgbaalgos/sccfilter.hh"