From 6fa42c90b8b4c9fde09245dfdb236c14709843f8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 23 Aug 2024 17:22:17 +0200 Subject: [PATCH] ltlfilt: add support for --relabel=io, --ins, and --outs * bin/common_ioap.cc, bin/common_ioap.hh (relabel_io): New function. * bin/ltlfilt.cc: Implement the above options. * doc/org/ltlfilt.org, NEWS: Illustrate them. * tests/core/ltlfilt.test: Add some quick tests. --- NEWS | 10 +++++ bin/common_ioap.cc | 34 +++++++++++++++ bin/common_ioap.hh | 6 +++ bin/ltlfilt.cc | 38 +++++++++++++++- doc/org/ltlfilt.org | 41 +++++++++++++++++- tests/core/ltlfilt.test | 96 +++++++++++++++++++++++++++++++++++++++++ 6 files changed, 222 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index 178ba5327..cacacf5d2 100644 --- a/NEWS +++ b/NEWS @@ -5,6 +5,16 @@ New in spot 2.12.0.dev (not yet released) - ltlmix is a new tool that generate formulas by combining existing ones. See https://spot.lre.epita.fr/ltlmix.html for examples. + - ltlfilt learned a --relabel=io mode, that is useful to shorten + atomic propositions in the context of LTL synthesis. For instance + + % ltlfilt -f 'G(req->Fack)&G(go->Fgrant)' --relabel=io --ins=req,go + G(i1 -> Fo0) & G(i0 -> Fo1) + + The resulting formulas are now usable by ltlsynt without having to + specify which atomic propositions are input or output, as this can + be inferred from their name. + - autfilt learned --restrict-dead-end-edges, to restricts labels of edges leading to dead-ends. See the description of restrict_dead_end_edges_here() below. diff --git a/bin/common_ioap.cc b/bin/common_ioap.cc index d38a190aa..312334051 100644 --- a/bin/common_ioap.cc +++ b/bin/common_ioap.cc @@ -164,3 +164,37 @@ filter_list_of_aps(spot::formula f, const char* filename, int linenum) } return {matched[0], matched[1]}; } + + +spot::formula relabel_io(spot::formula f, spot::relabeling_map& fro, + const char* filename, int linenum) +{ + auto [ins, outs] = filter_list_of_aps(f, filename, linenum); + // Different implementation of unordered_set, usinged in + // filter_list_of_aps can cause aps to be output in different order. + // Let's sort everything for the sake of determinism. + std::sort(ins.begin(), ins.end()); + std::sort(outs.begin(), outs.end()); + spot::relabeling_map to; + unsigned ni = 0; + for (std::string& i: ins) + { + std::ostringstream s; + s << 'i' << ni++; + spot::formula a1 = spot::formula::ap(i); + spot::formula a2 = spot::formula::ap(s.str()); + fro[a2] = a1; + to[a1] = a2; + } + unsigned no = 0; + for (std::string& o: outs) + { + std::ostringstream s; + s << 'o' << no++; + spot::formula a1 = spot::formula::ap(o); + spot::formula a2 = spot::formula::ap(s.str()); + fro[a2] = a1; + to[a1] = a2; + } + return spot::relabel_apply(f, &to); +} diff --git a/bin/common_ioap.hh b/bin/common_ioap.hh index 960b26a8a..cc20c61a5 100644 --- a/bin/common_ioap.hh +++ b/bin/common_ioap.hh @@ -25,6 +25,7 @@ #include #include #include +#include // --ins and --outs, as supplied on the command-line extern std::optional> all_output_aps; @@ -49,3 +50,8 @@ extern std::unordered_map identifier_map; // regex_out, and identifier_map. std::pair, std::vector> filter_list_of_aps(spot::formula f, const char* filename, int linenum); + + +// Relabel APs incrementally, based on i/o class. +spot::formula relabel_io(spot::formula f, spot::relabeling_map& fro, + const char* filename, int linenum); diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 2fd069dc2..8509b4c9f 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -31,6 +31,7 @@ #include "common_output.hh" #include "common_cout.hh" #include "common_conv.hh" +#include "common_ioap.hh" #include "common_r.hh" #include "common_range.hh" @@ -86,6 +87,7 @@ enum { OPT_IGNORE_ERRORS, OPT_IMPLIED_BY, OPT_IMPLY, + OPT_INS, OPT_LIVENESS, OPT_LTL, OPT_NEGATE, @@ -117,6 +119,7 @@ enum { OPT_SYNTACTIC_SAFETY, OPT_SYNTACTIC_SI, OPT_TO_DELTA2, + OPT_OUTS, OPT_UNABBREVIATE, OPT_UNIVERSAL, }; @@ -141,7 +144,7 @@ static const argp_option options[] = { "sonf-aps", OPT_SONF_APS, "FILENAME", OPTION_ARG_OPTIONAL, "when used with --sonf, output the newly introduced atomic " "propositions", 0 }, - { "relabel", OPT_RELABEL, "abc|pnn", OPTION_ARG_OPTIONAL, + { "relabel", OPT_RELABEL, "abc|pnn|io", OPTION_ARG_OPTIONAL, "relabel all atomic propositions, alphabetically unless " \ "specified otherwise", 0 }, { "relabel-bool", OPT_RELABEL_BOOL, "abc|pnn", OPTION_ARG_OPTIONAL, @@ -178,6 +181,12 @@ static const argp_option options[] = { "from-ltlf", OPT_FROM_LTLF, "alive", OPTION_ARG_OPTIONAL, "transform LTLf (finite LTL) to LTL by introducing some 'alive'" " proposition", 0 }, + { "ins", OPT_INS, "PROPS", 0, + "comma-separated list of input atomic propositions to use with " + "--relabel=io, interpreted as a regex if enclosed in slashes", 0 }, + { "outs", OPT_OUTS, "PROPS", 0, + "comma-separated list of output atomic propositions to use with " + "--relabel=io, interpreted as a regex if enclosed in slashes", 0 }, DECLARE_OPT_R, LEVEL_DOC(4), /**************************************************/ @@ -341,6 +350,7 @@ static range size = { -1, -1 }; static range bsize = { -1, -1 }; enum relabeling_mode { NoRelabeling = 0, ApRelabeling, + IOApRelabeling, BseRelabeling, OverlappingRelabeling }; static relabeling_mode relabeling = NoRelabeling; @@ -391,9 +401,12 @@ parse_relabeling_style(const char* arg, const char* optname) style = spot::Abc; else if (!strncasecmp(arg, "pnn", 4)) style = spot::Pnn; + else if (!*optname && !strncasecmp(arg, "io", 2)) + relabeling = IOApRelabeling; // style is actually not supported else error(2, 0, "invalid argument for --relabel%s: '%s'\n" - "expecting 'abc' or 'pnn'", optname, arg); + "expecting %s", optname, arg, + *optname ? "'abc' or 'pnn'" : "'abc', 'pnn', or 'io'"); } @@ -502,6 +515,12 @@ parse_opt(int key, char* arg, struct argp_state*) opt->imply = spot::formula::And({opt->imply, i}); break; } + case OPT_INS: + { + all_input_aps.emplace(std::vector{}); + split_aps(arg, *all_input_aps); + break; + } case OPT_LIVENESS: liveness = true; break; @@ -517,6 +536,12 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_NNF: nnf = true; break; + case OPT_OUTS: + { + all_output_aps.emplace(std::vector{}); + split_aps(arg, *all_output_aps); + break; + } case OPT_SONF: sonf = arg ? arg : "sonf_"; break; @@ -752,6 +777,12 @@ namespace f = spot::relabel(f, style, &relmap); break; } + case IOApRelabeling: + { + relmap.clear(); + f = relabel_io(f, relmap, filename, linenum); + break; + } case BseRelabeling: { relmap.clear(); @@ -948,6 +979,9 @@ main(int argc, char** argv) if (jobs.empty()) jobs.emplace_back("-", job_type::LTL_FILENAME); + if (relabeling == IOApRelabeling) + process_io_options(); + if (boolean_to_isop && simplification_level == 0) simplification_level = 1; spot::tl_simplifier_options tlopt(simplification_level); diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 6609afb4e..a5ae9f3f0 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -75,9 +75,15 @@ ltlfilt --help | sed -n '/Transformation options.*:/,/^$/p' | sed '1d;$d' propositions. --from-ltlf[=alive] transform LTLf (finite LTL) to LTL by introducing some 'alive' proposition + --ins=PROPS comma-separated list of input atomic propositions + to use with --relabel=io, interpreted as a regex + if enclosed in slashes --negate negate each formula --nnf rewrite formulas in negative normal form - --relabel[=abc|pnn] relabel all atomic propositions, alphabetically + --outs=PROPS comma-separated list of output atomic propositions + to use with --relabel=io, interpreted as a regex + if enclosed in slashes + --relabel[=abc|pnn|io] relabel all atomic propositions, alphabetically unless specified otherwise --relabel-bool[=abc|pnn] relabel Boolean subexpressions that do not share atomic propositions, relabel alphabetically @@ -95,6 +101,7 @@ ltlfilt --help | sed -n '/Transformation options.*:/,/^$/p' | sed '1d;$d' --sonf[=PREFIX] rewrite formulas in suffix operator normal form --sonf-aps[=FILENAME] when used with --sonf, output the newly introduced atomic propositions + --to-delta2 rewrite LTL formula in Δ₂-form --unabbreviate[=STR] remove all occurrences of the operators specified by STR, which must be a substring of "eFGiMRW^", where 'e', 'i', and '^' stand respectively for @@ -294,6 +301,38 @@ ltldo ltl3ba -f '"proc@loc1" U "proc@loc2"' --spin This case also relabels the formula before calling =ltl3ba=, and it then renames all the atomic propositions in the output. + +A special relabeling mode related to LTL synthesis is =--relabel=io=. +In LTL synthesis (see [[file:ltlsynt.org][=ltlsynt=]]), atomic propositions are partitioned +in two sets: the /input/ propositions represent choices from the +environment, while /output/ proposition represent choices by the +controller to be synthesized. For instance +=G(req -> Fack) & G(go -> Fgrant)= +represents could be a specification where =req= and =go= are inputs, +while =ack= and =grant= are outputs. Tool such as =ltlsynt= need +to be told using options such as =--ins= or =--outs= which atomic +propositions are input or output. Often these atomic propositions +can have very long names, so it is useful to be able to rename +them without fogeting about their nature. Option =--relabel=io= +combined with one if =--ins= or =--outs= will do exactly that: + +#+BEGIN_SRC sh +ltlfilt -f 'G(req -> Fack) & G(go -> Fgrant)' --relabel=io --ins=req,go +#+END_SRC +#+RESULTS: +: G(i1 -> Fo1) & G(i0 -> Fo0) + +Like in [[file:ltlsynt.org][=ltlsynt=]], options =--ins= and =--outs= take a comma-separated +list of atomic propositions as argument. Additionally, if an atomic +proposition in this list is enclosed in slashes (as in +=--out=req,/^go/=), it is used as a regular expression for matching +atomic propositions. + +By the way, such an IO-renamed formula can be given to [[file:ltlsynt.org][=ltlsynt=]] without +having to specify =--ins= or =--outs=, because when these two options +are missing the convention is that anything starting with =i= is an +input, and anything starting with =o= is an output. + An example showing how to use the =--from-ltlf= option is on [[file:tut12.org][a separate page]]. diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 426734851..2352c4707 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -531,6 +531,102 @@ EOF run 0 ltlfilt -s -u --relabel=pnn --define in >out diff exp out +cat >exp <(i0 || o0) && <>[](i0 || o0) +#define i0 (a) +#define i1 (b) +#define o0 (c) +i1 && []<>(i0 || o0) && <>[](i0 || o0) +#define o0 (c) +#define o1 (d) +#define o2 (e) +#define o3 (f) +#define o4 (h) +#define o5 (i) +o4 || o5 || [](o1 && o2) || <>[](!o0 || Xo3) +#define i0 (b) +#define o0 (c) +#define o1 (e) +#define o2 (f) +#define o3 (g) +i0 && o1 && (o2 || o3) && !Xo0 +#define i0 (a) +#define i1 (b) +#define o0 (c) +i1 && []<>(i0 || o0) && ![]<>!(i0 || o0) +#define i0 (a) +#define i1 (b) +#define o0 (c) +#define o1 (d) +<>(i0 <-> i1) -> !(o0 <-> o1) +#define i0 (a) +#define i1 (b) +#define o0 (c) +#define o1 (d) +#define o2 (e) +(i0 && i1 && o0) U (o0 && o1 && o2) +#define i0 (a) +#define i1 (b) +#define o0 (c) +(i0 && i1 && o0) U !(i0 && i1 && o0) +#define i0 (a) +#define i1 (b) +#define o0 (c) +#define o1 (d) +#define o2 (e) +(i0 && i1 && o0) U (!o0 && o1 && o2) +#define i0 (a) +#define i1 (b) +#define o0 (c) +#define o1 (d) +#define o2 (e) +#define o3 (f) +(o0 && o1 && (i0 || i1)) U (!o1 && o2 && o3) +#define i0 (a) +#define i1 (b) +#define o0 (d) +#define o1 (e) +#define o2 (f) +(o0 && (i0 || i1)) U (!o0 && o1 && o2) +#define i0 (a) +#define i1 (b) +#define o0 (c) +(i0 && !i0) || (i1 && !i1) || (o0 && !o0) +#define i0 (a) +#define i1 (b) +#define o0 (c) +#define o1 (d) +((i0 && !i0) || (i1 && !i1) || (o0 && !o0)) U o1 +#define i0 (a) +#define i1 (b) +#define o0 (c) +#define o1 (d) +#define o2 (e) +((i0 && !i0) || (i1 && !i1) || (o0 && o2)) U o1 +#define i0 (a) +#define i1 (b) +#define o0 (c) +((i0 && !i1) || (!i0 && i1)) U o0 +#define i0 (a) +#define i1 (b) +#define o0 (c) +((i0 && !i1) || (i0 -> i1)) U o0 +EOF + +run 0 ltlfilt -s -u --relabel=io --ins=a,b --define in >out +diff exp out +run 0 ltlfilt -s -u --relabel=io --ins='/[ab]/' --define in >out +diff exp out +run 0 ltlfilt -s -u --relabel=io --outs='/[^ab]/' --define in >out +diff exp out + cat >exp <