diff --git a/NEWS b/NEWS index d4bfa5b63..5d61462ee 100644 --- a/NEWS +++ b/NEWS @@ -22,6 +22,13 @@ New in spot 1.99.5a (not yet released) Boolean argument. This argument used to be optionnal (defaulting to True), but it no longer is. + * By default the HOA printer tries to not bloat the output with + properties that are probably useless. The HOA printer now has a + new option "v" (use "-Hv" from the command line) to output more + verbose "properties:". This currently includes outputing + "no-univ-branch", and outputting "unambiguous" even for automata + already tagged as "deterministic". + Python: * Add bindings for is_unambiguous(). diff --git a/doc/org/hoa.org b/doc/org/hoa.org index 0ab901d9a..a5858e751 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -553,6 +553,47 @@ property is added to the TωA class, we cannot forget to update all the calls =prop_copy()= or =prop_keep()= (because these functions will take a new argument). +The =HOA= printer also tries to not bloat the output with many +redundant and useless properties. For instance =deterministic= +automata are necessarily =unambiguous=, and people interested in +unambiguous automata know that, so Spot only output the =unambiguous= +property if an unambiguous automaton is non-deterministic. Similarly, +while Spot only outputs non-alternating automata, it does not output +the =no-univ-branch= property because we cannot think of a situation +where this would be useful. This decision can be overridden by +passing the =-Hv= (or =--hoa=v=) option to the command-line tools: +this requests "verbose" properties. + +The following table summarizes how supported properties are handled. In +particular: +- for the parser =checked= means that the property is always inferred + and checked against any declaration (if present), =trusted= means + that the property will be stored without being checked (unless + =--trust-hoa=no= is specified). +- Stored properties are those represented as bits in the automaton. +- the printer will sometime check some properties when it can do + it as part of its initial "survey scan" of the automaton; in that + case the stored property is not used. This makes it possible + to detect deterministic automata that have been output by algorithms + that do not try to output deterministic automata. + +| property | parser | stored | printer | notes | +|---------------------+---------+--------+---------------------------------------------+--------------------------------------------------------| +| =state-labels= | checked | no | never | state labels are always converted to transition labels | +| =trans-labels= | checked | no | always, unless =-Hi= | | +| =implicit-labels= | checked | no | if =-Hi= | =-Hi= only works for deterministic automata | +| =explicit-labels= | checked | no | always, unless =-Hi= | | +| =state-acc= | checked | yes | re-checked, unless =-Ht= or =-Hm= | | +| =trans-acc= | checked | no | if not =state-acc= and not =-Hm= | | +| =no-univ-branch= | ignored | no | only if =-Hv= | | +| =deterministic= | checked | yes | re-checked | | +| =complete= | checked | no | re-checked | | +| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be re-checked with =--check=unambiguous= | +| =stutter-invariant= | trusted | yes | as stored | can be re-checked with =--check=stuttering= | +| =stutter-sensitive= | trusted | yes | as stored | can be re-checked with =--check=stuttering= | +| =inherently-weak= | trusted | yes | as stored | | +| =colored= | ignored | no | checked | | + ** Named properties In addition to the bit properties discussed above, a TωA can carry diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 7273519c0..65b063039 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -93,13 +93,14 @@ static const argp_option options[] = "(r) rainbow colors for acceptance sets, " "(R) color acceptance sets by Inf/Fin, (s) with SCCs, " "(t) force transition-based acceptance.", 0 }, - { "hoaf", 'H', "i|s|t|m|l", OPTION_ARG_OPTIONAL, + { "hoaf", 'H', "i|l|m|s|t|v", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " "(i) use implicit labels for complete deterministic automata, " "(s) prefer state-based acceptance when possible [default], " "(t) force transition-based acceptance, " "(m) mix state and transition-based acceptance, " - "(l) single-line output", 0 }, + "(l) single-line output, " + "(v) verbose properties", 0 }, { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, "LBTT's format (add =t to force transition-based acceptance even" " on Büchi automata)", 0 }, diff --git a/src/tests/readsave.test b/src/tests/readsave.test index 5abfcee16..34769e03f 100755 --- a/src/tests/readsave.test +++ b/src/tests/readsave.test @@ -741,3 +741,25 @@ EOF diff output4 expect4 diff output4b expect4 diff output4c expect4 + +$autfilt -Hv --small input4 >output5 + +cat >expect5< 0) R XFp0)' diff --git a/src/twa/twa.hh b/src/twa/twa.hh index 30aa17431..bc9dc6034 100644 --- a/src/twa/twa.hh +++ b/src/twa/twa.hh @@ -837,7 +837,16 @@ namespace spot void prop_deterministic(bool val) { - is.deterministic = val; + if (val) + { + // deterministic implies unambiguous + is.deterministic = true; + is.unambiguous = true; + } + else + { + is.deterministic = false; + } } bool prop_unambiguous() const diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc index 887ec9776..7fcb5b7c5 100644 --- a/src/twaalgos/hoa.cc +++ b/src/twaalgos/hoa.cc @@ -243,6 +243,7 @@ namespace spot bool newline = true; hoa_acceptance acceptance = Hoa_Acceptance_States; bool implicit_labels = false; + bool verbose = false; if (opt) while (*opt) @@ -264,6 +265,9 @@ namespace spot case 't': acceptance = Hoa_Acceptance_Transitions; break; + case 'v': + verbose = true; + break; default: throw std::runtime_error (std::string("unknown option for print_hoa(): ") + c); @@ -387,6 +391,13 @@ namespace spot } os << str; }; + // We do not support alternating automata so far, and it's + // probable that nobody cares about the "no-univ-branch" + // properties. The "univ-branch" properties seems more important + // to announce that the automaton might not be parsable by tools + // that do not support alternating automata. + if (verbose) + prop(" no-univ-branch"); implicit_labels = md.use_implicit_labels; if (implicit_labels) prop(" implicit-labels"); @@ -402,7 +413,12 @@ namespace spot prop(" complete"); if (md.is_deterministic) prop(" deterministic"); - if (aut->prop_unambiguous()) + // Deterministic automata are also unambiguous, so writing both + // properties seems redundant. People working on unambiguous + // automata are usually concerned about non-deterministic + // unambiguous automata. So do not mention "unambiguous" + // in the case of deterministic automata. + if (aut->prop_unambiguous() && (verbose || !md.is_deterministic)) prop(" unambiguous"); assert(!(aut->prop_stutter_invariant() && aut->prop_stutter_sensitive())); if (aut->prop_stutter_invariant()) diff --git a/src/twaalgos/hoa.hh b/src/twaalgos/hoa.hh index f201ec229..64d83ec6b 100644 --- a/src/twaalgos/hoa.hh +++ b/src/twaalgos/hoa.hh @@ -34,7 +34,7 @@ namespace spot /// option: (i) implicit labels for complete and /// deterministic automata, (s) state-based acceptance, (t) /// transition-based acceptance, (m) mixed acceptance, (l) - /// single-line output. + /// single-line output, (v) verbose properties. SPOT_API std::ostream& print_hoa(std::ostream& os, const const_twa_ptr& g, diff --git a/src/twaalgos/isunamb.cc b/src/twaalgos/isunamb.cc index 5621f5fa3..c85bb6efe 100644 --- a/src/twaalgos/isunamb.cc +++ b/src/twaalgos/isunamb.cc @@ -27,7 +27,7 @@ namespace spot { bool is_unambiguous(const const_twa_graph_ptr& aut) { - if (aut->prop_deterministic() || aut->prop_unambiguous()) + if (aut->prop_unambiguous()) return true; auto clean_a = scc_filter_states(aut); if (clean_a->num_edges() == 0)