diff --git a/ChangeLog b/ChangeLog index c90a17576..bba8d2eb3 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,24 @@ +2011-11-27 Alexandre Duret-Lutz + + Add an ltl2tgba option to read Kripke structure. + + Also offers two ways to output Kripke structures. + + * src/kripketest/parse_print_test.cc, src/kripke/kripkeexplicit.cc + : Simplify includes. + * src/kripke/kripkeprint.hh (kripke_save_reachable, + kripke_save_reachable_renumbered): New declarations. + (KripkePrinter): Move and rename... + * src/kripke/kripkeprint.cc (kripke_printer): ... here. + (kripke_printer_renumbered): New class. + (kripke_save_reachable, kripke_save_reachable_renumbered): New + function. + * src/tgbatest/ltl2tgba.cc: Add an option to read Kripke + structures. + * iface/dve2/dve2check.cc: Use kripke_save_reachable_renumbered. + * iface/dve2/defs.in (run2): Remove. + * iface/dve2/kripke.test: Adjust tests. + 2011-11-27 Alexandre Duret-Lutz * AUTHORS: Add Thomas Badie. diff --git a/iface/dve2/defs.in b/iface/dve2/defs.in index fd8ed2bb7..fc2346ea7 100644 --- a/iface/dve2/defs.in +++ b/iface/dve2/defs.in @@ -1,5 +1,5 @@ # -*- shell-script -*- -# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -88,40 +88,4 @@ run() test $exitcode = $expected_exitcode || exit 1 } - -run2() -{ - expected_exitcode=$1 - shift - exitcode=0 - if test -n "$VALGRIND"; then - exec 6>valgrind.err - GLIBCPP_FORCE_NEW=1 \ - ../../../libtool --mode=execute \ - $VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" | grep -v + > log || - exitcode=$? - cat valgrind.err 1>&2 - test -z "`sed 1q valgrind.err`" || exit 50 - rm -f valgrind.err - else - "$@" || exitcode=$? - fi - test $exitcode = $expected_exitcode || exit 1 - - exec 6>valgrind.err - ../../../libtool --mode=execute \ - $VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q $1 log \ - | grep -v + > log2 || - exitcode=$? - cat valgrind.err 1>&2 - test -z "`sed 1q valgrind.err`" || exit 50 - rm -f valgrind.err - test $exitcode = $expected_exitcode || exit 1 - - diff log log2 || exit 42 - rm -f log log2 - -} - - set -x diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index ee994b489..fc15d31db 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -252,8 +252,7 @@ main(int argc, char **argv) if (output == Kripke) { tm.start("kripke output"); - spot::KripkePrinter p (model, std::cout); - p.run(); + spot::kripke_save_reachable_renumbered(std::cout, model); tm.stop("kripke output"); goto safe_exit; } diff --git a/iface/dve2/kripke.test b/iface/dve2/kripke.test index 984e88267..754dd479f 100755 --- a/iface/dve2/kripke.test +++ b/iface/dve2/kripke.test @@ -33,10 +33,12 @@ else exit 77 fi - set -e -run 0 ${top_builddir}/iface/dve2/dve2check -gK \ -${srcdir}/finite.dve 'F("P.a > 5")' | grep -v + > parse -run2 0 ${top_builddir}/src/kripketest/parse_print parse -rm -f parse +run 0 ../dve2check -gK ${srcdir}/finite.dve 'F("P.a > 5")' > output +run 0 ${top_builddir}/src/kripketest/parse_print output | tr -d '"' > output2 +tr -d '"' < output >outputF +cmp outputF output2 + +../dve2check -gK $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' > outputP +${top_builddir}/src/tgbatest/ltl2tgba -e -KPoutputP '!G("pos[1] < 3")' diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc index 3153f4ff3..8f620f77a 100644 --- a/src/kripke/kripkeexplicit.cc +++ b/src/kripke/kripkeexplicit.cc @@ -20,10 +20,9 @@ #include "kripkeexplicit.hh" -#include "../tgba/bddprint.hh" +#include "tgba/bddprint.hh" #include "tgba/formula2bdd.hh" #include -#include "../tgba/state.hh" namespace spot { diff --git a/src/kripke/kripkeprint.cc b/src/kripke/kripkeprint.cc index be4c312b6..eefb0046a 100644 --- a/src/kripke/kripkeprint.cc +++ b/src/kripke/kripkeprint.cc @@ -21,46 +21,120 @@ #include "kripkeprint.hh" #include "kripkeexplicit.hh" -#include "../tgba/bddprint.hh" +#include "tgba/bddprint.hh" #include "misc/escape.hh" +#include "tgbaalgos/reachiter.hh" #include +#include namespace spot { - KripkePrinter::KripkePrinter(const kripke* automata, - std::ostream& os) - : tgba_reachable_iterator_breadth_first(automata), os_(os) + namespace { - } - void KripkePrinter::start() - { - } - - void KripkePrinter::process_state(const state* s, - int, - tgba_succ_iterator* si) - { - const bdd_dict* d = automata_->get_dict(); - std::string cur = automata_->format_state(s); - os_ << "\""; - escape_str(os_, automata_->format_state(s)); - os_ << "\", \""; - const kripke* automata = down_cast - (automata_); - assert(automata); - escape_str(os_, bdd_format_formula(d, - automata->state_condition(s))); - - os_ << "\","; - for (si->first(); !si->done(); si->next()) + class kripke_printer : public tgba_reachable_iterator_breadth_first { - state* dest = si->current_state(); - os_ << " \""; - escape_str(os_, automata_->format_state(dest)); - os_ << "\""; - } - os_ << ";" << std::endl; + public: + kripke_printer(const kripke* a, std::ostream& os) + : tgba_reachable_iterator_breadth_first(a), os_(os) + { + } + + void process_state(const state* s, int, tgba_succ_iterator* si) + { + const bdd_dict* d = automata_->get_dict(); + os_ << "\""; + escape_str(os_, automata_->format_state(s)); + os_ << "\", \""; + const kripke* automata = down_cast (automata_); + assert(automata); + escape_str(os_, bdd_format_formula(d, + automata->state_condition(s))); + + os_ << "\","; + for (si->first(); !si->done(); si->next()) + { + state* dest = si->current_state(); + os_ << " \""; + escape_str(os_, automata_->format_state(dest)); + os_ << "\""; + } + os_ << ";\n"; + } + + private: + std::ostream& os_; + }; + + class kripke_printer_renumbered : + public tgba_reachable_iterator_breadth_first + { + public: + kripke_printer_renumbered(const kripke* a, std::ostream& os) + : tgba_reachable_iterator_breadth_first(a), os_(os), + notfirst(false) + { + } + + void finish_state() + { + os_ << lastsuccs.str() << ";\n"; + lastsuccs.str(""); + } + + void process_state(const state* s, int in_s, tgba_succ_iterator*) + { + if (notfirst) + finish_state(); + else + notfirst = true; + + const bdd_dict* d = automata_->get_dict(); + std::string cur = automata_->format_state(s); + os_ << "S" << in_s << ", \""; + const kripke* automata = down_cast(automata_); + assert(automata); + escape_str(os_, bdd_format_formula(d, + automata->state_condition(s))); + os_ << "\","; + } + + void + process_link(const state*, int, const state*, int d, + const tgba_succ_iterator*) + { + lastsuccs << " S" << d; + } + + void + end() + { + finish_state(); + } + + private: + std::ostream& os_; + std::ostringstream lastsuccs; + bool notfirst; + }; + } + std::ostream& + kripke_save_reachable(std::ostream& os, const kripke* k) + { + kripke_printer p(k, os); + p.run(); + return os; + } + + std::ostream& + kripke_save_reachable_renumbered(std::ostream& os, const kripke* k) + { + kripke_printer_renumbered p(k, os); + p.run(); + return os; + } + + } // End namespace Spot diff --git a/src/kripke/kripkeprint.hh b/src/kripke/kripkeprint.hh index 124b6f735..eb6ad40f0 100644 --- a/src/kripke/kripkeprint.hh +++ b/src/kripke/kripkeprint.hh @@ -23,30 +23,32 @@ # define SPOT_KRIPKE_KRIPKEPRINT_HH # include -# include "tgbaalgos/reachiter.hh" namespace spot { - class kripke_explicit; - class state_kripke; - class kripke_succ_iterator; class kripke; - /// \brief Iterate over all reachable states of a spot::kripke - /// Override start and process_state methods from - /// tgba_reachable_iterator_breadth_first. - class KripkePrinter : public tgba_reachable_iterator_breadth_first - { - public: - KripkePrinter(const kripke* state, std::ostream& os); + /// \brief Save the reachable part of Kripke structure in text format. + /// + /// The states will be named with the value returned by the + /// kripke::format_state() method. Such a string can be large, so + /// the output will not be I/O efficient. We recommend using this + /// function only for debugging. Use + /// kripke_save_reachable_renumbered() for large output. + /// + /// \ingroup tgba_io + std::ostream& kripke_save_reachable(std::ostream& os, const kripke* k); - void start(); - - void process_state(const state*, int, tgba_succ_iterator* si); - - private: - std::ostream& os_; - }; + /// \brief Save the reachable part of Kripke structure in text format. + /// + /// States will be renumbered with sequential number. This is much + /// more I/O efficient when dumping large Kripke structures with big + /// state names. The drawback is that any information carried by + /// the state name is lost. + /// + /// \ingroup tgba_io + std::ostream& kripke_save_reachable_renumbered(std::ostream& os, + const kripke* k); } // End namespace spot diff --git a/src/kripketest/parse_print_test.cc b/src/kripketest/parse_print_test.cc index e09aac34a..2c6db871a 100644 --- a/src/kripketest/parse_print_test.cc +++ b/src/kripketest/parse_print_test.cc @@ -19,10 +19,8 @@ // 02111-1307, USA. -#include "../kripkeparse/public.hh" -#include "../kripkeparse/parsedecl.hh" -#include "../kripke/kripkeprint.hh" -#include "../tgba/bddprint.hh" +#include "kripkeparse/public.hh" +#include "kripke/kripkeprint.hh" #include "ltlast/allnodes.hh" @@ -30,7 +28,7 @@ using namespace spot; int main(int argc, char** argv) { - int returnValue = 0; + int return_value = 0; kripke_parse_error_list pel; bdd_dict* dict = new bdd_dict; @@ -38,15 +36,11 @@ int main(int argc, char** argv) if (!pel.empty()) { format_kripke_parse_errors(std::cerr, argv[1], pel); - returnValue = 1; + return_value = 1; } - if (!returnValue) - { - KripkePrinter* kp = new KripkePrinter(k, std::cout); - kp->run(); - delete kp; - } + if (!return_value) + kripke_save_reachable(std::cout, k); delete k; delete dict; @@ -54,5 +48,5 @@ int main(int argc, char** argv) assert(ltl::unop::instance_count() == 0); assert(ltl::binop::instance_count() == 0); assert(ltl::multop::instance_count() == 0); - return returnValue; + return return_value; } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index ba6d6d128..05311c6af 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -58,10 +58,11 @@ #include "tgbaalgos/gtec/gtec.hh" #include "eltlparse/public.hh" #include "misc/timer.hh" - #include "tgbaalgos/stats.hh" #include "tgbaalgos/scc.hh" #include "tgbaalgos/emptiness_stats.hh" +#include "tgbaalgos/scc.hh" +#include "kripkeparse/public.hh" std::string ltl_defs() @@ -111,9 +112,10 @@ syntax(char* prog) << std::endl << " -XN do not compute an automaton, read it from a" << " neverclaim file" << std::endl - << " -Pfile multiply the formula automaton with the automaton" - << " from `file'" - << std::endl + << " -Pfile multiply the formula automaton with the TGBA read" + << " from `file'\n" + << " -KPfile multiply the formula automaton with the Kripke" + << " structure from `file'\n" << std::endl << "Translation algorithm:" << std::endl @@ -330,7 +332,7 @@ main(int argc, char** argv) bool spin_comments = false; spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::atomic_prop_set* unobservables = 0; - spot::tgba_explicit_string* system = 0; + spot::tgba* system = 0; const spot::tgba* product = 0; const spot::tgba* product_to_free = 0; spot::bdd_dict* dict = new spot::bdd_dict(); @@ -498,6 +500,18 @@ main(int argc, char** argv) { output = 10; } + else if (!strncmp(argv[formula_index], "-KP", 3)) + { + tm.start("reading -KP's argument"); + + spot::kripke_parse_error_list pel; + system = spot::kripke_parse(argv[formula_index] + 3, + pel, dict, env, debug_opt); + if (spot::format_kripke_parse_errors(std::cerr, + argv[formula_index] + 2, pel)) + return 2; + tm.stop("reading -KP's argument"); + } else if (!strcmp(argv[formula_index], "-KV")) { output = 11; @@ -555,14 +569,15 @@ main(int argc, char** argv) tm.start("reading -P's argument"); spot::tgba_parse_error_list pel; - system = spot::tgba_parse(argv[formula_index] + 2, - pel, dict, env, env, debug_opt); + spot::tgba_explicit_string* s; + s = spot::tgba_parse(argv[formula_index] + 2, + pel, dict, env, env, debug_opt); if (spot::format_tgba_parse_errors(std::cerr, argv[formula_index] + 2, pel)) return 2; - system->merge_transitions(); - + s->merge_transitions(); tm.stop("reading -P's argument"); + system = s; } else if (!strcmp(argv[formula_index], "-r")) {