From 8c6a2b33d900a160d5026770e1d2c1e86a6387ea Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 10 Nov 2009 17:45:41 +0100 Subject: [PATCH] Do not comment states in the never claim by default. It takes too much time when the formula is large, and it is useless when the purpose is model-checking with Spin. * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Add the comments option. * src/tgbaalgos/neverclaim.cc (never_claim_bfs, never_claim_reachable): Honor the comment option. * src/tgba/tests/ltl2tgba.cc (-N): Do not comment states. (-NN) New option to output a commented never claim. --- ChangeLog | 13 +++++++++++++ src/tgbaalgos/neverclaim.cc | 20 ++++++++++++-------- src/tgbaalgos/neverclaim.hh | 7 +++++-- src/tgbatest/ltl2tgba.cc | 15 ++++++++++++--- 4 files changed, 42 insertions(+), 13 deletions(-) diff --git a/ChangeLog b/ChangeLog index a6d879612..a154df645 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2009-11-10 Alexandre Duret-Lutz + + Do not comment states in the never claim by default. It takes too + much time when the formula is large, and it is useless when the + purpose is model-checking with Spin. + + * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Add the + comments option. + * src/tgbaalgos/neverclaim.cc (never_claim_bfs, + never_claim_reachable): Honor the comment option. + * src/tgba/tests/ltl2tgba.cc (-N): Do not comment states. + (-NN) New option to output a commented never claim. + 2009-11-10 Damien Lefortier * src/tgba/taa.cc, src/tgba/taa.hh: Fix it. diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc index 379341016..d4c372a92 100644 --- a/src/tgbaalgos/neverclaim.cc +++ b/src/tgbaalgos/neverclaim.cc @@ -37,9 +37,10 @@ namespace spot { public: never_claim_bfs(const tgba_sba_proxy* a, std::ostream& os, - const ltl::formula* f) + const ltl::formula* f, bool comments) : tgba_reachable_iterator_breadth_first(a), - os_(os), f_(f), accept_all_(-1), fi_needed_(false) + os_(os), f_(f), accept_all_(-1), fi_needed_(false), + comments_(comments) { } @@ -126,8 +127,9 @@ namespace spot { if (fi_needed_ != 0) os_ << " fi;" << std::endl; - os_ << get_state_label(s, n) << ": "; - os_ << "/* " << automata_->format_state(s) << " */"; + os_ << get_state_label(s, n) << ":"; + if (comments_) + os_ << " /* " << automata_->format_state(s) << " */"; os_ << std::endl; os_ << " if" << std::endl; os_ << " :: (0) -> goto " << get_state_label(s, n) << std::endl; @@ -145,8 +147,9 @@ namespace spot { if (fi_needed_) os_ << " fi;" << std::endl; - os_ << get_state_label(s, n) << ": "; - os_ << "/* " << automata_->format_state(s) << " */"; + os_ << get_state_label(s, n) << ":"; + if (comments_) + os_ << " /* " << automata_->format_state(s) << " */"; os_ << std::endl; os_ << " if" << std::endl; fi_needed_ = true; @@ -179,14 +182,15 @@ namespace spot int accept_all_; bool fi_needed_; state* init_; + bool comments_; }; } // anonymous std::ostream& never_claim_reachable(std::ostream& os, const tgba_sba_proxy* g, - const ltl::formula* f) + const ltl::formula* f, bool comments) { - never_claim_bfs n(g, os, f); + never_claim_bfs n(g, os, f, comments); n.run(); return os; } diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh index 2d2eb562b..f6ccb59a4 100644 --- a/src/tgbaalgos/neverclaim.hh +++ b/src/tgbaalgos/neverclaim.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -35,9 +35,12 @@ namespace spot /// \param g The degeneralized automaton to output. /// \param f The (optional) formula associated to the automaton. If given /// it will be output as a comment. + /// \param comments Whether to comment each state of the never clause + /// with the label of the \a g automaton. std::ostream& never_claim_reachable(std::ostream& os, const tgba_sba_proxy* g, - const ltl::formula* f = 0); + const ltl::formula* f = 0, + bool comments = false); } #endif // SPOT_TGBAALGOS_NEVERCLAIM_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 7535569c5..6e8c8d0ea 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -106,8 +106,10 @@ syntax(char* prog) << " -lS label acceptance conditions on states" << std::endl << " -m try to reduce accepting runs, in a second pass" << std::endl - << " -N display the never clain for Spin " - << "(implies -D)" << std::endl + << " -N display the never clain for Spin (implies -D)" + << std::endl + << " -NN display the never clain for Spin, with commented states" + << " (implies -D)" << std::endl << " -p branching postponement (implies -f)" << std::endl << " -Pfile multiply the formula with the automaton from `file'." << std::endl @@ -200,6 +202,7 @@ main(int argc, char** argv) bool opt_reduce = false; bool containment = false; bool show_fc = false; + 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; @@ -377,6 +380,12 @@ main(int argc, char** argv) degeneralize_opt = DegenSBA; output = 8; } + else if (!strcmp(argv[formula_index], "-NN")) + { + degeneralize_opt = DegenSBA; + output = 8; + spin_comments = true; + } else if (!strcmp(argv[formula_index], "-p")) { post_branching = true; @@ -794,7 +803,7 @@ main(int argc, char** argv) assert(degeneralize_opt == DegenSBA); const spot::tgba_sba_proxy* s = static_cast(degeneralized); - spot::never_claim_reachable(std::cout, s, f); + spot::never_claim_reachable(std::cout, s, f, spin_comments); break; } case 9: