Line data    Source code

       1             : // Author(s): Jan Friso Groote
       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/lps/linearise.h
      10             : /// \brief Linearisation of process specifications
      11             : 
      12             : #ifndef MCRL2_LPS_LINEARISE_H
      13             : #define MCRL2_LPS_LINEARISE_H
      14             : 
      15             : #include "mcrl2/data/rewriter.h"
      16             : #include "mcrl2/lps/linearisation_method.h"
      17             : #include "mcrl2/lps/stochastic_specification.h"
      18             : #include "mcrl2/process/parse.h"
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace lps
      24             : {
      25             : 
      26             : /// \brief Options for linearisation
      27             : struct t_lin_options
      28             : {
      29             :   t_lin_method lin_method;
      30             :   bool no_intermediate_cluster;
      31             :   bool final_cluster;
      32             :   bool newstate;
      33             :   bool binary;
      34             :   bool statenames;
      35             :   bool norewrite;
      36             :   bool noglobalvars;
      37             :   bool nosumelm;
      38             :   bool nodeltaelimination;
      39             :   bool ignore_time;
      40             :   bool do_not_apply_constelm;
      41             :   bool apply_alphabet_axioms;
      42             :   bool balance_summands;      // Used to balance long expressions of the shape p1 + p2 + ... + pn. By default the parser delivers
      43             :                               // such expressions in a skewed form, causing stack overflow. 
      44             :   mcrl2::data::rewriter::strategy rewrite_strategy;
      45             : 
      46         241 :   t_lin_options()
      47         241 :     : lin_method(lmRegular),
      48         241 :       no_intermediate_cluster(false),
      49         241 :       final_cluster(false),
      50         241 :       newstate(false),
      51         241 :       binary(false),
      52         241 :       statenames(false),
      53         241 :       norewrite(false),
      54         241 :       noglobalvars(false),
      55         241 :       nosumelm(false),
      56         241 :       nodeltaelimination(false),
      57         241 :       ignore_time(false),
      58         241 :       do_not_apply_constelm(false),
      59         241 :       apply_alphabet_axioms(false),
      60         241 :       balance_summands(false),              
      61         241 :       rewrite_strategy(mcrl2::data::jitty)
      62         241 :   {}
      63             : };
      64             : 
      65             : /// \brief Linearises a process specification
      66             : /// \param[in] type_checked_spec A process specification
      67             : /// \param[in] lin_options options that should be used during linearisation
      68             : /// \return An LPS equivalent to spec, which is linearised using lin_options
      69             : /// \exception mcrl2::runtime_error Linearisation failed
      70             : mcrl2::lps::stochastic_specification linearise(
      71             :   const mcrl2::process::process_specification& type_checked_spec,
      72             :   mcrl2::lps::t_lin_options lin_options = t_lin_options());
      73             : 
      74             : /// \brief Linearises a process specification from a textual specification
      75             : /// \param[in] text A string containing a process specification
      76             : /// \param[in] lin_options options that should be used during linearisation
      77             : /// \return An LPS equivalent to the specification representing text, which is linearised using lin_options
      78             : /// \exception mcrl2::runtime_error Linearisation failed
      79         881 : inline mcrl2::lps::stochastic_specification linearise(
      80             :   const std::string& text,
      81             :   mcrl2::lps::t_lin_options lin_options = t_lin_options())
      82             : {
      83             :   mcrl2::process::process_specification spec =
      84         881 :       mcrl2::process::parse_process_specification(text);
      85        1726 :   return linearise(spec, lin_options);
      86         875 : }
      87             : 
      88             : } // namespace lps
      89             : 
      90             : } // namespace mcrl2
      91             : 
      92             : #endif // MCRL2_LPS_LINEARISE_H