From 7144efabb927f2c1fbee02c1378672ef5fe8c1e8 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 20 Apr 2016 15:19:14 +0200
Subject: [PATCH] hoa: add option to output version 1.1

* spot/twaalgos/hoa.cc: Implement the option.
* bin/common_aoutput.cc, doc/org/hoa.org,
doc/org/oaut.org, spot/twaalgos/hoa.hh, NEWS: Document it.
* tests/core/strength.test: Test that.
---
 NEWS                     |   9 +
 bin/common_aoutput.cc    |   3 +-
 doc/org/hoa.org          |  18 ++
 doc/org/oaut.org         |  47 +++++
 spot/twaalgos/hoa.cc     |  40 ++++-
 spot/twaalgos/hoa.hh     |   3 +-
 tests/core/strength.test | 369 ++++++++++++++++++++++++++++++++++++++-
 7 files changed, 484 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index 525dac33c..fd86eb0e3 100644
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,14 @@
 New in spot 2.0a (not yet released)
 
+  Library:
+
+  * The print_hoa() function will now output version 1.1 of the HOA
+    format when passed the "1.1" option (i.e., use -H1.1 from any
+    command-line tool).  As far as Spot is concerned, this allows
+    negated properties to be expressed.  Version 1 of the HOA format
+    is still the default, but we plan to default to version 1.1 in the
+    future.
+
   Bug fixes:
 
   * Typo in documentation of the -H option in --help output.
diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc
index a966c40bf..285234b45 100644
--- a/bin/common_aoutput.cc
+++ b/bin/common_aoutput.cc
@@ -101,8 +101,9 @@ static const argp_option options[] =
       "(+INT) add INT to all set numbers, "
       "(<INT) display at most INT states, "
       "(#) show internal edge numbers", 0 },
-    { "hoaf", 'H', "i|k|l|m|s|t|v", OPTION_ARG_OPTIONAL,
+    { "hoaf", 'H', "1.1|i|k|l|m|s|t|v", OPTION_ARG_OPTIONAL,
       "Output the automaton in HOA format (default).  Add letters to select "
+      "(1.1) version 1.1 of the format, "
       "(i) use implicit labels for complete deterministic automata, "
       "(s) prefer state-based acceptance when possible [default], "
       "(t) force transition-based acceptance, "
diff --git a/doc/org/hoa.org b/doc/org/hoa.org
index 72c61b790..64dae991e 100644
--- a/doc/org/hoa.org
+++ b/doc/org/hoa.org
@@ -21,6 +21,13 @@ some information that are useful to better understand the behavior
 of the tools distributed by Spot, and it also look at some lower-level,
 discussing details that are interesting when programming with Spot.
 
+Spot can read files written using either version 1 or version 1.1 of
+the HOA format.  It currently outputs version 1 by default, but
+version 1.1 can be requested from the command-line using option
+=-H1.1=.  Future version of Spot are likely to switch to version 1.1
+of HOA by default, so version 1 can already be requested explicitly
+using =-H1=.
+
 * Format, files, and TωA
 
 Some note about the abbreviation first.  We usually write "HOA format"
@@ -48,6 +55,9 @@ the HOA format, the output may not be exactly the same as the input.
   deterministic" or "deterministic") automata are currently supported
   by Spot.
 
+- Automata using explicit alphabet (introduced in version 1.1 of the format
+  via =Alphabet:=) are not supported.
+
 - The maximum number of acceptance sets used is (currently) limited
   to 32.
 
@@ -672,6 +682,14 @@ particular:
 | =inherently-weak=   | trusted | yes    | as stored if (=-Hv= or not =weak=)          | can be checked with =--check=strength=                           |
 | =colored=           | ignored | no     | checked                                     |                                                                  |
 
+The above table is for version 1 of the format.  When version 1.1 is
+selected (using =-H1.1=), some negated properties may be output.  In
+particular, =stutter-sensitive= is replaced by =!stutter-invariant=.
+The logic of not cluttering the output with all of =!terminal=,
+=!weak=, and =!inhenrently-weak= is similar to the positive versions:
+=!inherently-weak= implies =!weak= which in turn implies =!terminal=,
+so only one of those is emitted unless =-Hv= is used.
+
 ** Named properties
 
 In addition to the bit properties discussed above, a TωA can carry
diff --git a/doc/org/oaut.org b/doc/org/oaut.org
index 5ad6aa41a..b9cf5e85c 100644
--- a/doc/org/oaut.org
+++ b/doc/org/oaut.org
@@ -391,6 +391,53 @@ HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptanc
 HOA: v1 name: "(Gb | F!a) W c" States: 5 Start: 1 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc stutter-invariant --BODY-- State: 0 [0] 0 {0} State: 1 [0&1&!2] 0 [!1&!2] 1 {0} [1&!2] 2 [2] 3 State: 2 [!1&!2] 1 {0} [1&!2] 2 [!1&2] 3 [1&2] 4 State: 3 [t] 3 {0} State: 4 [!1] 3 [1] 4 --END--
 #+END_SRC
 
+Finally, version 1.1 of the HOA format can be specified using the
+=-H1.1= option.  Version 1, which is currently the default, can also
+be requested explicitly using =-H1=.  The main advantage of version
+1.1, as far as Spot is concerned, is that some of negated properties
+can be transmitted.  For instance, compare
+
+#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
+ltl2tgba -f GFa -f FGa -H1 --check | grep -E '^(HOA|properties|name):'
+#+END_SRC
+
+#+RESULTS:
+#+BEGIN_SRC hoa
+HOA: v1
+name: "GFa"
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic stutter-invariant
+HOA: v1
+name: "FGa"
+properties: trans-labels explicit-labels state-acc stutter-invariant
+properties: weak
+#+END_SRC
+
+versus
+
+#+BEGIN_SRC sh :results verbatim :exports both :wrap SRC hoa
+ltl2tgba -f GFa -f FGa -H1.1 --check | grep -E '^(HOA|properties|name):'
+#+END_SRC
+
+#+RESULTS:
+#+BEGIN_SRC hoa
+HOA: v1.1
+name: "GFa"
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic stutter-invariant !inherently-weak
+HOA: v1.1
+name: "FGa"
+properties: trans-labels explicit-labels state-acc !complete
+properties: !deterministic !unambiguous stutter-invariant weak
+properties: !terminal
+#+END_SRC
+
+The =--check= option inspects the automata for additional properties
+such that their strength or whether they are stutter-invariant and
+unambiguous.  You can see in this example that version 1.1 of the
+format carries additional negated properties that could not be
+represented in the first version.
+
 * LBTT output
 
 The [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] output has two flavors: state-based (which is used to output
diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc
index 74a8bb128..9110d39c7 100644
--- a/spot/twaalgos/hoa.cc
+++ b/spot/twaalgos/hoa.cc
@@ -252,12 +252,29 @@ namespace spot
     bool implicit_labels = false;
     bool verbose = false;
     bool state_labels = false;
+    bool v1_1 = false;
 
     if (opt)
       while (*opt)
         {
           switch (char c = *opt++)
             {
+            case '1':
+              if (opt[0] == '.' && opt[1] == '1')
+                {
+                  v1_1 = true;
+                  opt += 2;
+                }
+              else if (opt[0] == '.' && opt[1] == '0')
+                {
+                  v1_1 = false;
+                  opt += 2;
+                }
+              else
+                {
+                  v1_1 = false;
+                }
+              break;
             case 'i':
               implicit_labels = true;
               break;
@@ -297,7 +314,7 @@ namespace spot
     unsigned num_states = aut->num_states();
 
     const char nl = newline ? '\n' : ' ';
-    os << "HOA: v1" << nl;
+    os << (v1_1 ? "HOA: v1.1" : "HOA: v1") << nl;
     auto n = aut->get_named_prop<std::string>("automaton-name");
     if (n)
       escape_str(os << "name: \"", *n) << '"' << nl;
@@ -423,10 +440,16 @@ namespace spot
       prop(" trans-acc");
     if (md.is_colored)
       prop(" colored");
+    else if (verbose && v1_1)
+      prop(" !colored");
     if (md.is_complete)
       prop(" complete");
+    else if (v1_1)
+      prop(" !complete");
     if (md.is_deterministic)
       prop(" deterministic");
+    else if (v1_1)
+      prop(" !deterministic");
     // Deterministic automata are also unambiguous, so writing both
     // properties seems redundant.  People working on unambiguous
     // automata are usually concerned about non-deterministic
@@ -434,16 +457,29 @@ namespace spot
     // in the case of deterministic automata.
     if (aut->prop_unambiguous() && (verbose || !md.is_deterministic))
       prop(" unambiguous");
+    else if (v1_1 && !aut->prop_unambiguous())
+      prop(" !unambiguous");
     if (aut->prop_stutter_invariant())
       prop(" stutter-invariant");
     if (!aut->prop_stutter_invariant())
-      prop(" stutter-sensitive");
+      {
+        if (v1_1)
+          prop(" !stutter-invariant");
+        else
+          prop(" stutter-sensitive");
+      }
     if (aut->prop_terminal())
       prop(" terminal");
     if (aut->prop_weak() && (verbose || aut->prop_terminal() != true))
       prop(" weak");
     if (aut->prop_inherently_weak() && (verbose || aut->prop_weak() != true))
       prop(" inherently-weak");
+    if (v1_1 && !aut->prop_terminal() && (aut->prop_weak() || verbose))
+      prop(" !terminal");
+    if (v1_1 && !aut->prop_weak() && (aut->prop_inherently_weak() || verbose))
+      prop(" !weak");
+    if (v1_1 && !aut->prop_inherently_weak())
+      prop(" !inherently-weak");
     os << nl;
 
     // If we want to output implicit labels, we have to
diff --git a/spot/twaalgos/hoa.hh b/spot/twaalgos/hoa.hh
index b5acff88f..5f9258555 100644
--- a/spot/twaalgos/hoa.hh
+++ b/spot/twaalgos/hoa.hh
@@ -35,7 +35,8 @@ namespace spot
   ///        deterministic automata, (k) state labels when possible,
   ///        (s) state-based acceptance when possible, (t)
   ///        transition-based acceptance, (m) mixed acceptance, (l)
-  ///        single-line output, (v) verbose properties.
+  ///        single-line output, (v) verbose properties, (1.1) use
+  ///        version 1.1 of the HOA format.
   SPOT_API std::ostream&
   print_hoa(std::ostream& os,
             const const_twa_ptr& g,
diff --git a/tests/core/strength.test b/tests/core/strength.test
index f9fe38811..50c0efe2a 100755
--- a/tests/core/strength.test
+++ b/tests/core/strength.test
@@ -588,4 +588,371 @@ State: 4
 EOF
 
 diff out expected
-autfilt -q expected
+
+# Test HOA v1.1
+autfilt expected -H1.1 --check > out2
+
+cat >expected2 <<EOF
+HOA: v1.1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc !complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0
+[1] 1
+[0&!1] 0
+State: 1 {0}
+[t] 1
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0 {0}
+[0] 1
+[!0] 0
+State: 1 {0}
+[t] 0
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0 {0}
+[0] 1
+[!0] 0
+State: 1 {0}
+[t] 0
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0 {0}
+[t] 1
+State: 1 {0}
+[t] 0
+--END--
+HOA: v1.1
+States: 4
+Start: 0
+AP: 2 "a" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0
+[!0&!1] 0
+[0&!1] 1
+[1] 2
+State: 1
+[!0&!1] 0
+[0&!1] 1
+[!0&1] 2
+[0&1] 3
+State: 2 {0}
+[t] 2
+State: 3
+[!0] 2
+[0] 3
+--END--
+HOA: v1.1
+States: 1
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored !complete
+properties: deterministic stutter-invariant weak !terminal
+--BODY--
+State: 0 {0}
+[!0] 0
+--END--
+HOA: v1.1
+States: 3
+Start: 0
+AP: 3 "b" "a" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc !complete
+properties: !deterministic !unambiguous weak !terminal
+--BODY--
+State: 0
+[0&1&!2] 1
+[!1&!2] 0
+[1&!2] 2
+State: 1 {0}
+[0] 1
+State: 2
+[!1&!2] 0
+[1&!2] 2
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 2 "a" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc !complete
+properties: deterministic stutter-invariant !inherently-weak
+--BODY--
+State: 0
+[!0&!1] 0 {0}
+[0&!1] 1
+State: 1
+[!0&!1] 0 {0}
+[0&!1] 1
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc !complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0
+[1] 1
+[0&!1] 0
+State: 1 {0}
+[t] 1
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0 {0}
+[0] 1
+[!0] 0
+State: 1 {0}
+[t] 0
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0 {0}
+[0] 1
+[!0] 0
+State: 1 {0}
+[t] 0
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0 {0}
+[t] 1
+State: 1 {0}
+[t] 0
+--END--
+HOA: v1.1
+States: 1
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored !complete
+properties: deterministic stutter-invariant weak !terminal
+--BODY--
+State: 0 {0}
+[!0] 0
+--END--
+HOA: v1.1
+States: 5
+Start: 0
+AP: 3 "b" "a" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc !complete
+properties: !deterministic !unambiguous weak !terminal
+--BODY--
+State: 0
+[0&1&!2] 1
+[!1&!2] 0
+[1&!2] 2
+[2] 3
+State: 1 {0}
+[0] 1
+State: 2
+[!1&!2] 0
+[1&!2] 2
+[!1&2] 3
+[1&2] 4
+State: 3 {0}
+[t] 3
+State: 4
+[!1] 3
+[1] 4
+--END--
+HOA: v1.1
+States: 1
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored !complete
+properties: deterministic stutter-invariant weak !terminal
+--BODY--
+State: 0 {0}
+[!0] 0
+--END--
+HOA: v1.1
+States: 3
+Start: 0
+AP: 3 "b" "a" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc !complete
+properties: !deterministic !unambiguous !inherently-weak
+--BODY--
+State: 0
+[0&1&!2] 1
+[!1&!2] 0 {0}
+[1&!2] 2
+State: 1
+[0] 1 {0}
+State: 2
+[!1&!2] 0 {0}
+[1&!2] 2
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc !complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0
+[1] 1
+[0&!1] 0
+State: 1 {0}
+[t] 1
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0 {0}
+[0] 1
+[!0] 0
+State: 1 {0}
+[t] 0
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 1 "a"
+Acceptance: 2 Inf(0) | Inf(1)
+properties: trans-labels explicit-labels trans-acc colored complete
+properties: deterministic stutter-invariant inherently-weak !weak
+--BODY--
+State: 0
+[0] 1 {1}
+[!0] 0 {0}
+State: 1
+[t] 0 {0}
+--END--
+HOA: v1.1
+States: 2
+Start: 0
+AP: 0
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic stutter-invariant terminal
+--BODY--
+State: 0 {0}
+[t] 1
+State: 1 {0}
+[t] 0
+--END--
+HOA: v1.1
+States: 1
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored !complete
+properties: deterministic stutter-invariant weak !terminal
+--BODY--
+State: 0 {0}
+[!0] 0
+--END--
+HOA: v1.1
+States: 5
+Start: 0
+AP: 3 "b" "a" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc !complete
+properties: !deterministic !unambiguous !inherently-weak
+--BODY--
+State: 0
+[0&1&!2] 1
+[!1&!2] 0 {0}
+[1&!2] 2
+[2] 3
+State: 1
+[0] 1 {0}
+State: 2
+[!1&!2] 0 {0}
+[1&!2] 2
+[!1&2] 3
+[1&2] 4
+State: 3
+[t] 3 {0}
+State: 4
+[!1] 3
+[1] 4
+--END--
+EOF
+
+diff out2 expected2
+
+# Make sure no property are lost
+autfilt -H1.1 out2 > out3
+diff out3 expected2