diff --git a/doc/org/tut01.org b/doc/org/tut01.org index dcdf7a9a8..24c0b0a85 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -66,7 +66,6 @@ exceptions. #include #include "ltlparse/public.hh" #include "ltlvisit/tostring.hh" - #include "ltlvisit/lbt.hh" int main() { @@ -98,7 +97,6 @@ parser. Additionally, this give you control over how to print errors. #include #include "ltlparse/public.hh" #include "ltlvisit/tostring.hh" - #include "ltlvisit/lbt.hh" int main() { @@ -144,7 +142,6 @@ with the "fixed" formula if you wish. Here is an example: #include #include "ltlparse/public.hh" #include "ltlvisit/tostring.hh" - #include "ltlvisit/lbt.hh" int main() { diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index 3c3ed2504..37090fb44 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -22,7 +22,6 @@ #include #include #include "ltlvisit/tostring.hh" -#include "ltlvisit/lbt.hh" #include "misc/formater.hh" #include "misc/escape.hh" #include "common_cout.hh" diff --git a/src/bin/common_trans.cc b/src/bin/common_trans.cc index 281c3c5b9..6c8a9c751 100644 --- a/src/bin/common_trans.cc +++ b/src/bin/common_trans.cc @@ -29,7 +29,6 @@ #include "error.h" #include "ltlvisit/tostring.hh" -#include "ltlvisit/lbt.hh" #include "common_conv.hh" // A set of tools for which we know the correct output diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index b8049e813..173ee70c9 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -44,7 +44,6 @@ #include "ltlvisit/apcollect.hh" #include "ltlvisit/mutation.hh" #include "ltlvisit/relabel.hh" -#include "ltlvisit/lbt.hh" #include "twaalgos/lbtt.hh" #include "twaalgos/hoa.hh" #include "twaalgos/product.hh" diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index cae72d8e2..08f989ab5 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -32,7 +32,6 @@ ltlvisit_HEADERS = \ dotty.hh \ dump.hh \ exclusive.hh \ - lbt.hh \ length.hh \ lunabbrev.hh \ mutation.hh \ @@ -56,7 +55,6 @@ libltlvisit_la_SOURCES = \ dotty.cc \ dump.cc \ exclusive.cc \ - lbt.cc \ length.cc \ lunabbrev.cc \ mark.cc \ diff --git a/src/ltlvisit/lbt.cc b/src/ltlvisit/lbt.cc deleted file mode 100644 index 31fe9eef5..000000000 --- a/src/ltlvisit/lbt.cc +++ /dev/null @@ -1,224 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// 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 -#include -#include -#include -#include -#include "ltlast/allnodes.hh" -#include "ltlast/visitor.hh" -#include "lbt.hh" - - -namespace spot -{ - namespace ltl - { - namespace - { - // Does str match p[0-9]+ ? - static bool - is_pnum(const char* str) - { - if (str[0] != 'p' || str[1] == 0) - return false; - while (*++str) - if (*str < '0' || *str > '9') - return false; - return true; - } - - class lbt_visitor: public visitor - { - protected: - std::ostream& os_; - bool first_; - public: - - lbt_visitor(std::ostream& os) - : os_(os), first_(true) - { - } - - void blank() - { - if (first_) - first_ = false; - else - os_ << ' '; - } - - virtual - ~lbt_visitor() - { - } - - void - visit(const atomic_prop* ap) - { - blank(); - std::string str = ap->name(); - if (!is_pnum(str.c_str())) - os_ << '"' << str << '"'; - else - os_ << str; - } - - void - visit(const constant* c) - { - blank(); - switch (c->val()) - { - case constant::False: - os_ << 'f'; - break; - case constant::True: - os_ << 't'; - break; - case constant::EmptyWord: - SPOT_UNIMPLEMENTED(); - break; - } - } - - void - visit(const binop* bo) - { - blank(); - switch (bo->op()) - { - case binop::Xor: - os_ << '^'; - break; - case binop::Implies: - os_ << 'i'; - break; - case binop::Equiv: - os_ << 'e'; - break; - case binop::U: - os_ << 'U'; - break; - case binop::R: - os_ << 'V'; - break; - case binop::W: - os_ << 'W'; - break; - case binop::M: - os_ << 'M'; - break; - case binop::UConcat: - case binop::EConcat: - case binop::EConcatMarked: - SPOT_UNIMPLEMENTED(); - break; - } - bo->first()->accept(*this); - bo->second()->accept(*this); - } - - void - visit(const bunop*) - { - SPOT_UNIMPLEMENTED(); - } - - void - visit(const unop* uo) - { - blank(); - switch (uo->op()) - { - case unop::Not: - os_ << '!'; - break; - case unop::X: - os_ << 'X'; - break; - case unop::F: - os_ << 'F'; - break; - case unop::G: - os_ << 'G'; - break; - case unop::Closure: - case unop::NegClosure: - case unop::NegClosureMarked: - SPOT_UNIMPLEMENTED(); - break; - } - uo->child()->accept(*this); - } - - void - visit(const multop* mo) - { - char o = 0; - switch (mo->op()) - { - case multop::Or: - o = '|'; - break; - case multop::And: - o = '&'; - break; - case multop::OrRat: - case multop::AndRat: - case multop::AndNLM: - case multop::Concat: - case multop::Fusion: - SPOT_UNIMPLEMENTED(); - break; - } - - unsigned n = mo->size(); - for (unsigned i = n - 1; i != 0; --i) - { - blank(); - os_ << o; - } - - for (unsigned i = 0; i < n; ++i) - mo->nth(i)->accept(*this); - } - }; - - } // anonymous - - std::ostream& - to_lbt_string(const formula* f, std::ostream& os) - { - assert(f->is_ltl_formula()); - lbt_visitor v(os); - f->accept(v); - return os; - } - - std::string - to_lbt_string(const formula* f) - { - std::ostringstream os; - to_lbt_string(f, os); - return os.str(); - } - } -} diff --git a/src/ltlvisit/lbt.hh b/src/ltlvisit/lbt.hh deleted file mode 100644 index ef4382085..000000000 --- a/src/ltlvisit/lbt.hh +++ /dev/null @@ -1,59 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// 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 -#include -#include - -namespace spot -{ - namespace ltl - { - /// \addtogroup ltl_io - /// @{ - - /// \brief Output an LTL formula as a string in LBT's format. - /// - /// The formula must be an LTL formula (ELTL and PSL operators - /// are not supported). The M and W operator will be output - /// as-is, because this is accepted by LBTT, however if you - /// plan to use the output with other tools, you should probably - /// rewrite these two operators using unabbreviate_wm(). - /// - /// \param f The formula to translate. - /// \param os The stream where it should be output. - SPOT_API std::ostream& - to_lbt_string(const formula* f, std::ostream& os); - - /// \brief Output an LTL formula as a string in LBT's format. - /// - /// The formula must be an LTL formula (ELTL and PSL operators - /// are not supported). The M and W operator will be output - /// as-is, because this is accepted by LBTT, however if you - /// plan to use the output with other tools, you should probably - /// rewrite these two operators using unabbreviate_wm(). - /// - /// \param f The formula to translate. - SPOT_API std::string - to_lbt_string(const formula* f); - /// @} - } -} diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 21e737300..5b97e074b 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -1025,6 +1025,195 @@ namespace spot return os.str(); } + namespace + { + // Does str match p[0-9]+ ? + static bool + is_pnum(const char* str) + { + if (str[0] != 'p' || str[1] == 0) + return false; + while (*++str) + if (*str < '0' || *str > '9') + return false; + return true; + } + + class lbt_visitor: public visitor + { + protected: + std::ostream& os_; + bool first_; + public: + + lbt_visitor(std::ostream& os) + : os_(os), first_(true) + { + } + + void blank() + { + if (first_) + first_ = false; + else + os_ << ' '; + } + + virtual + ~lbt_visitor() + { + } + + void + visit(const atomic_prop* ap) + { + blank(); + std::string str = ap->name(); + if (!is_pnum(str.c_str())) + os_ << '"' << str << '"'; + else + os_ << str; + } + + void + visit(const constant* c) + { + blank(); + switch (c->val()) + { + case constant::False: + os_ << 'f'; + break; + case constant::True: + os_ << 't'; + break; + case constant::EmptyWord: + SPOT_UNIMPLEMENTED(); + break; + } + } + + void + visit(const binop* bo) + { + blank(); + switch (bo->op()) + { + case binop::Xor: + os_ << '^'; + break; + case binop::Implies: + os_ << 'i'; + break; + case binop::Equiv: + os_ << 'e'; + break; + case binop::U: + os_ << 'U'; + break; + case binop::R: + os_ << 'V'; + break; + case binop::W: + os_ << 'W'; + break; + case binop::M: + os_ << 'M'; + break; + case binop::UConcat: + case binop::EConcat: + case binop::EConcatMarked: + SPOT_UNIMPLEMENTED(); + break; + } + bo->first()->accept(*this); + bo->second()->accept(*this); + } + + void + visit(const bunop*) + { + SPOT_UNIMPLEMENTED(); + } + + void + visit(const unop* uo) + { + blank(); + switch (uo->op()) + { + case unop::Not: + os_ << '!'; + break; + case unop::X: + os_ << 'X'; + break; + case unop::F: + os_ << 'F'; + break; + case unop::G: + os_ << 'G'; + break; + case unop::Closure: + case unop::NegClosure: + case unop::NegClosureMarked: + SPOT_UNIMPLEMENTED(); + break; + } + uo->child()->accept(*this); + } + + void + visit(const multop* mo) + { + char o = 0; + switch (mo->op()) + { + case multop::Or: + o = '|'; + break; + case multop::And: + o = '&'; + break; + case multop::OrRat: + case multop::AndRat: + case multop::AndNLM: + case multop::Concat: + case multop::Fusion: + SPOT_UNIMPLEMENTED(); + break; + } + + unsigned n = mo->size(); + for (unsigned i = n - 1; i != 0; --i) + { + blank(); + os_ << o; + } + + for (unsigned i = 0; i < n; ++i) + mo->nth(i)->accept(*this); + } + }; + + } // anonymous + + std::ostream& + to_lbt_string(const formula* f, std::ostream& os) + { + assert(f->is_ltl_formula()); + lbt_visitor v(os); + f->accept(v); + return os; + } + + std::string + to_lbt_string(const formula* f) + { + std::ostringstream os; + to_lbt_string(f, os); + return os.str(); + } } } diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh index 5f7a7603c..150e134e7 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/tostring.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // 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. @@ -143,6 +143,31 @@ namespace spot SPOT_API std::string to_sclatex_string(const formula* f, bool full_parent = false, bool ratexp = false); + + /// \brief Output an LTL formula as a string in LBT's format. + /// + /// The formula must be an LTL formula (ELTL and PSL operators + /// are not supported). The M and W operator will be output + /// as-is, because this is accepted by LBTT, however if you + /// plan to use the output with other tools, you should probably + /// rewrite these two operators using unabbreviate_wm(). + /// + /// \param f The formula to translate. + /// \param os The stream where it should be output. + SPOT_API std::ostream& + to_lbt_string(const formula* f, std::ostream& os); + + /// \brief Output an LTL formula as a string in LBT's format. + /// + /// The formula must be an LTL formula (ELTL and PSL operators + /// are not supported). The M and W operator will be output + /// as-is, because this is accepted by LBTT, however if you + /// plan to use the output with other tools, you should probably + /// rewrite these two operators using unabbreviate_wm(). + /// + /// \param f The formula to translate. + SPOT_API std::string + to_lbt_string(const formula* f); /// @} } } diff --git a/src/twaalgos/lbtt.cc b/src/twaalgos/lbtt.cc index 1cfac8b91..f9b81cb50 100644 --- a/src/twaalgos/lbtt.cc +++ b/src/twaalgos/lbtt.cc @@ -28,7 +28,7 @@ #include "reachiter.hh" #include "misc/bddlt.hh" #include "priv/accmap.hh" -#include "ltlvisit/lbt.hh" +#include "ltlvisit/tostring.hh" #include "ltlparse/public.hh" namespace spot diff --git a/wrap/python/spot_impl.i b/wrap/python/spot_impl.i index 37ea3d80d..5580c5ef8 100644 --- a/wrap/python/spot_impl.i +++ b/wrap/python/spot_impl.i @@ -104,7 +104,6 @@ namespace std { #include "ltlvisit/simplify.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/tunabbrev.hh" -#include "ltlvisit/lbt.hh" #include "ltlvisit/randomltl.hh" #include "ltlvisit/length.hh" #include "ltlvisit/remove_x.hh" @@ -247,7 +246,6 @@ using namespace spot; %include "ltlvisit/simplify.hh" %include "ltlvisit/tostring.hh" %include "ltlvisit/tunabbrev.hh" -%include "ltlvisit/lbt.hh" %include "ltlvisit/randomltl.hh" %include "ltlvisit/length.hh" %include "ltlvisit/remove_x.hh"