mcrl2/pbes/pbes.h

Include file:

#include "mcrl2/pbes/pbes.h"

The class pbes.

Functions

void complete_data_specification(pbes &p)

Adds all sorts that appear in the PBES p to the data specification of p.

Parameters:

  • p a PBES.
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

void lpsbisim2pbes(const std::string &input_filename1, const std::string &input_filename2, const std::string &output_filename, const utilities::file_format &output_format, bisimulation_type type, bool normalize)
pbes mcrl2::pbes_system::lts2pbes(const lts::lts_lts_t &l, const state_formulas::state_formula_specification &formspec, bool preprocess_modal_operators = false, bool generate_counter_example = false)

Translates an LTS and a modal formula into a PBES that represents the corresponding model checking problem.

Parameters:

  • l A labelled transition system.
  • formspec A modal formula specification.
  • preprocess_modal_operators A boolean indicating that modal operators must be preprocessed.
  • generate_counter_example A boolean indicating that a counter example must be generated.
std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const pbes &x)

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const srf_equation &eqn)
std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const srf_summand &summand)
bool mcrl2::pbes_system::operator==(const pbes &p1, const pbes &p2)

Equality operator on PBESs.

Returns: True if the PBESs have exactly the same internal representation. Note that this is in general not a very useful test.

srf_pbes mcrl2::pbes_system::pbes2srf(const pbes &p)

Converts a PBES into standard recursive form.

Pre: The pbes p must be normalized

void txt2pbes(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, bool normalize)
pbes mcrl2::pbes_system::txt2pbes(const std::string &text, bool normalize = true)

Parses a PBES specification from a string.

Parameters:

  • text A string
  • normalize If true, the resulting PBES is normalized after reading.

Returns: The parsed PBES

pbes mcrl2::pbes_system::txt2pbes(std::istream &spec_stream, bool normalize = true)

Parses a PBES specification from an input stream.

Parameters:

  • spec_stream A stream from which can be read
  • normalize If true, the resulting PBES is normalized after reading.

Returns: The parsed PBES