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

* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,

Browse source 
src/tgbaalgos/reductgba_sim.cc,	src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/reductgba_sim_del.cc: Remove some comments.

* src/tgbatest/ltl2tgba.cc, src/tgbatest/reductgba.cc: Adjust ...
* src/tgbatest/spotlbtt.test: More test (delayed simulation)
This commit is contained in:
martinez 2004-07-05 16:03:26 +00:00
parent 7ff3898139
commit 9ce6888872
9 changed files with 227 additions and 757 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2004-07-02 Thomas Martinez <martinez@src.lip6.fr>
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/reductgba_sim_del.cc: Remove some comments.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/reductgba.cc: Adjust ...
* src/tgbatest/spotlbtt.test: More test (delayed simulation)
2004-06-29 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-06-29 Alexandre Duret-Lutz <adl@src.lip6.fr>
* configure.ac, NEWS: Bump version to 0.0w. * configure.ac, NEWS: Bump version to 0.0w.

21
src/tgba/tgbareduc.cc
View file

@ -122,7 +122,6 @@ namespace spot
if (!scc_computed_) if (!scc_computed_)
this->compute_scc(); this->compute_scc();
this->prune_acc(); this->prune_acc();
// FIXME
this->delete_scc(); this->delete_scc();
} }
@ -144,26 +143,6 @@ namespace spot
return i->second; return i->second;
} }
int
tgba_reduc::get_nb_state()
{
return state_name_map_.size();
}
int
tgba_reduc::get_nb_transition()
{
int nb_transition = 0;
sn_map::iterator i;
for (i = state_name_map_.begin();
i != state_name_map_.end(); ++i)
{
nb_transition += (i->first)->size();
}
return nb_transition;
}
//////////////////////////////////////////// ////////////////////////////////////////////
void void

6
src/tgba/tgbareduc.hh
View file

@ -64,11 +64,7 @@ namespace spot
/// Add the SCC index to the display of the state \a state. /// Add the SCC index to the display of the state \a state.
virtual std::string format_state(const spot::state* state) const; virtual std::string format_state(const spot::state* state) const;
/// Obsolete. // For Debug
int get_nb_state();
int get_nb_transition();
// Just for Debug !!
void display_rel_sim(simulation_relation* rel, std::ostream& os); void display_rel_sim(simulation_relation* rel, std::ostream& os);
void display_scc(std::ostream& os); void display_scc(std::ostream& os);

273
src/tgbaalgos/reductgba_sim.cc
View file

@ -50,7 +50,6 @@ namespace spot
bool bool
spoiler_node::add_succ(spoiler_node* n) spoiler_node::add_succ(spoiler_node* n)
{ {
//std::cout << "spoiler_node::add_succ" << std::endl;
bool exist = false; bool exist = false;
for (sn_v::iterator i = lnode_succ->begin(); for (sn_v::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i) i != lnode_succ->end(); ++i)
@ -84,15 +83,6 @@ namespace spot
spoiler_node::add_pred(spoiler_node* n) spoiler_node::add_pred(spoiler_node* n)
{ {
lnode_pred->push_back(n); lnode_pred->push_back(n);
/*
bool exist = false;
for (sn_v::iterator i = lnode_pred->begin();
i != lnode_pred->end(); ++i)
if ((*i)->compare(n) == 0)
exist = true;
if (!exist)
lnode_pred->push_back(n);
*/
} }
void void
@ -120,25 +110,10 @@ namespace spot
return change != not_win; return change != not_win;
} }
/*
bool
spoiler_node::set_win()
{
bool change = not_win;
for (Sgi::vector<spoiler_node*>::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i)
{
not_win |= (*i)->not_win;
}
return change != not_win;
}
*/
std::string std::string
spoiler_node::to_string(const tgba* a) spoiler_node::to_string(const tgba* a)
{ {
std::ostringstream os; std::ostringstream os;
// print the node.
os << num_ os << num_
<< " [shape=box, label=\"(" << " [shape=box, label=\"("
<< a->format_state(sc_->first) << a->format_state(sc_->first)
@ -164,7 +139,6 @@ namespace spot
bool bool
spoiler_node::compare(spoiler_node* n) spoiler_node::compare(spoiler_node* n)
{ {
//std::cout << "spoiler_node::compare" << std::endl;
return (((sc_->first)->compare((n->get_pair())->first) == 0) && return (((sc_->first)->compare((n->get_pair())->first) == 0) &&
((sc_->second)->compare((n->get_pair())->second) == 0)); ((sc_->second)->compare((n->get_pair())->second) == 0));
} }
@ -235,34 +209,10 @@ namespace spot
return change != not_win; return change != not_win;
} }
/*
bool
duplicator_node::set_win()
{
bool change = not_win;
if (!this->get_nb_succ())
not_win = true;
else
{
not_win = true;
for (Sgi::vector<spoiler_node*>::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i)
{
not_win &= (*i)->not_win;
}
}
return change != not_win;
}
*/
std::string std::string
duplicator_node::to_string(const tgba* a) duplicator_node::to_string(const tgba* a)
{ {
std::ostringstream os; std::ostringstream os;
// print the node.
os << num_ os << num_
<< " [shape=box, label=\"(" << " [shape=box, label=\"("
<< a->format_state(sc_->first) << a->format_state(sc_->first)
@ -274,14 +224,12 @@ namespace spot
bdd_print_acc(os, a->get_dict(), acc_); bdd_print_acc(os, a->get_dict(), acc_);
os << ")\"]" os << ")\"]"
<< std::endl; << std::endl;
return os.str(); return os.str();
} }
bool bool
duplicator_node::compare(spoiler_node* n) duplicator_node::compare(spoiler_node* n)
{ {
//std::cout << "duplicator_node::compare" << std::endl;
return (this->spoiler_node::compare(n) && return (this->spoiler_node::compare(n) &&
(label_ == dynamic_cast<duplicator_node*>(n)->get_label()) && (label_ == dynamic_cast<duplicator_node*>(n)->get_label()) &&
(acc_ == dynamic_cast<duplicator_node*>(n)->get_acc())); (acc_ == dynamic_cast<duplicator_node*>(n)->get_acc()));
@ -591,216 +539,6 @@ namespace spot
} }
} }
/*
void
parity_game_graph_direct::build_couple()
{
// 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;
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)
build_recurse_successor_spoiler(*j, os);
}
void
parity_game_graph_direct::
build_recurse_successor_spoiler(spoiler_node* sn,
std::ostringstream& os)
{
//std::cout << os.str() << "build_recurse_successor_spoiler : begin"
//<< std::endl;
tgba_succ_iterator* si = automata_->succ_iter(sn->get_spoiler_node());
for (si->first(); !si->done(); si->next())
{
bdd btmp = 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)
{
delete s;
duplicator_node* dn
= add_duplicator_node(*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
delete s;
}
}
delete si;
//std::cout << os.str() << "build_recurse_successor_spoiler : end" <<
//std::endl;
}
void
parity_game_graph_direct::
build_recurse_successor_duplicator(duplicator_node* dn,
spoiler_node* ,
std::ostringstream& os)
{
//std::cout << "build_recurse_successor_duplicator : begin" << std::endl;
tgba_succ_iterator* si = automata_->succ_iter(dn->get_duplicator_node());
for (si->first(); !si->done(); si->next())
{
// if si->current_condition() doesn't implies sn->get_label()
// then duplicator can't play.
if ((!dn->get_label() | si->current_condition()) != 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)
{
delete s;
spoiler_node* sn_n
= add_spoiler_node(dn->get_spoiler_node(),
*i1,
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
delete s;
}
}
delete si;
//std::cout << os.str() << "build_recurse_successor_duplicator : end"
//<< std::endl;
}
duplicator_node*
parity_game_graph_direct::add_duplicator_node(const spot::state* sn,
const spot::state* dn,
bdd acc,
bdd label,
int nb)
{
bool exist = false;
duplicator_node* dn_n
= new duplicator_node(sn, dn, acc, label, nb);
for (Sgi::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 = *i;
break;
}
}
if (!exist)
duplicator_vertice_.push_back(dn_n);
return dn_n;
}
spoiler_node*
parity_game_graph_direct::add_spoiler_node(const spot::state* sn,
const spot::state* dn,
int nb)
{
bool exist = false;
spoiler_node* sn_n
= new spoiler_node(sn, dn, nb);
for (Sgi::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 = *i;
break;
}
}
if (!exist)
spoiler_vertice_.push_back(sn_n);
return sn_n;
}
*/
/*
void
parity_game_graph_direct::lift()
{
for (Sgi::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i)
{
(*i)->set_win();
}
}
*/
void void
parity_game_graph_direct::lift() parity_game_graph_direct::lift()
{ {
@ -874,12 +612,14 @@ namespace spot
/////////////////////////////////////////////////////////////////////// ///////////////////////////////////////////////////////////////////////
simulation_relation* simulation_relation*
get_direct_relation_simulation(const tgba* f, int opt) get_direct_relation_simulation(const tgba* f,
std::ostream& os,
int opt)
{ {
parity_game_graph_direct* G = new parity_game_graph_direct(f); parity_game_graph_direct* G = new parity_game_graph_direct(f);
simulation_relation* rel = G->get_relation(); simulation_relation* rel = G->get_relation();
if (opt == 1) if (opt == 1)
G->print(std::cout); G->print(os);
delete G; delete G;
return rel; return rel;
} }
@ -931,7 +671,7 @@ namespace spot
if (opt & Reduce_Dir_Sim) if (opt & Reduce_Dir_Sim)
{ {
simulation_relation* rel simulation_relation* rel
= get_direct_relation_simulation(automatareduc); = get_direct_relation_simulation(automatareduc, std::cout);
automatareduc->display_rel_sim(rel, std::cout); automatareduc->display_rel_sim(rel, std::cout);
automatareduc->prune_automata(rel); automatareduc->prune_automata(rel);
@ -942,7 +682,7 @@ namespace spot
if (opt & Reduce_Del_Sim) if (opt & Reduce_Del_Sim)
{ {
simulation_relation* rel simulation_relation* rel
= get_delayed_relation_simulation(automatareduc); = get_delayed_relation_simulation(automatareduc, std::cout);
automatareduc->display_rel_sim(rel, std::cout); automatareduc->display_rel_sim(rel, std::cout);
automatareduc->prune_automata(rel); automatareduc->prune_automata(rel);
@ -952,7 +692,6 @@ namespace spot
if (opt & Reduce_Scc) if (opt & Reduce_Scc)
{ {
automatareduc->compute_scc();
automatareduc->prune_scc(); automatareduc->prune_scc();
} }

63
src/tgbaalgos/reductgba_sim.hh
View file

@ -58,21 +58,19 @@ namespace spot
/// \brief Compute a direct simulation relation on state of tgba \a f. /// \brief Compute a direct simulation relation on state of tgba \a f.
simulation_relation* get_direct_relation_simulation(const tgba* a, simulation_relation* get_direct_relation_simulation(const tgba* a,
std::ostream& os,
int opt = -1); int opt = -1);
/// Compute a delayed simulation relation on state of tgba \a f. /// Compute a delayed simulation relation on state of tgba \a f.
/// FIXME : this method is incorrect !! // FIXME: This method is correct but she build sometime (when there are more
/// Don't use it !! // than one acceptance condition) only a part of the simulation relation.
simulation_relation* get_delayed_relation_simulation(const tgba* a, simulation_relation* get_delayed_relation_simulation(const tgba* a,
std::ostream& os,
int opt = -1); int opt = -1);
/// To free a simulation relation. /// To free a simulation relation.
void free_relation_simulation(simulation_relation* rel); void free_relation_simulation(simulation_relation* rel);
/// Test if the initial state of a2 fair simulate this of a1.
/// Not implemented.
bool is_include(const tgba* a1, const tgba* a2);
/////////////////////////////////////////////////////////////////////// ///////////////////////////////////////////////////////////////////////
// simulation. // simulation.
@ -108,11 +106,6 @@ namespace spot
/// \brief Compute each node of the graph. /// \brief Compute each node of the graph.
virtual void build_graph() = 0; virtual void build_graph() = 0;
/// \brief Compute the link of the graph.
/// Successor of spoiler node (resp. duplicator node)
/// are duplicator node (resp. spoiler node).
//virtual void build_link() = 0;
/// \brief Remove edge from spoiler to duplicator that make /// \brief Remove edge from spoiler to duplicator that make
/// duplicator loose. /// duplicator loose.
/// Spoiler node whose still have some link, reveal /// Spoiler node whose still have some link, reveal
@ -156,7 +149,6 @@ namespace spot
protected: protected:
sn_v* lnode_succ; sn_v* lnode_succ;
sn_v* lnode_pred; sn_v* lnode_pred;
//Sgi::vector<spoiler_node*>* lnode_succ;
state_couple* sc_; state_couple* sc_;
}; };
@ -200,23 +192,6 @@ namespace spot
virtual void lift(); virtual void lift();
void build_link(); void build_link();
/*
private:
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);
duplicator_node* add_duplicator_node(const spot::state* sn,
const spot::state* dn,
bdd acc,
bdd label,
int nb);
spoiler_node* add_spoiler_node(const spot::state* sn,
const spot::state* dn,
int nb);
*/
}; };
@ -230,8 +205,7 @@ namespace spot
spoiler_node_delayed(const state* d_node, spoiler_node_delayed(const state* d_node,
const state* s_node, const state* s_node,
bdd a, bdd a,
int num, int num);
bool l2a = true);
~spoiler_node_delayed(); ~spoiler_node_delayed();
/// Return true if the progress_measure has changed. /// Return true if the progress_measure has changed.
@ -242,16 +216,16 @@ namespace spot
int get_progress_measure() const; int get_progress_measure() const;
bool get_lead_2_acc_all(); bool get_lead_2_acc_all();
/* bool set_lead_2_acc_all(bdd acc = bddfalse);
void set_lead_2_acc_all();
*/ //
bool seen_;
protected: protected:
/// a Bdd for retain all the acceptance condition /// a Bdd for retain all the acceptance condition
/// that a node has visited. /// that a node has visited.
bdd acceptance_condition_visited_; bdd acceptance_condition_visited_;
int progress_measure_; int progress_measure_;
bool lead_2_acc_all_; bool lead_2_acc_all_;
}; };
/// Duplicator node of parity game graph for delayed simulation. /// Duplicator node of parity game graph for delayed simulation.
@ -271,9 +245,12 @@ namespace spot
bool implies_label(bdd l); bool implies_label(bdd l);
bool implies_acc(bdd a); bool implies_acc(bdd a);
int get_progress_measure(); int get_progress_measure();
bool get_lead_2_acc_all();
void set_lead_2_acc_all();
bool get_lead_2_acc_all();
bool set_lead_2_acc_all(bdd acc = bddfalse);
//
bool seen_;
protected: protected:
int progress_measure_; int progress_measure_;
bool lead_2_acc_all_; bool lead_2_acc_all_;
@ -316,9 +293,6 @@ namespace spot
/// Return the number of acceptance condition. /// Return the number of acceptance condition.
int nb_set_acc_cond(); int nb_set_acc_cond();
/// Compute sub_set_acc_cond_;
void build_sub_set_acc_cond();
/// ///
duplicator_node_delayed* add_duplicator_node_delayed(const spot::state* sn, duplicator_node_delayed* add_duplicator_node_delayed(const spot::state* sn,
const spot::state* dn, const spot::state* dn,
@ -332,21 +306,18 @@ namespace spot
bdd acc, bdd acc,
int nb); int nb);
/// \brief Compute the couple as for direct simulation,
virtual void build_graph();
//virtual void build_link();
void build_recurse_successor_spoiler(spoiler_node* sn, void build_recurse_successor_spoiler(spoiler_node* sn,
std::ostringstream& os); std::ostringstream& os);
void build_recurse_successor_duplicator(duplicator_node* dn, void build_recurse_successor_duplicator(duplicator_node* dn,
spoiler_node* sn, spoiler_node* sn,
std::ostringstream& os); std::ostringstream& os);
/// \brief Compute the couple as for direct simulation,
virtual void build_graph();
/// \brief The Jurdzinski's lifting algorithm. /// \brief The Jurdzinski's lifting algorithm.
virtual void lift(); virtual void lift();
/// \brief Remove all node so as to there is no dead ends (terminal node).
//virtual void prune();
}; };
} }

521
src/tgbaalgos/reductgba_sim_del.cc
View file

@ -33,7 +33,13 @@ namespace spot
static int nb_spoiler; static int nb_spoiler;
static int nb_duplicator; static int nb_duplicator;
//static int nb_node; static bdd all_acc_cond = bddfalse;
static Sgi::vector<bool*> bool_v;
//static int nb_node = 0;
//seen_map_node seen_node_;
/////////////////////////////////////////////////////////////////////// ///////////////////////////////////////////////////////////////////////
// spoiler_node_delayed // spoiler_node_delayed
@ -41,8 +47,7 @@ namespace spot
spoiler_node_delayed::spoiler_node_delayed(const state* d_node, spoiler_node_delayed::spoiler_node_delayed(const state* d_node,
const state* s_node, const state* s_node,
bdd a, bdd a,
int num, int num)
bool l2a)
: spoiler_node(d_node, s_node, num), : spoiler_node(d_node, s_node, num),
acceptance_condition_visited_(a) acceptance_condition_visited_(a)
{ {
@ -50,7 +55,11 @@ namespace spot
progress_measure_ = 0; progress_measure_ = 0;
if (acceptance_condition_visited_ != bddfalse) if (acceptance_condition_visited_ != bddfalse)
nb_spoiler_loose_++; nb_spoiler_loose_++;
lead_2_acc_all_ = l2a; lead_2_acc_all_ = false;
seen_ = false;
//seen_ = new bool(false);
//bool_v[nb_node++] = seen_;
} }
spoiler_node_delayed::~spoiler_node_delayed() spoiler_node_delayed::~spoiler_node_delayed()
@ -76,11 +85,14 @@ namespace spot
bool change; bool change;
int tmpmax = 0; int tmpmax = 0;
int tmp = 0; int tmp = 0;
int tmpmaxwin = -1;
sn_v::iterator i = lnode_succ->begin(); sn_v::iterator i = lnode_succ->begin();
if (i != lnode_succ->end()) if (i != lnode_succ->end())
{ {
tmpmax = tmpmax =
dynamic_cast<duplicator_node_delayed*>(*i)->get_progress_measure(); dynamic_cast<duplicator_node_delayed*>(*i)->get_progress_measure();
if (dynamic_cast<duplicator_node_delayed*>(*i)->get_lead_2_acc_all())
tmpmaxwin = tmpmax;
++i; ++i;
} }
for (; i != lnode_succ->end(); ++i) for (; i != lnode_succ->end(); ++i)
@ -89,8 +101,14 @@ namespace spot
dynamic_cast<duplicator_node_delayed*>(*i)->get_progress_measure(); dynamic_cast<duplicator_node_delayed*>(*i)->get_progress_measure();
if (tmp > tmpmax) if (tmp > tmpmax)
tmpmax = tmp; tmpmax = tmp;
if (dynamic_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 // If the priority of the node is 1
// acceptance_condition_visited_ != bddfalse // acceptance_condition_visited_ != bddfalse
// then we increment the progress measure of 1. // then we increment the progress measure of 1.
@ -136,8 +154,12 @@ namespace spot
os << "ACC"; os << "ACC";
} }
os << ")" os << ")"
<< " pm = " << progress_measure_ << "\"]" << " pm = " << progress_measure_;
<< std::endl; if (lead_2_acc_all_)
os << ", 1\"]";
else
os << ", 0\"]";
os << std::endl;
return os.str(); return os.str();
} }
@ -161,15 +183,31 @@ namespace spot
bool bool
spoiler_node_delayed::get_lead_2_acc_all() spoiler_node_delayed::get_lead_2_acc_all()
{ {
//std::cout << "spoiler_node_delayed::get_lead_2_acc_all" << std::endl;
return lead_2_acc_all_; return lead_2_acc_all_;
} }
/*
void bool
spoiler_node_delayed::set_lead_2_acc_all() spoiler_node_delayed::set_lead_2_acc_all(bdd acc)
{ {
//std::cout << "spoiler_node_delayed::set_lead_2_acc_all" << std::endl;
if (!seen_)
{
seen_ = true;
for (sn_v::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i)
dynamic_cast<duplicator_node_delayed*>(*i)->set_lead_2_acc_all(acc);
} }
*/ else
{
//seen_ = true;
if (acc == all_acc_cond)
lead_2_acc_all_ = true;
}
return lead_2_acc_all_;
}
/////////////////////////////////////////////////////////////////////// ///////////////////////////////////////////////////////////////////////
// duplicator_node_delayed // duplicator_node_delayed
@ -183,6 +221,13 @@ namespace spot
{ {
nb_duplicator++; nb_duplicator++;
progress_measure_ = 0; progress_measure_ = 0;
all_acc_cond |= a;
lead_2_acc_all_ = false;
seen_ = false;
//seen_ = new bool(false);
//bool_v[nb_node++] = seen_;
} }
duplicator_node_delayed::~duplicator_node_delayed() duplicator_node_delayed::~duplicator_node_delayed()
@ -239,8 +284,12 @@ namespace spot
//<< ", "; //<< ", ";
//bdd_print_acc(os, a->get_dict(), acc_); //bdd_print_acc(os, a->get_dict(), acc_);
os << ")" os << ")"
<< " pm = " << progress_measure_ << "\"]" << " pm = " << progress_measure_;
<< std::endl; if (lead_2_acc_all_)
os << ", 1\"]";
else
os << ", 0\"]";
os << std::endl;
return os.str(); return os.str();
} }
@ -266,17 +315,24 @@ namespace spot
bool bool
duplicator_node_delayed::get_lead_2_acc_all() duplicator_node_delayed::get_lead_2_acc_all()
{ {
//std::cout << "duplicator_node_delayed::get_lead_2_acc_all" << std::endl;
return lead_2_acc_all_; return lead_2_acc_all_;
} }
void bool
duplicator_node_delayed::set_lead_2_acc_all() duplicator_node_delayed::set_lead_2_acc_all(bdd acc)
{ {
if (!lead_2_acc_all_) //std::cout << "duplicator_node_delayed::set_lead_2_acc_all" << std::endl;
acc |= acc_;
if (!seen_)
{
seen_ = true;
for (sn_v::iterator i = lnode_succ->begin(); for (sn_v::iterator i = lnode_succ->begin();
i != lnode_succ->end(); ++i) i != lnode_succ->end(); ++i)
lead_2_acc_all_ lead_2_acc_all_
|= dynamic_cast<spoiler_node_delayed*>(*i)->get_lead_2_acc_all(); |= dynamic_cast<spoiler_node_delayed*>(*i)->set_lead_2_acc_all(acc);
}
return lead_2_acc_all_;
} }
/////////////////////////////////////////////////////////////////////// ///////////////////////////////////////////////////////////////////////
@ -297,252 +353,6 @@ namespace spot
return count; return count;
} }
void
parity_game_graph_delayed::build_sub_set_acc_cond()
{
// compute the number of acceptance conditions
bdd acc, all;
acc = all = automata_->all_acceptance_conditions();
int count = 0;
while (all != bddfalse)
{
//std::cout << "add acc" << std::endl;
sub_set_acc_cond_.push_back(bdd_satone(all));
all -= bdd_satone(all);
count++;
}
// sub_set_acc_cond_ contains all the acceptance condition.
// but we must have all the sub-set of acceptance condition.
// In fact we must have 2^count sub-set.
if (count == 2)
{
sub_set_acc_cond_.push_back(acc);
sub_set_acc_cond_.push_back(bddfalse);
}
/*
bdd_v::iterator i;
bdd_v::iterator j;
for (i = sub_set_acc_cond_.begin(); i != sub_set_acc_cond_.end(); ++i)
for (j = sub_set_acc_cond_.begin(); j != sub_set_acc_cond_.end(); ++j)
sub_set_acc_cond_.push_back(*i | *j);
std::cout << std::endl;
for (i = sub_set_acc_cond_.begin(); i != sub_set_acc_cond_.end();)
{
bdd_print_acc(std::cout, automata_->get_dict(), *i);
std::cout << " // " << std::endl;
++i;
}
std::cout << std::endl;
*/
}
/*
void
parity_game_graph_delayed::build_couple()
{
//std::cout << "build couple" << std::endl;
nb_spoiler = 0;
nb_duplicator = 0;
tgba_succ_iterator* si = 0;
typedef Sgi::pair<bdd, bdd> couple_bdd;
couple_bdd *p = 0;
Sgi::vector<couple_bdd*>* trans = 0;
bool exist = false;
spot::state* s = 0;
s_v::iterator i;
for (i = tgba_state_.begin(); i != tgba_state_.end(); ++i)
{
// for each sub-set of the set of acceptance condition.
bdd_v::iterator i2;
for (i2 = sub_set_acc_cond_.begin();
i2 != sub_set_acc_cond_.end(); ++i2)
{
// spoiler node are all state couple (i,j)
// multiply by 2^(|F|)
s_v::iterator i3;
for (i3 = tgba_state_.begin();
i3 != tgba_state_.end(); ++i3)
{
//nb_spoiler++;
spoiler_node_delayed* n1
= new spoiler_node_delayed(*i,
*i3,
*i2,
nb_node_parity_game++);
spoiler_vertice_.push_back(n1);
}
// duplicator node are all state couple where
// the first state i are reachable.
trans = new Sgi::vector<couple_bdd*>;
for (i3 = tgba_state_.begin();
i3 != tgba_state_.end(); ++i3)
{
si = automata_->succ_iter(*i3);
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;
Sgi::vector<couple_bdd*>::iterator i4;
for (i4 = trans->begin();
i4 != trans->end(); ++i4)
{
if ((si->current_condition() == (*i4)->first))
// We don't need the acceptance condition
//&&
//(si->current_acceptance_conditions()
//== (*i4)->second))
exist = true;
}
if (!exist)
{
// We build all the state couple with the label p.
// multiply by 2^(|F|)
trans->push_back(p);
Sgi::vector<const state*>::iterator i5;
for (i5 = tgba_state_.begin();
i5 != tgba_state_.end(); ++i5)
{
//nb_duplicator++;
int nb = nb_node_parity_game++;
duplicator_node_delayed* n2
= new
duplicator_node_delayed(*i,
*i5,
si->
current_condition(),
*i2,
nb);
duplicator_vertice_.push_back(n2);
}
}
else
delete p;
}
delete s;
}
delete si;
}
Sgi::vector<couple_bdd*>::iterator i6;
for (i6 = trans->begin(); i6 != trans->end(); ++i6)
{
delete *i6;
}
delete trans;
}
}
nb_spoiler_loose_++;
//std::cout << "spoiler node : " << nb_spoiler << std::endl;
//std::cout << "duplicator node : " << nb_duplicator << std::endl;
//std::cout << "nb_spoiler_loose_ : " << nb_spoiler_loose_ << std::endl;
}
void
parity_game_graph_delayed::build_link()
{
//std::cout << "build link" << std::endl;
int nb_ds = 0;
int nb_sd = 0;
spot::state* s = 0;
// for each couple of (spoiler, duplicator)
sn_v::iterator i;
for (i = spoiler_vertice_.begin(); i != spoiler_vertice_.end(); ++i)
{
dn_v::iterator i2;
for (i2 = duplicator_vertice_.begin();
i2 != duplicator_vertice_.end(); ++i2)
{
// We add a link between a duplicator and a spoiler.
if ((*i2)->get_spoiler_node()->compare((*i)
->get_spoiler_node()) == 0)
{
tgba_succ_iterator* si
= automata_->succ_iter((*i2)->get_duplicator_node());
for (si->first(); !si->done(); si->next())
{
s = si->current_state();
bdd btmp2 = dynamic_cast<spoiler_node_delayed*>(*i)->
get_acceptance_condition_visited();
bdd btmp = btmp2 - si->current_acceptance_conditions();
//if ((s->compare((*i)->get_duplicator_node()) == 0) &&
//dynamic_cast<duplicator_node_delayed*>(*i2)->
// implies_label(si->current_condition()) &&
//(btmp == btmp2))
if ((s->compare((*i)->get_duplicator_node()) == 0) &&
dynamic_cast<duplicator_node_delayed*>(*i2)->
implies_label(si->current_condition()) &&
(dynamic_cast<spoiler_node_delayed*>(*i)->
get_acceptance_condition_visited() != bddfalse))
{
//std::cout << "add duplicator -> spoiler" << std::endl;
(*i2)->add_succ(*i);
(*i)->add_pred(*i2);
nb_ds++;
}
delete s;
}
delete si;
}
// We add a link between a spoiler and a duplicator.
if ((*i2)->get_duplicator_node()
->compare((*i)->get_duplicator_node()) == 0)
{
tgba_succ_iterator* si
= automata_->succ_iter((*i)->get_spoiler_node());
for (si->first(); !si->done(); si->next())
{
s = si->current_state();
bdd btmp = si->current_acceptance_conditions() |
dynamic_cast<spoiler_node_delayed*>(*i)->
get_acceptance_condition_visited();
if ((s->compare((*i2)->get_spoiler_node()) == 0) &&
(*i2)->match(si->current_condition(), btmp))
{
//std::cout << "add spoiler -> duplicator" << std::endl;
(*i)->add_succ(*i2);
(*i2)->add_pred(*i);
nb_sd++;
}
delete s;
}
delete si;
}
}
}
}
*/
// We build only node which are reachable // We build only node which are reachable
void void
parity_game_graph_delayed::build_graph() parity_game_graph_delayed::build_graph()
@ -577,16 +387,6 @@ namespace spot
// The acc of the duplicator must contains the // The acc of the duplicator must contains the
// acceptance_condition_visited_ of the spoiler. // acceptance_condition_visited_ of the spoiler.
//std::cout << "build_link : iter " << ++n << std::endl; //std::cout << "build_link : iter " << ++n << std::endl;
/*
std::cout << "["
<< automata_->format_state((*j)->get_spoiler_node())
<< "] // ["
<< automata_->format_state((*j)->get_duplicator_node())
<< "]"
<< std::endl;
*/
build_recurse_successor_spoiler(*j, os); build_recurse_successor_spoiler(*j, os);
} }
@ -615,25 +415,6 @@ namespace spot
dynamic_cast<spoiler_node_delayed*>(sn)-> dynamic_cast<spoiler_node_delayed*>(sn)->
get_acceptance_condition_visited(); get_acceptance_condition_visited();
// If the spoiler node has witnessed an accepting condition,
// so we force to play on an arc which have a different accepting
// condition. => FALSE !!!!!!
/*
if ((dynamic_cast<spoiler_node_delayed*>(sn)->
get_acceptance_condition_visited() ==
si->current_acceptance_conditions()) &&
(si->current_acceptance_conditions() != bddfalse))
continue;
*/
/*
if (btmp == bddfalse)
std::cout << "btmp == bddfasle" << std::endl;
else
std::cout << "btmp != bddfasle" << std::endl;
*/
s_v::iterator i1; s_v::iterator i1;
state* s; state* s;
for (i1 = tgba_state_.begin(); for (i1 = tgba_state_.begin();
@ -675,23 +456,46 @@ namespace spot
spoiler_node* , spoiler_node* ,
std::ostringstream& os) std::ostringstream& os)
{ {
//std::cout << "build_recurse_successor_duplicator : begin" << std::endl; /*
std::cout << os.str() << "build_recurse_successor_duplicator : begin"
<< std::endl;
*/
tgba_succ_iterator* si = automata_->succ_iter(dn->get_duplicator_node()); tgba_succ_iterator* si = automata_->succ_iter(dn->get_duplicator_node());
for (si->first(); !si->done(); si->next()) for (si->first(); !si->done(); si->next())
{ {
// if si->current_condition() doesn't implies sn->get_label()
// then duplicator can't play.
if ((!dn->get_label() | si->current_condition()) != bddtrue)
continue;
// FIXME
/* /*
bdd btmp = dn->get_acc(); std::cout << automata_->format_state(dn->get_spoiler_node())
bdd btmp2 = btmp - (btmp & si->current_acceptance_conditions()); << std::endl;
std::cout << automata_->format_state(dn->get_duplicator_node())
<< std::endl;
*/ */
/*
bdd_print_acc(std::cout,
automata_->get_dict(),
si->current_condition());
std::cout << " // ";
bdd_print_acc(std::cout,
automata_->get_dict(),
dn->get_label());
std::cout << " // ";
bdd_print_acc(std::cout,
automata_->get_dict(),
si->current_condition() | !dn->get_label());
std::cout << std::endl;
*/
// if si->current_condition() doesn't implies dn->get_label()
// then duplicator can't play.
if ((si->current_condition() | !dn->get_label()) != bddtrue)
{
//std::cout << "doesn't implies" << std::endl;
continue;
}
bdd btmp = dn->get_acc() - bdd btmp = dn->get_acc() -
(dn->get_acc() & si->current_acceptance_conditions()); (dn->get_acc() & si->current_acceptance_conditions());
@ -725,8 +529,10 @@ namespace spot
delete si; delete si;
//std::cout << os.str() << "build_recurse_successor_duplicator : end" /*
//<< std::endl; std::cout << os.str() << "build_recurse_successor_duplicator : end"
<< std::endl;
*/
} }
duplicator_node_delayed* duplicator_node_delayed*
@ -770,7 +576,7 @@ namespace spot
//bool l2a = (acc != automata_->all_acceptance_conditions()); //bool l2a = (acc != automata_->all_acceptance_conditions());
spoiler_node_delayed* sn_n spoiler_node_delayed* sn_n
= new spoiler_node_delayed(sn, dn, acc, nb, false); = new spoiler_node_delayed(sn, dn, acc, nb);
for (Sgi::vector<spoiler_node*>::iterator i for (Sgi::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin(); = spoiler_vertice_.begin();
@ -791,79 +597,44 @@ namespace spot
return sn_n; return sn_n;
} }
/*
void
parity_game_graph_delayed::prune()
{
bool change = true;
std::cout << "prune : nb spoiler : "
<< spoiler_vertice_.size()
<< std::endl
<< "prune : nb duplicator : "
<< duplicator_vertice_.size()
<< std::endl;
while (change)
{
std::cout << "prune::change = true" << std::endl;
change = false;
for (Sgi::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin();
i != duplicator_vertice_.end();)
{
if ((*i)->get_nb_succ() == 0)
{
std::cout << "Remove duplicator" << std::endl;
(*i)->del_pred();
delete *i;
i = duplicator_vertice_.erase(i);
change = true;
}
else
++i;
}
for (Sgi::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin();
i != spoiler_vertice_.end();)
{
if ((*i)->get_nb_succ() == 0)
{
std::cout << "Remove spoiler" << std::endl;
(*i)->del_pred();
delete *i;
i = spoiler_vertice_.erase(i);
change = true;
}
else
++i;
}
}
std::cout << "prune::change = false" << std::endl;
std::cout << "prune : nb spoiler : "
<< spoiler_vertice_.size()
<< std::endl
<< "prune : nb duplicator : "
<< duplicator_vertice_.size()
<< std::endl;
}
*/
void void
parity_game_graph_delayed::lift() parity_game_graph_delayed::lift()
{ {
// TEST of the hash_map of node
/*
for (Sgi::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin();
i != duplicator_vertice_.end(); ++i)
seen_node_[*i] = 1;
for (Sgi::vector<spoiler_node*>::iterator i
= spoiler_vertice_.begin();
i != spoiler_vertice_.end(); ++i)
seen_node_[*i] = 1;
*/
//
// Before the lift we compute each vertices // Before the lift we compute each vertices
// to know if he belong to a all accepting cycle // to know if he belong to a all accepting cycle
// of the graph. // of the graph.
/* FIXME
if (this->nb_set_acc_cond() > 1)
for (Sgi::vector<duplicator_node*>::iterator i for (Sgi::vector<duplicator_node*>::iterator i
= duplicator_vertice_.begin(); = duplicator_vertice_.begin();
i != duplicator_vertice_.end(); ++i) i != duplicator_vertice_.end(); ++i)
{ {
if (dynamic_cast<duplicator_node_delayed*>(*i)->get_lead_2_acc_all()) for (Sgi::vector<duplicator_node*>::iterator i2
= duplicator_vertice_.begin();
i2 != duplicator_vertice_.end(); ++i2)
dynamic_cast<duplicator_node_delayed*>(*i2)->seen_ = false;
for (Sgi::vector<spoiler_node*>::iterator i3
= spoiler_vertice_.begin();
i3 != spoiler_vertice_.end(); ++i3)
dynamic_cast<spoiler_node_delayed*>(*i3)->seen_ = false;
dynamic_cast<duplicator_node_delayed*>(*i)->set_lead_2_acc_all(); dynamic_cast<duplicator_node_delayed*>(*i)->set_lead_2_acc_all();
} }
*/
// Jurdzinski's algorithm // Jurdzinski's algorithm
//int iter = 0; //int iter = 0;
@ -937,38 +708,24 @@ namespace spot
return; return;
*/ */
//this->build_sub_set_acc_cond();
//std::cout << "build couple" << std::endl; //std::cout << "build couple" << std::endl;
this->build_graph(); this->build_graph();
//std::cout << "build link" << std::endl; //std::cout << "lift begin : " << nb_spoiler_loose_ << std::endl;
//this->build_link();
//std::cout << "prune" << std::endl;
//this->prune();
std::cout << "lift begin : " << nb_spoiler_loose_ << std::endl;
this->lift(); this->lift();
std::cout << "lift end : " << nb_spoiler_loose_ << std::endl; //std::cout << "lift end : " << nb_spoiler_loose_ << std::endl;
//std::cout << "END" << std::endl; //std::cout << "END" << std::endl;
//this->print(std::cout);
} }
/////////////////////////////////////////// ///////////////////////////////////////////
simulation_relation* simulation_relation*
get_delayed_relation_simulation(const tgba* f, int opt) get_delayed_relation_simulation(const tgba* f, std::ostream& os, int opt)
{ {
/// FIXME : this method is incorrect !!
/// Don't use it !!
parity_game_graph_delayed* G = new parity_game_graph_delayed(f); parity_game_graph_delayed* G = new parity_game_graph_delayed(f);
simulation_relation* rel = G->get_relation(); simulation_relation* rel = G->get_relation();
if (opt == 1) if (opt == 1)
G->print(std::cout); G->print(os);
delete G; delete G;
return rel; return rel;
/*
return get_direct_relation_simulation(f, opt);
*/
} }
} }

62
src/tgbatest/ltl2tgba.cc
View file

@ -98,6 +98,8 @@ syntax(char* prog)
<< std::endl << std::endl
<< " -Rd to display simulation relation" << " -Rd to display simulation relation"
<< std::endl << std::endl
<< " -RD to display parity game (dot format)"
<< std::endl
<< " -s convert to explicit automata, and number states " << " -s convert to explicit automata, and number states "
<< "in DFS order" << std::endl << "in DFS order" << std::endl
<< " -S convert to explicit automata, and number states " << " -S convert to explicit automata, and number states "
@ -138,6 +140,7 @@ main(int argc, char** argv)
int redopt = spot::ltl::Reduce_None; int redopt = spot::ltl::Reduce_None;
bool display_reduce_form = false; bool display_reduce_form = false;
bool display_rel_sim = false; bool display_rel_sim = false;
bool display_parity_game = false;
bool post_branching = false; bool post_branching = false;
bool fair_loop_approx = false; bool fair_loop_approx = false;
@ -257,6 +260,30 @@ main(int argc, char** argv)
{ {
output = 3; output = 3;
} }
else if (!strcmp(argv[formula_index], "-R1"))
{
reduc_aut |= spot::Reduce_Dir_Sim;
}
else if (!strcmp(argv[formula_index], "-R2"))
{
reduc_aut |= spot::Reduce_Del_Sim;
}
else if (!strcmp(argv[formula_index], "-R3"))
{
reduc_aut |= spot::Reduce_Scc;
}
else if (!strcmp(argv[formula_index], "-rd"))
{
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], "-s")) else if (!strcmp(argv[formula_index], "-s"))
{ {
dupexp = DFS; dupexp = DFS;
@ -291,26 +318,6 @@ main(int argc, char** argv)
fm_opt = true; fm_opt = true;
fm_symb_merge_opt = false; fm_symb_merge_opt = false;
} }
else if (!strcmp(argv[formula_index], "-R1"))
{
reduc_aut |= spot::Reduce_Dir_Sim;
}
else if (!strcmp(argv[formula_index], "-R2"))
{
reduc_aut |= spot::Reduce_Del_Sim;
}
else if (!strcmp(argv[formula_index], "-R3"))
{
reduc_aut |= spot::Reduce_Scc;
}
else if (!strcmp(argv[formula_index], "-rd"))
{
display_reduce_form = true;
}
else if (!strcmp(argv[formula_index], "-Rd"))
{
display_rel_sim = true;
}
else else
{ {
break; break;
@ -399,14 +406,22 @@ main(int argc, char** argv)
if (reduc_aut != spot::Reduce_None) if (reduc_aut != spot::Reduce_None)
{ {
a = aut_red = new spot::tgba_reduc(a); a = aut_red = new spot::tgba_reduc(a);
if (reduc_aut & spot::Reduce_Scc)
aut_red->prune_scc();
if ((reduc_aut & spot::Reduce_Dir_Sim) || if ((reduc_aut & spot::Reduce_Dir_Sim) ||
(reduc_aut & spot::Reduce_Del_Sim)) (reduc_aut & spot::Reduce_Del_Sim))
{ {
spot::simulation_relation* rel; spot::simulation_relation* rel;
if (reduc_aut & spot::Reduce_Dir_Sim) if (reduc_aut & spot::Reduce_Dir_Sim)
rel = spot::get_direct_relation_simulation(a); rel = spot::get_direct_relation_simulation(a,
std::cout,
display_parity_game);
else if (reduc_aut & spot::Reduce_Del_Sim) else if (reduc_aut & spot::Reduce_Del_Sim)
rel = spot::get_delayed_relation_simulation(a); rel = spot::get_delayed_relation_simulation(a,
std::cout,
display_parity_game);
else else
assert(0); assert(0);
@ -422,9 +437,6 @@ main(int argc, char** argv)
spot::free_relation_simulation(rel); spot::free_relation_simulation(rel);
} }
if (reduc_aut & spot::Reduce_Scc)
aut_red->prune_scc();
} }
spot::tgba_explicit* expl = 0; spot::tgba_explicit* expl = 0;

4
src/tgbatest/reductgba.cc
View file

@ -112,12 +112,12 @@ main(int argc, char** argv)
if (o & spot::Reduce_Dir_Sim) if (o & spot::Reduce_Dir_Sim)
{ {
rel = spot::get_direct_relation_simulation(automatareduc); rel = spot::get_direct_relation_simulation(automatareduc, std::cout);
automatareduc->prune_automata(rel); automatareduc->prune_automata(rel);
} }
else if (o & spot::Reduce_Del_Sim) else if (o & spot::Reduce_Del_Sim)
{ {
rel = spot::get_delayed_relation_simulation(automatareduc); rel = spot::get_delayed_relation_simulation(automatareduc, std::cout);
automatareduc->quotient_state(rel); automatareduc->quotient_state(rel);
} }

7
src/tgbatest/spotlbtt.test
View file

@ -98,6 +98,13 @@ Algorithm
Enabled = yes Enabled = yes
} }
Algorithm
{
Name = "Spot (Couvreur -- FM), post reduction with delayed simulation"
Path = "${LBTT_TRANSLATE} --spot './ltl2tgba -R2 -F -f -t'"
Enabled = yes
}
Algorithm Algorithm
{ {
Name = "Spot (Couvreur -- FM), post reduction with scc" Name = "Spot (Couvreur -- FM), post reduction with scc"