From cbee5c1a3f5554b2342028df7ffd06ef30addf6a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 3 Feb 2015 09:21:13 +0100
Subject: [PATCH] hoaparse: detect duplicate atomic propositions

Reported by Joachim Klein.

* src/hoaparse/hoaparse.yy: Add a std::set to keep track of duplicate
propositions.
* src/tgbatest/hoaparse.test: Test it.
---
 src/hoaparse/hoaparse.yy   | 17 ++++++++++++++---
 src/tgbatest/hoaparse.test |  3 ++-
 2 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index f48c67e51..cda1be996 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -83,6 +83,7 @@
       spot::acc_cond::mark_t pos_acc_sets = 0U;
       std::vector<std::string>* state_names = nullptr;
       std::map<unsigned, unsigned> states_map;
+      std::set<int> ap_set;
       unsigned cur_state;
       int states = -1;
       int ap_count = -1;
@@ -523,17 +524,27 @@ ap-name: STRING
 	   if (!res.ignore_more_ap)
 	     {
 	       auto f = res.env->require(*$1);
+	       auto d = res.h->aut->get_dict();
+	       int b = 0;
 	       if (f == nullptr)
 		 {
 		   std::ostringstream out;
 		   out << "unknown atomic proposition \"" << *$1 << "\"";
-		   delete $1;
 		   error(@1, out.str());
 		   f = spot::ltl::default_environment::instance()
 		     .require("$unknown$");
+		   b = d->register_proposition(f, res.h->aut);
+		 }
+	       else
+		 {
+		   b = d->register_proposition(f, res.h->aut);
+		   if (!res.ap_set.emplace(b).second)
+		     {
+		       std::ostringstream out;
+		       out << "duplicate atomic proposition \"" << *$1 << "\"";
+		       error(@1, out.str());
+		     }
 		 }
-	       auto b =
-		 res.h->aut->get_dict()->register_proposition(f, res.h->aut);
 	       f->destroy();
 	       res.ap.push_back(b);
 	     }
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index e20ef1b31..8b2f88cab 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -145,7 +145,7 @@ EOF
 
 cat >input <<EOF
 HOA: v1
-AP: 1 "a"
+AP: 2 "a" "a"
 States: 0
 Start: 1
 --BODY--
@@ -155,6 +155,7 @@ State: 0 {0 1}
 EOF
 
 expecterr input <<EOF
+input:2.11-13: duplicate atomic proposition "a"
 input:4.1-8: initial state number is larger than state count...
 input:3.1-9: ... declared here.
 input:1.1-4.8: missing 'Acceptance:' header