From 8af99968637e484b4fd55e2c4a2f4371ec5d4f7e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 9 Jul 2003 14:11:25 +0000 Subject: [PATCH] * src/ExternalTranslator.h (class ExternalTranslator): Declare class SpotWrapper as a friend. * src/SpotWrapper.h, src/SpotWrapper.cc: New files. * src/Makefile.am (lbtt_translate_SOURCES): Add SpotWrapper.cc and SpotWrapper.h. * src/translate.cc (main): Add the --spot option, and build a SpotWrapper of required. --- lbtt/ChangeLog | 10 +++ lbtt/src/ExternalTranslator.h | 5 +- lbtt/src/Makefile.am | 30 +++++-- lbtt/src/SpotWrapper.cc | 105 ++++++++++++++++++++++++ lbtt/src/SpotWrapper.h | 146 ++++++++++++++++++++++++++++++++++ lbtt/src/translate.cc | 49 +++++++----- 6 files changed, 317 insertions(+), 28 deletions(-) create mode 100644 lbtt/src/SpotWrapper.cc create mode 100644 lbtt/src/SpotWrapper.h diff --git a/lbtt/ChangeLog b/lbtt/ChangeLog index 21c506766..f3db77441 100644 --- a/lbtt/ChangeLog +++ b/lbtt/ChangeLog @@ -1,3 +1,13 @@ +2003-07-09 Alexandre Duret-Lutz + + * src/ExternalTranslator.h (class ExternalTranslator): + Declare class SpotWrapper as a friend. + * src/SpotWrapper.h, src/SpotWrapper.cc: New files. + * src/Makefile.am (lbtt_translate_SOURCES): Add SpotWrapper.cc + and SpotWrapper.h. + * src/translate.cc (main): Add the --spot option, and build + a SpotWrapper of required. + 2003-07-04 Alexandre Duret-Lutz * src/Config-parse.yy: Remove stray `,' in %token arguments. diff --git a/lbtt/src/ExternalTranslator.h b/lbtt/src/ExternalTranslator.h index 4835f6ef0..0ecac54cb 100644 --- a/lbtt/src/ExternalTranslator.h +++ b/lbtt/src/ExternalTranslator.h @@ -210,8 +210,8 @@ private: */ stack > /* information. */ + deque > /* information. */ temporary_file_objects; friend class KecWrapper; /* Friend declarations. */ @@ -219,6 +219,7 @@ private: friend class Ltl2BaWrapper; friend class ProdWrapper; friend class SpinWrapper; + friend class SpotWrapper; friend class WringWrapper; /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ diff --git a/lbtt/src/Makefile.am b/lbtt/src/Makefile.am index 4c45bc70d..20d7bdcb5 100644 --- a/lbtt/src/Makefile.am +++ b/lbtt/src/Makefile.am @@ -13,10 +13,30 @@ UserCommands.cc EXTRA_lbtt_SOURCES = gnu-getopt.h Config-parse.h lbtt_LDADD = @LIBOBJS@ @READLINELIBS@ -lbtt_translate_SOURCES = Alloc.h BitArray.h BitArray.cc Exception.h \ -ExternalTranslator.h ExternalTranslator.cc FormulaWriter.h LbtWrapper.h \ -LtlFormula.h LtlFormula.cc NeverClaim-parse.yy NeverClaim-lex.ll \ -NeverClaimAutomaton.h NeverClaimAutomaton.cc SpinWrapper.h SpinWrapper.cc \ -StringUtil.h StringUtil.cc translate.h translate.cc TranslatorInterface.h +lbtt_translate_SOURCES = \ + Alloc.h \ + BitArray.h \ + BitArray.cc \ + Exception.h \ + ExternalTranslator.h \ + ExternalTranslator.cc \ + FormulaWriter.h \ + LbtWrapper.h \ + LtlFormula.h \ + LtlFormula.cc \ + NeverClaim-parse.yy \ + NeverClaim-lex.ll \ + NeverClaimAutomaton.h \ + NeverClaimAutomaton.cc \ + SpinWrapper.h \ + SpinWrapper.cc \ + SpotWrapper.h \ + SpotWrapper.cc \ + StringUtil.h \ + StringUtil.cc \ + translate.h \ + translate.cc \ + TranslatorInterface.h + EXTRA_lbtt_translate_SOURCES = gnu-getopt.h NeverClaim-parse.h lbtt_translate_LDADD = @LIBOBJS@ diff --git a/lbtt/src/SpotWrapper.cc b/lbtt/src/SpotWrapper.cc new file mode 100644 index 000000000..cc93e4535 --- /dev/null +++ b/lbtt/src/SpotWrapper.cc @@ -0,0 +1,105 @@ +/* + * Copyright (C) 2003 + * Heikki Tauriainen + * + * Derived from SpinWrapper.cc by Alexandre Duret-Lutz . + * + * This program 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. + * + * This program 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, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#ifdef __GNUC__ +#pragma implementation +#endif /* __GNUC__ */ + +#include +#ifdef HAVE_SSTREAM +#include +#else +#include +#endif /* HAVE_SSTREAM */ +#include "Exception.h" +#include "FormulaWriter.h" +#include "NeverClaimAutomaton.h" +#include "SpotWrapper.h" + +/****************************************************************************** + * + * Definitions for operator symbols specific to Spot. + * + *****************************************************************************/ + +const char SpotWrapper::SPOT_AND[] = "&"; +const char SpotWrapper::SPOT_OR[] = "|"; + + + +/****************************************************************************** + * + * Function definitions for class SpotWrapper. + * + *****************************************************************************/ + +/* ========================================================================= */ +void SpotWrapper::translateFormula + (const ::Ltl::LtlFormula& formula, string& translated_formula) +/* ---------------------------------------------------------------------------- + * + * Description: Translates an LtlFormula into a string which contains the + * formula in the input syntax of Spot. + * + * Arguments: formula -- The LtlFormula to be translated. + * translated_formula -- A reference to a string for storing + * the results. + * + * Returns: Nothing. The result of the translation can be found in + * the string `translated_formula'. + * + * ------------------------------------------------------------------------- */ +{ + using namespace Ltl; + +#ifdef HAVE_SSTREAM + ostringstream translated_formula_stream; +#else + ostrstream translated_formula_stream; +#endif /* HAVE_SSTREAM */ + Exceptional_ostream estream(&translated_formula_stream, ios::goodbit); + + FormulaWriter, + ConstantWriter, + AtomWriter, + UnaryOperatorWriter, + UnaryOperatorWriter, + UnaryOperatorWriter, + UnaryOperatorWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + BinaryOperatorInfixWriter, + WriterErrorReporter, + WriterErrorReporter, + WriterErrorReporter> + fw(estream); + + formula.traverse(fw, LTL_PREORDER | LTL_INORDER | LTL_POSTORDER); + + translated_formula = translated_formula_stream.str(); +#ifndef HAVE_SSTREAM + translated_formula_stream.freeze(0); +#endif /* HAVE_SSTREAM */ +} diff --git a/lbtt/src/SpotWrapper.h b/lbtt/src/SpotWrapper.h new file mode 100644 index 000000000..1975ac2ad --- /dev/null +++ b/lbtt/src/SpotWrapper.h @@ -0,0 +1,146 @@ +/* + * Copyright (C) 2003 + * Heikki Tauriainen + * + * Derived from SpinWrapper.h by Alexandre Duret-Lutz . + * + * This program 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. + * + * This program 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, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. + */ + +#ifndef SPOTWRAPPER_H +#define SPOTWRAPPER_H + +#ifdef __GNUC__ +#pragma interface +#endif /* __GNUC__ */ + +#include +#include +#include "ExternalTranslator.h" +#include "LtlFormula.h" + +/****************************************************************************** + * + * Interface class for Spot. + * + *****************************************************************************/ + +class SpotWrapper : public ExternalTranslator +{ +public: + SpotWrapper(); /* Constructor. */ + + ~SpotWrapper(); /* Destructor. */ + + void translateFormula /* Translates a formula */ + (const ::Ltl::LtlFormula& formula, /* into a Büchi */ + string& translated_formula); /* automaton. */ + + /* `formatInput' inherited from ExternalTranslator */ + + string commandLine /* Prepares the command */ + (const string& input_filename, /* line for executing */ + const string& output_filename); /* Spot. */ + + /* `execSuccess' inherited from ExternalTranslator */ + + void parseAutomaton /* Translates the output */ + (const string& input_filename, /* of the translation */ + const string& output_filename); /* algorithm into lbtt + * format. + */ + +private: + SpotWrapper(const SpotWrapper&); /* Prevent copying and */ + SpotWrapper& operator=(const SpotWrapper&); /* assignment of + * SpotWrapper objects. + */ + + static const char SPOT_AND[]; /* Symbols for */ + static const char SPOT_OR[]; /* operators. */ +}; + + + +/****************************************************************************** + * + * Inline function definitions for class SpotWrapper. + * + *****************************************************************************/ + +/* ========================================================================= */ +inline SpotWrapper::SpotWrapper() +/* ---------------------------------------------------------------------------- + * + * Description: Constructor for class SpotWrapper. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline SpotWrapper::~SpotWrapper() +/* ---------------------------------------------------------------------------- + * + * Description: Destructor for class SpotWrapper. + * + * Arguments: None. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +/* ========================================================================= */ +inline string SpotWrapper::commandLine + (const string& input_filename, const string&) +/* ---------------------------------------------------------------------------- + * + * Description: Prepares the command line for Spot. + * + * Arguments: input_filename -- Name of the input file. + * The other argument is only needed for supporting the + * ExternalTranslator interface; the output will be written to + * the filename stored in `command_line_arguments[4]'. + * + * Returns: The command line string. + * + * ------------------------------------------------------------------------- */ +{ + return (string(" ") + input_filename + + " >" + string(command_line_arguments[4])); +} + +/* ========================================================================= */ +inline void SpotWrapper::parseAutomaton(const string&, const string&) +/* ---------------------------------------------------------------------------- + * + * Description: Dummy function which is needed to support the + * ExternalTranslator interface. + * + * Arguments: References to two constant strings. + * + * Returns: Nothing. + * + * ------------------------------------------------------------------------- */ +{ +} + +#endif /* !SPINWRAPPER_H */ diff --git a/lbtt/src/translate.cc b/lbtt/src/translate.cc index bf2679c74..4b2d3577e 100644 --- a/lbtt/src/translate.cc +++ b/lbtt/src/translate.cc @@ -1,5 +1,5 @@ /* - * Copyright (C) 1999, 2000, 2001, 2002 + * Copyright (C) 1999, 2000, 2001, 2002, 2003 * Heikki Tauriainen * * This program is free software; you can redistribute it and/or @@ -29,6 +29,7 @@ #include "LbtWrapper.h" #include "LtlFormula.h" #include "SpinWrapper.h" +#include "SpotWrapper.h" #ifdef HAVE_GETOPT_LONG #include #define OPTIONSTRUCT struct option @@ -52,7 +53,7 @@ char** command_line_arguments; /****************************************************************************** * * A function for showing warnings to the user. - * + * *****************************************************************************/ void printWarning(const string& msg) @@ -87,7 +88,7 @@ RETSIGTYPE signalHandler(int signal_number) int main(int argc, char** argv) { - typedef enum {OPT_HELP = 'h', OPT_LBT, OPT_SPIN, OPT_VERSION = 'v'} + typedef enum {OPT_HELP = 'h', OPT_LBT, OPT_SPIN, OPT_SPOT, OPT_VERSION = 'v'} OptionType; static OPTIONSTRUCT command_line_options[] = @@ -95,6 +96,7 @@ int main(int argc, char** argv) {"help", no_argument, 0, OPT_HELP}, {"lbt", no_argument, 0, OPT_LBT}, {"spin", no_argument, 0, OPT_SPIN}, + {"spot", no_argument, 0, OPT_SPOT}, {"version", no_argument, 0, OPT_VERSION}, {0, 0, 0, 0} }; @@ -117,19 +119,20 @@ int main(int argc, char** argv) case OPT_HELP : cout << string("Usage: ") << command_line_arguments[0] << " [translator] [command line for translator] [formula " - "file] [automaton file]\n" - "General options:\n" - " --h, --help Show this help\n" - " --v, --version Show version and exit\n\n" - "Translator options:\n" - " --lbt lbt\n" - " --spin Spin\n" - "The command line for these translators must be given as a " - "single argument\n" - "including the name (and location) of an external program to " - "execute, together\n" - "with any optional parameters to be passed to the " - "program.\n\n"; + "file] [automaton file]\n" + "General options:\n" + " --h, --help Show this help\n" + " --v, --version Show version and exit\n\n" + "Translator options:\n" + " --lbt lbt\n" + " --spin Spin\n" + " --spot Spot\n" + "The command line for these translators must be given as a " + "single argument\n" + "including the name (and location) of an external program to " + "execute, together\n" + "with any optional parameters to be passed to the " + "program.\n\n"; exit(0); break; @@ -141,13 +144,17 @@ int main(int argc, char** argv) translator = new SpinWrapper(); break; + case OPT_SPOT : + translator = new SpotWrapper(); + break; + case OPT_VERSION : cout << "lbtt-translate " PACKAGE_VERSION "\n" - "lbtt-translate is free software; you may change and " - "redistribute it under the\n" - "terms of the GNU General Public License. lbtt-translate " - "comes with NO WARRANTY.\n" - "See the file COPYING for details.\n"; + "lbtt-translate is free software; you may change and " + "redistribute it under the\n" + "terms of the GNU General Public License. lbtt-translate " + "comes with NO WARRANTY.\n" + "See the file COPYING for details.\n"; exit(0); break;