specification_basic_type Class Reference

Classes
class	enumeratedtype
class	enumtype
struct	make_substitution
class	process_pid_pair
class	stacklisttype
class	stackoperations

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)
	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
using	variableposition = enum { first, later }
using	state = enum { alt_state, sum_state, seq_state, name_state, multiaction_state }
using	terminationstatus = enum { terminating, infinite }
using	variableposition = enum { first, later }
using	state = enum { alt_state, sum_state, seq_state, name_state, multiaction_state }
using	terminationstatus = enum { terminating, infinite }

Private Member Functions
bool	isDeltaAtZero (const process_expression &t)
template<class Expression , IsSubstitution Substitution>
Expression	replace_variables_capture_avoiding_alt (const Expression &e, Substitution &sigma)
void	detail_check_objectdata (const process_identifier &o) const
objectdatatype &	objectIndex (const process_identifier &o)
const objectdatatype &	objectIndex (const process_identifier &o) const
void	addString (const identifier_string &str)
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)
objectdatatype &	addMultiAction (const process_expression &multiAction, bool &isnew)
void	insertvariable (const variable &var, const bool mustbenew)
void	insertvariables (const variable_list &vars, const bool mustbenew)
template<data::IsSubstitution Substitution>
std::set< data::variable >	sigma_variables (const Substitution &sigma)
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) const
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)
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 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<IsSubstitution MutableSubstitution>
void	alphaconvertprocess (variable_list &sumvars, MutableSubstitution &sigma, const process_expression &p)
template<IsSubstitution MutableSubstitution>
void	alphaconvert (variable_list &sumvars, MutableSubstitution &sigma, const variable_list &occurvars, const data_expression_list &occurterms)
std::set< variable >	find_free_variables_process (const process_expression &p)
template<IsSubstitution Substitution>
assignment_list	substitute_assignmentlist (const assignment_list &assignments, const variable_list &parameters, const bool replacelhs, const bool replacerhs, Substitution &sigma)
bool	check_valid_process_instance_assignment (const process_identifier &id, const assignment_list &assignments)
template<IsSubstitution 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)
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)
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)
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, mutable_indexed_substitution<> &parameter_renaming)
variable_list	joinparameters (const variable_list &par1, const variable_list &par2, mutable_indexed_substitution<> &parameter_renaming)
variable_list	collectparameterlist (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) const
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 (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)
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) const
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	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)
assignment_list	make_optimised_assignment_list (const variable_list &parameters, const data_expression_list &resultnextstate, const variable_list &sum_vars, const variable_list &stoch_vars)
stochastic_action_summand	collect_sum_arg_arg_cond (const enumtype &e, const stochastic_action_summand_vector &action_summands, const variable_list &parameters)
deadlock_summand	collect_sum_arg_arg_cond (const enumtype &e, const deadlock_summand_vector &deadlock_summands, const variable_list &parameters)
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)
variable_list	construct_renaming (const variable_list &pars1, const variable_list &pars2, variable_list &pars3, variable_list &pars4, const bool unique=true)
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)
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)
bool	isDeltaAtZero (const process_expression &t)
template<class Expression , IsSubstitution Substitution>
Expression	replace_variables_capture_avoiding_alt (const Expression &e, Substitution &sigma)
void	detail_check_objectdata (const process_identifier &o) const
objectdatatype &	objectIndex (const process_identifier &o)
const objectdatatype &	objectIndex (const process_identifier &o) const
void	addString (const identifier_string &str)
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)
objectdatatype &	addMultiAction (const process_expression &multiAction, bool &isnew)
void	insertvariable (const variable &var, const bool mustbenew)
void	insertvariables (const variable_list &vars, const bool mustbenew)
template<data::IsSubstitution Substitution>
std::set< data::variable >	sigma_variables (const Substitution &sigma)
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) const
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)
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 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<IsSubstitution MutableSubstitution>
void	alphaconvertprocess (variable_list &sumvars, MutableSubstitution &sigma, const process_expression &p)
template<IsSubstitution MutableSubstitution>
void	alphaconvert (variable_list &sumvars, MutableSubstitution &sigma, const variable_list &occurvars, const data_expression_list &occurterms)
std::set< variable >	find_free_variables_process (const process_expression &p)
template<IsSubstitution Substitution>
assignment_list	substitute_assignmentlist (const assignment_list &assignments, const variable_list &parameters, const bool replacelhs, const bool replacerhs, Substitution &sigma)
bool	check_valid_process_instance_assignment (const process_identifier &id, const assignment_list &assignments)
template<IsSubstitution 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)
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)
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)
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, mutable_indexed_substitution<> &parameter_renaming)
variable_list	joinparameters (const variable_list &par1, const variable_list &par2, mutable_indexed_substitution<> &parameter_renaming)
variable_list	collectparameterlist (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) const
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 (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)
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) const
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	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)
assignment_list	make_optimised_assignment_list (const variable_list &parameters, const data_expression_list &resultnextstate, const variable_list &sum_vars, const variable_list &stoch_vars)
stochastic_action_summand	collect_sum_arg_arg_cond (const enumtype &e, const stochastic_action_summand_vector &action_summands, const variable_list &parameters)
deadlock_summand	collect_sum_arg_arg_cond (const enumtype &e, const deadlock_summand_vector &deadlock_summands, const variable_list &parameters)
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)
variable_list	construct_renaming (const variable_list &pars1, const variable_list &pars2, variable_list &pars3, variable_list &pars4, const bool unique=true)
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)
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 data_expression	real_times_optimized (const data_expression &r1, const data_expression &r2)
static process_expression	delta_at_zero ()
static process_expression	action_list_to_process (const action_list &ma)
static action_list	to_action_list (const process_expression &p)
static action_list	to_sorted_action_list (const process_expression &p)
	Convert the process expression to a sorted action list.
static action_label_list	getnames (const process_expression &multiAction)
static data_expression_list	getarguments (const action_list &multiAction)
static action_list	makemultiaction (const process::action_label_list &actionIds, const data_expression_list &args)
static std::size_t	upperpowerof2 (std::size_t i)
static bool	occursintermlist (const variable &var, const data_expression_list &r)
static assignment_list	filter_assignments (const assignment_list &assignments, const variable_list &parameters)
static bool	check_assignment_list (const assignment_list &assignments, const variable_list &parameters)
static assignment_list	sort_assignments (const assignment_list &ass, const variable_list &parameters)
static assignment_list	parameters_to_assignment_list (const variable_list &parameters, const std::set< variable > &variables_bound_in_sum)
static int	match_sequence (const std::vector< process_instance_assignment > &s1, const std::vector< process_instance_assignment > &s2, const bool regular2)
static process_identifier	get_last (const process_identifier &id, const std::map< process_identifier, process_identifier > &identifier_identifier_map)
static 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)
static void	complete_proc_identifier_map (std::map< process_identifier, process_identifier > &identifier_identifier_map)
static bool	occursin (const variable &name, const variable_list &pars)
static data_expression_list	extend (const data_expression &c, const data_expression_list &cl)
static bool	summandsCanBeClustered (const stochastic_action_summand &summand1, const stochastic_action_summand &summand2)
static data_expression	getRHSassignment (const variable &var, const assignment_list &as)
static sort_expression_list	getActionSorts (const action_list &actionlist)
static bool	occursinvarandremove (const variable &var, variable_list &vl)
template<typename List >
static sort_expression_list	get_sorts (const List &l)
static bool	check_real_variable_occurrence (const variable_list &sumvars, const data_expression &actiontime, const data_expression &condition)
static data_expression	real_times_optimized (const data_expression &r1, const data_expression &r2)
static process_expression	delta_at_zero ()
static process_expression	action_list_to_process (const action_list &ma)
static action_list	to_action_list (const process_expression &p)
static action_list	to_sorted_action_list (const process_expression &p)
	Convert the process expression to a sorted action list.
static action_label_list	getnames (const process_expression &multiAction)
static data_expression_list	getarguments (const action_list &multiAction)
static action_list	makemultiaction (const process::action_label_list &actionIds, const data_expression_list &args)
static std::size_t	upperpowerof2 (std::size_t i)
static bool	occursintermlist (const variable &var, const data_expression_list &r)
static assignment_list	filter_assignments (const assignment_list &assignments, const variable_list &parameters)
static bool	check_assignment_list (const assignment_list &assignments, const variable_list &parameters)
static assignment_list	sort_assignments (const assignment_list &ass, const variable_list &parameters)
static assignment_list	parameters_to_assignment_list (const variable_list &parameters, const std::set< variable > &variables_bound_in_sum)
static int	match_sequence (const std::vector< process_instance_assignment > &s1, const std::vector< process_instance_assignment > &s2, const bool regular2)
static process_identifier	get_last (const process_identifier &id, const std::map< process_identifier, process_identifier > &identifier_identifier_map)
static 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)
static void	complete_proc_identifier_map (std::map< process_identifier, process_identifier > &identifier_identifier_map)
static bool	occursin (const variable &name, const variable_list &pars)
static data_expression_list	extend (const data_expression &c, const data_expression_list &cl)
static bool	summandsCanBeClustered (const stochastic_action_summand &summand1, const stochastic_action_summand &summand2)
static data_expression	getRHSassignment (const variable &var, const assignment_list &as)
static sort_expression_list	getActionSorts (const action_list &actionlist)
static bool	occursinvarandremove (const variable &var, variable_list &vl)
template<typename List >
static sort_expression_list	get_sorts (const List &l)
static bool	check_real_variable_occurrence (const variable_list &sumvars, const data_expression &actiontime, const data_expression &condition)

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 = false
bool	stochastic_operator_is_being_used = false
bool	fresh_equation_added = false
std::map< aterm, objectdatatype >	objectdata
set_identifier_generator	fresh_identifier_generator
std::vector< enumeratedtype >	enumeratedtypes
stackoperations *	stack_operations_list

Detailed Description

Definition at line 131 of file linearise.cpp.

Member Typedef Documentation

state [1/2]

using specification_basic_type::state = enum { alt_state, sum_state, seq_state, name_state, multiaction_state }

private

Definition at line 2013 of file linearise.cpp.

state [2/2]

using specification_basic_type::state = enum { alt_state, sum_state, seq_state, name_state, multiaction_state }

private

Definition at line 2013 of file linearise.cpp.

terminationstatus [1/2]

using specification_basic_type::terminationstatus = enum { terminating, infinite }

private

Definition at line 2524 of file linearise.cpp.

terminationstatus [2/2]

using specification_basic_type::terminationstatus = enum { terminating, infinite }

private

Definition at line 2524 of file linearise.cpp.

variableposition [1/2]

using specification_basic_type::variableposition = enum { first, later }

private

Definition at line 1855 of file linearise.cpp.

variableposition [2/2]

using specification_basic_type::variableposition = enum { first, later }

private

Definition at line 1855 of file linearise.cpp.

Constructor & Destructor Documentation

specification_basic_type() [1/4]

specification_basic_type::specification_basic_type ( const specification_basic_type &  )

delete

specification_basic_type() [2/4]

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 178 of file linearise.cpp.

~specification_basic_type() [1/2]

specification_basic_type::~specification_basic_type ( )

inline

Definition at line 220 of file linearise.cpp.

specification_basic_type() [3/4]

specification_basic_type::specification_basic_type ( const specification_basic_type &  )

delete

specification_basic_type() [4/4]

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 178 of file linearise.cpp.

~specification_basic_type() [2/2]

specification_basic_type::~specification_basic_type ( )

inline

Definition at line 220 of file linearise.cpp.

Member Function Documentation

action_list_to_process() [1/2]

static process_expression specification_basic_type::action_list_to_process ( const action_list &  ma )

inlinestaticprivate

Definition at line 320 of file linearise.cpp.

action_list_to_process() [2/2]

static process_expression specification_basic_type::action_list_to_process ( const action_list &  ma )

inlinestaticprivate

Definition at line 320 of file linearise.cpp.

adapt_multiaction_to_stack() [1/2]

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

inlineprivate

Adapt multiactions to stack by traversing the list. Note: the result is sorted w.r.t. operator< on action.

Definition at line 4551 of file linearise.cpp.

adapt_multiaction_to_stack() [2/2]

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

inlineprivate

Adapt multiactions to stack by traversing the list. Note: the result is sorted w.r.t. operator< on action.

Definition at line 4551 of file linearise.cpp.

adapt_term_to_stack() [1/2]

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 4453 of file linearise.cpp.

adapt_term_to_stack() [2/2]

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 4453 of file linearise.cpp.

adapt_termlist_to_stack() [1/2]

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 4533 of file linearise.cpp.

adapt_termlist_to_stack() [2/2]

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 4533 of file linearise.cpp.

add_summands() [1/2]

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 5059 of file linearise.cpp.

add_summands() [2/2]

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 5059 of file linearise.cpp.

addcondition() [1/2]

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

inlineprivate

Definition at line 5736 of file linearise.cpp.

addcondition() [2/2]

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

inlineprivate

Definition at line 5736 of file linearise.cpp.

addMultiAction() [1/2]

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

inlineprivate

Definition at line 452 of file linearise.cpp.

addMultiAction() [2/2]

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

inlineprivate

Definition at line 452 of file linearise.cpp.

addString() [1/2]

void specification_basic_type::addString ( const identifier_string &  str )

inlineprivate

Definition at line 314 of file linearise.cpp.

addString() [2/2]

void specification_basic_type::addString ( const identifier_string &  str )

inlineprivate

Definition at line 314 of file linearise.cpp.

AddTerminationActionIfNecessary() [1/2]

void specification_basic_type::AddTerminationActionIfNecessary ( const stochastic_action_summand_vector &  summands )

inlineprivate

Definition at line 9908 of file linearise.cpp.

AddTerminationActionIfNecessary() [2/2]

void specification_basic_type::AddTerminationActionIfNecessary ( const stochastic_action_summand_vector &  summands )

inlineprivate

Definition at line 9908 of file linearise.cpp.

all_equal() [1/2]

template<class T >

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

inlineprivate

Definition at line 5851 of file linearise.cpp.

all_equal() [2/2]

template<class T >

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

inlineprivate

Definition at line 5851 of file linearise.cpp.

alphaconversion() [1/2]

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

inlineprivate

Definition at line 8693 of file linearise.cpp.

alphaconversion() [2/2]

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

inlineprivate

Definition at line 8693 of file linearise.cpp.

alphaconversionterm() [1/2]

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 8556 of file linearise.cpp.

alphaconversionterm() [2/2]

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 8556 of file linearise.cpp.

alphaconvert() [1/2]

template<IsSubstitution MutableSubstitution>

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

inlineprivate

Definition at line 1437 of file linearise.cpp.

alphaconvert() [2/2]

template<IsSubstitution MutableSubstitution>

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

inlineprivate

Definition at line 1437 of file linearise.cpp.

alphaconvertprocess() [1/2]

template<IsSubstitution MutableSubstitution>

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

inlineprivate

Definition at line 1410 of file linearise.cpp.

alphaconvertprocess() [2/2]

template<IsSubstitution MutableSubstitution>

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

inlineprivate

Definition at line 1410 of file linearise.cpp.

alreadypresent() [1/2]

bool specification_basic_type::alreadypresent ( variable &  var, const variable_list &  vl, mutable_indexed_substitution<> &  parameter_renaming  )

inlineprivate

Definition at line 3979 of file linearise.cpp.

alreadypresent() [2/2]

bool specification_basic_type::alreadypresent ( variable &  var, const variable_list &  vl, mutable_indexed_substitution<> &  parameter_renaming  )

inlineprivate

Definition at line 3979 of file linearise.cpp.

argscollect_regular() [1/2]

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 3015 of file linearise.cpp.

argscollect_regular() [2/2]

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 3015 of file linearise.cpp.

argscollect_regular2() [1/2]

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

inlineprivate

Definition at line 3032 of file linearise.cpp.

argscollect_regular2() [2/2]

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

inlineprivate

Definition at line 3032 of file linearise.cpp.

bodytovarheadGNF() [1/2]

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 2157 of file linearise.cpp.

bodytovarheadGNF() [2/2]

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 2157 of file linearise.cpp.

calculate_communication_merge() [1/2]

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 8001 of file linearise.cpp.

calculate_communication_merge() [2/2]

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 8001 of file linearise.cpp.

calculate_communication_merge_action_deadlock_summands() [1/2]

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 7846 of file linearise.cpp.

calculate_communication_merge_action_deadlock_summands() [2/2]

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 7846 of file linearise.cpp.

calculate_communication_merge_action_summands() [1/2]

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 7742 of file linearise.cpp.

calculate_communication_merge_action_summands() [2/2]

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 7742 of file linearise.cpp.

calculate_communication_merge_deadlock_summands() [1/2]

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 7905 of file linearise.cpp.

calculate_communication_merge_deadlock_summands() [2/2]

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 7905 of file linearise.cpp.

calculate_left_merge() [1/2]

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 7709 of file linearise.cpp.

calculate_left_merge() [2/2]

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 7709 of file linearise.cpp.

calculate_left_merge_action() [1/2]

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 7531 of file linearise.cpp.

calculate_left_merge_action() [2/2]

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 7531 of file linearise.cpp.

calculate_left_merge_deadlock() [1/2]

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 7609 of file linearise.cpp.

calculate_left_merge_deadlock() [2/2]

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 7609 of file linearise.cpp.

canterminate_rec() [1/2]

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

inlineprivate

Definition at line 9484 of file linearise.cpp.

canterminate_rec() [2/2]

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

inlineprivate

Definition at line 9484 of file linearise.cpp.

canterminatebody() [1/4]

bool specification_basic_type::canterminatebody ( const process_expression &  t )

inlineprivate

Definition at line 9504 of file linearise.cpp.

canterminatebody() [2/4]

bool specification_basic_type::canterminatebody ( const process_expression &  t )

inlineprivate

Definition at line 9504 of file linearise.cpp.

canterminatebody() [3/4]

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

inlineprivate

Definition at line 9367 of file linearise.cpp.

canterminatebody() [4/4]

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

inlineprivate

Definition at line 9367 of file linearise.cpp.

check_assignment_list() [1/2]

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

inlinestaticprivate

Definition at line 1489 of file linearise.cpp.

check_assignment_list() [2/2]

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

inlinestaticprivate

Definition at line 1489 of file linearise.cpp.

check_real_variable_occurrence() [1/2]

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

inlinestaticprivate

Definition at line 7155 of file linearise.cpp.

check_real_variable_occurrence() [2/2]

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

inlinestaticprivate

Definition at line 7155 of file linearise.cpp.

check_valid_process_instance_assignment() [1/2]

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

inlineprivate

Definition at line 1634 of file linearise.cpp.

check_valid_process_instance_assignment() [2/2]

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

inlineprivate

Definition at line 1634 of file linearise.cpp.

cluster_actions() [1/2]

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 6838 of file linearise.cpp.

cluster_actions() [2/2]

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 6838 of file linearise.cpp.

collect_sum_arg_arg_cond() [1/4]

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

inlineprivate

Definition at line 6573 of file linearise.cpp.

collect_sum_arg_arg_cond() [2/4]

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

inlineprivate

Definition at line 6573 of file linearise.cpp.

collect_sum_arg_arg_cond() [3/4]

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

inlineprivate

Definition at line 5952 of file linearise.cpp.

collect_sum_arg_arg_cond() [4/4]

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

inlineprivate

Definition at line 5952 of file linearise.cpp.

collectparameterlist() [1/2]

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

inlineprivate

Definition at line 4042 of file linearise.cpp.

collectparameterlist() [2/2]

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

inlineprivate

Definition at line 4042 of file linearise.cpp.

collectPcrlProcesses() [1/4]

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

inlineprivate

Definition at line 1193 of file linearise.cpp.

collectPcrlProcesses() [2/4]

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

inlineprivate

Definition at line 1193 of file linearise.cpp.

collectPcrlProcesses() [3/4]

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

inlineprivate

Definition at line 1176 of file linearise.cpp.

collectPcrlProcesses() [4/4]

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

inlineprivate

Definition at line 1176 of file linearise.cpp.

collectPcrlProcesses_term() [1/2]

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

inlineprivate

Definition at line 1067 of file linearise.cpp.

collectPcrlProcesses_term() [2/2]

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

inlineprivate

Definition at line 1067 of file linearise.cpp.

collectsumlist() [1/2]

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 5326 of file linearise.cpp.

collectsumlist() [2/2]

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 5326 of file linearise.cpp.

collectsumlistterm() [1/2]

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 5282 of file linearise.cpp.

collectsumlistterm() [2/2]

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 5282 of file linearise.cpp.

combine_summand_lists() [1/2]

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 8032 of file linearise.cpp.

combine_summand_lists() [2/2]

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 8032 of file linearise.cpp.

combine_ultimate_delays() [1/2]

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 7510 of file linearise.cpp.

combine_ultimate_delays() [2/2]

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 7510 of file linearise.cpp.

complete_proc_identifier_map() [1/2]

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

inlinestaticprivate

Definition at line 3761 of file linearise.cpp.

complete_proc_identifier_map() [2/2]

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

inlinestaticprivate

Definition at line 3761 of file linearise.cpp.

construct_binary_case_tree() [1/2]

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 5869 of file linearise.cpp.

construct_binary_case_tree() [2/2]

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 5869 of file linearise.cpp.

construct_binary_case_tree_rec() [1/2]

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 5814 of file linearise.cpp.

construct_binary_case_tree_rec() [2/2]

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 5814 of file linearise.cpp.

construct_renaming() [1/2]

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 7085 of file linearise.cpp.

construct_renaming() [2/2]

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 7085 of file linearise.cpp.

containstime_rec() [1/2]

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 8847 of file linearise.cpp.

containstime_rec() [2/2]

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 8847 of file linearise.cpp.

containstimebody() [1/4]

bool specification_basic_type::containstimebody ( const process_expression &  t )

inlineprivate

Definition at line 8879 of file linearise.cpp.

containstimebody() [2/4]

bool specification_basic_type::containstimebody ( const process_expression &  t )

inlineprivate

Definition at line 8879 of file linearise.cpp.

containstimebody() [3/4]

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 8727 of file linearise.cpp.

containstimebody() [4/4]

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 8727 of file linearise.cpp.

correctstatecond() [1/2]

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 4386 of file linearise.cpp.

correctstatecond() [2/2]

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 4386 of file linearise.cpp.

create_case_function_on_enumeratedtype() [1/2]

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

inlineprivate

Definition at line 5495 of file linearise.cpp.

create_case_function_on_enumeratedtype() [2/2]

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

inlineprivate

Definition at line 5495 of file linearise.cpp.

create_enumeratedtype() [1/2]

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

inlineprivate

Definition at line 5415 of file linearise.cpp.

create_enumeratedtype() [2/2]

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

inlineprivate

Definition at line 5415 of file linearise.cpp.

create_regular_invocation() [1/2]

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 3102 of file linearise.cpp.

create_regular_invocation() [2/2]

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 3102 of file linearise.cpp.

cut_off_unreachable_tail() [1/2]

process_expression specification_basic_type::cut_off_unreachable_tail ( const process_expression &  t )

inlineprivate

Definition at line 3074 of file linearise.cpp.

cut_off_unreachable_tail() [2/2]

process_expression specification_basic_type::cut_off_unreachable_tail ( const process_expression &  t )

inlineprivate

Definition at line 3074 of file linearise.cpp.

declare_control_state() [1/2]

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

inlineprivate

Definition at line 4069 of file linearise.cpp.

declare_control_state() [2/2]

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

inlineprivate

Definition at line 4069 of file linearise.cpp.

define_equations_for_case_function() [1/2]

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 5444 of file linearise.cpp.

define_equations_for_case_function() [2/2]

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 5444 of file linearise.cpp.

delta_at_zero() [1/2]

static process_expression specification_basic_type::delta_at_zero ( )

inlinestaticprivate

Definition at line 252 of file linearise.cpp.

delta_at_zero() [2/2]

static process_expression specification_basic_type::delta_at_zero ( )

inlinestaticprivate

Definition at line 252 of file linearise.cpp.

detail_check_objectdata() [1/2]

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

inlineprivate

Definition at line 281 of file linearise.cpp.

detail_check_objectdata() [2/2]

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

inlineprivate

Definition at line 281 of file linearise.cpp.

determine_process_status() [1/2]

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

inlineprivate

Definition at line 1031 of file linearise.cpp.

determine_process_status() [2/2]

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

inlineprivate

Definition at line 1031 of file linearise.cpp.

determine_process_statusterm() [1/2]

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

inlineprivate

Definition at line 792 of file linearise.cpp.

determine_process_statusterm() [2/2]

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

inlineprivate

Definition at line 792 of file linearise.cpp.

determinewhetherprocessescanterminate() [1/2]

void specification_basic_type::determinewhetherprocessescanterminate ( const process_identifier &  procId )

inlineprivate

Definition at line 9511 of file linearise.cpp.

determinewhetherprocessescanterminate() [2/2]

void specification_basic_type::determinewhetherprocessescanterminate ( const process_identifier &  procId )

inlineprivate

Definition at line 9511 of file linearise.cpp.

determinewhetherprocessescontaintime() [1/2]

bool specification_basic_type::determinewhetherprocessescontaintime ( const process_identifier &  procId )

inlineprivate

Definition at line 8887 of file linearise.cpp.

determinewhetherprocessescontaintime() [2/2]

bool specification_basic_type::determinewhetherprocessescontaintime ( const process_identifier &  procId )

inlineprivate

Definition at line 8887 of file linearise.cpp.

distribute_condition() [1/2]

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

inlineprivate

Definition at line 2614 of file linearise.cpp.

distribute_condition() [2/2]

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

inlineprivate

Definition at line 2614 of file linearise.cpp.

distribute_sum() [1/2]

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

inlineprivate

Definition at line 2816 of file linearise.cpp.

distribute_sum() [2/2]

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

inlineprivate

Definition at line 2816 of file linearise.cpp.

distribute_sum_over_a_stochastic_operator() [1/2]

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 2773 of file linearise.cpp.

distribute_sum_over_a_stochastic_operator() [2/2]

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 2773 of file linearise.cpp.

distributeActionOverConditions() [1/2]

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 2075 of file linearise.cpp.

distributeActionOverConditions() [2/2]

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 2075 of file linearise.cpp.

distributeTime() [1/2]

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 3269 of file linearise.cpp.

distributeTime() [2/2]

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 3269 of file linearise.cpp.

dummyparameterlist() [1/2]

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

inlineprivate

Definition at line 5007 of file linearise.cpp.

dummyparameterlist() [2/2]

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

inlineprivate

Definition at line 5007 of file linearise.cpp.

enumerate_distribution_and_sums() [1/2]

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 2699 of file linearise.cpp.

enumerate_distribution_and_sums() [2/2]

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 2699 of file linearise.cpp.

exists_variable_for_sequence() [1/2]

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

inlineprivate

Definition at line 2911 of file linearise.cpp.

exists_variable_for_sequence() [2/2]

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

inlineprivate

Definition at line 2911 of file linearise.cpp.

expand_process_instance_assignment() [1/4]

process_instance_assignment specification_basic_type::expand_process_instance_assignment ( const process_instance_assignment &  t )

inlineprivate

Definition at line 9603 of file linearise.cpp.

expand_process_instance_assignment() [2/4]

process_instance_assignment specification_basic_type::expand_process_instance_assignment ( const process_instance_assignment &  t )

inlineprivate

Definition at line 9603 of file linearise.cpp.

expand_process_instance_assignment() [3/4]

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 9574 of file linearise.cpp.

expand_process_instance_assignment() [4/4]

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 9574 of file linearise.cpp.

extend() [1/2]

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

inlinestaticprivate

Definition at line 5676 of file linearise.cpp.

extend() [2/2]

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

inlinestaticprivate

Definition at line 5676 of file linearise.cpp.

extend_conditions() [1/2]

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

inlineprivate

Definition at line 5696 of file linearise.cpp.

extend_conditions() [2/2]

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

inlineprivate

Definition at line 5696 of file linearise.cpp.

extract_names() [1/2]

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

inlineprivate

Definition at line 2931 of file linearise.cpp.

extract_names() [2/2]

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

inlineprivate

Definition at line 2931 of file linearise.cpp.

filter_assignments() [1/2]

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

inlinestaticprivate

Definition at line 1475 of file linearise.cpp.

filter_assignments() [2/2]

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

inlinestaticprivate

Definition at line 1475 of file linearise.cpp.

filter_vars_by_assignmentlist() [1/2]

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 1314 of file linearise.cpp.

filter_vars_by_assignmentlist() [2/2]

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 1314 of file linearise.cpp.

filter_vars_by_multiaction() [1/2]

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 1302 of file linearise.cpp.

filter_vars_by_multiaction() [2/2]

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 1302 of file linearise.cpp.

filter_vars_by_term() [1/2]

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 1203 of file linearise.cpp.

filter_vars_by_term() [2/2]

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 1203 of file linearise.cpp.

filter_vars_by_termlist() [1/2]

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 1290 of file linearise.cpp.

filter_vars_by_termlist() [2/2]

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 1290 of file linearise.cpp.

find_() [1/2]

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 4581 of file linearise.cpp.

find_() [2/2]

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 4581 of file linearise.cpp.

find_case_function() [1/2]

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

inlineprivate

Definition at line 5428 of file linearise.cpp.

find_case_function() [2/2]

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

inlineprivate

Definition at line 5428 of file linearise.cpp.

find_dummy_arguments() [1/2]

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 4635 of file linearise.cpp.

find_dummy_arguments() [2/2]

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 4635 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 1466 of file linearise.cpp.

find_free_variables_process() [2/2]

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

inlineprivate

Definition at line 1466 of file linearise.cpp.

findarguments() [1/2]

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 4614 of file linearise.cpp.

findarguments() [2/2]

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 4614 of file linearise.cpp.

generateLPEmCRL() [1/2]

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 8485 of file linearise.cpp.

generateLPEmCRL() [2/2]

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 8485 of file linearise.cpp.

generateLPEmCRLterm() [1/2]

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 8215 of file linearise.cpp.

generateLPEmCRLterm() [2/2]

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 8215 of file linearise.cpp.

generateLPEpCRL() [1/2]

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 6952 of file linearise.cpp.

generateLPEpCRL() [2/2]

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 6952 of file linearise.cpp.

get_fresh_variable() [1/2]

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

inlineprivate

Definition at line 2022 of file linearise.cpp.

get_fresh_variable() [2/2]

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

inlineprivate

Definition at line 2022 of file linearise.cpp.

get_last() [1/2]

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

inlinestaticprivate

Definition at line 3716 of file linearise.cpp.

get_last() [2/2]

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

inlinestaticprivate

Definition at line 3716 of file linearise.cpp.

get_sorts() [1/2]

template<typename List >

static sort_expression_list specification_basic_type::get_sorts ( const List &  l )

inlinestaticprivate

Definition at line 7149 of file linearise.cpp.

get_sorts() [2/2]

template<typename List >

static sort_expression_list specification_basic_type::get_sorts ( const List &  l )

inlinestaticprivate

Definition at line 7149 of file linearise.cpp.

getActionSorts() [1/2]

static sort_expression_list specification_basic_type::getActionSorts ( const action_list &  actionlist )

inlinestaticprivate

Definition at line 6827 of file linearise.cpp.

getActionSorts() [2/2]

static sort_expression_list specification_basic_type::getActionSorts ( const action_list &  actionlist )

inlinestaticprivate

Definition at line 6827 of file linearise.cpp.

getarguments() [1/2]

static data_expression_list specification_basic_type::getarguments ( const action_list &  multiAction )

inlinestaticprivate

Definition at line 421 of file linearise.cpp.

getarguments() [2/2]

static data_expression_list specification_basic_type::getarguments ( const action_list &  multiAction )

inlinestaticprivate

Definition at line 421 of file linearise.cpp.

getnames() [1/2]

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

inlinestaticprivate

Definition at line 364 of file linearise.cpp.

getnames() [2/2]

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

inlinestaticprivate

Definition at line 364 of file linearise.cpp.

getparameters() [1/2]

variable_list specification_basic_type::getparameters ( const process_expression &  multiAction )

inlineprivate

Definition at line 414 of file linearise.cpp.

getparameters() [2/2]

variable_list specification_basic_type::getparameters ( const process_expression &  multiAction )

inlineprivate

Definition at line 414 of file linearise.cpp.

getparameters_rec() [1/2]

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

inlineprivate

Definition at line 402 of file linearise.cpp.

getparameters_rec() [2/2]

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

inlineprivate

Definition at line 402 of file linearise.cpp.

getRHSassignment() [1/2]

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

inlinestaticprivate

Definition at line 5916 of file linearise.cpp.

getRHSassignment() [2/2]

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

inlinestaticprivate

Definition at line 5916 of file linearise.cpp.

getUltimateDelayCondition() [1/2]

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 7261 of file linearise.cpp.

getUltimateDelayCondition() [2/2]

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 7261 of file linearise.cpp.

getvar() [1/2]

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

inlineprivate

Definition at line 4258 of file linearise.cpp.

getvar() [2/2]

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

inlineprivate

Definition at line 4258 of file linearise.cpp.

insert_process_declaration() [1/2]

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 688 of file linearise.cpp.

insert_process_declaration() [2/2]

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 688 of file linearise.cpp.

insert_summand() [1/2]

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 5019 of file linearise.cpp.

insert_summand() [2/2]

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 5019 of file linearise.cpp.

insertAction() [1/2]

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

inlineprivate

Definition at line 659 of file linearise.cpp.

insertAction() [2/2]

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

inlineprivate

Definition at line 659 of file linearise.cpp.

insertvariable() [1/2]

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

inlineprivate

Definition at line 478 of file linearise.cpp.

insertvariable() [2/2]

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

inlineprivate

Definition at line 478 of file linearise.cpp.

insertvariables() [1/2]

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

inlineprivate

Definition at line 493 of file linearise.cpp.

insertvariables() [2/2]

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

inlineprivate

Definition at line 493 of file linearise.cpp.

is_global_variable() [1/2]

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

inlineprivate

Definition at line 4253 of file linearise.cpp.

is_global_variable() [2/2]

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

inlineprivate

Definition at line 4253 of file linearise.cpp.

isDeltaAtZero() [1/2]

bool specification_basic_type::isDeltaAtZero ( const process_expression &  t )

inlineprivate

Definition at line 257 of file linearise.cpp.

isDeltaAtZero() [2/2]

bool specification_basic_type::isDeltaAtZero ( const process_expression &  t )

inlineprivate

Definition at line 257 of file linearise.cpp.

joinparameters() [1/2]

variable_list specification_basic_type::joinparameters ( const variable_list &  par1, const variable_list &  par2, mutable_indexed_substitution<> &  parameter_renaming  )

inlineprivate

Definition at line 4018 of file linearise.cpp.

joinparameters() [2/2]

variable_list specification_basic_type::joinparameters ( const variable_list &  par1, const variable_list &  par2, mutable_indexed_substitution<> &  parameter_renaming  )

inlineprivate

Definition at line 4018 of file linearise.cpp.

linMergeMultiActionList() [1/2]

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

inlineprivate

Definition at line 774 of file linearise.cpp.

linMergeMultiActionList() [2/2]

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

inlineprivate

Definition at line 774 of file linearise.cpp.

linMergeMultiActionListProcess() [1/2]

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

inlineprivate

Definition at line 785 of file linearise.cpp.

linMergeMultiActionListProcess() [2/2]

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

inlineprivate

Definition at line 785 of file linearise.cpp.

make_binary_sums() [1/2]

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 5787 of file linearise.cpp.

make_binary_sums() [2/2]

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 5787 of file linearise.cpp.

make_initialstate() [1/2]

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 4963 of file linearise.cpp.

make_initialstate() [2/2]

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 4963 of file linearise.cpp.

make_optimised_assignment_list() [1/2]

assignment_list specification_basic_type::make_optimised_assignment_list ( const variable_list &  parameters, const data_expression_list &  resultnextstate, const variable_list &  sum_vars, const variable_list &  stoch_vars  )

inlineprivate

Definition at line 5933 of file linearise.cpp.

make_optimised_assignment_list() [2/2]

assignment_list specification_basic_type::make_optimised_assignment_list ( const variable_list &  parameters, const data_expression_list &  resultnextstate, const variable_list &  sum_vars, const variable_list &  stoch_vars  )

inlineprivate

Definition at line 5933 of file linearise.cpp.

make_parameters_and_sum_variables_unique() [1/2]

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 7400 of file linearise.cpp.

make_parameters_and_sum_variables_unique() [2/2]

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 7400 of file linearise.cpp.

make_parameters_rec() [1/2]

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

inlineprivate

Definition at line 377 of file linearise.cpp.

make_parameters_rec() [2/2]

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

inlineprivate

Definition at line 377 of file linearise.cpp.

make_pars() [1/2]

variable_list specification_basic_type::make_pars ( const sort_expression_list &  sortlist )

inlineprivate

Definition at line 2058 of file linearise.cpp.

make_pars() [2/2]

variable_list specification_basic_type::make_pars ( const sort_expression_list &  sortlist )

inlineprivate

Definition at line 2058 of file linearise.cpp.

make_pCRL_procs() [1/4]

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

inlineprivate

Definition at line 3650 of file linearise.cpp.

make_pCRL_procs() [2/4]

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

inlineprivate

Definition at line 3650 of file linearise.cpp.

make_pCRL_procs() [3/4]

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

inlineprivate

Definition at line 3639 of file linearise.cpp.

make_pCRL_procs() [4/4]

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

inlineprivate

Definition at line 3639 of file linearise.cpp.

make_procargs() [1/2]

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 4818 of file linearise.cpp.

make_procargs() [2/2]

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 4818 of file linearise.cpp.

make_procargs_regular() [1/2]

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 4706 of file linearise.cpp.

make_procargs_regular() [2/2]

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 4706 of file linearise.cpp.

make_procargs_stack() [1/2]

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 4765 of file linearise.cpp.

make_procargs_stack() [2/2]

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 4765 of file linearise.cpp.

make_unique_variables() [1/2]

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 7380 of file linearise.cpp.

make_unique_variables() [2/2]

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 7380 of file linearise.cpp.

makemultiaction() [1/2]

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

inlinestaticprivate

Definition at line 432 of file linearise.cpp.

makemultiaction() [2/2]

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

inlinestaticprivate

Definition at line 432 of file linearise.cpp.

makesingleultimatedelaycondition() [1/2]

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 7182 of file linearise.cpp.

makesingleultimatedelaycondition() [2/2]

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 7182 of file linearise.cpp.

match_sequence() [1/2]

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

inlinestaticprivate

Definition at line 2870 of file linearise.cpp.

match_sequence() [2/2]

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

inlinestaticprivate

Definition at line 2870 of file linearise.cpp.

merge_var() [1/2]

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 5752 of file linearise.cpp.

merge_var() [2/2]

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 5752 of file linearise.cpp.

mergeoccursin() [1/2]

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 5597 of file linearise.cpp.

mergeoccursin() [2/2]

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 5597 of file linearise.cpp.

minimize_set_of_reachable_process_identifiers() [1/2]

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 3801 of file linearise.cpp.

minimize_set_of_reachable_process_identifiers() [2/2]

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 3801 of file linearise.cpp.

newprocess() [1/2]

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 1883 of file linearise.cpp.

newprocess() [2/2]

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 1883 of file linearise.cpp.

objectIndex() [1/4]

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

inlineprivate

Definition at line 290 of file linearise.cpp.

objectIndex() [2/4]

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

inlineprivate

Definition at line 290 of file linearise.cpp.

objectIndex() [3/4]

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

inlineprivate

Definition at line 306 of file linearise.cpp.

objectIndex() [4/4]

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

inlineprivate

Definition at line 306 of file linearise.cpp.

obtain_initial_distribution() [1/2]

process_expression specification_basic_type::obtain_initial_distribution ( const process_identifier &  procId )

inlineprivate

Definition at line 9342 of file linearise.cpp.

obtain_initial_distribution() [2/2]

process_expression specification_basic_type::obtain_initial_distribution ( const process_identifier &  procId )

inlineprivate

Definition at line 9342 of file linearise.cpp.

obtain_initial_distribution_term() [1/2]

process_expression specification_basic_type::obtain_initial_distribution_term ( const process_expression &  t )

inlineprivate

Definition at line 9149 of file linearise.cpp.

obtain_initial_distribution_term() [2/2]

process_expression specification_basic_type::obtain_initial_distribution_term ( const process_expression &  t )

inlineprivate

Definition at line 9149 of file linearise.cpp.

occursin() [1/2]

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

inlinestaticprivate

Definition at line 4837 of file linearise.cpp.

occursin() [2/2]

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

inlinestaticprivate

Definition at line 4837 of file linearise.cpp.

occursinpCRLterm() [1/2]

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

inlineprivate

Definition at line 1328 of file linearise.cpp.

occursinpCRLterm() [2/2]

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

inlineprivate

Definition at line 1328 of file linearise.cpp.

occursintermlist() [1/4]

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

inlineprivate

Definition at line 1263 of file linearise.cpp.

occursintermlist() [2/4]

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

inlineprivate

Definition at line 1263 of file linearise.cpp.

occursintermlist() [3/4]

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

inlinestaticprivate

Definition at line 1251 of file linearise.cpp.

occursintermlist() [4/4]

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

inlinestaticprivate

Definition at line 1251 of file linearise.cpp.

occursinvarandremove() [1/2]

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

inlinestaticprivate

Definition at line 7056 of file linearise.cpp.

occursinvarandremove() [2/2]

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

inlinestaticprivate

Definition at line 7056 of file linearise.cpp.

operator=() [1/2]

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

delete

operator=() [2/2]

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

delete

parallelcomposition() [1/2]

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 8130 of file linearise.cpp.

parallelcomposition() [2/2]

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 8130 of file linearise.cpp.

parameters_that_occur_in_body() [1/2]

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

inlineprivate

Definition at line 1863 of file linearise.cpp.

parameters_that_occur_in_body() [2/2]

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

inlineprivate

Definition at line 1863 of file linearise.cpp.

parameters_to_assignment_list() [1/2]

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

inlinestaticprivate

Definition at line 2143 of file linearise.cpp.

parameters_to_assignment_list() [2/2]

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

inlinestaticprivate

Definition at line 2143 of file linearise.cpp.

parscollect() [1/2]

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

inlineprivate

Definition at line 2966 of file linearise.cpp.

parscollect() [2/2]

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

inlineprivate

Definition at line 2966 of file linearise.cpp.

pCRLrewrite() [1/2]

process_expression specification_basic_type::pCRLrewrite ( const process_expression &  t )

inlineprivate

Definition at line 594 of file linearise.cpp.

pCRLrewrite() [2/2]

process_expression specification_basic_type::pCRLrewrite ( const process_expression &  t )

inlineprivate

Definition at line 594 of file linearise.cpp.

processencoding() [1/4]

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

inlineprivate

Definition at line 4283 of file linearise.cpp.

processencoding() [2/4]

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

inlineprivate

Definition at line 4283 of file linearise.cpp.

processencoding() [3/4]

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

inlineprivate

Definition at line 4336 of file linearise.cpp.

processencoding() [4/4]

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

inlineprivate

Definition at line 4336 of file linearise.cpp.

procstorealGNF() [1/2]

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

inlineprivate

Definition at line 3611 of file linearise.cpp.

procstorealGNF() [2/2]

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

inlineprivate

Definition at line 3611 of file linearise.cpp.

procstorealGNFbody() [1/2]

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 3349 of file linearise.cpp.

procstorealGNFbody() [2/2]

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 3349 of file linearise.cpp.

procstorealGNFrec() [1/2]

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

inlineprivate

Definition at line 3547 of file linearise.cpp.

procstorealGNFrec() [2/2]

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

inlineprivate

Definition at line 3547 of file linearise.cpp.

procstovarheadGNF() [1/2]

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

inlineprivate

Definition at line 2499 of file linearise.cpp.

procstovarheadGNF() [2/2]

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

inlineprivate

Definition at line 2499 of file linearise.cpp.

push_regular() [1/2]

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 4677 of file linearise.cpp.

push_regular() [2/2]

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 4677 of file linearise.cpp.

push_stack() [1/2]

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 4735 of file linearise.cpp.

push_stack() [2/2]

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 4735 of file linearise.cpp.

pushdummy_regular() [1/2]

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

inlineprivate

Definition at line 4885 of file linearise.cpp.

pushdummy_regular() [2/2]

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

inlineprivate

Definition at line 4885 of file linearise.cpp.

pushdummy_regular_data_expressions() [1/2]

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

inlineprivate

Definition at line 4852 of file linearise.cpp.

pushdummy_regular_data_expressions() [2/2]

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

inlineprivate

Definition at line 4852 of file linearise.cpp.

pushdummy_stack() [1/2]

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

inlineprivate

Definition at line 4955 of file linearise.cpp.

pushdummy_stack() [2/2]

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

inlineprivate

Definition at line 4955 of file linearise.cpp.

pushdummyrec_stack() [1/2]

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 4917 of file linearise.cpp.

pushdummyrec_stack() [2/2]

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 4917 of file linearise.cpp.

putbehind() [1/2]

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

inlineprivate

Definition at line 2530 of file linearise.cpp.

putbehind() [2/2]

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

inlineprivate

Definition at line 2530 of file linearise.cpp.

real_times_optimized() [1/2]

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

inlinestaticprivate

Definition at line 234 of file linearise.cpp.

real_times_optimized() [2/2]

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

inlinestaticprivate

Definition at line 234 of file linearise.cpp.

remove_stochastic_operators_from_front() [1/2]

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 3904 of file linearise.cpp.

remove_stochastic_operators_from_front() [2/2]

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 3904 of file linearise.cpp.

replace_variables_capture_avoiding_alt() [1/2]

template<class Expression , IsSubstitution Substitution>

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

inlineprivate

Definition at line 273 of file linearise.cpp.

replace_variables_capture_avoiding_alt() [2/2]

template<class Expression , IsSubstitution Substitution>

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

inlineprivate

Definition at line 273 of file linearise.cpp.

representative_generator_internal() [1/2]

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

inlineprivate

Definition at line 4569 of file linearise.cpp.

representative_generator_internal() [2/2]

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

inlineprivate

Definition at line 4569 of file linearise.cpp.

rewrite_assignments() [1/2]

assignment_list specification_basic_type::rewrite_assignments ( const assignment_list &  t )

inlineprivate

Definition at line 557 of file linearise.cpp.

rewrite_assignments() [2/2]

assignment_list specification_basic_type::rewrite_assignments ( const assignment_list &  t )

inlineprivate

Definition at line 557 of file linearise.cpp.

RewriteAction() [1/2]

action specification_basic_type::RewriteAction ( const action &  t )

inlineprivate

Definition at line 567 of file linearise.cpp.

RewriteAction() [2/2]

action specification_basic_type::RewriteAction ( const action &  t )

inlineprivate

Definition at line 567 of file linearise.cpp.

RewriteMultAct() [1/2]

process_expression specification_basic_type::RewriteMultAct ( const process_expression &  t )

inlineprivate

Definition at line 577 of file linearise.cpp.

RewriteMultAct() [2/2]

process_expression specification_basic_type::RewriteMultAct ( const process_expression &  t )

inlineprivate

Definition at line 577 of file linearise.cpp.

RewriteProcess() [1/2]

process_instance_assignment specification_basic_type::RewriteProcess ( const process_instance_assignment &  t )

inlineprivate

Definition at line 572 of file linearise.cpp.

RewriteProcess() [2/2]

process_instance_assignment specification_basic_type::RewriteProcess ( const process_instance_assignment &  t )

inlineprivate

Definition at line 572 of file linearise.cpp.

RewriteTerm() [1/2]

data_expression specification_basic_type::RewriteTerm ( const data_expression &  t )

inlineprivate

Definition at line 533 of file linearise.cpp.

RewriteTerm() [2/2]

data_expression specification_basic_type::RewriteTerm ( const data_expression &  t )

inlineprivate

Definition at line 533 of file linearise.cpp.

RewriteTermList() [1/2]

data_expression_list specification_basic_type::RewriteTermList ( const data_expression_list &  t )

inlineprivate

Definition at line 547 of file linearise.cpp.

RewriteTermList() [2/2]

data_expression_list specification_basic_type::RewriteTermList ( const data_expression_list &  t )

inlineprivate

Definition at line 547 of file linearise.cpp.

searchProcDeclaration() [1/2]

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  ) const

inlineprivate

Definition at line 730 of file linearise.cpp.

searchProcDeclaration() [2/2]

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  ) const

inlineprivate

Definition at line 730 of file linearise.cpp.

set_proc_identifier_map() [1/2]

static 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  )

inlinestaticprivate

Definition at line 3738 of file linearise.cpp.

set_proc_identifier_map() [2/2]

static 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  )

inlinestaticprivate

Definition at line 3738 of file linearise.cpp.

SieveProcDataVarsAssignments() [1/2]

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

inline

Definition at line 9971 of file linearise.cpp.

SieveProcDataVarsAssignments() [2/2]

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

inline

Definition at line 9971 of file linearise.cpp.

SieveProcDataVarsSummands() [1/2]

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 9926 of file linearise.cpp.

SieveProcDataVarsSummands() [2/2]

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 9926 of file linearise.cpp.

sigma_variables() [1/2]

template<data::IsSubstitution Substitution>

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

inlineprivate

Definition at line 502 of file linearise.cpp.

sigma_variables() [2/2]

template<data::IsSubstitution Substitution>

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

inlineprivate

Definition at line 502 of file linearise.cpp.

sort_assignments() [1/2]

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

inlinestaticprivate

Definition at line 1614 of file linearise.cpp.

sort_assignments() [2/2]

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

inlinestaticprivate

Definition at line 1614 of file linearise.cpp.

split_body() [1/2]

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 9789 of file linearise.cpp.

split_body() [2/2]

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 9789 of file linearise.cpp.

split_process() [1/2]

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 9524 of file linearise.cpp.

split_process() [2/2]

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 9524 of file linearise.cpp.

splitmCRLandpCRLprocsAndAddTerminatedAction() [1/2]

process_identifier specification_basic_type::splitmCRLandpCRLprocsAndAddTerminatedAction ( const process_identifier &  procId )

inlineprivate

Definition at line 9898 of file linearise.cpp.

splitmCRLandpCRLprocsAndAddTerminatedAction() [2/2]

process_identifier specification_basic_type::splitmCRLandpCRLprocsAndAddTerminatedAction ( const process_identifier &  procId )

inlineprivate

Definition at line 9898 of file linearise.cpp.

storeact() [1/2]

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

inlineprivate

Definition at line 678 of file linearise.cpp.

storeact() [2/2]

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

inlineprivate

Definition at line 678 of file linearise.cpp.

storeinit() [1/2]

process_identifier specification_basic_type::storeinit ( const process_expression &  init )

inline

Definition at line 758 of file linearise.cpp.

storeinit() [2/2]

process_identifier specification_basic_type::storeinit ( const process_expression &  init )

inline

Definition at line 758 of file linearise.cpp.

storeprocs() [1/2]

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

inlineprivate

Definition at line 718 of file linearise.cpp.

storeprocs() [2/2]

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

inlineprivate

Definition at line 718 of file linearise.cpp.

substitute_assignmentlist() [1/2]

template<IsSubstitution 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 1509 of file linearise.cpp.

substitute_assignmentlist() [2/2]

template<IsSubstitution 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 1509 of file linearise.cpp.

substitute_pCRLproc() [1/2]

template<IsSubstitution Substitution>

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

inlineprivate

Definition at line 1669 of file linearise.cpp.

substitute_pCRLproc() [2/2]

template<IsSubstitution Substitution>

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

inlineprivate

Definition at line 1669 of file linearise.cpp.

summandsCanBeClustered() [1/2]

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

inlinestaticprivate

Definition at line 5880 of file linearise.cpp.

summandsCanBeClustered() [2/2]

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

inlinestaticprivate

Definition at line 5880 of file linearise.cpp.

to_action_list() [1/2]

static action_list specification_basic_type::to_action_list ( const process_expression &  p )

inlinestaticprivate

Convert the process expression to an action list. Note: The resulting actions are not sorted.

Definition at line 336 of file linearise.cpp.

to_action_list() [2/2]

static action_list specification_basic_type::to_action_list ( const process_expression &  p )

inlinestaticprivate

Convert the process expression to an action list. Note: The resulting actions are not sorted.

Definition at line 336 of file linearise.cpp.

to_regular_form() [1/2]

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 3187 of file linearise.cpp.

to_regular_form() [2/2]

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 3187 of file linearise.cpp.

to_sorted_action_list() [1/2]

static action_list specification_basic_type::to_sorted_action_list ( const process_expression &  p )

inlinestaticprivate

Convert the process expression to a sorted action list.

Definition at line 358 of file linearise.cpp.

to_sorted_action_list() [2/2]

static action_list specification_basic_type::to_sorted_action_list ( const process_expression &  p )

inlinestaticprivate

Convert the process expression to a sorted action list.

Definition at line 358 of file linearise.cpp.

transform() [1/2]

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 9995 of file linearise.cpp.

transform() [2/2]

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 9995 of file linearise.cpp.

transform_initial_distribution_term() [1/2]

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 8908 of file linearise.cpp.

transform_initial_distribution_term() [2/2]

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 8908 of file linearise.cpp.

transform_matching_list() [1/2]

data_expression specification_basic_type::transform_matching_list ( const variable_list &  matchinglist )

inlineprivate

Definition at line 5717 of file linearise.cpp.

transform_matching_list() [2/2]

data_expression specification_basic_type::transform_matching_list ( const variable_list &  matchinglist )

inlineprivate

Definition at line 5717 of file linearise.cpp.

transform_process_arguments() [1/4]

void specification_basic_type::transform_process_arguments ( const process_identifier &  procId )

inlineprivate

Definition at line 9645 of file linearise.cpp.

transform_process_arguments() [2/4]

void specification_basic_type::transform_process_arguments ( const process_identifier &  procId )

inlineprivate

Definition at line 9645 of file linearise.cpp.

transform_process_arguments() [3/4]

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

inlineprivate

Definition at line 9627 of file linearise.cpp.

transform_process_arguments() [4/4]

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

inlineprivate

Definition at line 9627 of file linearise.cpp.

transform_process_arguments_body() [1/2]

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 9653 of file linearise.cpp.

transform_process_arguments_body() [2/2]

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 9653 of file linearise.cpp.

transform_process_instance_to_process_instance_assignment() [1/2]

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 1814 of file linearise.cpp.

transform_process_instance_to_process_instance_assignment() [2/2]

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 1814 of file linearise.cpp.

upperpowerof2() [1/2]

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

inlinestaticprivate

Definition at line 518 of file linearise.cpp.

upperpowerof2() [2/2]

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

inlinestaticprivate

Definition at line 518 of file linearise.cpp.

variables_are_equal_to_default_values() [1/2]

data_expression specification_basic_type::variables_are_equal_to_default_values ( const variable_list &  vl )

inlineprivate

Definition at line 5684 of file linearise.cpp.

variables_are_equal_to_default_values() [2/2]

data_expression specification_basic_type::variables_are_equal_to_default_values ( const variable_list &  vl )

inlineprivate

Definition at line 5684 of file linearise.cpp.

wraptime() [1/2]

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

inlineprivate

Definition at line 1935 of file linearise.cpp.

wraptime() [2/2]

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

inlineprivate

Definition at line 1935 of file linearise.cpp.

Member Data Documentation

acts

process::action_label_list specification_basic_type::acts

Definition at line 134 of file linearise.cpp.

data

data_specification specification_basic_type::data

Definition at line 139 of file linearise.cpp.

delta_process

process_identifier specification_basic_type::delta_process

private

Definition at line 160 of file linearise.cpp.

enumeratedtypes

std::vector< enumeratedtype > specification_basic_type::enumeratedtypes

private

Definition at line 174 of file linearise.cpp.

fresh_equation_added

bool specification_basic_type::fresh_equation_added = false

private

Definition at line 168 of file linearise.cpp.

fresh_identifier_generator

set_identifier_generator specification_basic_type::fresh_identifier_generator

private

Definition at line 173 of file linearise.cpp.

global_variables

std::set< variable > specification_basic_type::global_variables

Definition at line 135 of file linearise.cpp.

initdatavars

variable_list specification_basic_type::initdatavars

Definition at line 137 of file linearise.cpp.

objectdata

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

private

Definition at line 169 of file linearise.cpp.

options

t_lin_options specification_basic_type::options

private

Definition at line 165 of file linearise.cpp.

procs

std::vector< process_equation > specification_basic_type::procs

private

Definition at line 150 of file linearise.cpp.

representedprocesses

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

private

Definition at line 163 of file linearise.cpp.

rewr

mcrl2::data::rewriter specification_basic_type::rewr

private

Definition at line 155 of file linearise.cpp.

seq_varnames

std::vector< process_identifier > specification_basic_type::seq_varnames

private

Definition at line 161 of file linearise.cpp.

stack_operations_list

stackoperations * specification_basic_type::stack_operations_list

private

Definition at line 175 of file linearise.cpp.

stochastic_operator_is_being_used

bool specification_basic_type::stochastic_operator_is_being_used = false

private

Definition at line 167 of file linearise.cpp.

tau_process

process_identifier specification_basic_type::tau_process

private

Definition at line 159 of file linearise.cpp.

terminatedProcId

process_identifier specification_basic_type::terminatedProcId

private

Definition at line 157 of file linearise.cpp.

terminationAction

action specification_basic_type::terminationAction

private

Definition at line 156 of file linearise.cpp.

timeIsBeingUsed

bool specification_basic_type::timeIsBeingUsed = false

private

Definition at line 166 of file linearise.cpp.

---

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

• lps/source/linearise.cpp