|
mCRL2
|
add your file description here. More...
Go to the source code of this file.
Namespaces | |
| namespace | mcrl2 |
| namespace | mcrl2::pbes_system |
| The main namespace for the PBES library. | |
| namespace | mcrl2::pbes_system::algorithms |
Functions | |
| 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. | |
| 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. | |
| 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 =>. | |
| bool | mcrl2::pbes_system::algorithms::is_normalized (const pbes &x) |
| Checks if a PBEs is normalized. | |
| void | mcrl2::pbes_system::algorithms::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 | 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. | |
| bool | mcrl2::pbes_system::algorithms::is_bes (const pbes &x) |
| Returns true if a PBES is in BES form. | |
| std::string | mcrl2::pbes_system::algorithms::print_removed_equations (const std::vector< propositional_variable > &removed) |
| Print removed equations. | |
| 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. | |
| std::set< data::variable > | mcrl2::pbes_system::algorithms::significant_variables (const pbes_expression &x) |
| Returns the significant variables of a pbes expression. | |
add your file description here.
Definition in file algorithms.h.