From 71979840cb36ff92e5274f9194b378b8eb0fcc82 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 25 Oct 2015 21:54:55 +0100 Subject: [PATCH] bin: factor handling of -B/-C/-D/... output options * src/bin/common_post.cc: Handle the options for BA/TGBA/Monitor as well as Complete/SBAcc here, and in the same group. Rename "Translation intent" and "Optimization level" to "Simplification goal" and "Simplification level" so that it makes sense even in autfilt. * src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc: Remove common code. * doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org: Adjust sed invocations. --- doc/org/autfilt.org | 44 ++++++++++++++++----------- doc/org/dstar2tgba.org | 20 +++++++------ doc/org/ltl2tgba.org | 12 +++----- src/bin/autfilt.cc | 30 ++----------------- src/bin/common_post.cc | 67 +++++++++++++++++++++++++++++++----------- src/bin/dstar2tgba.cc | 25 +--------------- src/bin/ltl2tgba.cc | 26 +--------------- 7 files changed, 97 insertions(+), 127 deletions(-) diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index f4c77cef4..0d599524b 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -193,44 +193,46 @@ This set of options controls the desired type of output automaton: autfilt --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: -: -B, --ba Büchi Automaton +: -B, --ba Büchi Automaton (with state-based acceptance) +: -C, --complete output a complete automaton : --generic Any acceptance is allowed (default) : -M, --monitor Monitor (accepts all finite prefixes of the given : property) -: --tgba Transition-based Generalized Büchi Automaton +: -S, --state-based-acceptance, --sbacc +: define the acceptance using states +: --tgba Transition-based Generalized Büchi Automaton -These options specifies desired properties: +These options specify any simplification goal: #+BEGIN_SRC sh :results verbatim :exports results -autfilt --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' +autfilt --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : -a, --any no preference, do not bother making it small or -: deterministic (default) -: -C, --complete output a complete automaton (combine with other -: intents) +: deterministic : -D, --deterministic prefer deterministic automata : --small prefer small automata -: -S, --state-based-acceptance, --sbacc -: define the acceptance using states Finally, the following switches control the amount of effort applied -to reach the desired properties: +toward the desired goal: #+BEGIN_SRC sh :results verbatim :exports results -autfilt --help | sed -n '/Optimization level:/,/^$/p' | sed '1d;$d' +autfilt --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : --high all available optimizations (slow) -: --low minimal optimizations (fast, default) +: --low minimal optimizations (fast) : --medium moderate optimizations By default, =--any --low= is used, which cause all simplifications to -be skipped. If you want to reduce the size of the automaton, try -=--small --high= and if you want to try to make it deterministic -(their is to guaranty of result, this is only a preference), try -=--deterministic --high=. +be skipped. However if any goal is given, than the simplification level +defaults to =--high= (unless specified otherwise). If a simplification +level is given without specifying any goal, then the goal default to =--small=. + +So if you want to reduce the size of the automaton, try =--small= and +if you want to try to make (or keep) it deterministic (there is to +guaranty of result, this is only a preference) try =--deterministic=. * Transformations @@ -245,6 +247,8 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d' --cleanup-acceptance remove unused acceptance sets from the automaton --cnf-acceptance put the acceptance condition in Conjunctive Normal Form + --complement complement each automaton (currently support only + deterministic automata) --complement-acceptance complement the acceptance condition (without touching the automaton) --destut allow less stuttering @@ -263,7 +267,11 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d' sets --merge-transitions merge transitions with same destination and acceptance - --product=FILENAME build the product with the automaton in FILENAME + --product=FILENAME, --product-and=FILENAME + build the product with the automaton in FILENAME + to intersect languages + --product-or=FILENAME build the product with the automaton in FILENAME + to sum languages --randomize[=s|t] randomize states and transitions (specify 's' or 't' to randomize only states or transitions) --remove-ap=AP[=0|=1][,AP...] @@ -276,6 +284,8 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d' --remove-unreachable-states remove states that are unreachable from the initial state + --sat-minimize[=options] minimize the automaton using a SAT solver + (only work for deterministic automata) --separate-sets if both Inf(x) and Fin(x) appear in the acceptance condition, replace Fin(x) by a new Fin(y) and adjust the automaton diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index e4a0f5cfb..e69ac7438 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -324,21 +324,23 @@ dstar2tgba --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: -: -B, --ba Büchi Automaton +: -B, --ba Büchi Automaton (implies -S) +: -C, --complete output a complete automaton : -M, --monitor Monitor (accepts all finite prefixes of the given -: formula) -: --tgba Transition-based Generalized Büchi Automaton +: property) +: -S, --state-based-acceptance, --sbacc +: define the acceptance using states +: --tgba Transition-based Generalized Büchi Automaton : (default) -And these may be refined by a translation intent, should the +And these may be refined by a simplification goal, should the post-processor routine had a choice to make: #+BEGIN_SRC sh :results verbatim :exports results -dstar2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' +dstar2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: -: -a, --any no preference -: -C, --complete output a complete automaton (combine with other -: intents) +: -a, --any no preference, do not bother making it small or +: deterministic : -D, --deterministic prefer deterministic automata : --small prefer small automata (default) @@ -346,7 +348,7 @@ The effort put into post-processing can be limited with the =--low= or =--medium= options: #+BEGIN_SRC sh :results verbatim :exports results -dstar2tgba --help | sed -n '/Optimization level:/,/^$/p' | sed '1d;$d' +dstar2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : --high all available optimizations (slow, default) diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 9300cbe07..819d887a1 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -405,22 +405,18 @@ ltl2tgba -s --lenient '(a < b) U (process[2]@ok)' * Do you favor deterministic or small automata? The translation procedure can be controled by a few switches. A first -set of options specifies the intent of the translation: whenever -possible, would you prefer a small automaton (=--small=) or a +set of options specifies the goal of the simplification routines: +whenever possible, would you prefer a small automaton (=--small=) or a deterministic (=--deterministic=) automaton? #+BEGIN_SRC sh :results verbatim :exports results -ltl2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' +ltl2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : -a, --any no preference, do not bother making it small or : deterministic -: -C, --complete output a complete automaton (combine with other -: intents) : -D, --deterministic prefer deterministic automata : --small prefer small automata (default) -: -U, --unambiguous output unambiguous automata (combine with other -: intents) The =--any= option tells the translator that it should attempt to reduce or produce a deterministic result result: any automaton @@ -641,7 +637,7 @@ A last parameter that can be used to tune the translation is the amount of pre- and post-processing performed. These two steps can be adjusted via a common set of switches: #+BEGIN_SRC sh :results verbatim :exports results -ltl2tgba --help | sed -n '/Optimization level:/,/^$/p' | sed '1d;$d' +ltl2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : --high all available optimizations (slow, default) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 6ee8bbdf3..80b6cf9bb 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -101,7 +101,6 @@ enum { OPT_SIMPLIFY_EXCLUSIVE_AP, OPT_STATES, OPT_STRIPACC, - OPT_TGBA, }; static const argp_option options[] = @@ -111,16 +110,6 @@ static const argp_option options[] = { "file", 'F', "FILENAME", 0, "process the automaton in FILENAME", 0 }, /**************************************************/ - { nullptr, 0, nullptr, 0, "Output automaton type:", 2 }, - { "generic", OPT_GENERIC, nullptr, 0, - "Any acceptance is allowed (default)", 0 }, - { "tgba", OPT_TGBA, nullptr, 0, - "Transition-based Generalized Büchi Automaton", 0 }, - { "ba", 'B', nullptr, 0, - "Büchi Automaton (with state-based acceptance)", 0 }, - { "monitor", 'M', nullptr, 0, "Monitor (accepts all finite prefixes " - "of the given property)", 0 }, - /**************************************************/ { "count", 'c', nullptr, 0, "print only a count of matched automata", 3 }, { "max-count", 'n', "NUM", 0, "output at most NUM automata", 3 }, /**************************************************/ @@ -213,9 +202,9 @@ static const argp_option options[] = RANGE_DOC_FULL, { nullptr, 0, nullptr, 0, "If any option among --small, --deterministic, or --any is given, " - "then the optimization level defaults to --high unless specified " + "then the simplification level defaults to --high unless specified " "otherwise. If any option among --low, --medium, or --high is given, " - "then the translation intent defaults to --small unless specified " + "then the simplification goal defaults to --small unless specified " "otherwise. If none of those options are specified, then autfilt " "acts as is --any --low were given: these actually disable the " "simplification routines.", 22 }, @@ -233,7 +222,7 @@ static const struct argp_child children[] = { &hoaread_argp, 0, nullptr, 0 }, { &aoutput_argp, 0, nullptr, 0 }, { &aoutput_io_format_argp, 0, nullptr, 4 }, - { &post_argp_disabled, 0, nullptr, 20 }, + { &post_argp_disabled, 0, nullptr, 0 }, { &misc_argp, 0, nullptr, -1 }, { nullptr, 0, nullptr, 0 } }; @@ -298,18 +287,12 @@ parse_opt(int key, char* arg, struct argp_state*) // This switch is alphabetically-ordered. switch (key) { - case 'B': - type = spot::postprocessor::BA; - break; case 'c': automaton_format = Count; break; case 'F': jobs.emplace_back(arg, true); break; - case 'M': - type = spot::postprocessor::Monitor; - break; case 'n': opt_max_count = to_pos_int(arg); break; @@ -359,8 +342,6 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_EXCLUSIVE_AP: excl_ap.add_group(arg); break; - case OPT_GENERIC: - type = spot::postprocessor::Generic; case OPT_INSTUT: if (!arg || (arg[0] == '1' && arg[1] == 0)) opt_instut = 1; @@ -493,11 +474,6 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_STRIPACC: opt_stripacc = true; break; - case OPT_TGBA: - if (automaton_format == Spin) - error(2, 0, "--spin and --tgba are incompatible"); - type = spot::postprocessor::TGBA; - break; case ARGP_KEY_ARG: jobs.emplace_back(arg, true); break; diff --git a/src/bin/common_post.cc b/src/bin/common_post.cc index 89568f8ff..0df6b0108 100644 --- a/src/bin/common_post.cc +++ b/src/bin/common_post.cc @@ -19,6 +19,7 @@ #include "common_post.hh" #include "common_r.hh" +#include "common_aoutput.hh" #include "error.h" spot::postprocessor::output_type type = spot::postprocessor::TGBA; @@ -31,27 +32,36 @@ bool level_set = false; bool pref_set = false; enum { - OPT_HIGH = 1, + OPT_GENERIC = 1, + OPT_HIGH, OPT_LOW, OPT_MEDIUM, OPT_SMALL, + OPT_TGBA, }; static const argp_option options[] = { /**************************************************/ - { nullptr, 0, nullptr, 0, "Translation intent:", 20 }, - { "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 }, - { "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 }, - { "any", 'a', nullptr, 0, "no preference, do not bother making it small " - "or deterministic", 0 }, - { "complete", 'C', nullptr, 0, "output a complete automaton (combine " - "with other intents)", 0 }, + { nullptr, 0, nullptr, 0, "Output automaton type:", 2 }, + { "tgba", OPT_TGBA, nullptr, 0, + "Transition-based Generalized Büchi Automaton (default)", 0 }, + { "ba", 'B', nullptr, 0, + "Büchi Automaton (implies -S)", 0 }, + { "monitor", 'M', nullptr, 0, "Monitor (accepts all finite prefixes " + "of the given property)", 0 }, + { "complete", 'C', nullptr, 0, "output a complete automaton", 0 }, { "state-based-acceptance", 'S', nullptr, 0, "define the acceptance using states", 0 }, { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, /**************************************************/ - { nullptr, 0, nullptr, 0, "Optimization level:", 21 }, + { nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, + { "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 }, + { "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 }, + { "any", 'a', nullptr, 0, "no preference, do not bother making it small " + "or deterministic", 0 }, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Simplification level:", 21 }, { "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 }, { "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 }, { "high", OPT_HIGH, nullptr, 0, @@ -62,18 +72,27 @@ static const argp_option options[] = static const argp_option options_disabled[] = { /**************************************************/ - { nullptr, 0, nullptr, 0, "Translation intent:", 20 }, - { "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 }, - { "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 }, - { "any", 'a', nullptr, 0, "no preference, do not bother making it small " - "or deterministic", 0 }, - { "complete", 'C', nullptr, 0, "output a complete automaton (combine " - "with other intents)", 0 }, + { nullptr, 0, nullptr, 0, "Output automaton type:", 2 }, + { "generic", OPT_GENERIC, nullptr, 0, + "Any acceptance is allowed (default)", 0 }, + { "tgba", OPT_TGBA, nullptr, 0, + "Transition-based Generalized Büchi Automaton", 0 }, + { "ba", 'B', nullptr, 0, + "Büchi Automaton (with state-based acceptance)", 0 }, + { "monitor", 'M', nullptr, 0, "Monitor (accepts all finite prefixes " + "of the given property)", 0 }, + { "complete", 'C', nullptr, 0, "output a complete automaton", 0 }, { "state-based-acceptance", 'S', nullptr, 0, "define the acceptance using states", 0 }, { "sbacc", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, /**************************************************/ - { nullptr, 0, nullptr, 0, "Optimization level:", 21 }, + { nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, + { "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 }, + { "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 }, + { "any", 'a', nullptr, 0, "no preference, do not bother making it small " + "or deterministic", 0 }, + /**************************************************/ + { nullptr, 0, nullptr, 0, "Simplification level:", 21 }, { "low", OPT_LOW, nullptr, 0, "minimal optimizations (fast)", 0 }, { "medium", OPT_MEDIUM, nullptr, 0, "moderate optimizations", 0 }, { "high", OPT_HIGH, nullptr, 0, @@ -91,6 +110,9 @@ parse_opt_post(int key, char*, struct argp_state*) pref = spot::postprocessor::Any; pref_set = true; break; + case 'B': + type = spot::postprocessor::BA; + break; case 'C': comp = spot::postprocessor::Complete; break; @@ -98,9 +120,15 @@ parse_opt_post(int key, char*, struct argp_state*) pref = spot::postprocessor::Deterministic; pref_set = true; break; + case 'M': + type = spot::postprocessor::Monitor; + break; case 'S': sbacc = spot::postprocessor::SBAcc; break; + case OPT_GENERIC: + type = spot::postprocessor::Generic; + break; case OPT_HIGH: level = spot::postprocessor::High; simplification_level = 3; @@ -120,6 +148,11 @@ parse_opt_post(int key, char*, struct argp_state*) pref = spot::postprocessor::Small; pref_set = true; break; + case OPT_TGBA: + if (automaton_format == Spin) + error(2, 0, "--spin and --tgba are incompatible"); + type = spot::postprocessor::TGBA; + break; default: return ARGP_ERR_UNKNOWN; } diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index cf4e2fb9e..80ea7d739 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -53,10 +53,6 @@ Büchi automata.\n\nThis reads automata into any supported format \ Transition-based Generalized Büchi Automata in GraphViz's format by default. \ Each supplied file may contain multiple automata."; -enum { - OPT_TGBA = 1, -}; - static const argp_option options[] = { /**************************************************/ @@ -64,14 +60,6 @@ static const argp_option options[] = { "file", 'F', "FILENAME", 0, "process the automaton in FILENAME", 0 }, /**************************************************/ - { nullptr, 0, nullptr, 0, "Output automaton type:", 2 }, - { "tgba", OPT_TGBA, nullptr, 0, - "Transition-based Generalized Büchi Automaton (default)", 0 }, - { "ba", 'B', nullptr, 0, - "Büchi Automaton (with state-based acceptance)", 0 }, - { "monitor", 'M', nullptr, 0, "Monitor (accepts all finite prefixes " - "of the given property)", 0 }, - /**************************************************/ { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { "extra-options", 'x', "OPTS", 0, "fine-tuning options (see spot-x (7))", 0 }, @@ -83,7 +71,7 @@ static const struct argp_child children[] = { &hoaread_argp, 0, nullptr, 0 }, { &aoutput_argp, 0, nullptr, 0 }, { &aoutput_io_format_argp, 0, nullptr, 4 }, - { &post_argp, 0, nullptr, 20 }, + { &post_argp, 0, nullptr, 0 }, { &misc_argp, 0, nullptr, -1 }, { nullptr, 0, nullptr, 0 } }; @@ -96,15 +84,9 @@ parse_opt(int key, char* arg, struct argp_state*) // This switch is alphabetically-ordered. switch (key) { - case 'B': - type = spot::postprocessor::BA; - break; case 'F': jobs.emplace_back(arg, true); break; - case 'M': - type = spot::postprocessor::Monitor; - break; case 'x': { const char* opt = extra_options.parse_options(arg); @@ -112,11 +94,6 @@ parse_opt(int key, char* arg, struct argp_state*) error(2, 0, "failed to parse --options near '%s'", opt); } break; - case OPT_TGBA: - if (automaton_format == Spin) - error(2, 0, "--spin and --tgba are incompatible"); - type = spot::postprocessor::TGBA; - break; case ARGP_KEY_ARG: jobs.emplace_back(arg, true); break; diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 62e4a8b3e..25da76702 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -47,26 +47,13 @@ in GraphViz's format.\n\ If multiple formulas are supplied, several automata will be output."; -enum { - OPT_TGBA = 1, -}; - static const argp_option options[] = { /**************************************************/ - { nullptr, 0, nullptr, 0, "Output automaton type:", 2 }, - { "tgba", OPT_TGBA, nullptr, 0, - "Transition-based Generalized Büchi Automaton (default)", 0 }, - { "ba", 'B', nullptr, 0, - "Büchi Automaton (with state-based acceptance)", 0 }, - { "monitor", 'M', nullptr, 0, "Monitor (accepts all finite prefixes " - "of the given formula)", 0 }, - /**************************************************/ { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the formula, in Spot's syntax", 4 }, /**************************************************/ - { "unambiguous", 'U', nullptr, 0, "output unambiguous automata " - "(combine with other intents)", 20 }, + { "unambiguous", 'U', nullptr, 0, "output unambiguous automata", 2 }, { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, { "extra-options", 'x', "OPTS", 0, "fine-tuning options (see spot-x (7))", 0 }, @@ -92,12 +79,6 @@ parse_opt(int key, char* arg, struct argp_state*) // This switch is alphabetically-ordered. switch (key) { - case 'B': - type = spot::postprocessor::BA; - break; - case 'M': - type = spot::postprocessor::Monitor; - break; case 'U': unambig = spot::postprocessor::Unambiguous; break; @@ -108,11 +89,6 @@ parse_opt(int key, char* arg, struct argp_state*) error(2, 0, "failed to parse --options near '%s'", opt); } break; - case OPT_TGBA: - if (automaton_format == Spin) - error(2, 0, "--spin and --tgba are incompatible"); - type = spot::postprocessor::TGBA; - break; case ARGP_KEY_ARG: // FIXME: use stat() to distinguish filename from string? jobs.emplace_back(arg, false);