From 72eed9b2e234ad39b6cb5440b04d29dcb2dfb4fc Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 17 Mar 2015 18:29:28 +0100
Subject: [PATCH] sat: add missing prop_state_based_acc() call

Fixes #62.

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Add call to
prop_state_based_acc() when building an automaton with state-based
acceptance.
* src/tgbatest/satmin2.test: New test.
* doc/org/satmin.org: Update.
---
 doc/org/satmin.org        | 14 +++++++-------
 src/tgbaalgos/dtbasat.cc  |  2 ++
 src/tgbaalgos/dtgbasat.cc |  3 ++-
 src/tgbatest/satmin2.test |  6 ++++++
 4 files changed, 17 insertions(+), 8 deletions(-)

diff --git a/doc/org/satmin.org b/doc/org/satmin.org
index da9eedf25..eb137ae75 100644
--- a/doc/org/satmin.org
+++ b/doc/org/satmin.org
@@ -162,17 +162,17 @@ digraph G {
   0 -> 0 [label=<!a &amp; b>]
   0 -> 1 [label=<!b>]
   0 -> 2 [label=<a &amp; b>]
-  1 [label="1"]
-  1 -> 4 [label=<!a<br/><font color="#5DA5DA">⓿</font>>]
-  1 -> 5 [label=<a<br/><font color="#5DA5DA">⓿</font>>]
+  1 [label="1", peripheries=2]
+  1 -> 4 [label=<!a>]
+  1 -> 5 [label=<a>]
   2 [label="2"]
   2 -> 1 [label=<!b>]
   2 -> 4 [label=<!a &amp; b>]
   2 -> 5 [label=<a &amp; b>]
-  3 [label="3"]
-  3 -> 0 [label=<!a<br/><font color="#5DA5DA">⓿</font>>]
-  3 -> 1 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
-  3 -> 2 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
+  3 [label="3", peripheries=2]
+  3 -> 0 [label=<!a>]
+  3 -> 1 [label=<a &amp; !b>]
+  3 -> 2 [label=<a &amp; b>]
   4 [label="4"]
   4 -> 0 [label=<!a &amp; !b>]
   4 -> 1 [label=<a &amp; b>]
diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc
index fefff6535..cb47abaa9 100644
--- a/src/tgbaalgos/dtbasat.cc
+++ b/src/tgbaalgos/dtbasat.cc
@@ -639,6 +639,8 @@ namespace spot
       auto a = make_tgba_digraph(autdict);
       a->copy_ap_of(aut);
       acc_cond::mark_t acc = a->set_single_acceptance_set();
+      if (state_based)
+	a->prop_state_based_acc();
       a->new_states(satdict.cand_size);
 
       unsigned last_aut_trans = -1U;
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index 1798a91ff..230a67f62 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/src/tgbaalgos/dtgbasat.cc
@@ -780,7 +780,8 @@ namespace spot
       auto a = make_tgba_digraph(autdict);
       a->copy_ap_of(aut);
       a->set_generalized_buchi(satdict.cand_nacc);
-
+      if (state_based)
+	a->prop_state_based_acc();
       a->new_states(satdict.cand_size);
 
       // Last transition set in the automaton.
diff --git a/src/tgbatest/satmin2.test b/src/tgbatest/satmin2.test
index 5e37d3475..b8a0cacaf 100755
--- a/src/tgbatest/satmin2.test
+++ b/src/tgbatest/satmin2.test
@@ -57,3 +57,9 @@ EOF
 
 ../ltl2tgba -RS1 -kt -XH input.hoa > output
 diff output expected
+
+# At some point, this formula was correctly minimized, but
+# the output was not marked as state-based.
+../../bin/ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -H >out
+grep 'properties:.*state-acc' out
+grep 'properties:.*deterministic' out