Simulation keeps track of simulated states in the input automaton.

* NEWS: Document the change.
* spot/twaalgos/simulation.cc: Implement the change.
* spot/twa/twagraph.cc: `copy_state_names_from` uses simulated states
  info if present.
* spot/twaalgos/determinize.cc: Pretty-print in determinization follows
  simulated states, avoiding possible confusion.
* tests/Makefile.am, tests/python/simstate.py: Add a test.

NEWS

@@ -54,6 +54,11 @@ New in spot 2.3.4.dev (not yet released)
     the second command outputs an automaton with states that show
     references to the first one.
 
+  - A new named property for automata called "simulated-states" can be
+    used to record the origin of a state through simulation. The
+    behavior is similar to "original-states" above. Determinization
+    takes advantage of this in its pretty print.
+
   - The new function spot::acc_cond::is_streett_like() checks whether
     an acceptance condition is conjunction of disjunctive clauses
     containing at most one Inf and at most one Fin.  It builds a

spot/twa/twagraph.cc

@@ -635,11 +635,22 @@ namespace spot
   {
     if (other == shared_from_this())
       return;
+
     auto orig = get_named_prop<std::vector<unsigned>>("original-states");
+    auto sims = get_named_prop<std::vector<unsigned>>("simulated-states");
+
+    if (orig && sims)
+      throw std::runtime_error("copy_state_names_from(): original-states and "
+                               "simulated-states are both set");
+
     if (orig && orig->size() != num_states())
       throw std::runtime_error("copy_state_names_from(): unexpected size "
                                "for original-states");
 
+    if (sims && sims->size() != other->num_states())
+      throw std::runtime_error("copy_state_names_from(): unexpected size "
+                               "for simulated-states");
+
     auto names = std::unique_ptr<std::vector<std::string>>
       (new std::vector<std::string>);
     unsigned ns = num_states();
@@ -647,11 +658,27 @@ namespace spot
 
     for (unsigned s = 0; s < ns; ++s)
       {
-        unsigned other_s = orig ? (*orig)[s] : s;
+        std::string newname = "";
-        if (other_s >= ons)
+        if (sims)
-          throw std::runtime_error("copy_state_names_from(): state does not"
+          {
-                                   " exist in source automaton");
+            for (unsigned t = 0; t < ons; ++t)
-        names->emplace_back(other->format_state(other_s));
+              {
+                if (s == (*sims)[t])
+                  newname += other->format_state(t) + ',';
+              }
+            assert(!newname.empty());
+            newname.pop_back(); // remove trailing comma
+            newname = '[' + newname + ']';
+          }
+        else
+          {
+            unsigned other_s = orig ? (*orig)[s] : s;
+            if (other_s >= ons)
+              throw std::runtime_error("copy_state_names_from(): state does not"
+                                       " exist in source automaton");
+            newname = other->format_state(other_s);
+          }
+        names->emplace_back(newname);
       }
 
     set_named_prop("state-names", names.release());

spot/twaalgos/determinize.cc

@@ -185,7 +185,8 @@ namespace spot
     }
 
     std::string
-    nodes_to_string(const safra_state::nodes_t& states)
+    nodes_to_string(const const_twa_graph_ptr& aut,
+                    const safra_state::nodes_t& states)
     {
       auto copy = sorted_nodes(states);
       std::ostringstream os;
@@ -223,7 +224,7 @@ namespace spot
             }
           if (!first)
             os << ' ';
-          os << n.first;
+          os << aut->format_state(n.first);
           first = false;
         }
       // Finish unwinding stack to print last braces
@@ -236,11 +237,12 @@ namespace spot
     }
 
     std::vector<std::string>*
-    print_debug(std::map<safra_state, int>& states)
+    print_debug(const const_twa_graph_ptr& aut,
+                const std::map<safra_state, int>& states)
     {
       auto res = new std::vector<std::string>(states.size());
-      for (auto& p: states)
+      for (const auto& p: states)
-        (*res)[p.second] = nodes_to_string(p.first.nodes_);
+        (*res)[p.second] = nodes_to_string(aut, p.first.nodes_);
       return res;
     }
 
@@ -576,11 +578,16 @@ namespace spot
 
     // Degeneralize
     twa_graph_ptr aut = spot::degeneralize_tba(a);
+    if (pretty_print)
+      aut->copy_state_names_from(a);
     std::vector<bdd> implications;
     if (use_simulation)
       {
         aut = spot::scc_filter(aut);
-        aut = simulation(aut, &implications);
+        auto aut2 = simulation(aut, &implications);
+        if (pretty_print)
+          aut2->copy_state_names_from(aut);
+        aut = aut2;
       }
     scc_info scc = scc_info(aut);
     std::vector<bool> is_connected = find_scc_paths(scc);
@@ -694,7 +701,7 @@ namespace spot
     res->prop_state_acc(false);
 
     if (pretty_print)
-      res->set_named_prop("state-names", print_debug(seen));
+      res->set_named_prop("state-names", print_debug(aut, seen));
     return res;
   }
 }

spot/twaalgos/simulation.cc

@@ -439,6 +439,10 @@ namespace spot
         res->copy_ap_of(a_);
         res->copy_acceptance_of(a_);
 
+        auto state_mapping = new std::vector<unsigned>();
+        state_mapping->resize(a_->num_states());
+        res->set_named_prop("simulated-states", state_mapping);
+
         // Non atomic propositions variables (= acc and class)
         bdd nonapvars = all_proms_ & bdd_support(all_class_var_);
 
@@ -454,6 +458,9 @@ namespace spot
             // its class, or by all the implied classes.
             auto s = gb->new_state(cl.id());
             gb->alias_state(s, relation_[cl].id());
+            // update state_mapping
+            for (auto& st : p.second)
+              (*state_mapping)[st] = s;
             if (implications)
               (*implications)[s] = relation_[cl];
           }

tests/Makefile.am

@@ -362,6 +362,7 @@ TESTS_python = \
   python/sccinfo.py \
   python/setacc.py \
   python/setxor.py \
+  python/simstate.py \
   python/rs_like.py \
   python/sum.py \
   python/trival.py \

tests/python/simstate.py

@@ -0,0 +1,169 @@
+# -*- mode: python; coding: utf-8 -*-
+# Copyright (C) 2015, 2017  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
+from sys import exit
+
+aut = spot.automaton("""
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0
+[t] 1 {0}
+State: 1
+[t] 1 {0}
+--END--
+""")
+
+aut2 = spot.simulation(aut)
+assert aut2.to_str() == """HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic
+--BODY--
+State: 0 {0}
+[t] 0
+--END--"""
+
+aut2.copy_state_names_from(aut)
+assert aut2.to_str() == """HOA: v1
+States: 1
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored complete
+properties: deterministic
+--BODY--
+State: 0 "[0,1]" {0}
+[t] 0
+--END--"""
+
+aut = spot.translate('GF((p0 -> Gp0) R p1)')
+
+daut = spot.tgba_determinize(aut, True)
+assert daut.to_str() == """HOA: v1
+States: 3
+Start: 0
+AP: 2 "p1" "p0"
+acc-name: parity min odd 4
+Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))
+properties: trans-labels explicit-labels trans-acc complete
+properties: deterministic stutter-invariant
+--BODY--
+State: 0 "{₀[1]₀}"
+[0&1] 1 {3}
+[!0&1] 0
+[0&!1] 0 {1}
+[!0&!1] 0
+State: 1 "{₀[1]{₂[0]₂}₀}{₁[2]₁}"
+[0&1] 1 {3}
+[!0&1] 2
+[0&!1] 0 {1}
+[!0&!1] 0 {2}
+State: 2 "{₀[1]₀}{₁[2]₁}"
+[0&1] 1 {3}
+[!0&1] 2
+[0&!1] 0 {1}
+[!0&!1] 0 {2}
+--END--"""
+
+aut = spot.automaton("""
+HOA: v1
+States: 2
+Start: 0
+AP: 2 "a" "b"
+Acceptance: 2 Inf(0)&Inf(1)
+--BODY--
+State: 0
+[0] 0
+[1] 1 {1}
+State: 1
+[0] 1 {0}
+[1] 0
+--END--
+""")
+
+daut = spot.tgba_determinize(aut, True)
+assert daut.to_str() == """HOA: v1
+States: 12
+Start: 0
+AP: 2 "a" "b"
+acc-name: parity min odd 4
+Acceptance: 4 Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))
+properties: trans-labels explicit-labels trans-acc deterministic
+--BODY--
+State: 0 "{₀[0,0]₀}"
+[0&!1] 0
+[0&1] 1
+[!0&1] 2
+State: 1 "{₀[0,0] [1]₀}"
+[0&!1] 3
+[0&1] 4
+[!0&1] 1
+State: 2 "{₀[1]₀}"
+[0&!1] 5 {1}
+[0&1] 3
+[!0&1] 0
+State: 3 "{₀[0,0]{₁[1]₁}₀}"
+[0&!1] 3
+[0&1] 6
+[!0&1] 7
+State: 4 "{₀[0,0] [1]{₁[1]₁}₀}"
+[0&!1] 3
+[0&1] 6
+[!0&1] 7
+State: 5 "{₀[1]₀}"
+[0&!1] 5
+[0&1] 8
+[!0&1] 0
+State: 6 "{₀[1]{₁[0,0] [1]₁}₀}"
+[0&!1] 8 {1}
+[0&1] 9 {1}
+[!0&1] 1 {1}
+State: 7 "{₀[1]{₁[0,0]₁}₀}"
+[0&!1] 8 {1}
+[0&1] 9 {1}
+[!0&1] 10
+State: 8 "{₀[0,0] [1]₀}"
+[0&!1] 8
+[0&1] 9
+[!0&1] 1
+State: 9 "{₀[0,0] [1] [1]₀}"
+[0&!1] 3
+[0&1] 4
+[!0&1] 1
+State: 10 "{₀[0,0]{₁[1]₁}₀}"
+[0&!1] 3 {3}
+[0&1] 11
+[!0&1] 7
+State: 11 "{₀[1]{₁[0,0]{₂[1]₂}₁}₀}"
+[0&!1] 8 {1}
+[0&1] 9 {1}
+[!0&1] 1 {1}
+--END--"""
+