mCRL2
Loading...
Searching...
No Matches
mcrl2::pbes_system::algorithms Namespace Reference

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_variableremove_unreachable_variables (pbes &p)
 Removes equations that are not (syntactically) reachable from the initial state of a PBES.
 
std::set< data::variablesignificant_variables (const pbes_expression &x)
 Returns the significant variables of a pbes expression.
 

Function Documentation

◆ instantiate_global_variables()

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.

Definition at line 65 of file pbes.cpp.

◆ is_bes()

bool mcrl2::pbes_system::algorithms::is_bes ( const pbes x)

Returns true if a PBES is in BES form.

Parameters
xa PBES

Definition at line 70 of file pbes.cpp.

◆ is_normalized()

bool mcrl2::pbes_system::algorithms::is_normalized ( const pbes x)

Checks if a PBEs is normalized.

Returns
True if the PBES is normalized

Definition at line 48 of file algorithms.cpp.

◆ normalize()

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 =>.

Parameters
xan object containing pbes expressions

Definition at line 36 of file algorithms.cpp.

◆ pbesinst_finite()

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.

◆ print_removed_equations()

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.

◆ remove_parameters() [1/2]

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.

Parameters
xA PBES library object that does not derive from atermpp::aterm
to_be_removedA mapping that maps propositional variable names to indices of parameters that are removed
Returns
The expression x with parameters removed according to the mapping to_be_removed

Definition at line 31 of file algorithms.cpp.

◆ remove_parameters() [2/2]

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.

Parameters
xA PBES library object that does not derive from atermpp::aterm
to_be_removedA set of parameters that are to be removed
Returns
The expression x with parameters removed according to the mapping to_be_removed

Definition at line 26 of file algorithms.cpp.

◆ remove_unreachable_variables()

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.

Returns
The removed variables

Definition at line 63 of file algorithms.cpp.

◆ significant_variables()

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.