173 std::vector < process_equation >
procs;
202 const std::vector< process_equation >& ps,
205 const std::set < data::variable >& glob_vars,
307 template <
class Expression,
class Substitution>
326 throw mcrl2::runtime_error(
"Fail to recognize " + process::pp(o) +
". This is an internal error in the lineariser. ");
394 std::set < variable>& occurs_set)
404 if (
is_variable(e) && std::find(occurs_set.begin(),occurs_set.end(),e)==occurs_set.end())
406 const variable& v = atermpp::down_cast<variable>(e);
408 occurs_set.insert(v);
419 std::set < variable>& occurs_set)
432 std::set < variable > occurs_set;
441 result=
reverse(a.arguments()) + result;
452 std::size_t arity=l.sorts().size();
454 for (std::size_t i=0 ; i< arity; ++i,++e_walker)
456 assert(e_walker!=args.
end());
462 assert(e_walker==args.
end());
479 object.parameters=templist;
486 object.free_variables=std::set<variable>(
object.parameters.begin(),
object.parameters.end());
487 object.free_variables_defined=
true;
496 if (!
object.free_variables_defined)
499 object.free_variables_defined=
true;
501 return object.free_variables;
508 if (
objectdata.count(var.name())>0 && mustbenew)
527 template <
class SUBSTITUTION>
530 std::set<data::variable> result;
531 for (
typename SUBSTITUTION::const_iterator i =
sigma.begin(); i !=
sigma.end(); ++i)
533 std::set<data::variable> V = data::find_free_variables(i->second);
535 result.insert(V.begin(), V.end());
550 std::size_t powerof2=1;
551 for (; powerof2< i ; n++)
632 return new_then_case;
634 return if_then(new_cond,new_then_case);
649 return at(t1,atTime);
665 return RewriteAction(atermpp::down_cast<process::action>(t));
688 throw mcrl2::runtime_error(
"Action " + process::pp(actionId) +
" is added twice. This is an internal error in the lineariser. Please report. ");
718 const bool canterminate,
719 const bool containstime)
722 const std::string str=procId.
name();
727 throw mcrl2::runtime_error(
"Process " + process::pp(procId) +
" is added twice. This is an internal error in the lineariser. Please report. ");
733 object.processbody=body;
734 object.free_variables_defined=
false;
735 object.canterminate=canterminate;
736 object.containstime=containstime;
737 object.processstatus=s;
738 object.parameters=parameters;
750 e.formal_parameters(),
760 const bool canterminate,
761 const bool containstime,
764 for(
const std::pair<const aterm,objectdatatype>& d:
objectdata)
766 if (d.second.object==
proc &&
767 d.second.parameters==parameters &&
768 d.second.processbody==body &&
769 d.second.canterminate==canterminate &&
770 d.second.containstime==containstime &&
771 d.second.processstatus==s)
800 if (std::string(a1.
name())<std::string(a2.
name()))
848 for (
const action& a: ma1)
878 throw mcrl2::runtime_error(
"Choice operator occurs in a multi-action in " + process::pp(body) +
". The lineariser cannot handle such a pattern. ");
884 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs within the scope of a choice operator in " + process::pp(body) +
885 ". The lineariser cannot handle such processes. ");
894 throw mcrl2::runtime_error(
"Sequential operator occurs in a multi-action in " + process::pp(body) +
". The lineariser cannot handle such a pattern. ");
900 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs in the scope of a sequential operator in " + process::pp(body) +
". "
901 +
"The lineariser cannot handle such processes. ");
910 throw mcrl2::runtime_error(
"The parallel operator occurs in the scope of recursion, or the condition, sequential or choice operator in " +
911 process::pp(body) +
". The lineariser cannot handle such processes. ");
920 throw mcrl2::runtime_error(
"Cannot linearise because the specification contains a leftmerge. ");
927 throw mcrl2::runtime_error(
"If-then occurs in a multi-action in " + process::pp(body) +
". The lineariser cannot linearise this. ");
932 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs in the scope of the if-then operator in " + process::pp(body) +
". "
933 +
"The lineariser cannot handle such processes. ");
942 throw mcrl2::runtime_error(
"If-then-else occurs in a multi-action in " + process::pp(body) +
".");
948 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs in the scope of the if-then-else operator in " + process::pp(body) +
949 ". " +
"The lineariser cannot handle such processes. ");
961 throw mcrl2::runtime_error(
"The sum operator occurs within a multi-action in " + process::pp(body) +
". "
962 +
"The lineariser cannot handle such processes. ");
967 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs in the scope of the sum operator in " + process::pp(body) +
". "
968 "The lineariser cannot handle such processes. ");
982 throw mcrl2::runtime_error(
"Stochastic operator occurs within a multi-action in " + process::pp(body) +
".");
987 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs in the scope of the stochastic operator in " + process::pp(body) +
". "
988 +
"The lineariser cannot handle such processes. ");
997 throw mcrl2::runtime_error(
"The communication operator occurs in the scope of recursion, the condition, the sequential operation or the choice in "
998 + process::pp(body) +
". The lineariser cannot linearise such processes. ");
1006 throw mcrl2::runtime_error(
"Cannot linearise a specification with the bounded initialization operator.");
1014 throw mcrl2::runtime_error(
"Time operator occurs in a multi-action in " + process::pp(body) +
".");
1019 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs in the scope of a time operator in " + process::pp(body) +
"."
1020 +
"The lineariser cannot handle such processes. ");
1031 throw mcrl2::runtime_error(
"Other objects than multi-actions occur in the scope of a synch operator in " + process::pp(body) +
".");
1061 throw mcrl2::runtime_error(
"A hide operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +
".");
1071 throw mcrl2::runtime_error(
"A rename operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +
".");
1081 throw mcrl2::runtime_error(
"An allow operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +
".");
1091 throw mcrl2::runtime_error(
"A block operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +
".");
1108 s=
object.processstatus;
1112 object.processstatus=status;
1123 object.processstatus=s;
1131 object.processstatus=
pCRL;
1140 std::vector <process_identifier>& pcrlprocesses,
1141 std::set <process_identifier>& visited)
1250 std::vector <process_identifier>& pcrlprocesses,
1251 std::set <process_identifier>& visited)
1253 if (visited.count(procDecl)==0)
1255 visited.insert(procDecl);
1257 if (
object.processstatus==
pCRL)
1259 pcrlprocesses.push_back(procDecl);
1267 std::vector <process_identifier>& pcrlprocesses)
1269 std::set <process_identifier> visited;
1277 return data::search_free_variable(t, var);
1282 const std::set < variable >& vars_set,
1283 std::set < variable >& vars_result_set)
1287 const variable& v = atermpp::down_cast<variable>(t);
1288 if (vars_set.find(v)!=vars_set.end())
1290 vars_result_set.insert(v);
1324 const application& a=atermpp::down_cast<const application>(t);
1343 std::set<variable> assigned_variables;
1350 assigned_variables.insert(l.lhs());
1358 if (assigned_variables.count(var)==0)
1367 template <
typename Iterator>
1370 const Iterator& end,
1371 const std::set < variable >& vars_set,
1372 std::set < variable >& vars_result_set)
1374 for (; begin != end; ++begin)
1382 const std::set < variable >& vars_set,
1383 std::set < variable >& vars_result_set)
1385 for (
const action& ma: multiaction)
1395 const std::set < variable >& vars_set,
1396 std::set < variable >& vars_result_set)
1484 template <
class MutableSubstitution>
1487 MutableSubstitution&
sigma,
1500 newsumvars.push_back(newvar);
1505 newsumvars.push_back(var);
1508 sumvars=
variable_list(newsumvars.begin(), newsumvars.end());
1511 template <
class MutableSubstitution>
1514 MutableSubstitution&
sigma,
1575 free_variables_in_p.insert(v);
1584 free_variables_in_p.insert(v);
1595 for(
const variable& v:
static_cast<const sum&
>(p).variables())
1597 free_variables_in_p.erase(v);
1608 free_variables_in_p.insert(v);
1613 free_variables_in_p.erase(v);
1623 free_variables_in_p.insert(v);
1632 std::set<variable> parameter_set(parameters.
begin(),parameters.
end());
1638 free_variables_in_p.insert(v);
1640 parameter_set.erase(a.lhs());
1643 for(
const variable& v: parameter_set)
1645 free_variables_in_p.insert(v);
1652 for(
const variable& v: process::find_free_variables(p))
1654 free_variables_in_p.insert(v);
1661 for(
const variable& v: data::find_free_variables(
at(p).time_stamp()))
1663 free_variables_in_p.insert(v);
1735 std::set<variable> free_variables_in_p;
1737 return free_variables_in_p;
1746 if (std::find(parameters.
begin(),parameters.
end(),a.lhs())!=parameters.
end())
1748 result.push_back(a);
1762 if (i!=assignments.
end() && v==i->lhs())
1767 return i==assignments.
end();
1774 template <
class Substitution>
1778 const bool replacelhs,
1779 const bool replacerhs,
1780 Substitution&
sigma)
1800 assert(replacelhs==0 || replacelhs==1);
1801 assert(replacerhs==0 || replacerhs==1);
1802 if (parameters.
empty())
1804 assert(assignments.
empty());
1810 if (!assignments.
empty())
1822 lhs = atermpp::down_cast<variable>(
sigma(lhs));
1852 lhs = atermpp::down_cast<data::variable>(
sigma(lhs));
1882 std::map<variable,data_expression>assignment_map;
1885 assignment_map[a.lhs()]=a.rhs();
1891 const std::map<variable,data_expression>::const_iterator j=assignment_map.find(v);
1892 if (j!=assignment_map.end())
1894 result.push_back(
assignment(j->first,j->second));
1913 if (parameters.
empty())
1917 v=parameters.
front();
1934 template <
class Substitution>
1937 Substitution&
sigma)
1951 return choice(left,right);
2004 for( std::map < variable, data_expression >::const_iterator i=
sigma.begin(); i!=
sigma.end(); ++i)
2024 for( std::map < variable, data_expression >::const_iterator i=
sigma.begin(); i!=
sigma.end(); ++i)
2088 const std::set<variable>& bound_variables=std::set<variable>())
2098 assert(j!=rhss.
end());
2101 if (bound_variables.count(*i)>0)
2103 new_assignments.push_back(
assignment(*i,*j));
2108 new_assignments.push_back(
assignment(*i,*j));
2111 assert(j==rhss.
end());
2140 result.push_back(p);
2155 const bool canterminate,
2156 const bool containstime)
2167 static std::size_t numberOfNewProcesses=0, warningNumber=25;
2168 numberOfNewProcesses++;
2169 if (numberOfNewProcesses == warningNumber)
2175 mCRL2log(
mcrl2::log::warning) <<
" A possible unbounded loop can be avoided by using `regular2' or `stack' as linearisation method." << std::endl;
2179 mCRL2log(
mcrl2::log::warning) <<
" A possible unbounded loop can be avoided by using `stack' as the linearisation method." << std::endl;
2185 warningNumber=warningNumber*5;
2190 assert(std::string(p.
name()).size()>0);
2224 body1=
wraptime(body1,time1,sumvars+freevars);
2225 return sum(sumvars,body1);
2240 body1=
wraptime(body1,time1,sumvars+freevars);
2273 return at(body,time);
2276 throw mcrl2::runtime_error(
"Internal error: expect a pCRL process in wraptime " + process::pp(body));
2301 static std::map < int , std::map < variable,variable > > generated_variables;
2304 if (generated_variables[reuse_index].count(table_index_term)>0)
2306 old_variable=generated_variables[reuse_index][table_index_term];
2312 generated_variables[reuse_index][table_index_term]=old_variable;
2314 return old_variable;
2323 if (sortlist.
empty())
2340 const std::set<variable>& variables_bound_in_sum)
2361 if_then(restterm).then_case(),
2362 freevars,variables_bound_in_sum),
2367 freevars,variables_bound_in_sum));
2383 const data_expression& c=down_cast<if_then_else>(restterm).condition();
2389 freevars,variables_bound_in_sum),
2394 freevars,variables_bound_in_sum));
2407 if (variables_bound_in_sum.count(v)>0)
2421 const std::set<variable>& variables_bound_in_sum)
2440 return choice(body1,body2);
2460 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
2461 variables_bound_in_sum1.insert(sumvars.
begin(),sumvars.
end());
2471 return sum(sumvars,body1);
2494 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
2495 variables_bound_in_sum1.insert(sumvars.
begin(),sumvars.
end());
2512 const data_expression& condition=down_cast<if_then>(body).condition();
2532 const data_expression& condition=down_cast<if_then_else>(body).condition();
2632 return seq(body1,body2);
2663 object.process_representing_action=tempvar;
2667 action(body).arguments()));
2697 object.process_representing_action=tempvar;
2711 first,variables_bound_in_sum);
2714 body1=
wraptime(body1,time,freevars);
2755 throw mcrl2::runtime_error(
"unexpected process format in bodytovarheadGNF " + process::pp(body) +
".");
2770 std::set<variable> variables_bound_in_sum;
2777 variables_bound_in_sum);
2778 object.processbody=result;
2837 return seq(body1,body2);
2842 return seq(body1,body2);
2847 return seq(body1,body2);
2857 return seq(body1,body2);
2863 return seq(body1,body2);
2866 throw mcrl2::runtime_error(
"Internal error. Unexpected process format in putbehind " + process::pp(body1) +
".");
2884 return if_then(condition,body1);
2936 return if_then(condition,body1);
2939 throw mcrl2::runtime_error(
"Internal error. Unexpected process format in distribute condition " + process::pp(body1) +
".");
2964 throw mcrl2::runtime_error(
"The use of the rewriter must be allowed to distribute a sum operator over a distribution.");
2971 std::vector < data_expression_vector > new_data_vector;
2975 throw mcrl2::runtime_error(
"Cannot distribute a sum variable of non finite sort " +
pp(v.sort()) +
" over a distribution, which is required for linearisation.");
2983 new_dv.push_back(d);
2984 new_data_vector.push_back(new_dv);
2988 data_vector.swap(new_data_vector);
2991 assert(!data_vector.empty());
2996 bool result_defined=
false;
3002 data_expression_vector::const_iterator i=d.begin();
3013 resulting_body=
choice(resulting_body, d1);
3014 resulting_distribution=
sort_real::times(resulting_distribution,new_distribution);
3015 resulting_stochastic_variables=resulting_stochastic_variables + vl;
3020 resulting_distribution=new_distribution;
3021 resulting_stochastic_variables=vl;
3022 result_defined=
true;
3027 return stochastic_operator(resulting_stochastic_variables, resulting_distribution, resulting_body);
3065 stochastic_variables + inner_stoch_vars,
3069 throw mcrl2::runtime_error(
"Internal error. Unexpected process format in distribute_sum " + process::pp(body) +
".");
3093 return sum(sumvars,body1);
3102 return sum(sumvars+inner_sumvars,new_body1);
3122 throw mcrl2::runtime_error(
"Internal error. Unexpected process format in distribute_sum " + process::pp(body1) +
".");
3127 const std::vector < process_instance_assignment >& s1,
3128 const std::vector < process_instance_assignment >& s2,
3129 const bool regular2)
3137 std::vector < process_instance_assignment >::const_iterator i2=s2.begin();
3138 for (std::vector < process_instance_assignment >::const_iterator i1=s1.begin();
3139 i1!=s1.end(); ++i1,++i2)
3147 if (i1->identifier()!=i2->identifier())
3168 const std::vector < process_instance_assignment >& process_names,
3171 std::vector < std::vector < process_instance_assignment > >::const_iterator rwalker=
representedprocesses.begin();
3172 for (std::vector < process_identifier >::const_iterator walker=
seq_varnames.begin();
3189 std::vector < process_instance_assignment >& result)
3193 result.push_back(atermpp::down_cast<process_instance_assignment>(sequence));
3209 result.push_back(atermpp::down_cast<process_instance_assignment>(
first));
3211 if (
object.canterminate)
3219 throw mcrl2::runtime_error(
"Internal error. Expected sequence of process names (1) " + process::pp(sequence) +
".");
3241 if (
object.canterminate)
3250 assert(j!=new_pars.
end());
3256 assert(std::set<variable>(result.
begin(),result.
end()).size()==result.
size());
3266 throw mcrl2::runtime_error(
"Internal error. Expected a sequence of process names (2) " + process::pp(oldbody) +
".");
3273 const std::set<variable>& variables_bound_in_sum)
3297 std::map<variable,data_expression>
sigma;
3300 sigma[a.lhs()]=a.rhs();
3306 assert(!vl.
empty());
3319 if (
object.canterminate)
3323 return first_assignment;
3326 throw mcrl2::runtime_error(
"Internal error. Expected a sequence of process names (3) " + process::pp(t) +
".");
3346 if (
object.canterminate)
3353 throw mcrl2::runtime_error(
"Internal error. Expected a sequence of process names (4) " + process::pp(t) +
".");
3359 std::vector <process_identifier>& todo,
3361 const std::set<variable>& variables_bound_in_sum)
3372 std::set<variable> variables_bound_in_sum_new=variables_bound_in_sum;
3381 std::vector < process_instance_assignment > process_names;
3383 assert(!process_names.empty());
3385 if (process_names.size()==1)
3396 throw mcrl2::runtime_error(
"Internal error. Expected a sequence of process names " + process::pp(sequence) +
".");
3424 todo.push_back(new_process);
3444 std::vector <process_identifier>& todo,
3446 const std::set<variable>& variables_bound_in_sum)
3481 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
3482 variables_bound_in_sum1.insert(sumvars.
begin(),sumvars.
end());
3488 variables_bound_in_sum1));
3503 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
3504 variables_bound_in_sum1.insert(sumvars.
begin(),sumvars.
end());
3512 variables_bound_in_sum1));
3546 body1=
distributeTime(body1,time1,sumvars+freevars,timecondition);
3547 return sum(sumvars,body1);
3560 new_body=
distributeTime(new_body,time1,sumvars+freevars,timecondition);
3597 return at(body,time);
3600 throw mcrl2::runtime_error(
"Internal error: expect a pCRL process in distributeTime " + process::pp(body) +
".");
3607 std::vector <process_identifier>& todo,
3611 const std::set <variable>& variables_bound_in_sum)
3629 variables_bound_in_sum);
3632 at(body).time_stamp(),
3640 regular,mode,freevars,variables_bound_in_sum);
3642 regular,mode,freevars,variables_bound_in_sum);
3643 return choice(body1,body2);
3649 todo,regular,mode,freevars,variables_bound_in_sum);
3651 todo,regular,mode,freevars,variables_bound_in_sum);
3653 if ((regular) && (v==
first))
3665 todo,regular,mode,freevars,variables_bound_in_sum),
3673 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
3674 variables_bound_in_sum1.insert(sumvars.
begin(),sumvars.
end());
3677 todo,regular,mode,sumvars+freevars,variables_bound_in_sum1));
3684 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
3685 variables_bound_in_sum1.insert(sumvars.
begin(),sumvars.
end());
3690 todo,regular,mode,sumvars+freevars,variables_bound_in_sum1));
3723 if (
object.processstatus==
mCRL)
3735 sigma[a.lhs()]=a.rhs();
3759 todo,regular,mode,freevars,variables_bound_in_sum);
3761 todo,regular,mode,freevars,variables_bound_in_sum);
3797 throw mcrl2::runtime_error(
"unexpected process format in procstorealGNF " + process::pp(body) +
".");
3805 std::vector <process_identifier>& todo,
3816 if (
object.processstatus==
pCRL)
3819 std::set<variable> variables_bound_in_sum;
3821 todo,regular,
pCRL,
object.parameters,variables_bound_in_sum);
3822 if (
object.processstatus!=
GNFbusy)
3827 object.processbody=t;
3828 object.processstatus=
GNF;
3832 if (
object.processstatus==
mCRL)
3835 std::set<variable> variables_bound_in_sum;
3837 regular,
mCRL,
object.parameters,variables_bound_in_sum);
3850 if ((
object.processstatus==
GNFbusy)||
3851 (
object.processstatus==
GNF)||
3858 if (
object.processstatus==
mCRLbusy)
3869 std::vector <process_identifier> todo;
3870 todo.push_back(procsIdDecl);
3871 for (; !todo.empty() ;)
3895 std::set<process_identifier>& reachable_process_identifiers)
3897 if (reachable_process_identifiers.count(
id)==0)
3899 reachable_process_identifiers.insert(
id);
3906 std::set<process_identifier>& reachable_process_identifiers)
3942 make_pCRL_procs(atermpp::down_cast<process_instance_assignment>(t).identifier(), reachable_process_identifiers);
3951 throw mcrl2::runtime_error(
"unexpected process format " + process::pp(t) +
" in make_pCRL_procs");
3976 const std::map< process_identifier, process_identifier >::const_iterator i=identifier_identifier_map.find(target_id);
3977 if (i==identifier_identifier_map.end())
3983 target_id=i->second;
3992 std::map< process_identifier, process_identifier >& identifier_identifier_map,
4004 if (id1==initial_process)
4010 identifier_identifier_map[id1]=id2;
4016 std::map< process_identifier, process_identifier > new_identifier_identifier_map;
4017 for(
const std::pair<const process_identifier, process_identifier >& p: identifier_identifier_map)
4019 new_identifier_identifier_map[p.first]=
get_last(p.second,identifier_identifier_map);
4021 identifier_identifier_map.swap(new_identifier_identifier_map);
4024 typedef std::pair< const process_identifier, process_identifier > identifier_identifier_pair;
4025 for(
const identifier_identifier_pair& p: identifier_identifier_map)
4027 assert(identifier_identifier_map.count(p.second)==0);
4036 const std::map< process_identifier, process_identifier >&
m_map;
4044 const std::map< process_identifier, process_identifier >::const_iterator i=
m_map.find(
id);
4053 std::set< process_identifier >
4057 assert(reachable_process_identifiers.count(initial_process)>0);
4058 typedef std::pair< variable_list, process_expression > parameters_process_pair;
4059 typedef std::map< std::pair< variable_list, process_expression >,
process_identifier > mapping_type;
4060 typedef std::pair<const std::pair< variable_list, process_expression >,
process_identifier > mapping_type_pair;
4063 mapping_type process_mapping;
4064 std::map< process_identifier, process_identifier > identifier_identifier_map;
4068 const parameters_process_pair p(
object.parameters,
object.processbody);
4069 mapping_type::const_iterator i=process_mapping.find(p);
4070 if (i==process_mapping.end())
4072 process_mapping[p]=id;
4081 while (!identifier_identifier_map.empty())
4087 std::map< process_identifier, process_identifier > new_identifier_identifier_map;
4088 mapping_type new_process_mapping;
4089 for(
const mapping_type_pair& p: process_mapping)
4093 mapping_type::const_iterator i=new_process_mapping.find(p_new);
4094 if (i==new_process_mapping.end())
4096 new_process_mapping[p_new]=
sigma(p.second);
4104 identifier_identifier_map.swap(new_identifier_identifier_map);
4105 process_mapping.swap(new_process_mapping);
4116 std::set< process_identifier > result;
4117 for(
const mapping_type_pair& p: process_mapping)
4119 result.insert(p.second);
4121 object.processbody=p.first.second;
4123 assert(result.count(initial_process)>0);
4163 std::set< process_identifier >
4165 const std::set< process_identifier >& reachable_process_identifiers,
4170 std::map< process_identifier, process_pid_pair > processes_with_stochastic_distribution_first;
4171 std::set< process_identifier > result;
4178 processes_with_stochastic_distribution_first.insert(std::pair< process_identifier, process_pid_pair >(p,
process_pid_pair(proc_,p)));
4191 vars +
object.parameters,
4192 process::replace_variables_capture_avoiding_with_an_identifier_generator(
proc.operand(),
4200 processes_with_stochastic_distribution_first.insert(
4201 std::pair< process_identifier, process_pid_pair >
4208 result.insert(newproc);
4226 initial_process_id=processes_with_stochastic_distribution_first.at(initial_process_id).process_id();
4259 assert(var.name()!=var1.
name());
4300 const std::set < process_identifier >& pCRLprocs)
4348 constructors.push_back(sc_emptystack);
4351 stacksort=data::normalize_sorts(stack_sort_alias,spec.
data);
4355 const std::vector< data::function_symbol > projection_functions =
4357 pop=projection_functions.back();
4358 getstate=projection_functions.front();
4408 const std::set < process_identifier >& pCRLprocs,
4409 const bool singlecontrolstate)
4411 assert(pCRLprocs.size()>0);
4435 if (!singlecontrolstate)
4462 (spec.
options.
binary?std::string(
"binary"):std::string(
"an enumerated type")));
4505 walker!=
stack.parameters.end() ; ++walker,++getmappings)
4511 assert(getmappings!=
stack.opns->get.end());
4554 for (; k>0 ; k--, ++boolean_state_variables)
4604 for (; k>0 ; k--, ++boolean_state_variables)
4623 const std::set < process_identifier >& pCRLproc,
4706 if (std::find(vars.
begin(),vars.
end(),t)!=vars.
end())
4713 if (std::find(stochastic_variables.
begin(),stochastic_variables.
end(),t)!=stochastic_variables.
end())
4721 return getvar(atermpp::down_cast<variable>(t),
stack);
4727 const application&a=atermpp::down_cast<application>(t);
4735 const abstraction& abs_t=down_cast<abstraction>(t);
4767 template <
typename Iterator>
4770 const Iterator& end,
4776 for (; begin != end; ++begin)
4799 act.arguments().begin(),
4800 act.arguments().end(),
4833 const std::set<variable>& free_variables_in_body,
4852 if (free_variables_in_body.find(s)==free_variables_in_body.end())