From 33c496a4bbb6c76a10a8e073bd6606d48e726789 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 20 Feb 2015 13:16:46 +0100
Subject: [PATCH] acc: Add operators == and != for acc_code
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

and make sure are_isomorphic does not look only at the number of
acceptance sets

* src/tgba/acc.hh: Here.
* src/tgbaalgos/are_isomorphic.cc: Use it to ensure two automata
have the same acceptance condition.
* src/tgbatest/explpro4.test: Test product between Büchi and co-Büchi,
and make sure the isomorphic check look at the acceptance condition.
---
 src/tgba/acc.hh                 | 36 +++++++++++++++++++++++++++++++++
 src/tgbaalgos/are_isomorphic.cc |  6 ++++--
 src/tgbatest/explpro4.test      | 28 ++++++++++++++++++-------
 3 files changed, 61 insertions(+), 9 deletions(-)

diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh
index 3dd56361d..b00f300b9 100644
--- a/src/tgba/acc.hh
+++ b/src/tgba/acc.hh
@@ -211,6 +211,42 @@ namespace spot
 
     struct acc_code: public std::vector<acc_word>
     {
+      bool operator==(const acc_code& other)
+      {
+	unsigned pos = size();
+	if (other.size() != pos)
+	  return false;
+	while (pos > 0)
+	  {
+	    auto op = (*this)[pos - 1].op;
+	    auto sz = (*this)[pos - 1].size;
+	    if (other[pos - 1].op != op ||
+		other[pos - 1].size != sz)
+	      return false;
+	    switch (op)
+	      {
+	      case acc_cond::acc_op::And:
+	      case acc_cond::acc_op::Or:
+		--pos;
+		break;
+	      case acc_cond::acc_op::Inf:
+	      case acc_cond::acc_op::InfNeg:
+	      case acc_cond::acc_op::Fin:
+	      case acc_cond::acc_op::FinNeg:
+		pos -= 2;
+		if (other[pos].mark != (*this)[pos].mark)
+		  return false;
+		break;
+	      }
+	  }
+	return true;
+      };
+
+      bool operator!=(const acc_code& other)
+      {
+	return !(*this == other);
+      }
+
       bool is_true() const
       {
 	unsigned s = size();
diff --git a/src/tgbaalgos/are_isomorphic.cc b/src/tgbaalgos/are_isomorphic.cc
index ec192bb2f..97b2d823b 100644
--- a/src/tgbaalgos/are_isomorphic.cc
+++ b/src/tgbaalgos/are_isomorphic.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014 Laboratoire de Recherche et
+// Copyright (C) 2014, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -102,7 +102,9 @@ namespace
   {
     return aut1->num_states() != aut2->num_states() ||
       aut1->num_transitions() != aut2->num_transitions() ||
-      aut1->acc().num_sets() != aut2->acc().num_sets();
+      // FIXME: At some point, it would be nice to support reordering
+      // of acceptance sets (issue #58).
+      aut1->acc().get_acceptance() != aut2->acc().get_acceptance();
   }
 }
 
diff --git a/src/tgbatest/explpro4.test b/src/tgbatest/explpro4.test
index dc3648fa8..8852e0a71 100755
--- a/src/tgbatest/explpro4.test
+++ b/src/tgbatest/explpro4.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2009, 2014, 2015 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 # Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -47,7 +47,7 @@ States: 1
 Start: 0
 AP: 1 "a"
 acc-name: Buchi
-Acceptance: 1 Inf(0)
+Acceptance: 1 Fin(0)
 properties: trans-labels explicit-labels trans-acc complete deterministic
 --BODY--
 State: 0
@@ -61,8 +61,21 @@ HOA: v1
 States: 1
 Start: 0
 AP: 1 "a"
-acc-name: generalized-Buchi 2
-Acceptance: 2 Inf(0)&Inf(1)
+Acceptance: 2 Inf(0) & Fin(1)
+properties: trans-labels explicit-labels trans-acc complete deterministic
+--BODY--
+State: 0
+[!0] 0 {1}
+[0] 0 {0}
+--END--
+EOF
+
+cat >unexpected <<'EOF'
+HOA: v1
+States: 1
+Start: 0
+AP: 1 "a"
+Acceptance: 2 Inf(0) & Inf(1)
 properties: trans-labels explicit-labels trans-acc complete deterministic
 --BODY--
 State: 0
@@ -72,6 +85,7 @@ State: 0
 EOF
 
 run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout
-run 0 ../../bin/autfilt -F stdout --isomorph expected
+run 0 ../../bin/autfilt -q stdout --isomorph expected
+run 1 ../../bin/autfilt -q stdout --isomorph unexpected
 
-rm input1 input2 stdout expected
+true