Started to implement a pbesinst variant that takes a symbolic strategy.

libraries/pbes/include/mcrl2/pbes/detail/pbes_remove_counterexample_info.h

@@ -22,6 +22,7 @@ namespace mcrl2::pbes_system::detail
 
 static std::regex positive("Zpos_(\\d+)_.*");
 static std::regex negative("Zneg_(\\d+)_.*");
+static std::regex positive_or_negative("Z(neg|pos)_(\\d+)_.*");
 
 /// \brief Guesses if a pbes has counter example information
 inline

libraries/pbes/include/mcrl2/pbes/pbesreach.h

@@ -198,6 +198,7 @@ class pbesreach_algorithm
     data::enumerator_algorithm<> m_enumerator;
     data::variable_list m_process_parameters;
     std::size_t m_n;
+    std::unordered_map<core::identifier_string, data::data_expression> m_propvar_map;
     std::vector<symbolic::data_expression_index> m_data_index;
     std::vector<pbes_summand_group> m_summand_groups;
     data::data_expression_list m_initial_state;
@@ -276,10 +277,9 @@ class pbesreach_algorithm
       }
 
       data::basic_sort propvar_sort("PropositionalVariable"); // todo: choose a unique name
-      std::unordered_map<core::identifier_string, data::data_expression> propvar_map;
       for (const auto& equation: m_pbes.equations())
       {
-        propvar_map[equation.variable().name()] = data::function_symbol(equation.variable().name(), propvar_sort);
+        m_propvar_map[equation.variable().name()] = data::function_symbol(equation.variable().name(), propvar_sort);
       }
 
       m_process_parameters = m_pbes.equations().front().variable().parameters();
@@ -288,7 +288,7 @@ class pbesreach_algorithm
 
       // Rewrite the initial expressions to normal form,
       std::vector<data::data_expression> initial_values;
-      for (const data::data_expression& expression : make_state(m_pbes.initial_state(), propvar_map))
+      for (const data::data_expression& expression : make_state(m_pbes.initial_state(), m_propvar_map))
       {
         initial_values.push_back(m_rewr(expression));
       }
@@ -316,7 +316,7 @@ class pbesreach_algorithm
       m_group_patterns = symbolic::compute_summand_group_patterns(m_summand_patterns, groups);
       for (std::size_t j = 0; j < m_group_patterns.size(); j++)
       {
-        m_summand_groups.emplace_back(m_pbes, m_process_parameters, propvar_map, groups[j], m_group_patterns[j], m_summand_patterns, m_variable_order);
+        m_summand_groups.emplace_back(m_pbes, m_process_parameters, m_propvar_map, groups[j], m_group_patterns[j], m_summand_patterns, m_variable_order);
       }
 
       for (std::size_t i = 0; i < m_summand_groups.size(); i++)
@@ -567,6 +567,11 @@ class pbesreach_algorithm
       return m_process_parameters;
     }
 
+    const std::unordered_map<core::identifier_string, data::data_expression>& propvar_map() const
+    {
+      return m_propvar_map;
+    }
+
     const std::vector<symbolic::data_expression_index>& data_index() const
     {
       return m_data_index;

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

@@ -10,6 +10,7 @@
 #ifndef MCRL2_PBES_SYMBOLIC_PBESSOLVE_H
 #define MCRL2_PBES_SYMBOLIC_PBESSOLVE_H
 
+#include "sylvan_ldd.hpp"
 #ifdef MCRL2_ENABLE_SYLVAN
 
 #include "symbolic_parity_game.h"
@@ -89,7 +90,8 @@ class symbolic_pbessolve_algorithm
     /// \brief Solve the given game restricted to V with Zielonka's recursive algorithm as solver.
     ///        The remaining parameters are sinks, vertices won by even and odd respectively.
     ///        Terminates early when initial_vertex has been solved.
-    bool solve(const ldd& initial_vertex,
+    /// \returns The winner and W0, W1, S0, S1. Where S0 and S1 are the strategies.
+    std::tuple<bool, ldd, ldd, ldd, ldd> solve(const ldd& initial_vertex,
         const ldd& V,
         const ldd& Vsinks = sylvan::ldds::empty_set(),
         const ldd& W0 = sylvan::ldds::empty_set(),
@@ -103,12 +105,12 @@ class symbolic_pbessolve_algorithm
       if (includes(winning[0], initial_vertex))
       {
         mCRL2log(log::verbose) << "finished solving (time = " << std::setprecision(2) << std::fixed << timer.seconds() << "s)\n";
-        return true;
+        return std::make_tuple(true, winning[0], winning[1], empty_set(), empty_set());
       }
       else if (includes(winning[1], initial_vertex))
       {
         mCRL2log(log::verbose) << "finished solving (time = " << std::setprecision(2) << std::fixed << timer.seconds() << "s)\n";
-        return false;
+        return std::make_tuple(false, winning[0], winning[1], empty_set(), empty_set());
       }
 
       // If the initial vertex has not yet been won then run the zielonka solver as well.
@@ -119,11 +121,11 @@ class symbolic_pbessolve_algorithm
       mCRL2log(log::trace) << "W1 = " << m_G.print_nodes(solved1) << std::endl;
       if (includes(solved0, initial_vertex))
       {
-        return true;
+        return std::make_tuple(true, solved0, solved1, strategy0, strategy1);
       }
       else if (includes(solved1, initial_vertex))
       {
-        return false;
+        return std::make_tuple(false, solved0, solved1, strategy0, strategy1);
       }
       else
       {