mcrl2/pbes/lps2pbes.h

Include file:

#include "mcrl2/pbes/lps2pbes.h"

Add your file description here.

Functions

pbes_system::pbes mcrl2::pbes_system::complps2pbes(const process::process_specification &procspec, const state_formulas::state_formula&)
void complps2pbes(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, const std::string &formula_filename)
pbes mcrl2::pbes_system::lps2pbes(const lps::specification &lpsspec, const state_formulas::state_formula &formula, bool timed = false, bool structured = false, bool unoptimized = false, bool preprocess_modal_operators = false, bool generate_counter_example = false, bool check_only = false)

Translates a linear process specification and a state formula to a PBES. If the solution of the PBES is true, the formula holds for the specification.

Parameters:

  • lpsspec A linear process specification.
  • formula A modal formula.
  • timed determines whether the timed or untimed variant of the algorithm is chosen.
  • structured use the ‘structured’ approach of generating equations.
  • unoptimized if true, the resulting PBES is not simplified, if false (default), the PBES is simplified.
  • preprocess_modal_operators A boolean indicating that the modal operators can be preprocessed to obtain a more compact PBES.
  • generate_counter_example A boolean indicating that a counter example must be generated.

Returns: The resulting pbes.

pbes mcrl2::pbes_system::lps2pbes(const lps::specification &lpsspec, const state_formulas::state_formula_specification &formspec, bool timed = false, bool structured = false, bool unoptimized = false, bool preprocess_modal_operators = false, bool generate_counter_example = false, bool check_only = false)

Translates a linear process specification and a state formula to a PBES. If the solution of the PBES is true, the formula holds for the specification.

Parameters:

  • lpsspec A linear process specification.
  • formspec A modal formula specification.
  • timed determines whether the timed or untimed variant of the algorithm is chosen.
  • structured use the ‘structured’ approach of generating equations.
  • unoptimized if true, the resulting PBES is not simplified, if false (default), the PBES is simplified.
  • preprocess_modal_operators A boolean indicating that the modal operators can be preprocessed to obtain a more compact PBES.
  • generate_counter_example A boolean indicating that a counter example must be generated.
  • check_only If check_only is true, only the formula will be checked, but no PBES is generated

Returns: The resulting pbes.

void lps2pbes(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, const std::string &formula_filename, bool timed, bool structured, bool unoptimized, bool preprocess_modal_operators, bool generate_counter_example, bool check_only)
pbes mcrl2::pbes_system::lps2pbes(const std::string &spec_text, const std::string &formula_text, bool timed = false, bool structured = false, bool unoptimized = false, bool preprocess_modal_operators = false, bool generate_counter_example = false, bool check_only = false)

Applies the lps2pbes algorithm.

Parameters:

  • spec_text A string.
  • formula_text A string.
  • timed Determines whether the timed or untimed version of the translation algorithm is used.
  • structured use the ‘structured’ approach of generating equations.
  • unoptimized if true, the resulting PBES is not simplified, if false (default), the PBES is simplified.
  • preprocess_modal_operators A boolean indicating that the modal operators can be preprocessed to obtain a more compact PBES.
  • generate_counter_example A boolean indicating that a counter example must be generated.
  • check_only If check_only is true, only the formula will be checked, but no PBES is generated

Returns: The result of the algorithm