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/tools/lpsbisim2pbes.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_TOOLS_LPSBISIM2PBES_H
      13             : #define MCRL2_PBES_TOOLS_LPSBISIM2PBES_H
      14             : 
      15             : #include "mcrl2/lps/io.h"
      16             : #include "mcrl2/pbes/algorithms.h"
      17             : #include "mcrl2/pbes/bisimulation.h"
      18             : #include "mcrl2/pbes/bisimulation_type.h"
      19             : #include "mcrl2/pbes/io.h"
      20             : 
      21             : namespace mcrl2 {
      22             : 
      23             : namespace pbes_system {
      24             : 
      25           0 : void lpsbisim2pbes(const std::string& input_filename1,
      26             :                    const std::string& input_filename2,
      27             :                    const std::string& output_filename,
      28             :                    const utilities::file_format& output_format,
      29             :                    bisimulation_type type,
      30             :                    bool normalize
      31             :                   )
      32             : {
      33           0 :   lps::specification M;
      34           0 :   lps::specification S;
      35             : 
      36           0 :   load_lps(M, input_filename1);
      37           0 :   load_lps(S, input_filename2);
      38           0 :   pbes result;
      39           0 :   switch (type)
      40             :   {
      41           0 :     case strong_bisim:
      42           0 :       result = strong_bisimulation(M, S);
      43           0 :       break;
      44           0 :     case weak_bisim:
      45           0 :       result = weak_bisimulation(M, S);
      46           0 :       break;
      47           0 :     case branching_bisim:
      48           0 :       result = branching_bisimulation(M, S);
      49           0 :       break;
      50           0 :     case branching_sim:
      51           0 :       result = branching_simulation_equivalence(M, S);
      52           0 :       break;
      53             :   }
      54           0 :   if (normalize)
      55             :   {
      56           0 :     algorithms::normalize(result);
      57             :   }
      58           0 :   save_pbes(result, output_filename, output_format);
      59           0 : }
      60             : 
      61             : } // namespace pbes_system
      62             : 
      63             : } // namespace mcrl2
      64             : 
      65             : #endif // MCRL2_PBES_TOOLS_LPSBISIM2PBES_H