From d25cdd4c6c06efb27de1d23604909a3d422304a7 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 22 Apr 2017 14:36:11 +0200
Subject: [PATCH] ks_cobuchi: forbid n=0

* spot/gen/automata.hh: State the precondition.
* spot/gen/automata.cc: Catch n==0.
* tests/core/genaut.test: Test it.
---
 spot/gen/automata.cc   | 3 ++-
 spot/gen/automata.hh   | 3 ++-
 tests/core/genaut.test | 3 +++
 3 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc
index ed2fdde9e..39e83f507 100644
--- a/spot/gen/automata.cc
+++ b/spot/gen/automata.cc
@@ -29,6 +29,8 @@ namespace spot
     twa_graph_ptr
     ks_cobuchi(unsigned n)
     {
+      if (n == 0)
+        throw std::runtime_error("ks_cobuchi() expects a positive argument");
       // the alphabet has four letters:
       // i, s (for sigma), p (for pi), h (for hash)
       // we encode this four letters alphabet thanks to two AP a and b
@@ -86,4 +88,3 @@ namespace spot
     }
   }
 }
-
diff --git a/spot/gen/automata.hh b/spot/gen/automata.hh
index 8570e61fd..b4d5a0057 100644
--- a/spot/gen/automata.hh
+++ b/spot/gen/automata.hh
@@ -41,8 +41,9 @@ namespace spot
     ///     year={2015},
     ///     organization={Springer}
     /// }
+    ///
+    /// \pre n>0
     SPOT_API twa_graph_ptr
     ks_cobuchi(unsigned n);
   }
 }
-
diff --git a/tests/core/genaut.test b/tests/core/genaut.test
index 2660e942f..b6c08e714 100644
--- a/tests/core/genaut.test
+++ b/tests/core/genaut.test
@@ -36,3 +36,6 @@ cat >expected <<EOF
 7,20,48,1,Fin(0)
 EOF
 diff out expected
+
+genaut --ks-cobuchi=0 2>err && exit 1
+grep positive err