diff --git a/NEWS b/NEWS index 2e4d094f2..d95157cdd 100644 --- a/NEWS +++ b/NEWS @@ -37,6 +37,10 @@ New in spot 2.12.2.dev (not yet released) be inferred from their name. (This suspports a --part-file option as well.) + - ltlfilt learned --save-part-file[=FILENAME] option that can be + used to create partition files suitable for many synthesis tools + (including ltlsynt). + - genltl learned --lily-patterns to generate the example LTL synthesis specifications from Lily 1.0.2. Those come with input and output atomic proposition rewriten in the form "iNN" or "oNN", diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 4c17f2214..1669a707d 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -103,6 +103,7 @@ enum { OPT_REMOVE_WM, OPT_REMOVE_X, OPT_SAFETY, + OPT_SAVE_PART_FILE, OPT_SIGMA2, OPT_SIZE, OPT_SIZE_MAX, @@ -184,13 +185,18 @@ static const argp_option options[] = " 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 }, + "--relabel=io or --save-part-file, 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 }, + "--relabel=io or --save-part-file, interpreted as a regex if " + "enclosed in slashes", 0 }, { "part-file", OPT_PART_FILE, "FILENAME", 0, "file containing the partition of atomic propositions to use with " "--relabel=io", 0 }, + { "save-part-file", OPT_SAVE_PART_FILE, "FILENAME", OPTION_ARG_OPTIONAL, + "file containing the partition of atomic propositions, " + "readable by --part-file", 0 }, DECLARE_OPT_R, LEVEL_DOC(4), /**************************************************/ @@ -377,6 +383,7 @@ static struct opt_t { spot::bdd_dict_ptr dict = spot::make_bdd_dict(); spot::exclusive_ap excl_ap; + std::unique_ptr output_part = nullptr; std::unique_ptr output_define = nullptr; std::unique_ptr output_sonf = nullptr; spot::formula implied_by = nullptr; @@ -596,6 +603,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_SAFETY: safety = obligation = true; break; + case OPT_SAVE_PART_FILE: + opt->output_part.reset(new output_file(arg ? arg : "-")); + break; case OPT_SIZE: size = parse_range(arg, 0, std::numeric_limits::max()); break; @@ -954,6 +964,40 @@ namespace oldname, filename, std::to_string(linenum).c_str()) << ")\n"; } + if (opt->output_part + && output_format != count_output + && output_format != quiet_output) + { + std::vector ins; + std::vector outs; + spot::atomic_prop_set* s = atomic_prop_collect(f); + for (spot::formula ap: *s) + { + spot::formula apo = ap; + if (auto it = relmap.find(ap); it != relmap.end()) + apo = it->second; + if (is_output(apo.ap_name(), filename, linenum)) + outs.push_back(ap); + else + ins.push_back(ap); + } + delete s; + auto& os = opt->output_part->ostream(); + if (!ins.empty()) + { + os << ".inputs"; + for (const auto& ap: ins) + os << ' ' << str_psl(ap); + os << '\n'; + } + if (!outs.empty()) + { + os << ".outputs"; + for (const auto& ap: outs) + os << ' ' << str_psl(ap); + os << '\n'; + } + } one_match = true; output_formula_checked(f, &timer, filename, linenum, match_count, prefix, suffix); @@ -982,7 +1026,7 @@ main(int argc, char** argv) if (jobs.empty()) jobs.emplace_back("-", job_type::LTL_FILENAME); - if (relabeling == IOApRelabeling) + if (relabeling == IOApRelabeling || opt->output_part) process_io_options(); if (boolean_to_isop && simplification_level == 0) diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index d28d265eb..fad49bcf5 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -301,14 +301,18 @@ 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. +An example showing how to use the =--from-ltlf= option is on [[file:tut12.org][a +separate page]]. + +* I/O-partitioned formulas 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 +environment, while /output/ propositions 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, +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 @@ -331,8 +335,24 @@ 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]]. +=ltlfilt= can also be instructed to create a partition file (usually +named =*.part=) that can be used by synthesis tools. + +#+BEGIN_SRC sh +ltlfilt -f 'G(req -> Fack) & G(go -> Fgrant)' --relabel=io \ + --ins=req,go --save-part=out.part +#+END_SRC +#+RESULTS: +: G(i1 -> Fo0) & G(i0 -> Fo1) + +In addition to the relabeling, this also created a file =out.part= +containing the following: +#+BEGIN_SRC sh :exports results +cat out.part +#+END_SRC +#+RESULTS: +: .inputs i0 i1 +: .outputs o0 o1 * Filtering diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 2019151ca..2c456878a 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -872,3 +872,19 @@ diff expected out # would stick to the rest of the file unless overridden. run 2 ltlfilt -Ffile/1 -Ffile : + + +run 0 ltlfilt -f 'i1 U o2 U i3' --save-part=p.part +cat > exp.part<out +cat > exp<