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/pbesrewr.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_TOOLS_PBESREWR_H
      13             : #define MCRL2_PBES_TOOLS_PBESREWR_H
      14             : 
      15             : #include "mcrl2/data/detail/one_point_rule_preprocessor.h"
      16             : #include "mcrl2/pbes/detail/bqnf_traverser.h"
      17             : #include "mcrl2/pbes/detail/ppg_rewriter.h"
      18             : #include "mcrl2/pbes/detail/ppg_traverser.h"
      19             : #include "mcrl2/pbes/io.h"
      20             : #include "mcrl2/pbes/normalize.h"
      21             : #include "mcrl2/pbes/pbes_rewriter_type.h"
      22             : #include "mcrl2/pbes/rewrite.h"
      23             : #include "mcrl2/pbes/rewriter.h"
      24             : #include "mcrl2/pbes/rewriters/one_point_rule_rewriter.h"
      25             : #include "mcrl2/pbes/rewriters/quantifiers_inside_rewriter.h"
      26             : 
      27             : namespace mcrl2 {
      28             : 
      29             : namespace pbes_system {
      30             : 
      31           0 : void pbesrewr(const std::string& input_filename,
      32             :               const std::string& output_filename,
      33             :               const utilities::file_format& input_format,
      34             :               const utilities::file_format& output_format,
      35             :               const data::rewrite_strategy rewrite_strategy,
      36             :               pbes_rewriter_type rewriter_type)
      37             : {
      38             :   // load the pbes
      39           0 :   pbes p;
      40           0 :   load_pbes(p, input_filename, input_format);
      41             : 
      42             :   // data rewriter
      43           0 :   data::rewriter datar(p.data(), rewrite_strategy);
      44             : 
      45             :   // pbes rewriter
      46           0 :   switch (rewriter_type)
      47             :   {
      48           0 :     case simplify:
      49             :     {
      50           0 :       simplify_quantifiers_data_rewriter<data::rewriter> pbesr(datar);
      51             :       //simplify_data_rewriter<data::rewriter> pbesr(datar);
      52           0 :       pbes_rewrite(p, pbesr);
      53           0 :       break;
      54             :     }
      55           0 :     case quantifier_all:
      56             :     {
      57           0 :       bool enumerate_infinite_sorts = true;
      58           0 :       enumerate_quantifiers_rewriter pbesr(datar, p.data(), enumerate_infinite_sorts);
      59           0 :       pbes_rewrite(p, pbesr);
      60           0 :       break;
      61           0 :     }
      62           0 :     case quantifier_finite:
      63             :     {
      64           0 :       bool enumerate_infinite_sorts = false;
      65           0 :       enumerate_quantifiers_rewriter pbesr(datar, p.data(), enumerate_infinite_sorts);
      66           0 :       pbes_rewrite(p, pbesr);
      67           0 :       break;
      68           0 :     }
      69           0 :     case quantifier_inside:
      70             :     {
      71             :       quantifiers_inside_rewriter pbesr;
      72           0 :       pbes_rewrite(p, pbesr);
      73           0 :       break;
      74             :     }
      75           0 :     case quantifier_one_point:
      76             :     {
      77             :       // apply the one point rule rewriter
      78             :       one_point_rule_rewriter pbesr;
      79           0 :       bool innermost = false;
      80           0 :       replace_pbes_expressions(p, pbesr, innermost); // use replace, since the one point rule rewriter does the recursion itself
      81             : 
      82             :       // post processing: apply the simplifying rewriter
      83           0 :       simplify_data_rewriter<data::rewriter> simp(datar);
      84           0 :       pbes_rewrite(p, simp);
      85           0 :       break;
      86             :     }
      87           0 :     case pfnf:
      88             :     {
      89             :       pfnf_rewriter pbesr;
      90           0 :       pbes_system::normalize(p);
      91           0 :       pbes_rewrite(p, pbesr);
      92           0 :       break;
      93             :     }
      94           0 :     case ppg:
      95             :     {
      96             :       //bool bqnf = detail::is_bqnf(p);
      97             :       //std::clog << "bqnf_traverser says: p is " << (bqnf ? "" : "NOT ") << "in BQNF." << std::endl;
      98           0 :       bool ppg = detail::is_ppg(p);
      99           0 :       if (ppg)
     100             :       {
     101           0 :         mCRL2log(log::verbose) << "PBES is already a PPG." << std::endl;
     102             :       }
     103             :       else
     104             :       {
     105           0 :         mCRL2log(log::verbose) << "Rewriting..." << std::endl;
     106           0 :         pbes q = detail::to_ppg(p);
     107           0 :         mCRL2log(log::verbose) << "Rewriting done." << std::endl;
     108           0 :         ppg = detail::is_ppg(q);
     109           0 :         if (!ppg)
     110             :         {
     111           0 :           throw(std::runtime_error("The result PBES if not a PPG!"));
     112             :         }
     113           0 :         p = q;
     114           0 :       }
     115           0 :       break;
     116             :     }
     117           0 :     case bqnf_quantifier:
     118             :     {
     119           0 :       bqnf_rewriter pbesr;
     120           0 :       pbes_rewrite(p, pbesr);
     121           0 :       break;
     122           0 :     }
     123           0 :     case prover:
     124             :     default:
     125             :     {
     126             :       // Just ignore.
     127           0 :       assert(false);  // The PBES rewriter cannot be activated through
     128             :       // the commandline. So, we cannot end up here.
     129             :       break;
     130             :     }
     131             :   }
     132           0 :   save_pbes(p, output_filename, output_format);
     133           0 : }
     134             : 
     135             : } // namespace pbes_system
     136             : 
     137             : } // namespace mcrl2
     138             : 
     139             : #endif // MCRL2_PBES_TOOLS_PBESREWR_H