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

Generated by: LCOV version 1.13