linearise.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_LPS_LINEARISE_H
#define MCRL2_LPS_LINEARISE_H
 
#include "mcrl2/data/rewriter.h"
#include "mcrl2/lps/linearisation_method.h"
#include "mcrl2/lps/stochastic_specification.h"
#include "mcrl2/process/parse.h"
 
namespace mcrl2
{
 
namespace lps
{
 
struct t_lin_options
{
  t_lin_method lin_method;
  bool no_intermediate_cluster;
  bool final_cluster;
  bool newstate;
  bool binary;
  bool statenames;
  bool norewrite;
  bool noglobalvars;
  bool nosumelm;
  bool nodeltaelimination;
  bool ignore_time;
  bool do_not_apply_constelm;
  bool apply_alphabet_axioms;
  bool balance_summands;      // Used to balance long expressions of the shape p1 + p2 + ... + pn. By default the parser delivers
                              // such expressions in a skewed form, causing stack overflow. 
  mcrl2::data::rewriter::strategy rewrite_strategy;
 
  t_lin_options()
    : lin_method(lmRegular),
      no_intermediate_cluster(false),
      final_cluster(false),
      newstate(false),
      binary(false),
      statenames(false),
      norewrite(false),
      noglobalvars(false),
      nosumelm(false),
      nodeltaelimination(false),
      ignore_time(false),
      do_not_apply_constelm(false),
      apply_alphabet_axioms(false),
      balance_summands(false),              
      rewrite_strategy(mcrl2::data::jitty)
  {}
};
 
mcrl2::lps::stochastic_specification linearise(
  const mcrl2::process::process_specification& type_checked_spec,
  mcrl2::lps::t_lin_options lin_options = t_lin_options());
 
inline mcrl2::lps::stochastic_specification linearise(
  const std::string& text,
  mcrl2::lps::t_lin_options lin_options = t_lin_options())
{
  mcrl2::process::process_specification spec =
      mcrl2::process::parse_process_specification(text);
  return linearise(spec, lin_options);
}
 
} // namespace lps
 
} // namespace mcrl2
 
#endif // MCRL2_LPS_LINEARISE_H