pbesbackelm.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::pbesbackelm_options
struct	mcrl2::pbes_system::substitute_propositional_variables_builder< Builder >
struct	mcrl2::pbes_system::pbesbackelm_pbes_backward_substituter

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::pbes_system
	The main namespace for the PBES library.

Functions
void	mcrl2::pbes_system::self_substitute (pbes_equation &equation, substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter)
void	mcrl2::pbes_system::substitute (pbes_equation &into, const pbes_equation &by, substitute_propositional_variables_builder< pbes_system::pbes_expression_builder > &substituter)
void	mcrl2::pbes_system::pbesbackelm (const std::string &input_filename, const std::string &output_filename, const utilities::file_format &input_format, const utilities::file_format &output_format, pbesbackelm_options options)

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 pbesbackelm.h.