mcrl2/pbes/tools/lps2pbes.h

Include file:

#include "mcrl2/pbes/tools/lps2pbes.h"

add your file description here.

Functions

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&)
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

Functions

void mcrl2::pbes_system::detail::check_lps2pbes_actions(const state_formulas::state_formula &formula, const lps::specification &lpsspec)

Prints a warning if formula contains an action that is not used in lpsspec.