From 97eedd7c5c58254b62a931de66a01d29eaf27581 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 24 Nov 2020 16:24:44 +0100
Subject: [PATCH] simulation: remove unnecessary iteration

This fixes #442.

* spot/twaalgos/simulation.cc (iterated_simulations_): Initialize next
so that we can exit after the first iteration if no change was made.
* NEWS: Mention the bug.
---
 NEWS                        | 4 ++++
 spot/twaalgos/simulation.cc | 8 ++++----
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/NEWS b/NEWS
index 9c46fdf6b..70418963d 100644
--- a/NEWS
+++ b/NEWS
@@ -152,6 +152,10 @@ New in spot 2.9.5.dev (not yet released)
   - twa_graph::merge_edges() could fail to merge two transitions if the
     destination transition was the first of the automaton.  (Issue #441)
 
+  - On non-deterministic automata, iterated_simulations() was
+    performing an (unnecessary) second iteration even when the first
+    one failed to reduce the automaton.  (Issue #442)
+
 New in spot 2.9.5 (2020-11-19)
 
   Bugs fixed:
diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc
index 41d049ef7..8f45e68d0 100644
--- a/spot/twaalgos/simulation.cc
+++ b/spot/twaalgos/simulation.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -70,13 +70,13 @@ namespace spot
       {
       }
 
-      automaton_size(const twa_graph_ptr& a)
+      automaton_size(const const_twa_graph_ptr& a)
         : edges(a->num_edges()),
           states(a->num_states())
       {
       }
 
-      void set_size(const twa_graph_ptr& a)
+      void set_size(const const_twa_graph_ptr& a)
       {
         states = a->num_states();
         edges = a->num_edges();
@@ -920,7 +920,7 @@ namespace spot
   {
     twa_graph_ptr res = nullptr;
     automaton_size prev;
-    automaton_size next;
+    automaton_size next(t);
 
     do
       {