Function object for applying a substitution to LPS data types. More...

#include <is_well_typed.h>

Public Member Functions
	lps_well_typed_checker ()

bool	check_time (const data::data_expression &t, const std::string &type) const
	Checks if the sort of t has type real.

bool	check_condition (const data::data_expression &t, const std::string &type) const
	Checks if the sort of t has type bool.

bool	check_assignments (const data::assignment_list &l, const std::string &type) const
	Checks if the assignments are well typed and have unique left hand sides.

template<typename Container >
bool	is_well_typed_container (const Container &c) const
	Checks well typedness of the elements of a container.

bool	is_well_typed (const data::sort_expression &d) const
	Checks well typedness of a sort expression.

bool	is_well_typed (const data::variable &d) const
	Checks well typedness of a variable.

bool	is_well_typed (const data::data_expression &d) const
	Checks well typedness of a data expression.

bool	is_well_typed (const data::assignment &a) const
	Traverses an assignment.

bool	is_well_typed (const process::action_label &d) const
	Traverses an action label.

bool	is_well_typed (const process::action &a) const
	Traverses an action.

bool	is_well_typed (const deadlock &d) const
	Checks well typedness of a deadlock.

bool	is_well_typed (const multi_action &a) const
	Checks well typedness of a multi-action.

bool	is_well_typed (const action_summand &s) const
	Checks well typedness of a summand.

bool	is_well_typed (const deadlock_summand &s) const
	Checks well typedness of a summand.

template<typename ActionSummand >
bool	is_well_typed (const linear_process_base< ActionSummand > &p) const
	Checks well typedness of a linear process.

template<typename LinearProcess , typename InitialProcessExpression >
bool	is_well_typed (const specification_base< LinearProcess, InitialProcessExpression > &spec, const std::set< data::variable > &free_variables) const
	Checks well typedness of a linear process specification.

bool	is_well_typed (const specification &spec) const

bool	is_well_typed (const stochastic_specification &spec) const

template<typename Term >
bool	operator() (const Term &t) const

Public Attributes
bool	result

std::ostringstream	error

Detailed Description

Function object for applying a substitution to LPS data types.

Definition at line 28 of file is_well_typed.h.

Constructor & Destructor Documentation

◆ lps_well_typed_checker()

mcrl2::lps::detail::lps_well_typed_checker::lps_well_typed_checker ( )

inline

Definition at line 36 of file is_well_typed.h.

Member Function Documentation

◆ check_assignments()

bool mcrl2::lps::detail::lps_well_typed_checker::check_assignments	(	const data::assignment_list &	l,
		const std::string &	type
	)		const

inline

Checks if the assignments are well typed and have unique left hand sides.

Definition at line 63 of file is_well_typed.h.

◆ check_condition()

bool mcrl2::lps::detail::lps_well_typed_checker::check_condition	(	const data::data_expression &	t,
		const std::string &	type
	)		const

inline

Checks if the sort of t has type bool.

Definition at line 52 of file is_well_typed.h.

◆ check_time()

bool mcrl2::lps::detail::lps_well_typed_checker::check_time	(	const data::data_expression &	t,
		const std::string &	type
	)		const

inline

Checks if the sort of t has type real.

Definition at line 41 of file is_well_typed.h.

◆ is_well_typed() [1/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const action_summand & s ) const

inline

Checks well typedness of a summand.

Parameters

s	An action summand

Definition at line 182 of file is_well_typed.h.

◆ is_well_typed() [2/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const data::assignment & a ) const

inline

Traverses an assignment.

Parameters

a	An assignment

Definition at line 123 of file is_well_typed.h.

◆ is_well_typed() [3/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const data::data_expression & d ) const

inline

Checks well typedness of a data expression.

Parameters

d	A data expression

Definition at line 115 of file is_well_typed.h.

◆ is_well_typed() [4/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const data::sort_expression & d ) const

inline

Checks well typedness of a sort expression.

Parameters

d	A sort expression.

Definition at line 99 of file is_well_typed.h.

◆ is_well_typed() [5/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const data::variable & d ) const

inline

Checks well typedness of a variable.

Parameters

d	A variable.

Definition at line 107 of file is_well_typed.h.

◆ is_well_typed() [6/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const deadlock & d ) const

inline

Checks well typedness of a deadlock.

Parameters

d	A deadlock

Returns

Returns true if

the (optional) time has sort Real

Definition at line 156 of file is_well_typed.h.

◆ is_well_typed() [7/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const deadlock_summand & s ) const

inline

Checks well typedness of a summand.

Parameters

s A summand

Definition at line 206 of file is_well_typed.h.

◆ is_well_typed() [8/14]

template<typename ActionSummand >

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const linear_process_base< ActionSummand > & p ) const

inline

Checks well typedness of a linear process.

Parameters

p	A linear_process

Returns

True if

the process parameters have unique names
process parameters and summation variables have different names
the left hand sides of the assignments of summands are contained in the process parameters
the summands are well typed

Definition at line 229 of file is_well_typed.h.

◆ is_well_typed() [9/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const multi_action & a ) const

inline

Checks well typedness of a multi-action.

Parameters

a	A multi-action

Returns

Returns true if

the (optional) time has sort Real

Definition at line 171 of file is_well_typed.h.

◆ is_well_typed() [10/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const process::action & a ) const

inline

Traverses an action.

Parameters

a	An action.

Definition at line 144 of file is_well_typed.h.

◆ is_well_typed() [11/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const process::action_label & d ) const

inline

Traverses an action label.

Parameters

d	An action label.

Definition at line 136 of file is_well_typed.h.

◆ is_well_typed() [12/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const specification & spec ) const

inline

Definition at line 366 of file is_well_typed.h.

◆ is_well_typed() [13/14]

template<typename LinearProcess , typename InitialProcessExpression >

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed	(	const specification_base< LinearProcess, InitialProcessExpression > &	spec,
		const std::set< data::variable > &	free_variables
	)		const

inline

Checks well typedness of a linear process specification.

Parameters

spec	A linear process specification.
free_variables	Free variables that can be used.

Returns

True if

the sorts occurring in the summation variables are declared in the data specification
the sorts occurring in the process parameters are declared in the data specification
the sorts occurring in the free variables are declared in the data specification
the sorts occurring in the action labels are declared in the data specification
the action labels occurring in the process are contained in action_labels()
the process is well typed
the data specification is well typed
the initial process is well typed
the free variables occurring in the linear process are declared in the global variable specification
the free variables occurring in the initial process are declared in the global variable specification
the global variables have unique names

Definition at line 293 of file is_well_typed.h.

◆ is_well_typed() [14/14]

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed ( const stochastic_specification & spec ) const

inline

Definition at line 372 of file is_well_typed.h.

◆ is_well_typed_container()

template<typename Container >

bool mcrl2::lps::detail::lps_well_typed_checker::is_well_typed_container ( const Container & c ) const

inline

Checks well typedness of the elements of a container.

Definition at line 85 of file is_well_typed.h.

◆ operator()()

template<typename Term >

bool mcrl2::lps::detail::lps_well_typed_checker::operator() ( const Term & t ) const

inline

Definition at line 379 of file is_well_typed.h.

Member Data Documentation

◆ error

std::ostringstream mcrl2::lps::detail::lps_well_typed_checker::error

mutable

Definition at line 34 of file is_well_typed.h.

◆ result

bool mcrl2::lps::detail::lps_well_typed_checker::result

Definition at line 31 of file is_well_typed.h.

The documentation for this struct was generated from the following file:

lps/include/mcrl2/lps/is_well_typed.h

Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ lps_well_typed_checker()

Member Function Documentation

◆ check_assignments()

◆ check_condition()

◆ check_time()

◆ is_well_typed() [1/14]

◆ is_well_typed() [2/14]

◆ is_well_typed() [3/14]

◆ is_well_typed() [4/14]

◆ is_well_typed() [5/14]

◆ is_well_typed() [6/14]

◆ is_well_typed() [7/14]

◆ is_well_typed() [8/14]

◆ is_well_typed() [9/14]

◆ is_well_typed() [10/14]

◆ is_well_typed() [11/14]

◆ is_well_typed() [12/14]

◆ is_well_typed() [13/14]

◆ is_well_typed() [14/14]

◆ is_well_typed_container()

◆ operator()()

Member Data Documentation

◆ error

◆ result