mCRL2
Loading...
Searching...
No Matches
specification_basic_type Member List

This is the complete list of members for specification_basic_type, including all inherited members.

action_list_to_process(const action_list &ma)specification_basic_typeinlineprivatestatic
actsspecification_basic_type
adapt_multiaction_to_stack(const action_list &multiAction, const stacklisttype &stack, const variable_list &vars)specification_basic_typeinlineprivate
adapt_term_to_stack(const data_expression &t, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)specification_basic_typeinlineprivate
adapt_termlist_to_stack(Iterator begin, const Iterator &end, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
addcondition(const variable_list &matchinglist, const data_expression_list &conditionlist)specification_basic_typeinlineprivate
addMultiAction(const process_expression &multiAction, bool &isnew)specification_basic_typeinlineprivate
addString(const identifier_string &str)specification_basic_typeinlineprivate
AddTerminationActionIfNecessary(const stochastic_action_summand_vector &summands)specification_basic_typeinlineprivate
all_equal(const atermpp::term_list< T > &l)specification_basic_typeinlineprivate
alphaconversion(const process_identifier &procId, const variable_list &parameters)specification_basic_typeinlineprivate
alphaconversionterm(const process_expression &t, const variable_list &parameters, maintain_variables_in_rhs< mutable_map_substitution<> > sigma)specification_basic_typeinlineprivate
alphaconvert(variable_list &sumvars, MutableSubstitution &sigma, const variable_list &occurvars, const data_expression_list &occurterms)specification_basic_typeinlineprivate
alphaconvertprocess(variable_list &sumvars, MutableSubstitution &sigma, const process_expression &p)specification_basic_typeinlineprivate
alreadypresent(variable &var, const variable_list &vl)specification_basic_typeinlineprivatestatic
alt_state enum valuespecification_basic_typeprivate
argscollect_regular(const process_expression &t, const variable_list &vl, const std::set< variable > &variables_bound_in_sum)specification_basic_typeinlineprivate
argscollect_regular2(const process_expression &t, variable_list &vl)specification_basic_typeinlineprivate
bodytovarheadGNF(const process_expression &body, const state s, const variable_list &freevars, const variableposition v, const std::set< variable > &variables_bound_in_sum)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
canterminate_rec(const process_identifier &procId, bool &stable, std::set< process_identifier > &visited)specification_basic_typeinlineprivate
canterminatebody(const process_expression &t, bool &stable, std::set< process_identifier > &visited, const bool allowrecursion)specification_basic_typeinlineprivate
canterminatebody(const process_expression &t)specification_basic_typeinlineprivate
check_assignment_list(const assignment_list &assignments, const variable_list &parameters)specification_basic_typeinlineprivatestatic
check_real_variable_occurrence(const variable_list &sumvars, const data_expression &actiontime, const data_expression &condition)specification_basic_typeinlineprivatestatic
check_valid_process_instance_assignment(const process_identifier &id, const assignment_list &assignments)specification_basic_typeinlineprivate
cluster_actions(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const variable_list &pars)specification_basic_typeinlineprivate
collect_sum_arg_arg_cond(const enumtype &e, std::size_t n, const stochastic_action_summand_vector &action_summands, const variable_list &parameters)specification_basic_typeinlineprivate
collect_sum_arg_arg_cond(const enumtype &e, std::size_t n, const deadlock_summand_vector &deadlock_summands, const variable_list &parameters)specification_basic_typeinlineprivate
collectparameterlist(const std::set< process_identifier > &pCRLprocs)specification_basic_typeinlineprivate
collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)specification_basic_typeinlineprivate
collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses)specification_basic_typeinlineprivate
collectPcrlProcesses_term(const process_expression &body, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
combine_ultimate_delays(const lps::detail::ultimate_delay &delay1, const lps::detail::ultimate_delay &delay2)specification_basic_typeinlineprivate
complete_proc_identifier_map(std::map< process_identifier, process_identifier > &identifier_identifier_map)specification_basic_typeinlineprivatestatic
construct_binary_case_tree(std::size_t n, const variable_list &sums, data_expression_list terms, const sort_expression &termsort, const enumtype &e)specification_basic_typeinlineprivate
construct_binary_case_tree_rec(std::size_t n, const variable_list &sums, data_expression_list &terms, const sort_expression &termsort, const enumtype &e)specification_basic_typeinlineprivate
construct_renaming(const variable_list &pars1, const variable_list &pars2, variable_list &pars3, variable_list &pars4, const bool unique=true)specification_basic_typeinlineprivate
containstime_rec(const process_identifier &procId, bool *stable, std::set< process_identifier > &visited, bool &contains_if_then)specification_basic_typeinlineprivate
containstimebody(const process_expression &t, bool *stable, std::set< process_identifier > &visited, bool allowrecursion, bool &contains_if_then)specification_basic_typeinlineprivate
containstimebody(const process_expression &t)specification_basic_typeinlineprivate
correctstatecond(const process_identifier &procId, const std::set< process_identifier > &pCRLproc, const stacklisttype &stack, int regular)specification_basic_typeinlineprivate
create_case_function_on_enumeratedtype(const sort_expression &sort, const std::size_t enumeratedtype_index)specification_basic_typeinlineprivate
create_enumeratedtype(const std::size_t n)specification_basic_typeinlineprivate
create_regular_invocation(process_expression sequence, std::vector< process_identifier > &todo, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)specification_basic_typeinlineprivate
cut_off_unreachable_tail(const process_expression &t)specification_basic_typeinlineprivate
dataspecification_basic_type
declare_control_state(const std::set< process_identifier > &pCRLprocs)specification_basic_typeinlineprivate
define_equations_for_case_function(const std::size_t index, const data::function_symbol &functionname, const sort_expression &sort)specification_basic_typeinlineprivate
delta_at_zero()specification_basic_typeinlineprivatestatic
delta_processspecification_basic_typeprivate
detail_check_objectdata(const aterm &o) constspecification_basic_typeinlineprivate
determine_process_status(const process_identifier &procDecl, const processstatustype status)specification_basic_typeinlineprivate
determine_process_statusterm(const process_expression &body, const processstatustype status)specification_basic_typeinlineprivate
determinewhetherprocessescanterminate(const process_identifier &procId)specification_basic_typeinlineprivate
determinewhetherprocessescontaintime(const process_identifier &procId)specification_basic_typeinlineprivate
distribute_condition(const process_expression &body1, const data_expression &condition)specification_basic_typeinlineprivate
distribute_sum(const variable_list &sumvars, const process_expression &body1)specification_basic_typeinlineprivate
distribute_sum_over_a_stochastic_operator(const variable_list &sumvars, const variable_list &stochastic_variables, const data_expression &distribution, const process_expression &body)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
distributeTime(const process_expression &body, const data_expression &time, const variable_list &freevars, data_expression &timecondition)specification_basic_typeinlineprivate
dummyparameterlist(const stacklisttype &stack, const bool singlestate)specification_basic_typeinlineprivate
enumerate_distribution_and_sums(const variable_list &sumvars, const variable_list &stochvars, const data_expression &distribution, const process_expression &body)specification_basic_typeinlineprivate
enumeratedtypesspecification_basic_typeprivate
exists_variable_for_sequence(const std::vector< process_instance_assignment > &process_names, process_identifier &result)specification_basic_typeinlineprivate
expand_process_instance_assignment(const process_instance_assignment &t, std::set< process_identifier > &visited_processes)specification_basic_typeinlineprivate
expand_process_instance_assignment(const process_instance_assignment &t)specification_basic_typeinlineprivate
extend(const data_expression &c, const data_expression_list &cl)specification_basic_typeinlineprivatestatic
extend_conditions(const variable &var, const data_expression_list &conditionlist)specification_basic_typeinlineprivate
extract_names(const process_expression &sequence, std::vector< process_instance_assignment > &result)specification_basic_typeinlineprivate
filter_assignments(const assignment_list &assignments, const variable_list &parameters)specification_basic_typeinlineprivatestatic
filter_vars_by_assignmentlist(const assignment_list &assignments, const variable_list &parameters, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)specification_basic_typeinlineprivate
filter_vars_by_multiaction(const action_list &multiaction, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)specification_basic_typeinlineprivate
filter_vars_by_term(const data_expression &t, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)specification_basic_typeinlineprivate
filter_vars_by_termlist(Iterator begin, const Iterator &end, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
find_case_function(std::size_t index, const sort_expression &sort) constspecification_basic_typeinlineprivate
find_dummy_arguments(const variable_list &parlist, const assignment_list &args, const std::set< variable > &free_variables_in_body, const variable_list &stochastic_variables)specification_basic_typeinlineprivate
find_free_variables_process(const process_expression &p, std::set< variable > &free_variables_in_p)specification_basic_typeinlineprivate
find_free_variables_process(const process_expression &p)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
first enum valuespecification_basic_typeprivate
fresh_equation_addedspecification_basic_typeprivate
fresh_identifier_generatorspecification_basic_typeprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
get_free_variables(objectdatatype &object)specification_basic_typeinlineprivate
get_fresh_variable(const std::string &s, const sort_expression &sort, const int reuse_index=-1)specification_basic_typeinlineprivate
get_last(const process_identifier &id, const std::map< process_identifier, process_identifier > &identifier_identifier_map)specification_basic_typeinlineprivatestatic
get_sorts(const List &l)specification_basic_typeinlineprivatestatic
getActionSorts(const action_list &actionlist)specification_basic_typeinlineprivatestatic
getarguments(const action_list &multiAction)specification_basic_typeinlineprivatestatic
getnames(const process_expression &multiAction)specification_basic_typeinlineprivatestatic
getparameters(const process_expression &multiAction)specification_basic_typeinlineprivate
getparameters_rec(const process_expression &multiAction, std::set< variable > &occurs_set)specification_basic_typeinlineprivate
getRHSassignment(const variable &var, const assignment_list &as)specification_basic_typeinlineprivatestatic
getUltimateDelayCondition(const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands, const variable_list &freevars)specification_basic_typeinlineprivate
getvar(const variable &var, const stacklisttype &stack) constspecification_basic_typeinlineprivate
global_variablesspecification_basic_type
guarantee_that_parameters_have_unique_type(const process_identifier &procId, std::set< process_identifier > &visited_processes, std::set< identifier_string > &used_variable_names, maintain_variables_in_rhs< mutable_map_substitution<> > &parameter_mapping, std::set< variable > &variables_in_lhs_of_parameter_mapping)specification_basic_typeinlineprivate
guarantee_that_parameters_have_unique_type(const process_identifier &procId)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
hide_(const identifier_string_list &hidelist, const action_list &multiaction)specification_basic_typeinlineprivatestatic
hidecomposition(const identifier_string_list &hidelist, stochastic_action_summand_vector &action_summands)specification_basic_typeinlineprivatestatic
infinite enum valuespecification_basic_typeprivate
initdatavarsspecification_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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
insertAction(const action_label &actionId)specification_basic_typeinlineprivate
insertvariable(const variable &var, const bool mustbenew)specification_basic_typeinlineprivate
insertvariables(const variable_list &vars, const bool mustbenew)specification_basic_typeinlineprivate
is_global_variable(const data_expression &d) constspecification_basic_typeinlineprivate
isDeltaAtZero(const process_expression &t)specification_basic_typeinlineprivate
joinparameters(const variable_list &par1, const variable_list &par2)specification_basic_typeinlineprivatestatic
later enum valuespecification_basic_typeprivate
linMergeMultiActionList(const action_list &ma1, const action_list &ma2)specification_basic_typeinlineprivate
linMergeMultiActionListProcess(const process_expression &ma1, const process_expression &ma2)specification_basic_typeinlineprivate
make_binary_sums(std::size_t n, const sort_expression &enumtypename, data_expression &condition, const variable_list &tail)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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="")specification_basic_typeinlineprivate
make_parameters_rec(const data_expression_list &l, std::set< variable > &occurs_set)specification_basic_typeinlineprivate
make_pars(const sort_expression_list &sortlist)specification_basic_typeinlineprivate
make_pCRL_procs(const process_identifier &id, std::set< process_identifier > &reachable_process_identifiers)specification_basic_typeinlineprivate
make_pCRL_procs(const process_expression &t, std::set< process_identifier > &reachable_process_identifiers)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
make_procargs_regular(const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const bool singlestate, const variable_list &stochastic_variables)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
make_unique_variables(const variable_list &var_list, const std::string &hint)specification_basic_typeinlineprivate
makemultiaction(const process::action_label_list &actionIds, const data_expression_list &args)specification_basic_typeinlineprivatestatic
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)specification_basic_typeinlineprivate
match_sequence(const std::vector< process_instance_assignment > &s1, const std::vector< process_instance_assignment > &s2, const bool regular2)specification_basic_typeinlineprivatestatic
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)specification_basic_typeinlineprivate
mergeoccursin(variable &var, const variable_list &v, variable_list &matchinglist, variable_list &pars, data_expression_list &args, const variable_list &process_parameters)specification_basic_typeinlineprivate
minimize_set_of_reachable_process_identifiers(const std::set< process_identifier > &reachable_process_identifiers, const process_identifier &initial_process)specification_basic_typeinlineprivate
multiaction_state enum valuespecification_basic_typeprivate
name_state enum valuespecification_basic_typeprivate
newprocess(const variable_list &parameters, const process_expression &body, const processstatustype ps, const bool canterminate, const bool containstime)specification_basic_typeinlineprivate
objectdataspecification_basic_typeprivate
objectIndex(const aterm &o)specification_basic_typeinlineprivate
objectIndex(const aterm &o) constspecification_basic_typeinlineprivate
obtain_initial_distribution(const process_identifier &procId)specification_basic_typeinlineprivate
obtain_initial_distribution_term(const process_expression &t)specification_basic_typeinlineprivate
occursin(const variable &name, const variable_list &pars)specification_basic_typeinlineprivatestatic
occursinpCRLterm(const variable &var, const process_expression &p, const bool strict)specification_basic_typeinlineprivate
occursintermlist(const variable &var, const data_expression_list &r)specification_basic_typeinlineprivatestatic
occursintermlist(const variable &var, const assignment_list &r, const process_identifier &proc_name) constspecification_basic_typeinlineprivate
occursinvarandremove(const variable &var, variable_list &vl)specification_basic_typeinlineprivatestatic
operator=(const specification_basic_type &)=deletespecification_basic_type
optionsspecification_basic_typeprivate
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)specification_basic_typeinlineprivate
parameters_that_occur_in_body(const variable_list &parameters, const process_expression &body)specification_basic_typeinlineprivate
parameters_to_assignment_list(const variable_list &parameters, const std::set< variable > &variables_bound_in_sum)specification_basic_typeinlineprivatestatic
parscollect(const process_expression &oldbody, process_expression &newbody)specification_basic_typeinlineprivate
pCRLrewrite(const process_expression &t)specification_basic_typeinlineprivate
processencoding(std::size_t i, const assignment_list &t1, const stacklisttype &stack)specification_basic_typeinlineprivate
processencoding(std::size_t i, const data_expression_list &t1, const stacklisttype &stack)specification_basic_typeinlineprivate
procsspecification_basic_typeprivate
procstorealGNF(const process_identifier &procsIdDecl, const bool regular)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
procstorealGNFrec(const process_identifier &procIdDecl, const variableposition v, std::vector< process_identifier > &todo, const bool regular)specification_basic_typeinlineprivate
procstovarheadGNF(const std::vector< process_identifier > &procs)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
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)specification_basic_typeinlineprivate
pushdummy_regular(const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)specification_basic_typeinlineprivate
pushdummy_regular_data_expressions(const variable_list &pars, const stacklisttype &stack)specification_basic_typeinlineprivate
pushdummy_stack(const variable_list &parameters, const stacklisttype &stack, const variable_list &stochastic_variables)specification_basic_typeinlineprivate
pushdummyrec_stack(const variable_list &totalpars, const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)specification_basic_typeinlineprivate
putbehind(const process_expression &body1, const process_expression &body2)specification_basic_typeinlineprivate
real_times_optimized(const data_expression &r1, const data_expression &r2)specification_basic_typeinlineprivatestatic
remove_stochastic_operators_from_front(const std::set< process_identifier > &reachable_process_identifiers, process_identifier &initial_process_id, stochastic_distribution &initial_stochastic_distribution)specification_basic_typeinlineprivate
replace_variables_capture_avoiding_alt(const Expression &e, Substitution &sigma)specification_basic_typeinlineprivate
representative_generator_internal(const sort_expression &s, const bool allow_dont_care_var=true)specification_basic_typeinlineprivate
representedprocessesspecification_basic_typeprivate
rewrspecification_basic_typeprivate
rewrite_assignments(const assignment_list &t)specification_basic_typeinlineprivate
RewriteAction(const action &t)specification_basic_typeinlineprivate
RewriteMultAct(const process_expression &t)specification_basic_typeinlineprivate
RewriteProcess(const process_instance_assignment &t)specification_basic_typeinlineprivate
RewriteTerm(const data_expression &t)specification_basic_typeinlineprivate
RewriteTermList(const data_expression_list &t)specification_basic_typeinlineprivate
searchProcDeclaration(const variable_list &parameters, const process_expression &body, const processstatustype s, const bool canterminate, const bool containstime, process_identifier &p) constspecification_basic_typeinlineprivate
seq_state enum valuespecification_basic_typeprivate
seq_varnamesspecification_basic_typeprivate
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)specification_basic_typeinlineprivatestatic
SieveProcDataVarsAssignments(const std::set< variable > &vars, const data_expression_list &initial_state_expressions)specification_basic_typeinline
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_typeinline
sigma_variables(const SUBSTITUTION &sigma)specification_basic_typeinlineprivate
sort_assignments(const assignment_list &ass, const variable_list &parameters)specification_basic_typeinlineprivatestatic
specification_basic_type(const specification_basic_type &)=deletespecification_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)specification_basic_typeinline
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)specification_basic_typeinlineprivate
split_process(const process_identifier &procId, std::map< process_identifier, process_identifier > &visited_id, std::map< process_expression, process_expression > &visited_proc)specification_basic_typeinlineprivate
splitmCRLandpCRLprocsAndAddTerminatedAction(const process_identifier &procId)specification_basic_typeinlineprivate
stack_operations_listspecification_basic_typeprivate
state enum namespecification_basic_typeprivate
stochastic_operator_is_being_usedspecification_basic_typeprivate
storeact(const process::action_label_list &acts)specification_basic_typeinlineprivate
storeinit(const process_expression &init)specification_basic_typeinline
storeprocs(const std::vector< process_equation > &procs)specification_basic_typeinlineprivate
substitute_assignmentlist(const assignment_list &assignments, const variable_list &parameters, const bool replacelhs, const bool replacerhs, Substitution &sigma)specification_basic_typeinlineprivate
substitute_pCRLproc(const process_expression &p, Substitution &sigma)specification_basic_typeinlineprivate
sum_state enum valuespecification_basic_typeprivate
summandsCanBeClustered(const stochastic_action_summand &summand1, const stochastic_action_summand &summand2)specification_basic_typeinlineprivatestatic
tau_processspecification_basic_typeprivate
terminatedProcIdspecification_basic_typeprivate
terminating enum valuespecification_basic_typeprivate
terminationActionspecification_basic_typeprivate
terminationstatus enum namespecification_basic_typeprivate
timeIsBeingUsedspecification_basic_typeprivate
to_action_list(const process_expression &p)specification_basic_typeinlineprivatestatic
to_regular_form(const process_expression &t, std::vector< process_identifier > &todo, const variable_list &freevars, const std::set< variable > &variables_bound_in_sum)specification_basic_typeinlineprivate
to_sorted_action_list(const process_expression &p)specification_basic_typeinlineprivatestatic
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_typeinline
transform_initial_distribution_term(const process_expression &t, const std::map< process_identifier, process_pid_pair > &processes_with_initial_distribution)specification_basic_typeinlineprivate
transform_matching_list(const variable_list &matchinglist)specification_basic_typeinlineprivate
transform_process_arguments(const process_identifier &procId, std::set< process_identifier > &visited_processes)specification_basic_typeinlineprivate
transform_process_arguments(const process_identifier &procId)specification_basic_typeinlineprivate
transform_process_arguments_body(const process_expression &t, const std::set< variable > &bound_variables, std::set< process_identifier > &visited_processes)specification_basic_typeinlineprivate
transform_process_instance_to_process_instance_assignment(const process_instance &procId, const std::set< variable > &bound_variables=std::set< variable >())specification_basic_typeinlineprivate
upperpowerof2(std::size_t i)specification_basic_typeinlineprivatestatic
variableposition enum namespecification_basic_typeprivate
variables_are_equal_to_default_values(const variable_list &vl)specification_basic_typeinlineprivate
wraptime(const process_expression &body, const data_expression &time, const variable_list &freevars)specification_basic_typeinlineprivate
~specification_basic_type()specification_basic_typeinline