Fixed compilation errors, and replaced boost::optional by std::optional.

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

@@ -15,6 +15,7 @@
 #include "mcrl2/lps/detail/instantiate_global_variables.h"
 #include "mcrl2/pbes/pbesinst_structure_graph.h"
 #include "mcrl2/pbes/solve_structure_graph.h"
+#include <optional>
 
 namespace mcrl2 {
 
@@ -30,7 +31,7 @@ bool pbessolve(const pbes& p)
   structure_graph G;
   pbesinst_structure_graph_algorithm algorithm(options, pbesspec, G);
   algorithm.run();
-  return solve_structure_graph(G);
+  return solve_structure_graph(G).first;
 }
 
 } // namespace detail

libraries/pbes/include/mcrl2/pbes/pbesinst_lazy.h

@@ -9,8 +9,13 @@
 /// \file mcrl2/pbes/pbesinst_lazy_algorithm.h
 /// \brief A lazy algorithm for instantiating a PBES, ported from bes_deprecated.h.
 
+#ifndef MCRL2_PBES_PBESINST_LAZY_H
+#define MCRL2_PBES_PBESINST_LAZY_H
+
 #include <thread>
 #include <mutex>
+#include <functional>
+#include <regex>
 
 #include "mcrl2/atermpp/standard_containers/deque.h"
 #include "mcrl2/atermpp/standard_containers/indexed_set.h"
@@ -24,12 +29,11 @@
 #include "mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h"
 #include "mcrl2/pbes/rewriters/one_point_rule_rewriter.h"
 #include "mcrl2/pbes/rewriters/simplify_quantifiers_rewriter.h"
+#include "mcrl2/pbes/structure_graph.h"
 #include "mcrl2/pbes/transformation_strategy.h"
 #include "mcrl2/pbes/transformations.h"
 #include "mcrl2/utilities/detail/container_utility.h"
 
-#ifndef MCRL2_PBES_PBESINST_LAZY_H
-#define MCRL2_PBES_PBESINST_LAZY_H
 
 namespace mcrl2
 {
@@ -443,7 +447,7 @@ class pbesinst_lazy_algorithm
 
     // rewrite the right hand side of the equation X = psi
     virtual void rewrite_psi(const std::size_t /* thread_index */,
-                             boost::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::set<structure_graph::index_type>&>> proof_graph,
                              pbes_expression& result,
                              const fixpoint_symbol& symbol,
                              const propositional_variable_instantiation& X,
@@ -471,7 +475,7 @@ class pbesinst_lazy_algorithm
     }
 
     virtual void run_thread(const std::size_t thread_index,
-                            boost::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::set<structure_graph::index_type>&>> proof_graph,
                             pbesinst_lazy_todo& todo,
                             std::atomic<std::size_t>& number_of_active_processes,
                             data::mutable_indexed_substitution<> sigma,
@@ -549,7 +553,7 @@ class pbesinst_lazy_algorithm
     }
 
     /// \brief Runs the algorithm. The result is obtained by calling the function \p get_result.
-    virtual void run(boost::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::set<structure_graph::index_type>&>> proof_graph)
     {
       m_iteration_count = 0;
 

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(boost::optional<std::tuple<const structure_graph&, bool, const std::set<structure_graph::index_type>&>> proof_graph) override
+    void run(std::optional<std::tuple<const structure_graph&, bool, const std::set<structure_graph::index_type>&>> proof_graph = std::nullopt) override
     {
       pbesinst_lazy_algorithm::run(proof_graph);
       m_graph_builder.finalize();

libraries/pbes/include/mcrl2/pbes/pbesinst_structure_graph2.h

@@ -512,7 +512,7 @@ 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,
-                     boost::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::set<structure_graph::index_type>&>> proof_graph,
                      pbes_expression& result,
                      const fixpoint_symbol& symbol,
                      const propositional_variable_instantiation& X,

libraries/pbes/include/mcrl2/pbes/tools/pbessolve.h

@@ -314,7 +314,7 @@ class pbessolve_tool
       PbesInstAlgorithm instantiate(options, pbesspec, G);
 
       timer().start("instantiation");
-      instantiate.run(boost::none);
+      instantiate.run();
       timer().finish("instantiation");
 
       run_solve(pbesspec, sigma, G, instantiate.equation_index());
@@ -336,7 +336,7 @@ class pbessolve_tool
       PbesInstAlgorithm first_instantiate(options, pbesspec_without_counterexample, initial_G);
 
       timer().start("first-instantiation");
-      first_instantiate.run(boost::none);
+      first_instantiate.run();
       timer().finish("first-instantiation");
 
       mCRL2log(log::verbose) << "Number of vertices in the structure graph: "
@@ -358,7 +358,7 @@ class pbessolve_tool
 
       // Perform the second instantiation given the proof graph.      
       timer().start("second-instantiation");
-      second_instantiate.run(boost::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::set<structure_graph::index_type>&>(initial_G, !result, W_alpha)));
       timer().finish("second-instantiation");
 
       mCRL2log(log::verbose) << "Number of vertices in the structure graph: "