mCRL2
|
Functions | |
void | remove_parameters (pbes &x, const std::set< data::variable > &to_be_removed) |
Removes parameters from propositional variable instantiations in a pbes expression. | |
void | remove_parameters (pbes &x, const std::map< core::identifier_string, std::vector< std::size_t > > &to_be_removed) |
Removes parameters from propositional variable instantiations in a pbes expression. | |
void | normalize (pbes &x) |
The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>. | |
bool | is_normalized (const pbes &x) |
Checks if a PBEs is normalized. | |
void | instantiate_global_variables (pbes &p) |
Attempts to eliminate the free variables of a PBES, by substituting a constant value for them. If no constant value is found for one of the variables, an exception is thrown. | |
void | pbesinst_finite (pbes &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection) |
Apply finite instantiation to the given PBES. | |
bool | is_bes (const pbes &x) |
Returns true if a PBES is in BES form. | |
std::string | print_removed_equations (const std::vector< propositional_variable > &removed) |
Print removed equations. | |
std::vector< propositional_variable > | remove_unreachable_variables (pbes &p) |
Removes equations that are not (syntactically) reachable from the initial state of a PBES. | |
std::set< data::variable > | significant_variables (const pbes_expression &x) |
Returns the significant variables of a pbes expression. | |
void mcrl2::pbes_system::algorithms::instantiate_global_variables | ( | pbes & | p | ) |
bool mcrl2::pbes_system::algorithms::is_bes | ( | const pbes & | x | ) |
bool mcrl2::pbes_system::algorithms::is_normalized | ( | const pbes & | x | ) |
Checks if a PBEs is normalized.
Definition at line 48 of file algorithms.cpp.
void mcrl2::pbes_system::algorithms::normalize | ( | pbes & | x | ) |
The function normalize brings (embedded) pbes expressions into positive normal form, i.e. a formula without any occurrences of ! or =>.
x | an object containing pbes expressions |
Definition at line 36 of file algorithms.cpp.
void mcrl2::pbes_system::algorithms::pbesinst_finite | ( | pbes & | p, |
data::rewrite_strategy | rewrite_strategy, | ||
const std::string & | finite_parameter_selection | ||
) |
Apply finite instantiation to the given PBES.
Definition at line 53 of file algorithms.cpp.
std::string mcrl2::pbes_system::algorithms::print_removed_equations | ( | const std::vector< propositional_variable > & | removed | ) |
Print removed equations.
Definition at line 58 of file algorithms.cpp.
void mcrl2::pbes_system::algorithms::remove_parameters | ( | pbes & | x, |
const std::map< core::identifier_string, std::vector< std::size_t > > & | to_be_removed | ||
) |
Removes parameters from propositional variable instantiations in a pbes expression.
x | A PBES library object that does not derive from atermpp::aterm |
to_be_removed | A mapping that maps propositional variable names to indices of parameters that are removed |
x
with parameters removed according to the mapping to_be_removed
Definition at line 31 of file algorithms.cpp.
void mcrl2::pbes_system::algorithms::remove_parameters | ( | pbes & | x, |
const std::set< data::variable > & | to_be_removed | ||
) |
Removes parameters from propositional variable instantiations in a pbes expression.
x | A PBES library object that does not derive from atermpp::aterm |
to_be_removed | A set of parameters that are to be removed |
x
with parameters removed according to the mapping to_be_removed
Definition at line 26 of file algorithms.cpp.
std::vector< propositional_variable > mcrl2::pbes_system::algorithms::remove_unreachable_variables | ( | pbes & | p | ) |
Removes equations that are not (syntactically) reachable from the initial state of a PBES.
Definition at line 63 of file algorithms.cpp.
std::set< data::variable > mcrl2::pbes_system::algorithms::significant_variables | ( | const pbes_expression & | x | ) |
Returns the significant variables of a pbes expression.
Definition at line 68 of file algorithms.cpp.