diff --git a/ChangeLog b/ChangeLog index def4d0fee..cd417ef57 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,20 @@ 2004-01-09 Alexandre Duret-Lutz + * src/tgbaalgos/emptinesscheck.cc (emptiness_check::check2): + New function, variant of emptiness_check::check(). + * src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2): + Likewise. + * src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Exercize -e2. + * src/tgbatest/ltl2tgba.cc: Support -e2, for emptiness_check::check2(). + * iface/gspn/Makefile.am [WITH_GSPN_EESRG] (check_PROGRAMS): + Compile ltlgspn-eesrg instead of ltleesrg. + (ltleesrg_SOURCES, ltleesrg_LDADD): Replace by... + (ltlgspn_eesrg_SOURCES, ltlgspn_eesrg_LDADD, LIBGSPNESRG_LDFLAGS): + ... these. + * iface/gspn/ltleesrg.cc: Delete. + * iface/gspn/ltlgspn.cc [EESRG]: Support EESRG conditionally. + Support -e2. + * src/tgbaalgos/ltl2tgba_lacim.cc: Typo in comment. * src/tgbaalgos/emptinesscheck.cc (emptiness_check::check): Typos diff --git a/iface/gspn/Makefile.am b/iface/gspn/Makefile.am index c00dbb327..c05a7c888 100644 --- a/iface/gspn/Makefile.am +++ b/iface/gspn/Makefile.am @@ -44,7 +44,7 @@ if WITH_GSPN_EESRG gspn_HEADERS += eesrg.hh check_PROGRAMS += \ dottygspn-eesrg \ - ltleesrg + ltlgspn-eesrg libspotgspneesrg_la_LIBADD = $(top_builddir)/src/libspot.la libspotgspneesrg_la_CPPFLAGS = -DESYMBOLIC $(AM_CPPFLAGS) @@ -69,8 +69,9 @@ ltlgspn_rg_LDADD = libspotgspn.la $(LIBGSPNRG_LDFLAGS) ltlgspn_srg_SOURCES = ltlgspn.cc ltlgspn_srg_LDADD = libspotgspn.la $(LIBGSPNSRG_LDFLAGS) -ltleesrg_SOURCES = ltleesrg.cc -ltleesrg_LDADD = libspotgspneesrg.la $(LIBGSPNESRG_LDFLAGS) +ltlgspn_eesrg_SOURCES = ltlgspn.cc +ltlgspn_eesrg_LDADD = libspotgspneesrg.la $(LIBGSPNESRG_LDFLAGS) +ltlgspn_eesrg_CPPFLAGS = -DEESRG=1 $(AM_CPPFLAGS) EXTRA_DIST = \ examples/DCSwave/DCSWave.def \ diff --git a/iface/gspn/ltleesrg.cc b/iface/gspn/ltleesrg.cc deleted file mode 100644 index 95d5bc473..000000000 --- a/iface/gspn/ltleesrg.cc +++ /dev/null @@ -1,98 +0,0 @@ -// 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. - -#include "eesrg.hh" -#include "tgbaalgos/dotty.hh" -#include "tgba/tgbaexplicit.hh" -#include "tgbaparse/public.hh" -#include "tgbaalgos/ltl2tgba_fm.hh" -#include "tgbaalgos/emptinesscheck.hh" -#include "ltlparse/public.hh" -#include "ltlvisit/destroy.hh" -#include "tgba/tgbaproduct.hh" - -int -main(int argc, char **argv) - try - { - spot::gspn_environment env; - - if (argc <= 4) - { - std::cerr << "usage: " << argv[0] - << " model ltlformula automata props..." - << std::endl; - exit(1); - } - - while (argc > 4) - env.declare(argv[--argc]); - - spot::ltl::parse_error_list pel; - spot::ltl::formula* f = spot::ltl::parse(argv[2], pel, env); - if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel)) - exit(2); - - spot::gspn_eesrg_interface gspn(2, argv); - spot::bdd_dict* dict = new spot::bdd_dict(); - - spot::tgba_parse_error_list pel1; - spot::tgba_explicit* control = spot::tgba_parse(argv[3], pel1, - dict, env); - if (spot::format_tgba_parse_errors(std::cerr, pel1)) - return 2; - - spot::tgba* a_f = spot::ltl_to_tgba_fm(f, dict); - spot::ltl::destroy(f); - - spot::tgba_product* prod = new spot::tgba_product(control, a_f); - - - { - spot::tgba_gspn_eesrg a(dict, env, prod); - - spot::emptiness_check ec(&a); - bool res = ec.check(); - if (!res) - { - ec.counter_example(); - ec.print_result(std::cout, &a); - } - else - { - std::cout << "empty" << std::endl; - } - std::cout << std::endl; - ec.print_stats(std::cout); - if (!res) - exit(1); - } - - delete prod; - delete a_f; - delete control; - delete dict; - } - catch (spot::gspn_exeption e) - { - std::cerr << e << std::endl; - throw; - } diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index b7a540dea..537f1a2fc 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -19,7 +19,15 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#ifndef EESRG #include "gspn.hh" +#define MIN_ARG 3 +#else +#include "eesrg.hh" +#define MIN_ARG 4 +#include "tgba/tgbaexplicit.hh" +#include "tgbaparse/public.hh" +#endif #include "ltlparse/public.hh" #include "ltlvisit/destroy.hh" #include "tgba/tgbatba.hh" @@ -29,16 +37,22 @@ #include "tgbaalgos/magic.hh" #include "tgbaalgos/emptinesscheck.hh" + void syntax(char* prog) { std::cerr << "Usage: "<< prog +#ifndef EESRG << " [OPTIONS...] model formula props..." << std::endl +#else + << " [OPTIONS...] model formula automata props..." << std::endl +#endif << std::endl << " -c compute an example" << std::endl << " (instead of just checking for emptiness)" << std::endl << std::endl << " -e use Couvreur's emptiness-check (default)" << std::endl + << " -e2 use Couvreur's emptiness-check variant" << std::endl << " -m degeneralize and perform a magic-search" << std::endl << std::endl << " -l use Couvreur's LaCIM algorithm for translation (default)" @@ -53,7 +67,7 @@ main(int argc, char **argv) try { int formula_index = 1; - enum { Couvreur, Magic } check = Couvreur; + enum { Couvreur, Couvreur2, Magic } check = Couvreur; enum { Lacim, Fm } trans = Lacim; bool compute_counter_example = false; bool proj = true; @@ -70,6 +84,10 @@ main(int argc, char **argv) { check = Couvreur; } + else if (!strcmp(argv[formula_index], "-e2")) + { + check = Couvreur2; + } else if (!strcmp(argv[formula_index], "-m")) { check = Magic; @@ -92,11 +110,11 @@ main(int argc, char **argv) } ++formula_index; } - if (argc < formula_index + 3) + if (argc < formula_index + MIN_ARG) syntax(argv[0]); - while (argc > formula_index + 2) + while (argc >= formula_index + 3) { env.declare(argv[argc - 1]); --argc; @@ -111,9 +129,20 @@ main(int argc, char **argv) exit(2); argv[1] = argv[formula_index]; - spot::gspn_interface gspn(2, argv); spot::bdd_dict* dict = new spot::bdd_dict(); +#if EESRG + spot::gspn_eesrg_interface gspn(2, argv); + + spot::tgba_parse_error_list pel1; + spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2], + pel1, dict, env); + if (spot::format_tgba_parse_errors(std::cerr, pel1)) + return 2; +#else + spot::gspn_interface gspn(2, argv); +#endif + spot::tgba* a_f = 0; switch (trans) { @@ -126,15 +155,26 @@ main(int argc, char **argv) } spot::ltl::destroy(f); +#ifndef EESRG spot::tgba* model = new spot::tgba_gspn(dict, env); spot::tgba_product* prod = new spot::tgba_product(model, a_f); +#else + spot::tgba_product* ca = new spot::tgba_product(control, a_f); + spot::tgba* model = new spot::tgba_gspn_eesrg(dict, env, ca); + spot::tgba* prod = model; +#endif switch (check) { case Couvreur: + case Couvreur2: { spot::emptiness_check ec(prod); - bool res = ec.check(); + bool res; + if (check == Couvreur) + res = ec.check(); + else + res = ec.check2(); if (!res) { if (compute_counter_example) @@ -177,8 +217,13 @@ main(int argc, char **argv) delete d; } } +#ifndef EESRG delete prod; delete model; +#else + delete model; + delete control; +#endif delete a_f; delete dict; } diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc index 3a3eebbb7..6a94c7718 100644 --- a/src/tgbaalgos/emptinesscheck.cc +++ b/src/tgbaalgos/emptinesscheck.cc @@ -25,6 +25,7 @@ #include #include #include +#include namespace spot { @@ -208,7 +209,7 @@ namespace spot if (dest != i->first) delete dest; - // If we have reached a dead component. Ignore it. + // If we have reached a dead component, ignore it. if (i->second == -1) continue; @@ -257,6 +258,171 @@ namespace spot return true; } + struct successor { + bdd acc; + const spot::state* s; + successor(bdd acc, const spot::state* s): acc(acc), s(s) {} + }; + + bool + emptiness_check::check2() + { + // We use five main data in this algorithm: + // * emptiness_check::root, a stack of strongly connected components (SCC), + // * emptiness_check::h, a hash of all visited nodes, with their order, + // (it is called "Hash" in Couvreur's paper) + // * arc, a stack of acceptance conditions between each of these SCC, + std::stack arc; + // * num, the number of visited nodes. Used to set the order of each + // visited node, + int num = 1; + // * todo, the depth-first search stack. This holds pairs of the + // form (STATE, SUCCESSORS) where SUCCESSORS is a list of + // (ACCEPTANCE_CONDITIONS, STATE) pairs. + typedef std::list succ_queue; + typedef std::pair pair_state_successors; + std::stack todo; + + // Setup depth-first search from the initial state. + todo.push(pair_state_successors(0, succ_queue())); + todo.top().second.push_front(successor(bddtrue, aut_->get_init_state())); + + for (;;) + { + assert(root.size() == arc.size()); + + // Get the successors of the current state. + succ_queue& queue = todo.top().second; + + // First, we process all successors that we have already seen. + // This is an idea from Soheib Baarir. It helps to merge SCCs + // and get shorter traces faster. + succ_queue::iterator q = queue.begin(); + while (q != queue.end()) + { + hash_type::iterator i = h.find(q->s); + if (i == h.end()) + { + // Skip unknown states. + ++q; + continue; + } + + // Skip states from dead SCCs. + if (i->second != -1) + { + // Now this is the most interesting case. We have + // reached a state S1 which is already part of a + // non-dead SCC. Any such non-dead SCC has + // necessarily been crossed by our path to this + // state: there is a state S2 in our path which + // belongs to this SCC too. We are going to merge + // all states between this S1 and S2 into this + // SCC. + // + // This merge is easy to do because the order of + // the SCC in ROOT is ascending: we just have to + // merge all SCCs from the top of ROOT that have + // an index greater to the one of the SCC of S2 + // (called the "threshold"). + int threshold = i->second; + bdd acc = q->acc; + while (threshold < root.top().index) + { + assert(!root.empty()); + assert(!arc.empty()); + acc |= root.top().condition; + acc |= arc.top(); + root.pop(); + arc.pop(); + } + // Note that we do not always have + // threshold == root.top().index + // after this loop, the SCC whose index is threshold + // might have been merged with a lower SCC. + + // Accumulate all acceptance conditions into the + // merged SCC. + root.top().condition |= acc; + + if (root.top().condition == aut_->all_acceptance_conditions()) + { + // We have found an accepting SCC. Clean up TODO. + // We must delete all states of apparing in TODO + // unless they are used as keys in H. + while (!todo.empty()) + { + succ_queue& queue = todo.top().second; + for (succ_queue::iterator q = queue.begin(); + q != queue.end(); ++q) + { + hash_type::iterator i = h.find(q->s); + if (i == h.end() || i->first != q->s) + delete q->s; + } + todo.pop(); + } + return false; + } + } + // We know the state exists. Since a state can have several + // representations (i.e., objects), make sure we delete + // anything but the first one seen (the one used as key in H). + if (q->s != i->first) + delete q->s; + // Remove that state from the queue, so we do not + // recurse into it. + succ_queue::iterator old = q++; + queue.erase(old); + } + + // If there is no more successor, backtrack. + if (queue.empty()) + { + // We have explored all successors of state CURR. + const state* curr = todo.top().first; + // Backtrack TODO. + todo.pop(); + if (todo.empty()) + // This automaton recognizes no word. + return true; + + // When backtracking the root of an SCC, we must also + // remove that SCC from the ARC/ROOT stacks. We must + // discard from H all reachable states from this SCC. + hash_type::iterator i = h.find(curr); + assert(i != h.end()); + assert(!root.empty()); + if (root.top().index == i->second) + { + assert(!arc.empty()); + arc.pop(); + root.pop(); + remove_component(curr); + } + continue; + } + + // Recurse. (Finally!) + + // Pick one successor off the list, and schedule its + // successors first on TODO. Update the various hashes and + // stacks. + successor succ = queue.front(); + queue.pop_front(); + h[succ.s] = ++num; + root.push(connected_component(num)); + arc.push(succ.acc); + todo.push(pair_state_successors(succ.s, succ_queue())); + succ_queue& new_queue = todo.top().second; + tgba_succ_iterator* iter = aut_->succ_iter(succ.s); + for (iter->first(); ! iter->done(); iter->next()) + new_queue.push_back(successor(iter->current_acceptance_conditions(), + iter->current_state())); + delete iter; + } + } + std::ostream& emptiness_check::print_result(std::ostream& os, const tgba* restrict) const diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh index 8c784bb29..dcb9c59f4 100644 --- a/src/tgbaalgos/emptinesscheck.hh +++ b/src/tgbaalgos/emptinesscheck.hh @@ -64,6 +64,7 @@ namespace spot /// This function returns true if the automata's language is empty, /// and builds a stack of SCC. bool check(); + bool check2(); /// Compute a counter example if tgba_emptiness_check() returned false. void counter_example(); diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 86e85f02e..1f0c38c70 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -31,6 +31,10 @@ expect_ce() run 0 ./ltl2tgba -e -D "$1" run 0 ./ltl2tgba -e -f "$1" run 0 ./ltl2tgba -e -f -D "$1" + run 0 ./ltl2tgba -e2 "$1" + run 0 ./ltl2tgba -e2 -D "$1" + run 0 ./ltl2tgba -e2 -f "$1" + run 0 ./ltl2tgba -e2 -f -D "$1" run 0 ./ltl2tgba -m "$1" run 0 ./ltl2tgba -m -f "$1" } @@ -41,6 +45,10 @@ expect_no() run 0 ./ltl2tgba -E -D "$1" run 0 ./ltl2tgba -E -f "$1" run 0 ./ltl2tgba -E -f -D "$1" + run 0 ./ltl2tgba -E2 "$1" + run 0 ./ltl2tgba -E2 -D "$1" + run 0 ./ltl2tgba -E2 -f "$1" + run 0 ./ltl2tgba -E2 -f -D "$1" run 0 ./ltl2tgba -M "$1" run 0 ./ltl2tgba -M -f "$1" } diff --git a/src/tgbatest/emptchke.test b/src/tgbatest/emptchke.test index 62e37a2a9..1aad5fd4c 100755 --- a/src/tgbatest/emptchke.test +++ b/src/tgbatest/emptchke.test @@ -33,4 +33,5 @@ s1, "s2", "a & !b", c d; EOF run 0 ./ltl2tgba -e -X input +run 0 ./ltl2tgba -e2 -X input run 0 ./ltl2tgba -m -X input diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 6651097df..f1e462f0e 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -32,8 +32,12 @@ syntax(char* prog) << " -D degeneralize the automaton" << std::endl << " -e emptiness-check (Couvreur), expect and compute " << "a counter-example" << std::endl + << " -e2 emptiness-check (Couvreur variant), expect and compute " + << "a counter-example" << std::endl << " -E emptiness-check (Couvreur), expect no counter-example " << std::endl + << " -E2 emptiness-check (Couvreur variant), expect no " + << "counter-example " << std::endl << " -f use Couvreur's FM algorithm for translation" << std::endl << " -F read the formula from the file" << std::endl @@ -69,7 +73,7 @@ main(int argc, char** argv) bool file_opt = false; int output = 0; int formula_index = 0; - enum { None, Couvreur, MagicSearch } echeck = None; + enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None; enum { NoneDup, BFS, DFS } dupexp = NoneDup; bool magic_many = false; bool expect_counter_example = false; @@ -104,12 +108,24 @@ main(int argc, char** argv) expect_counter_example = true; output = -1; } + else if (!strcmp(argv[formula_index], "-e2")) + { + echeck = Couvreur2; + expect_counter_example = true; + output = -1; + } else if (!strcmp(argv[formula_index], "-E")) { echeck = Couvreur; expect_counter_example = false; output = -1; } + else if (!strcmp(argv[formula_index], "-E2")) + { + echeck = Couvreur2; + expect_counter_example = false; + output = -1; + } else if (!strcmp(argv[formula_index], "-f")) { fm_opt = true; @@ -290,9 +306,16 @@ main(int argc, char** argv) case None: break; case Couvreur: + case Couvreur2: { spot::emptiness_check ec = spot::emptiness_check(a); - bool res = ec.check(); + bool res; + + if (echeck == Couvreur) + res = ec.check(); + else + res = ec.check2(); + if (expect_counter_example) { if (res)