From 4d82758726f722e490fe835288ece409d0b81279 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 16 May 2018 14:11:32 +0200
Subject: [PATCH] autfilt: --complement accepts non-deterministic input
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* bin/autfilt.cc: Fix the --help string for --complement, and also
merge edges in the resulting automaton, as suggested by František
Blahoudek.
* tests/core/complement.test: Adjust output and add František's
example.
---
 bin/autfilt.cc             |  8 +++++---
 tests/core/complement.test | 22 +++++++++++++++++++---
 2 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index e5b4e5451..cff6829c6 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -304,8 +304,7 @@ static const argp_option options[] =
     { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0,
       "remove unused acceptance sets from the automaton", 0 },
     { "complement", OPT_COMPLEMENT, nullptr, 0,
-      "complement each automaton (currently support only deterministic "
-      "automata)", 0 },
+      "complement each automaton (currently via determinization)", 0 },
     { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0,
       "complement the acceptance condition (without touching the automaton)",
       0 },
@@ -1423,7 +1422,10 @@ namespace
         }
 
       if (opt_complement)
-        aut = spot::dualize(ensure_deterministic(aut));
+        {
+          aut = spot::dualize(ensure_deterministic(aut));
+          aut->merge_edges();
+        }
 
       if (opt_dualize)
         aut = spot::dualize(aut);
diff --git a/tests/core/complement.test b/tests/core/complement.test
index 3ca643564..7d466f483 100755
--- a/tests/core/complement.test
+++ b/tests/core/complement.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015-2017 Laboratoire de Recherche et Développement de
+# Copyright (C) 2015-2018 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -50,7 +50,7 @@ EOF
 diff out expected
 
 
-ltl2tgba -H 'GFa & GFb' Xa Fa | autfilt --complement -H >out
+ltl2tgba -H 'GFa & GFb' Xa Fa 'FGa & FGb' | autfilt --complement -H >out
 cat >expected <<EOF
 HOA: v1
 States: 1
@@ -63,8 +63,8 @@ properties: deterministic stutter-invariant
 --BODY--
 State: 0
 [!0&!1] 0
-[!0&1] 0 {1}
 [0&!1] 0 {0}
+[!0&1] 0 {1}
 [0&1] 0 {0 1}
 --END--
 HOA: v1
@@ -101,6 +101,22 @@ State: 1
 [0] 0
 [!0] 1
 --END--
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: parity min even 2
+Acceptance: 2 Inf(0) | Fin(1)
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic stutter-invariant
+--BODY--
+State: 0
+[!0 | !1] 0
+[0&1] 1 {1}
+State: 1
+[!0 | !1] 0 {0}
+[0&1] 1 {1}
+--END--
 EOF
 diff out expected