postproc: do not simplify BA via transitions-based simulation

This addresses the easy part of #79.

* src/twaalgos/postproc.cc: If the input is already BA and we want a BA
as output, do not try the transition-based simulation only to
degeneralize the result.
* src/tests/optba.test: New file.
* src/tests/Makefile.am: Add it.

src/tests/Makefile.am

@@ -172,6 +172,7 @@ TESTS_twa = \
   det.test \
   neverclaimread.test \
   hoaparse.test \
+  optba.test \
   complete.test \
   remfin.test \
   dstar.test \

src/tests/optba.test

@@ -0,0 +1,163 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2015 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+
+# This is a case where autfilt is used to optimize BA, but used to
+# produce a larger one.   See issue #79.
+
+autfilt=../../bin/autfilt
+
+# ltldo -s -f '!(((p1 W c1) U Gp2) || (GXc2 <-> F!F!c1))' 'ltl3ba -M0'
+cat >input <<EOF
+never {
+T0_init:
+  if
+  :: ((!(c1)) && (!(p1)) && (!(p2))) -> goto accept_S1
+  :: ((!(c1)) && (!(p1))) -> goto T0_S2
+  :: ((!(c1)) && (!(p2))) -> goto T0_S3
+  :: ((true)) -> goto T0_S4
+  :: ((!(c1)) && (!(p1)) && (!(p2))) -> goto T0_S5
+  :: ((!(c1)) && (!(p1))) -> goto T0_S6
+  :: ((!(c1)) && (!(p2))) -> goto T0_S7
+  :: ((true)) -> goto T0_S8
+  fi;
+accept_S1:
+  if
+  :: ((!(c1)) && (c2)) -> goto accept_S1
+  :: ((c2)) -> goto T0_S9
+  fi;
+T0_S2:
+  if
+  :: ((c2) && (!(p2))) -> goto T0_S9
+  :: ((c2)) -> goto T0_S2
+  fi;
+T0_S3:
+  if
+  :: ((!(c1)) && (c2) && (!(p1))) -> goto accept_S1
+  :: ((!(c1)) && (c2)) -> goto T0_S3
+  fi;
+T0_S4:
+  if
+  :: ((!(c1)) && (c2) && (!(p1)) && (!(p2))) -> goto accept_S1
+  :: ((!(c1)) && (c2) && (!(p1))) -> goto T0_S2
+  :: ((!(c1)) && (c2) && (!(p2))) -> goto T0_S3
+  :: ((c2) && (!(p2))) -> goto T0_S10
+  :: ((!(c1)) && (c2) && (!(p2))) -> goto accept_S11
+  :: ((c2)) -> goto T0_S4
+  fi;
+T0_S5:
+  if
+  :: ((true)) -> goto T0_S5
+  :: ((!(c2))) -> goto T0_S12
+  fi;
+T0_S6:
+  if
+  :: ((!(p2))) -> goto T0_S5
+  :: ((true)) -> goto T0_S6
+  :: ((!(c2)) && (!(p2))) -> goto T0_S12
+  :: ((!(c2))) -> goto T0_S13
+  fi;
+T0_S7:
+  if
+  :: ((!(c1)) && (!(p1))) -> goto T0_S5
+  :: ((!(c1))) -> goto T0_S7
+  :: ((!(c1)) && (!(c2)) && (!(p1))) -> goto T0_S12
+  :: ((!(c1)) && (!(c2))) -> goto T0_S14
+  fi;
+T0_S8:
+  if
+  :: ((!(c1)) && (!(p1)) && (!(p2))) -> goto T0_S5
+  :: ((!(c1)) && (!(p1))) -> goto T0_S6
+  :: ((!(c1)) && (!(p2))) -> goto T0_S7
+  :: ((!(c1)) && (!(c2)) && (!(p1)) && (!(p2))) -> goto T0_S12
+  :: ((!(c1)) && (!(c2)) && (!(p1))) -> goto T0_S13
+  :: ((!(c1)) && (!(c2)) && (!(p2))) -> goto T0_S14
+  :: ((!(c2))) -> goto T0_S18
+  :: ((true)) -> goto T0_S8
+  fi;
+T0_S9:
+  if
+  :: ((!(c1)) && (c2)) -> goto accept_S1
+  :: ((c2)) -> goto T0_S9
+  fi;
+T0_S10:
+  if
+  :: ((!(c1)) && (c2) && (!(p1)) && (!(p2))) -> goto accept_S1
+  :: ((!(c1)) && (c2) && (!(p1))) -> goto T0_S2
+  :: ((!(c1)) && (c2) && (!(p2))) -> goto T0_S3
+  :: ((c2)) -> goto T0_S10
+  :: ((!(c1)) && (c2)) -> goto accept_S11
+  fi;
+accept_S11:
+  if
+  :: ((!(c1)) && (c2) && (!(p1)) && (!(p2))) -> goto accept_S1
+  :: ((!(c1)) && (c2) && (!(p1))) -> goto T0_S2
+  :: ((!(c1)) && (c2) && (!(p2))) -> goto T0_S3
+  :: ((c2) && (!(p2))) -> goto T0_S10
+  :: ((!(c1)) && (c2) && (!(p2))) -> goto accept_S11
+  :: ((c2)) -> goto T0_S4
+  fi;
+T0_S12:
+  if
+  :: ((true)) -> goto T0_S12
+  :: ((c1)) -> goto accept_S15
+  fi;
+T0_S13:
+  if
+  :: ((!(p2))) -> goto T0_S12
+  :: ((c1) && (!(p2))) -> goto accept_S15
+  :: ((true)) -> goto T0_S13
+  fi;
+T0_S14:
+  if
+  :: ((!(c1)) && (!(p1))) -> goto T0_S12
+  :: ((!(c1))) -> goto T0_S14
+  fi;
+accept_S15:
+  if
+  :: ((c1)) -> goto accept_S15
+  fi;
+accept_S16:
+  if
+  :: ((c1) && (!(p2))) -> goto accept_S16
+  :: ((c1)) -> goto T0_S17
+  fi;
+T0_S17:
+  if
+  :: ((c1) && (!(p2))) -> goto accept_S16
+  :: ((c1)) -> goto T0_S17
+  fi;
+T0_S18:
+  if
+  :: ((!(c1)) && (!(p1)) && (!(p2))) -> goto T0_S12
+  :: ((!(c1)) && (!(p1))) -> goto T0_S13
+  :: ((!(c1)) && (!(p2))) -> goto T0_S14
+  :: ((c1)) -> goto T0_S17
+  :: ((true)) -> goto T0_S18
+  fi;
+}
+EOF
+
+# 18 states is fine for transition-based acceptance
+test `$autfilt --exclusive-ap=c1,c2 --high --small --stats=%s input` = 18
+
+# But we should have 19 with Büchi acceptance, not 20.
+test `$autfilt --exclusive-ap=c1,c2 --high --small -B --stats=%s input` = 19

src/twaalgos/postproc.cc

@@ -109,6 +109,8 @@ namespace spot
   twa_graph_ptr
   postprocessor::do_ba_simul(const twa_graph_ptr& a, int opt)
   {
+    if (ba_simul_ <= 0)
+      return a;
     switch (opt)
       {
       case 0:
@@ -130,8 +132,6 @@ namespace spot
 			  degen_reset_, degen_order_,
 			  degen_cache_, degen_lskip_,
 			  degen_lowinit_);
-    if (ba_simul_ <= 0)
-      return d;
     return do_ba_simul(d, ba_simul_);
   }
 
@@ -243,11 +243,18 @@ namespace spot
     // at hard levels if we want a small output.
     if (!dba || (level_ == High && PREF_ == Small))
       {
-	sim = do_simul(a, simul_);
+	if (type_ == BA && a->is_sba() && !tba_determinisation_)
-	// Degeneralize the result of the simulation if needed.
+	  {
-	// No need to do that if tba_determinisation_ will be used.
+	    sim = do_ba_simul(a, ba_simul_);
-	if (type_ == BA && !tba_determinisation_)
+	  }
-	  sim = do_degen(sim);
+	else
+	  {
+	    sim = do_simul(a, simul_);
+	    // Degeneralize the result of the simulation if needed.
+	    // No need to do that if tba_determinisation_ will be used.
+	    if (type_ == BA && !tba_determinisation_)
+	      sim = do_degen(sim);
+	  }
       }
 
     // If WDBA failed, but the simulation returned a deterministic
@@ -401,7 +408,6 @@ namespace spot
 	  sim = nullptr;
       }
 
-
     if (type_ == TGBA && level_ == High && scc_filter_ != 0)
       {
 	if (dba && !dba_is_minimal) // WDBA is already clean.