From 8d8af2e53a5601dbb0a06508f76a8b973f6fcc7a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 21 Apr 2004 15:18:07 +0000 Subject: [PATCH] * src/ltlvisit/tostring.hh (to_spin_string): New function. Convert a formula into a string parsable by Spin. * src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: New files. Print the never claim in Spin format of a degeneralized TGBA. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/ltl2tgba.cc: Add the option -N which outputs the never claim in Spin format of a degeneralized TGBA. * src/tgbatest/ltl2neverclaim.test: New file. * src/tgbatest/Makefile.am: Add it. --- ChangeLog | 12 +++ lbtt/src/ExternalTranslator.cc | 2 + src/ltlvisit/tostring.cc | 140 +++++++++++++++++++++++- src/ltlvisit/tostring.hh | 9 ++ src/tgbaalgos/Makefile.am | 2 + src/tgbaalgos/neverclaim.cc | 177 +++++++++++++++++++++++++++++++ src/tgbaalgos/neverclaim.hh | 35 ++++++ src/tgbatest/Makefile.am | 1 + src/tgbatest/ltl2neverclaim.test | 41 +++++++ src/tgbatest/ltl2tgba.cc | 14 ++- src/tgbatest/spotlbtt.test | 9 +- 11 files changed, 437 insertions(+), 5 deletions(-) create mode 100644 src/tgbaalgos/neverclaim.cc create mode 100644 src/tgbaalgos/neverclaim.hh create mode 100755 src/tgbatest/ltl2neverclaim.test diff --git a/ChangeLog b/ChangeLog index a91bace2b..5b235e005 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2004-04-21 Denis Poitrenaud + + * src/ltlvisit/tostring.hh (to_spin_string): New function. + Convert a formula into a string parsable by Spin. + * src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: New files. + Print the never claim in Spin format of a degeneralized TGBA. + * src/tgbaalgos/Makefile.am: Add them. + * src/tgbatest/ltl2tgba.cc: Add the option -N which outputs the + never claim in Spin format of a degeneralized TGBA. + * src/tgbatest/ltl2neverclaim.test: New file. + * src/tgbatest/Makefile.am: Add it. + 2004-04-20 Alexandre Duret-Lutz * src/ltltest/defs.in, src/tgbatest/defs.in: Correctly set exitcode diff --git a/lbtt/src/ExternalTranslator.cc b/lbtt/src/ExternalTranslator.cc index 7da7b87d0..9a1043aa4 100644 --- a/lbtt/src/ExternalTranslator.cc +++ b/lbtt/src/ExternalTranslator.cc @@ -108,6 +108,8 @@ void ExternalTranslator::translate string translated_formula; translateFormula(formula, translated_formula); + std::cout << translated_formula << std::endl; + ofstream input_file; input_file.open(external_program_input_file.getName().c_str(), ios::out | ios::trunc); diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index c3b2a7529..81a851f8f 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -11,7 +11,7 @@ // // 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 +// 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 @@ -35,7 +35,7 @@ namespace spot { public: to_string_visitor(std::ostream& os = std::cout) - : os_(os) + : os_(os) { } @@ -147,7 +147,7 @@ namespace spot } os_ << ")"; } - private: + protected: std::ostream& os_; }; @@ -166,5 +166,139 @@ namespace spot to_string(f, os); return os.str(); } + + class to_spin_string_visitor : public to_string_visitor + { + public: + to_spin_string_visitor(std::ostream& os = std::cout) + : to_string_visitor(os) + { + } + + virtual + ~to_spin_string_visitor() + { + } + + void + visit(const binop* bo) + { + os_ << "("; + + switch(bo->op()) + { + case binop::Xor: + os_ << "(!"; + bo->first()->accept(*this); + os_ << " && "; + bo->second()->accept(*this); + os_ << ") || ("; + bo->first()->accept(*this); + os_ << " && !"; + bo->second()->accept(*this); + os_ << ")"; + break; + case binop::Implies: + os_ << "!"; + bo->first()->accept(*this); + os_ << " || "; + bo->second()->accept(*this); + break; + case binop::Equiv: + os_ << "("; + bo->first()->accept(*this); + os_ << " && "; + bo->second()->accept(*this); + os_ << ") || (!"; + bo->first()->accept(*this); + os_ << " && !"; + bo->second()->accept(*this); + os_ << ")"; + case binop::U: + bo->first()->accept(*this); + os_ << " U "; + bo->second()->accept(*this); + break; + case binop::R: + bo->first()->accept(*this); + os_ << " V "; + bo->second()->accept(*this); + break; + } + + os_ << ")"; + } + + void + visit(const unop* uo) + { + // The parser treats X0, and X1 as atomic propositions. So + // make sure we output X(0) and X(1). + bool need_parent = false; + switch(uo->op()) + { + case unop::Not: + os_ << "!"; + break; + case unop::X: + need_parent = !! dynamic_cast(uo->child()); + os_ << "X"; + break; + case unop::F: + os_ << "<>"; + break; + case unop::G: + os_ << "[]"; + break; + } + + if (need_parent) + os_ << "("; + uo->child()->accept(*this); + if (need_parent) + os_ << ")"; + } + + void + visit(const multop* mo) + { + os_ << "("; + unsigned max = mo->size(); + mo->nth(0)->accept(*this); + const char* ch = " "; + switch (mo->op()) + { + case multop::Or: + ch = " || "; + break; + case multop::And: + ch = " && "; + break; + } + + for (unsigned n = 1; n < max; ++n) + { + os_ << ch; + mo->nth(n)->accept(*this); + } + os_ << ")"; + } + }; + + std::ostream& + to_spin_string(const formula* f, std::ostream& os) + { + to_spin_string_visitor v(os); + f->accept(v); + return os; + } + + std::string + to_spin_string(const formula* f) + { + std::ostringstream os; + to_spin_string(f, os); + return os.str(); + } } } diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh index dc4e37eca..3b6558c20 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/tostring.hh @@ -37,6 +37,15 @@ namespace spot /// \brief Convert a formula into a (parsable) string. /// \param f The formula to translate. std::string to_string(const formula* f); + + /// \brief Output a formula as a (parsable by Spin) string. + /// \param f The formula to translate. + /// \param os The stream where it should be output. + std::ostream& to_spin_string(const formula* f, std::ostream& os); + + /// \brief Convert a formula into a (parsable by Spin) string. + /// \param f The formula to translate. + std::string to_spin_string(const formula* f); } } diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 8c9bfcb13..00d01a7b0 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -33,6 +33,7 @@ tgbaalgos_HEADERS = \ ltl2tgba_fm.hh \ ltl2tgba_lacim.hh \ magic.hh \ + neverclaim.hh \ powerset.hh \ reachiter.hh \ save.hh \ @@ -46,6 +47,7 @@ libtgbaalgos_la_SOURCES = \ ltl2tgba_fm.cc \ ltl2tgba_lacim.cc \ magic.cc \ + neverclaim.cc \ powerset.cc \ reachiter.cc \ save.cc \ diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc new file mode 100644 index 000000000..a9826f590 --- /dev/null +++ b/src/tgbaalgos/neverclaim.cc @@ -0,0 +1,177 @@ +// 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 +#include "bdd.h" +#include "tgba/tgbatba.hh" +#include "neverclaim.hh" +#include "tgba/bddprint.hh" +#include "reachiter.hh" +#include "ltlvisit/tostring.hh" +#include "tgba/formula2bdd.hh" +#include "ltlvisit/destroy.hh" + +namespace spot +{ + + class never_claim_bfs : public tgba_reachable_iterator_breadth_first + { + public: + never_claim_bfs(const tgba_tba_proxy* a, std::ostream& os, const ltl::formula* f) + : tgba_reachable_iterator_breadth_first(a), os_(os), f_(f), accept_all_(-1), fi_needed_(false) + { + } + + void + start() + { + os_ << "never {"; + if (f_) + { + os_ << " /* "; + to_spin_string(f_, os_); + os_ << " */"; + } + os_ << std::endl; + init_ = automata_->get_init_state(); + } + + void + end() + { + if (fi_needed_) + os_ << " fi;" << std::endl; + if (accept_all_ != -1) + { + os_ << "accept_all :" << std::endl; + os_ << " skip" << std::endl; + } + os_ << "}" << std::endl; + delete init_; + } + + std::string + get_state_label(const state* s, int n) + { + std::string label; + if (s->compare(init_) == 0) + if (dynamic_cast(automata_)->state_is_accepting(s)) + label = "accept_init"; + else + label = "T0_init"; + else + { + std::ostringstream ost; + ost << n; + std::string ns(ost.str()); + + if (dynamic_cast(automata_)->state_is_accepting(s)) + { + tgba_succ_iterator* it = automata_->succ_iter(s); + it->first(); + if (it->done()) + label = "accept_S" + ns; + else + { + state* current = it->current_state(); + if (it->current_condition() != bddtrue || s->compare(current) != 0) + label = "accept_S" + ns; + else + label = "accept_all"; + delete current; + } + delete it; + } + else + label = "T0_S" + ns; + } + return label; + } + + void + process_state(const state* s, int n, tgba_succ_iterator*) + { + tgba_succ_iterator* it = automata_->succ_iter(s); + it->first(); + if (it->done()) + { + if (fi_needed_ != 0) + os_ << " fi;" << std::endl; + os_ << get_state_label(s, n) << " : "; + os_ << "/* " << automata_->format_state(s) << " */" ; + os_ << std::endl; + os_ << " if" << std::endl; + os_ << " :: (0) -> goto " << get_state_label(s, n) << std::endl; + fi_needed_ = true; + } + else + { + state* current =it->current_state(); + if (dynamic_cast(automata_)->state_is_accepting(s) && + (it->current_condition() == bddtrue) && s->compare(init_) != 0 && + s->compare(current) == 0) + accept_all_ = n; + else + { + if (fi_needed_) + os_ << " fi;" << std::endl; + os_ << get_state_label(s, n) << " : "; + os_ << "/* " << automata_->format_state(s) << " */"; + os_ << std::endl; + os_ << " if" << std::endl; + fi_needed_ = true; + } + delete current; + } + delete it; + } + + void + process_link(int in, int out, const tgba_succ_iterator* si) + { + if (in != accept_all_) + { + os_ << " :: (" ; + const ltl::formula* f = bdd_to_formula(si->current_condition(), automata_->get_dict()); + to_spin_string(f, os_); + destroy(f); + state* current = si->current_state(); + os_ << ") -> goto " << get_state_label(current, out) << std::endl; + delete current; + } + } + + private: + std::ostream& os_; + const ltl::formula* f_; + int accept_all_; + bool fi_needed_; + state* init_; + }; + + std::ostream& + never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g, const ltl::formula* f) + { + never_claim_bfs n(g, os, f); + n.run(); + return os; + } +} diff --git a/src/tgbaalgos/neverclaim.hh b/src/tgbaalgos/neverclaim.hh new file mode 100644 index 000000000..00349e55a --- /dev/null +++ b/src/tgbaalgos/neverclaim.hh @@ -0,0 +1,35 @@ +// 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_NEVERCLAIM_HH +# define SPOT_TGBAALGOS_NEVERCLAIM_HH + +#include +#include "ltlast/formula.hh" +#include "tgba/tgbatba.hh" + +namespace spot +{ + /// \brief Print reachable states in Spin never claim format. + std::ostream& never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g, const ltl::formula* f=0); +} + +#endif // SPOT_TGBAALGOS_NEVERCLAIM_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index e776ccefb..c98d2b33c 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -60,6 +60,7 @@ TESTS = \ tgbaread.test \ readsave.test \ ltl2tgba.test \ + ltl2neverclaim.test \ ltlprod.test \ bddprod.test \ explprod.test \ diff --git a/src/tgbatest/ltl2neverclaim.test b/src/tgbatest/ltl2neverclaim.test new file mode 100755 index 000000000..0ab3766d4 --- /dev/null +++ b/src/tgbatest/ltl2neverclaim.test @@ -0,0 +1,41 @@ +#!/bin/sh +# 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. + + +. ./defs + +set -e + +# We don't check the output, but just running these might be enough to +# trigger assertions. + +run 0 ./ltl2tgba -N -x a +run 0 ./ltl2tgba -N -x 'a U b' +run 0 ./ltl2tgba -N -x 'X a' +run 0 ./ltl2tgba -N -x 'a & b & c' +run 0 ./ltl2tgba -N -x 'a | b | (c U (d & (g U (h ^ i))))' +run 0 ./ltl2tgba -N -x 'Xa & (b U !a) & (b U !a)' +run 0 ./ltl2tgba -N -x 'Fa & Xb & GFc & Gd' +run 0 ./ltl2tgba -N -x 'Fa & Xa & GFc & Gc' +run 0 ./ltl2tgba -N -x 'Fc & X(a | Xb) & GF(a | Xb) & Gc' +run 0 ./ltl2tgba -N -x 'a R (b R c)' +run 0 ./ltl2tgba -N -x '(a U b) U (c U d)' diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 8c28e0bb3..db6a663ad 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -37,6 +37,7 @@ #include "tgbaalgos/gtec/ce.hh" #include "tgbaparse/public.hh" #include "tgbaalgos/dupexp.hh" +#include "tgbaalgos/neverclaim.hh" void syntax(char* prog) @@ -69,6 +70,8 @@ syntax(char* prog) << std::endl << " -n same as -m, but display more counter-examples" << std::endl + << " -N display the never clain for Spin " + << "(implies -D)" << std::endl << " -r display the relation BDD, not the reachability graph" << std::endl << " -R same as -r, but as a set" << std::endl @@ -186,6 +189,11 @@ main(int argc, char** argv) output = -1; magic_many = true; } + else if (!strcmp(argv[formula_index], "-N")) + { + degeneralize_opt = true; + output = 8; + } else if (!strcmp(argv[formula_index], "-r")) { output = 1; @@ -295,7 +303,6 @@ main(int argc, char** argv) fm_symb_merge_opt); else to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict); - spot::ltl::destroy(f); } spot::tgba_tba_proxy* degeneralized = 0; @@ -354,6 +361,9 @@ main(int argc, char** argv) case 7: spot::nonacceptant_lbtt_reachable(std::cout, a); break; + case 8: + spot::never_claim_reachable(std::cout, degeneralized, f); + break; default: assert(!"unknown output option"); } @@ -414,6 +424,8 @@ main(int argc, char** argv) break; } + if (f) + spot::ltl::destroy(f); if (expl) delete expl; if (degeneralize_opt) diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 4aa8d6ee6..afa30a16f 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -70,6 +70,13 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- FM), degeneralized, via never claim" + Path = "${LBTT_TRANSLATE} --spin './ltl2tgba -F -f -N'" + Enabled = yes +} + Algorithm { Name = "Spot (Couvreur -- FM), fake" @@ -257,7 +264,7 @@ FormulaOptions AndPriority = 10 OrPriority = 10 - # XorPriority = 0 + XorPriority = 0 # EquivalencePriority = 0 BeforePriority = 0