hoa: output "unambiguous" only for non-deterministic automata by default

* src/twaalgos/hoa.cc: Output do not output "unambiguous" if the
automaton is deterministic.  Add option "v" to cancel this restriction,
and also output "no-univ-branch".
* src/twaalgos/hoa.hh: Document the "v" option.
* src/tests/readsave.test: Test it.
* src/tests/unambig.test: Adjust for unambiguous not being output
if the automaton is deterministic.
* src/bin/common_aoutput.cc, NEWS: Document it.
* doc/org/hoa.org: Add a summary table about how properties are handled.
* src/twa/twa.hh (prop_deterministic): Setting this should also
set the unambiguous property.
* src/twaalgos/isunamb.cc: Simplify the property check.

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().
 

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

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 },

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<<EOF
+HOA: v1
+States: 3
+Start: 1
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: no-univ-branch trans-labels explicit-labels state-acc
+properties: deterministic unambiguous inherently-weak
+--BODY--
+State: 0
+[1] 2
+State: 1
+[0] 0
+State: 2 {0}
+[0] 2
+--END--
+EOF
+diff output5 expect5

src/tests/unambig.test

@@ -36,8 +36,10 @@ for f in 'Ga' \
 do
   $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous
   $ltl2tgba -UH "!($f)" | $autfilt -q --is-unambiguous
-  $ltl2tgba -UH "$f" | $autfilt --check | grep unambiguous
-  $ltl2tgba -UH "!($f)" | $autfilt --check | grep unambiguous
+  $ltl2tgba -UH "$f" | $autfilt --check |
+      grep -E 'properties:.* (unambiguous|deterministic)'
+  $ltl2tgba -UH "!($f)" | $autfilt --check |
+      grep -E 'properties:.* (unambiguous|deterministic)'
 done
 
 for f in FGa '(({p1[*0..1]}[]-> 0) R XFp0)'

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

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())

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,

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)