Term containing a string.
parameterized boolean equation system
Standard exception class for reporting runtime errors.
rewrite_strategy
The strategy of the rewriter.
std::set< data::variable > significant_variables(const pbes_expression &x)
Returns the significant variables of a pbes expression.
void remove_parameters(pbes &x, const std::set< data::variable > &to_be_removed)
Removes parameters from propositional variable instantiations in a pbes expression.
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_normalized(const pbes &x)
Checks if a PBEs is normalized.
std::vector< propositional_variable > remove_unreachable_variables(pbes &p)
Removes equations that are not (syntactically) reachable from the initial state of a PBES.
std::string print_removed_equations(const std::vector< propositional_variable > &removed)
Print removed equations.
void normalize(pbes &x)
The function normalize brings (embedded) pbes expressions into positive normal form,...
std::string print_removed_equations(const std::vector< propositional_variable > &removed)
T remove_parameters(const T &x, const std::vector< std::size_t > &to_be_removed, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
Removes parameters from propositional variable instantiations in a pbes expression.
void pbesinst_finite(pbes &p, data::rewrite_strategy rewrite_strategy, const std::string &finite_parameter_selection)
std::set< data::variable > significant_variables(const pbes_expression &x)
void normalize(T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
The function normalize brings (embedded) pbes expressions into positive normal form,...
std::vector< propositional_variable > remove_unreachable_variables(pbes &p)
Removes equations that are not (syntactically) reachable from the initial state of a PBES.
bool is_normalized(const T &x)
Checks if a pbes expression is normalized.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Normalization of pbes expressions.
add your file description here.
Functions for removing insignificant parameters from pbes types.
add your file description here.
add your file description here.