Classes
class	comm_entry

class	enumeratedtype

class	enumtype

struct	make_substitution

class	process_pid_pair

class	stacklisttype

class	stackoperations

struct	tuple_list

Public Member Functions
	specification_basic_type (const specification_basic_type &)=delete

specification_basic_type &	operator= (const specification_basic_type &)=delete

	specification_basic_type (const process::action_label_list &as, const std::vector< process_equation > &ps, const variable_list &idvs, const data_specification &ds, const std::set< data::variable > &glob_vars, const t_lin_options &opt, const process_specification &procspec)

	~specification_basic_type ()

process_identifier	storeinit (const process_expression &init)

variable_list	SieveProcDataVarsSummands (const std::set< variable > &vars, const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands, const variable_list &parameters)

variable_list	SieveProcDataVarsAssignments (const std::set< variable > &vars, const data_expression_list &initial_state_expressions)

void	transform (const process_identifier &init, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, variable_list &parameters, data_expression_list &initial_state, stochastic_distribution &initial_stochastic_distribution)

Public Attributes
process::action_label_list	acts

std::set< variable >	global_variables

variable_list	initdatavars

data_specification	data

Private Types
enum	variableposition { first , later }

enum	state { alt_state , sum_state , seq_state , name_state , multiaction_state }

enum	terminationstatus { terminating , infinite }

Private Member Functions
data_expression	real_times_optimized (const data_expression &r1, const data_expression &r2)

process_expression	delta_at_zero (void)

bool	isDeltaAtZero (const process_expression &t)

template<class Expression , class Substitution >
Expression	replace_variables_capture_avoiding_alt (const Expression &e, Substitution &sigma)

void	detail_check_objectdata (const aterm &o) const

objectdatatype &	objectIndex (const aterm &o)

const objectdatatype &	objectIndex (const aterm &o) const

void	addString (const identifier_string &str)

process_expression	action_list_to_process (const action_list &ma)

action_list	to_action_list (const process_expression &p)

process::action_label_list	getnames (const process_expression &multiAction)

variable_list	make_parameters_rec (const data_expression_list &l, std::set< variable > &occurs_set)

variable_list	getparameters_rec (const process_expression &multiAction, std::set< variable > &occurs_set)

variable_list	getparameters (const process_expression &multiAction)

data_expression_list	getarguments (const action_list &multiAction)

action_list	makemultiaction (const process::action_label_list &actionIds, const data_expression_list &args)

objectdatatype &	addMultiAction (const process_expression &multiAction, bool &isnew)

const std::set< variable > &	get_free_variables (objectdatatype &object)

void	insertvariable (const variable &var, const bool mustbenew)

void	insertvariables (const variable_list &vars, const bool mustbenew)

template<class SUBSTITUTION >
std::set< data::variable >	sigma_variables (const SUBSTITUTION &sigma)

std::size_t	upperpowerof2 (std::size_t i)

data_expression	RewriteTerm (const data_expression &t)

data_expression_list	RewriteTermList (const data_expression_list &t)

assignment_list	rewrite_assignments (const assignment_list &t)

action	RewriteAction (const action &t)

process_instance_assignment	RewriteProcess (const process_instance_assignment &t)

process_expression	RewriteMultAct (const process_expression &t)

process_expression	pCRLrewrite (const process_expression &t)

objectdatatype &	insertAction (const action_label &actionId)

void	storeact (const process::action_label_list &acts)

objectdatatype &	insert_process_declaration (const process_identifier &procId, const variable_list &parameters, const process_expression &body, processstatustype s, const bool canterminate, const bool containstime)

void	storeprocs (const std::vector< process_equation > &procs)

bool	searchProcDeclaration (const variable_list &parameters, const process_expression &body, const processstatustype s, const bool canterminate, const bool containstime, process_identifier &p)

bool	actioncompare (const action_label &a1, const action_label &a2)

action_list	linInsertActionInMultiActionList (const action &act, action_list multiAction)

action_list	linMergeMultiActionList (const action_list &ma1, const action_list &ma2)

action_list	linMergeMultiActionListProcess (const process_expression &ma1, const process_expression &ma2)

processstatustype	determine_process_statusterm (const process_expression &body, const processstatustype status)

void	determine_process_status (const process_identifier &procDecl, const processstatustype status)

void	collectPcrlProcesses_term (const process_expression &body, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)

void	collectPcrlProcesses (const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)

void	collectPcrlProcesses (const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses)

bool	occursinterm (const variable &var, const data_expression &t) const

void	filter_vars_by_term (const data_expression &t, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)

bool	occursintermlist (const variable &var, const data_expression_list &r) const

bool	occursintermlist (const variable &var, const assignment_list &r, const process_identifier &proc_name) const

template<typename Iterator >
void	filter_vars_by_termlist (Iterator begin, const Iterator &end, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)

void	filter_vars_by_multiaction (const action_list &multiaction, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)

void	filter_vars_by_assignmentlist (const assignment_list &assignments, const variable_list &parameters, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)

bool	occursinpCRLterm (const variable &var, const process_expression &p, const bool strict)

template<class MutableSubstitution >
void	alphaconvertprocess (variable_list &sumvars, MutableSubstitution &sigma, const process_expression &p)

template<class MutableSubstitution >
void	alphaconvert (variable_list &sumvars, MutableSubstitution &sigma, const variable_list &occurvars, const data_expression_list &occurterms)

void	find_free_variables_process (const process_expression &p, std::set< variable > &free_variables_in_p)

std::set< variable >	find_free_variables_process (const process_expression &p)

assignment_list	filter_assignments (const assignment_list &assignments, const variable_list &parameters)

template<class Substitution >
assignment_list	substitute_assignmentlist (const assignment_list &assignments, const variable_list &parameters, const bool replacelhs, const bool replacerhs, Substitution &sigma)

assignment_list	sort_assignments (const assignment_list &ass, const variable_list &parameters)

bool	check_valid_process_instance_assignment (const process_identifier &id, const assignment_list &assignments)

template<class Substitution >
process_expression	substitute_pCRLproc (const process_expression &p, Substitution &sigma)

process_instance_assignment	transform_process_instance_to_process_instance_assignment (const process_instance &procId, const std::set< variable > &bound_variables=std::set< variable >())

variable_list	parameters_that_occur_in_body (const variable_list &parameters, const process_expression &body)

process_identifier	newprocess (const variable_list &parameters, const process_expression &body, const processstatustype ps, const bool canterminate, const bool containstime)

process_expression	wraptime (const process_expression &body, const data_expression &time, const variable_list &freevars)

variable	get_fresh_variable (const std::string &s, const sort_expression &sort, const int reuse_index=-1)

variable_list	make_pars (const sort_expression_list &sortlist)

process_expression	distributeActionOverConditions (const process_expression &act, const data_expression &condition, const process_expression &restterm, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)

assignment_list	parameters_to_assignment_list (const variable_list &parameters, const std::set< variable > &variables_bound_in_sum)

process_expression	bodytovarheadGNF (const process_expression &body, const state s, const variable_list &freevars, const variableposition v, const std::set< variable > &variables_bound_in_sum)

void	procstovarheadGNF (const std::vector< process_identifier > &procs)

process_expression	putbehind (const process_expression &body1, const process_expression &body2)

process_expression	distribute_condition (const process_expression &body1, const data_expression &condition)

process_expression	enumerate_distribution_and_sums (const variable_list &sumvars, const variable_list &stochvars, const data_expression &distribution, const process_expression &body)

process_expression	distribute_sum_over_a_stochastic_operator (const variable_list &sumvars, const variable_list &stochastic_variables, const data_expression &distribution, const process_expression &body)

process_expression	distribute_sum (const variable_list &sumvars, const process_expression &body1)

int	match_sequence (const std::vector< process_instance_assignment > &s1, const std::vector< process_instance_assignment > &s2, const bool regular2)

bool	exists_variable_for_sequence (const std::vector< process_instance_assignment > &process_names, process_identifier &result)

void	extract_names (const process_expression &sequence, std::vector< process_instance_assignment > &result)

variable_list	parscollect (const process_expression &oldbody, process_expression &newbody)

assignment_list	argscollect_regular (const process_expression &t, const variable_list &vl, const std::set< variable > &variables_bound_in_sum)

assignment_list	argscollect_regular2 (const process_expression &t, variable_list &vl)

process_expression	cut_off_unreachable_tail (const process_expression &t)

process_expression	create_regular_invocation (process_expression sequence, std::vector< process_identifier > &todo, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)

process_expression	to_regular_form (const process_expression &t, std::vector< process_identifier > &todo, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)

process_expression	distributeTime (const process_expression &body, const data_expression &time, const variable_list &freevars, data_expression &timecondition)

process_expression	procstorealGNFbody (const process_expression &body, variableposition v, std::vector< process_identifier > &todo, const bool regular, processstatustype mode, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)

void	procstorealGNFrec (const process_identifier &procIdDecl, const variableposition v, std::vector< process_identifier > &todo, const bool regular)

void	procstorealGNF (const process_identifier &procsIdDecl, const bool regular)

void	make_pCRL_procs (const process_identifier &id, std::set< process_identifier > &reachable_process_identifiers)

void	make_pCRL_procs (const process_expression &t, std::set< process_identifier > &reachable_process_identifiers)

process_identifier	get_last (const process_identifier &id, const std::map< process_identifier, process_identifier > &identifier_identifier_map)

void	set_proc_identifier_map (std::map< process_identifier, process_identifier > &identifier_identifier_map, const process_identifier &id1_, const process_identifier &id2_, const process_identifier &initial_process)

void	complete_proc_identifier_map (std::map< process_identifier, process_identifier > &identifier_identifier_map)

std::set< process_identifier >	minimize_set_of_reachable_process_identifiers (const std::set< process_identifier > &reachable_process_identifiers, const process_identifier &initial_process)

std::set< process_identifier >	remove_stochastic_operators_from_front (const std::set< process_identifier > &reachable_process_identifiers, process_identifier &initial_process_id, stochastic_distribution &initial_stochastic_distribution)

bool	alreadypresent (variable &var, const variable_list &vl)

variable_list	joinparameters (const variable_list &par1, const variable_list &par2)

variable_list	collectparameterlist (const std::set< process_identifier > &pCRLprocs)

void	declare_control_state (const std::set< process_identifier > &pCRLprocs)

bool	is_global_variable (const data_expression &d) const

data_expression	getvar (const variable &var, const stacklisttype &stack)

assignment_list	processencoding (std::size_t i, const assignment_list &t1, const stacklisttype &stack)

data_expression_list	processencoding (std::size_t i, const data_expression_list &t1, const stacklisttype &stack)

data_expression	correctstatecond (const process_identifier &procId, const std::set< process_identifier > &pCRLproc, const stacklisttype &stack, int regular)

data_expression	adapt_term_to_stack (const data_expression &t, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)

template<typename Iterator >
data_expression_vector	adapt_termlist_to_stack (Iterator begin, const Iterator &end, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)

action_list	adapt_multiaction_to_stack_rec (const action_list &multiAction, const stacklisttype &stack, const variable_list &vars)

action_list	adapt_multiaction_to_stack (const action_list &multiAction, const stacklisttype &stack, const variable_list &vars)

data_expression	representative_generator_internal (const sort_expression &s, const bool allow_dont_care_var=true)

data_expression	find_ (const variable &s, const assignment_list &args, const stacklisttype &stack, const variable_list &vars, const std::set< variable > &free_variables_in_body, const variable_list &stochastic_variables)

data_expression_list	findarguments (const variable_list &pars, const variable_list &parlist, const assignment_list &args, const data_expression_list &t2, const stacklisttype &stack, const variable_list &vars, const std::set< variable > &free_variables_in_body, const variable_list &stochastic_variables)

assignment_list	find_dummy_arguments (const variable_list &parlist, const assignment_list &args, const std::set< variable > &free_variables_in_body, const variable_list &stochastic_variables)

assignment_list	push_regular (const process_identifier &procId, const assignment_list &args, const stacklisttype &stack, const std::set< process_identifier > &pCRLprocs, bool singlestate, const variable_list &stochastic_variables)

assignment_list	make_procargs_regular (const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const bool singlestate, const variable_list &stochastic_variables)

data_expression	push_stack (const process_identifier &procId, const assignment_list &args, const data_expression_list &t2, const stacklisttype &stack, const std::set< process_identifier > &pCRLprocs, const variable_list &vars, const variable_list &stochastic_variables)

data_expression	make_procargs_stack (const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const variable_list &vars, const variable_list &stochastic_variables)

assignment_list	make_procargs (const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const variable_list &vars, const bool regular, const bool singlestate, const variable_list &stochastic_variables)

bool	occursin (const variable &name, const variable_list &pars)

data_expression_list	pushdummy_regular_data_expressions (const variable_list &pars, const stacklisttype &stack)

assignment_list	pushdummy_regular (const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)

data_expression_list	pushdummyrec_stack (const variable_list &totalpars, const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)

data_expression_list	pushdummy_stack (const variable_list &parameters, const stacklisttype &stack, const variable_list &stochastic_variables)

data_expression_list	make_initialstate (const process_identifier &initialProcId, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const bool regular, const bool singlecontrolstate, const stochastic_distribution &initial_stochastic_distribution)

assignment_list	dummyparameterlist (const stacklisttype &stack, const bool singlestate)

void	insert_summand (stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const variable_list &sumvars, const data_expression &condition, const action_list &multiAction, const data_expression &actTime, const stochastic_distribution &distribution, const assignment_list &procargs, const bool has_time, const bool is_deadlock_summand)

void	add_summands (const process_identifier &procId, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, process_expression summandterm, const std::set< process_identifier > &pCRLprocs, const stacklisttype &stack, const bool regular, const bool singlestate, const variable_list &process_parameters)

void	collectsumlistterm (const process_identifier &procId, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_expression &body, const variable_list &pars, const stacklisttype &stack, const bool regular, const bool singlestate, const std::set< process_identifier > &pCRLprocs)

void	collectsumlist (stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const std::set< process_identifier > &pCRLprocs, const variable_list &pars, const stacklisttype &stack, bool regular, bool singlestate)

std::size_t	create_enumeratedtype (const std::size_t n)

data::function_symbol	find_case_function (std::size_t index, const sort_expression &sort)

void	define_equations_for_case_function (const std::size_t index, const data::function_symbol &functionname, const sort_expression &sort)

void	create_case_function_on_enumeratedtype (const sort_expression &sort, const std::size_t enumeratedtype_index)

bool	mergeoccursin (variable &var, const variable_list &v, variable_list &matchinglist, variable_list &pars, data_expression_list &args, const variable_list &process_parameters)

data_expression_list	extend (const data_expression &c, const data_expression_list &cl)

data_expression	variables_are_equal_to_default_values (const variable_list &vl)

data_expression_list	extend_conditions (const variable &var, const data_expression_list &conditionlist)

data_expression	transform_matching_list (const variable_list &matchinglist)

data_expression_list	addcondition (const variable_list &matchinglist, const data_expression_list &conditionlist)

variable_list	merge_var (const variable_list &v1, const variable_list &v2, std::vector< variable_list > &renamings_pars, std::vector< data_expression_list > &renamings_args, data_expression_list &conditionlist, const variable_list &process_parameters)

variable_list	make_binary_sums (std::size_t n, const sort_expression &enumtypename, data_expression &condition, const variable_list &tail)

data_expression	construct_binary_case_tree_rec (std::size_t n, const variable_list &sums, data_expression_list &terms, const sort_expression &termsort, const enumtype &e)

template<class T >
bool	all_equal (const atermpp::term_list< T > &l)

data_expression	construct_binary_case_tree (std::size_t n, const variable_list &sums, data_expression_list terms, const sort_expression &termsort, const enumtype &e)

bool	summandsCanBeClustered (const stochastic_action_summand &summand1, const stochastic_action_summand &summand2)

data_expression	getRHSassignment (const variable &var, const assignment_list &as)

stochastic_action_summand	collect_sum_arg_arg_cond (const enumtype &e, std::size_t n, const stochastic_action_summand_vector &action_summands, const variable_list &parameters)

deadlock_summand	collect_sum_arg_arg_cond (const enumtype &e, std::size_t n, const deadlock_summand_vector &deadlock_summands, const variable_list &parameters)

sort_expression_list	getActionSorts (const action_list &actionlist)

void	cluster_actions (stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const variable_list &pars)

void	generateLPEpCRL (stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_identifier &procId, const bool containstime, const bool regular, variable_list &parameters, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution)

action_list	hide_ (const identifier_string_list &hidelist, const action_list &multiaction)

void	hidecomposition (const identifier_string_list &hidelist, stochastic_action_summand_vector &action_summands)

bool	implies_condition (const data_expression &c1, const data_expression &c2)

void	insert_timed_delta_summand (const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const deadlock_summand &s)

bool	allowsingleaction (const action_name_multiset &allowaction, const action_list &multiaction)
	determine whether the multiaction has the same labels as the allow action,

bool	allow_ (const action_name_multiset_list &allowlist, const action_list &multiaction)

bool	encap (const action_name_multiset_list &encaplist, const action_list &multiaction)

void	allowblockcomposition (const action_name_multiset_list &allowlist1, const bool is_allow, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)

action	rename_action (const rename_expression_list &renamings, const action &act)

action_list	rename_actions (const rename_expression_list &renamings, const action_list &multiaction)

void	renamecomposition (const rename_expression_list &renamings, stochastic_action_summand_vector &action_summands)

bool	occursinvarandremove (const variable &var, variable_list &vl)

variable_list	construct_renaming (const variable_list &pars1, const variable_list &pars2, variable_list &pars3, variable_list &pars4, const bool unique=true)

template<typename List >
sort_expression_list	get_sorts (const List &l)

data_expression	pairwiseMatch (const data_expression_list &l1, const data_expression_list &l2)

tuple_list	addActionCondition (const action &firstaction, const data_expression &condition, const tuple_list &L, tuple_list S)

process::action_label	can_communicate (const action_list &m, comm_entry &comm_table)

tuple_list	phi (const action_list &m, const data_expression_list &d, const action_list &w, const action_list &n, const action_list &r, const bool r_is_null, comm_entry &comm_table)

bool	xi (const action_list &alpha, const action_list &beta, comm_entry &comm_table)

data_expression	psi (const action_list &alpha_in, comm_entry &comm_table)

tuple_list	makeMultiActionConditionList_aux (const action_list &multiaction, comm_entry &comm_table, const action_list &r, const bool r_is_null)

tuple_list	makeMultiActionConditionList (const action_list &multiaction, const communication_expression_list &communications)

void	communicationcomposition (const communication_expression_list &communications, const action_name_multiset_list &allowlist1, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)

bool	check_real_variable_occurrence (const variable_list &sumvars, const data_expression &actiontime, const data_expression &condition)

data_expression	makesingleultimatedelaycondition (const variable_list &sumvars, const variable_list &freevars, const data_expression &condition, const bool has_time, const variable &timevariable, const data_expression &actiontime, variable_list &used_sumvars)

lps::detail::ultimate_delay	getUltimateDelayCondition (const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands, const variable_list &freevars)

data::maintain_variables_in_rhs< data::mutable_map_substitution<> >	make_unique_variables (const variable_list &var_list, const std::string &hint)

void	make_parameters_and_sum_variables_unique (stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, variable_list &pars, lps::detail::ultimate_delay &ultimate_delay_condition, const std::string &hint="")

lps::detail::ultimate_delay	combine_ultimate_delays (const lps::detail::ultimate_delay &delay1, const lps::detail::ultimate_delay &delay2)
	Returns the conjunction of the two delay conditions and the join of the variables, where the variables in delay2 are renamed to avoid conflict with those in delay1.

void	calculate_left_merge_action (const lps::detail::ultimate_delay &ultimate_delay_condition, const stochastic_action_summand_vector &action_summands1, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands)

void	calculate_left_merge_deadlock (const lps::detail::ultimate_delay &ultimate_delay_condition, const deadlock_summand_vector &deadlock_summands1, const bool is_allow, const bool is_block, const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)

void	calculate_left_merge (const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const lps::detail::ultimate_delay &ultimate_delay_condition2, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)

void	calculate_communication_merge_action_summands (const stochastic_action_summand_vector &action_summands1, const stochastic_action_summand_vector &action_summands2, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands)

void	calculate_communication_merge_action_deadlock_summands (const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)

void	calculate_communication_merge_deadlock_summands (const deadlock_summand_vector &deadlock_summands1, const deadlock_summand_vector &deadlock_summands2, const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)

void	calculate_communication_merge (const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const stochastic_action_summand_vector &action_summands2, const deadlock_summand_vector &deadlock_summands2, const action_name_multiset_list &allowlist, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)

void	combine_summand_lists (const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const lps::detail::ultimate_delay &ultimate_delay_condition1, const stochastic_action_summand_vector &action_summands2, const deadlock_summand_vector &deadlock_summands2, const lps::detail::ultimate_delay &ultimate_delay_condition2, const variable_list &par1, const variable_list &par3, const action_name_multiset_list &allowlist1, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)

void	parallelcomposition (const stochastic_action_summand_vector &action_summands1, const deadlock_summand_vector &deadlock_summands1, const variable_list &pars1, const data_expression_list &init1, const stochastic_distribution &initial_stochastic_distribution1, const lps::detail::ultimate_delay &ultimate_delay_condition1, const stochastic_action_summand_vector &action_summands2, const deadlock_summand_vector &deadlock_summands2, const variable_list &pars2, const data_expression_list &init2, const stochastic_distribution &initial_stochastic_distribution2, const lps::detail::ultimate_delay &ultimate_delay_condition2, const action_name_multiset_list &allowlist1, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, variable_list &pars_result, data_expression_list &init_result, stochastic_distribution &initial_stochastic_distribution, lps::detail::ultimate_delay &ultimate_delay_condition)

void	generateLPEmCRLterm (stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_expression &t, const bool regular, const bool rename_variables, variable_list &pars, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution, lps::detail::ultimate_delay &ultimate_delay_condition)
	Linearise a process indicated by procIdDecl.

void	generateLPEmCRL (stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_identifier &procIdDecl, const bool regular, variable_list &pars, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution, lps::detail::ultimate_delay &ultimate_delay_condition)

process_expression	alphaconversionterm (const process_expression &t, const variable_list &parameters, maintain_variables_in_rhs< mutable_map_substitution<> > sigma)

void	alphaconversion (const process_identifier &procId, const variable_list &parameters)

bool	containstimebody (const process_expression &t, bool *stable, std::set< process_identifier > &visited, bool allowrecursion, bool &contains_if_then)

bool	containstime_rec (const process_identifier &procId, bool *stable, std::set< process_identifier > &visited, bool &contains_if_then)

bool	containstimebody (const process_expression &t)

bool	determinewhetherprocessescontaintime (const process_identifier &procId)

process_expression	transform_initial_distribution_term (const process_expression &t, const std::map< process_identifier, process_pid_pair > &processes_with_initial_distribution)

process_expression	obtain_initial_distribution_term (const process_expression &t)

process_expression	obtain_initial_distribution (const process_identifier &procId)

bool	canterminatebody (const process_expression &t, bool &stable, std::set< process_identifier > &visited, const bool allowrecursion)

bool	canterminate_rec (const process_identifier &procId, bool &stable, std::set< process_identifier > &visited)

bool	canterminatebody (const process_expression &t)

void	determinewhetherprocessescanterminate (const process_identifier &procId)

process_identifier	split_process (const process_identifier &procId, std::map< process_identifier, process_identifier > &visited_id, std::map< process_expression, process_expression > &visited_proc)

process_instance_assignment	expand_process_instance_assignment (const process_instance_assignment &t, std::set< process_identifier > &visited_processes)

process_instance_assignment	expand_process_instance_assignment (const process_instance_assignment &t)

void	transform_process_arguments (const process_identifier &procId, std::set< process_identifier > &visited_processes)

void	transform_process_arguments (const process_identifier &procId)

process_expression	transform_process_arguments_body (const process_expression &t, const std::set< variable > &bound_variables, std::set< process_identifier > &visited_processes)

void	guarantee_that_parameters_have_unique_type (const process_identifier &procId, std::set< process_identifier > &visited_processes, std::set< identifier_string > &used_variable_names, maintain_variables_in_rhs< mutable_map_substitution<> > &parameter_mapping, std::set< variable > &variables_in_lhs_of_parameter_mapping)

void	guarantee_that_parameters_have_unique_type (const process_identifier &procId)

process_expression	guarantee_that_parameters_have_unique_type_body (const process_expression &t, std::set< process_identifier > &visited_processes, std::set< identifier_string > &used_variable_names, maintain_variables_in_rhs< mutable_map_substitution<> > &parameter_mapping, std::set< variable > &variables_in_lhs_of_parameter_mapping)

process_expression	split_body (const process_expression &t, std::map< process_identifier, process_identifier > &visited_id, std::map< process_expression, process_expression > &visited_proc, const variable_list &parameters)

process_identifier	splitmCRLandpCRLprocsAndAddTerminatedAction (const process_identifier &procId)

void	AddTerminationActionIfNecessary (const stochastic_action_summand_vector &summands)

Static Private Member Functions
static bool	check_assignment_list (const assignment_list &assignments, const variable_list &parameters)

static action_name_multiset_list	sort_multi_action_labels (const action_name_multiset_list &l)

static action_name_multiset	sort_action_labels (const action_name_multiset &actionlabels)

static bool	might_communicate (const action_list &m, comm_entry &comm_table, const action_list &n)

Private Attributes
std::vector< process_equation >	procs

mcrl2::data::rewriter	rewr

action	terminationAction

process_identifier	terminatedProcId

process_identifier	tau_process

process_identifier	delta_process

std::vector< process_identifier >	seq_varnames

std::vector< std::vector< process_instance_assignment > >	representedprocesses

t_lin_options	options

bool	timeIsBeingUsed

bool	stochastic_operator_is_being_used

bool	fresh_equation_added

std::map< aterm, objectdatatype >	objectdata

set_identifier_generator	fresh_identifier_generator

std::vector< enumeratedtype >	enumeratedtypes

stackoperations *	stack_operations_list

Detailed Description

Definition at line 154 of file linearise.cpp.

Member Enumeration Documentation

◆ state

enum specification_basic_type::state

private

Enumerator
alt_state
sum_state
seq_state
name_state
multiaction_state

Definition at line 2280 of file linearise.cpp.

◆ terminationstatus

enum specification_basic_type::terminationstatus

private

Enumerator
terminating
infinite

Definition at line 2784 of file linearise.cpp.

◆ variableposition

enum specification_basic_type::variableposition

private

Enumerator
first
later

Definition at line 2127 of file linearise.cpp.

Constructor & Destructor Documentation

◆ specification_basic_type() [1/2]

specification_basic_type::specification_basic_type ( const specification_basic_type & )

delete

◆ specification_basic_type() [2/2]

specification_basic_type::specification_basic_type	(	const process::action_label_list &	as,
		const std::vector< process_equation > &	ps,
		const variable_list &	idvs,
		const data_specification &	ds,
		const std::set< data::variable > &	glob_vars,
		const t_lin_options &	opt,
		const process_specification &	procspec
	)

inline

Definition at line 201 of file linearise.cpp.

◆ ~specification_basic_type()

specification_basic_type::~specification_basic_type ( )

inline

Definition at line 246 of file linearise.cpp.

Member Function Documentation

◆ action_list_to_process()

process_expression specification_basic_type::action_list_to_process ( const action_list & ma )

inlineprivate

Definition at line 347 of file linearise.cpp.

◆ actioncompare()

bool specification_basic_type::actioncompare	(	const action_label &	a1,
		const action_label &	a2
	)

inlineprivate

Definition at line 797 of file linearise.cpp.

◆ adapt_multiaction_to_stack()

action_list specification_basic_type::adapt_multiaction_to_stack	(	const action_list &	multiAction,
		const stacklisttype &	stack,
		const variable_list &	vars
	)

inlineprivate

Definition at line 4808 of file linearise.cpp.

◆ adapt_multiaction_to_stack_rec()

action_list specification_basic_type::adapt_multiaction_to_stack_rec	(	const action_list &	multiAction,
		const stacklisttype &	stack,
		const variable_list &	vars
	)

inlineprivate

Definition at line 4784 of file linearise.cpp.

◆ adapt_term_to_stack()

data_expression specification_basic_type::adapt_term_to_stack	(	const data_expression &	t,
		const stacklisttype &	stack,
		const variable_list &	vars,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 4688 of file linearise.cpp.

◆ adapt_termlist_to_stack()

template<typename Iterator >

data_expression_vector specification_basic_type::adapt_termlist_to_stack	(	Iterator	begin,
		const Iterator &	end,
		const stacklisttype &	stack,
		const variable_list &	vars,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 4768 of file linearise.cpp.

◆ add_summands()

void specification_basic_type::add_summands	(	const process_identifier &	procId,
		stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		process_expression	summandterm,
		const std::set< process_identifier > &	pCRLprocs,
		const stacklisttype &	stack,
		const bool	regular,
		const bool	singlestate,
		const variable_list &	process_parameters
	)

inlineprivate

Definition at line 5307 of file linearise.cpp.

◆ addActionCondition()

tuple_list specification_basic_type::addActionCondition	(	const action &	firstaction,
		const data_expression &	condition,
		const tuple_list &	L,
		tuple_list	S
	)

inlineprivate

Definition at line 7789 of file linearise.cpp.

◆ addcondition()

data_expression_list specification_basic_type::addcondition	(	const variable_list &	matchinglist,
		const data_expression_list &	conditionlist
	)

inlineprivate

Definition at line 5984 of file linearise.cpp.

◆ addMultiAction()

objectdatatype & specification_basic_type::addMultiAction	(	const process_expression &	multiAction,
		bool &	isnew
	)

inlineprivate

Definition at line 466 of file linearise.cpp.

◆ addString()

void specification_basic_type::addString ( const identifier_string & str )

inlineprivate

Definition at line 342 of file linearise.cpp.

◆ AddTerminationActionIfNecessary()

void specification_basic_type::AddTerminationActionIfNecessary ( const stochastic_action_summand_vector & summands )

inlineprivate

Definition at line 11116 of file linearise.cpp.

◆ all_equal()

template<class T >

bool specification_basic_type::all_equal ( const atermpp::term_list< T > & l )

inlineprivate

Definition at line 6099 of file linearise.cpp.

◆ allow_()

bool specification_basic_type::allow_	(	const action_name_multiset_list &	allowlist,
		const action_list &	multiaction
	)

inlineprivate

Definition at line 7463 of file linearise.cpp.

◆ allowblockcomposition()

void specification_basic_type::allowblockcomposition	(	const action_name_multiset_list &	allowlist1,
		const bool	is_allow,
		stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands
	)

inlineprivate

Definition at line 7506 of file linearise.cpp.

◆ allowsingleaction()

bool specification_basic_type::allowsingleaction	(	const action_name_multiset &	allowaction,
		const action_list &	multiaction
	)

inlineprivate

determine whether the multiaction has the same labels as the allow action,

Definition at line 7438 of file linearise.cpp.

◆ alphaconversion()

void specification_basic_type::alphaconversion	(	const process_identifier &	procId,
		const variable_list &	parameters
	)

inlineprivate

Definition at line 9672 of file linearise.cpp.

◆ alphaconversionterm()

process_expression specification_basic_type::alphaconversionterm	(	const process_expression &	t,
		const variable_list &	parameters,
		maintain_variables_in_rhs< mutable_map_substitution<> >	sigma
	)

inlineprivate

Definition at line 9535 of file linearise.cpp.

◆ alphaconvert()

template<class MutableSubstitution >

void specification_basic_type::alphaconvert	(	variable_list &	sumvars,
		MutableSubstitution &	sigma,
		const variable_list &	occurvars,
		const data_expression_list &	occurterms
	)

inlineprivate

Definition at line 1512 of file linearise.cpp.

◆ alphaconvertprocess()

template<class MutableSubstitution >

void specification_basic_type::alphaconvertprocess	(	variable_list &	sumvars,
		MutableSubstitution &	sigma,
		const process_expression &	p
	)

inlineprivate

Definition at line 1485 of file linearise.cpp.

◆ alreadypresent()

bool specification_basic_type::alreadypresent	(	variable &	var,
		const variable_list &	vl
	)

inlineprivate

Definition at line 4239 of file linearise.cpp.

◆ argscollect_regular()

assignment_list specification_basic_type::argscollect_regular	(	const process_expression &	t,
		const variable_list &	vl,
		const std::set< variable > &	variables_bound_in_sum
	)

inlineprivate

Definition at line 3270 of file linearise.cpp.

◆ argscollect_regular2()

assignment_list specification_basic_type::argscollect_regular2	(	const process_expression &	t,
		variable_list &	vl
	)

inlineprivate

Definition at line 3287 of file linearise.cpp.

◆ bodytovarheadGNF()

process_expression specification_basic_type::bodytovarheadGNF	(	const process_expression &	body,
		const state	s,
		const variable_list &	freevars,
		const variableposition	v,
		const std::set< variable > &	variables_bound_in_sum
	)

inlineprivate

Definition at line 2416 of file linearise.cpp.

◆ calculate_communication_merge()

void specification_basic_type::calculate_communication_merge	(	const stochastic_action_summand_vector &	action_summands1,
		const deadlock_summand_vector &	deadlock_summands1,
		const stochastic_action_summand_vector &	action_summands2,
		const deadlock_summand_vector &	deadlock_summands2,
		const action_name_multiset_list &	allowlist,
		const bool	is_allow,
		const bool	is_block,
		stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands
	)

inlineprivate

Definition at line 9074 of file linearise.cpp.

◆ calculate_communication_merge_action_deadlock_summands()

void specification_basic_type::calculate_communication_merge_action_deadlock_summands	(	const stochastic_action_summand_vector &	action_summands1,
		const deadlock_summand_vector &	deadlock_summands1,
		const stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands
	)

inlineprivate

Definition at line 8958 of file linearise.cpp.

◆ calculate_communication_merge_action_summands()

void specification_basic_type::calculate_communication_merge_action_summands	(	const stochastic_action_summand_vector &	action_summands1,
		const stochastic_action_summand_vector &	action_summands2,
		const action_name_multiset_list &	allowlist,
		const bool	is_allow,
		const bool	is_block,
		stochastic_action_summand_vector &	action_summands
	)

inlineprivate

Definition at line 8860 of file linearise.cpp.

◆ calculate_communication_merge_deadlock_summands()

void specification_basic_type::calculate_communication_merge_deadlock_summands	(	const deadlock_summand_vector &	deadlock_summands1,
		const deadlock_summand_vector &	deadlock_summands2,
		const stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands
	)

inlineprivate

Definition at line 9016 of file linearise.cpp.

◆ calculate_left_merge()

void specification_basic_type::calculate_left_merge	(	const stochastic_action_summand_vector &	action_summands1,
		const deadlock_summand_vector &	deadlock_summands1,
		const lps::detail::ultimate_delay &	ultimate_delay_condition2,
		const action_name_multiset_list &	allowlist,
		const bool	is_allow,
		const bool	is_block,
		stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands
	)

inlineprivate

Definition at line 8842 of file linearise.cpp.

◆ calculate_left_merge_action()

void specification_basic_type::calculate_left_merge_action	(	const lps::detail::ultimate_delay &	ultimate_delay_condition,
		const stochastic_action_summand_vector &	action_summands1,
		const action_name_multiset_list &	allowlist,
		const bool	is_allow,
		const bool	is_block,
		stochastic_action_summand_vector &	action_summands
	)

inlineprivate

Definition at line 8708 of file linearise.cpp.

◆ calculate_left_merge_deadlock()

void specification_basic_type::calculate_left_merge_deadlock	(	const lps::detail::ultimate_delay &	ultimate_delay_condition,
		const deadlock_summand_vector &	deadlock_summands1,
		const bool	is_allow,
		const bool	is_block,
		const stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands
	)

inlineprivate

Definition at line 8781 of file linearise.cpp.

◆ can_communicate()

process::action_label specification_basic_type::can_communicate	(	const action_list &	m,
		comm_entry &	comm_table
	)

inlineprivate

Definition at line 7845 of file linearise.cpp.

◆ canterminate_rec()

bool specification_basic_type::canterminate_rec	(	const process_identifier &	procId,
		bool &	stable,
		std::set< process_identifier > &	visited
	)

inlineprivate

Definition at line 10463 of file linearise.cpp.

◆ canterminatebody() [1/2]

bool specification_basic_type::canterminatebody ( const process_expression & t )

inlineprivate

Definition at line 10483 of file linearise.cpp.

◆ canterminatebody() [2/2]

bool specification_basic_type::canterminatebody	(	const process_expression &	t,
		bool &	stable,
		std::set< process_identifier > &	visited,
		const bool	allowrecursion
	)

inlineprivate

Definition at line 10346 of file linearise.cpp.

◆ check_assignment_list()

static bool specification_basic_type::check_assignment_list	(	const assignment_list &	assignments,
		const variable_list &	parameters
	)

inlinestaticprivate

Definition at line 1755 of file linearise.cpp.

◆ check_real_variable_occurrence()

bool specification_basic_type::check_real_variable_occurrence	(	const variable_list &	sumvars,
		const data_expression &	actiontime,
		const data_expression &	condition
	)

inlineprivate

Definition at line 8331 of file linearise.cpp.

◆ check_valid_process_instance_assignment()

bool specification_basic_type::check_valid_process_instance_assignment	(	const process_identifier &	id,
		const assignment_list &	assignments
	)

inlineprivate

Definition at line 1900 of file linearise.cpp.

◆ cluster_actions()

void specification_basic_type::cluster_actions	(	stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		const variable_list &	pars
	)

inlineprivate

Definition at line 7061 of file linearise.cpp.

◆ collect_sum_arg_arg_cond() [1/2]

deadlock_summand specification_basic_type::collect_sum_arg_arg_cond	(	const enumtype &	e,
		std::size_t	n,
		const deadlock_summand_vector &	deadlock_summands,
		const variable_list &	parameters
	)

inlineprivate

Definition at line 6797 of file linearise.cpp.

◆ collect_sum_arg_arg_cond() [2/2]

stochastic_action_summand specification_basic_type::collect_sum_arg_arg_cond	(	const enumtype &	e,
		std::size_t	n,
		const stochastic_action_summand_vector &	action_summands,
		const variable_list &	parameters
	)

inlineprivate

Definition at line 6174 of file linearise.cpp.

◆ collectparameterlist()

variable_list specification_basic_type::collectparameterlist ( const std::set< process_identifier > & pCRLprocs )

inlineprivate

Definition at line 4286 of file linearise.cpp.

◆ collectPcrlProcesses() [1/2]

void specification_basic_type::collectPcrlProcesses	(	const process_identifier &	procDecl,
		std::vector< process_identifier > &	pcrlprocesses
	)

inlineprivate

Definition at line 1265 of file linearise.cpp.

◆ collectPcrlProcesses() [2/2]

void specification_basic_type::collectPcrlProcesses	(	const process_identifier &	procDecl,
		std::vector< process_identifier > &	pcrlprocesses,
		std::set< process_identifier > &	visited
	)

inlineprivate

Definition at line 1248 of file linearise.cpp.

◆ collectPcrlProcesses_term()

void specification_basic_type::collectPcrlProcesses_term	(	const process_expression &	body,
		std::vector< process_identifier > &	pcrlprocesses,
		std::set< process_identifier > &	visited
	)

inlineprivate

Definition at line 1139 of file linearise.cpp.

◆ collectsumlist()

void specification_basic_type::collectsumlist	(	stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		const std::set< process_identifier > &	pCRLprocs,
		const variable_list &	pars,
		const stacklisttype &	stack,
		bool	regular,
		bool	singlestate
	)

inlineprivate

Definition at line 5565 of file linearise.cpp.

◆ collectsumlistterm()

void specification_basic_type::collectsumlistterm	(	const process_identifier &	procId,
		stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		const process_expression &	body,
		const variable_list &	pars,
		const stacklisttype &	stack,
		const bool	regular,
		const bool	singlestate,
		const std::set< process_identifier > &	pCRLprocs
	)

inlineprivate

Definition at line 5528 of file linearise.cpp.

◆ combine_summand_lists()

void specification_basic_type::combine_summand_lists	(	const stochastic_action_summand_vector &	action_summands1,
		const deadlock_summand_vector &	deadlock_summands1,
		const lps::detail::ultimate_delay &	ultimate_delay_condition1,
		const stochastic_action_summand_vector &	action_summands2,
		const deadlock_summand_vector &	deadlock_summands2,
		const lps::detail::ultimate_delay &	ultimate_delay_condition2,
		const variable_list &	par1,
		const variable_list &	par3,
		const action_name_multiset_list &	allowlist1,
		const bool	is_allow,
		const bool	is_block,
		stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands
	)

inlineprivate

Definition at line 9092 of file linearise.cpp.

◆ combine_ultimate_delays()

lps::detail::ultimate_delay specification_basic_type::combine_ultimate_delays	(	const lps::detail::ultimate_delay &	delay1,
		const lps::detail::ultimate_delay &	delay2
	)

inlineprivate

Returns the conjunction of the two delay conditions and the join of the variables, where the variables in delay2 are renamed to avoid conflict with those in delay1.

Definition at line 8687 of file linearise.cpp.

◆ communicationcomposition()

void specification_basic_type::communicationcomposition	(	const communication_expression_list &	communications,
		const action_name_multiset_list &	allowlist1,
		const bool	is_allow,
		const bool	is_block,
		stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands
	)

inlineprivate

Definition at line 8182 of file linearise.cpp.

◆ complete_proc_identifier_map()

void specification_basic_type::complete_proc_identifier_map ( std::map< process_identifier, process_identifier > & identifier_identifier_map )

inlineprivate

Definition at line 4014 of file linearise.cpp.

◆ construct_binary_case_tree()

data_expression specification_basic_type::construct_binary_case_tree	(	std::size_t	n,
		const variable_list &	sums,
		data_expression_list	terms,
		const sort_expression &	termsort,
		const enumtype &	e
	)

inlineprivate

Definition at line 6117 of file linearise.cpp.

◆ construct_binary_case_tree_rec()

data_expression specification_basic_type::construct_binary_case_tree_rec	(	std::size_t	n,
		const variable_list &	sums,
		data_expression_list &	terms,
		const sort_expression &	termsort,
		const enumtype &	e
	)

inlineprivate

Definition at line 6062 of file linearise.cpp.

◆ construct_renaming()

variable_list specification_basic_type::construct_renaming	(	const variable_list &	pars1,
		const variable_list &	pars2,
		variable_list &	pars3,
		variable_list &	pars4,
		const bool	unique = `true`
	)

inlineprivate

Definition at line 7685 of file linearise.cpp.

◆ containstime_rec()

bool specification_basic_type::containstime_rec	(	const process_identifier &	procId,
		bool *	stable,
		std::set< process_identifier > &	visited,
		bool &	contains_if_then
	)

inlineprivate

Definition at line 9826 of file linearise.cpp.

◆ containstimebody() [1/2]

bool specification_basic_type::containstimebody ( const process_expression & t )

inlineprivate

Definition at line 9858 of file linearise.cpp.

◆ containstimebody() [2/2]

bool specification_basic_type::containstimebody	(	const process_expression &	t,
		bool *	stable,
		std::set< process_identifier > &	visited,
		bool	allowrecursion,
		bool &	contains_if_then
	)

inlineprivate

Definition at line 9706 of file linearise.cpp.

◆ correctstatecond()

data_expression specification_basic_type::correctstatecond	(	const process_identifier &	procId,
		const std::set< process_identifier > &	pCRLproc,
		const stacklisttype &	stack,
		int	regular
	)

inlineprivate

Definition at line 4621 of file linearise.cpp.

◆ create_case_function_on_enumeratedtype()

void specification_basic_type::create_case_function_on_enumeratedtype	(	const sort_expression &	sort,
		const std::size_t	enumeratedtype_index
	)

inlineprivate

Definition at line 5741 of file linearise.cpp.

◆ create_enumeratedtype()

std::size_t specification_basic_type::create_enumeratedtype ( const std::size_t n )

inlineprivate

Definition at line 5661 of file linearise.cpp.

◆ create_regular_invocation()

process_expression specification_basic_type::create_regular_invocation	(	process_expression	sequence,
		std::vector< process_identifier > &	todo,
		const variable_list &	freevars,
		const std::set< variable > &	variables_bound_in_sum
	)

inlineprivate

Definition at line 3357 of file linearise.cpp.

◆ cut_off_unreachable_tail()

process_expression specification_basic_type::cut_off_unreachable_tail ( const process_expression & t )

inlineprivate

Definition at line 3329 of file linearise.cpp.

◆ declare_control_state()

void specification_basic_type::declare_control_state ( const std::set< process_identifier > & pCRLprocs )

inlineprivate

Definition at line 4299 of file linearise.cpp.

◆ define_equations_for_case_function()

void specification_basic_type::define_equations_for_case_function	(	const std::size_t	index,
		const data::function_symbol &	functionname,
		const sort_expression &	sort
	)

inlineprivate

Definition at line 5690 of file linearise.cpp.

◆ delta_at_zero()

process_expression specification_basic_type::delta_at_zero ( void )

inlineprivate

Definition at line 287 of file linearise.cpp.

◆ detail_check_objectdata()

void specification_basic_type::detail_check_objectdata ( const aterm & o ) const

inlineprivate

Definition at line 316 of file linearise.cpp.

◆ determine_process_status()

void specification_basic_type::determine_process_status	(	const process_identifier &	procDecl,
		const processstatustype	status
	)

inlineprivate

Definition at line 1102 of file linearise.cpp.

◆ determine_process_statusterm()

processstatustype specification_basic_type::determine_process_statusterm	(	const process_expression &	body,
		const processstatustype	status
	)

inlineprivate

Definition at line 863 of file linearise.cpp.

◆ determinewhetherprocessescanterminate()

void specification_basic_type::determinewhetherprocessescanterminate ( const process_identifier & procId )

inlineprivate

Definition at line 10490 of file linearise.cpp.

◆ determinewhetherprocessescontaintime()

bool specification_basic_type::determinewhetherprocessescontaintime ( const process_identifier & procId )

inlineprivate

Definition at line 9866 of file linearise.cpp.

◆ distribute_condition()

process_expression specification_basic_type::distribute_condition	(	const process_expression &	body1,
		const data_expression &	condition
	)

inlineprivate

Definition at line 2871 of file linearise.cpp.

◆ distribute_sum()

process_expression specification_basic_type::distribute_sum	(	const variable_list &	sumvars,
		const process_expression &	body1
	)

inlineprivate

Definition at line 3073 of file linearise.cpp.

◆ distribute_sum_over_a_stochastic_operator()

process_expression specification_basic_type::distribute_sum_over_a_stochastic_operator	(	const variable_list &	sumvars,
		const variable_list &	stochastic_variables,
		const data_expression &	distribution,
		const process_expression &	body
	)

inlineprivate

Definition at line 3030 of file linearise.cpp.

◆ distributeActionOverConditions()

process_expression specification_basic_type::distributeActionOverConditions	(	const process_expression &	act,
		const data_expression &	condition,
		const process_expression &	restterm,
		const variable_list &	freevars,
		const std::set< variable > &	variables_bound_in_sum
	)

inlineprivate

Definition at line 2335 of file linearise.cpp.

◆ distributeTime()

process_expression specification_basic_type::distributeTime	(	const process_expression &	body,
		const data_expression &	time,
		const variable_list &	freevars,
		data_expression &	timecondition
	)

inlineprivate

Definition at line 3524 of file linearise.cpp.

◆ dummyparameterlist()

assignment_list specification_basic_type::dummyparameterlist	(	const stacklisttype &	stack,
		const bool	singlestate
	)

inlineprivate

Definition at line 5255 of file linearise.cpp.

◆ encap()

bool specification_basic_type::encap	(	const action_name_multiset_list &	encaplist,
		const action_list &	multiaction
	)

inlineprivate

Definition at line 7489 of file linearise.cpp.

◆ enumerate_distribution_and_sums()

process_expression specification_basic_type::enumerate_distribution_and_sums	(	const variable_list &	sumvars,
		const variable_list &	stochvars,
		const data_expression &	distribution,
		const process_expression &	body
	)

inlineprivate

Definition at line 2956 of file linearise.cpp.

◆ exists_variable_for_sequence()

bool specification_basic_type::exists_variable_for_sequence	(	const std::vector< process_instance_assignment > &	process_names,
		process_identifier &	result
	)

inlineprivate

Definition at line 3167 of file linearise.cpp.

◆ expand_process_instance_assignment() [1/2]

process_instance_assignment specification_basic_type::expand_process_instance_assignment ( const process_instance_assignment & t )

inlineprivate

Definition at line 10581 of file linearise.cpp.

◆ expand_process_instance_assignment() [2/2]

process_instance_assignment specification_basic_type::expand_process_instance_assignment	(	const process_instance_assignment &	t,
		std::set< process_identifier > &	visited_processes
	)

inlineprivate

Definition at line 10553 of file linearise.cpp.

◆ extend()

data_expression_list specification_basic_type::extend	(	const data_expression &	c,
		const data_expression_list &	cl
	)

inlineprivate

Definition at line 5924 of file linearise.cpp.

◆ extend_conditions()

data_expression_list specification_basic_type::extend_conditions	(	const variable &	var,
		const data_expression_list &	conditionlist
	)

inlineprivate

Definition at line 5944 of file linearise.cpp.

◆ extract_names()

void specification_basic_type::extract_names	(	const process_expression &	sequence,
		std::vector< process_instance_assignment > &	result
	)

inlineprivate

Definition at line 3187 of file linearise.cpp.

◆ filter_assignments()

assignment_list specification_basic_type::filter_assignments	(	const assignment_list &	assignments,
		const variable_list &	parameters
	)

inlineprivate

Definition at line 1741 of file linearise.cpp.

◆ filter_vars_by_assignmentlist()

void specification_basic_type::filter_vars_by_assignmentlist	(	const assignment_list &	assignments,
		const variable_list &	parameters,
		const std::set< variable > &	vars_set,
		std::set< variable > &	vars_result_set
	)

inlineprivate

Definition at line 1392 of file linearise.cpp.

◆ filter_vars_by_multiaction()

void specification_basic_type::filter_vars_by_multiaction	(	const action_list &	multiaction,
		const std::set< variable > &	vars_set,
		std::set< variable > &	vars_result_set
	)

inlineprivate

Definition at line 1380 of file linearise.cpp.

◆ filter_vars_by_term()

void specification_basic_type::filter_vars_by_term	(	const data_expression &	t,
		const std::set< variable > &	vars_set,
		std::set< variable > &	vars_result_set
	)

inlineprivate

Definition at line 1280 of file linearise.cpp.

◆ filter_vars_by_termlist()

template<typename Iterator >

void specification_basic_type::filter_vars_by_termlist	(	Iterator	begin,
		const Iterator &	end,
		const std::set< variable > &	vars_set,
		std::set< variable > &	vars_result_set
	)

inlineprivate

Definition at line 1368 of file linearise.cpp.

◆ find_()

data_expression specification_basic_type::find_	(	const variable &	s,
		const assignment_list &	args,
		const stacklisttype &	stack,
		const variable_list &	vars,
		const std::set< variable > &	free_variables_in_body,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 4828 of file linearise.cpp.

◆ find_case_function()

data::function_symbol specification_basic_type::find_case_function	(	std::size_t	index,
		const sort_expression &	sort
	)

inlineprivate

Definition at line 5674 of file linearise.cpp.

◆ find_dummy_arguments()

assignment_list specification_basic_type::find_dummy_arguments	(	const variable_list &	parlist,
		const assignment_list &	args,
		const std::set< variable > &	free_variables_in_body,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 4882 of file linearise.cpp.

◆ find_free_variables_process() [1/2]

std::set< variable > specification_basic_type::find_free_variables_process ( const process_expression & p )

inlineprivate

Definition at line 1733 of file linearise.cpp.

◆ find_free_variables_process() [2/2]

void specification_basic_type::find_free_variables_process	(	const process_expression &	p,
		std::set< variable > &	free_variables_in_p
	)

inlineprivate

Definition at line 1551 of file linearise.cpp.

◆ findarguments()

data_expression_list specification_basic_type::findarguments	(	const variable_list &	pars,
		const variable_list &	parlist,
		const assignment_list &	args,
		const data_expression_list &	t2,
		const stacklisttype &	stack,
		const variable_list &	vars,
		const std::set< variable > &	free_variables_in_body,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 4861 of file linearise.cpp.

◆ generateLPEmCRL()

void specification_basic_type::generateLPEmCRL	(	stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		const process_identifier &	procIdDecl,
		const bool	regular,
		variable_list &	pars,
		data_expression_list &	init,
		stochastic_distribution &	initial_stochastic_distribution,
		lps::detail::ultimate_delay &	ultimate_delay_condition
	)

inlineprivate

Definition at line 9465 of file linearise.cpp.

◆ generateLPEmCRLterm()

void specification_basic_type::generateLPEmCRLterm	(	stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		const process_expression &	t,
		const bool	regular,
		const bool	rename_variables,
		variable_list &	pars,
		data_expression_list &	init,
		stochastic_distribution &	initial_stochastic_distribution,
		lps::detail::ultimate_delay &	ultimate_delay_condition
	)

inlineprivate

Linearise a process indicated by procIdDecl.

Returns actions_summands, deadlock_summands, the process parameters and the initial assignment list.

Definition at line 9213 of file linearise.cpp.

◆ generateLPEpCRL()

void specification_basic_type::generateLPEpCRL	(	stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		const process_identifier &	procId,
		const bool	containstime,
		const bool	regular,
		variable_list &	parameters,
		data_expression_list &	init,
		stochastic_distribution &	initial_stochastic_distribution
	)

inlineprivate

Definition at line 7176 of file linearise.cpp.

◆ get_free_variables()

const std::set< variable > & specification_basic_type::get_free_variables ( objectdatatype & object )

inlineprivate

Definition at line 494 of file linearise.cpp.

◆ get_fresh_variable()

variable specification_basic_type::get_fresh_variable	(	const std::string &	s,
		const sort_expression &	sort,
		const int	reuse_index = `-1`
	)

inlineprivate

Definition at line 2282 of file linearise.cpp.

◆ get_last()

process_identifier specification_basic_type::get_last	(	const process_identifier &	id,
		const std::map< process_identifier, process_identifier > &	identifier_identifier_map
	)

inlineprivate

Definition at line 3970 of file linearise.cpp.

◆ get_sorts()

template<typename List >

sort_expression_list specification_basic_type::get_sorts ( const List & l )

inlineprivate

Definition at line 7755 of file linearise.cpp.

◆ getActionSorts()

sort_expression_list specification_basic_type::getActionSorts ( const action_list & actionlist )

inlineprivate

Definition at line 7050 of file linearise.cpp.

◆ getarguments()

data_expression_list specification_basic_type::getarguments ( const action_list & multiAction )

inlineprivate

Definition at line 436 of file linearise.cpp.

◆ getnames()

process::action_label_list specification_basic_type::getnames ( const process_expression & multiAction )

inlineprivate

Definition at line 380 of file linearise.cpp.

◆ getparameters()

variable_list specification_basic_type::getparameters ( const process_expression & multiAction )

inlineprivate

Definition at line 430 of file linearise.cpp.

◆ getparameters_rec()

variable_list specification_basic_type::getparameters_rec	(	const process_expression &	multiAction,
		std::set< variable > &	occurs_set
	)

inlineprivate

Definition at line 418 of file linearise.cpp.

◆ getRHSassignment()

data_expression specification_basic_type::getRHSassignment	(	const variable &	var,
		const assignment_list &	as
	)

inlineprivate

Definition at line 6162 of file linearise.cpp.

◆ getUltimateDelayCondition()

lps::detail::ultimate_delay specification_basic_type::getUltimateDelayCondition	(	const stochastic_action_summand_vector &	action_summands,
		const deadlock_summand_vector &	deadlock_summands,
		const variable_list &	freevars
	)

inlineprivate

Definition at line 8437 of file linearise.cpp.

◆ getvar()

data_expression specification_basic_type::getvar	(	const variable &	var,
		const stacklisttype &	stack
	)

inlineprivate

Definition at line 4493 of file linearise.cpp.

◆ guarantee_that_parameters_have_unique_type() [1/2]

void specification_basic_type::guarantee_that_parameters_have_unique_type ( const process_identifier & procId )

inlineprivate

Definition at line 10817 of file linearise.cpp.

◆ guarantee_that_parameters_have_unique_type() [2/2]

void specification_basic_type::guarantee_that_parameters_have_unique_type	(	const process_identifier &	procId,
		std::set< process_identifier > &	visited_processes,
		std::set< identifier_string > &	used_variable_names,
		maintain_variables_in_rhs< mutable_map_substitution<> > &	parameter_mapping,
		std::set< variable > &	variables_in_lhs_of_parameter_mapping
	)

inlineprivate

Definition at line 10773 of file linearise.cpp.

◆ guarantee_that_parameters_have_unique_type_body()

process_expression specification_basic_type::guarantee_that_parameters_have_unique_type_body	(	const process_expression &	t,
		std::set< process_identifier > &	visited_processes,
		std::set< identifier_string > &	used_variable_names,
		maintain_variables_in_rhs< mutable_map_substitution<> > &	parameter_mapping,
		std::set< variable > &	variables_in_lhs_of_parameter_mapping
	)

inlineprivate

Definition at line 10830 of file linearise.cpp.

◆ hide_()

action_list specification_basic_type::hide_	(	const identifier_string_list &	hidelist,
		const action_list &	multiaction
	)

inlineprivate

Definition at line 7278 of file linearise.cpp.

◆ hidecomposition()

void specification_basic_type::hidecomposition	(	const identifier_string_list &	hidelist,
		stochastic_action_summand_vector &	action_summands
	)

inlineprivate

Definition at line 7294 of file linearise.cpp.

◆ implies_condition()

bool specification_basic_type::implies_condition	(	const data_expression &	c1,
		const data_expression &	c2
	)

inlineprivate

Definition at line 7309 of file linearise.cpp.

◆ insert_process_declaration()

objectdatatype & specification_basic_type::insert_process_declaration	(	const process_identifier &	procId,
		const variable_list &	parameters,
		const process_expression &	body,
		processstatustype	s,
		const bool	canterminate,
		const bool	containstime
	)

inlineprivate

Definition at line 713 of file linearise.cpp.

◆ insert_summand()

void specification_basic_type::insert_summand	(	stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		const variable_list &	sumvars,
		const data_expression &	condition,
		const action_list &	multiAction,
		const data_expression &	actTime,
		const stochastic_distribution &	distribution,
		const assignment_list &	procargs,
		const bool	has_time,
		const bool	is_deadlock_summand
	)

inlineprivate

Definition at line 5267 of file linearise.cpp.

◆ insert_timed_delta_summand()

void specification_basic_type::insert_timed_delta_summand	(	const stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		const deadlock_summand &	s
	)

inlineprivate

Definition at line 7368 of file linearise.cpp.

◆ insertAction()

objectdatatype & specification_basic_type::insertAction ( const action_label & actionId )

inlineprivate

Definition at line 684 of file linearise.cpp.

◆ insertvariable()

void specification_basic_type::insertvariable	(	const variable &	var,
		const bool	mustbenew
	)

inlineprivate

Definition at line 504 of file linearise.cpp.

◆ insertvariables()

void specification_basic_type::insertvariables	(	const variable_list &	vars,
		const bool	mustbenew
	)

inlineprivate

Definition at line 519 of file linearise.cpp.

◆ is_global_variable()

bool specification_basic_type::is_global_variable ( const data_expression & d ) const

inlineprivate

Definition at line 4488 of file linearise.cpp.

◆ isDeltaAtZero()

bool specification_basic_type::isDeltaAtZero ( const process_expression & t )

inlineprivate

Definition at line 292 of file linearise.cpp.

◆ joinparameters()

variable_list specification_basic_type::joinparameters	(	const variable_list &	par1,
		const variable_list &	par2
	)

inlineprivate

Definition at line 4265 of file linearise.cpp.

◆ linInsertActionInMultiActionList()

action_list specification_basic_type::linInsertActionInMultiActionList	(	const action &	act,
		action_list	multiAction
	)

inlineprivate

Definition at line 815 of file linearise.cpp.

◆ linMergeMultiActionList()

action_list specification_basic_type::linMergeMultiActionList	(	const action_list &	ma1,
		const action_list &	ma2
	)

inlineprivate

Definition at line 845 of file linearise.cpp.

◆ linMergeMultiActionListProcess()

action_list specification_basic_type::linMergeMultiActionListProcess	(	const process_expression &	ma1,
		const process_expression &	ma2
	)

inlineprivate

Definition at line 856 of file linearise.cpp.

◆ make_binary_sums()

variable_list specification_basic_type::make_binary_sums	(	std::size_t	n,
		const sort_expression &	enumtypename,
		data_expression &	condition,
		const variable_list &	tail
	)

inlineprivate

Definition at line 6035 of file linearise.cpp.

◆ make_initialstate()

data_expression_list specification_basic_type::make_initialstate	(	const process_identifier &	initialProcId,
		const stacklisttype &	stack,
		const std::set< process_identifier > &	pcrlprcs,
		const bool	regular,
		const bool	singlecontrolstate,
		const stochastic_distribution &	initial_stochastic_distribution
	)

inlineprivate

Definition at line 5211 of file linearise.cpp.

◆ make_parameters_and_sum_variables_unique()

void specification_basic_type::make_parameters_and_sum_variables_unique	(	stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		variable_list &	pars,
		lps::detail::ultimate_delay &	ultimate_delay_condition,
		const std::string &	hint = `""`
	)

inlineprivate

Definition at line 8576 of file linearise.cpp.

◆ make_parameters_rec()

variable_list specification_basic_type::make_parameters_rec	(	const data_expression_list &	l,
		std::set< variable > &	occurs_set
	)

inlineprivate

Definition at line 393 of file linearise.cpp.

◆ make_pars()

variable_list specification_basic_type::make_pars ( const sort_expression_list & sortlist )

inlineprivate

Definition at line 2318 of file linearise.cpp.

◆ make_pCRL_procs() [1/2]

void specification_basic_type::make_pCRL_procs	(	const process_expression &	t,
		std::set< process_identifier > &	reachable_process_identifiers
	)

inlineprivate

Definition at line 3905 of file linearise.cpp.

◆ make_pCRL_procs() [2/2]

void specification_basic_type::make_pCRL_procs	(	const process_identifier &	id,
		std::set< process_identifier > &	reachable_process_identifiers
	)

inlineprivate

Definition at line 3894 of file linearise.cpp.

◆ make_procargs()

assignment_list specification_basic_type::make_procargs	(	const process_expression &	t,
		const stacklisttype &	stack,
		const std::set< process_identifier > &	pcrlprcs,
		const variable_list &	vars,
		const bool	regular,
		const bool	singlestate,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 5067 of file linearise.cpp.

◆ make_procargs_regular()

assignment_list specification_basic_type::make_procargs_regular	(	const process_expression &	t,
		const stacklisttype &	stack,
		const std::set< process_identifier > &	pcrlprcs,
		const bool	singlestate,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 4955 of file linearise.cpp.

◆ make_procargs_stack()

data_expression specification_basic_type::make_procargs_stack	(	const process_expression &	t,
		const stacklisttype &	stack,
		const std::set< process_identifier > &	pcrlprcs,
		const variable_list &	vars,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 5014 of file linearise.cpp.

◆ make_unique_variables()

data::maintain_variables_in_rhs< data::mutable_map_substitution<> > specification_basic_type::make_unique_variables	(	const variable_list &	var_list,
		const std::string &	hint
	)

inlineprivate

Definition at line 8556 of file linearise.cpp.

◆ makemultiaction()

action_list specification_basic_type::makemultiaction	(	const process::action_label_list &	actionIds,
		const data_expression_list &	args
	)

inlineprivate

Definition at line 446 of file linearise.cpp.

◆ makeMultiActionConditionList()

tuple_list specification_basic_type::makeMultiActionConditionList	(	const action_list &	multiaction,
		const communication_expression_list &	communications
	)

inlineprivate

Definition at line 8174 of file linearise.cpp.

◆ makeMultiActionConditionList_aux()

tuple_list specification_basic_type::makeMultiActionConditionList_aux	(	const action_list &	multiaction,
		comm_entry &	comm_table,
		const action_list &	r,
		const bool	r_is_null
	)

inlineprivate

Definition at line 8141 of file linearise.cpp.

◆ makesingleultimatedelaycondition()

data_expression specification_basic_type::makesingleultimatedelaycondition	(	const variable_list &	sumvars,
		const variable_list &	freevars,
		const data_expression &	condition,
		const bool	has_time,
		const variable &	timevariable,
		const data_expression &	actiontime,
		variable_list &	used_sumvars
	)

inlineprivate

Definition at line 8358 of file linearise.cpp.

◆ match_sequence()

int specification_basic_type::match_sequence	(	const std::vector< process_instance_assignment > &	s1,
		const std::vector< process_instance_assignment > &	s2,
		const bool	regular2
	)

inlineprivate

Definition at line 3126 of file linearise.cpp.

◆ merge_var()

variable_list specification_basic_type::merge_var	(	const variable_list &	v1,
		const variable_list &	v2,
		std::vector< variable_list > &	renamings_pars,
		std::vector< data_expression_list > &	renamings_args,
		data_expression_list &	conditionlist,
		const variable_list &	process_parameters
	)

inlineprivate

Definition at line 6000 of file linearise.cpp.

◆ mergeoccursin()

bool specification_basic_type::mergeoccursin	(	variable &	var,
		const variable_list &	v,
		variable_list &	matchinglist,
		variable_list &	pars,
		data_expression_list &	args,
		const variable_list &	process_parameters
	)

inlineprivate

Definition at line 5845 of file linearise.cpp.

◆ might_communicate()

static bool specification_basic_type::might_communicate	(	const action_list &	m,
		comm_entry &	comm_table,
		const action_list &	n
	)

inlinestaticprivate

Definition at line 7912 of file linearise.cpp.

◆ minimize_set_of_reachable_process_identifiers()

std::set< process_identifier > specification_basic_type::minimize_set_of_reachable_process_identifiers	(	const std::set< process_identifier > &	reachable_process_identifiers,
		const process_identifier &	initial_process
	)

inlineprivate

Definition at line 4054 of file linearise.cpp.

◆ newprocess()

process_identifier specification_basic_type::newprocess	(	const variable_list &	parameters,
		const process_expression &	body,
		const processstatustype	ps,
		const bool	canterminate,
		const bool	containstime
	)

inlineprivate

Definition at line 2151 of file linearise.cpp.

◆ objectIndex() [1/2]

objectdatatype & specification_basic_type::objectIndex ( const aterm & o )

inlineprivate

Definition at line 330 of file linearise.cpp.

◆ objectIndex() [2/2]

const objectdatatype & specification_basic_type::objectIndex ( const aterm & o ) const

inlineprivate

Definition at line 336 of file linearise.cpp.

◆ obtain_initial_distribution()

process_expression specification_basic_type::obtain_initial_distribution ( const process_identifier & procId )

inlineprivate

Definition at line 10321 of file linearise.cpp.

◆ obtain_initial_distribution_term()

process_expression specification_basic_type::obtain_initial_distribution_term ( const process_expression & t )

inlineprivate

Definition at line 10128 of file linearise.cpp.

◆ occursin()

bool specification_basic_type::occursin	(	const variable &	name,
		const variable_list &	pars
	)

inlineprivate

Definition at line 5085 of file linearise.cpp.

◆ occursinpCRLterm()

bool specification_basic_type::occursinpCRLterm	(	const variable &	var,
		const process_expression &	p,
		const bool	strict
	)

inlineprivate

Definition at line 1406 of file linearise.cpp.

◆ occursinterm()

bool specification_basic_type::occursinterm	(	const variable &	var,
		const data_expression &	t
	)		const

inlineprivate

Definition at line 1275 of file linearise.cpp.

◆ occursintermlist() [1/2]

bool specification_basic_type::occursintermlist	(	const variable &	var,
		const assignment_list &	r,
		const process_identifier &	proc_name
	)		const

inlineprivate

Definition at line 1341 of file linearise.cpp.

◆ occursintermlist() [2/2]

bool specification_basic_type::occursintermlist	(	const variable &	var,
		const data_expression_list &	r
	)		const

inlineprivate

Definition at line 1329 of file linearise.cpp.

◆ occursinvarandremove()

bool specification_basic_type::occursinvarandremove	(	const variable &	var,
		variable_list &	vl
	)

inlineprivate

Definition at line 7656 of file linearise.cpp.

◆ operator=()

specification_basic_type & specification_basic_type::operator= ( const specification_basic_type & )

delete

◆ pairwiseMatch()

data_expression specification_basic_type::pairwiseMatch	(	const data_expression_list &	l1,
		const data_expression_list &	l2
	)

inlineprivate

Definition at line 7761 of file linearise.cpp.

◆ parallelcomposition()

void specification_basic_type::parallelcomposition	(	const stochastic_action_summand_vector &	action_summands1,
		const deadlock_summand_vector &	deadlock_summands1,
		const variable_list &	pars1,
		const data_expression_list &	init1,
		const stochastic_distribution &	initial_stochastic_distribution1,
		const lps::detail::ultimate_delay &	ultimate_delay_condition1,
		const stochastic_action_summand_vector &	action_summands2,
		const deadlock_summand_vector &	deadlock_summands2,
		const variable_list &	pars2,
		const data_expression_list &	init2,
		const stochastic_distribution &	initial_stochastic_distribution2,
		const lps::detail::ultimate_delay &	ultimate_delay_condition2,
		const action_name_multiset_list &	allowlist1,
		const bool	is_allow,
		const bool	is_block,
		stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		variable_list &	pars_result,
		data_expression_list &	init_result,
		stochastic_distribution &	initial_stochastic_distribution,
		lps::detail::ultimate_delay &	ultimate_delay_condition
	)

inlineprivate

Definition at line 9141 of file linearise.cpp.

◆ parameters_that_occur_in_body()

variable_list specification_basic_type::parameters_that_occur_in_body	(	const variable_list &	parameters,
		const process_expression &	body
	)

inlineprivate

Definition at line 2131 of file linearise.cpp.

◆ parameters_to_assignment_list()

assignment_list specification_basic_type::parameters_to_assignment_list	(	const variable_list &	parameters,
		const std::set< variable > &	variables_bound_in_sum
	)

inlineprivate

Definition at line 2402 of file linearise.cpp.

◆ parscollect()

variable_list specification_basic_type::parscollect	(	const process_expression &	oldbody,
		process_expression &	newbody
	)

inlineprivate

Definition at line 3222 of file linearise.cpp.

◆ pCRLrewrite()

process_expression specification_basic_type::pCRLrewrite ( const process_expression & t )

inlineprivate

Definition at line 619 of file linearise.cpp.

◆ phi()

tuple_list specification_basic_type::phi	(	const action_list &	m,
		const data_expression_list &	d,
		const action_list &	w,
		const action_list &	n,
		const action_list &	r,
		const bool	r_is_null,
		comm_entry &	comm_table
	)

inlineprivate

Definition at line 8024 of file linearise.cpp.

◆ processencoding() [1/2]

assignment_list specification_basic_type::processencoding	(	std::size_t	i,
		const assignment_list &	t1,
		const stacklisttype &	stack
	)

inlineprivate

Definition at line 4518 of file linearise.cpp.

◆ processencoding() [2/2]

data_expression_list specification_basic_type::processencoding	(	std::size_t	i,
		const data_expression_list &	t1,
		const stacklisttype &	stack
	)

inlineprivate

Definition at line 4571 of file linearise.cpp.

◆ procstorealGNF()

void specification_basic_type::procstorealGNF	(	const process_identifier &	procsIdDecl,
		const bool	regular
	)

inlineprivate

Definition at line 3866 of file linearise.cpp.

◆ procstorealGNFbody()

process_expression specification_basic_type::procstorealGNFbody	(	const process_expression &	body,
		variableposition	v,
		std::vector< process_identifier > &	todo,
		const bool	regular,
		processstatustype	mode,
		const variable_list &	freevars,
		const std::set< variable > &	variables_bound_in_sum
	)

inlineprivate

Definition at line 3604 of file linearise.cpp.

◆ procstorealGNFrec()

void specification_basic_type::procstorealGNFrec	(	const process_identifier &	procIdDecl,
		const variableposition	v,
		std::vector< process_identifier > &	todo,
		const bool	regular
	)

inlineprivate

Definition at line 3802 of file linearise.cpp.

◆ procstovarheadGNF()

void specification_basic_type::procstovarheadGNF ( const std::vector< process_identifier > & procs )

inlineprivate

Definition at line 2759 of file linearise.cpp.

◆ psi()

data_expression specification_basic_type::psi	(	const action_list &	alpha_in,
		comm_entry &	comm_table
	)

inlineprivate

Definition at line 8115 of file linearise.cpp.

◆ push_regular()

assignment_list specification_basic_type::push_regular	(	const process_identifier &	procId,
		const assignment_list &	args,
		const stacklisttype &	stack,
		const std::set< process_identifier > &	pCRLprocs,
		bool	singlestate,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 4926 of file linearise.cpp.

◆ push_stack()

data_expression specification_basic_type::push_stack	(	const process_identifier &	procId,
		const assignment_list &	args,
		const data_expression_list &	t2,
		const stacklisttype &	stack,
		const std::set< process_identifier > &	pCRLprocs,
		const variable_list &	vars,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 4984 of file linearise.cpp.

◆ pushdummy_regular()

assignment_list specification_basic_type::pushdummy_regular	(	const variable_list &	pars,
		const stacklisttype &	stack,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 5133 of file linearise.cpp.

◆ pushdummy_regular_data_expressions()

data_expression_list specification_basic_type::pushdummy_regular_data_expressions	(	const variable_list &	pars,
		const stacklisttype &	stack
	)

inlineprivate

Definition at line 5100 of file linearise.cpp.

◆ pushdummy_stack()

data_expression_list specification_basic_type::pushdummy_stack	(	const variable_list &	parameters,
		const stacklisttype &	stack,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 5203 of file linearise.cpp.

◆ pushdummyrec_stack()

data_expression_list specification_basic_type::pushdummyrec_stack	(	const variable_list &	totalpars,
		const variable_list &	pars,
		const stacklisttype &	stack,
		const variable_list &	stochastic_variables
	)

inlineprivate

Definition at line 5165 of file linearise.cpp.

◆ putbehind()

process_expression specification_basic_type::putbehind	(	const process_expression &	body1,
		const process_expression &	body2
	)

inlineprivate

Definition at line 2786 of file linearise.cpp.

◆ real_times_optimized()

data_expression specification_basic_type::real_times_optimized	(	const data_expression &	r1,
		const data_expression &	r2
	)

inlineprivate

Definition at line 270 of file linearise.cpp.

◆ remove_stochastic_operators_from_front()

std::set< process_identifier > specification_basic_type::remove_stochastic_operators_from_front	(	const std::set< process_identifier > &	reachable_process_identifiers,
		process_identifier &	initial_process_id,
		stochastic_distribution &	initial_stochastic_distribution
	)

inlineprivate

Definition at line 4164 of file linearise.cpp.

◆ rename_action()

action specification_basic_type::rename_action	(	const rename_expression_list &	renamings,
		const action &	act
	)

inlineprivate

Definition at line 7608 of file linearise.cpp.

◆ rename_actions()

action_list specification_basic_type::rename_actions	(	const rename_expression_list &	renamings,
		const action_list &	multiaction
	)

inlineprivate

Definition at line 7623 of file linearise.cpp.

◆ renamecomposition()

void specification_basic_type::renamecomposition	(	const rename_expression_list &	renamings,
		stochastic_action_summand_vector &	action_summands
	)

inlineprivate

Definition at line 7637 of file linearise.cpp.

◆ replace_variables_capture_avoiding_alt()

template<class Expression , class Substitution >

Expression specification_basic_type::replace_variables_capture_avoiding_alt	(	const Expression &	e,
		Substitution &	sigma
	)

inlineprivate

Definition at line 308 of file linearise.cpp.

◆ representative_generator_internal()

data_expression specification_basic_type::representative_generator_internal	(	const sort_expression &	s,
		const bool	allow_dont_care_var = `true`
	)

inlineprivate

Definition at line 4816 of file linearise.cpp.

◆ rewrite_assignments()

assignment_list specification_basic_type::rewrite_assignments ( const assignment_list & t )

inlineprivate

Definition at line 582 of file linearise.cpp.

◆ RewriteAction()

action specification_basic_type::RewriteAction ( const action & t )

inlineprivate

Definition at line 592 of file linearise.cpp.

◆ RewriteMultAct()

process_expression specification_basic_type::RewriteMultAct ( const process_expression & t )

inlineprivate

Definition at line 602 of file linearise.cpp.

◆ RewriteProcess()

process_instance_assignment specification_basic_type::RewriteProcess ( const process_instance_assignment & t )

inlineprivate

Definition at line 597 of file linearise.cpp.

◆ RewriteTerm()

data_expression specification_basic_type::RewriteTerm ( const data_expression & t )

inlineprivate

Definition at line 558 of file linearise.cpp.

◆ RewriteTermList()

data_expression_list specification_basic_type::RewriteTermList ( const data_expression_list & t )

inlineprivate

Definition at line 572 of file linearise.cpp.

◆ searchProcDeclaration()

bool specification_basic_type::searchProcDeclaration	(	const variable_list &	parameters,
		const process_expression &	body,
		const processstatustype	s,
		const bool	canterminate,
		const bool	containstime,
		process_identifier &	p
	)

inlineprivate

Definition at line 756 of file linearise.cpp.

◆ set_proc_identifier_map()

void specification_basic_type::set_proc_identifier_map	(	std::map< process_identifier, process_identifier > &	identifier_identifier_map,
		const process_identifier &	id1_,
		const process_identifier &	id2_,
		const process_identifier &	initial_process
	)

inlineprivate

Definition at line 3991 of file linearise.cpp.

◆ SieveProcDataVarsAssignments()

variable_list specification_basic_type::SieveProcDataVarsAssignments	(	const std::set< variable > &	vars,
		const data_expression_list &	initial_state_expressions
	)

inline

Definition at line 11180 of file linearise.cpp.

◆ SieveProcDataVarsSummands()

variable_list specification_basic_type::SieveProcDataVarsSummands	(	const std::set< variable > &	vars,
		const stochastic_action_summand_vector &	action_summands,
		const deadlock_summand_vector &	deadlock_summands,
		const variable_list &	parameters
	)

inline

Definition at line 11134 of file linearise.cpp.

◆ sigma_variables()

template<class SUBSTITUTION >

std::set< data::variable > specification_basic_type::sigma_variables ( const SUBSTITUTION & sigma )

inlineprivate

Definition at line 528 of file linearise.cpp.

◆ sort_action_labels()

static action_name_multiset specification_basic_type::sort_action_labels ( const action_name_multiset & actionlabels )

inlinestaticprivate

Definition at line 7746 of file linearise.cpp.

◆ sort_assignments()

assignment_list specification_basic_type::sort_assignments	(	const assignment_list &	ass,
		const variable_list &	parameters
	)

inlineprivate

Definition at line 1880 of file linearise.cpp.

◆ sort_multi_action_labels()

static action_name_multiset_list specification_basic_type::sort_multi_action_labels ( const action_name_multiset_list & l )

inlinestaticprivate

Definition at line 7429 of file linearise.cpp.

◆ split_body()

process_expression specification_basic_type::split_body	(	const process_expression &	t,
		std::map< process_identifier, process_identifier > &	visited_id,
		std::map< process_expression, process_expression > &	visited_proc,
		const variable_list &	parameters
	)

inlineprivate

Definition at line 10997 of file linearise.cpp.

◆ split_process()

process_identifier specification_basic_type::split_process	(	const process_identifier &	procId,
		std::map< process_identifier, process_identifier > &	visited_id,
		std::map< process_expression, process_expression > &	visited_proc
	)

inlineprivate

Definition at line 10503 of file linearise.cpp.

◆ splitmCRLandpCRLprocsAndAddTerminatedAction()

process_identifier specification_basic_type::splitmCRLandpCRLprocsAndAddTerminatedAction ( const process_identifier & procId )

inlineprivate

Definition at line 11106 of file linearise.cpp.

◆ storeact()

void specification_basic_type::storeact ( const process::action_label_list & acts )

inlineprivate

Definition at line 703 of file linearise.cpp.

◆ storeinit()

process_identifier specification_basic_type::storeinit ( const process_expression & init )

inline

Definition at line 784 of file linearise.cpp.

◆ storeprocs()

void specification_basic_type::storeprocs ( const std::vector< process_equation > & procs )

inlineprivate

Definition at line 744 of file linearise.cpp.

◆ substitute_assignmentlist()

template<class Substitution >

assignment_list specification_basic_type::substitute_assignmentlist	(	const assignment_list &	assignments,
		const variable_list &	parameters,
		const bool	replacelhs,
		const bool	replacerhs,
		Substitution &	sigma
	)

inlineprivate

Definition at line 1775 of file linearise.cpp.

◆ substitute_pCRLproc()

template<class Substitution >

process_expression specification_basic_type::substitute_pCRLproc	(	const process_expression &	p,
		Substitution &	sigma
	)

inlineprivate

Definition at line 1935 of file linearise.cpp.

◆ summandsCanBeClustered()

bool specification_basic_type::summandsCanBeClustered	(	const stochastic_action_summand &	summand1,
		const stochastic_action_summand &	summand2
	)

inlineprivate

Definition at line 6127 of file linearise.cpp.

◆ to_action_list()

action_list specification_basic_type::to_action_list ( const process_expression & p )

inlineprivate

Definition at line 360 of file linearise.cpp.

◆ to_regular_form()

process_expression specification_basic_type::to_regular_form	(	const process_expression &	t,
		std::vector< process_identifier > &	todo,
		const variable_list &	freevars,
		const std::set< variable > &	variables_bound_in_sum
	)

inlineprivate

Definition at line 3442 of file linearise.cpp.

◆ transform()

void specification_basic_type::transform	(	const process_identifier &	init,
		stochastic_action_summand_vector &	action_summands,
		deadlock_summand_vector &	deadlock_summands,
		variable_list &	parameters,
		data_expression_list &	initial_state,
		stochastic_distribution &	initial_stochastic_distribution
	)

inline

Definition at line 11205 of file linearise.cpp.

◆ transform_initial_distribution_term()

process_expression specification_basic_type::transform_initial_distribution_term	(	const process_expression &	t,
		const std::map< process_identifier, process_pid_pair > &	processes_with_initial_distribution
	)

inlineprivate

Definition at line 9887 of file linearise.cpp.

◆ transform_matching_list()

data_expression specification_basic_type::transform_matching_list ( const variable_list & matchinglist )

inlineprivate

Definition at line 5965 of file linearise.cpp.

◆ transform_process_arguments() [1/2]

void specification_basic_type::transform_process_arguments ( const process_identifier & procId )

inlineprivate

Definition at line 10623 of file linearise.cpp.

◆ transform_process_arguments() [2/2]

void specification_basic_type::transform_process_arguments	(	const process_identifier &	procId,
		std::set< process_identifier > &	visited_processes
	)

inlineprivate

Definition at line 10605 of file linearise.cpp.

◆ transform_process_arguments_body()

process_expression specification_basic_type::transform_process_arguments_body	(	const process_expression &	t,
		const std::set< variable > &	bound_variables,
		std::set< process_identifier > &	visited_processes
	)

inlineprivate

Definition at line 10631 of file linearise.cpp.

◆ transform_process_instance_to_process_instance_assignment()

process_instance_assignment specification_basic_type::transform_process_instance_to_process_instance_assignment	(	const process_instance &	procId,
		const std::set< variable > &	bound_variables = `std::set<variable>()`
	)

inlineprivate

Definition at line 2086 of file linearise.cpp.

◆ upperpowerof2()

std::size_t specification_basic_type::upperpowerof2 ( std::size_t i )

inlineprivate

Definition at line 543 of file linearise.cpp.

◆ variables_are_equal_to_default_values()

data_expression specification_basic_type::variables_are_equal_to_default_values ( const variable_list & vl )

inlineprivate

Definition at line 5932 of file linearise.cpp.

◆ wraptime()

process_expression specification_basic_type::wraptime	(	const process_expression &	body,
		const data_expression &	time,
		const variable_list &	freevars
	)

inlineprivate

Definition at line 2202 of file linearise.cpp.

◆ xi()

bool specification_basic_type::xi	(	const action_list &	alpha,
		const action_list &	beta,
		comm_entry &	comm_table
	)

inlineprivate

Definition at line 8087 of file linearise.cpp.

Member Data Documentation

◆ acts

process::action_label_list specification_basic_type::acts

Definition at line 157 of file linearise.cpp.

◆ data

data_specification specification_basic_type::data

Definition at line 162 of file linearise.cpp.

◆ delta_process

process_identifier specification_basic_type::delta_process

private

Definition at line 183 of file linearise.cpp.

◆ enumeratedtypes

std::vector< enumeratedtype > specification_basic_type::enumeratedtypes

private

Definition at line 197 of file linearise.cpp.

◆ fresh_equation_added

bool specification_basic_type::fresh_equation_added

private

Definition at line 191 of file linearise.cpp.

◆ fresh_identifier_generator

set_identifier_generator specification_basic_type::fresh_identifier_generator

private

Definition at line 196 of file linearise.cpp.

◆ global_variables

std::set< variable > specification_basic_type::global_variables

Definition at line 158 of file linearise.cpp.

◆ initdatavars

variable_list specification_basic_type::initdatavars

Definition at line 160 of file linearise.cpp.

◆ objectdata

std::map< aterm, objectdatatype > specification_basic_type::objectdata

private

Definition at line 192 of file linearise.cpp.

◆ options

t_lin_options specification_basic_type::options

private

Definition at line 188 of file linearise.cpp.

◆ procs

std::vector< process_equation > specification_basic_type::procs

private

Definition at line 173 of file linearise.cpp.

◆ representedprocesses

std::vector< std::vector < process_instance_assignment > > specification_basic_type::representedprocesses

private

Definition at line 186 of file linearise.cpp.

◆ rewr

mcrl2::data::rewriter specification_basic_type::rewr

private

Definition at line 178 of file linearise.cpp.

◆ seq_varnames

std::vector< process_identifier > specification_basic_type::seq_varnames

private

Definition at line 184 of file linearise.cpp.

◆ stack_operations_list

stackoperations* specification_basic_type::stack_operations_list

private

Definition at line 198 of file linearise.cpp.

◆ stochastic_operator_is_being_used

bool specification_basic_type::stochastic_operator_is_being_used

private

Definition at line 190 of file linearise.cpp.

◆ tau_process

process_identifier specification_basic_type::tau_process

private

Definition at line 182 of file linearise.cpp.

◆ terminatedProcId

process_identifier specification_basic_type::terminatedProcId

private

Definition at line 180 of file linearise.cpp.

◆ terminationAction

action specification_basic_type::terminationAction

private

Definition at line 179 of file linearise.cpp.

◆ timeIsBeingUsed

bool specification_basic_type::timeIsBeingUsed

private

Definition at line 189 of file linearise.cpp.

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

lps/source/linearise.cpp

Classes

Public Member Functions

Public Attributes

Private Types

Private Member Functions

Static Private Member Functions

Private Attributes

Detailed Description

Member Enumeration Documentation

◆ state

◆ terminationstatus

◆ variableposition

Constructor & Destructor Documentation

◆ specification_basic_type() [1/2]

◆ specification_basic_type() [2/2]

◆ ~specification_basic_type()

Member Function Documentation

◆ action_list_to_process()

◆ actioncompare()

◆ adapt_multiaction_to_stack()

◆ adapt_multiaction_to_stack_rec()

◆ adapt_term_to_stack()

◆ adapt_termlist_to_stack()

◆ add_summands()

◆ addActionCondition()

◆ addcondition()

◆ addMultiAction()

◆ addString()

◆ AddTerminationActionIfNecessary()

◆ all_equal()

◆ allow_()

◆ allowblockcomposition()

◆ allowsingleaction()

◆ alphaconversion()

◆ alphaconversionterm()

◆ alphaconvert()

◆ alphaconvertprocess()

◆ alreadypresent()

◆ argscollect_regular()

◆ argscollect_regular2()

◆ bodytovarheadGNF()

◆ calculate_communication_merge()

◆ calculate_communication_merge_action_deadlock_summands()

◆ calculate_communication_merge_action_summands()

◆ calculate_communication_merge_deadlock_summands()

◆ calculate_left_merge()

◆ calculate_left_merge_action()

◆ calculate_left_merge_deadlock()

◆ can_communicate()

◆ canterminate_rec()

◆ canterminatebody() [1/2]

◆ canterminatebody() [2/2]

◆ check_assignment_list()

◆ check_real_variable_occurrence()

◆ check_valid_process_instance_assignment()

◆ cluster_actions()

◆ collect_sum_arg_arg_cond() [1/2]

◆ collect_sum_arg_arg_cond() [2/2]

◆ collectparameterlist()

◆ collectPcrlProcesses() [1/2]

◆ collectPcrlProcesses() [2/2]

◆ collectPcrlProcesses_term()

◆ collectsumlist()

◆ collectsumlistterm()

◆ combine_summand_lists()

◆ combine_ultimate_delays()

◆ communicationcomposition()

◆ complete_proc_identifier_map()

◆ construct_binary_case_tree()

◆ construct_binary_case_tree_rec()

◆ construct_renaming()

◆ containstime_rec()

◆ containstimebody() [1/2]

◆ containstimebody() [2/2]

◆ correctstatecond()

◆ create_case_function_on_enumeratedtype()

◆ create_enumeratedtype()

◆ create_regular_invocation()

◆ cut_off_unreachable_tail()

◆ declare_control_state()