specification_basic_type

class specification_basic_type

Private types

type specification_basic_type::state

Values:

• alt_state

• sum_state
• seq_state
• name_state
• multiaction_state

type specification_basic_type::terminationstatus

Values:

• terminating

• infinite

type specification_basic_type::variableposition

Values:

• first

• later

Public attributes

process::action_label_list specification_basic_type::acts

data_specification specification_basic_type::data

std::set<variable> specification_basic_type::global_variables

variable_list specification_basic_type::initdatavars

Private attributes

process_identifier specification_basic_type::delta_process

std::vector<enumeratedtype> specification_basic_type::enumeratedtypes

bool specification_basic_type::fresh_equation_added

set_identifier_generator specification_basic_type::fresh_identifier_generator

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

t_lin_options specification_basic_type::options

std::vector<process_equation> specification_basic_type::procs

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

mcrl2::data::rewriter specification_basic_type::rewr

std::vector<process_identifier> specification_basic_type::seq_varnames

stackoperations *specification_basic_type::stack_operations_list

bool specification_basic_type::stochastic_operator_is_being_used

process_identifier specification_basic_type::tau_process

process_identifier specification_basic_type::terminatedProcId

action specification_basic_type::terminationAction

bool specification_basic_type::timeIsBeingUsed

Public member functions

specification_basic_type &operator=(const specification_basic_type&) = delete

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

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)

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(const specification_basic_type&) = delete

process_identifier storeinit(const process_expression &init)

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

Private member functions

process_expression action_list_to_process(const action_list &ma)

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

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

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

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

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

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)

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

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

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

void addString(const identifier_string &str)

void AddTerminationActionIfNecessary(const stochastic_action_summand_vector &summands)

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

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

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

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

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

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

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

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

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

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

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 bodytovarheadGNF(const process_expression &body, const state s, const variable_list &freevars, const variableposition v, const std::set<variable> &variables_bound_in_sum)

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

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

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

bool canterminatebody(const process_expression &t)

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

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

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

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

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

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

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

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

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

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

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)

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

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 communicationcomposition(const communication_expression_list &communications, const action_name_multiset_list &allowlist1, const bool is_allow, const bool is_block, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)

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

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)

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)

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

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 containstimebody(const process_expression &t, bool *stable, std::set<process_identifier> &visited, bool allowrecursion, bool &contains_if_then)

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

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

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

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 cut_off_unreachable_tail(const process_expression &t)

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

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

process_expression delta_at_zero(void)

void detail_check_objectdata(const aterm_appl &o) const

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

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

void determinewhetherprocessescanterminate(const process_identifier &procId)

bool determinewhetherprocessescontaintime(const process_identifier &procId)

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

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

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 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 distributeTime(const process_expression &body, const data_expression &time, const variable_list &freevars, data_expression &timecondition)

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

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

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

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

process_instance_assignment expand_process_instance_assignment(const process_instance_assignment &t)

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

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

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

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

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

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)

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_term(const data_expression &t, const std::set<variable> &vars_set, std::set<variable> &vars_result_set)

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

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::function_symbol find_case_function(std::size_t index, const sort_expression &sort)

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)

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

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

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)

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)

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.

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

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)

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

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

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

sort_expression_list get_sorts(const List &l)

sort_expression_list getActionSorts(const action_list &actionlist)

data_expression_list getarguments(const action_list &multiAction)

process::action_label_list getnames(const process_expression &multiAction)

variable_list getparameters(const process_expression &multiAction)

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

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

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

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

void guarantee_that_parameters_have_unique_type(const process_identifier &procId)

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

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

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

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

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

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 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 insert_timed_delta_summand(const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const deadlock_summand &s)

objectdatatype &insertAction(const action_label &actionId)

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

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

bool is_global_variable(const data_expression &d) const

bool isDeltaAtZero(const process_expression &t)

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

action_list linInsertActionInMultiActionList(const action &act, action_list multiAction)

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

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

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

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)

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 = "")

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

variable_list make_pars(const sort_expression_list &sortlist)

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

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

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)

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

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

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

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

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

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)

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

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)

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

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

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

objectdatatype &objectIndex(const aterm_appl &o)

const objectdatatype &objectIndex(const aterm_appl &o) const

process_expression obtain_initial_distribution(const process_identifier &procId)

process_expression obtain_initial_distribution_term(const process_expression &t)

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

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

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

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

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

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

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

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)

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

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

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

process_expression pCRLrewrite(const process_expression &t)

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

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)

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

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 procstovarheadGNF(const std::vector<process_identifier> &procs)

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

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)

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)

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

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

data_expression_list pushdummy_stack(const variable_list &parameters, 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)

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

data_expression real_one()

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

data_expression real_zero()

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)

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

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

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

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

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

assignment_list rewrite_assignments(const assignment_list &t)

action RewriteAction(const action &t)

process_expression RewriteMultAct(const process_expression &t)

process_instance_assignment RewriteProcess(const process_instance_assignment &t)

data_expression RewriteTerm(const data_expression &t)

data_expression_list RewriteTermList(const data_expression_list &t)

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

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)

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

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

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 split_process(const process_identifier &procId, std::map<process_identifier, process_identifier> &visited_id, std::map<process_expression, process_expression> &visited_proc)

process_identifier splitmCRLandpCRLprocsAndAddTerminatedAction(const process_identifier &procId)

void storeact(const process::action_label_list &acts)

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

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

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

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

action_list to_action_list(const process_expression &p)

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 transform_initial_distribution_term(const process_expression &t, const std::map<process_identifier, process_pid_pair> &processes_with_initial_distribution)

data_expression transform_matching_list(const variable_list &matchinglist)

void transform_process_arguments(const process_identifier &procId)

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

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

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

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

data_expression variables_are_equal_to_default_values(const variable_list &vl)

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

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

Private static member functions

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

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

static action_name_multiset sort_action_labels(const action_name_multiset &actionlabels)

static action_name_multiset_list sort_multi_action_labels(const action_name_multiset_list &l)