diff --git a/NEWS b/NEWS index b10103d37..06c50dfb5 100644 --- a/NEWS +++ b/NEWS @@ -44,7 +44,7 @@ New in spot 1.99.4a (not yet released) looks like a subversion of v1 and no parse error was detected. * The way to pass option to the automaton parser has been changed to - make it easier to introduct new options. One such new option is + make it easier to introduce new options. One such new option is "trust_hoa": when true (the default) supported properties declared in HOA files are trusted even if they cannot be easily be verified. @@ -53,6 +53,10 @@ New in spot 1.99.4a (not yet released) tgba_statistics::transitions -> twa_statistics::edges tgba_sub_statistics::sub_transitions -> twa_sub_statistics::transitions tgba_run -> twa_run + reduce_run -> twa_run::reduce + replay_twa_run -> twa_run::replay + print_twa_run -> operator<< + twa_run_to_tgba -> twa_run::as_twa Python: diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc index 0375c88c3..3c003912f 100644 --- a/iface/ltsmin/modelcheck.cc +++ b/iface/ltsmin/modelcheck.cc @@ -23,7 +23,6 @@ #include "tl/parse.hh" #include "twaalgos/translate.hh" #include "twaalgos/emptiness.hh" -#include "twaalgos/reducerun.hh" #include "twaalgos/postproc.hh" #include "twa/twaproduct.hh" #include "misc/timer.hh" @@ -336,11 +335,10 @@ checked_main(int argc, char **argv) else { tm.start("reducing accepting run"); - run = spot::reduce_run(res->automaton(), run); + run = run->reduce(); tm.stop("reducing accepting run"); - tm.start("printing accepting run"); - spot::print_twa_run(std::cout, product, run); + std::cout << run; tm.stop("printing accepting run"); } } diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh index d8c8aa647..e3e9be924 100644 --- a/src/bin/common_aoutput.hh +++ b/src/bin/common_aoutput.hh @@ -29,7 +29,6 @@ #include "twaalgos/stats.hh" #include "twaalgos/sccinfo.hh" #include "twaalgos/gtec/gtec.hh" -#include "twaalgos/reducerun.hh" #include "twaalgos/word.hh" #include "twaalgos/isdet.hh" #include "common_file.hh" @@ -179,8 +178,7 @@ public: { auto run = res->accepting_run(); assert(run); - run = reduce_run(run); - spot::tgba_word w(run); + spot::tgba_word w(run->reduce()); w.simplify(); std::ostringstream out; w.print(out, aut->get_dict()); diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 8c557cd3b..38f9107d8 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -52,7 +52,6 @@ #include "twaalgos/randomgraph.hh" #include "twaalgos/sccinfo.hh" #include "twaalgos/isweakscc.hh" -#include "twaalgos/reducerun.hh" #include "twaalgos/word.hh" #include "twaalgos/complement.hh" #include "twaalgos/cleanacc.hh" @@ -703,10 +702,9 @@ namespace auto run = res->accepting_run(); if (run) { - run = reduce_run(run); std::cerr << "; both automata accept the infinite word\n" << " "; - spot::tgba_word w(run); + spot::tgba_word w(run->reduce()); w.simplify(); w.print(example(), prod->get_dict()) << '\n'; } diff --git a/src/tests/emptchk.cc b/src/tests/emptchk.cc index 093722ffc..c50343889 100644 --- a/src/tests/emptchk.cc +++ b/src/tests/emptchk.cc @@ -161,8 +161,7 @@ main(int argc, char** argv) std::cout << ce_found << " counterexample found\n"; if (auto run = res->accepting_run()) { - auto ar = spot::twa_run_to_tgba(a, run); - spot::print_dot(std::cout, ar); + spot::print_dot(std::cout, run->as_twa()); } std::cout << '\n'; if (runs == 0) diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index 3e1a9b746..35b8dfdcd 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -38,13 +38,11 @@ #include "twaalgos/hoa.hh" #include "twaalgos/degen.hh" #include "twa/twaproduct.hh" -#include "twaalgos/reducerun.hh" #include "parseaut/public.hh" #include "twaalgos/copy.hh" #include "twaalgos/minimize.hh" #include "taalgos/minimize.hh" #include "twaalgos/neverclaim.hh" -#include "twaalgos/replayrun.hh" #include "twaalgos/sccfilter.hh" #include "twaalgos/safety.hh" #include "twaalgos/gtec/gtec.hh" @@ -1580,13 +1578,13 @@ checked_main(int argc, char** argv) if (opt_reduce) { tm.start("reducing accepting run"); - run = spot::reduce_run(run); + run = run->reduce(); tm.stop("reducing accepting run"); } if (accepting_run_replay) { tm.start("replaying acc. run"); - if (!spot::replay_twa_run(std::cout, run, true)) + if (!run->replay(std::cout, true)) exit_code = 1; tm.stop("replaying acc. run"); } @@ -1594,14 +1592,9 @@ checked_main(int argc, char** argv) { tm.start("printing accepting run"); if (graph_run_tgba_opt) - { - auto ar = spot::twa_run_to_tgba(a, run); - spot::print_dot(std::cout, ar); - } + spot::print_dot(std::cout, run->as_twa()); else - { - std::cout << run; - } + std::cout << run; tm.stop("printing accepting run"); } } diff --git a/src/tests/randtgba.cc b/src/tests/randtgba.cc index 4988b1122..861894d81 100644 --- a/src/tests/randtgba.cc +++ b/src/tests/randtgba.cc @@ -51,8 +51,6 @@ #include "twaalgos/emptiness.hh" #include "twaalgos/emptiness_stats.hh" -#include "twaalgos/reducerun.hh" -#include "twaalgos/replayrun.hh" struct ec_algo { @@ -1026,7 +1024,7 @@ main(int argc, char** argv) { tm_ar.stop(algo); std::ostringstream s; - if (!spot::replay_twa_run(s, run)) + if (!run->replay(s)) { if (!opt_paper) std::cout << ", but could not replay " @@ -1047,8 +1045,8 @@ main(int argc, char** argv) if (opt_reduce) { - auto redrun = spot::reduce_run(run); - if (!spot::replay_twa_run(s, redrun)) + auto redrun = run->reduce(); + if (!redrun->replay(s)) { if (!opt_paper) std::cout diff --git a/src/twaalgos/Makefile.am b/src/twaalgos/Makefile.am index 66da8ff9c..8603fa58c 100644 --- a/src/twaalgos/Makefile.am +++ b/src/twaalgos/Makefile.am @@ -62,11 +62,9 @@ twaalgos_HEADERS = \ randomgraph.hh \ randomize.hh \ reachiter.hh \ - reducerun.hh \ relabel.hh \ remfin.hh \ remprop.hh \ - replayrun.hh \ safety.hh \ sbacc.hh \ sccfilter.hh \ @@ -119,10 +117,8 @@ libtwaalgos_la_SOURCES = \ randomgraph.cc \ randomize.cc \ reachiter.cc \ - reducerun.cc \ remfin.cc \ remprop.cc \ - replayrun.cc \ relabel.cc \ safety.cc \ sbacc.cc \ diff --git a/src/twaalgos/emptiness.cc b/src/twaalgos/emptiness.cc index c3329653c..8cb28200a 100644 --- a/src/twaalgos/emptiness.cc +++ b/src/twaalgos/emptiness.cc @@ -22,79 +22,19 @@ #include #include "emptiness.hh" -#include "twa/twa.hh" +#include "bfssteps.hh" +#include "gtec/gtec.hh" +#include "gv04.hh" +#include "magic.hh" +#include "misc/hash.hh" +#include "se05.hh" +#include "tau03.hh" +#include "tau03opt.hh" #include "twa/bddprint.hh" -#include "twaalgos/gtec/gtec.hh" -#include "twaalgos/gv04.hh" -#include "twaalgos/magic.hh" -#include "twaalgos/se05.hh" -#include "twaalgos/tau03.hh" -#include "twaalgos/tau03opt.hh" namespace spot { - // twa_run - ////////////////////////////////////////////////////////////////////// - - twa_run::~twa_run() - { - for (auto i : prefix) - i.s->destroy(); - for (auto i : cycle) - i.s->destroy(); - } - - twa_run::twa_run(const twa_run& run) - { - aut = run.aut; - for (step s : run.prefix) - { - s.s = s.s->clone(); - prefix.push_back(s); - } - for (step s : run.cycle) - { - s.s = s.s->clone(); - cycle.push_back(s); - } - } - - twa_run& - twa_run::operator=(const twa_run& run) - { - if (&run != this) - { - this->~twa_run(); - new(this) twa_run(run); - } - return *this; - } - - std::ostream& - operator<<(std::ostream& os, const twa_run_ptr& run) - { - auto& a = run->aut; - bdd_dict_ptr d = a->get_dict(); - - auto pstep = [&](const twa_run::step& st) - { - os << " " << a->format_state(st.s) << "\n | "; - bdd_print_formula(os, d, st.label); - if (st.acc) - os << '\t' << st.acc; - os << '\n'; - }; - - os << "Prefix:" << std::endl; - for (auto& s: run->prefix) - pstep(s); - os << "Cycle:" << std::endl; - for (auto& s: run->cycle) - pstep(s); - return os; - } - // emptiness_check_result ////////////////////////////////////////////////////////////////////// @@ -276,18 +216,459 @@ namespace spot return nullptr; } - // twa_run_to_tgba + // twa_run ////////////////////////////////////////////////////////////////////// - twa_graph_ptr - twa_run_to_tgba(const const_twa_ptr& a, const const_twa_run_ptr& run) + twa_run::~twa_run() { - auto d = a->get_dict(); - auto res = make_twa_graph(d); - res->copy_ap_of(a); - res->copy_acceptance_of(a); + for (auto i : prefix) + i.s->destroy(); + for (auto i : cycle) + i.s->destroy(); + } - const state* s = a->get_init_state(); + twa_run::twa_run(const twa_run& run) + { + aut = run.aut; + for (step s : run.prefix) + { + s.s = s.s->clone(); + prefix.push_back(s); + } + for (step s : run.cycle) + { + s.s = s.s->clone(); + cycle.push_back(s); + } + } + + twa_run& + twa_run::operator=(const twa_run& run) + { + if (&run != this) + { + this->~twa_run(); + new(this) twa_run(run); + } + return *this; + } + + std::ostream& + operator<<(std::ostream& os, const twa_run_ptr& run) + { + auto& a = run->aut; + bdd_dict_ptr d = a->get_dict(); + + auto pstep = [&](const twa_run::step& st) + { + os << " " << a->format_state(st.s) << "\n | "; + bdd_print_formula(os, d, st.label); + if (st.acc) + os << '\t' << st.acc; + os << '\n'; + }; + + os << "Prefix:" << std::endl; + for (auto& s: run->prefix) + pstep(s); + os << "Cycle:" << std::endl; + for (auto& s: run->cycle) + pstep(s); + return os; + } + + namespace + { + class shortest_path: public bfs_steps + { + public: + shortest_path(const const_twa_ptr& a) + : bfs_steps(a), target(nullptr) + { + } + + ~shortest_path() + { + state_set::const_iterator i = seen.begin(); + while (i != seen.end()) + { + const state* ptr = *i; + ++i; + ptr->destroy(); + } + } + + void + set_target(const state_set* t) + { + target = t; + } + + const state* + search(const state* start, twa_run::steps& l) + { + return this->bfs_steps::search(filter(start), l); + } + + const state* + filter(const state* s) + { + state_set::const_iterator i = seen.find(s); + if (i == seen.end()) + seen.insert(s); + else + { + s->destroy(); + s = *i; + } + return s; + } + + bool + match(twa_run::step&, const state* dest) + { + return target->find(dest) != target->end(); + } + + private: + state_set seen; + const state_set* target; + }; + } + + twa_run_ptr twa_run::reduce() const + { + auto& a = aut; + auto res = std::make_shared(a); + state_set ss; + shortest_path shpath(a); + shpath.set_target(&ss); + + // We want to find a short segment of the original cycle that + // contains all acceptance conditions. + + const state* segment_start; // The initial state of the segment. + const state* segment_next; // The state immediately after the segment. + + // Start from the end of the original cycle, and rewind until all + // acceptance sets have been seen. + acc_cond::mark_t seen_acc = 0U; + twa_run::steps::const_iterator seg = cycle.end(); + do + { + assert(seg != cycle.begin()); + --seg; + seen_acc |= seg->acc; + } + while (!a->acc().accepting(seen_acc)); + segment_start = seg->s; + + // Now go forward and ends the segment as soon as we have seen all + // acceptance sets, cloning it in our result along the way. + seen_acc = 0U; + do + { + assert(seg != cycle.end()); + seen_acc |= seg->acc; + + twa_run::step st = { seg->s->clone(), seg->label, seg->acc }; + res->cycle.push_back(st); + + ++seg; + } + while (!a->acc().accepting(seen_acc)); + segment_next = seg == cycle.end() ? cycle.front().s : seg->s; + + // Close this cycle if needed, that is, compute a cycle going + // from the state following the segment to its starting state. + if (segment_start != segment_next) + { + ss.insert(segment_start); + const state* s = shpath.search(segment_next->clone(), res->cycle); + ss.clear(); + assert(s->compare(segment_start) == 0); + (void)s; + } + + // Compute the prefix: it's the shortest path from the initial + // state of the automata to any state of the cycle. + + // Register all states from the cycle as target of the BFS. + for (twa_run::steps::const_iterator i = res->cycle.begin(); + i != res->cycle.end(); ++i) + ss.insert(i->s); + + const state* prefix_start = a->get_init_state(); + // There are two cases: either the initial state is already on + // the cycle, or it is not. If it is, we will have to rotate + // the cycle so it begins on this position. Otherwise we will shift + // the cycle so it begins on the state that follows the prefix. + // cycle_entry_point is that state. + const state* cycle_entry_point; + state_set::const_iterator ps = ss.find(prefix_start); + if (ps != ss.end()) + { + // The initial state is on the cycle. + prefix_start->destroy(); + cycle_entry_point = *ps; + } + else + { + // This initial state is outside the cycle. Compute the prefix. + cycle_entry_point = shpath.search(prefix_start, res->prefix); + } + + // Locate cycle_entry_point on the cycle. + twa_run::steps::iterator cycle_ep_it; + for (cycle_ep_it = res->cycle.begin(); + cycle_ep_it != res->cycle.end() + && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) + continue; + assert(cycle_ep_it != res->cycle.end()); + + // Now shift the cycle so it starts on cycle_entry_point. + res->cycle.splice(res->cycle.end(), res->cycle, + res->cycle.begin(), cycle_ep_it); + + return res; + } + + namespace + { + static void + print_annotation(std::ostream& os, + const const_twa_ptr& a, + const twa_succ_iterator* i) + { + std::string s = a->transition_annotation(i); + if (s == "") + return; + os << ' ' << s; + } + } + + bool twa_run::replay(std::ostream& os, bool debug) const + { + const state* s = aut->get_init_state(); + int serial = 1; + const twa_run::steps* l; + std::string in; + acc_cond::mark_t all_acc = 0U; + bool all_acc_seen = false; + typedef std::unordered_map, + state_ptr_hash, state_ptr_equal> state_map; + state_map seen; + + if (prefix.empty()) + { + l = &cycle; + in = "cycle"; + if (!debug) + os << "No prefix.\nCycle:\n"; + } + else + { + l = &prefix; + in = "prefix"; + if (!debug) + os << "Prefix:\n"; + } + + twa_run::steps::const_iterator i = l->begin(); + + if (s->compare(i->s)) + { + if (debug) + os << "ERROR: First state of run (in " << in << "): " + << aut->format_state(i->s) + << "\ndoes not match initial state of automata: " + << aut->format_state(s) << '\n'; + s->destroy(); + return false; + } + + for (; i != l->end(); ++serial) + { + if (debug) + { + // Keep track of the serial associated to each state so we + // can note duplicate states and make the replay easier to read. + state_map::iterator o = seen.find(s); + std::ostringstream msg; + if (o != seen.end()) + { + for (auto d: o->second) + msg << " == " << d; + o->second.insert(serial); + s->destroy(); + s = o->first; + } + else + { + seen[s].insert(serial); + } + os << "state " << serial << " in " << in << msg.str() << ": "; + } + else + { + os << " "; + } + os << aut->format_state(s) << '\n'; + + // expected outgoing transition + bdd label = i->label; + acc_cond::mark_t acc = i->acc; + + // compute the next expected state + const state* next; + ++i; + if (i != l->end()) + { + next = i->s; + } + else + { + if (l == &prefix) + { + l = &cycle; + in = "cycle"; + i = l->begin(); + if (!debug) + os << "Cycle:\n"; + } + next = l->begin()->s; + } + + // browse the actual outgoing transitions + twa_succ_iterator* j = aut->succ_iter(s); + // When not debugging, S is not used as key in SEEN, so we can + // destroy it right now. + if (!debug) + s->destroy(); + if (j->first()) + do + { + if (j->current_condition() != label + || j->current_acceptance_conditions() != acc) + continue; + + const state* s2 = j->current_state(); + if (s2->compare(next)) + { + s2->destroy(); + continue; + } + else + { + s = s2; + break; + } + } + while (j->next()); + if (j->done()) + { + if (debug) + { + os << "ERROR: no transition with label=" + << bdd_format_formula(aut->get_dict(), label) + << " and acc=" << aut->acc().format(acc) + << " leaving state " << serial + << " for state " << aut->format_state(next) << '\n' + << "The following transitions leave state " << serial + << ":\n"; + if (j->first()) + do + { + const state* s2 = j->current_state(); + os << " *"; + print_annotation(os, aut, j); + os << " label=" + << bdd_format_formula(aut->get_dict(), + j->current_condition()) + << " and acc=" + << (aut->acc().format + (j->current_acceptance_conditions())) + << " going to " << aut->format_state(s2) << '\n'; + s2->destroy(); + } + while (j->next()); + } + aut->release_iter(j); + s->destroy(); + return false; + } + if (debug) + { + os << "transition"; + print_annotation(os, aut, j); + os << " with label=" + << bdd_format_formula(aut->get_dict(), label) + << " and acc=" << aut->acc().format(acc) + << std::endl; + } + else + { + os << " | "; + print_annotation(os, aut, j); + bdd_print_formula(os, aut->get_dict(), label); + os << '\t'; + aut->acc().format(acc); + os << std::endl; + } + aut->release_iter(j); + + // Sum acceptance conditions. + // + // (Beware l and i designate the next step to consider. + // Therefore if i is at the beginning of the cycle, `acc' + // contains the acceptance conditions of the last transition + // in the prefix; we should not account it.) + if (l == &cycle && i != l->begin()) + { + all_acc |= acc; + if (!all_acc_seen && aut->acc().accepting(all_acc)) + { + all_acc_seen = true; + if (debug) + os << "all acceptance conditions (" + << aut->acc().format(all_acc) + << ") have been seen\n"; + } + } + } + s->destroy(); + if (!aut->acc().accepting(all_acc)) + { + if (debug) + os << "ERROR: The cycle's acceptance conditions (" + << aut->acc().format(all_acc) + << ") do not\nmatch those of the automaton (" + << aut->acc().format(aut->acc().all_sets()) + << ")\n"; + return false; + } + + state_map::const_iterator o = seen.begin(); + while (o != seen.end()) + { + // Advance the iterator before deleting the "key" pointer. + const state* ptr = o->first; + ++o; + ptr->destroy(); + } + + return true; + } + + twa_graph_ptr + twa_run::as_twa() const + { + auto d = aut->get_dict(); + auto res = make_twa_graph(d); + res->copy_ap_of(aut); + res->copy_acceptance_of(aut); + + const state* s = aut->get_init_state(); unsigned src; unsigned dst; const twa_run::steps* l; @@ -297,10 +678,10 @@ namespace spot state_ptr_hash, state_ptr_equal> state_map; state_map seen; - if (run->prefix.empty()) - l = &run->cycle; + if (prefix.empty()) + l = &cycle; else - l = &run->prefix; + l = &prefix; twa_run::steps::const_iterator i = l->begin(); @@ -323,9 +704,9 @@ namespace spot } else { - if (l == &run->prefix) + if (l == &prefix) { - l = &run->cycle; + l = &cycle; i = l->begin(); } next = l->begin()->s; @@ -334,7 +715,7 @@ namespace spot // browse the actual outgoing transitions and // look for next; const state* the_next = nullptr; - for (auto j: a->succ(s)) + for (auto j: aut->succ(s)) { if (j->current_condition() != label || j->current_acceptance_conditions() != acc) @@ -362,13 +743,13 @@ namespace spot src = dst; // Sum acceptance conditions. - if (l == &run->cycle && i != l->begin()) + if (l == &cycle && i != l->begin()) seen_acc |= acc; } s->destroy(); - assert(a->acc().accepting(seen_acc)); + assert(aut->acc().accepting(seen_acc)); return res; } diff --git a/src/twaalgos/emptiness.hh b/src/twaalgos/emptiness.hh index d79a65d1c..b3e72fd27 100644 --- a/src/twaalgos/emptiness.hh +++ b/src/twaalgos/emptiness.hh @@ -292,6 +292,31 @@ namespace spot twa_run(const twa_run& run); twa_run& operator=(const twa_run& run); + /// \brief Reduce an accepting run. + /// + /// Return a run which is still accepting for aut, + /// but is no longer than this one. + twa_run_ptr reduce() const; + + /// \brief Replay a run. + /// + /// This is similar to os << run;, except that the + /// run is actually replayed on the automaton while it is printed. + /// Doing so makes it possible to display transition annotations + /// (returned by spot::twa::transition_annotation()). The output + /// will stop if the run cannot be completed. + /// + /// \param os the stream on which the replay should be traced + /// \param debug if set the output will be more verbose and extra + /// debugging informations will be output on failure + /// \return true iff the run could be completed + bool replay(std::ostream& os, bool debug = false) const; + + /// \brief Return a twa_graph_ptr corresponding to \a run + /// + /// Identical states are merged. + twa_graph_ptr as_twa() const; + /// \brief Display a twa_run. /// /// Output the prefix and cycle parts of the twa_run \a run on \a os. @@ -309,15 +334,6 @@ namespace spot SPOT_API friend std::ostream& operator<<(std::ostream& os, const twa_run_ptr& run); }; - - - /// \brief Return an explicit_tgba corresponding to \a run (i.e. comparable - /// states are merged). - /// - /// \pre \a run must correspond to an actual run of the automaton \a a. - SPOT_API twa_graph_ptr - twa_run_to_tgba(const const_twa_ptr& a, const const_twa_run_ptr& run); - /// @} /// \addtogroup emptiness_check_stats Emptiness-check statistics diff --git a/src/twaalgos/reducerun.cc b/src/twaalgos/reducerun.cc deleted file mode 100644 index 4813e34e4..000000000 --- a/src/twaalgos/reducerun.cc +++ /dev/null @@ -1,187 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// 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 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include "misc/hash.hh" -#include "emptiness.hh" -#include "twa/twa.hh" -#include "bfssteps.hh" -#include "reducerun.hh" - -namespace spot -{ - namespace - { - class shortest_path: public bfs_steps - { - public: - shortest_path(const const_twa_ptr& a) - : bfs_steps(a), target(nullptr) - { - } - - ~shortest_path() - { - state_set::const_iterator i = seen.begin(); - while (i != seen.end()) - { - const state* ptr = *i; - ++i; - ptr->destroy(); - } - } - - void - set_target(const state_set* t) - { - target = t; - } - - const state* - search(const state* start, twa_run::steps& l) - { - return this->bfs_steps::search(filter(start), l); - } - - const state* - filter(const state* s) - { - state_set::const_iterator i = seen.find(s); - if (i == seen.end()) - seen.insert(s); - else - { - s->destroy(); - s = *i; - } - return s; - } - - bool - match(twa_run::step&, const state* dest) - { - return target->find(dest) != target->end(); - } - - private: - state_set seen; - const state_set* target; - }; - } - - twa_run_ptr - reduce_run(const const_twa_run_ptr& org) - { - auto& a = org->aut; - auto res = std::make_shared(a); - state_set ss; - shortest_path shpath(a); - shpath.set_target(&ss); - - // We want to find a short segment of the original cycle that - // contains all acceptance conditions. - - const state* segment_start; // The initial state of the segment. - const state* segment_next; // The state immediately after the segment. - - // Start from the end of the original cycle, and rewind until all - // acceptance sets have been seen. - acc_cond::mark_t seen_acc = 0U; - twa_run::steps::const_iterator seg = org->cycle.end(); - do - { - assert(seg != org->cycle.begin()); - --seg; - seen_acc |= seg->acc; - } - while (!a->acc().accepting(seen_acc)); - segment_start = seg->s; - - // Now go forward and ends the segment as soon as we have seen all - // acceptance sets, cloning it in our result along the way. - seen_acc = 0U; - do - { - assert(seg != org->cycle.end()); - seen_acc |= seg->acc; - - twa_run::step st = { seg->s->clone(), seg->label, seg->acc }; - res->cycle.push_back(st); - - ++seg; - } - while (!a->acc().accepting(seen_acc)); - segment_next = seg == org->cycle.end() ? org->cycle.front().s : seg->s; - - // Close this cycle if needed, that is, compute a cycle going - // from the state following the segment to its starting state. - if (segment_start != segment_next) - { - ss.insert(segment_start); - const state* s = shpath.search(segment_next->clone(), res->cycle); - ss.clear(); - assert(s->compare(segment_start) == 0); - (void)s; - } - - // Compute the prefix: it's the shortest path from the initial - // state of the automata to any state of the cycle. - - // Register all states from the cycle as target of the BFS. - for (twa_run::steps::const_iterator i = res->cycle.begin(); - i != res->cycle.end(); ++i) - ss.insert(i->s); - - const state* prefix_start = a->get_init_state(); - // There are two cases: either the initial state is already on - // the cycle, or it is not. If it is, we will have to rotate - // the cycle so it begins on this position. Otherwise we will shift - // the cycle so it begins on the state that follows the prefix. - // cycle_entry_point is that state. - const state* cycle_entry_point; - state_set::const_iterator ps = ss.find(prefix_start); - if (ps != ss.end()) - { - // The initial state is on the cycle. - prefix_start->destroy(); - cycle_entry_point = *ps; - } - else - { - // This initial state is outside the cycle. Compute the prefix. - cycle_entry_point = shpath.search(prefix_start, res->prefix); - } - - // Locate cycle_entry_point on the cycle. - twa_run::steps::iterator cycle_ep_it; - for (cycle_ep_it = res->cycle.begin(); - cycle_ep_it != res->cycle.end() - && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) - continue; - assert(cycle_ep_it != res->cycle.end()); - - // Now shift the cycle so it starts on cycle_entry_point. - res->cycle.splice(res->cycle.end(), res->cycle, - res->cycle.begin(), cycle_ep_it); - - return res; - } -} diff --git a/src/twaalgos/reducerun.hh b/src/twaalgos/reducerun.hh deleted file mode 100644 index f95c9759f..000000000 --- a/src/twaalgos/reducerun.hh +++ /dev/null @@ -1,38 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2010, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita. -// 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 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#pragma once - -#include "misc/common.hh" -#include "twa/fwd.hh" -#include "twaalgos/emptiness.hh" - -namespace spot -{ - /// \ingroup twa_run - /// \brief Reduce an accepting run. - /// - /// Return a run which is still accepting for org->aut, - /// but is no longer than \a org. - SPOT_API twa_run_ptr - reduce_run(const const_twa_run_ptr& org); -} diff --git a/src/twaalgos/replayrun.cc b/src/twaalgos/replayrun.cc deleted file mode 100644 index f330ded0e..000000000 --- a/src/twaalgos/replayrun.cc +++ /dev/null @@ -1,260 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// 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 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include "misc/hash.hh" -#include "replayrun.hh" -#include "twa/twa.hh" -#include "emptiness.hh" -#include "twa/bddprint.hh" -#include - -namespace spot -{ - namespace - { - void - print_annotation(std::ostream& os, - const const_twa_ptr& a, - const twa_succ_iterator* i) - { - std::string s = a->transition_annotation(i); - if (s == "") - return; - os << ' ' << s; - } - } - - bool - replay_twa_run(std::ostream& os, - const const_twa_run_ptr& run, bool debug) - { - auto& a = run->aut; - const state* s = a->get_init_state(); - int serial = 1; - const twa_run::steps* l; - std::string in; - acc_cond::mark_t all_acc = 0U; - bool all_acc_seen = false; - typedef std::unordered_map, - state_ptr_hash, state_ptr_equal> state_map; - state_map seen; - - if (run->prefix.empty()) - { - l = &run->cycle; - in = "cycle"; - if (!debug) - os << "No prefix.\nCycle:\n"; - } - else - { - l = &run->prefix; - in = "prefix"; - if (!debug) - os << "Prefix:\n"; - } - - twa_run::steps::const_iterator i = l->begin(); - - if (s->compare(i->s)) - { - if (debug) - os << "ERROR: First state of run (in " << in << "): " - << a->format_state(i->s) - << "\ndoes not match initial state of automata: " - << a->format_state(s) << '\n'; - s->destroy(); - return false; - } - - for (; i != l->end(); ++serial) - { - if (debug) - { - // Keep track of the serial associated to each state so we - // can note duplicate states and make the replay easier to read. - state_map::iterator o = seen.find(s); - std::ostringstream msg; - if (o != seen.end()) - { - for (auto d: o->second) - msg << " == " << d; - o->second.insert(serial); - s->destroy(); - s = o->first; - } - else - { - seen[s].insert(serial); - } - os << "state " << serial << " in " << in << msg.str() << ": "; - } - else - { - os << " "; - } - os << a->format_state(s) << '\n'; - - // expected outgoing transition - bdd label = i->label; - acc_cond::mark_t acc = i->acc; - - // compute the next expected state - const state* next; - ++i; - if (i != l->end()) - { - next = i->s; - } - else - { - if (l == &run->prefix) - { - l = &run->cycle; - in = "cycle"; - i = l->begin(); - if (!debug) - os << "Cycle:\n"; - } - next = l->begin()->s; - } - - // browse the actual outgoing transitions - twa_succ_iterator* j = a->succ_iter(s); - // When not debugging, S is not used as key in SEEN, so we can - // destroy it right now. - if (!debug) - s->destroy(); - if (j->first()) - do - { - if (j->current_condition() != label - || j->current_acceptance_conditions() != acc) - continue; - - const state* s2 = j->current_state(); - if (s2->compare(next)) - { - s2->destroy(); - continue; - } - else - { - s = s2; - break; - } - } - while (j->next()); - if (j->done()) - { - if (debug) - { - os << "ERROR: no transition with label=" - << bdd_format_formula(a->get_dict(), label) - << " and acc=" << a->acc().format(acc) - << " leaving state " << serial - << " for state " << a->format_state(next) << '\n' - << "The following transitions leave state " << serial - << ":\n"; - if (j->first()) - do - { - const state* s2 = j->current_state(); - os << " *"; - print_annotation(os, a, j); - os << " label=" - << bdd_format_formula(a->get_dict(), - j->current_condition()) - << " and acc=" - << a->acc().format(j->current_acceptance_conditions()) - << " going to " << a->format_state(s2) << '\n'; - s2->destroy(); - } - while (j->next()); - } - a->release_iter(j); - s->destroy(); - return false; - } - if (debug) - { - os << "transition"; - print_annotation(os, a, j); - os << " with label=" - << bdd_format_formula(a->get_dict(), label) - << " and acc=" << a->acc().format(acc) - << std::endl; - } - else - { - os << " | "; - print_annotation(os, a, j); - bdd_print_formula(os, a->get_dict(), label); - os << '\t'; - a->acc().format(acc); - os << std::endl; - } - a->release_iter(j); - - // Sum acceptance conditions. - // - // (Beware l and i designate the next step to consider. - // Therefore if i is at the beginning of the cycle, `acc' - // contains the acceptance conditions of the last transition - // in the prefix; we should not account it.) - if (l == &run->cycle && i != l->begin()) - { - all_acc |= acc; - if (!all_acc_seen && a->acc().accepting(all_acc)) - { - all_acc_seen = true; - if (debug) - os << "all acceptance conditions (" - << a->acc().format(all_acc) - << ") have been seen\n"; - } - } - } - s->destroy(); - if (!a->acc().accepting(all_acc)) - { - if (debug) - os << "ERROR: The cycle's acceptance conditions (" - << a->acc().format(all_acc) - << ") do not\nmatch those of the automaton (" - << a->acc().format(a->acc().all_sets()) - << ")\n"; - return false; - } - - state_map::const_iterator o = seen.begin(); - while (o != seen.end()) - { - // Advance the iterator before deleting the "key" pointer. - const state* ptr = o->first; - ++o; - ptr->destroy(); - } - - return true; - } -} diff --git a/src/twaalgos/replayrun.hh b/src/twaalgos/replayrun.hh deleted file mode 100644 index b95ca342a..000000000 --- a/src/twaalgos/replayrun.hh +++ /dev/null @@ -1,52 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). -// 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 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#pragma once - -#include "misc/common.hh" -#include -#include "twa/fwd.hh" -#include "twaalgos/emptiness.hh" - -namespace spot -{ - struct twa_run; - - /// \ingroup twa_run - /// \brief Replay a twa_run on a tgba. - /// - /// This is similar to os << run;, except that the run is - /// actually replayed on the automaton while it is printed. Doing - /// so makes it possible to display transition annotations (returned - /// by spot::twa::transition_annotation()). The output will stop - /// if the run cannot be completed. - /// - /// \param run the run to replay - /// \param os the stream on which the replay should be traced - /// \param debug if set the output will be more verbose and extra - /// debugging informations will be output on failure - /// \return true iff the run could be completed - SPOT_API bool - replay_twa_run(std::ostream& os, - const const_twa_run_ptr& run, - bool debug = false); -} diff --git a/wrap/python/ajax/spotcgi.in b/wrap/python/ajax/spotcgi.in index 3aebc0a31..2a1714beb 100755 --- a/wrap/python/ajax/spotcgi.in +++ b/wrap/python/ajax/spotcgi.in @@ -843,7 +843,7 @@ if output_type == 'r': unbufprint('
%s
' % cgi.escape(str(ec_run))) if draw_acc_run: - render_automaton(spot.twa_run_to_tgba(ec_a, ec_run), False) + render_automaton(ec_run.as_twa(), False) del ec_run del ec_res unbufprint('')