From e6ebbdf65fae199692ba6c9ab90dfab4da7b1ec3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 3 Sep 2024 14:20:17 +0200 Subject: [PATCH] ltlfilt, ltlsynt, ltlmix: add a --part-file option * bin/common_ioap.cc, bin/common_ioap.hh (read_part_file): New function. * bin/ltlfilt.cc, bin/ltlmix.cc, bin/ltlsynt.cc: Use it. * doc/org/ltlfilt.org, doc/org/ltlmix.org, doc/org/ltlsynt.org: Mention that new option, and improve the links to its description in ltlsynt.org. * NEWS: Mention the new option. * tests/core/ltlfilt.test, tests/core/ltlmix.test, tests/core/ltlsynt.test: Adjust test cases. --- NEWS | 9 +- bin/common_ioap.cc | 70 ++++++++++++++- bin/common_ioap.hh | 3 + bin/ltlfilt.cc | 23 ++--- bin/ltlmix.cc | 31 ++++--- bin/ltlsynt.cc | 22 ++--- doc/org/ltlfilt.org | 18 ++-- doc/org/ltlmix.org | 6 +- doc/org/ltlsynt.org | 193 ++++++++++++++++++++++------------------ tests/core/ltlfilt.test | 12 +++ tests/core/ltlmix.test | 16 ++++ tests/core/ltlsynt.test | 6 +- 12 files changed, 271 insertions(+), 138 deletions(-) diff --git a/NEWS b/NEWS index f53ef6ece..b255d1319 100644 --- a/NEWS +++ b/NEWS @@ -2,9 +2,13 @@ New in spot 2.12.0.dev (not yet released) Command-line tools: - - ltlmix is a new tool that generate formulas by combining existing + - ltlmix is a new tool that generates formulas by combining existing ones. See https://spot.lre.epita.fr/ltlmix.html for examples. + - ltlsynt learned a --part-file option, to specify the partition of + input/output proposition from a *.part file, as used in several + other tools. + - ltlfilt learned a --relabel=io mode, that is useful to shorten atomic propositions in the context of LTL synthesis. For instance @@ -13,7 +17,8 @@ New in spot 2.12.0.dev (not yet released) 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. + be inferred from their name. (This suspports a --part-file option + as well.) - genltl learned --lily-patterns to generate the example LTL synthesis specifications from Lily 1.0.2. Those come with input diff --git a/bin/common_ioap.cc b/bin/common_ioap.cc index 65e05c7ca..6bb246a63 100644 --- a/bin/common_ioap.cc +++ b/bin/common_ioap.cc @@ -18,6 +18,7 @@ #include "common_ioap.hh" #include "error.h" +#include #include // --ins and --outs, as supplied on the command-line @@ -31,6 +32,8 @@ std::vector regex_out; // map identifier to input/output (false=input, true=output) std::unordered_map identifier_map; +static bool a_part_file_was_read = false; + static std::string str_tolower(std::string s) { @@ -71,7 +74,10 @@ void process_io_options() regex_out.push_back(std::regex(f.substr(1, sz - 2))); else if (auto [it, is_new] = identifier_map.try_emplace(f, true); !is_new && !it->second) - error(2, 0, "'%s' appears in both --ins and --outs", + error(2, 0, + a_part_file_was_read ? + "'%s' appears in both inputs and outputs" : + "'%s' appears in both --ins and --outs", f.c_str()); } } @@ -125,19 +131,23 @@ is_output(const std::string& a, const char* filename, int linenum) } if (found_in && found_out) error_at_line(2, 0, filename, linenum, + a_part_file_was_read ? + "'%s' matches both inputs and outputs" : "'%s' matches both --ins and --outs", a.c_str()); if (!found_in && !found_out) { if (all_input_aps.has_value() || all_output_aps.has_value()) error_at_line(2, 0, filename, linenum, + a_part_file_was_read ? + "'%s' does not match any input or output" : "one of --ins or --outs should match '%s'", a.c_str()); else error_at_line(2, 0, filename, linenum, "since '%s' does not start with 'i' or 'o', " "it is unclear if it is an input or " - "an output;\n use --ins or --outs", + "an output;\n use --ins, --outs, or --part-file", a.c_str()); } } @@ -200,3 +210,59 @@ spot::formula relabel_io(spot::formula f, spot::relabeling_map& fro, } return spot::relabel_apply(f, &to); } + +// Read FILENAME as a ".part" file. It should +// contains lines of text of the following form: +// +// .inputs IN1 IN2 IN3... +// .outputs OUT1 OUT2 OUT3... +void read_part_file(const char* filename) +{ + std::ifstream in(filename); + if (!in) + error(2, errno, "cannot open '%s'", filename); + + // This parsing is inspired from Lily's parser for .part files. We + // read words one by one, and change the "mode" if we the word is + // ".inputs" or ".outputs". A '#' introduce a comment until the end + // of the line. + std::string word; + enum { Unknown, Input, Output } mode = Unknown; + while (in >> word) + { + // The benchmarks for Syft use ".inputs:" instead of ".inputs". + if (word == ".inputs" || word == ".inputs:") + { + mode = Input; + if (!all_input_aps.has_value()) + all_input_aps.emplace(); + } + // The benchmarks for Syft use ".outputs:" instead of ".outputs". + else if (word == ".outputs" || word == ".outputs:") + { + mode = Output; + if (!all_output_aps.has_value()) + all_output_aps.emplace(); + } + else if (word[0] == '#') + { + // Skip the rest of the line. + in.ignore(std::numeric_limits::max(), '\n'); + } + else if (mode == Unknown) + { + error_at_line(2, 0, filename, 0, + "expected '.inputs' or '.outputs' instead of '%s'", + word.c_str()); + } + else if (mode == Input) + { + all_input_aps->push_back(str_tolower(word)); + } + else /* mode == Output */ + { + all_output_aps->push_back(str_tolower(word)); + } + } + a_part_file_was_read = true; +} diff --git a/bin/common_ioap.hh b/bin/common_ioap.hh index 575e749bf..f5ff41f01 100644 --- a/bin/common_ioap.hh +++ b/bin/common_ioap.hh @@ -64,3 +64,6 @@ 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); + +// Read a .part file. +void read_part_file(const char* filename); diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 8509b4c9f..4c17f2214 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -120,6 +120,7 @@ enum { OPT_SYNTACTIC_SI, OPT_TO_DELTA2, OPT_OUTS, + OPT_PART_FILE, OPT_UNABBREVIATE, OPT_UNIVERSAL, }; @@ -187,6 +188,9 @@ static const argp_option options[] = { "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 }, + { "part-file", OPT_PART_FILE, "FILENAME", 0, + "file containing the partition of atomic propositions to use with " + "--relabel=io", 0 }, DECLARE_OPT_R, LEVEL_DOC(4), /**************************************************/ @@ -516,11 +520,9 @@ parse_opt(int key, char* arg, struct argp_state*) break; } case OPT_INS: - { - all_input_aps.emplace(std::vector{}); - split_aps(arg, *all_input_aps); - break; - } + all_input_aps.emplace(); + split_aps(arg, *all_input_aps); + break; case OPT_LIVENESS: liveness = true; break; @@ -537,11 +539,12 @@ parse_opt(int key, char* arg, struct argp_state*) nnf = true; break; case OPT_OUTS: - { - all_output_aps.emplace(std::vector{}); - split_aps(arg, *all_output_aps); - break; - } + all_output_aps.emplace(); + split_aps(arg, *all_output_aps); + break; + case OPT_PART_FILE: + read_part_file(arg); + break; case OPT_SONF: sonf = arg ? arg : "sonf_"; break; diff --git a/bin/ltlmix.cc b/bin/ltlmix.cc index a97c807d0..0cbc4ac48 100644 --- a/bin/ltlmix.cc +++ b/bin/ltlmix.cc @@ -40,6 +40,7 @@ enum { OPT_INS, OPT_LTL_PRIORITIES, OPT_OUTS, + OPT_PART_FILE, OPT_SEED, OPT_TREE_SIZE, }; @@ -102,8 +103,10 @@ static const argp_option options[] = { "comma-separated list of atomic propositions to consider as input, " "interpreted as a regex if enclosed in slashes", 0 }, { "outs", OPT_OUTS, "PROPS", 0, - "comma-separated list of atomic propositions to consider as putput, " + "comma-separated list of atomic propositions to consider as output, " "interpreted as a regex if enclosed in slashes", 0 }, + { "part-file", OPT_PART_FILE, "FILENAME", 0, + "read the I/O partition of atomic propositions from FILENAME", 0 }, RANGE_DOC, /**************************************************/ { nullptr, 0, nullptr, 0, "Adjusting probabilities:", 4 }, @@ -253,19 +256,19 @@ parse_opt(int key, char* arg, struct argp_state*) opt_unique = false; break; case OPT_INS: - { - all_input_aps.emplace(std::vector{}); - split_aps(arg, *all_input_aps); - opt_io = true; - break; - } + all_input_aps.emplace(); + split_aps(arg, *all_input_aps); + opt_io = true; + break; case OPT_OUTS: - { - all_output_aps.emplace(std::vector{}); - split_aps(arg, *all_output_aps); - opt_io = true; - break; - } + all_output_aps.emplace(); + split_aps(arg, *all_output_aps); + opt_io = true; + break; + case OPT_PART_FILE: + read_part_file(arg); + opt_io = true; + break; case OPT_SEED: opt_seed = to_int(arg, "--seed"); break; @@ -303,7 +306,7 @@ main(int argc, char* argv[]) if (opt_io && !opt_out_ap_count) error(2, 0, - "options --ins and --outs only make sense when the " + "options --ins, --outs, --part-file only make sense when the " "two-argument version of '-A N,M' or '-P N,M' is used."); if (opt_out_ap_count > 0) // Do not require --ins/--outs to be used, as the input diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index bc4bd1561..f465e2bf7 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -57,6 +57,7 @@ enum OPT_HIDE, OPT_INPUT, OPT_OUTPUT, + OPT_PART_FILE, OPT_POLARITY, OPT_PRINT, OPT_PRINT_AIGER, @@ -79,6 +80,8 @@ static const argp_option options[] = { "ins", OPT_INPUT, "PROPS", 0, "comma-separated list of uncontrollable (a.k.a. input) atomic" " propositions, interpreted as a regex if enclosed in slashes", 0 }, + { "part-file", OPT_PART_FILE, "FILENAME", 0, + "read the I/O partition of atomic propositions from FILENAME", 0 }, { "tlsf", OPT_TLSF, "FILENAME", 0, "Read a TLSF specification from FILENAME, and call syfco to " "convert it into LTL", 0 }, @@ -993,17 +996,16 @@ parse_opt(int key, char *arg, struct argp_state *) show_status = false; break; case OPT_INPUT: - { - all_input_aps.emplace(std::vector{}); - split_aps(arg, *all_input_aps); - break; - } + all_input_aps.emplace(); + split_aps(arg, *all_input_aps); + break; case OPT_OUTPUT: - { - all_output_aps.emplace(std::vector{}); - split_aps(arg, *all_output_aps); - break; - } + all_output_aps.emplace(); + split_aps(arg, *all_output_aps); + break; + case OPT_PART_FILE: + read_part_file(arg); + break; case OPT_POLARITY: opt_polarity = XARGMATCH("--polarity", arg, polarity_args, polarity_values); diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index a5ae9f3f0..d28d265eb 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -314,7 +314,7 @@ 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: +combined with one if =--ins=, =--outs=, or =--part-file= will do exactly that: #+BEGIN_SRC sh ltlfilt -f 'G(req -> Fack) & G(go -> Fgrant)' --relabel=io --ins=req,go @@ -322,16 +322,14 @@ ltlfilt -f 'G(req -> Fack) & G(go -> Fgrant)' --relabel=io --ins=req,go #+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. +The syntax for options =--ins=, =--outs= and =--part-file= is the +same as for [[file:ltlsynt.org::#input-options][=ltlsynt=]]. -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. +By the way, such an IO-renamed formula can be given to [[file:ltlsynt.org][=ltlsynt=]] +without having to specify =--ins=, =--outs=, or =--part-file=, 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/doc/org/ltlmix.org b/doc/org/ltlmix.org index b8555592e..c62a649e5 100644 --- a/doc/org/ltlmix.org +++ b/doc/org/ltlmix.org @@ -489,6 +489,6 @@ chose from may help to get more realizable formulas. When the original LTL synthesis specification formulas have atomic -proposition that do not start with =i= or =o=, options =--ins= and -=--outs= can be used to specify the nature of the atomic propositions. -These options work as with [[file:ltlsynt.org][=ltlsynt=]]. +proposition that do not start with =i= or =o=, options =--ins=, +=--outs=, or =--part-file= can be used to specify the nature of the +atomic propositions. These options work as [[file:ltlsynt.org::#input-options][=ltlsynt='s input options]]. diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index be1c8d085..93c92e29b 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -9,7 +9,7 @@ This tool synthesizes reactive controllers from LTL/PSL formulas. -Consider a set $I$ of /input/ atomic propositions, a set $O$ of output atomic +Consider a set $I$ of /input/ atomic propositions, a set $O$ of /output/ atomic propositions, and a PSL formula \phi over the propositions in $I \cup O$. A *reactive controller* realizing \phi is a function $c: (2^{I})^\star \times 2^I \mapsto 2^O$ such that, for every \omega-word $(u_i)_{i \in N} \in (2^I)^\omega$ over @@ -21,46 +21,34 @@ exists. Such controllers are easily represented as automata (or more specifically as Mealy machines). In the automaton representing the controller, the acceptance condition is irrelevant and trivially true. -=ltlsynt= has three mandatory options: -- =--ins=: a comma-separated list of input atomic propositions, or input regexes enclosed in slashes; -- =--outs=: a comma-separated list of output atomic propositions, or output regexes enclosed in slashes; -- =--formula= or =--file=: a specification in LTL or PSL. - -One of =--ins= or =--outs= may be omitted, as any atomic proposition -not listed as input can be assumed to be output and vice versa. If -both are omitted, =ltlsynts= will assume ~--ins=/^[iI]/~ and -~--outs=/^[oO]/~, i.e., atomic propositions will be classified as -input or output based on their first letter. - -The following example illustrates the synthesis of a controller -ensuring that input =i1= and =i2= are both true initially if and only -if eventually output =o1= will go from true to false at some point. -Note that this is an equivalence, not an implication. +Here is a small example where $I=\{i_1,i_2\}$ and $O=\{o_1\}$. The +specification asks that $o_1$ hold at some point if and only if $i_1$ +and $i_2$ hold one after the other at some point. #+NAME: example #+BEGIN_SRC sh :exports both -ltlsynt -f '(i1 & i2) <-> F(o1 & X(!o1))' +ltlsynt -f 'F(i1 & Xi2) <-> F(o1)' #+END_SRC #+RESULTS: example #+begin_example REALIZABLE HOA: v1 -States: 3 +States: 2 Start: 0 -AP: 3 "i1" "i2" "o1" +AP: 3 "i1" "o1" "i2" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic -controllable-AP: 2 +controllable-AP: 1 --BODY-- State: 0 -[0&1&2] 1 -[!0&2 | !1&2] 2 +[!0&!1] 0 +[0&!1] 1 State: 1 -[!2] 1 -State: 2 -[2] 2 +[!0&!1&!2] 0 +[0&!1&!2] 1 +[1&2] 1 --END-- #+end_example @@ -78,7 +66,7 @@ to visualize this machine. #+NAME: exampledot #+BEGIN_SRC sh :exports code -ltlsynt -f '(i1 & i2) <-> F(o1 & X(!o1))' --hide-status --dot +ltlsynt -f 'F(i1 & Xi2) <-> F(o1)' --hide-status --dot #+END_SRC #+BEGIN_SRC dot :file ltlsyntex.svg :var txt=exampledot :exports results @@ -99,75 +87,49 @@ ltlsynt --ins=a -f 'F a' #+RESULTS: : UNREALIZABLE -By default, the controller is output in HOA format, but it can be -output as an And-Inverter-Graph in [[http://fmv.jku.at/aiger/][AIGER format]] using the =--aiger= -flag. This is the output format required for the [[http://syntcomp.org/][SYNTCOMP]] competition. +* Input options + :PROPERTIES: + :CUSTOM_ID: input-options + :END: -#+NAME: exampleaig -#+BEGIN_SRC sh :exports both -ltlsynt -f '(i1 & i2) <-> F(o1 & X(!o1))' --aiger -#+END_SRC +=ltlsynt= require two pieces of information two solve a reactive +LTL/PSL synthesis problem: an LTL (or PSL) formula, and a partition of +its atomic propositions as input and output. -#+RESULTS: exampleaig -#+begin_example -REALIZABLE -aag 18 2 2 1 14 -2 -4 -6 23 -8 37 -7 -10 6 9 -12 4 9 -14 5 10 -16 13 15 -18 2 17 -20 3 10 -22 19 21 -24 7 8 -26 4 24 -28 5 7 -30 27 29 -32 2 31 -34 3 7 -36 33 35 -i0 i1 -i1 i2 -o0 o1 -#+end_example +The specification formula can be passed with =-f/--formula= or +=-F/--file=. If multiple specifications formulas are passed, they +will all be solved individually. -The above format is not very human friendly. Again, by passing both -=--aiger= and =--dot=, one can display the And-Inverter-Graph representing -the controller: +The input/output partition can be given in several ways. If it is +not specified, =ltlsynt= assumes that input variables should start +with =i=, and output variables should start with =o=. -#+NAME: exampleaigdot -#+BEGIN_SRC sh :exports code -ltlsynt -f '(i1 & i2) <-> F(o1 & X(!o1))' --hide-status --aiger --dot -#+END_SRC +Options =--ins= and =--outs= should be followed by a comma-separated +list of input atomic propositions, or input regexes enclosed in +slashes. E.g., =--ins=switch,/^in/,car=. If only one of these +options is given, atomic propositions not matched by that option +are assumed to belong to the other set. -#+BEGIN_SRC dot :file ltlsyntexaig.svg :var txt=exampleaigdot :exports results - $txt -#+END_SRC +Another way to specify the input/output partition is using a =*.part= +file passed to the =--part-file= option. Such a file is used by +several other synthesis tools. The format is space-separated list of +words representing atomic-propositions. Two keywords =.inputs= and +=.outputs= indicate the set of the atomic-propositions that follow. +For instance: -#+RESULTS: -[[file:ltlsyntexaig.svg]] +#+BEGIN_EXAMPLE +.inputs request cancel +.outputs grant ack +#+END_EXAMPLE -In the above diagram, round nodes represent AND gates. Small black -circles represent inversions (or negations), colored triangles are -used to represent input signals (at the bottom) and output signals (at -the top), and finally rectangles represent latches. A latch is a one -bit register that delays the signal by one step. Initially, all -latches are assumed to contain =false=, and they emit their value from -the =L0_out= and =L1_out= rectangles at the bottom. Their input value, -to be emitted at the next step, is received via the =L0_in= and =L1_in= -boxes at the top. In =ltlsynt='s encoding, the set of latches is used -to keep track of the current state of the Mealy machine. +Using =--part-file=THEABOVEFILE= is equivalent to +=--ins=request,cancel --outs=grant,ack=. -The generation of a controller can be disabled with the flag -=--realizability=. In this case, =ltlsynt='s output is limited to -=REALIZABLE= or =UNREALIZABLE=. +As an extension to this simple =*.part= format, words enclosed in +slashes are interpreted as regexes, like for the =--ins= and =--outs= +options. -* TLSF +* TLSF input =ltlsynt= was made with the [[http://syntcomp.org/][SYNTCOMP]] competition in mind, and more specifically the TLSF track of this competition. TLSF is a high-level @@ -193,6 +155,65 @@ ltlsynt --formula="$LTL" --outs="$OUT" #+END_SRC +* Output options + +By default, the controller is output in HOA format, but it can be +output as an And-Inverter-Graph in [[http://fmv.jku.at/aiger/][AIGER format]] using the =--aiger= +flag. This is the output format required for the [[http://syntcomp.org/][SYNTCOMP]] competition. + +#+NAME: exampleaig +#+BEGIN_SRC sh :exports both +ltlsynt -f 'F(i1 & Xi2) <-> F(o1)' --aiger +#+END_SRC + +#+RESULTS: exampleaig +#+begin_example +REALIZABLE +aag 5 2 1 1 2 +2 +4 +6 11 +8 +8 4 6 +10 3 9 +i0 i1 +i1 i2 +o0 o1 +#+end_example + +The above format is not very human friendly. Again, by passing both +=--aiger= and =--dot=, one can display the And-Inverter-Graph representing +the controller: + +#+NAME: exampleaigdot +#+BEGIN_SRC sh :exports code +ltlsynt -f 'F(i1 & Xi2) <-> F(o1)' --hide-status --aiger --dot +#+END_SRC + +#+RESULTS: exampleaigdot + +#+BEGIN_SRC dot :file ltlsyntexaig.svg :var txt=exampleaigdot :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:ltlsyntexaig.svg]] + +In the above diagram, round nodes represent AND gates. Small black +circles represent inversions (or negations), colored triangles are +used to represent input signals (at the bottom) and output signals (at +the top), and finally rectangles represent latches. A latch is a one +bit register that delays the signal by one step. Initially, all +latches are assumed to contain =false=, and they emit their value from +the =*_out= rectangles at the bottom. Their input value, to be +emitted at the next step, is received via the =*_in= boxes at the top. +In =ltlsynt='s encoding, the set of latches is used to keep track of +the current state of the Mealy machine. + +The generation of a controller can be disabled with the flag +=--realizability=. In this case, =ltlsynt='s output is limited to +=REALIZABLE= or =UNREALIZABLE=. + * Internal details The tool reduces the synthesis problem to a parity game, and solves the parity diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 2352c4707..2019151ca 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -626,6 +626,18 @@ 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 +echo '.inputs a b' >rel.part +run 0 ltlfilt -s -u --relabel=io --part=rel.part --define in >out +diff exp out +echo '.inputs /[ab]/ # .output ignored' >rel.part +run 0 ltlfilt -s -u --relabel=io --part=rel.part --define in >out +diff exp out +echo '.outputs /[^ab]/ # .input ignored' >rel.part +run 0 ltlfilt -s -u --relabel=io --part=rel.part --define in >out +diff exp out +echo 'error /[^ab]/' >rel.part +run 2 ltlfilt -s -u --relabel=io --part=rel.part --define in 2>err +grep "expected '.inputs' or '.outputs'" err cat >exp < err && exit 1 cat err grep 'ins.*outs' err + +echo '.inputs a c .outputs b d ' > part.part +ltlmix -fXa -fGb -f'c U d' --part-file=part.part -C4 -A3,3 -n10 >out +cat >expected <stderr && : test $? -eq 2 -grep "[-]-ins or --outs" stderr +grep "[-]-ins.*--outs" stderr # Try to find a direct strategy for GFa <-> GFb and a direct strategy for # Gc @@ -1139,11 +1139,15 @@ ltlsynt --decomp=yes -f "$s" --realizability >out ltlsynt --decomp=no --outs='/^o[0-9]*$/' -f "$s" --realizability >>out ltlsynt --decomp=no --outs='/^o[0-9]$/' -f "$s" --realizability >>out && : ltlsynt -f "$s" --ins='/^i[0-9]*$/' --realizability >>out +echo ".inputs i1 i2 i3 i4 i5 i6 i7 i8" > part.part +echo ".outputs /^o1[0-9]*/ o01 o02 o03 o04 o05 o06 o07 o08 o09" >> part.part +ltlsynt -f "$s" --part-file=part.part --realizability >>out cat >expected <