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.

void complps2pbes(const std::string &input_filename, const std::string &output_filename, const utilities::file_format &output_format, const std::string &formula_filename)
pbes_system::pbes mcrl2::pbes_system::complps2pbes(const process::process_specification &procspec, const state_formulas::state_formula&)
std::set<data::variable> find_all_variables(const pbes_system::pbes &x)
std::set<data::variable> find_free_variables(const pbes_system::pbes &x)
std::set<data::function_symbol> find_function_symbols(const pbes_system::pbes &x)
std::set<data::sort_expression> find_sort_expressions(const pbes_system::pbes &x)
bool is_well_typed_equation(const pbes_equation &eqn, const std::set<data::sort_expression> &declared_sorts, const std::set<data::variable> &declared_global_variables, const data::data_specification &data_spec)
bool is_well_typed_pbes(const std::set<data::sort_expression> &declared_sorts, const std::set<data::variable> &declared_global_variables, const std::set<data::variable> &occurring_global_variables, const std::set<propositional_variable> &declared_variables, const std::set<propositional_variable_instantiation> &occ, const propositional_variable_instantiation &init, const data::data_specification &data_spec)
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 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.

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.

void normalize_sorts(pbes &x, const data::sort_specification &sortspec)
std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const srf_summand &summand)
std::ostream &mcrl2::pbes_system::operator<<(std::ostream &out, const srf_equation &eqn)
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

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

atermpp::aterm_appl pbes_to_aterm(const pbes &p)

Conversion to atermappl.

Returns: The PBES converted to aterm format.

std::string pp(const pbes &x)
void translate_user_notation(pbes_system::pbes &x)
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(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

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