LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/tools - lps2pbes.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 24 0.0 %
Date: 2020-02-13 00:44:47 Functions: 0 1 0.0 %
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 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           0 : void lps2pbes(const std::string& input_filename,
      25             :               const std::string& output_filename,
      26             :               const utilities::file_format& output_format,
      27             :               const std::string& formula_filename,
      28             :               bool timed,
      29             :               bool structured,
      30             :               bool unoptimized,
      31             :               bool preprocess_modal_operators,
      32             :               bool generate_counter_example,
      33             :               bool check_only
      34             :              )
      35             : {
      36           0 :   if (formula_filename.empty())
      37             :   {
      38           0 :     throw mcrl2::runtime_error("option -f is not specified");
      39             :   }
      40           0 :   if (input_filename.empty())
      41             :   {
      42           0 :     mCRL2log(log::verbose) << "reading LPS from stdin..." << std::endl;
      43             :   }
      44             :   else
      45             :   {
      46           0 :     mCRL2log(log::verbose) << "reading LPS from file '" <<  input_filename << "'..." << std::endl;
      47             :   }
      48           0 :   lps::specification lpsspec;
      49           0 :   load_lps(lpsspec, input_filename);
      50           0 :   mCRL2log(log::verbose) << "reading input from file '" <<  formula_filename << "'..." << std::endl;
      51           0 :   std::ifstream from(formula_filename.c_str(), std::ifstream::in | std::ifstream::binary);
      52           0 :   if (!from)
      53             :   {
      54           0 :     throw mcrl2::runtime_error("cannot open state formula file: " + formula_filename);
      55             :   }
      56           0 :   std::string text = utilities::read_text(from);
      57           0 :   state_formulas::state_formula_specification formspec = state_formulas::algorithms::parse_state_formula_specification(text, lpsspec);
      58           0 :   mCRL2log(log::verbose) << "converting state formula and LPS to a PBES..." << std::endl;
      59           0 :   pbes_system::pbes result = pbes_system::lps2pbes(lpsspec, formspec, timed, structured, unoptimized, preprocess_modal_operators, generate_counter_example, check_only);
      60             : 
      61           0 :   if (check_only)
      62             :   {
      63           0 :     mCRL2log(mcrl2::log::info)
      64             :       << "the file '" << formula_filename
      65           0 :       << "' contains a well-formed state formula" << std::endl;
      66           0 :     return;
      67             :   }
      68             : 
      69           0 :   if (output_filename.empty())
      70             :   {
      71           0 :     mCRL2log(log::verbose) << "writing PBES to stdout..." << std::endl;
      72             :   }
      73             :   else
      74             :   {
      75           0 :     mCRL2log(log::verbose) << "writing PBES to file '" <<  output_filename << "'..." << std::endl;
      76             :   }
      77           0 :   save_pbes(result, output_filename, output_format);
      78             : }
      79             : 
      80             : } // namespace pbes_system
      81             : 
      82             : } // namespace mcrl2
      83             : 
      84             : #endif // MCRL2_PBES_TOOLS_LPS2PBES_H

Generated by: LCOV version 1.13