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/lps2pbes.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_TOOLS_LPS2PBES_H
      13             : #define MCRL2_PBES_TOOLS_LPS2PBES_H
      14             : 
      15             : #include "mcrl2/lps/io.h"
      16             : #include "mcrl2/modal_formula/parse.h"
      17             : #include "mcrl2/pbes/io.h"
      18             : #include "mcrl2/pbes/lps2pbes.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace pbes_system {
      23             : 
      24             : namespace detail
      25             : {
      26             : /// \brief Prints a warning if formula contains an action that is not used in lpsspec.
      27           0 : inline void check_lps2pbes_actions(const state_formulas::state_formula& formula, const lps::stochastic_specification& lpsspec)
      28             : {
      29           0 :   std::set<process::action_label> used_lps_actions = lps::find_action_labels(lpsspec.process());
      30           0 :   std::set<process::action_label> used_state_formula_actions = state_formulas::find_action_labels(formula);
      31           0 :   std::set<process::action_label> diff = utilities::detail::set_difference(used_state_formula_actions, used_lps_actions);
      32           0 :   if (!diff.empty())
      33             :   {
      34           0 :     mCRL2log(log::warning) << "Warning: the modal formula contains an action "
      35           0 :                            << *diff.begin()
      36           0 :                            << " that does not appear in the LPS!" << std::endl;
      37             :   }
      38           0 : }
      39             : 
      40             : } // namespace detail
      41             : 
      42           0 : void lps2pbes(const std::string& input_filename,
      43             :               const std::string& output_filename,
      44             :               const utilities::file_format& output_format,
      45             :               const std::string& formula_filename,
      46             :               bool timed,
      47             :               bool structured,
      48             :               bool unoptimized,
      49             :               bool preprocess_modal_operators,
      50             :               bool generate_counter_example,
      51             :               bool check_only
      52             :              )
      53             : {
      54           0 :   if (formula_filename.empty())
      55             :   {
      56           0 :     throw mcrl2::runtime_error("option -f is not specified");
      57             :   }
      58           0 :   if (input_filename.empty())
      59             :   {
      60           0 :     mCRL2log(log::verbose) << "reading LPS from stdin..." << std::endl;
      61             :   }
      62             :   else
      63             :   {
      64           0 :     mCRL2log(log::verbose) << "reading LPS from file '" <<  input_filename << "'..." << std::endl;
      65             :   }
      66           0 :   lps::stochastic_specification lpsspec;
      67           0 :   load_lps(lpsspec, input_filename);
      68           0 :   mCRL2log(log::verbose) << "reading input from file '" <<  formula_filename << "'..." << std::endl;
      69           0 :   std::ifstream from(formula_filename.c_str(), std::ifstream::in | std::ifstream::binary);
      70           0 :   if (!from)
      71             :   {
      72           0 :     throw mcrl2::runtime_error("cannot open state formula file: " + formula_filename);
      73             :   }
      74           0 :   std::string text = utilities::read_text(from);
      75           0 :   const bool formula_is_quantitative = false;
      76           0 :   state_formulas::state_formula_specification formspec = state_formulas::algorithms::parse_state_formula_specification(text, lpsspec, formula_is_quantitative);
      77           0 :   detail::check_lps2pbes_actions(formspec.formula(), lpsspec);
      78           0 :   mCRL2log(log::verbose) << "converting state formula and LPS to a PBES..." << std::endl;
      79           0 :   pbes_system::pbes result = pbes_system::lps2pbes(lpsspec, formspec, timed, structured, unoptimized, preprocess_modal_operators, generate_counter_example, check_only);
      80             : 
      81           0 :   if (check_only)
      82             :   {
      83           0 :     mCRL2log(mcrl2::log::info)
      84             :       << "the file '" << formula_filename
      85           0 :       << "' contains a well-formed state formula" << std::endl;
      86           0 :     return;
      87             :   }
      88             : 
      89           0 :   if (output_filename.empty())
      90             :   {
      91           0 :     mCRL2log(log::verbose) << "writing PBES to stdout..." << std::endl;
      92             :   }
      93             :   else
      94             :   {
      95           0 :     mCRL2log(log::verbose) << "writing PBES to file '" <<  output_filename << "'..." << std::endl;
      96             :   }
      97           0 :   save_pbes(result, output_filename, output_format);
      98           0 : }
      99             : 
     100             : } // namespace pbes_system
     101             : 
     102             : } // namespace mcrl2
     103             : 
     104             : #endif // MCRL2_PBES_TOOLS_LPS2PBES_H