Fixed some issues with the strategy computation.

libraries/pbes/include/mcrl2/pbes/symbolic_parity_game.h

@@ -162,6 +162,71 @@ std::string print_nodes(const ldd& U, const ldd& V)
   return core::detail::print_set(u);
 }
 
+// print the indices of U (subset of V)
+std::string print_strategy(const ldd& S, const ldd& V)
+{
+  using namespace sylvan::ldds;
+
+  auto index = [](const std::vector<ldd>& v, const ldd& x)
+  {
+    auto i = std::find(v.begin(), v.end(), x);
+    if (i == v.end())
+    {
+      throw mcrl2::runtime_error("print_graph: index error");
+    }
+    return i - v.begin();
+  };
+
+  auto values = [](const ldd& X)
+  {
+    std::vector<ldd> result;
+    auto X_elements = ldd_solutions(X);
+    for (const auto& x: X_elements)
+    {
+      result.push_back(cube(x));
+    }
+    return std::make_pair(result, X_elements);
+  };
+
+  auto interleaved_values = [](const ldd& X)
+  {
+    std::vector<std::pair<ldd, ldd>> R;
+    std::vector<std::uint32_t> from;
+    std::vector<std::uint32_t> to;
+
+    auto X_elements = ldd_solutions(X);
+    for (const auto& x: X_elements)
+    {
+      // Take the interleaved strategy and compute two cubes.
+      auto it = x.begin();
+      from.clear();
+      to.clear();
+
+      while (it != x.end())
+      {
+        from.push_back(*it);
+        ++it;
+        to.push_back(*it);
+        ++it;
+      }
+
+      R.emplace_back(cube(from), cube(to));
+    }
+    return std::make_tuple(R, X_elements);
+  };
+
+  auto [V_values, V_solutions] = values(V);
+  auto [R_values, R_solutions] = interleaved_values(S);
+
+  std::vector<std::pair<std::size_t, std::size_t>> u;
+  for (const auto& [from, to]: R_values)
+  {
+    u.emplace_back(index(V_values, from), index(V_values, to));
+  }
+  return core::detail::print_map(u);
+}
+
+
 /// \brief maps proposition variable ldd values to (rank, is_disjunctive)
 std::map<std::size_t, std::pair<std::size_t, bool>> compute_equation_info(const pbes_system::srf_pbes& pbes, const std::vector<symbolic::data_expression_index>& data_index)
 {
@@ -311,6 +376,12 @@ class symbolic_parity_game
       return detail::print_nodes(V, m_all_nodes);
     }
 
+    /// \returns A string representing the given strategy in human readable form..
+    std::string print_strategy(const ldd& V) const
+    {
+      return detail::print_strategy(V, m_all_nodes);
+    }
+
     /// \returns A string representing the graph restricted to V.
     std::string print_graph(const ldd& V) const
     {

libraries/pbes/include/mcrl2/pbes/symbolic_pbessolve.h

@@ -63,7 +63,7 @@ class symbolic_pbessolve_algorithm
       {
         W[alpha] = union_(A, W_1[alpha]);
         W[1 - alpha] = empty_set();
-        strategy[alpha] = union_(merge(A_strategy, strategy_1[alpha]), merge(U, V));
+        strategy[alpha] = union_(union_(A_strategy, strategy_1[alpha]), merge(U, V));
         strategy[1 - alpha] = empty_set();
       }
       else
@@ -81,6 +81,9 @@ class symbolic_pbessolve_algorithm
       mCRL2log(log::trace) << "\n  --- zielonka solution for ---\n" << m_G.print_graph(V) << std::endl;
       mCRL2log(log::trace) << "W0 = " << m_G.print_nodes(W[0]) << std::endl;
       mCRL2log(log::trace) << "W1 = " << m_G.print_nodes(W[1]) << std::endl;
+      mCRL2log(log::trace) << "S0 = " << m_G.print_strategy(strategy[0]) << std::endl;
+      mCRL2log(log::trace) << "S1 = " << m_G.print_strategy(strategy[1]) << std::endl;
+
       assert(union_(W[0], W[1]) == V);
       return { W[0], W[1], strategy[0], strategy[1] };
     }
@@ -119,6 +122,9 @@ class symbolic_pbessolve_algorithm
       mCRL2log(log::verbose) << "finished solving (time = " << std::setprecision(2) << std::fixed << timer.seconds() << "s)\n";
       mCRL2log(log::trace) << "W0 = " << m_G.print_nodes(solved0) << std::endl;
       mCRL2log(log::trace) << "W1 = " << m_G.print_nodes(solved1) << std::endl;
+      mCRL2log(log::trace) << "S0 = " << m_G.print_strategy(strategy0) << std::endl;
+      mCRL2log(log::trace) << "S1 = " << m_G.print_strategy(strategy1) << std::endl;
+      // TODO: Print the strategy
       if (includes(solved0, initial_vertex))
       {
         return std::make_tuple(true, solved0, solved1, strategy0, strategy1);

tools/release/pbessolvesymbolic/pbessolvesymbolic.cpp

@@ -13,11 +13,13 @@
 #include <iomanip>
 #include <sylvan_ldd.hpp>
 
+#include "mcrl2/core/identifier_string.h"
 #include "mcrl2/data/rewriter_tool.h"
 #include "mcrl2/pbes/detail/pbes_io.h"
 #include "mcrl2/pbes/detail/pbes_remove_counterexample_info.h"
 #include "mcrl2/pbes/pbesinst_structure_graph.h"
 #include "mcrl2/pbes/pbesreach.h"
+#include "mcrl2/pbes/srf_pbes.h"
 #include "mcrl2/pbes/symbolic_pbessolve.h"
 #include "mcrl2/pbes/unify_parameters.h"
 #include "mcrl2/utilities/exception.h"
@@ -191,17 +193,18 @@ class pbesinst_symbolic_counter_example_structure_graph_algorithm: public pbesin
 
           // Add the interleaved data expressions.
           std::size_t i = 1;
-          auto Y_it = Y.parameters().begin();
-          for (auto it = X.parameters().begin(); it != X.parameters().end(); ++it)
+          auto param_Y_it = Y.parameters().begin();
+
+
+          for (auto param_X_it = X.parameters().begin(); param_X_it != X.parameters().end(); ++param_X_it)
           {
-            singleton.emplace_back(data_index[i].index(*it));
-            singleton.emplace_back(data_index[i].index(*Y_it));
+            singleton.emplace_back(data_index[i].index(*param_X_it));
+            singleton.emplace_back(data_index[i].index(*param_Y_it));
 
-            ++Y_it;
+            ++param_Y_it;
             ++i;
           }
-
-
+
           if (sylvan::ldds::member_cube(strategy, singleton))
           {
             // If Y in E0