From 8248072057f88d04f5347d0cb46905ca8a922218 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Apr 2015 13:54:06 +0200 Subject: [PATCH] ltlfilt: add a --define option * src/bin/ltlfilt.cc: Implement it. * src/bin/common_output.cc, src/bin/common_output.hh: export the stream_formula function. * src/ltltest/ltlfilt.test: Test it. * src/ltlvisit/relabel.hh: Make it possible to clear the relabeling map. * NEWS, doc/org/ltlfilt.org: Mention --define. --- NEWS | 4 +++ doc/org/ltlfilt.org | 60 ++++++++++++++++++++++++++++++++++++++++ src/bin/common_output.cc | 3 +- src/bin/common_output.hh | 5 ++++ src/bin/ltlfilt.cc | 30 ++++++++++++++++++-- src/ltltest/ltlfilt.test | 51 ++++++++++++++++++++++++++++++++++ src/ltlvisit/relabel.hh | 11 ++++++-- 7 files changed, 159 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index 0fea8aa1a..11562c107 100644 --- a/NEWS +++ b/NEWS @@ -47,6 +47,10 @@ New in spot 1.99b (not yet released) - ltlfilt has a new --exclusive-ap option to constrain formulas based on a list of mutually exclusive atomic propositions. + - ltlfilt has a new option --define to be used in conjunction with + --relabel or --relabel-bool to print the mapping between old and + new labels. + - all tools that produce formulas or automata now have an --output (a.k.a. -o) option to redirect that output to a file instead of standard output. The name of this file can be constructed using diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 66aad9d04..fc5f871b8 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -184,6 +184,66 @@ Here 29 formulas were reduced into 9 formulas after relabeling of Boolean subexpression and removing of duplicate formulas. In other words the original set of formulas contains 9 different patterns. + +An option that can be used in combination with =--relabel= or +=--relabel-bool= is =--define=. This causes the correspondence of old +a new names to be printed as a set of =#define= statements. + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -f '(a & !b) & GF(a & !b) & FG(!c)' --relabel-bool=pnn --define --spin +#+END_SRC + +#+RESULTS: +: #define p0 (a && !b) +: #define p1 (!c) +: p0 && []<>p0 && <>[]p1 + +This can be used for instance if you want to use some complex atomic +propositions with third-party translators that do not understand them. +For instance the following sequence show how to use =ltl3ba= to create +a neverclaim for an LTL formula containing atomic propositions that +=ltl3ba= cannot parse: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -f '"proc@loc1" U "proc@loc2"' --relabel=pnn --define=ltlex.def --spin | + ltl3ba -F - >ltlex.never +cat ltlex.def ltlex.never +#+END_SRC + +#+RESULTS: +#+begin_example +#define p0 ((proc@loc1)) +#define p1 ((proc@loc2)) +never { /* p0 U p1 */ +T0_init: + if + :: (!p1 && p0) -> goto T0_init + :: (p1) -> goto accept_all + fi; +accept_all: + skip +} +#+end_example + +As a side note, the tool [[file:ltldo.org][=ltldo=]] might be a simpler answer to this syntactic problem: + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo ltl3ba -f '"proc@loc1" U "proc@loc2"' --spin +#+END_SRC +#+RESULTS: +: never { +: T0_init: +: if +: :: ((proc@loc1) && (!(proc@loc2))) -> goto T0_init +: :: ((proc@loc2)) -> goto accept_all +: fi; +: accept_all: +: skip +: } + +This case also relabels the formula before calling =ltl3ba=, and it +then rename all the atomic propositions in the output. + * Filtering =ltlfilt= supports many ways to filter formulas: diff --git a/src/bin/common_output.cc b/src/bin/common_output.cc index 2e0d251fd..920dccc9b 100644 --- a/src/bin/common_output.cc +++ b/src/bin/common_output.cc @@ -77,7 +77,7 @@ report_not_ltl(const spot::ltl::formula* f, error(2, 0, msg, s.c_str(), syn); } -static void +std::ostream& stream_formula(std::ostream& out, const spot::ltl::formula* f, const char* filename, int linenum) { @@ -114,6 +114,7 @@ stream_formula(std::ostream& out, case quiet_output: break; } + return out; } static void diff --git a/src/bin/common_output.hh b/src/bin/common_output.hh index 1f540b7a9..e340f2cd3 100644 --- a/src/bin/common_output.hh +++ b/src/bin/common_output.hh @@ -40,6 +40,11 @@ extern const struct argp output_argp; int parse_opt_output(int key, char* arg, struct argp_state* state); +// Low-level output +std::ostream& +stream_formula(std::ostream& out, + const spot::ltl::formula* f, const char* filename, int linenum); + void output_formula_checked(const spot::ltl::formula* f, const char* filename = 0, int linenum = 0, const char* prefix = 0, const char* suffix = 0); diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index ace159e00..00e976cd9 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -42,6 +42,7 @@ #include "ltlvisit/remove_x.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/exclusive.hh" +#include "ltlvisit/tostring.hh" #include "ltlast/unop.hh" #include "ltlast/multop.hh" #include "tgbaalgos/ltl2tgba_fm.hh" @@ -62,6 +63,7 @@ enum { OPT_BOOLEAN_TO_ISOP, OPT_BSIZE_MAX, OPT_BSIZE_MIN, + OPT_DEFINE, OPT_DROP_ERRORS, OPT_EQUIVALENT_TO, OPT_EXCLUSIVE_AP, @@ -112,6 +114,9 @@ static const argp_option options[] = { "relabel-bool", OPT_RELABEL_BOOL, "abc|pnn", OPTION_ARG_OPTIONAL, "relabel Boolean subexpressions, alphabetically unless " \ "specified otherwise", 0 }, + { "define", OPT_DEFINE, "[FILENAME]", OPTION_ARG_OPTIONAL, + "when used with --relabel or --relabel-bool, output the relabeling map " + "using #define statements", 0 }, { "remove-wm", OPT_REMOVE_WM, 0, 0, "rewrite operators W and M using U and R", 0 }, { "boolean-to-isop", OPT_BOOLEAN_TO_ISOP, 0, 0, @@ -247,6 +252,8 @@ static unsigned ap_n = 0; static int opt_max_count = -1; static long int match_count = 0; static spot::exclusive_ap excl_ap; +static std::unique_ptr output_define = nullptr; + static const spot::ltl::formula* implied_by = 0; static const spot::ltl::formula* imply = 0; @@ -302,6 +309,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_BSIZE_MAX: bsize_max = to_int(arg); break; + case OPT_DEFINE: + output_define.reset(new output_file(arg ? arg : "-")); + break; case OPT_DROP_ERRORS: error_style = drop_errors; break; @@ -427,6 +437,7 @@ namespace public: spot::ltl::ltl_simplifier& simpl; fset_t unique_set; + spot::ltl::relabeling_map relmap; ~ltl_processor() { @@ -531,14 +542,16 @@ namespace { case ApRelabeling: { - const spot::ltl::formula* res = spot::ltl::relabel(f, style); + relmap.clear(); + auto res = spot::ltl::relabel(f, style, &relmap); f->destroy(); f = res; break; } case BseRelabeling: { - const spot::ltl::formula* res = spot::ltl::relabel_bse(f, style); + relmap.clear(); + auto res = spot::ltl::relabel_bse(f, style, &relmap); f->destroy(); f = res; break; @@ -628,6 +641,19 @@ namespace if (matched) { + if (output_define + && output_format != count_output + && output_format != quiet_output) + { + // Sort the formulas alphabetically. + std::map m; + for (auto& p: relmap) + m.emplace(to_string(p.first), p.second); + for (auto& p: m) + stream_formula(output_define->ostream() + << "#define " << p.first << " (", + p.second, filename, linenum) << ")\n"; + } one_match = true; output_formula_checked(f, filename, linenum, prefix, suffix); ++match_count; diff --git a/src/ltltest/ltlfilt.test b/src/ltltest/ltlfilt.test index f88ff036f..0b35e75e2 100755 --- a/src/ltltest/ltlfilt.test +++ b/src/ltltest/ltlfilt.test @@ -171,6 +171,57 @@ EOF run 0 ../../bin/ltlfilt -u --nnf --relabel-bool=pnn in >out diff exp out +cat >exp <(p0 || p2) && <>[](p0 || p2) +#define p0 (b) +#define p1 (a || c) +p0 && []<>p1 && <>[]p1 +#define p0 (h || i) +#define p1 (d && e) +#define p2 (!c) +#define p3 (f) +p0 || []p1 || <>[](p2 || Xp3) +EOF + +run 0 ../../bin/ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out +diff exp out + +cat >exp <out +diff exp out + SPOT_STUTTER_CHECK=0 \ ../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1 test $? = 2 diff --git a/src/ltlvisit/relabel.hh b/src/ltlvisit/relabel.hh index 6b996a51a..924efd177 100644 --- a/src/ltlvisit/relabel.hh +++ b/src/ltlvisit/relabel.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -33,10 +33,17 @@ namespace spot const formula*, ptr_hash> { - ~relabeling_map() + void clear() { for (iterator i = begin(); i != end(); ++i) i->second->destroy(); + this->std::unordered_map>::clear(); + } + + ~relabeling_map() + { + clear(); } }; -- GitLab