Skip to content

Commit

Permalink
Introduce a mapping from propositional variables to their vertices in…
Browse files Browse the repository at this point in the history 
… the proof graph.
  • Loading branch information
@mlaveaux
mlaveaux committed Jun 5, 2024
1 parent 5b7c017 commit 1c9107e
Show file tree
Hide file tree
Showing 5 changed files with 48 additions and 39 deletions.
67 changes: 34 additions & 33 deletions libraries/pbes/include/mcrl2/pbes/pbesinst_lazy.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -277,7 +278,7 @@ class pbesinst_lazy_algorithm
static void rewrite_star(pbes_expression& result,
const structure_graph& G,
bool alpha,
const std::set<structure_graph::index_type>& W,
const std::unordered_map<pbes_expression, structure_graph::index_type>& W,
const fixpoint_symbol& symbol,
const propositional_variable_instantiation& X,
const pbes_expression& psi)
Expand All @@ -292,43 +293,43 @@ class pbesinst_lazy_algorithm
std::set<pbes_expression> 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<structure_graph::index_type> todo = { index };
std::set<structure_graph::index_type> 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<structure_graph::index_type> todo = { index };
std::set<structure_graph::index_type> 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;
}
}

Expand Down Expand Up @@ -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<std::tuple<const structure_graph&, bool, const std::set<structure_graph::index_type>&>> proof_graph,
pbes_expression& result,
std::optional<std::tuple<const structure_graph&, bool, const std::unordered_map<pbes_expression, structure_graph::index_type>&>> proof_graph,
const fixpoint_symbol& symbol,
const propositional_variable_instantiation& X,
const pbes_expression& psi
Expand All @@ -482,7 +483,7 @@ class pbesinst_lazy_algorithm
}

virtual void run_thread(const std::size_t thread_index,
std::optional<std::tuple<const structure_graph&, bool, const std::set<structure_graph::index_type>&>> proof_graph,
std::optional<std::tuple<const structure_graph&, bool, const std::unordered_map<pbes_expression, structure_graph::index_type>&>> proof_graph,
pbesinst_lazy_todo& todo,
std::atomic<std::size_t>& number_of_active_processes,
data::mutable_indexed_substitution<> sigma,
Expand Down Expand Up @@ -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<propositional_variable_instantiation> occ = find_propositional_variable_instantiations(psi_e);
Expand Down Expand Up @@ -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<std::tuple<const structure_graph&, bool, const std::set<structure_graph::index_type>&>> proof_graph)
virtual void run(std::optional<std::tuple<const structure_graph&, bool, const std::unordered_map<pbes_expression, structure_graph::index_type>&>> proof_graph)
{
m_iteration_count = 0;

Expand Down
2 changes: 1 addition & 1 deletion libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ class pbesinst_structure_graph_algorithm: public pbesinst_lazy_algorithm
SG0(X, psi, k);
}

void run(std::optional<std::tuple<const structure_graph&, bool, const std::set<structure_graph::index_type>&>> proof_graph = std::nullopt) override
void run(std::optional<std::tuple<const structure_graph&, bool, const std::unordered_map<pbes_expression, structure_graph::index_type>&>> proof_graph = std::nullopt) override
{
pbesinst_lazy_algorithm::run(proof_graph);
m_graph_builder.finalize();
Expand Down
4 changes: 2 additions & 2 deletions libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph2.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<std::tuple<const structure_graph&, bool, const std::set<structure_graph::index_type>&>> proof_graph,
pbes_expression& result,
std::optional<std::tuple<const structure_graph&, bool, const std::unordered_map<pbes_expression, structure_graph::index_type>&>> 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))
Expand Down
12 changes: 10 additions & 2 deletions libraries/pbes/include/mcrl2/pbes/solve_structure_graph.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -595,7 +595,7 @@ bool solve_structure_graph(structure_graph& G, bool check_strategy = false)
}

inline
std::pair<bool, std::set<structure_graph::index_type>> solve_structure_graph_minimal_winning_set(structure_graph& G, bool check_strategy = false)
std::pair<bool, std::unordered_map<pbes_expression, structure_graph::index_type>> 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);
Expand All @@ -616,14 +616,22 @@ std::pair<bool, std::set<structure_graph::index_type>> 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<structure_graph::index_type> 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;
for (const auto& index : W_minimal) {
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<pbes_expression, structure_graph::index_type> 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
Expand Down
2 changes: 1 addition & 1 deletion libraries/pbes/include/mcrl2/pbes/tools/pbessolve.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<const structure_graph&, bool, const std::set<structure_graph::index_type>&>(initial_G, !result, W_alpha)));
second_instantiate.run(std::make_optional(std::tuple<const structure_graph&, bool, const std::unordered_map<pbes_expression, structure_graph::index_type>&>(initial_G, !result, W_alpha)));
timer().finish("second-instantiation");

mCRL2log(log::verbose) << "Number of vertices in the structure graph: "
Expand Down

0 comments on commit 1c9107e

Please sign in to comment.