From 1c9107e7905dc3fe32aa03a2869314a2a8fb8319 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 5 Jun 2024 16:18:30 +0200 Subject: [PATCH] Introduce a mapping from propositional variables to their vertices in the proof graph. --- .../pbes/include/mcrl2/pbes/pbesinst_lazy.h | 67 ++++++++++--------- .../mcrl2/pbes/pbesinst_structure_graph.h | 2 +- .../mcrl2/pbes/pbesinst_structure_graph2.h | 4 +- .../mcrl2/pbes/solve_structure_graph.h | 12 +++- .../pbes/include/mcrl2/pbes/tools/pbessolve.h | 2 +- 5 files changed, 48 insertions(+), 39 deletions(-) diff --git a/libraries/pbes/include/mcrl2/pbes/pbesinst_lazy.h b/libraries/pbes/include/mcrl2/pbes/pbesinst_lazy.h index bdb67b6548..bd05bbdb3c 100644 --- a/libraries/pbes/include/mcrl2/pbes/pbesinst_lazy.h +++ b/libraries/pbes/include/mcrl2/pbes/pbesinst_lazy.h @@ -23,6 +23,7 @@ #include "mcrl2/pbes/detail/bes_equation_limit.h" #include "mcrl2/pbes/detail/instantiate_global_variables.h" #include "mcrl2/pbes/pbes_equation_index.h" +#include "mcrl2/pbes/pbes_expression.h" #include "mcrl2/pbes/pbessolve_options.h" #include "mcrl2/pbes/remove_equations.h" #include "mcrl2/pbes/replace_constants_by_variables.h" @@ -277,7 +278,7 @@ class pbesinst_lazy_algorithm static void rewrite_star(pbes_expression& result, const structure_graph& G, bool alpha, - const std::set& W, + const std::unordered_map& W, const fixpoint_symbol& symbol, const propositional_variable_instantiation& X, const pbes_expression& psi) @@ -292,43 +293,43 @@ class pbesinst_lazy_algorithm std::set Ys; // If X is won by player alpha, i.e. in the winning set W. - for (const auto& index : W) + auto it = W.find(X); + if (it != W.end()) { - if (G.find_vertex(index).formula() == X) - { - // We know that X itself (if it can be reached by a self loop) is in W - // (the initial vertex is in W and every reachable one). - Ys.insert(X); + structure_graph::index_type index = it->second; - std::set todo = { index }; - std::set done; + // We know that X itself (if it can be reached by a self loop) is in W + // (the initial vertex is in W and every reachable one). + Ys.insert(X); - while (!todo.empty()) - { - structure_graph::index_type u = *todo.begin(); - todo.erase(todo.begin()); - done.insert(u); + std::set todo = { index }; + std::set done; - // Explore all outgoing edges. - for (structure_graph::index_type v: G.all_successors(u)) + while (!todo.empty()) + { + structure_graph::index_type u = *todo.begin(); + todo.erase(todo.begin()); + done.insert(u); + + // Explore all outgoing edges. + for (structure_graph::index_type v: G.all_successors(u)) + { + if (!mcrl2::utilities::detail::contains(done, v)) { - if (!mcrl2::utilities::detail::contains(done, v)) + if (G.rank(v) == undefined_vertex()) { - if (G.rank(v) == undefined_vertex()) - { - // explore all outgoing edges that are unranked - todo.insert(v); - } - else if (mcrl2::utilities::detail::contains(W, v)) - { - // Insert the outgoing edge, but do not add it to the todo set to stop exploring this vertex. - Ys.insert(G.find_vertex(v).formula()); - } + // explore all outgoing edges that are unranked + todo.insert(v); + } + else if (W.count(G.find_vertex(v).formula()) != 0) + { + // Insert the outgoing edge, but do not add it to the todo set to stop exploring this vertex. + Ys.insert(G.find_vertex(v).formula()); } } - - break; } + + break; } } @@ -454,8 +455,8 @@ class pbesinst_lazy_algorithm // rewrite the right hand side of the equation X = psi virtual void rewrite_psi(const std::size_t /* thread_index */, - std::optional&>> proof_graph, pbes_expression& result, + std::optional&>> proof_graph, const fixpoint_symbol& symbol, const propositional_variable_instantiation& X, const pbes_expression& psi @@ -482,7 +483,7 @@ class pbesinst_lazy_algorithm } virtual void run_thread(const std::size_t thread_index, - std::optional&>> proof_graph, + std::optional&>> proof_graph, pbesinst_lazy_todo& todo, std::atomic& number_of_active_processes, data::mutable_indexed_substitution<> sigma, @@ -519,7 +520,7 @@ class pbesinst_lazy_algorithm // optional step m_todo_access.lock(); - rewrite_psi(thread_index, proof_graph, psi_e, eqn.symbol(), X_e, psi_e); + rewrite_psi(thread_index, psi_e, proof_graph, eqn.symbol(), X_e, psi_e); m_todo_access.unlock(); std::set occ = find_propositional_variable_instantiations(psi_e); @@ -560,7 +561,7 @@ class pbesinst_lazy_algorithm } /// \brief Runs the algorithm. The result is obtained by calling the function \p get_result. - virtual void run(std::optional&>> proof_graph) + virtual void run(std::optional&>> proof_graph) { m_iteration_count = 0; diff --git a/libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph.h b/libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph.h index 5e0f0927d0..e10dfd4f72 100644 --- a/libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph.h +++ b/libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph.h @@ -134,7 +134,7 @@ class pbesinst_structure_graph_algorithm: public pbesinst_lazy_algorithm SG0(X, psi, k); } - void run(std::optional&>> proof_graph = std::nullopt) override + void run(std::optional&>> proof_graph = std::nullopt) override { pbesinst_lazy_algorithm::run(proof_graph); m_graph_builder.finalize(); diff --git a/libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph2.h b/libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph2.h index ead2f9086e..f680bcc1b2 100644 --- a/libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph2.h +++ b/libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph2.h @@ -512,14 +512,14 @@ class pbesinst_structure_graph_algorithm2: public pbesinst_structure_graph_algor // Optimization 2 is implemented by overriding the function rewrite_psi. void rewrite_psi(const std::size_t thread_index, - std::optional&>> proof_graph, pbes_expression& result, + std::optional&>> proof_graph, const fixpoint_symbol& symbol, const propositional_variable_instantiation& X, const pbes_expression& psi ) override { - super::rewrite_psi(thread_index, proof_graph, result, symbol, X, psi); + super::rewrite_psi(thread_index, result, proof_graph, symbol, X, psi); auto rplus_result = Rplus(result); b[thread_index] = rplus_result.b; if (is_true(rplus_result.b)) diff --git a/libraries/pbes/include/mcrl2/pbes/solve_structure_graph.h b/libraries/pbes/include/mcrl2/pbes/solve_structure_graph.h index c60d1ec829..cba495e47a 100644 --- a/libraries/pbes/include/mcrl2/pbes/solve_structure_graph.h +++ b/libraries/pbes/include/mcrl2/pbes/solve_structure_graph.h @@ -595,7 +595,7 @@ bool solve_structure_graph(structure_graph& G, bool check_strategy = false) } inline -std::pair> solve_structure_graph_minimal_winning_set(structure_graph& G, bool check_strategy = false) +std::pair> solve_structure_graph_minimal_winning_set(structure_graph& G, bool check_strategy = false) { bool use_toms_optimization = !check_strategy; solve_structure_graph_algorithm algorithm(check_strategy, use_toms_optimization); @@ -616,6 +616,7 @@ std::pair> solve_structure_graph_min // Sorting is necessary for the set intersection computed below. auto& W_alpha = is_disjunctive ? W.first : W.second; W_alpha.sort(); + std::set W_minimal; std::set_intersection(minimal_set.begin(), minimal_set.end(), W_alpha.vertices().begin(), W_alpha.vertices().end(), std::inserter(W_minimal, W_minimal.begin())); mCRL2log(log::debug) << "\nExtracted minimal set W " << core::detail::print_set(W_minimal) << std::endl; @@ -623,7 +624,14 @@ std::pair> solve_structure_graph_min mCRL2log(log::debug) << std::setw(4) << index << " " << G.find_vertex(index) << std::endl; } - return { is_disjunctive, W_minimal }; + // Make a mapping from the formula to the index it belongs to. + std::unordered_map mapping; + + for (structure_graph::index_type index : W_alpha.vertices()) { + mapping.insert(std::make_pair(G.find_vertex(index).formula(), index)); + } + + return { is_disjunctive, mapping }; } inline diff --git a/libraries/pbes/include/mcrl2/pbes/tools/pbessolve.h b/libraries/pbes/include/mcrl2/pbes/tools/pbessolve.h index 6d1fa2be3a..57b3796d9c 100644 --- a/libraries/pbes/include/mcrl2/pbes/tools/pbessolve.h +++ b/libraries/pbes/include/mcrl2/pbes/tools/pbessolve.h @@ -358,7 +358,7 @@ class pbessolve_tool // Perform the second instantiation given the proof graph. timer().start("second-instantiation"); - second_instantiate.run(std::make_optional(std::tuple&>(initial_G, !result, W_alpha))); + second_instantiate.run(std::make_optional(std::tuple&>(initial_G, !result, W_alpha))); timer().finish("second-instantiation"); mCRL2log(log::verbose) << "Number of vertices in the structure graph: "