Converts a process expression into linear process format. Use the convert member functions for this. More...

#include <linear_process_conversion_traverser.h>

Inheritance diagram for mcrl2::process::detail::linear_process_conversion_traverser:

Classes
struct	non_linear_process
	Exception that is thrown to denote that the process is not linear. More...

Public Types
using	super = process_expression_traverser< linear_process_conversion_traverser >

Public Types inherited from mcrl2::process::add_traverser_process_expressions< Traverser, Derived >
using	super = Traverser< Derived >

Public Member Functions
void	clear_summand ()
	Clears the current summand.

void	add_summand ()
	Adds a summand to the result.

void	leave (const delta &)
	Visit delta node.

void	leave (const process::tau &)
	Visit tau node.

void	leave (const process::action &x)
	Visit action node.

void	leave (const process::sum &x)
	Visit sum node.

void	leave (const process::block &x)
	Visit block node.

void	leave (const process::hide &x)
	Visit hide node.

void	leave (const process::rename &x)
	Visit rename node.

void	leave (const process::comm &x)
	Visit comm node.

void	leave (const process::allow &x)
	Visit allow node.

void	apply (const process::sync &x)
	Visit sync node.

void	leave (const process::at &x)
	Visit at node.

void	apply (const process::seq &x)
	Visit seq node.

void	leave (const process::if_then &x)
	Visit if_then node.

void	leave (const process::if_then_else &x)
	Visit if_then_else node.

void	leave (const process::bounded_init &x)
	Visit bounded_init node.

void	leave (const process::merge &x)
	Visit merge node.

void	leave (const process::left_merge &x)
	Visit left_merge node.

void	apply (const process::choice &x)
	Visit choice node.

void	convert (const process_equation &)
	Converts a process equation.

lps::specification	convert (const process_specification &p)
	Converts a process_specification into a specification. Throws `non_linear_process` if a non-linear sub-expression is encountered. Throws `mcrl2::runtime_error` in the following cases:

Public Member Functions inherited from mcrl2::process::add_traverser_process_expressions< Traverser, Derived >
void	apply (const process::process_specification &x)

void	apply (const process::process_equation &x)

void	apply (const process::action &x)

void	apply (const process::process_instance &x)

void	apply (const process::process_instance_assignment &x)

void	apply (const process::delta &x)

void	apply (const process::tau &x)

void	apply (const process::sum &x)

void	apply (const process::block &x)

void	apply (const process::hide &x)

void	apply (const process::rename &x)

void	apply (const process::comm &x)

void	apply (const process::allow &x)

void	apply (const process::sync &x)

void	apply (const process::at &x)

void	apply (const process::seq &x)

void	apply (const process::if_then &x)

void	apply (const process::if_then_else &x)

void	apply (const process::bounded_init &x)

void	apply (const process::merge &x)

void	apply (const process::left_merge &x)

void	apply (const process::choice &x)

void	apply (const process::stochastic_operator &x)

void	apply (const process::untyped_process_assignment &x)

void	apply (const process::process_expression &x)

Public Attributes
lps::action_summand_vector	m_action_summands
	The result of the conversion.

lps::deadlock_summand_vector	m_deadlock_summands
	The result of the conversion.

process_equation	m_equation
	The process equation that is checked.

data::variable_list	m_sum_variables
	Contains intermediary results.

data::assignment_list	m_next_state
	Contains intermediary results.

lps::multi_action	m_multi_action
	Contains intermediary results.

lps::deadlock	m_deadlock
	Contains intermediary results.

bool	m_deadlock_changed = false
	True if m_deadlock was changed.

bool	m_multi_action_changed = false
	True if m_multi_action was changed.

bool	m_next_state_changed = false
	True if m_next_state was changed.

data::data_expression	m_condition
	Contains intermediary results.

Detailed Description

Converts a process expression into linear process format. Use the convert member functions for this.

Definition at line 25 of file linear_process_conversion_traverser.h.

Member Typedef Documentation

◆ super

using mcrl2::process::detail::linear_process_conversion_traverser::super = process_expression_traverser<linear_process_conversion_traverser>

Definition at line 27 of file linear_process_conversion_traverser.h.

Member Function Documentation

◆ add_summand()

void mcrl2::process::detail::linear_process_conversion_traverser::add_summand ( )

inline

Adds a summand to the result.

Definition at line 89 of file linear_process_conversion_traverser.h.

◆ apply() [1/3]

void mcrl2::process::detail::linear_process_conversion_traverser::apply ( const process::choice & x )

inline

Visit choice node.

Parameters

x	A process expression

Definition at line 290 of file linear_process_conversion_traverser.h.

◆ apply() [2/3]

void mcrl2::process::detail::linear_process_conversion_traverser::apply ( const process::seq & x )

inline

Visit seq node.

Parameters

x	A process expression

Definition at line 214 of file linear_process_conversion_traverser.h.

◆ apply() [3/3]

void mcrl2::process::detail::linear_process_conversion_traverser::apply ( const process::sync & x )

inline

Visit sync node.

Parameters

x	A process expression

Definition at line 185 of file linear_process_conversion_traverser.h.

◆ clear_summand()

void mcrl2::process::detail::linear_process_conversion_traverser::clear_summand ( )

inline

Clears the current summand.

Definition at line 76 of file linear_process_conversion_traverser.h.

◆ convert() [1/2]

void mcrl2::process::detail::linear_process_conversion_traverser::convert ( const process_equation & )

inline

Converts a process equation.

Definition at line 305 of file linear_process_conversion_traverser.h.

◆ convert() [2/2]

lps::specification mcrl2::process::detail::linear_process_conversion_traverser::convert ( const process_specification & p )

inline

Converts a process_specification into a specification. Throws non_linear_process if a non-linear sub-expression is encountered. Throws mcrl2::runtime_error in the following cases:

The number of equations is not equal to one
The initial process is not a process instance, or it does not match with the equation
A sequential process is found with a right hand side that is not a process instance, or it doesn't match the equation
Parameters

p A process specification

Returns
The converted specification

Definition at line 321 of file linear_process_conversion_traverser.h.

◆ leave() [1/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const delta & )

inline

Visit delta node.

Parameters

x	A process expression

Definition at line 114 of file linear_process_conversion_traverser.h.

◆ leave() [2/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::action & x )

inline

Visit action node.

Parameters

x	A process expression

Definition at line 132 of file linear_process_conversion_traverser.h.

◆ leave() [3/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::allow & x )

inline

Visit allow node.

Parameters

x	A process expression

Definition at line 178 of file linear_process_conversion_traverser.h.

◆ leave() [4/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::at & x )

inline

Visit at node.

Parameters

x	A process expression

Definition at line 198 of file linear_process_conversion_traverser.h.

◆ leave() [5/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::block & x )

inline

Visit block node.

Parameters

x	A process expression

Definition at line 150 of file linear_process_conversion_traverser.h.

◆ leave() [6/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::bounded_init & x )

inline

Visit bounded_init node.

Parameters

x	A process expression

Definition at line 269 of file linear_process_conversion_traverser.h.

◆ leave() [7/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::comm & x )

inline

Visit comm node.

Parameters

x	A process expression

Definition at line 171 of file linear_process_conversion_traverser.h.

◆ leave() [8/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::hide & x )

inline

Visit hide node.

Parameters

x	A process expression

Definition at line 157 of file linear_process_conversion_traverser.h.

◆ leave() [9/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::if_then & x )

inline

Visit if_then node.

Parameters

x	A process expression

Definition at line 254 of file linear_process_conversion_traverser.h.

◆ leave() [10/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::if_then_else & x )

inline

Visit if_then_else node.

Parameters

x	A process expression

Definition at line 262 of file linear_process_conversion_traverser.h.

◆ leave() [11/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::left_merge & x )

inline

Visit left_merge node.

Parameters

x	A process expression

Definition at line 283 of file linear_process_conversion_traverser.h.

◆ leave() [12/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::merge & x )

inline

Visit merge node.

Parameters

x	A process expression

Definition at line 276 of file linear_process_conversion_traverser.h.

◆ leave() [13/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::rename & x )

inline

Visit rename node.

Parameters

x	A process expression

Definition at line 164 of file linear_process_conversion_traverser.h.

◆ leave() [14/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::sum & x )

inline

Visit sum node.

Parameters

x	A process expression

Definition at line 142 of file linear_process_conversion_traverser.h.

◆ leave() [15/15]

void mcrl2::process::detail::linear_process_conversion_traverser::leave ( const process::tau & )

inline

Visit tau node.

Parameters

x	A process expression

Definition at line 123 of file linear_process_conversion_traverser.h.

Member Data Documentation

◆ m_action_summands

lps::action_summand_vector mcrl2::process::detail::linear_process_conversion_traverser::m_action_summands

The result of the conversion.

Definition at line 33 of file linear_process_conversion_traverser.h.

◆ m_condition

data::data_expression mcrl2::process::detail::linear_process_conversion_traverser::m_condition

Contains intermediary results.

Definition at line 63 of file linear_process_conversion_traverser.h.

◆ m_deadlock

lps::deadlock mcrl2::process::detail::linear_process_conversion_traverser::m_deadlock

Contains intermediary results.

Definition at line 51 of file linear_process_conversion_traverser.h.

◆ m_deadlock_changed

bool mcrl2::process::detail::linear_process_conversion_traverser::m_deadlock_changed = false

True if m_deadlock was changed.

Definition at line 54 of file linear_process_conversion_traverser.h.

◆ m_deadlock_summands

lps::deadlock_summand_vector mcrl2::process::detail::linear_process_conversion_traverser::m_deadlock_summands

The result of the conversion.

Definition at line 36 of file linear_process_conversion_traverser.h.

◆ m_equation

process_equation mcrl2::process::detail::linear_process_conversion_traverser::m_equation

The process equation that is checked.

Definition at line 39 of file linear_process_conversion_traverser.h.

◆ m_multi_action

lps::multi_action mcrl2::process::detail::linear_process_conversion_traverser::m_multi_action

Contains intermediary results.

Definition at line 48 of file linear_process_conversion_traverser.h.

◆ m_multi_action_changed

bool mcrl2::process::detail::linear_process_conversion_traverser::m_multi_action_changed = false

True if m_multi_action was changed.

Definition at line 57 of file linear_process_conversion_traverser.h.

◆ m_next_state

data::assignment_list mcrl2::process::detail::linear_process_conversion_traverser::m_next_state

Contains intermediary results.

Definition at line 45 of file linear_process_conversion_traverser.h.

◆ m_next_state_changed

bool mcrl2::process::detail::linear_process_conversion_traverser::m_next_state_changed = false

True if m_next_state was changed.

Definition at line 60 of file linear_process_conversion_traverser.h.

◆ m_sum_variables

data::variable_list mcrl2::process::detail::linear_process_conversion_traverser::m_sum_variables

Contains intermediary results.

Definition at line 42 of file linear_process_conversion_traverser.h.

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

lps/include/mcrl2/lps/detail/linear_process_conversion_traverser.h

Classes

Public Types

Public Member Functions

Public Attributes

Detailed Description

Member Typedef Documentation

◆ super

Member Function Documentation

◆ add_summand()

◆ apply() [1/3]

◆ apply() [2/3]

◆ apply() [3/3]

◆ clear_summand()

◆ convert() [1/2]

◆ convert() [2/2]

◆ leave() [1/15]

◆ leave() [2/15]

◆ leave() [3/15]

◆ leave() [4/15]

◆ leave() [5/15]

◆ leave() [6/15]

◆ leave() [7/15]

◆ leave() [8/15]

◆ leave() [9/15]

◆ leave() [10/15]

◆ leave() [11/15]

◆ leave() [12/15]

◆ leave() [13/15]

◆ leave() [14/15]

◆ leave() [15/15]

Member Data Documentation

◆ m_action_summands

◆ m_condition

◆ m_deadlock

◆ m_deadlock_changed

◆ m_deadlock_summands

◆ m_equation

◆ m_multi_action

◆ m_multi_action_changed

◆ m_next_state

◆ m_next_state_changed

◆ m_sum_variables