Adding sat-based minimization for mealy machines

* spot/twaalgos/mealy_machine.hh,
spot/twaalgos/mealy_machine.cc: Here
* spot/twaalgos/Makefile.am: Here
* tests/python/mealy.py: Added tests
* tests/Makefile.am: Adding mealy.py
* python/spot/impl.i: Here

python/spot/impl.i

@@ -130,6 +130,7 @@
 #include <spot/twaalgos/determinize.hh>
 #include <spot/twaalgos/magic.hh>
 #include <spot/twaalgos/minimize.hh>
+#include <spot/twaalgos/mealy_machine.hh>
 #include <spot/twaalgos/neverclaim.hh>
 #include <spot/twaalgos/randomize.hh>
 #include <spot/twaalgos/remfin.hh>
@@ -638,6 +639,7 @@ def state_is_accepting(self, src) -> "bool":
 %include <spot/twaalgos/langmap.hh>
 %include <spot/twaalgos/magic.hh>
 %include <spot/twaalgos/minimize.hh>
+%include <spot/twaalgos/mealy_machine.hh>
 %include <spot/twaalgos/neverclaim.hh>
 %include <spot/twaalgos/randomize.hh>
 %include <spot/twaalgos/remfin.hh>

spot/twaalgos/Makefile.am

@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2008-2018, 2020 Laboratoire de Recherche et
+## Copyright (C) 2008-2018, 2020-2021 Laboratoire de Recherche et
 ## Développement de l'Epita (LRDE).
 ## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -66,6 +66,7 @@ twaalgos_HEADERS = \
   magic.hh \
   mask.hh \
   minimize.hh \
+  mealy_machine.hh \
   couvreurnew.hh \
   neverclaim.hh \
   parity.hh \
@@ -136,6 +137,7 @@ libtwaalgos_la_SOURCES = \
   magic.cc \
   mask.cc \
   minimize.cc \
+  mealy_machine.cc \
   couvreurnew.cc \
   ndfs_result.hxx \
   neverclaim.cc \

spot/twaalgos/mealy_machine.hh

@@ -0,0 +1,70 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 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/>.
+
+#pragma once
+
+#include <spot/twa/twagraph.hh>
+
+namespace spot
+{
+  /// \brief Minimizes an (in)completely specified mealy machine
+  ///        Based on signature inclusion or equality. This is not guaranteed
+  ///        to find the minimal number of states but is usually faster.
+  ///        This also comes at another drawback:
+  ///        All applicable sequences have to be infinite. Finite
+  ///        traces are disregarded
+  /// \Note The graph does not have to be split into env and player
+  ///        states as for minimize_mealy
+  SPOT_API
+  void minimize_mealy_fast_here(twa_graph_ptr& mm,
+                              bool use_inclusion = false);
+
+  /// \brief Like minimize_mealy_fast_here
+  SPOT_API
+  twa_graph_ptr minimize_mealy_fast(const const_twa_graph_ptr& mm,
+                                    bool use_inclusion = false);
+
+  /// \brief Minimizes an (in)completely specified mealy machine
+  ///        The approach is basically described in \cite abel2015memin
+  /// \param premin Use minimize_mealy_fast before applying the
+  ///               main algorithm if demanded AND
+  ///               the original machine has no finite trace.
+  ///               -1 : Do not use;
+  ///                0 : Use without inclusion;
+  ///                1 : Use with inclusion
+  /// \param keep_split Whether or not to keep the automaton states
+  ///                   partitioned into player and env states
+  /// \pre Graph must be split into env states and player states,
+  ///      such that they alternate. Edges leaving env states must be labeled
+  ///      with input proposition and edges leaving player states must be
+  ///      labeled with output propositions.
+  SPOT_API
+  twa_graph_ptr minimize_mealy(const const_twa_graph_ptr& mm,
+                               int premin = -1,
+                               bool keep_split = true);
+
+
+  /// \brief Test if the mealy machine \a right is a specialization of
+  /// the mealy machine \a left. That is all input sequences valid for left
+  /// must be applicable for right and the induced sequence of output signals
+  /// of right must imply the ones of left
+  SPOT_API bool is_mealy_specialization(const_twa_graph_ptr left,
+                                        const_twa_graph_ptr right,
+                                        bool verbose = false);
+}

tests/Makefile.am

@@ -409,6 +409,7 @@ TESTS_python = \
   python/ltlf.py \
   python/ltlparse.py \
   python/ltlsimple.py \
+  python/mealy.py \
   python/merge.py \
   python/mergedge.py \
   python/minato.py \

tests/python/mealy.py

@@ -0,0 +1,386 @@
+#!/usr/bin/python3
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2021 Laboratoire de Recherche et Développement de
+# l'EPITA.
+#
+# 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/>.
+
+import spot, buddy
+
+# Empty bdd intersection bug test
+# See issue #472
+true = buddy.bddtrue
+
+a = spot.make_twa_graph()
+o1 = buddy.bdd_ithvar(a.register_ap("o1"))
+o2 = buddy.bdd_ithvar(a.register_ap("o2"))
+no1 = buddy.bdd_not(o1)
+no2 = buddy.bdd_not(o2)
+a.new_states(6)
+a.new_edge(0,1,true)
+a.new_edge(1,2,no1)
+a.new_edge(2,3,true)
+a.new_edge(3,4,no2)
+a.new_edge(4,5,true)
+a.new_edge(5,4,(o1&no2)|(no1&o2))
+spot.set_state_players(a, [False,True,False,True,False,True])
+spot.set_synthesis_outputs(a, o1&o2)
+
+b = spot.minimize_mealy(a)
+assert(list(spot.get_state_players(b)).count(False) == 2)
+assert(spot.is_mealy_specialization(a, b))
+
+test_auts = [("""HOA: v1
+States: 22
+Start: 0
+AP: 6 "i0" "i1" "i2" "i3" "o0" "o1"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+spot-state-player: 0 1 0 1 0 1 0 1 0 1 1 0 1 0 1 0 1 1 0 1 0 1
+--BODY--
+State: 0
+[!2&3] 1
+[2&!3] 1
+[!2&!3] 1
+[!0&!1&2&3] 1
+[1&2&3] 3
+[0&!1&2&3] 5
+State: 1
+[!4&!5] 0
+State: 2
+[!2&3] 3
+[2&!3] 3
+[!2&!3] 3
+[!0&!1&2&3] 1
+[1&2&3] 7
+[0&!1&2&3] 5
+State: 3
+[!4&!5] 2
+State: 4
+[!2&3] 5
+[2&!3] 5
+[!2&!3] 5
+[!0&!1&2&3] 1
+[1&2&3] 3
+[0&!1&2&3] 14
+State: 5
+[!4&!5] 4
+State: 6
+[!2&3] 7
+[2&!3] 7
+[!2&!3] 7
+[!0&!1&2&3] 3
+[1&2&3] 9
+[0&!1&2&3] 5
+State: 7
+[!4&!5] 6
+State: 8
+[!2&3] 10
+[2&!3] 10
+[!2&!3] 10
+[!0&!1&2&3] 12
+[1&2&3] 10
+[0&!1&2&3] 5
+State: 9
+[!4&!5] 8
+State: 10
+[4&!5] 8
+State: 11
+[!2&3] 12
+[2&!3] 12
+[!2&!3] 12
+[!0&!1&2&3] 19
+[1&2&3] 3
+[0&!1&2&3] 5
+State: 12
+[!4&!5] 11
+State: 13
+[!2&3] 14
+[2&!3] 14
+[!2&!3] 14
+[!0&!1&2&3] 5
+[1&2&3] 3
+[0&!1&2&3] 16
+State: 14
+[!4&!5] 13
+State: 15
+[!2&3] 17
+[2&!3] 17
+[!2&!3] 17
+[!0&!1&2&3] 12
+[1&2&3] 3
+[0&!1&2&3] 17
+State: 16
+[!4&!5] 15
+State: 17
+[!4&5] 15
+State: 18
+[!2&3] 19
+[2&!3] 19
+[!2&!3] 19
+[!0&!1&2&3] 21
+[1&2&3] 3
+[0&!1&2&3] 5
+State: 19
+[!4&!5] 18
+State: 20
+[!2&3] 21
+[2&!3] 21
+[!2&!3] 21
+[!0&!1&2&3] 1
+[1&2&3] 3
+[0&!1&2&3] 5
+State: 21
+[!4&!5] 20
+--END--""", 7),
+("""HOA: v1
+States: 39
+Start: 0
+AP: 14 "i0" "i1" "i2" "i3" "i4" "i5" "i6" "o0" "o1" "o2" "o3" "o4" "o5" "o6"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc
+spot-state-player: 0 1 0 1 1 0 1 1 1 0 1 0 1 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 1 0
+                   1 1 1 1 0 1 0 0 0
+--BODY--
+State: 0
+[!0] 1
+[0&!1&!6] 3
+[0&!1&6] 4
+[0&1&!6] 6
+[0&1&6] 7
+State: 1
+[!7&!8&!9&!10&!11&!12&!13] 0
+State: 2
+[0&!1&!2] 8
+[0&!1&2&4] 10
+[0&!1&2&!4] 12
+[!0] 13
+[0&1] 14
+State: 3
+[!7&!8&9&10&!11&!13] 2
+State: 4
+[!7&!8&!9&10&!11&!13] 2
+State: 5
+[!0&!5] 31
+[0&1&!5] 32
+[!0&5] 33
+[0&!1] 8
+[0&1&5] 35
+State: 6
+[!7&!8&9&10&!11&12&!13] 5
+State: 7
+[!7&!8&!9&10&!11&12&!13] 5
+State: 8
+[!7&!8&!9&!10&!11&!13] 2
+State: 9
+[0&!1] 18
+[!0] 13
+[0&1] 14
+State: 10
+[7&!8&!9&!10&!11&!13] 9
+State: 11
+[0&!1] 16
+[!0] 13
+[0&1] 14
+State: 12
+[7&!8&!9&!10&!11&!13] 11
+State: 13
+[!7&!8&!9&12&!13] 5
+State: 14
+[!7&!8&!9&!10&!11&12&!13] 5
+State: 15
+[0&!1&!4] 12
+[0&!1&4] 10
+[!0] 13
+[0&1] 14
+State: 16
+[!7&!8&!9&!10&!11&!13] 15
+State: 17
+[0&!1&3] 10
+[0&!1&4] 10
+[0&!1&!3&!4] 20
+[!0] 13
+[0&1] 14
+State: 18
+[!7&!8&!9&!10&!11&!13] 17
+State: 19
+[0&!1&!5] 21
+[0&!1&5] 23
+[!0] 13
+[0&1] 14
+State: 20
+[!7&8&!9&!10&!11&12&!13] 19
+State: 21
+[!7&8&!9&!10&!11&!12&!13] 19
+State: 22
+[0&!1] 25
+[!0] 13
+[0&1] 14
+State: 23
+[!7&8&!9&!10&!11&!13] 22
+State: 24
+[0&!1&!5] 26
+[0&!1&5] 28
+[!0] 13
+[0&1] 14
+State: 25
+[!7&!8&!9&!10&!11&12&!13] 24
+State: 26
+[!7&!8&!9&!10&!11&!12&!13] 24
+State: 27
+[0&!1] 30
+[!0] 13
+[0&1] 14
+State: 28
+[7&!8&!9&!10&!11&!13] 27
+State: 29
+[0&!1&!2&3] 30
+[0&!1&!3&4] 4
+[0&!1&!3&!4] 20
+[0&!1&2&3] 28
+[!0] 13
+[0&1] 14
+State: 30
+[!7&!8&!9&!10&!11&!13] 29
+State: 31
+[!7&!8&!9&!12&!13] 5
+State: 32
+[!7&!8&!9&!10&!11&!12&!13] 5
+State: 33
+[!7&!8&!9&13] 0
+State: 34
+[0&1] 35
+[0&!1] 8
+[!0] 13
+State: 35
+[!7&!8&!9&!10&11&!13] 34
+State: 36
+[!0] 13
+State: 37
+[!0] 13
+State: 38
+[!0] 13
+--END--""", 13),
+("""HOA: v1
+States: 33
+Start: 0
+AP: 3 "i0" "i1" "o0"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+spot-state-player: 0 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0
+                   1 0 1
+--BODY--
+State: 0
+[0&!1] 2
+State: 1
+[0&!1] 4
+State: 2
+[2] 1
+State: 3
+[!0&!1] 6
+State: 4
+[2] 3
+State: 5
+[0&!1] 8
+State: 6
+[!2] 5
+State: 7
+[!0&!1] 10
+State: 8
+[2] 7
+State: 9
+[!0&1] 12
+State: 10
+[!2] 9
+State: 11
+[0&!1] 14
+State: 12
+[!2] 11
+State: 13
+[!0&!1] 16
+State: 14
+[!2] 13
+State: 15
+[!0&!1] 18
+State: 16
+[2] 15
+State: 17
+[!0&!1] 20
+State: 18
+[!2] 17
+State: 19
+[!0&!1] 22
+State: 20
+[2] 19
+State: 21
+[0&!1] 24
+State: 22
+[!2] 21
+State: 23
+[0&!1] 26
+State: 24
+[2] 23
+State: 25
+[!0&1] 28
+State: 26
+[2] 25
+State: 27
+[!0&!1] 30
+State: 28
+[2] 27
+State: 29
+[!0&1] 32
+State: 30
+[!2] 29
+State: 31
+State: 32
+[!2] 31
+--END--""", 3)
+]
+
+for (mealy_str, nenv_min) in test_auts:
+
+    mealy = spot.automaton(mealy_str)
+    mealy.merge_edges()
+    mealy_min_ks = spot.minimize_mealy(mealy, -1, True)
+    mealy_min_us = spot.minimize_mealy(mealy, -1, False)
+
+    n_e = sum([s == 0 for s in spot.get_state_players(mealy_min_ks)])
+    assert(n_e == nenv_min)
+    assert(mealy_min_us.num_states() == nenv_min)
+    assert(spot.is_mealy_specialization(mealy, mealy_min_ks, True))
+
+    outs = buddy.bddtrue
+    ins = buddy.bddtrue
+
+    for aap in mealy.ap():
+        if aap.ap_name().startswith("o"):
+            outs = outs & buddy.bdd_ithvar(mealy.register_ap(aap.ap_name()))
+        elif aap.ap_name().startswith("i"):
+            ins = ins & buddy.bdd_ithvar(mealy.register_ap(aap.ap_name()))
+        else:
+            assert("""Aps must start with either "i" or "o".""")
+    mealy_min_us_s = spot.split_2step(mealy_min_us, ins, outs, False, False)
+    assert(spot.is_mealy_specialization(mealy, mealy_min_us_s, True))
+
+
+
+
+
+