Resolve compilation errors on other platforms.

mCRL2org · Jul 18, 2023 · 1fef051 · 1fef051
1 parent 5712350
commit 1fef051
Show file tree

Hide file tree

Showing 9 changed files with 34 additions and 21 deletions.
diff --git a/benchmarks/CMakeLists.txt b/benchmarks/CMakeLists.txt
@@ -15,7 +15,10 @@ function(add_tool_benchmark NAME TOOL INPUT OUTPUT)
   )
 
   add_test(NAME ${TEST} 
-    COMMAND ${CMAKE_COMMAND} "--build" ${CMAKE_BINARY_DIR} "--target" "${TARGET}")
+    COMMAND ${CMAKE_COMMAND} 
+      "--build" ${CMAKE_BINARY_DIR} 
+      "--target" "${TARGET}")
+
   set_property(TEST ${TEST} PROPERTY LABELS "benchmark_tool")
 endfunction()
 
@@ -137,5 +140,15 @@ if (MCRL2_ENABLE_DEVELOPER)
       "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.dataspec" 
       "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.expressions" 
       "-rjitty")
+
+     add_tool_benchmark("${NAME}_jittyc" mcrl2rewrite 
+      "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.dataspec" 
+      "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.expressions" 
+      "-rjittyc")
+
+     add_tool_benchmark("${NAME}_innermost" mcrl2rewrite 
+      "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.dataspec" 
+      "${CMAKE_CURRENT_SOURCE_DIR}/REC/${NAME}.expressions" 
+      "-rinnermost")
   endforeach()
 endif()
diff --git a/libraries/atermpp/include/mcrl2/atermpp/detail/aterm_configuration.h b/libraries/atermpp/include/mcrl2/atermpp/detail/aterm_configuration.h
@@ -24,7 +24,7 @@ constexpr static bool EnableGarbageCollection = true;
 constexpr static bool EnableBlockAllocator = false;
 
 /// \brief Enable to print garbage collection statistics.
-constexpr static bool EnableGarbageCollectionMetrics = true;
+constexpr static bool EnableGarbageCollectionMetrics = false;
 
 /// Performs garbage collection intensively for testing purposes.
 constexpr static bool EnableAggressiveGarbageCollection = false;

diff --git a/libraries/data/include/mcrl2/data/detail/rewrite/innermost.h b/libraries/data/include/mcrl2/data/detail/rewrite/innermost.h
@@ -43,7 +43,7 @@ class InnermostRewriter final : public Rewriter
 
   rewrite_strategy getStrategy() override { return innermost; }
 
-  std::shared_ptr<detail::Rewriter> clone()
+  std::shared_ptr<detail::Rewriter> clone() override
   {
     return std::shared_ptr<Rewriter>(new InnermostRewriter(*this));
   }

diff --git 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::debug1) << "--- iteration " << iteration_count << " ---" << std::endl;
         mCRL2log(log::debug1) << "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
@@ -450,15 +450,15 @@ class pbesreach_algorithm
 
       mCRL2log(log::debug1) << "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;
       m_deadlocks = empty_set();
 
       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::debug1) << "--- iteration " << iteration_count << " ---" << std::endl;
         mCRL2log(log::debug1) << "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
@@ -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::debug1) << "todo = " << print_nodes(todo) << std::endl;
         mCRL2log(log::debug1) << "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::debug1) << "todo = " << print_nodes(todo) << std::endl;
         mCRL2log(log::debug1) << "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::debug1) << "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::debug1) << "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::debug1) << "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
@@ -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<ldd, 2> 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<ldd, 2> 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
@@ -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]];

diff --git a/tools/release/pbessolvesymbolic/pbessolvesymbolic.cpp b/tools/release/pbessolvesymbolic/pbessolvesymbolic.cpp
@@ -48,7 +48,7 @@ class pbesreach_algorithm_partial : public pbes_system::pbesreach_algorithm
     if (time_solving * 10 < (time_solving + time_exploring) || m_options.aggressive)
     {
       mCRL2log(log::verbose) << "start partial solving\n";
-      stopwatch timer;
+      mcrl2::utilities::stopwatch timer;
 
       // Store the set of won states to keep track of whether new states have been solved.
       std::array<sylvan::ldds::ldd, 2> Vwon = m_Vwon;
@@ -127,7 +127,7 @@ class pbesreach_algorithm_partial : public pbes_system::pbesreach_algorithm
 
   double time_solving = 0.0;
   double time_exploring = 0.0;
-  stopwatch explore_timer;
+  mcrl2::utilities::stopwatch explore_timer;
 };
 
 } // namespace mcrl2::pbes_system