pbesinst_algorithm.h File Reference

Algorithm for instantiating a PBES. More...

Go to the source code of this file.

Classes
struct	mcrl2::pbes_system::pbesinst_rename_long
	Creates a unique name for a propositional variable instantiation. The propositional variable instantiation must be closed. Originally implemented by Alexander van Dam. More...
struct	mcrl2::pbes_system::pbesinst_rename
	Creates a unique name for a propositional variable instantiation. The propositional variable instantiation must be closed. Originally implemented by Alexander van Dam. More...
class	mcrl2::pbes_system::pbesinst_algorithm
	Algorithm class for the pbesinst instantiation algorithm. More...

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

Functions
void	mcrl2::pbes_system::make_pbesinst_substitution (const data::variable_list &v, const data::data_expression_list &e, data::rewriter::substitution_type &sigma)
	Creates a substitution function for the pbesinst rewriter.
bool	mcrl2::pbes_system::pbesinst_is_constant (const pbes_expression &x)

Detailed Description

Algorithm for instantiating a PBES.

Definition in file pbesinst_algorithm.h.