pbesfixpointsolve.h File Reference

This file provides a tool that can simplify PBESs by substituting PBES equations for variables in the rhs, simplifying the result, and keeping it when it can eliminate PBES variables. More...

Go to the source code of this file.

Classes
struct	mcrl2::pbes_system::pbesfixpointsolve_options
struct	mcrl2::pbes_system::pbesfixpointsolve_pbes_fixpoint_iterator

Namespaces
namespace	mcrl2
namespace	mcrl2::pbes_system
	The main namespace for the PBES library.

Enumerations
enum class	mcrl2::pbes_system::InvResult { mcrl2::pbes_system::INV_TRUE , mcrl2::pbes_system::INV_FALSE , mcrl2::pbes_system::EQ_FALSE }

Functions
void	mcrl2::pbes_system::substitute (pbes_equation &into, const pbes_equation &by, detail::substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter)
data::data_expression	mcrl2::pbes_system::pbestodata (pbes_equation &equation, detail::replace_other_propositional_variables_with_functions_builder< pbes_system::pbes_expression_builder > &replace_substituter)
InvResult	mcrl2::pbes_system::global_invariant_check (pbes_equation &equation, detail::substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter, detail::replace_other_propositional_variables_with_functions_builder< pbes_system::pbes_expression_builder > &replace_substituter, data::data_specification data_spec, simplify_data_rewriter< data::rewriter > pbes_rewriter, std::set< data::variable > &global_variables)
void	mcrl2::pbes_system::perform_iteration (pbes_equation &equation, detail::substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter, detail::replace_other_propositional_variables_with_functions_builder< pbes_system::pbes_expression_builder > &replace_substituter, data::data_specification data_spec, pbesfixpointsolve_options options, propositional_variable_instantiation initial_state, simplify_data_rewriter< data::rewriter > pbes_rewriter)

Detailed Description

This file provides a tool that can simplify PBESs by substituting PBES equations for variables in the rhs, simplifying the result, and keeping it when it can eliminate PBES variables.

Definition in file pbesfixpointsolve.h.