diff --git a/ChangeLog b/ChangeLog index d7d44b70d..57161d3fe 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2004-10-28 Alexandre Duret-Lutz + + * src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh: New files. + Cannot test them because the run returned by the emptiness checks + are currently incomplete (they lack the acceptance conditions, and + sometimes even the labels in the prefix). + * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, + libtgbaalgos_la_SOURCES): Add them. + * src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run + when the emptiness checks are fixed. + 2004-10-27 Alexandre Duret-Lutz Introduce an emptiness-check interface, and modify the existing diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 5d623cb0a..0971e76e8 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -37,6 +37,7 @@ tgbaalgos_HEADERS = \ neverclaim.hh \ powerset.hh \ reachiter.hh \ + replayrun.hh \ save.hh \ stats.hh \ reductgba_sim.hh @@ -53,6 +54,7 @@ libtgbaalgos_la_SOURCES = \ neverclaim.cc \ powerset.cc \ reachiter.cc \ + replayrun.cc \ save.cc \ stats.cc \ reductgba_sim.cc \ diff --git a/src/tgbaalgos/replayrun.cc b/src/tgbaalgos/replayrun.cc new file mode 100644 index 000000000..583266cdb --- /dev/null +++ b/src/tgbaalgos/replayrun.cc @@ -0,0 +1,124 @@ +// Copyright (C) 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. + +#include "replayrun.hh" +#include "tgba/tgba.hh" +#include "emptiness.hh" + +namespace spot +{ + bool + replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run) + { + const state* s = a->get_init_state(); + int serial = 1; + const tgba_run::steps* l; + std::string in; + + if (run->prefix.empty()) + { + l = &run->cycle; + in = "cycle"; + } + else + { + l = &run->prefix; + in = "prefix"; + } + + tgba_run::steps::const_iterator i = l->begin(); + + if (s->compare(i->s)) + { + os << "ERROR: First state of run (in " << in << "): " + << a->format_state(i->s) << std::endl + << "does not match initial state of automata: " + << a->format_state(s) << std::endl; + delete s; + return false; + } + + for (;;) // process the prefix then the cycle + { + for (; i != l->end(); ++serial) + { + os << "state " << serial << " in " << in << ": " + << a->format_state(s) << std::endl; + + // expected outgoing transition + bdd label = i->label; + bdd acc = i->acc; + + // compute the next expected state + const state* next; + ++i; + if (i != l->end()) + next = i->s; + else + next = l->begin()->s; + + // browse the actual outgoing transition + tgba_succ_iterator* j = a->succ_iter(s); + delete s; + for (j->first(); !j->done(); j->next()) + { + if (j->current_condition() != label + || j->current_acceptance_conditions() != acc) + continue; + + const state* s2 = j->current_state(); + if (s2->compare(next)) + { + delete s2; + continue; + } + else + { + delete s; + s = s2; + break; + } + } + if (j->done()) + { + os << "ERROR: no transition with label=" << label + << " and acc=" << acc << " leaving state " << serial + << std::endl; + delete j; + return false; + } + os << "transition with label=" << label + << " and acc=" << acc << " found" << std::endl; + delete j; + } + if (l == &run->prefix) + { + l = &run->cycle; + in = "cycle"; + } + else + { + break; + } + } + return true; + } +} diff --git a/src/tgbaalgos/replayrun.hh b/src/tgbaalgos/replayrun.hh new file mode 100644 index 000000000..62e3cdaec --- /dev/null +++ b/src/tgbaalgos/replayrun.hh @@ -0,0 +1,41 @@ +// Copyright (C) 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. + +#ifndef SPOT_TGBAALGOS_REPLAYRUN_HH +# define SPOT_TGBAALGOS_REPLAYRUN_HH + +#include + +namespace spot +{ + struct tgba_run; + class tgba; + + /// \brief Replay a tgba_run on a tgba. + /// + /// \param run the run to replay + /// \param a the automata on which to replay that run + /// \param os the stream on which the replay should be traced + /// \return true iff the run could be completed + bool replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run); +} + +#endif // SPOT_TGBAALGOS_REPLAYRUN_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 0c9e9c7ca..b537e6468 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -42,6 +42,7 @@ #include "tgbaalgos/dupexp.hh" #include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/reductgba_sim.hh" +#include "tgbaalgos/replayrun.hh" void syntax(char* prog) @@ -575,11 +576,13 @@ main(int argc, char** argv) spot::tgba_run* run = res->accepting_run(); if (!run) { - std::cout << "an accepting run exist" << std::endl; + std::cout << "an accepting run exists" << std::endl; } else { spot::print_tgba_run(std::cout, run, ec_a); + // if (!spot::replay_tgba_run(std::cout, ec_a, run)) + // exit_code = 1; delete run; } }