Line data Source code
1 : // Author(s): Wieger Wesselink 2 : // Copyright: see the accompanying file COPYING or copy at 3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING 4 : // 5 : // Distributed under the Boost Software License, Version 1.0. 6 : // (See accompanying file LICENSE_1_0.txt or copy at 7 : // http://www.boost.org/LICENSE_1_0.txt) 8 : // 9 : /// \file mcrl2/pbes/detail/pbessolve.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_DETAIL_PBESSOLVE_H 13 : #define MCRL2_PBES_DETAIL_PBESSOLVE_H 14 : 15 : #include "mcrl2/lps/detail/instantiate_global_variables.h" 16 : #include "mcrl2/pbes/pbesinst_structure_graph.h" 17 : #include "mcrl2/pbes/solve_structure_graph.h" 18 : 19 : namespace mcrl2 { 20 : 21 : namespace pbes_system { 22 : 23 : namespace detail { 24 : 25 133 : bool pbessolve(const pbes& p) 26 : { 27 133 : pbessolve_options options; 28 133 : pbes pbesspec = p; 29 133 : pbes_system::algorithms::normalize(pbesspec); 30 133 : structure_graph G; 31 133 : pbesinst_structure_graph_algorithm algorithm(options, pbesspec, G); 32 133 : algorithm.run(); 33 266 : return solve_structure_graph(G); 34 133 : } 35 : 36 : } // namespace detail 37 : 38 : } // namespace pbes_system 39 : 40 : } // namespace mcrl2 41 : 42 : #endif // MCRL2_PBES_DETAIL_PBESSOLVE_H