From 8ec6ea838de92b0489b2c319f3c9246a1de00697 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 30 Jul 2019 15:30:36 +0200
Subject: [PATCH] twa_graph: fix precondition on set_init_state

Fixes #391.

* spot/twa/twagraph.hh: Here.
* tests/core/dualize.test, tests/python/except.py: New tests.
* NEWS: Mention the bug.
---
 NEWS                    |  6 +++-
 spot/twa/twagraph.hh    |  5 ++-
 tests/core/dualize.test | 79 ++++++++++++++++++++++++++++++++++++++++-
 tests/python/except.py  | 21 ++++++++++-
 4 files changed, 107 insertions(+), 4 deletions(-)

diff --git a/NEWS b/NEWS
index 148b1f905..7707c4312 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,10 @@
 New in spot 2.8.1.dev (not yet released)
 
-  Nothing yet.
+  Bugs fixed:
+
+  - Calling "autfilt --dualize" on an alternating automaton with
+    transition-based acceptance and universal initial states would
+    fail with "set_init_state() called with nonexisting state".
 
 New in spot 2.8.1 (2019-07-18)
 
diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh
index fcbdb97d8..090736096 100644
--- a/spot/twa/twagraph.hh
+++ b/spot/twa/twagraph.hh
@@ -285,7 +285,10 @@ namespace spot
 
     void set_init_state(state_num s)
     {
-      if (SPOT_UNLIKELY(s >= num_states()))
+      bool univ = is_univ_dest(s);
+      if (SPOT_UNLIKELY((!univ && s >= num_states())
+                        // univ destinations have at least length 2.
+                        || (univ && 2 + ~s >= g_.dests_vector().size())))
         throw std::invalid_argument
           ("set_init_state() called with nonexisting state");
       init_number_ = s;
diff --git a/tests/core/dualize.test b/tests/core/dualize.test
index 58ffa68d7..7e66c3b8f 100755
--- a/tests/core/dualize.test
+++ b/tests/core/dualize.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2017 Laboratoire de Recherche et
+# Copyright (C) 2017, 2019 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -65,3 +65,80 @@ EOF
 run 0 autfilt input1 --dualize --hoaf=t | tee stdout
 diff stdout expected
 rm input1 expected stdout
+
+# issue #391
+cat >input2 <<EOF
+HOA: v1
+States: 10
+Start: 0&4
+AP: 2 "p0" "p1"
+Acceptance: 2 Inf(0) | Inf(1)
+properties: trans-labels explicit-labels trans-acc univ-branch
+--BODY--
+State: 0
+[1] 1 {0}
+[0&!1] 2 {0}
+[!1] 3
+[!1] 0
+State: 1
+[t] 1 {0}
+State: 2
+[0] 2 {0}
+State: 3
+[1] 1 {0}
+[!1] 3
+State: 4
+[0] 5 {1}
+[t] 6
+[!0] 7 {1}
+[t] 4
+State: 5
+[!0] 8 {1}
+State: 6
+[!0] 9
+State: 7
+State: 8
+[t] 8 {1}
+State: 9
+[0] 8 {1}
+[!0] 9
+--END--
+EOF
+autfilt --dualize <input2 >output2
+cat >expected2<<EOF
+HOA: v1
+States: 9
+Start: 8
+AP: 2 "p0" "p1"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: trans-labels explicit-labels state-acc univ-branch
+--BODY--
+State: 0
+[!0&!1] 0&7
+[0&!1] 0&6&7
+State: 1
+[!0] 1&3
+[0] 1&2&3
+State: 2
+[0] 4
+State: 3
+[0] 4
+[!0] 5
+State: 4
+[t] 4
+State: 5
+[!0] 5
+State: 6 {0}
+[!0] 4
+[0] 6
+State: 7
+[!1] 7
+State: 8
+[!0] 1&3
+[t] 1&2&3
+[!0&!1] 0&7
+[!1] 0&6&7
+--END--
+EOF
+diff output2 expected2
diff --git a/tests/python/except.py b/tests/python/except.py
index d69417d22..598d70b6a 100644
--- a/tests/python/except.py
+++ b/tests/python/except.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -93,6 +93,25 @@ except RuntimeError as e:
 else:
     report_missing_exception()
 
+try:
+    alt.set_init_state(999)
+except ValueError as e:
+    assert "set_init_state()" in str(e)
+else:
+    report_missing_exception()
+
+alt.set_univ_init_state([s1, s2])
+u = alt.get_init_state_number()
+alt.set_init_state(u)
+
+try:
+    alt.set_init_state(u - 1)
+except ValueError as e:
+    assert "set_init_state()" in str(e)
+else:
+    report_missing_exception()
+
+
 r = spot.twa_run(aut)
 try:
     a = r.as_twa()