Commit 71979840 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent dee73ee3
......@@ -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
......
......@@ -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)
......
......@@ -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)
......
......@@ -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;
......
......@@ -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 },
{ 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, "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 },
{ "complete", 'C', nullptr, 0, "output a complete automaton (combine "
"with other intents)", 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 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 },
{ 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, "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 },
{ "complete", 'C', nullptr, 0, "output a complete automaton (combine "
"with other intents)", 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 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;
}
......
......@@ -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;
......
......@@ -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);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment