From 9ac173fbf6b5a6df3a388818354f9ca2985f1dd6 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux <2884328+mlaveaux@users.noreply.github.com> Date: Wed, 6 Mar 2024 16:11:28 +0000 Subject: [PATCH] Fixed the namespace of stopwatch. --- libraries/lps/include/mcrl2/lps/lpsreach.h | 2 +- libraries/pbes/include/mcrl2/pbes/pbesreach.h | 4 ++-- .../pbes/include/mcrl2/pbes/symbolic_parity_game.h | 14 +++++++------- .../pbes/include/mcrl2/pbes/symbolic_pbessolve.h | 10 +++++----- .../include/mcrl2/symbolic/symbolic_reachability.h | 2 +- 5 files changed, 16 insertions(+), 16 deletions(-) diff --git a/libraries/lps/include/mcrl2/lps/lpsreach.h b/libraries/lps/include/mcrl2/lps/lpsreach.h index 1b017e935e..36951de92e 100644 --- a/libraries/lps/include/mcrl2/lps/lpsreach.h +++ b/libraries/lps/include/mcrl2/lps/lpsreach.h @@ -281,7 +281,7 @@ class lpsreach_algorithm while (todo != empty_set() && (m_options.max_iterations == 0 || iteration_count < m_options.max_iterations)) { - stopwatch loop_start; + mcrl2::utilities::stopwatch loop_start; iteration_count++; mCRL2log(log::trace) << "--- iteration " << iteration_count << " ---" << std::endl; mCRL2log(log::trace) << "todo = " << print_states(m_lts.data_index, todo) << std::endl; diff --git a/libraries/pbes/include/mcrl2/pbes/pbesreach.h b/libraries/pbes/include/mcrl2/pbes/pbesreach.h index 66e046b8fa..4cab7e443f 100644 --- a/libraries/pbes/include/mcrl2/pbes/pbesreach.h +++ b/libraries/pbes/include/mcrl2/pbes/pbesreach.h @@ -450,7 +450,7 @@ class pbesreach_algorithm mCRL2log(log::trace) << "initial state = " << core::detail::print_list(m_initial_state) << std::endl; - stopwatch timer; + mcrl2::utilities::stopwatch timer; m_initial_vertex = initial_state(); m_visited = empty_set(); m_todo = m_initial_vertex; @@ -458,7 +458,7 @@ class pbesreach_algorithm while (m_todo != empty_set() && !solution_found() && (m_options.max_iterations == 0 || iteration_count < m_options.max_iterations)) { - stopwatch loop_start; + mcrl2::utilities::stopwatch loop_start; iteration_count++; mCRL2log(log::trace) << "--- iteration " << iteration_count << " ---" << std::endl; mCRL2log(log::trace) << "todo = " << print_states(m_data_index, m_todo) << std::endl; diff --git a/libraries/pbes/include/mcrl2/pbes/symbolic_parity_game.h b/libraries/pbes/include/mcrl2/pbes/symbolic_parity_game.h index a184ebcae1..594122b761 100644 --- a/libraries/pbes/include/mcrl2/pbes/symbolic_parity_game.h +++ b/libraries/pbes/include/mcrl2/pbes/symbolic_parity_game.h @@ -322,7 +322,7 @@ class symbolic_parity_game const ldd& I = sylvan::ldds::empty_set(), const ldd& T = sylvan::ldds::empty_set()) const { - stopwatch attractor_watch; + mcrl2::utilities::stopwatch attractor_watch; mCRL2log(log::debug) << "start attractor set computation\n"; using namespace sylvan::ldds; @@ -342,7 +342,7 @@ class symbolic_parity_game mCRL2log(log::trace) << "todo = " << print_nodes(todo) << std::endl; mCRL2log(log::trace) << "Zoutside = " << print_nodes(Zoutside) << std::endl; - stopwatch iter_start; + mcrl2::utilities::stopwatch iter_start; todo = minus(safe_control_predecessors_impl(alpha, todo, Zoutside, Zoutside, V, Vplayer, I), Z); Z = union_(Z, todo); @@ -372,7 +372,7 @@ class symbolic_parity_game { using namespace sylvan::ldds; - stopwatch attractor_watch; + mcrl2::utilities::stopwatch attractor_watch; mCRL2log(log::debug) << "start monotone attractor set computation\n"; using namespace sylvan::ldds; @@ -403,7 +403,7 @@ class symbolic_parity_game mCRL2log(log::trace) << "todo = " << print_nodes(todo) << std::endl; mCRL2log(log::trace) << "Zoutside = " << print_nodes(Zoutside) << std::endl; - stopwatch iter_start; + mcrl2::utilities::stopwatch iter_start; todo = intersect(Vc, minus(safe_control_predecessors_impl(alpha, union_(todo, U), V, minus(Zoutside, U), Vc, Vplayer, I), Z)); Z = union_(Z, todo); @@ -519,7 +519,7 @@ class symbolic_parity_game { const symbolic::summand_group& group = m_summand_groups[i]; - stopwatch watch; + mcrl2::utilities::stopwatch watch; result = union_(result, predecessors(U, V, group)); mCRL2log(log::trace) << "added predecessors for group " << i << " out of " << m_summand_groups.size() << " (time = " << std::setprecision(2) << std::fixed << watch.seconds() << "s)\n"; @@ -566,7 +566,7 @@ class symbolic_parity_game { const symbolic::summand_group& group = m_summand_groups[i]; - stopwatch watch; + mcrl2::utilities::stopwatch watch; ldd todo1 = predecessors(U, todo, group); mCRL2log(log::trace) << "added predecessors for group " << i << " out of " << m_summand_groups.size() << " (time = " << std::setprecision(2) << std::fixed << watch.seconds() << "s)\n"; @@ -598,7 +598,7 @@ class symbolic_parity_game { const symbolic::summand_group& group = m_summand_groups[i]; - stopwatch watch; + mcrl2::utilities::stopwatch watch; Pforced = minus(Pforced, predecessors(Pforced, outside, group)); mCRL2log(log::trace) << "removed 1 - alpha predecessors for group " << i << " out of " << m_summand_groups.size() diff --git a/libraries/pbes/include/mcrl2/pbes/symbolic_pbessolve.h b/libraries/pbes/include/mcrl2/pbes/symbolic_pbessolve.h index 3b64631388..c8091aefd1 100644 --- a/libraries/pbes/include/mcrl2/pbes/symbolic_pbessolve.h +++ b/libraries/pbes/include/mcrl2/pbes/symbolic_pbessolve.h @@ -39,7 +39,7 @@ class symbolic_pbessolve_algorithm return { empty_set(), empty_set() }; } - stopwatch timer; + mcrl2::utilities::stopwatch timer; mCRL2log(log::debug) << "start zielonka recursion\n"; auto [m, U] = m_G.get_min_rank(V); @@ -90,7 +90,7 @@ class symbolic_pbessolve_algorithm const ldd& W1 = sylvan::ldds::empty_set()) { using namespace sylvan::ldds; - stopwatch timer; + mcrl2::utilities::stopwatch timer; std::array winning = { W0, W1 }; ldd Vtotal = m_G.compute_total_graph(V, empty_set(), Vsinks, winning); @@ -207,7 +207,7 @@ class symbolic_pbessolve_algorithm std::size_t iter = 0; while (U != Unext) { - stopwatch timer; + mcrl2::utilities::stopwatch timer; U = Unext; Unext = m_G.predecessors(U, U); @@ -287,7 +287,7 @@ class symbolic_pbessolve_algorithm std::size_t iter = 0; while (U != Unext) { - stopwatch timer; + mcrl2::utilities::stopwatch timer; U = Unext; if (safe_variant) { @@ -331,7 +331,7 @@ class symbolic_pbessolve_algorithm const ldd& W1 = sylvan::ldds::empty_set()) { using namespace sylvan::ldds; - stopwatch timer; + mcrl2::utilities::stopwatch timer; std::array winning = { W0, W1 }; ldd Vtotal = m_G.compute_total_graph(V, I, Vsinks, winning); diff --git a/libraries/symbolic/include/mcrl2/symbolic/symbolic_reachability.h b/libraries/symbolic/include/mcrl2/symbolic/symbolic_reachability.h index f58c40a39c..d245bfb267 100644 --- a/libraries/symbolic/include/mcrl2/symbolic/symbolic_reachability.h +++ b/libraries/symbolic/include/mcrl2/symbolic/symbolic_reachability.h @@ -137,7 +137,7 @@ void learn_successors_callback(WorkerP*, Task*, std::uint32_t* x, std::size_t, v // add the assignments corresponding to x to sigma // add x to the transition xy - stopwatch learn_start; + mcrl2::utilities::stopwatch learn_start; for (std::size_t j = 0; j < x_size; j++) { sigma[group.read_parameters[j]] = data_index[group.read[j]][x[j]];