LCOV - code coverage report
Current view: top level - lps/source - tools.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 1 128 0.8 %
Date: 2020-02-28 00:44:21 Functions: 2 13 15.4 %
Legend: Lines: hit not hit

          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 tools.cpp
      10             : 
      11             : #include "mcrl2/lps/binary.h"
      12             : #include "mcrl2/lps/constelm.h"
      13             : #include "mcrl2/lps/detail/specification_property_map.h"
      14             : #include "mcrl2/lps/invelm_algorithm.h"
      15             : #include "mcrl2/lps/io.h"
      16             : #include "mcrl2/lps/parelm.h"
      17             : #include "mcrl2/lps/parse.h"
      18             : #include "mcrl2/lps/sumelm.h"
      19             : #include "mcrl2/lps/suminst.h"
      20             : #include "mcrl2/lps/tools.h"
      21             : #include "mcrl2/lps/untime.h"
      22             : #include "mcrl2/lps/one_point_rule_rewrite.h"
      23             : 
      24             : namespace mcrl2
      25             : {
      26             : 
      27             : namespace lps
      28             : {
      29             : 
      30           0 : void lpsbinary(const std::string& input_filename,
      31             :                const std::string& output_filename)
      32             : {
      33           0 :   lps::stochastic_specification spec;
      34           0 :   load_lps(spec, input_filename);
      35           0 :   data::rewriter r(spec.data());
      36             : 
      37           0 :   lps::binary_algorithm<data::rewriter, stochastic_specification>(spec, r).run();
      38           0 :   save_lps(spec, output_filename);
      39           0 : }
      40             : 
      41           0 : void lpsconstelm(const std::string& input_filename,
      42             :                  const std::string& output_filename,
      43             :                  data::rewriter::strategy rewrite_strategy,
      44             :                  bool instantiate_free_variables,
      45             :                  bool ignore_conditions,
      46             :                  bool remove_trivial_summands,
      47             :                  bool remove_singleton_sorts
      48             :                 )
      49             : {
      50           0 :   lps::stochastic_specification spec;
      51           0 :   load_lps(spec, input_filename);
      52           0 :   mcrl2::data::rewriter R(spec.data(), rewrite_strategy);
      53           0 :   lps::constelm_algorithm<data::rewriter, stochastic_specification> algorithm(spec, R);
      54             : 
      55             :   // preprocess: remove single element sorts
      56           0 :   if (remove_singleton_sorts)
      57             :   {
      58           0 :     algorithm.remove_singleton_sorts();
      59             :   }
      60             : 
      61             :   // apply constelm
      62           0 :   algorithm.run(instantiate_free_variables, ignore_conditions);
      63             : 
      64             :   // postprocess: remove trivial summands
      65           0 :   if (remove_trivial_summands)
      66             :   {
      67           0 :     algorithm.remove_trivial_summands();
      68             :   }
      69             : 
      70           0 :   save_lps(spec, output_filename);
      71           0 : }
      72             : 
      73           0 : void lpsinfo(const std::string& input_filename,
      74             :              const std::string& input_file_message
      75             :             )
      76             : {
      77           0 :   stochastic_specification spec;
      78           0 :   load_lps(spec, input_filename);
      79           0 :   lps::detail::specification_property_map<stochastic_specification> info(spec);
      80           0 :   std::cout << input_file_message << "\n\n";
      81           0 :   std::cout << info.info();
      82           0 : }
      83             : 
      84           0 : bool lpsinvelm(const std::string& input_filename,
      85             :                const std::string& output_filename,
      86             :                const std::string& invariant_filename,
      87             :                const std::string& dot_file_name,
      88             :                data::rewriter::strategy rewrite_strategy,
      89             :                data::detail::smt_solver_type solver_type,
      90             :                const bool no_check,
      91             :                const bool no_elimination,
      92             :                const bool simplify_all,
      93             :                const bool all_violations,
      94             :                const bool counter_example,
      95             :                const bool path_eliminator,
      96             :                const bool apply_induction,
      97             :                const int time_limit)
      98             : {
      99           0 :   stochastic_specification spec;
     100           0 :   data::data_expression invariant;
     101             : 
     102           0 :   load_lps(spec, input_filename);
     103             : 
     104           0 :   if (!invariant_filename.empty())
     105             :   {
     106           0 :     std::ifstream instream(invariant_filename.c_str());
     107             : 
     108           0 :     if (!instream.is_open())
     109             :     {
     110           0 :       throw mcrl2::runtime_error("cannot open input file '" + invariant_filename + "'");
     111             :     }
     112             : 
     113           0 :     mCRL2log(log::verbose) << "parsing input file '" <<  invariant_filename << "'..." << std::endl;
     114             : 
     115           0 :     data::variable_list& parameters=spec.process().process_parameters();
     116           0 :     invariant = data::parse_data_expression(instream, parameters, spec.data());
     117             : 
     118           0 :     instream.close();
     119             :   }
     120             :   else
     121             :   {
     122           0 :     throw mcrl2::runtime_error("A file containing an invariant must be specified using the option --invariant=INVFILE.");
     123             :   }
     124             : 
     125           0 :   if (no_check)
     126             :   {
     127           0 :     mCRL2log(log::warning) << "The invariant is not checked; it may not hold for this LPS." << std::endl;
     128             :   }
     129             :   else
     130             :   {
     131             :     detail::Invariant_Checker<stochastic_specification> v_invariant_checker(spec,
     132             :                                           rewrite_strategy,
     133             :                                           time_limit,
     134             :                                           path_eliminator,
     135             :                                           solver_type,
     136             :                                           apply_induction,
     137             :                                           counter_example,
     138             :                                           all_violations,
     139           0 :                                           dot_file_name);
     140             : 
     141           0 :     if (!v_invariant_checker.check_invariant(invariant))
     142             :     {
     143           0 :       return false; // The invariant was checked and found invalid.
     144             :     }
     145             :   }
     146             : 
     147             :   invelm_algorithm<stochastic_specification> algorithm(spec,
     148             :                                rewrite_strategy,
     149             :                                time_limit,
     150             :                                path_eliminator,
     151             :                                solver_type,
     152             :                                apply_induction,
     153           0 :                                simplify_all);
     154           0 :   algorithm.run(invariant, !no_elimination);
     155           0 :   save_lps(spec, output_filename);
     156           0 :   return true;
     157             : }
     158             : 
     159           0 : void lpsparelm(const std::string& input_filename,
     160             :                const std::string& output_filename
     161             :               )
     162             : {
     163           0 :   lps::stochastic_specification spec;
     164           0 :   load_lps(spec, input_filename);
     165           0 :   lps::parelm(spec, true);
     166           0 :   save_lps(spec, output_filename);
     167           0 : }
     168             : 
     169           0 : void lpspp(const std::string& input_filename,
     170             :            const std::string& output_filename,
     171             :            bool print_summand_numbers,
     172             :            core::print_format_type format
     173             :           )
     174             : {
     175           0 :   lps::stochastic_specification spec;
     176           0 :   load_lps(spec, input_filename);
     177             : 
     178           0 :   mCRL2log(log::verbose) << "printing LPS from "
     179           0 :                     << (input_filename.empty()?"standard input":input_filename)
     180           0 :                     << " to " << (output_filename.empty()?"standard output":output_filename)
     181           0 :                     << " in the " << core::pp_format_to_string(format) << " format" << std::endl;
     182             : 
     183           0 :   std::string text;
     184           0 :   if (format == core::print_internal)
     185             :   {
     186           0 :     text = pp(specification_to_aterm(spec));
     187             :   }
     188             :   else
     189             :   {
     190           0 :     text = print_summand_numbers ? lps::pp_with_summand_numbers(spec) : lps::pp(spec);
     191             :   }
     192           0 :   if (output_filename.empty())
     193             :   {
     194           0 :     std::cout << text;
     195             :   }
     196             :   else
     197             :   {
     198           0 :     std::ofstream output_stream(output_filename.c_str());
     199           0 :     if (output_stream)
     200             :     {
     201           0 :       output_stream << text;
     202           0 :       output_stream.close();
     203             :     }
     204             :     else
     205             :     {
     206           0 :       throw mcrl2::runtime_error("could not open output file " + output_filename + " for writing");
     207             :     }
     208             :   }
     209           0 : }
     210             : 
     211           0 : void lpsrewr(const std::string& input_filename,
     212             :              const std::string& output_filename,
     213             :              const data::rewriter::strategy rewrite_strategy,
     214             :              const lps_rewriter_type rewriter_type
     215             :             )
     216             : {
     217           0 :   stochastic_specification spec;
     218           0 :   load_lps(spec, input_filename);
     219           0 :   switch (rewriter_type)
     220             :   {
     221           0 :     case simplify:
     222             :     {
     223           0 :       mcrl2::data::rewriter R(spec.data(), rewrite_strategy);
     224           0 :       lps::rewrite(spec, R);
     225           0 :       break;
     226             :     }
     227           0 :     case quantifier_one_point:
     228             :     {
     229           0 :       one_point_rule_rewrite(spec);
     230           0 :       break;
     231             :     }
     232             :   }
     233           0 :   lps::remove_trivial_summands(spec);
     234           0 :   lps::remove_redundant_assignments(spec);
     235           0 :   save_lps(spec, output_filename);
     236           0 : }
     237             : 
     238           0 : void lpssumelm(const std::string& input_filename,
     239             :                const std::string& output_filename,
     240             :                const bool decluster)
     241             : {
     242           0 :   stochastic_specification spec;
     243           0 :   load_lps(spec, input_filename);
     244             : 
     245           0 :   sumelm_algorithm<stochastic_specification>(spec, decluster).run();
     246             : 
     247           0 :   mCRL2log(log::debug) << "Sum elimination completed, saving to " <<  output_filename << std::endl;
     248           0 :   save_lps(spec, output_filename);
     249           0 : }
     250             : 
     251           0 : void lpssuminst(const std::string& input_filename,
     252             :                 const std::string& output_filename,
     253             :                 const data::rewriter::strategy rewrite_strategy,
     254             :                 const std::string& sorts_string,
     255             :                 const bool finite_sorts_only,
     256             :                 const bool tau_summands_only)
     257             : {
     258           0 :   stochastic_specification spec;
     259           0 :   load_lps(spec, input_filename);
     260           0 :   std::set<data::sort_expression> sorts;
     261             : 
     262             :   // Determine set of sorts to be expanded
     263           0 :   if(!sorts_string.empty())
     264             :   {
     265           0 :     std::vector<std::string> parts = utilities::split(utilities::remove_whitespace(sorts_string), ",");
     266           0 :     for (auto & part : parts)
     267             :     {
     268           0 :       sorts.insert(data::parse_sort_expression(part, spec.data()));
     269             :     }
     270             :   }
     271           0 :   else if (finite_sorts_only)
     272             :   {
     273           0 :     sorts = lps::finite_sorts(spec.data());
     274             :   }
     275             :   else
     276             :   {
     277           0 :     const std::set<data::sort_expression>& sort_set=spec.data().sorts();
     278           0 :     sorts = std::set<data::sort_expression>(sort_set.begin(),sort_set.end());
     279             :   }
     280             : 
     281           0 :   mCRL2log(log::verbose, "lpssuminst") << "expanding summation variables of sorts: " << data::pp(sorts) << std::endl;
     282             : 
     283           0 :   mcrl2::data::rewriter r(spec.data(), rewrite_strategy);
     284           0 :   lps::suminst_algorithm<data::rewriter, stochastic_specification>(spec, r, sorts, tau_summands_only).run();
     285           0 :   save_lps(spec, output_filename);
     286           0 : }
     287             : 
     288           0 : void lpsuntime(const std::string& input_filename,
     289             :                const std::string& output_filename,
     290             :                const bool add_invariants,
     291             :                const bool apply_fourier_motzkin,
     292             :                const data::rewriter::strategy rewrite_strategy
     293             :               )
     294             : {
     295           0 :   stochastic_specification spec;
     296           0 :   load_lps(spec, input_filename);
     297           0 :   data::rewriter rewr(spec.data(),rewrite_strategy);
     298           0 :   untime_algorithm<stochastic_specification>(spec, add_invariants, apply_fourier_motzkin, rewr).run();
     299           0 :   save_lps(spec, output_filename);
     300           0 : }
     301             : 
     302           0 : void txt2lps(const std::string& input_filename,
     303             :              const std::string& output_filename
     304             :             )
     305             : {
     306           0 :   lps::stochastic_specification spec;
     307           0 :   std::ifstream ifs(input_filename);
     308           0 :   if (!ifs.good())
     309             :   {
     310           0 :     throw mcrl2::runtime_error("Could not open file " + input_filename + ".");
     311             :   }
     312           0 :   parse_lps(ifs, spec);
     313           0 :   save_lps(spec, output_filename);
     314           0 : }
     315             : 
     316             : } // namespace lps
     317             : 
     318         261 : } // namespace mcrl2

Generated by: LCOV version 1.13