parameterized boolean equation system More...

#include <pres.h>

Public Types
typedef pres_equation	equation_type

Public Member Functions
	pres ()=default
	Constructor.

	pres (data::data_specification const &data, const std::vector< pres_equation > &equations, propositional_variable_instantiation initial_state)
	Constructor.

	pres (data::data_specification const &data, const std::set< data::variable > &global_variables, const std::vector< pres_equation > &equations, propositional_variable_instantiation initial_state)
	Constructor.

const data::data_specification &	data () const
	Returns the data specification.

void	set_data (const data::data_specification &d)
	Allows to set the data specification of a pres.

const std::vector< pres_equation > &	equations () const
	Returns the equations.

std::vector< pres_equation > &	equations ()
	Returns the equations.

const std::set< data::variable > &	global_variables () const
	Returns the declared free variables of the pres.

std::set< data::variable > &	global_variables ()
	Returns the declared free variables of the pres.

const propositional_variable_instantiation &	initial_state () const
	Returns the initial state.

propositional_variable_instantiation &	initial_state ()
	Returns the initial state.

std::set< propositional_variable >	binding_variables () const
	Returns the set of binding variables of the pres. This is the set variables that occur on the left hand side of an equation.

std::set< propositional_variable_instantiation >	occurring_variable_instantiations () const
	Returns the set of occurring propositional variable instantiations of the pres. This is the set of variables that occur in the right hand side of an equation.

std::set< propositional_variable >	occurring_variables () const
	Returns the set of occurring propositional variable declarations of the pres, i.e. the propositional variable declarations that occur in the right hand side of an equation.

bool	is_closed () const
	True if the pres is closed.

bool	is_well_typed () const
	Checks if the PRES is well typed.

Protected Member Functions
std::set< propositional_variable >	compute_declared_variables () const
	Returns the predicate variables appearing in the left hand side of an equation.

template<typename Iter >
bool	is_declared_in (Iter first, Iter last, const propositional_variable_instantiation &v, const data::data_specification &data_spec) const
	Checks if the propositional variable instantiation v appears with the right type in the sequence of propositional variable declarations [first, last).

Protected Attributes
data::data_specification	m_data
	The data specification.

std::vector< pres_equation >	m_equations
	The sequence of pres equations.

std::set< data::variable >	m_global_variables
	The set of global variables.

propositional_variable_instantiation	m_initial_state
	The initial state.

Detailed Description

parameterized boolean equation system

Definition at line 58 of file pres.h.

Member Typedef Documentation

◆ equation_type

typedef pres_equation mcrl2::pres_system::pres::equation_type

Definition at line 61 of file pres.h.

Constructor & Destructor Documentation

◆ pres() [1/3]

mcrl2::pres_system::pres::pres ( )

default

Constructor.

◆ pres() [2/3]

mcrl2::pres_system::pres::pres	(	data::data_specification const &	data,
		const std::vector< pres_equation > &	equations,
		propositional_variable_instantiation	initial_state
	)

inline

Constructor.

Parameters

data	A data specification
equations	A sequence of pres equations
initial_state	A propositional variable instantiation

Definition at line 117 of file pres.h.

◆ pres() [3/3]

mcrl2::pres_system::pres::pres	(	data::data_specification const &	data,
		const std::set< data::variable > &	global_variables,
		const std::vector< pres_equation > &	equations,
		propositional_variable_instantiation	initial_state
	)

inline

Constructor.

Parameters

data	A data specification
equations	A sequence of pres equations
global_variables	A sequence of free variables
initial_state	A propositional variable instantiation

Definition at line 136 of file pres.h.

Member Function Documentation

◆ binding_variables()

std::set< propositional_variable > mcrl2::pres_system::pres::binding_variables ( ) const

inline

Returns the set of binding variables of the pres. This is the set variables that occur on the left hand side of an equation.

Returns: The set of binding variables of the pres.

Definition at line 213 of file pres.h.

◆ compute_declared_variables()

std::set< propositional_variable > mcrl2::pres_system::pres::compute_declared_variables ( ) const

inlineprotected

Returns the predicate variables appearing in the left hand side of an equation.

Returns: The predicate variables appearing in the left hand side of an equation.

Definition at line 78 of file pres.h.

◆ data()

const data::data_specification & mcrl2::pres_system::pres::data ( ) const

inline

Returns the data specification.

Returns: The data specification of the pres

Definition at line 153 of file pres.h.

◆ equations() [1/2]

std::vector< pres_equation > & mcrl2::pres_system::pres::equations ( )

inline

Returns the equations.

Returns: The equations.

Definition at line 177 of file pres.h.

◆ equations() [2/2]

const std::vector< pres_equation > & mcrl2::pres_system::pres::equations ( ) const

inline

Returns the equations.

Returns: The equations.

Definition at line 170 of file pres.h.

◆ global_variables() [1/2]

std::set< data::variable > & mcrl2::pres_system::pres::global_variables ( )

inline

Returns the declared free variables of the pres.

Returns: The declared free variables of the pres.

Definition at line 191 of file pres.h.

◆ global_variables() [2/2]

const std::set< data::variable > & mcrl2::pres_system::pres::global_variables ( ) const

inline

Returns the declared free variables of the pres.

Returns: The declared free variables of the pres.

Definition at line 184 of file pres.h.

◆ initial_state() [1/2]

propositional_variable_instantiation & mcrl2::pres_system::pres::initial_state ( )

inline

Returns the initial state.

Returns: The initial state.

Definition at line 205 of file pres.h.

◆ initial_state() [2/2]

const propositional_variable_instantiation & mcrl2::pres_system::pres::initial_state ( ) const

inline

Returns the initial state.

Returns: The initial state.

Definition at line 198 of file pres.h.

◆ is_closed()

bool mcrl2::pres_system::pres::is_closed ( ) const

inline

True if the pres is closed.

Returns: Returns true if all occurring variables are binding variables, and the initial state variable is a binding variable.

Definition at line 251 of file pres.h.

◆ is_declared_in()

template<typename Iter >

bool mcrl2::pres_system::pres::is_declared_in	(	Iter	first,
		Iter	last,
		const propositional_variable_instantiation &	v,
		const data::data_specification &	data_spec
	)		const

inlineprotected

Checks if the propositional variable instantiation v appears with the right type in the sequence of propositional variable declarations [first, last).

Parameters

first	Start of a sequence of propositional variable declarations
last	End of a sequence of propositional variable declarations
v	A propositional variable instantation
data_spec	A data specification.

Returns: True if the type of v is matched correctly

Parameters

v	A propositional variable instantiation

Definition at line 97 of file pres.h.

◆ is_well_typed()

bool mcrl2::pres_system::pres::is_well_typed ( ) const

inline

Checks if the PRES is well typed.

Returns

True if

the sorts occurring in the free variables of the equations are declared in the data specification
the sorts occurring in the binding variable parameters are declared in the data specification
the sorts occurring in the quantifier variables of the equations are declared in the data specification
the binding variables of the equations have unique names (well formedness)
the global variables occurring in the equations are declared in global_variables()
the global variables occurring in the equations with the same name are identical
the declared global variables and the quantifier variables occurring in the equations have different names
the predicate variable instantiations occurring in the equations match with their declarations
the predicate variable instantiation occurring in the initial state matches with the declaration
the data specification is well typed

N.B. Conflicts between the types of instantiations and declarations of binding variables are not checked!

Definition at line 273 of file pres.h.

◆ occurring_variable_instantiations()

std::set< propositional_variable_instantiation > mcrl2::pres_system::pres::occurring_variable_instantiations ( ) const

Returns the set of occurring propositional variable instantiations of the pres. This is the set of variables that occur in the right hand side of an equation.

Returns: The occurring propositional variable instantiations of the pres

Definition at line 111 of file pres.cpp.

◆ occurring_variables()

std::set< propositional_variable > mcrl2::pres_system::pres::occurring_variables ( ) const

inline

Returns the set of occurring propositional variable declarations of the pres, i.e. the propositional variable declarations that occur in the right hand side of an equation.

Returns: The occurring propositional variable declarations of the pres

Definition at line 233 of file pres.h.

◆ set_data()

void mcrl2::pres_system::pres::set_data ( const data::data_specification & d )

inline

Allows to set the data specification of a pres.

Definition at line 159 of file pres.h.

Member Data Documentation

◆ m_data

data::data_specification mcrl2::pres_system::pres::m_data

protected

The data specification.

Definition at line 65 of file pres.h.

◆ m_equations

std::vector<pres_equation> mcrl2::pres_system::pres::m_equations

protected

The sequence of pres equations.

Definition at line 68 of file pres.h.

◆ m_global_variables

std::set<data::variable> mcrl2::pres_system::pres::m_global_variables

protected

The set of global variables.

Definition at line 71 of file pres.h.

◆ m_initial_state

propositional_variable_instantiation mcrl2::pres_system::pres::m_initial_state

protected

The initial state.

Definition at line 74 of file pres.h.

The documentation for this class was generated from the following files:

pres/include/mcrl2/pres/pres.h
pres/source/pres.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ equation_type

Constructor & Destructor Documentation

◆ pres() [1/3]

◆ pres() [2/3]

◆ pres() [3/3]

Member Function Documentation

◆ binding_variables()

◆ compute_declared_variables()

◆ data()

◆ equations() [1/2]

◆ equations() [2/2]

◆ global_variables() [1/2]

◆ global_variables() [2/2]

◆ initial_state() [1/2]

◆ initial_state() [2/2]

◆ is_closed()

◆ is_declared_in()

◆ is_well_typed()

◆ occurring_variable_instantiations()

◆ occurring_variables()

◆ set_data()

Member Data Documentation

◆ m_data

◆ m_equations

◆ m_global_variables

◆ m_initial_state