parameterized boolean equation system More...

#include <pbes.h>

Public Types
using	equation_type = pbes_equation

Public Member Functions
	pbes ()=default
	Constructor.

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

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

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

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

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

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

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

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

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 pbes. 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 pbes. 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 pbes, i.e. the propositional variable declarations that occur in the right hand side of an equation.

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

bool	is_well_typed () const
	Checks if the PBES 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< pbes_equation >	m_equations
	The sequence of pbes 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 53 of file pbes.h.

Member Typedef Documentation

◆ equation_type

using mcrl2::pbes_system::pbes::equation_type = pbes_equation

Definition at line 56 of file pbes.h.

Constructor & Destructor Documentation

◆ pbes() [1/3]

mcrl2::pbes_system::pbes::pbes ( )

default

Constructor.

◆ pbes() [2/3]

mcrl2::pbes_system::pbes::pbes	(	const data::data_specification &	data,
		const std::vector< pbes_equation > &	equations,
		propositional_variable_instantiation	initial_state
	)

inline

Constructor.

Parameters

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

Definition at line 112 of file pbes.h.

◆ pbes() [3/3]

mcrl2::pbes_system::pbes::pbes	(	const data::data_specification &	data,
		const std::set< data::variable > &	global_variables,
		const std::vector< pbes_equation > &	equations,
		propositional_variable_instantiation	initial_state
	)

inline

Constructor.

Parameters

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

Definition at line 130 of file pbes.h.

Member Function Documentation

◆ binding_variables()

std::set< propositional_variable > mcrl2::pbes_system::pbes::binding_variables ( ) const

inline

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

Returns: The set of binding variables of the pbes.

Definition at line 203 of file pbes.h.

◆ compute_declared_variables()

std::set< propositional_variable > mcrl2::pbes_system::pbes::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 73 of file pbes.h.

◆ data() [1/2]

data::data_specification & mcrl2::pbes_system::pbes::data ( )

inline

Returns the data specification.

Returns: The data specification of the pbes

Definition at line 153 of file pbes.h.

◆ data() [2/2]

const data::data_specification & mcrl2::pbes_system::pbes::data ( ) const

inline

Returns the data specification.

Returns: The data specification of the pbes

Definition at line 146 of file pbes.h.

◆ equations() [1/2]

std::vector< pbes_equation > & mcrl2::pbes_system::pbes::equations ( )

inline

Returns the equations.

Returns: The equations.

Definition at line 167 of file pbes.h.

◆ equations() [2/2]

const std::vector< pbes_equation > & mcrl2::pbes_system::pbes::equations ( ) const

inline

Returns the equations.

Returns: The equations.

Definition at line 160 of file pbes.h.

◆ global_variables() [1/2]

std::set< data::variable > & mcrl2::pbes_system::pbes::global_variables ( )

inline

Returns the declared free variables of the pbes.

Returns: The declared free variables of the pbes.

Definition at line 181 of file pbes.h.

◆ global_variables() [2/2]

const std::set< data::variable > & mcrl2::pbes_system::pbes::global_variables ( ) const

inline

Returns the declared free variables of the pbes.

Returns: The declared free variables of the pbes.

Definition at line 174 of file pbes.h.

◆ initial_state() [1/2]

propositional_variable_instantiation & mcrl2::pbes_system::pbes::initial_state ( )

inline

Returns the initial state.

Returns: The initial state.

Definition at line 195 of file pbes.h.

◆ initial_state() [2/2]

const propositional_variable_instantiation & mcrl2::pbes_system::pbes::initial_state ( ) const

inline

Returns the initial state.

Returns: The initial state.

Definition at line 188 of file pbes.h.

◆ is_closed()

bool mcrl2::pbes_system::pbes::is_closed ( ) const

inline

True if the pbes is closed.

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

Definition at line 239 of file pbes.h.

◆ is_declared_in()

template<typename Iter >

bool mcrl2::pbes_system::pbes::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 92 of file pbes.h.

◆ is_well_typed()

bool mcrl2::pbes_system::pbes::is_well_typed ( ) const

inline

Checks if the PBES 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 261 of file pbes.h.

◆ occurring_variable_instantiations()

std::set< propositional_variable_instantiation > mcrl2::pbes_system::pbes::occurring_variable_instantiations ( ) const

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

Returns: The occurring propositional variable instantiations of the pbes

Definition at line 107 of file pbes.cpp.

◆ occurring_variables()

std::set< propositional_variable > mcrl2::pbes_system::pbes::occurring_variables ( ) const

inline

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

Returns: The occurring propositional variable declarations of the pbes

Definition at line 221 of file pbes.h.

Member Data Documentation

◆ m_data

data::data_specification mcrl2::pbes_system::pbes::m_data

protected

The data specification.

Definition at line 60 of file pbes.h.

◆ m_equations

std::vector<pbes_equation> mcrl2::pbes_system::pbes::m_equations

protected

The sequence of pbes equations.

Definition at line 63 of file pbes.h.

◆ m_global_variables

std::set<data::variable> mcrl2::pbes_system::pbes::m_global_variables

protected

The set of global variables.

Definition at line 66 of file pbes.h.

◆ m_initial_state

propositional_variable_instantiation mcrl2::pbes_system::pbes::m_initial_state

protected

The initial state.

Definition at line 69 of file pbes.h.

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

pbes/include/mcrl2/pbes/pbes.h
pbes/source/pbes.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ equation_type

Constructor & Destructor Documentation

◆ pbes() [1/3]

◆ pbes() [2/3]

◆ pbes() [3/3]

Member Function Documentation

◆ binding_variables()

◆ compute_declared_variables()

◆ data() [1/2]

◆ data() [2/2]

◆ 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()

Member Data Documentation

◆ m_data

◆ m_equations

◆ m_global_variables

◆ m_initial_state