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/stategraph.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_STATEGRAPH_H
      13             : #define MCRL2_PBES_STATEGRAPH_H
      14             : 
      15             : #include "mcrl2/pbes/detail/stategraph_global_reset_variables.h"
      16             : #include "mcrl2/pbes/detail/stategraph_local_reset_variables.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : /// \brief Apply the stategraph algorithm
      23             : /// \param p A PBES to which the algorithm is applied.
      24             : /// \param options The options for the algorithm.
      25             : inline
      26           0 : void stategraph(pbes& p, const pbesstategraph_options& options)
      27             : {
      28           0 :   algorithms::normalize(p);
      29           0 :   if (options.use_global_variant)
      30             :   {
      31           0 :     detail::global_reset_variables_algorithm algorithm(p, options);
      32           0 :     algorithm.run();
      33           0 :     p = algorithm.result();
      34           0 :     if (options.print_influence_graph)
      35             :     {
      36           0 :       detail::stategraph_influence_graph_algorithm ialgo(algorithm.get_pbes());
      37           0 :       ialgo.run();
      38           0 :     }
      39           0 :   }
      40             :   else
      41             :   {
      42           0 :     detail::local_reset_variables_algorithm algorithm(p, options);
      43           0 :     algorithm.run();
      44           0 :     p = algorithm.result();
      45           0 :     if (options.print_influence_graph)
      46             :     {
      47           0 :       detail::stategraph_influence_graph_algorithm ialgo(algorithm.get_pbes());
      48           0 :       ialgo.run();
      49           0 :     }
      50           0 :   }
      51           0 : }
      52             : 
      53             : } // namespace pbes_system
      54             : 
      55             : } // namespace mcrl2
      56             : 
      57             : #endif // MCRL2_PBES_STATEGRAPH_H