From 0fc3c6bcff5d1838e52bcb6801b1da0a07d64795 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 20 Oct 2012 13:32:05 +0200 Subject: [PATCH] Add support for printing LTL formulas using Wring's syntax. * src/ltlvisit/tostring.hh, src/ltlvisit/tostring.cc (to_wring_string): New option. * src/bin/common_output.hh, src/bin/common_output.cc: Add support for a --wring option. * src/bin/ltlcheck.cc: Add %w and %W format specifiers. --- src/bin/common_output.cc | 11 +++++++ src/bin/common_output.hh | 3 +- src/bin/ltlcheck.cc | 19 +++++++++--- src/ltlvisit/tostring.cc | 63 ++++++++++++++++++++++++++++++++++++++++ src/ltlvisit/tostring.hh | 13 +++++++-- 5 files changed, 102 insertions(+), 7 deletions(-) diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index 54f96c1f8..c967361bb 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -26,6 +26,7 @@ #include "error.h" #define OPT_SPOT 1 +#define OPT_WRING 2 output_format_t output_format = spot_output; bool full_parenth = false; @@ -37,6 +38,7 @@ static const argp_option options[] = { "spin", 's', 0, 0, "output in Spin's syntax", -20 }, { "spot", OPT_SPOT, 0, 0, "output in Spot's syntax (default)", -20 }, { "lbt", 'l', 0, 0, "output in LBT's syntax", -20 }, + { "wring", OPT_WRING, 0, 0, "output in Wring's syntax", -20 }, { "utf8", '8', 0, 0, "output using UTF-8 characters", -20 }, { 0, 0, 0, 0, 0, 0 } }; @@ -64,6 +66,9 @@ parse_opt_output(int key, char*, struct argp_state*) case OPT_SPOT: output_format = spot_output; break; + case OPT_WRING: + output_format = wring_output; + break; default: return ARGP_ERR_UNKNOWN; } @@ -105,6 +110,12 @@ output_formula(const spot::ltl::formula* f, const char* filename, int linenum) else report_not_ltl(f, filename, linenum, "Spin"); break; + case wring_output: + if (f->is_ltl_formula()) + spot::ltl::to_wring_string(f, std::cout); + else + report_not_ltl(f, filename, linenum, "Wring"); + break; case utf8_output: spot::ltl::to_utf8_string(f, std::cout, full_parenth); break; diff --git a/src/bin/common_output.hh b/src/bin/common_output.hh index 2209f952c..78af51a69 100644 --- a/src/bin/common_output.hh +++ b/src/bin/common_output.hh @@ -25,7 +25,8 @@ #include #include "ltlast/formula.hh" -enum output_format_t { spot_output, spin_output, utf8_output, lbt_output }; +enum output_format_t { spot_output, spin_output, utf8_output, + lbt_output, wring_output }; extern output_format_t output_format; extern bool full_parenth; diff --git a/src/bin/ltlcheck.cc b/src/bin/ltlcheck.cc index 35ab365f5..3376bf304 100644 --- a/src/bin/ltlcheck.cc +++ b/src/bin/ltlcheck.cc @@ -92,10 +92,11 @@ static const argp_option options[] = { 0, 0, 0, 0, "COMMANDFMT should specify input and output arguments using the " "following character sequences:", 3 }, - { "%f,%s,%l", 0, 0, OPTION_DOC | OPTION_NO_USAGE, - "the formula as a (quoted) string in Spot, Spin, or LBT's syntax", 0 }, - { "%F,%S,%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE, - "the formula as a file in Spot, Spin, or LBT's syntax", 0 }, + { "%f,%s,%l,%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the formula as a (quoted) string in Spot, Spin, LBT, or Wring's syntax", + 0 }, + { "%F,%S,%L,%W", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 }, { "%N,%T", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "the output automaton as a Never claim, or in LBTT's format", 0 }, { 0, 0, 0, 0, @@ -458,9 +459,11 @@ namespace quoted_string string_ltl_spot; quoted_string string_ltl_spin; quoted_string string_ltl_lbt; + quoted_string string_ltl_wring; quoted_string filename_ltl_spot; quoted_string filename_ltl_spin; quoted_string filename_ltl_lbt; + quoted_string filename_ltl_wring; // Run-specific variables printable_result_filename output; public: @@ -472,9 +475,11 @@ namespace declare('f', &string_ltl_spot); declare('s', &string_ltl_spin); declare('l', &string_ltl_lbt); + declare('w', &string_ltl_wring); declare('F', &filename_ltl_spot); declare('S', &filename_ltl_spin); declare('L', &filename_ltl_lbt); + declare('W', &filename_ltl_wring); declare('N', &output); declare('T', &output); @@ -503,6 +508,8 @@ namespace return string_ltl_spot; if (!string_ltl_spin.val().empty()) return string_ltl_spin; + if (!string_ltl_wring.val().empty()) + return string_ltl_wring; if (!string_ltl_lbt.val().empty()) return string_ltl_lbt; error(2, 0, "None of the translators need the input formula?"); @@ -518,12 +525,16 @@ namespace string_ltl_spin = spot::ltl::to_spin_string(f, true); if (has('l') || has('L')) string_ltl_lbt = spot::ltl::to_lbt_string(f); + if (has('w') || has('W')) + string_ltl_wring = spot::ltl::to_wring_string(f); if (has('F')) string_to_tmp(string_ltl_spot, serial, filename_ltl_spot); if (has('S')) string_to_tmp(string_ltl_spin, serial, filename_ltl_spin); if (has('L')) string_to_tmp(string_ltl_lbt, serial, filename_ltl_lbt); + if (has('W')) + string_to_tmp(string_ltl_wring, serial, filename_ltl_wring); } const spot::tgba* diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 35233e3e7..8cf15a4a9 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -128,6 +128,36 @@ namespace spot ":", // not supported }; + const char* wring_kw[] = { + "FALSE", + "TRUE", + "[*0]", // not supported + " ^ ", + " -> ", + " <-> ", + " U ", + " R ", + " W ", // rewritten + " M ", // rewritten + "<>-> ", // not supported + "<>=> ", // not supported + "<>+> ", // not supported + "<>=+> ", // not supported + "[]-> ", // not supported + "[]=> ", // not supported + "!", + "X", + "F", + "G", + " + ", + " | ", // not supported + " * ", + " && ", // not supported + " & ", // not supported + ";", // not supported + ":", // not supported + }; + const char* utf8_kw[] = { "0", "1", @@ -262,6 +292,8 @@ namespace spot { os_ << str; } + if (kw_ == wring_kw) + os_ << "=1"; if (full_parent_) os_ << ")"; } @@ -518,6 +550,15 @@ namespace spot overline = true; break; } + // If we negate an atomic proposition for Wring, + // output prop=0. + if (kw_ == wring_kw) + if (const ltl::atomic_prop* ap = is_atomic_prop(uo->child())) + if (is_bare_word(ap->name().c_str())) + { + os_ << ap->name() << "=0"; + goto skiprec; + } emit(KNot); break; case unop::X: @@ -570,6 +611,8 @@ namespace spot break; } + skiprec: + if (full_parent_ && !top_level) closep(); else if (overline) @@ -782,5 +825,25 @@ namespace spot to_spin_string(f, os, full_parent); return os.str(); } + + std::ostream& + to_wring_string(const formula* f, std::ostream& os) + { + // Remove W and M. + f = unabbreviate_wm(f); + to_string_visitor v(os, true, false, wring_kw); + f->accept(v); + f->destroy(); + return os; + } + + std::string + to_wring_string(const formula* f) + { + std::ostringstream os; + to_wring_string(f, os); + return os.str(); + } + } } diff --git a/src/ltlvisit/tostring.hh b/src/ltlvisit/tostring.hh index 47ef51b69..70189678f 100644 --- a/src/ltlvisit/tostring.hh +++ b/src/ltlvisit/tostring.hh @@ -74,7 +74,7 @@ namespace spot to_utf8_string(const formula* f, bool full_parent = false, bool ratexp = false); - /// \brief Output a formula as a (parsable by Spin) string. + /// \brief Output a formula as a string parsable by Spin. /// \param f The formula to translate. /// \param os The stream where it should be output. /// \param full_parent Whether or not the string should by fully @@ -82,12 +82,21 @@ namespace spot std::ostream& to_spin_string(const formula* f, std::ostream& os, bool full_parent = false); - /// \brief Convert a formula into a (parsable by Spin) string. + /// \brief Convert a formula into a string parsable by Spin. /// \param f The formula to translate. /// \param full_parent Whether or not the string should by fully /// parenthesized. std::string to_spin_string(const formula* f, bool full_parent = false); + /// \brief Output a formula as a string parsable by Wring. + /// \param f The formula to translate. + /// \param os The stream where it should be output. + std::ostream& to_wring_string(const formula* f, std::ostream& os); + + /// \brief Convert a formula into a string parsable by Wring + /// \param f The formula to translate. + std::string to_wring_string(const formula* f); + /// @} } }