14
15
16
17
18
19
20
21
22
23
24
25
26
38#include "mcrl2/atermpp/aterm.h"
39#include "mcrl2/data/substitutions/maintain_variables_in_rhs.h"
40#include "mcrl2/data/fourier_motzkin.h"
41#include "mcrl2/data/enumerator.h"
42#include "mcrl2/data/real_utilities.h"
45#include "mcrl2/lps/constelm.h"
46#include "mcrl2/lps/linearise.h"
47#include "mcrl2/lps/linearise_allow_block.h"
48#include "mcrl2/lps/linearise_communication.h"
49#include "mcrl2/lps/linearise_hide.h"
50#include "mcrl2/lps/linearise_rename.h"
51#include "mcrl2/lps/linearise_utility.h"
52#include "mcrl2/lps/replace_capture_avoiding_with_an_identifier_generator.h"
53#include "mcrl2/lps/sumelm.h"
55#include "mcrl2/lps/detail/ultimate_delay.h"
58#include "mcrl2/process/alphabet_reduce.h"
59#include "mcrl2/process/balance_nesting_depth.h"
60#include "mcrl2/process/process_expression.h"
66using namespace mcrl2::
core;
68using namespace mcrl2::
data;
70using namespace mcrl2::
lps;
75using processstatustype =
enum
92using objecttype =
enum
113
122 return process::find_free_variables(processbody);
136
138
152
153
154
158
162
164
179 const std::vector< process_equation >& ps,
180 const variable_list& idvs,
182 const std::set < data::variable >& glob_vars,
192 fresh_identifier_generator.add_identifiers(process::find_identifiers(procspec));
194 fresh_identifier_generator.add_identifiers(data::find_identifiers(ds.equations()));
195 fresh_identifier_generator.add_identifiers(data::find_identifiers(ds.user_defined_aliases()));
196 fresh_identifier_generator.add_identifiers(data::find_identifiers(ds.sorts()));
197 fresh_identifier_generator.add_identifiers(data::find_identifiers(ds.constructors()));
198 fresh_identifier_generator.add_identifiers(data::find_identifiers(ds.mappings()));
208 terminationAction=action(action_label(fresh_identifier_generator(
"Terminate"),sort_expression_list()),data_expression_list());
209 terminatedProcId=process_identifier(fresh_identifier_generator(
"Terminated**"), variable_list());
272 template <
class Expression, IsSubstitution Substitution>
275 return process::replace_variables_capture_avoiding_with_an_identifier_generator(e, sigma, fresh_identifier_generator);
283 if (objectdata.count(o)==0)
285 throw mcrl2::runtime_error(
"Fail to recognize " + process::pp(o) +
286 ". Most likely due to unguarded recursion in a process equation. ");
293 assert(objectdata.find(o)->second.objectname==o.name());
294 assert(objectdata.find(o)->second.parameters==o.variables());
297 for(
const variable& v: result.get_free_variables())
299 assert(std::find(result.parameters.begin(), result.parameters.end(), v)!=result.parameters.end()||
300 std::find(global_variables.begin(), global_variables.end(), v)!=global_variables.end());
309 assert(objectdata.find(o)->second.objectname==o.name());
310 assert(objectdata.find(o)->second.parameters==o.variables());
311 return objectdata.find(o)->second;
316 fresh_identifier_generator.add_identifier(str);
330 return process::sync(ma.front(),action_list_to_process(ma.tail()));
340 return action_list();
345 return action_list({ action(p) });
350 return to_action_list(process::sync(p).left())+to_action_list(process::sync(p).right());
353 return action_list();
360 return sort_actions(to_action_list(p));
368 return action_label_list({ action(multiAction).label() });
371 return getnames(process::sync(multiAction).left())+getnames(process::sync(multiAction).right());
378 std::set < variable>& occurs_set)
380 variable_list result;
381 for (
const data_expression& e: l)
384
385
386
387
388 if (is_variable(e) && std::find(occurs_set.begin(),occurs_set.end(),e)==occurs_set.end())
390 const variable& v = atermpp::down_cast<variable>(e);
391 result.push_front(v);
392 occurs_set.insert(v);
396 result.push_front(variable(get_fresh_variable(
"a",e.sort())));
399 return reverse(result);
403 std::set < variable>& occurs_set)
407 return make_parameters_rec(action(multiAction).arguments(),occurs_set);
410 return getparameters_rec(process::sync(multiAction).left(),occurs_set)+
411 getparameters_rec(process::sync(multiAction).right(),occurs_set);
416 std::set < variable > occurs_set;
417 return getparameters_rec(multiAction,occurs_set);
423 data_expression_list result;
424 for (
const action& a: multiAction)
426 result=reverse(a.arguments()) + result;
428 return reverse(result);
435 data_expression_list::const_iterator e_walker=args.begin();
436 for (
const process::action_label& l: actionIds)
438 std::size_t arity=l.sorts().size();
439 data_expression_list temp_args;
440 for (std::size_t i=0 ; i< arity; ++i,++e_walker)
442 assert(e_walker!=args.end());
443 temp_args.push_front(*e_walker);
445 temp_args=reverse(temp_args);
446 result.push_front(action(l,temp_args));
448 assert(e_walker==args.end());
449 return reverse(result);
454 const process::action_label_list actionnames=getnames(multiAction);
456 isnew=(objectdata.count(actionnames)==0);
464 const variable_list templist=getparameters(multiAction);
465 object.parameters=templist;
470 const action_list tempvar=makemultiaction(actionnames, variable_list_to_data_expression_list(object.parameters));
471 object.processbody=action_list_to_process(tempvar);
473 objectdata[actionnames]=object;
475 return objectdata.find(actionnames)->second;
482 if (objectdata.count(var.name())>0 && mustbenew)
484 throw mcrl2::runtime_error(
"Variable " + data::pp(var) +
" already exists. ");
490 objectdata[var.name()]=object;
495 for (
const variable& v: vars)
497 insertvariable(v,mustbenew);
501 template <
data::IsSubstitution Substitution>
504 std::set<data::variable> result;
505 for (
typename Substitution::const_iterator i = sigma.begin(); i != sigma.end(); ++i)
507 std::set<data::variable> V = data::find_free_variables(i->second);
509 result.insert(V.begin(), V.end());
520
521
522
525 std::size_t powerof2=1;
526 for (; powerof2< i ; n++)
535 if (!options.norewrite)
539 rewr=rewriter(data,options.rewrite_strategy);
549 data_expression_vector v;
550 for(
const data_expression& d: t)
552 v.push_back(RewriteTerm(d));
554 return data_expression_list(v.begin(),v.end());
560 for(
const assignment& a: t)
562 v.emplace_back(a.lhs(), RewriteTerm(a.rhs()));
564 return assignment_list(v.begin(),v.end());
569 return action(t.label(),RewriteTermList(t.arguments()));
574 return process_instance_assignment(t.identifier(),rewrite_assignments(t.assignments()));
596 if (options.norewrite)
607 return new_then_case;
624 return at(t1
,atTime
);
640 return RewriteAction(atermpp::down_cast<process::action>(t));
661 if (objectdata.count(actionId)>0)
663 throw mcrl2::runtime_error(
"Action " + process::pp(actionId) +
" is added twice. This is an internal error in the lineariser. Please report. ");
666 const identifier_string& str=actionId
.name();
674 objectdata[actionId]=object;
675 return objectdata.find(actionId)->second;
680 for (
const process::action_label& l: acts)
690 const variable_list& parameters,
693 const bool canterminate,
694 const bool containstime)
696 assert(procId.variables().size()==parameters.size());
697 const std::string str=procId.name();
700 if (objectdata.count(procId)>0)
702 throw mcrl2::runtime_error(
"Process " + process::pp(procId) +
" is added twice. This is an internal error in the lineariser. Please report. ");
712 object.parameters=parameters;
714 objectdata[procId]=object;
715 return objectdata.find(procId)->second;
718 void storeprocs(
const std::vector< process_equation >& procs)
720 for (
const process_equation& e: procs)
722 insert_process_declaration(
724 e.formal_parameters(),
726 unknown,
false,
false);
731 const variable_list& parameters,
733 const processstatustype s,
734 const bool canterminate,
735 const bool containstime,
738 for(
const std::pair<
const aterm,objectdatatype>& d: objectdata)
740 if (d.second.object==proc &&
741 d.second.parameters==parameters &&
742 d.second.processbody==body &&
743 d.second.canterminate==canterminate &&
744 d.second.containstime==containstime &&
745 d.second.processstatus==s)
747 p=process_identifier(d.second.objectname,d.second.parameters);
761
776 action_list result=ma2;
777 for (
const action& a: ma1)
779 result = atermpp::insert_sorted(a, result);
787 return linMergeMultiActionList(to_action_list(ma1),to_action_list(ma2));
794 const processstatustype status)
797
798
799
800
801
802
805 if (status==multiAction)
807 throw mcrl2::runtime_error(
"Choice operator occurs in a multi-action in " + process::pp(body) +
". The lineariser cannot handle such a pattern. ");
811 if ((s1==mCRL)||(s2==mCRL))
813 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs within the scope of a choice operator in " + process::pp(body) +
814 ". The lineariser cannot handle such processes. ");
821 if (status==multiAction)
823 throw mcrl2::runtime_error(
"Sequential operator occurs in a multi-action in " + process::pp(body) +
". The lineariser cannot handle such a pattern. ");
827 if ((s1==mCRL)||(s2==mCRL))
829 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs in the scope of a sequential operator in " + process::pp(body) +
". "
830 +
"The lineariser cannot handle such processes. ");
839 throw mcrl2::runtime_error(
"The parallel operator occurs in the scope of recursion, or the condition, sequential or choice operator in " +
840 process::pp(body) +
". The lineariser cannot handle such processes. ");
849 throw mcrl2::runtime_error(
"Cannot linearise because the specification contains a leftmerge. ");
854 if (status==multiAction)
856 throw mcrl2::runtime_error(
"If-then occurs in a multi-action in " + process::pp(body) +
". The lineariser cannot linearise this. ");
861 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs in the scope of the if-then operator in " + process::pp(body) +
". "
862 +
"The lineariser cannot handle such processes. ");
869 if (status==multiAction)
871 throw mcrl2::runtime_error(
"If-then-else occurs in a multi-action in " + process::pp(body) +
".");
875 if ((s1==mCRL)||(s2==mCRL))
877 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) +
878 ". " +
"The lineariser cannot handle such processes. ");
886
888 if (status==multiAction)
890 throw mcrl2::runtime_error(
"The sum operator occurs within a multi-action in " + process::pp(body) +
". "
891 +
"The lineariser cannot handle such processes. ");
896 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs in the scope of the sum operator in " + process::pp(body) +
". "
897 "The lineariser cannot handle such processes. ");
906
909 if (status==multiAction)
911 throw mcrl2::runtime_error(
"Stochastic operator occurs within a multi-action in " + process::pp(body) +
".");
916 throw mcrl2::runtime_error(
"An operator ||, allow, hide, rename, or comm occurs in the scope of the stochastic operator in " + process::pp(body) +
". "
917 +
"The lineariser cannot handle such processes. ");
926 throw mcrl2::runtime_error(
"The communication operator occurs in the scope of recursion, the condition, the sequential operation or the choice in "
927 + process::pp(body) +
". The lineariser cannot linearise such processes. ");
935 throw mcrl2::runtime_error(
"Cannot linearise a specification with the bounded initialization operator.");
941 if (status==multiAction)
943 throw mcrl2::runtime_error(
"Time operator 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 a time operator in " + process::pp(body) +
"."
949 +
"The lineariser cannot handle such processes. ");
958 if ((s1!=multiAction)||(s2!=multiAction))
960 throw mcrl2::runtime_error(
"Other objects than multi-actions occur in the scope of a synch operator in " + process::pp(body) +
".");
990 throw mcrl2::runtime_error(
"A hide operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +
".");
1000 throw mcrl2::runtime_error(
"A rename operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +
".");
1010 throw mcrl2::runtime_error(
"An allow operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +
".");
1020 throw mcrl2::runtime_error(
"A block operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +
".");
1026 throw mcrl2::runtime_error(
"Process has unexpected format (2) " + process::pp(body) +
".");
1033 const processstatustype status)
1068 std::vector <process_identifier>& pcrlprocesses,
1069 std::set <process_identifier>& visited)
1073 collectPcrlProcesses_term(if_then(body).then_case(),pcrlprocesses,visited);
1079 collectPcrlProcesses_term(if_then_else(body).then_case(),pcrlprocesses,visited);
1080 collectPcrlProcesses_term(if_then_else(body).else_case(),pcrlprocesses,visited);
1086 collectPcrlProcesses_term(choice(body).left(),pcrlprocesses,visited);
1087 collectPcrlProcesses_term(choice(body).right(),pcrlprocesses,visited);
1093 collectPcrlProcesses_term(seq(body).left(),pcrlprocesses,visited);
1094 collectPcrlProcesses_term(seq(body).right(),pcrlprocesses,visited);
1100 collectPcrlProcesses_term(process::merge(body).left(),pcrlprocesses,visited);
1101 collectPcrlProcesses_term(process::merge(body).right(),pcrlprocesses,visited);
1107 collectPcrlProcesses_term(process::sync(body).left(),pcrlprocesses,visited);
1108 collectPcrlProcesses_term(process::sync(body).right(),pcrlprocesses,visited);
1114 collectPcrlProcesses_term(sum(body).operand(),pcrlprocesses,visited);
1120 collectPcrlProcesses_term(stochastic_operator(body).operand(),pcrlprocesses,visited);
1126 collectPcrlProcesses_term(at(body).operand(),pcrlprocesses,visited);
1132 collectPcrlProcesses(process_instance_assignment(body).identifier(),pcrlprocesses,visited);
1138 collectPcrlProcesses_term(hide(body).operand(),pcrlprocesses,visited);
1144 collectPcrlProcesses_term(process::rename(body).operand(),pcrlprocesses,visited);
1150 collectPcrlProcesses_term(allow(body).operand(),pcrlprocesses,visited);
1156 collectPcrlProcesses_term(block(body).operand(),pcrlprocesses,visited);
1162 collectPcrlProcesses_term(comm(body).operand(),pcrlprocesses,visited);
1173 throw mcrl2::runtime_error(
"process has unexpected format (1) " + process::pp(body) +
".");
1178 std::vector <process_identifier>& pcrlprocesses,
1179 std::set <process_identifier>& visited)
1181 if (visited.count(procDecl)==0)
1183 visited.insert(procDecl);
1187 pcrlprocesses.push_back(procDecl);
1189 collectPcrlProcesses_term(object.processbody,pcrlprocesses,visited);
1195 std::vector <process_identifier>& pcrlprocesses)
1197 std::set <process_identifier> visited;
1198 collectPcrlProcesses(procDecl, pcrlprocesses, visited);
1205 const std::set < variable >& vars_set,
1206 std::set < variable >& vars_result_set)
1210 const variable& v = atermpp::down_cast<variable>(t);
1211 if (vars_set.find(v)!=vars_set.end())
1213 vars_result_set.insert(v);
1240 mCRL2log(mcrl2::log::log_level_t::error) <<
"term of unexpected type " << t << std::endl;
1245 const application& a=atermpp::down_cast<
const application>(t);
1246 filter_vars_by_term(a.head(),vars_set,vars_result_set);
1247 filter_vars_by_termlist(a.begin(),a.end(),vars_set,vars_result_set);
1253 for (
const data_expression& d: r)
1255 if (occursinterm(d, var))
1265 std::set<variable> assigned_variables;
1266 for (
const assignment& l: r)
1268 if (occursinterm(l.rhs(), var))
1272 assigned_variables.insert(l.lhs());
1276 for (
const variable& v: objectIndex(proc_name).parameters)
1280 if (assigned_variables.count(var)==0)
1289 template <
typename Iterator>
1292 const Iterator& end,
1293 const std::set < variable >& vars_set,
1294 std::set < variable >& vars_result_set)
1296 for (; begin != end; ++begin)
1298 filter_vars_by_term(*begin,vars_set,vars_result_set);
1303 const action_list& multiaction,
1304 const std::set < variable >& vars_set,
1305 std::set < variable >& vars_result_set)
1307 for (
const action& ma: multiaction)
1309 filter_vars_by_termlist(ma.arguments().begin(), ma.arguments().end(),vars_set,vars_result_set);
1315 const assignment_list& assignments,
1316 const variable_list& parameters,
1317 const std::set < variable >& vars_set,
1318 std::set < variable >& vars_result_set)
1320 const auto& l= parameters | std::views::transform([](
const variable& v) {
return atermpp::down_cast<data_expression>(v); });
1321 filter_vars_by_termlist(l.begin(),l.end(),vars_set,vars_result_set);
1322 for (
const assignment& a: assignments)
1324 filter_vars_by_term(a.rhs(),vars_set,vars_result_set);
1355
1405 throw mcrl2::runtime_error(
"unexpected process format in occursinCRLterm " + process::pp(p));
1409 template <IsSubstitution MutableSubstitution>
1411 variable_list& sumvars,
1412 MutableSubstitution& sigma,
1416
1417
1418 variable_vector newsumvars;
1420 for (
const variable& var: sumvars)
1422 if (occursinpCRLterm(var,p,
true))
1424 const variable newvar=get_fresh_variable(var.name(),var.sort());
1425 newsumvars.push_back(newvar);
1430 newsumvars.push_back(var);
1433 sumvars=variable_list(newsumvars.begin(), newsumvars.end());
1436 template <IsSubstitution MutableSubstitution>
1438 variable_list& sumvars,
1439 MutableSubstitution& sigma,
1440 const variable_list& occurvars,
1441 const data_expression_list& occurterms)
1444
1445
1446
1447 variable_list newsumvars;
1449 for (
const variable& var: sumvars)
1451 if (occursintermlist(var,variable_list_to_data_expression_list(occurvars)) ||
1452 occursintermlist(var,occurterms))
1454 const variable newvar=get_fresh_variable(var.name(),var.sort());
1455 newsumvars.push_front(newvar);
1460 newsumvars.push_front(var);
1463 sumvars=reverse(newsumvars);
1468 std::set<variable> free_variables_in_p_new;
1469 free_variables_in_p_new=process::find_free_variables(p);
1470 return free_variables_in_p_new;
1477 assignment_vector result;
1478 for(
const assignment& a: assignments)
1480 if (std::find(parameters.begin(),parameters.end(),a.lhs())!=parameters.end())
1482 result.push_back(a);
1485 return assignment_list(result.begin(),result.end());
1490 const assignment_list& assignments,
1491 const variable_list& parameters)
1493 assignment_list::iterator i=assignments.begin();
1494 for(
const variable& v: parameters)
1496 if (i!=assignments.end() && v==i->lhs())
1501 return i==assignments.end();
1508 template <IsSubstitution Substitution>
1510 const assignment_list& assignments,
1511 const variable_list& parameters,
1512 const bool replacelhs,
1513 const bool replacerhs,
1514 Substitution& sigma)
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1534 assert(replacelhs || replacerhs);
1535 if (parameters.empty())
1537 assert(assignments.empty());
1541 const variable& parameter=parameters.front();
1543 if (!assignments.empty())
1550
1555 lhs = atermpp::down_cast<variable>(sigma(lhs));
1559 rhs=replace_variables_capture_avoiding_alt(rhs,sigma);
1562 assignment_list result=
1563 substitute_assignmentlist(
1569 result.push_front(assignment(lhs,rhs));
1575
1576
1577
1578
1585 lhs = atermpp::down_cast<data::variable>(sigma(lhs));
1589 rhs=replace_variables_capture_avoiding_alt(rhs,sigma);
1594 return substitute_assignmentlist(
1601 assignment_list result=
1602 substitute_assignmentlist(
1608 result.push_front(assignment(lhs,rhs));
1616 std::map<variable,data_expression>assignment_map;
1617 for(
const assignment& a: ass)
1619 assignment_map[a.lhs()]=a.rhs();
1622 assignment_vector result;
1623 for(
const variable& v: parameters)
1625 const std::map<variable,data_expression>::const_iterator j=assignment_map.find(v);
1626 if (j!=assignment_map.end())
1628 result.emplace_back(j->first, j->second);
1631 return assignment_list(result.begin(),result.end());
1636 const assignment_list& assignments)
1639 variable_list parameters=object.parameters;
1640 for(
const assignment& a: assignments)
1647 if (parameters.empty())
1651 v=parameters.front();
1652 parameters.pop_front();
1661
1662
1666
1667
1668 template <IsSubstitution Substitution>
1671 Substitution& sigma)
1728 variable_list sumargs=sum(p).variables();
1730 data_expression_list terms;
1732 for( std::map < variable, data_expression >::const_iterator i=sigma.begin(); i!=sigma.end(); ++i)
1734 vars=push_back(vars,i->first);
1735 terms=push_back(terms,i->second);
1738 maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma=sigma;
1739 alphaconvert(sumargs,local_sigma,vars,terms);
1742 substitute_pCRLproc(sum(p).operand(),local_sigma));
1748 variable_list sumargs=sto.variables();
1750 data_expression_list terms;
1752 for( std::map < variable, data_expression >::const_iterator i=sigma.begin(); i!=sigma.end(); ++i)
1754 vars=push_back(vars,i->first);
1755 terms=push_back(terms,i->second);
1758 maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma=sigma;
1759 alphaconvert(sumargs,local_sigma,vars,terms);
1761 return stochastic_operator(
1763 replace_variables_capture_avoiding_alt(sto.distribution(),local_sigma),
1764 substitute_pCRLproc(sto.operand(),local_sigma));
1771 const variable_list parameters=object.parameters;
1772 const assignment_list new_assignments=substitute_assignmentlist(q.assignments(),parameters,
false,
true,sigma);
1773 assert(check_valid_process_instance_assignment(q.identifier(),new_assignments));
1774 return process_instance_assignment(q.identifier(),new_assignments);
1806 throw mcrl2::runtime_error(
"Internal error: expect a pCRL process (2) " + process::pp(p));
1819 const variable_list process_parameters=object.parameters;
1822 assignment_vector new_assignments;
1823 data_expression_list::const_iterator j=rhss.begin();
1824 for(variable_list::const_iterator i=process_parameters.begin(); i!=process_parameters.end(); ++i, ++j)
1826 assert(j!=rhss.end());
1829 if (bound_variables.count(*i)>0)
1831 new_assignments.emplace_back(*i, *j);
1836 new_assignments.emplace_back(*i, *j);
1839 assert(j==rhss.end());
1841 assert(check_valid_process_instance_assignment(procId.identifier(),assignment_list(new_assignments.begin(),new_assignments.end())));
1864 const variable_list& parameters,
1867 variable_vector result;
1868 for(
const variable& p: parameters)
1870 if (occursinpCRLterm(p,body,
false))
1872 result.push_back(p);
1875 return variable_list(result.begin(),result.end());
1884 const variable_list& parameters,
1886 const processstatustype ps,
1887 const bool canterminate,
1888 const bool containstime)
1899 static std::size_t numberOfNewProcesses = 0;
1900 static std::size_t warningNumber = 25;
1901 numberOfNewProcesses++;
1902 if (numberOfNewProcesses == warningNumber)
1904 mCRL2log(mcrl2::log::log_level_t::warning) <<
"Generated " << numberOfNewProcesses <<
" new internal processes.";
1906 if (options.lin_method==t_lin_method::lmRegular)
1908 mCRL2log(mcrl2::log::log_level_t::warning) <<
" If linearisation does not terminate, the use of the flag `--lin-method=regular2' or `--lin-method=stack' in mcrl22lps can help." << std::endl;
1910 else if (options.lin_method==t_lin_method::lmRegular2)
1912 mCRL2log(mcrl2::log::log_level_t::warning) <<
" If linearisation does not terminate, using the flag `--lin-method=stack' in mcrl22lps can help.\n" << std::endl;
1916 mCRL2log(mcrl2::log::log_level_t::warning) << std::endl;
1918 warningNumber=warningNumber*5;
1920 const variable_list parameters1=parameters_that_occur_in_body(parameters, body);
1921 const core::identifier_string s=fresh_identifier_generator(
"P");
1923 assert(std::string(p.name()).size()>0);
1924 insert_process_declaration(
1938 const variable_list& freevars)
1949 variable_list sumvars=sum(body).variables();
1952 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
1953 alphaconvert(sumvars,sigma,freevars,data_expression_list());
1954 body1=substitute_pCRLproc(body1, sigma);
1955 maintain_variables_in_rhs< mutable_map_substitution<> > sigma_aux(sigma);
1956 const data_expression time1=replace_variables_capture_avoiding_alt(time, sigma_aux);
1957 body1=wraptime(body1,time1,sumvars+freevars);
1958 return sum(sumvars,body1);
1964 variable_list sumvars=sto.variables();
1967 maintain_variables_in_rhs<mutable_map_substitution<> > sigma;
1968 alphaconvert(sumvars,sigma,freevars,data_expression_list());
1969 body1=substitute_pCRLproc(body1, sigma);
1970 const data_expression new_distribution=replace_variables_capture_avoiding_alt(sto.distribution(), sigma);
1971 maintain_variables_in_rhs< mutable_map_substitution<> > sigma_aux(sigma);
1972 const data_expression time1=replace_variables_capture_avoiding_alt(time, sigma_aux);
1973 body1=wraptime(body1,time1,sumvars+freevars);
1974 return stochastic_operator(sumvars,new_distribution,body1);
2006 return at(body
,time
);
2009 throw mcrl2::runtime_error(
"Internal error: expect a pCRL process in wraptime " + process::pp(body));
2025
2026
2027
2028
2029
2030
2035 variable v(fresh_identifier_generator(s),sort);
2041 static std::map <
int , std::map < variable,variable > > generated_variables;
2044 if (generated_variables[reuse_index].count(table_index_term)>0)
2046 old_variable=generated_variables[reuse_index][table_index_term];
2051 old_variable=get_fresh_variable(s,sort);
2052 generated_variables[reuse_index][table_index_term]=old_variable;
2054 return old_variable;
2058 variable_list
make_pars(
const sort_expression_list& sortlist)
2061
2063 if (sortlist.empty())
2065 return variable_list();
2070 variable_list result=make_pars(sortlist.tail());
2071 result.push_front(get_fresh_variable(
"a",sort));
2079 const variable_list& freevars,
2080 const std::set<variable>& variables_bound_in_sum)
2085
2086
2087
2088
2089
2090
2091
2092
2093
2094
2098 distributeActionOverConditions(
2100 lazy::and_(condition,c),
2101 if_then(restterm).then_case(),
2102 freevars,variables_bound_in_sum),
2103 distributeActionOverConditions(
2105 lazy::and_(condition,lazy::not_(c)),
2107 freevars,variables_bound_in_sum));
2113
2114
2115
2116
2117
2118
2119
2120
2121
2125 distributeActionOverConditions(
2127 lazy::and_(condition,c),
2128 if_then_else(restterm).then_case(),
2129 freevars,variables_bound_in_sum),
2130 distributeActionOverConditions(
2132 lazy::and_(condition,lazy::not_(c)),
2133 if_then_else(restterm).else_case(),
2134 freevars,variables_bound_in_sum));
2137 const process_expression restterm1=bodytovarheadGNF(restterm,seq_state,freevars,later,variables_bound_in_sum);
2145 assignment_vector result;
2146 for(
const variable& v: parameters)
2148 if (variables_bound_in_sum.count(v)>0)
2150 result.emplace_back(v, v);
2153 return assignment_list(result.begin(),result.end());
2160 const variable_list& freevars,
2161 const variableposition v,
2162 const std::set<variable>& variables_bound_in_sum)
2165
2171 const process_expression body1=bodytovarheadGNF(choice(body).left(),alt_state,freevars,first,variables_bound_in_sum);
2172 const process_expression body2=bodytovarheadGNF(choice(body).right(),alt_state,freevars,first,variables_bound_in_sum);
2183 const process_expression body1=bodytovarheadGNF(body,alt_state,freevars,first,variables_bound_in_sum);
2187 assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
2188 return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
2195 variable_list sumvars=sum(body).variables();
2198 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
2199 alphaconvert(sumvars,sigma,freevars,data_expression_list());
2200 body1=substitute_pCRLproc(body1,sigma);
2201 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
2202 variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
2203 body1=bodytovarheadGNF(body1,sum_state,sumvars+freevars,first,variables_bound_in_sum1);
2205
2206
2209 return choice(sum(sumvars,choice(body1).left()),
2210 sum(sumvars,choice(body1).right()));
2212 return sum(sumvars,body1);
2214 const process_expression body1=bodytovarheadGNF(body,alt_state,freevars,first,variables_bound_in_sum);
2218 assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
2219 return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
2227 variable_list sumvars=sto.variables();
2231 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
2232 alphaconvert(sumvars,sigma,freevars,data_expression_list());
2233 distribution=replace_variables_capture_avoiding_alt(distribution,sigma);
2234 body1=substitute_pCRLproc(body1,sigma);
2235 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
2236 variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
2237 body1=bodytovarheadGNF(body1,name_state,sumvars+freevars,v,variables_bound_in_sum1);
2239
2240
2241 return stochastic_operator(sumvars,distribution,body1);
2243 const process_expression body_=bodytovarheadGNF(body,seq_state,freevars,first,variables_bound_in_sum);
2247 assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
2248 return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
2260 bodytovarheadGNF(body1,seq_state,freevars,first,variables_bound_in_sum));
2262 const process_expression body2=bodytovarheadGNF(body,alt_state,freevars,first,variables_bound_in_sum);
2266 assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
2267 return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
2288 bodytovarheadGNF(body1,seq_state,freevars,first,variables_bound_in_sum));
2293 lazy::not_(condition),
2294 bodytovarheadGNF(body2,seq_state,freevars,first,variables_bound_in_sum));
2303 bodytovarheadGNF(body1,seq_state,freevars,first,variables_bound_in_sum)),
2305 lazy::not_(condition),
2306 bodytovarheadGNF(body2,seq_state,freevars,first,variables_bound_in_sum)));
2308 const process_expression body3=bodytovarheadGNF(body,alt_state,freevars,first,variables_bound_in_sum);
2312 assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
2313 return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
2324 body1=bodytovarheadGNF(body1,name_state,freevars,v,variables_bound_in_sum);
2333
2334
2335
2336
2337
2338
2339
2340
2341
2342
2347 distributeActionOverConditions(body1,c,if_then(body2).then_case(),freevars,variables_bound_in_sum),
2348 distributeActionOverConditions(body1,lazy::not_(c),delta_at_zero(),freevars,variables_bound_in_sum));
2355
2356
2357
2358
2359
2360
2361
2362
2363
2368 distributeActionOverConditions(body1,c,if_then_else(body2).then_case(),freevars,variables_bound_in_sum),
2369 distributeActionOverConditions(body1,lazy::not_(c),if_then_else(body2).else_case(),freevars,variables_bound_in_sum));
2372 body2=bodytovarheadGNF(body2,seq_state,freevars,later,variables_bound_in_sum);
2375 body1=bodytovarheadGNF(body,alt_state,freevars,first,variables_bound_in_sum);
2379 assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
2380 return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
2385 if ((s==multiaction_state)||(v==first))
2396
2397
2398
2399
2406 return transform_process_instance_to_process_instance_assignment(
2407 process_instance(object.process_representing_action,
2408 action(body).arguments()));
2416 const action_list ma=linMergeMultiActionListProcess(
2417 bodytovarheadGNF(body1,multiaction_state,freevars,v,variables_bound_in_sum),
2418 bodytovarheadGNF(body2,multiaction_state,freevars,v,variables_bound_in_sum));
2421 if ((s==multiaction_state)||(v==first))
2431
2432
2433
2440 return transform_process_instance_to_process_instance_assignment(
2442 process_identifier(object.process_representing_action),
2452 first,variables_bound_in_sum);
2465 assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
2466 return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
2495 throw mcrl2::runtime_error(
"unexpected process format in bodytovarheadGNF " + process::pp(body) +
".");
2502 for (
const process_identifier& i: procs)
2504 objectdatatype& object=objectIndex(i);
2510 std::set<variable> variables_bound_in_sum;
2511 const process_expression result=
2517 variables_bound_in_sum);
2518 object.processbody=result;
2552
2553 variable_list sumvars=sum(body1).variables();
2555 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
2556 alphaconvertprocess(sumvars,sigma,body2);
2558 putbehind(substitute_pCRLproc(sum(body1).operand(), sigma),
2565 variable_list stochvars=sto.variables();
2568 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
2569 alphaconvertprocess(stochvars,sigma,body2);
2570 return stochastic_operator(
2574 substitute_pCRLproc(sto.operand(),sigma),
2609 throw mcrl2::runtime_error(
"Internal error. Unexpected process format in putbehind " + process::pp(body1) +
".");
2640
2641 variable_list sumvars=sum(body1).variables();
2642 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
2643 alphaconvert(sumvars,sigma,variable_list(), data_expression_list({ condition }));
2646 distribute_condition(
2647 substitute_pCRLproc(sum(body1).operand(),sigma),
2654
2656 variable_list stochvars=sto.variables();
2657 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
2658 alphaconvert(stochvars,sigma,variable_list(), data_expression_list({ condition }));
2660 return stochastic_operator(
2663 replace_variables_capture_avoiding_alt(
2666 if_(variables_are_equal_to_default_values(stochvars),real_one(),real_zero())),
2667 distribute_condition(
2668 substitute_pCRLproc(sto.operand(),sigma),
2682 throw mcrl2::runtime_error(
"Internal error. Unexpected process format in distribute condition " + process::pp(body1) +
".");
2686
2687
2688
2689
2690
2691
2692
2693
2694
2695
2696
2697
2700 const variable_list& sumvars,
2701 const variable_list& stochvars,
2705 if (options.norewrite)
2707 throw mcrl2::runtime_error(
"The use of the rewriter must be allowed to distribute a sum operator over a distribution.");
2711 std::vector < data_expression_vector > data_vector(1,data_expression_vector());
2712 for(
const variable& v:sumvars)
2714 std::vector < data_expression_vector > new_data_vector;
2716 if (!data.is_certainly_finite(v.sort()))
2718 throw mcrl2::runtime_error(
"Cannot distribute a sum variable of non finite sort " + pp(v.sort()) +
" over a distribution, which is required for linearisation.");
2721 for(
const data_expression& d: enumerate_expressions(v.sort(),data,rewr))
2723 for(
const data_expression_vector& dv: data_vector)
2725 data_expression_vector new_dv=dv;
2726 new_dv.push_back(d);
2727 new_data_vector.push_back(new_dv);
2731 data_vector.swap(new_data_vector);
2734 assert(!data_vector.empty());
2738 variable_list resulting_stochastic_variables;
2739 bool result_defined=
false;
2740 for(
const data_expression_vector& d: data_vector)
2742 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
2743 variable_list vl = stochvars;
2744 alphaconvert(vl,sigma,stochvars,data_expression_list());
2745 data_expression_vector::const_iterator i=d.begin();
2746 for(
const variable& v: sumvars)
2751 const process_expression d1=substitute_pCRLproc(body,sigma);
2752 const data_expression new_distribution=replace_variables_capture_avoiding_alt(distribution, sigma);
2756 resulting_body=choice(resulting_body, d1);
2757 resulting_distribution=sort_real::times(resulting_distribution,new_distribution);
2758 resulting_stochastic_variables=resulting_stochastic_variables + vl;
2763 resulting_distribution=new_distribution;
2764 resulting_stochastic_variables=vl;
2765 result_defined=
true;
2770 return stochastic_operator(resulting_stochastic_variables, resulting_distribution, resulting_body);
2774 const variable_list& sumvars,
2775 const variable_list& stochastic_variables,
2802 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
2803 variable_list inner_stoch_vars=sto.variables();
2804 alphaconvert(inner_stoch_vars,sigma,sumvars,data_expression_list());
2806 const data_expression new_distribution=replace_variables_capture_avoiding_alt(sto.distribution(), sigma);
2807 return distribute_sum_over_a_stochastic_operator(sumvars,
2808 stochastic_variables + inner_stoch_vars,
2809 sort_real::times(distribution,new_distribution), new_body);
2812 throw mcrl2::runtime_error(
"Internal error. Unexpected process format in distribute_sum " + process::pp(body) +
".");
2817 const variable_list& sumvars,
2836 return sum(sumvars
,body1
);
2841 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
2842 variable_list inner_sumvars=sum(body1).variables();
2843 alphaconvert(inner_sumvars,sigma,sumvars,data_expression_list());
2845 return sum(sumvars+inner_sumvars,new_body1);
2851 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
2852 variable_list inner_stoch_vars=sto.variables();
2853 alphaconvert(inner_stoch_vars,sigma,sumvars,data_expression_list());
2855 const data_expression new_distribution=replace_variables_capture_avoiding_alt(sto.distribution(), sigma);
2856 return distribute_sum_over_a_stochastic_operator(sumvars, inner_stoch_vars, new_distribution, new_body1);
2865 throw mcrl2::runtime_error(
"Internal error. Unexpected process format in distribute_sum " + process::pp(body1) +
".");
2871 const std::vector < process_instance_assignment >& s1,
2872 const std::vector < process_instance_assignment >& s2,
2873 const bool regular2)
2876
2877
2878
2879
2881 std::vector < process_instance_assignment >::const_iterator i2=s2.begin();
2882 for (std::vector < process_instance_assignment >::const_iterator i1=s1.begin();
2883 i1!=s1.end(); ++i1,++i2)
2891 if (i1->identifier()!=i2->identifier())
2912 const std::vector < process_instance_assignment >& process_names,
2915 std::vector < std::vector < process_instance_assignment > >::const_iterator rwalker=representedprocesses.begin();
2916 for (std::vector < process_identifier >::const_iterator walker=seq_varnames.begin();
2917 walker!=seq_varnames.end(); ++walker,++rwalker)
2919 assert(rwalker!=representedprocesses.end());
2920 const process_identifier process=*walker;
2921 if (match_sequence(process_names,*rwalker,options.lin_method==t_lin_method::lmRegular2))
2927 assert(rwalker==representedprocesses.end());
2933 std::vector < process_instance_assignment >& result)
2937 result.push_back(atermpp::down_cast<process_instance_assignment>(sequence));
2944 extract_names(sto.operand(),result);
2953 result.push_back(atermpp::down_cast<process_instance_assignment>(first));
2954 objectdatatype& object=objectIndex(atermpp::down_cast<process_instance_assignment>(first).identifier());
2957 extract_names(seq(sequence).right(),result);
2963 throw mcrl2::runtime_error(
"Internal error. Expected sequence of process names (1) " + process::pp(sequence) +
".");
2973 const variable_list parameters=objectIndex(procId).parameters;
2988 const variable_list pars=parscollect(seq(oldbody).right(),newbody);
2989 variable_list pars1;
2990 variable_list pars2;
2991 const variable_list new_pars=construct_renaming(pars,objectIndex(procId).parameters,pars1,pars2,
false);
2992 assignment_vector new_assignment;
2993 for(variable_list::const_iterator i=pars2.begin(), j=new_pars.begin(); i!=pars2.end(); ++i,++j)
2995 assert(j!=new_pars.end());
2996 new_assignment.emplace_back(*i, *j);
2998 assert(check_valid_process_instance_assignment(procId,assignment_list(new_assignment.begin(),new_assignment.end())));
2999 newbody=seq(process_instance_assignment(procId,assignment_list(new_assignment.begin(),new_assignment.end())),newbody);
3000 const variable_list result=pars1+pars;
3001 assert(std::set<variable>(result.begin(),result.end()).size()==result.size());
3006 return parscollect(first,newbody);
3011 throw mcrl2::runtime_error(
"Internal error. Expected a sequence of process names (2) " + process::pp(oldbody) +
".");
3012 return variable_list();
3017 const variable_list& vl,
3018 const std::set<variable>& variables_bound_in_sum)
3020 assignment_vector result;
3021 for(
const variable& v: vl)
3023 if (variables_bound_in_sum.count(v)>0 && occursinpCRLterm(v,t,
false))
3025 result.emplace_back(v, v);
3029 return assignment_list(result.begin(),result.end());
3039 const variable_list pars=object.parameters;
3040 assert(pars.size()<=vl.size());
3042 std::map<variable,data_expression>sigma;
3043 for(
const assignment& a: p.assignments())
3045 sigma[a.lhs()]=a.rhs();
3048 assignment_list result;
3049 for(variable_list::const_iterator i=pars.begin(); i!=pars.end(); ++i, vl.pop_front())
3051 assert(!vl.empty());
3052 const data_expression new_rhs=make_map_substitution(sigma)(*i);
3053 result.push_front(assignment(vl.front(),new_rhs));
3056 return reverse(result);
3063 const assignment_list first_assignment=argscollect_regular2(firstproc,vl);
3066 return first_assignment + argscollect_regular2(seq(t).right(),vl);
3068 return first_assignment;
3071 throw mcrl2::runtime_error(
"Internal error. Expected a sequence of process names (3) " + process::pp(t) +
".");
3098 throw mcrl2::runtime_error(
"Internal error. Expected a sequence of process names (4) " + process::pp(t) +
".");
3104 std::vector <process_identifier>& todo,
3105 const variable_list& freevars,
3106 const std::set<variable>& variables_bound_in_sum)
3111
3112
3117 std::set<variable> variables_bound_in_sum_new=variables_bound_in_sum;
3118 variables_bound_in_sum_new.insert(sto.variables().begin(),sto.variables().end());
3119 return stochastic_operator(sto.variables(),
3121 create_regular_invocation(sto.operand(),todo,freevars+sto.variables(),variables_bound_in_sum_new));
3126 std::vector < process_instance_assignment > process_names;
3127 extract_names(sequence,process_names);
3128 assert(!process_names.empty());
3130 if (process_names.size()==1)
3141 throw mcrl2::runtime_error(
"Internal error. Expected a sequence of process names " + process::pp(sequence) +
".");
3144
3147
3148
3149 if (!exists_variable_for_sequence(process_names,new_process))
3152
3154 if (options.lin_method==t_lin_method::lmRegular2)
3156 variable_list pars=parscollect(sequence,newbody);
3157 new_process=newprocess(pars,newbody,pCRL,
3158 canterminatebody(newbody),
3159 containstimebody(newbody));
3160 representedprocesses.push_back(process_names);
3166 representedprocesses.push_back(process_names);
3168 seq_varnames.push_back(new_process);
3169 todo.push_back(new_process);
3172 variable_list parameters=objectIndex(new_process).parameters;
3173 if (options.lin_method==t_lin_method::lmRegular2)
3175 const assignment_list args=argscollect_regular2(sequence,parameters);
3176 assert(check_valid_process_instance_assignment(new_process,args));
3182 assert(check_valid_process_instance_assignment(new_process,argscollect_regular(sequence,parameters,variables_bound_in_sum)));
3183 return process_instance_assignment(new_process,argscollect_regular(sequence,parameters,variables_bound_in_sum));
3189 std::vector <process_identifier>& todo,
3190 const variable_list& freevars,
3191 const std::set<variable>& variables_bound_in_sum)
3193
3194
3195
3199 const process_expression t1=to_regular_form(choice(t).left(),todo,freevars,variables_bound_in_sum);
3200 const process_expression t2=to_regular_form(choice(t).right(),todo,freevars,variables_bound_in_sum);
3209
3210 return seq(firstact,create_regular_invocation(seq(t).right(),todo,freevars,variables_bound_in_sum));
3215 return if_then(if_then(t).condition(),to_regular_form(if_then(t).then_case(),todo,freevars,variables_bound_in_sum));
3220 variable_list sumvars=sum(t).variables();
3222 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
3223 alphaconvert(sumvars,sigma,freevars,data_expression_list());
3226 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
3227 variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
3233 variables_bound_in_sum1));
3239 variable_list sumvars=sto.variables();
3241 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
3242 alphaconvert(sumvars,sigma,freevars,data_expression_list());
3243 const data_expression distribution=replace_variables_capture_avoiding_alt(
3248 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
3249 variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
3250 return stochastic_operator(
3257 variables_bound_in_sum1));
3265 throw mcrl2::runtime_error(
"to regular form expects GNF " + process::pp(t) +
".");
3272 const variable_list& freevars,
3284 variable_list sumvars=sum(body).variables();
3286 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
3287 alphaconvert(sumvars,sigma,freevars,data_expression_list());
3288 body1=substitute_pCRLproc(body1, sigma);
3289 maintain_variables_in_rhs< mutable_map_substitution<> > sigma_aux(sigma);
3290 const data_expression time1=replace_variables_capture_avoiding_alt(time,sigma_aux);
3291 body1=distributeTime(body1,time1,sumvars+freevars,timecondition);
3292 return sum(sumvars,body1);
3298 variable_list sumvars=sto.variables();
3299 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
3300 alphaconvert(sumvars,sigma,freevars,data_expression_list());
3302 data_expression new_distribution=replace_variables_capture_avoiding_alt(sto.distribution(), sigma);
3303 maintain_variables_in_rhs< mutable_map_substitution<> > sigma_aux(sigma);
3304 const data_expression time1=replace_variables_capture_avoiding_alt(time,sigma_aux);
3305 new_body=distributeTime(new_body,time1,sumvars+freevars,timecondition);
3306 return stochastic_operator(sumvars,new_distribution,new_body);
3342 return at(body
,time
);
3345 throw mcrl2::runtime_error(
"Internal error: expect a pCRL process in distributeTime " + process::pp(body) +
".");
3352 std::vector <process_identifier>& todo,
3354 processstatustype mode,
3355 const variable_list& freevars,
3356 const std::set <variable>& variables_bound_in_sum)
3358
3359
3360
3361
3362
3374 variables_bound_in_sum);
3385 regular,mode,freevars,variables_bound_in_sum);
3387 regular,mode,freevars,variables_bound_in_sum);
3394 todo,regular,mode,freevars,variables_bound_in_sum);
3396 todo,regular,mode,freevars,variables_bound_in_sum);
3398 if ((regular) && (v==first))
3401 t3=to_regular_form(t3,todo,freevars,variables_bound_in_sum);
3409 procstorealGNFbody(if_then(body).then_case(),first,
3410 todo,regular,mode,freevars,variables_bound_in_sum),
3411 if_then(body).condition());
3417 const variable_list sumvars=sum(body).variables();
3418 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
3419 variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
3420 return distribute_sum(sumvars,
3421 procstorealGNFbody(sum(body).operand(),first,
3422 todo,regular,mode,sumvars+freevars,variables_bound_in_sum1));
3429 std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
3430 variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
3431 return stochastic_operator(
3434 procstorealGNFbody(sto.operand(),v,
3435 todo,regular,mode,sumvars+freevars,variables_bound_in_sum1));
3460
3461
3462
3463
3474
3475 procstorealGNFrec(t,first,todo,regular);
3477 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
3478 for(
const assignment& a:
static_cast<
const process_instance_assignment&>(body).assignments())
3480 sigma[a.lhs()]=a.rhs();
3485 t3=to_regular_form(t3,todo,freevars,variables_bound_in_sum);
3503 procstorealGNFbody(process::merge(body).left(),later,
3504 todo,regular,mode,freevars,variables_bound_in_sum);
3505 procstorealGNFbody(process::merge(body).right(),later,
3506 todo,regular,mode,freevars,variables_bound_in_sum);
3512 procstorealGNFbody(hide(body).operand(),later,todo,regular,mode,freevars,variables_bound_in_sum);
3518 procstorealGNFbody(process::rename(body).operand(),later,todo,regular,mode,freevars,variables_bound_in_sum);
3524 procstorealGNFbody(allow(body).operand(),later,todo,regular,mode,freevars,variables_bound_in_sum);
3530 procstorealGNFbody(block(body).operand(),later,todo,regular,mode,freevars,variables_bound_in_sum);
3536 procstorealGNFbody(comm(body).operand(),later,todo,regular,mode,freevars,variables_bound_in_sum);
3542 throw mcrl2::runtime_error(
"unexpected process format in procstorealGNF " + process::pp(body) +
".");
3549 const variableposition v,
3550 std::vector <process_identifier>& todo,
3554
3555
3556
3557
3564 std::set<variable> variables_bound_in_sum;
3566 todo,regular,pCRL,object.parameters,variables_bound_in_sum);
3569 throw mcrl2::runtime_error(
"There is something wrong with recursion.");
3580 std::set<variable> variables_bound_in_sum;
3582 regular,mCRL,object.parameters,variables_bound_in_sum);
3584
3592 throw mcrl2::runtime_error(
"Unguarded recursion in process " + process::pp(procIdDecl) +
".");
3605 throw mcrl2::runtime_error(
"Unguarded recursion in process " + process::pp(procIdDecl) +
".");
3608 throw mcrl2::runtime_error(
"strange process type: " + std::to_string(object.processstatus));
3614 std::vector <process_identifier> todo;
3615 todo.push_back(procsIdDecl);
3616 while (!todo.empty())
3618 const process_identifier pi=todo.back();
3620 procstorealGNFrec(pi,first,todo,regular);
3640 std::set<process_identifier>& reachable_process_identifiers)
3642 if (reachable_process_identifiers.count(id)==0)
3644 reachable_process_identifiers.insert(id);
3645 make_pCRL_procs(objectIndex(id).processbody,reachable_process_identifiers);
3651 std::set<process_identifier>& reachable_process_identifiers)
3655 make_pCRL_procs(choice(t).left(),reachable_process_identifiers);
3656 make_pCRL_procs(choice(t).right(),reachable_process_identifiers);
3662 make_pCRL_procs(seq(t).left(),reachable_process_identifiers);
3663 make_pCRL_procs(seq(t).right(),reachable_process_identifiers);
3669 make_pCRL_procs(if_then(t).then_case(),reachable_process_identifiers);
3675 make_pCRL_procs(sum(t).operand(),reachable_process_identifiers);
3681 make_pCRL_procs(stochastic_operator(t).operand(),reachable_process_identifiers);
3687 make_pCRL_procs(atermpp::down_cast<process_instance_assignment>(t).identifier(), reachable_process_identifiers);
3696 throw mcrl2::runtime_error(
"unexpected process format " + process::pp(t) +
" in make_pCRL_procs");
3702
3703
3704
3705
3706
3709
3710
3711
3712
3713
3722 const std::map< process_identifier, process_identifier >::const_iterator i=identifier_identifier_map.find(target_id);
3723 if (i==identifier_identifier_map.end())
3729 target_id=i->second;
3739 std::map< process_identifier, process_identifier >& identifier_identifier_map,
3747
3750 if (id1==initial_process)
3756 identifier_identifier_map[id1]=id2;
3763 std::map< process_identifier, process_identifier > new_identifier_identifier_map;
3764 for(
const std::pair<
const process_identifier, process_identifier >& p: identifier_identifier_map)
3766 new_identifier_identifier_map[p.first]=get_last(p.second,identifier_identifier_map);
3768 identifier_identifier_map.swap(new_identifier_identifier_map);
3771 using identifier_identifier_pair = std::pair<
const process_identifier, process_identifier>;
3772 for(
const identifier_identifier_pair& p: identifier_identifier_map)
3774 assert(identifier_identifier_map.count(p.second)==0);
3791 const std::map< process_identifier, process_identifier >::const_iterator i=m_map.find(id);
3804 assert(reachable_process_identifiers.count(initial_process)>0);
3805 using parameters_process_pair = std::pair<variable_list, process_expression>;
3806 using mapping_type = std::map<std::pair<variable_list, process_expression>, process_identifier>;
3807 using mapping_type_pair = std::pair<
const std::pair<variable_list, process_expression>, process_identifier>;
3810 mapping_type process_mapping;
3811 std::map< process_identifier, process_identifier > identifier_identifier_map;
3812 for(
const process_identifier& id: reachable_process_identifiers)
3814 objectdatatype& object=objectIndex(id);
3815 const parameters_process_pair p(object.parameters,object.processbody);
3816 mapping_type::const_iterator i=process_mapping.find(p);
3817 if (i==process_mapping.end())
3819 process_mapping[p]=id;
3823 set_proc_identifier_map(identifier_identifier_map,id,i->second,initial_process);
3826 complete_proc_identifier_map(identifier_identifier_map);
3828 while (!identifier_identifier_map.empty())
3831
3832
3833
3834 std::map< process_identifier, process_identifier > new_identifier_identifier_map;
3835 mapping_type new_process_mapping;
3836 for(
const mapping_type_pair& p: process_mapping)
3838 const make_substitution sigma(identifier_identifier_map);
3839 const parameters_process_pair p_new(p.first.first, replace_process_identifiers( p.first.second, sigma));
3840 mapping_type::const_iterator i=new_process_mapping.find(p_new);
3841 if (i==new_process_mapping.end())
3843 new_process_mapping[p_new]=sigma(p.second);
3847 set_proc_identifier_map(new_identifier_identifier_map,sigma(p.second),sigma(i->second),initial_process);
3850 complete_proc_identifier_map(new_identifier_identifier_map);
3851 identifier_identifier_map.swap(new_identifier_identifier_map);
3852 process_mapping.swap(new_process_mapping);
3856 std::set< process_identifier > result;
3857 for(
const mapping_type_pair& p: process_mapping)
3859 result.insert(p.second);
3860 objectdatatype& object=objectIndex(p.second);
3861 object.processbody=p.first.second;
3863 assert(result.count(initial_process)>0);
3897
3898
3899
3900
3901
3910 std::map< process_identifier, process_pid_pair > processes_with_stochastic_distribution_first;
3911 std::set< process_identifier > result;
3912 for(
const process_identifier& p: reachable_process_identifiers)
3914 objectdatatype& object = objectIndex(p);
3915 process_expression proc_=obtain_initial_distribution_term(object.processbody);
3916 if (!is_stochastic_operator(proc_))
3918 processes_with_stochastic_distribution_first.insert(std::pair< process_identifier, process_pid_pair >(p, process_pid_pair(proc_,p)));
3923 const stochastic_operator& proc=down_cast<
const stochastic_operator>(proc_);
3924 assert(!is_process_instance_assignment(proc.operand()));
3925 objectdatatype& object=objectIndex(p);
3926 maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma;
3927 variable_list vars=proc.variables();
3928 alphaconvert(vars,local_sigma, vars + object.parameters, data_expression_list());
3930 const process_identifier newproc=newprocess(
3931 vars + object.parameters,
3932 process::replace_variables_capture_avoiding_with_an_identifier_generator(proc.operand(),
3934 fresh_identifier_generator),
3936 canterminatebody(proc.operand()),
3937 containstimebody(proc.operand()));
3940 processes_with_stochastic_distribution_first.insert(
3941 std::pair< process_identifier, process_pid_pair >
3943 process_pid_pair(stochastic_operator(
3945 replace_variables_capture_avoiding_alt(proc.distribution(), local_sigma),
3948 result.insert(newproc);
3952 for(
const process_identifier& p: reachable_process_identifiers)
3954 objectdatatype& object=objectIndex(processes_with_stochastic_distribution_first.at(p).process_id());
3955 assert(!is_stochastic_operator(object.processbody));
3956 object.processbody=transform_initial_distribution_term(object.processbody,processes_with_stochastic_distribution_first);
3957 assert(!is_stochastic_operator(object.processbody));
3961 process_expression initial_distribution=processes_with_stochastic_distribution_first.at(initial_process_id).process_body();
3964 const stochastic_operator sto=atermpp::down_cast<stochastic_operator>(initial_distribution);
3966 initial_process_id=processes_with_stochastic_distribution_first.at(initial_process_id).process_id();
3980 const variable_list& vl,
3981 mutable_indexed_substitution<>& parameter_renaming)
3984
3985
3986
3987
3989 for(
const variable& v: vl)
3991 if (v.name()==var.name())
3993 if (v.sort()==var.sort())
3999 if (parameter_renaming(v)==v)
4001 const variable new_var(fresh_identifier_generator(var.name()),var.sort());
4002 parameter_renaming[var]=new_var;
4009 var=atermpp::down_cast<variable>(parameter_renaming(v));
4019 const variable_list& par2,
4020 mutable_indexed_substitution<>& parameter_renaming)
4030 variable_list result=joinparameters(par1,par2.tail(), parameter_renaming);
4031 if (alreadypresent(var2,par1, parameter_renaming))
4036 result.push_front(var2);
4045 mutable_indexed_substitution<> parameter_renaming;
4046 variable_list parameters;
4047 for (
const process_identifier& p: pCRLprocs)
4049 const objectdatatype& object=objectIndex(p);
4050 parameters=joinparameters(parameters,object.parameters, parameter_renaming);
4053 std::set<process_identifier> new_pCRLprocs;
4054 for (
const process_identifier& p: pCRLprocs)
4056 objectdatatype object=objectIndex(p);
4057 object.processbody=process::replace_all_variables(object.processbody,parameter_renaming);
4058 object.parameters=process::replace_all_variables(object.parameters,parameter_renaming);
4059 process_identifier p_new=process::replace_all_variables(p,parameter_renaming);
4060 objectdata[p_new]=object;
4061 new_pCRLprocs.insert(p_new);
4063 pCRLprocs=new_pCRLprocs;
4070 const std::set < process_identifier >& pCRLprocs)
4072 create_enumeratedtype(pCRLprocs.size());
4105 basic_sort stack_sort_alias(spec.fresh_identifier_generator(
"Stack"));
4106 structured_sort_constructor_argument_vector sp_push_arguments;
4107 for (
const variable& v: pl)
4109 sp_push_arguments.emplace_back(spec.fresh_identifier_generator(
"get" + std::string(v.name())), v.sort());
4110 sorts.push_front(v.sort());
4112 sp_push_arguments.emplace_back(spec.fresh_identifier_generator(
"pop"), stack_sort_alias);
4113 sorts=reverse(sorts);
4115 structured_sort_constructor sc_emptystack(spec.fresh_identifier_generator(
"emptystack"),spec.fresh_identifier_generator(
"isempty"));
4117 structured_sort_constructor_vector constructors(1,sc_push);
4118 constructors.push_back(sc_emptystack);
4120 spec.data.add_alias(alias(stack_sort_alias,structured_sort(constructors)));
4121 stacksort=
data::normalize_sorts(stack_sort_alias,spec.data);
4125 const std::vector< data::function_symbol > projection_functions =
4126 sc_push.projection_functions(stack_sort_alias);
4127 pop=projection_functions.back();
4128 getstate=projection_functions.front();
4129 get=function_symbol_list(projection_functions.begin()+1,projection_functions.end()-1);
4143
4144
4149
4150
4151
4158 const variable_list& parameters,
4161 if (stack_operations_list==
nullptr)
4165 if (parameters==stack_operations_list->parameter_list)
4167 return stack_operations_list;
4176 const std::set < process_identifier >& pCRLprocs,
4177 const bool singlecontrolstate)
4179 assert(pCRLprocs.size()>0);
4182 no_of_states=pCRLprocs.size();
4184 const std::string s3((spec.options.statenames)?std::string(last.name()):std::string(
"s"));
4185 if ((spec.options.binary) && (spec.options.newstate))
4187 std::size_t i=spec.upperpowerof2(no_of_states);
4190 variable name(spec.fresh_identifier_generator(
"bst"),sort_bool::bool_());
4191 spec.insertvariable(name,
true);
4192 booleanStateVariables.push_front(name);
4199 if (spec.options.newstate)
4201 if (!spec.options.binary)
4203 if (!singlecontrolstate)
4205 const std::size_t e=spec.create_enumeratedtype(no_of_states);
4206 stackvar=variable(spec.fresh_identifier_generator(s3), spec.enumeratedtypes[e].sortId);
4216 stackvar=variable(spec.fresh_identifier_generator(s3),sort_bool::bool_());
4221 stackvar=variable(spec.fresh_identifier_generator(s3), sort_pos::pos());
4227 if (spec.options.newstate)
4229 throw mcrl2::runtime_error(
"cannot combine stacks with " +
4230 (spec.options.binary?std::string(
"binary"):std::string(
"an enumerated type")));
4236 stackvar=variable(spec.fresh_identifier_generator(s3),opns->stacksort);
4241 variable_list temp=parlist;
4242 temp.push_front(variable(
"state",sort_pos::pos()));
4243 opns=(stackoperations*)
new stackoperations(temp,spec);
4244 stackvar = variable(spec.fresh_identifier_generator(s3), opns->stacksort);
4255 return is_variable(d) && global_variables.count(atermpp::down_cast<variable>(d)) > 0;
4262 if (global_variables.count(var)>0)
4268 function_symbol_list::const_iterator getmappings=stack.opns->get.begin();
4269 for (variable_list::const_iterator walker=stack.parameters.begin() ;
4270 walker!=stack.parameters.end() ; ++walker,++getmappings)
4274 return application(*getmappings,stack.stackvar);
4276 assert(getmappings!=stack.opns->get.end());
4279
4285 const assignment_list& t1,
4289 assignment_list t(t1);
4290 if (!options.newstate)
4292 assignment_list result=t;
4293 result.push_front(assignment(stack.stackvar,sort_pos::pos(i)));
4298
4300 if (!options.binary)
4302 const std::size_t e=create_enumeratedtype(stack.no_of_states);
4303 data_expression_list l=enumeratedtypes[e].elementnames;
4309 assignment_list result=t;
4311 result.push_front(assignment(stack.stackvar,l.front()));
4315
4317 std::size_t k=upperpowerof2(stack.no_of_states);
4318 variable_list::const_iterator boolean_state_variables=stack.booleanStateVariables.begin();
4319 for (; k>0 ; k--, ++boolean_state_variables)
4323 t.push_front(assignment(*boolean_state_variables,sort_bool::false_()));
4328 t.push_front(assignment(*boolean_state_variables,sort_bool::true_()));
4338 const data_expression_list& t1,
4341 data_expression_list t(t1);
4342 if (!options.newstate)
4344 data_expression_list result=t;
4345 result.push_front(sort_pos::pos(i));
4350
4352 if (!options.binary)
4354 const std::size_t e=create_enumeratedtype(stack.no_of_states);
4355 data_expression_list l(enumeratedtypes[e].elementnames);
4360 data_expression_list result=t;
4361 result.push_front(l.front());
4365
4367 std::size_t k=upperpowerof2(stack.no_of_states);
4368 variable_list::const_iterator boolean_state_variables=stack.booleanStateVariables.begin();
4369 for (; k>0 ; k--, ++boolean_state_variables)
4373 t.push_front(sort_bool::false_());
4378 t.push_front(sort_bool::true_());
4388 const std::set < process_identifier >& pCRLproc,
4393 for (
const process_identifier& p: pCRLproc)
4403 if (!options.newstate)
4407 return equal_to(stack.stackvar, processencoding(i,assignment_list(),stack).front().rhs());
4410 application(stack.opns->getstate,stack.stackvar),
4411 processencoding(i,assignment_list(),stack).front().rhs());
4414 if (!options.binary)
4415
4417 create_enumeratedtype(stack.no_of_states);
4420 return equal_to(stack.stackvar,
4421 processencoding(i,assignment_list(),stack).front().rhs());
4424 application(stack.opns->getstate, stack.stackvar),
4425 processencoding(i,assignment_list(),stack).front().rhs());
4429
4431 const variable_list vars=stack.booleanStateVariables;
4435 for (
const variable& v: vars)
4439 t3=lazy::and_(lazy::not_(v),t3);
4444 t3=lazy::and_(v,t3);
4456 const variable_list& vars,
4457 const variable_list& stochastic_variables)
4471 if (std::find(vars.begin(),vars.end(),t)!=vars.end())
4474
4478 if (std::find(stochastic_variables.begin(),stochastic_variables.end(),t)!=stochastic_variables.end())
4481
4486 return getvar(atermpp::down_cast<variable>(t), stack);
4492 const application&a=atermpp::down_cast<application>(t);
4495 adapt_termlist_to_stack(a.begin(),a.end(),stack,vars,stochastic_variables));
4510 const assignment_list old_assignments=reverse(where_t.assignments());
4511 variable_list new_vars=vars;
4512 assignment_list new_assignments;
4513 for (
const assignment& a: old_assignments)
4515 new_vars.push_front(a.lhs());
4516 new_assignments.push_front(
4519 adapt_term_to_stack(a.rhs(),stack,vars,stochastic_variables)));
4522 return where_clause(
4523 adapt_term_to_stack(where_t,stack,new_vars,stochastic_variables),
4532 template <
typename Iterator>
4540 data_expression_vector result;
4541 for (; begin != end; ++begin)
4543 result.push_back(adapt_term_to_stack(*begin,stack, vars,stochastic_variables));
4553 action_vector result;
4555 for (
const action& act : multiAction)
4557 const data_expression_vector vec(
4558 adapt_termlist_to_stack(act.arguments().begin(), act.arguments().end(), stack, vars, variable_list()));
4559 result.emplace_back(act.label(), data_expression_list(vec.begin(), vec.end()));
4564 std::sort(result.begin(), result.end());
4566 return action_list(result.begin(), result.end());
4571 if ((!options.noglobalvars) && allow_dont_care_var)
4573 const variable newVariable(fresh_identifier_generator(
"dc"),s);
4575 global_variables.insert(newVariable);
4578 return representative_generator(data)(s);
4583 const assignment_list& args,
4585 const variable_list& vars,
4586 const std::set<variable>& free_variables_in_body,
4587 const variable_list& stochastic_variables)
4590
4591
4592
4593
4594
4595
4596
4597 for (
const assignment& a: args)
4601 return adapt_term_to_stack(a.rhs(),stack,vars,stochastic_variables);
4605 if (free_variables_in_body.find(s)==free_variables_in_body.end())
4615 const variable_list& pars,
4616 const variable_list& parlist,
4617 const assignment_list& args,
4618 const data_expression_list& t2,
4620 const variable_list& vars,
4621 const std::set<variable>& free_variables_in_body,
4622 const variable_list& stochastic_variables)
4624 if (parlist.empty())
4628 data_expression_list result=findarguments(pars,parlist.tail(),args,t2,stack,vars,free_variables_in_body,stochastic_variables);
4629 data_expression rhs=find_(parlist.front(),args,stack,vars,free_variables_in_body,stochastic_variables);
4631 result.push_front(rhs);
4636 const variable_list& parlist,
4637 const assignment_list& args,
4638 const std::set<variable>& free_variables_in_body,
4639 const variable_list& stochastic_variables)
4641 std::map<variable,data_expression> assignment_map;
4642 for(
const assignment& a: args)
4644 assignment_map[a.lhs()]=a.rhs();
4647 assignment_vector result;
4648 for(
const variable& v: parlist)
4650 if (std::find(stochastic_variables.begin(),stochastic_variables.end(),v)!=stochastic_variables.end())
4653 result.emplace_back(v, v);
4655 else if (free_variables_in_body.find(v)==free_variables_in_body.end())
4658 const data_expression rhs=representative_generator_internal(v.sort());
4659 result.emplace_back(v, rhs);
4663 const std::map<variable,data_expression>::iterator k=assignment_map.find(v);
4664 if (k!=assignment_map.end())
4666 result.emplace_back(k->first, k->second);
4667 assignment_map.erase(k);
4672 return assignment_list(result.begin(), result.end());
4679 const assignment_list& args,
4681 const std::set < process_identifier >& pCRLprocs,
4683 const variable_list& stochastic_variables)
4686 const assignment_list t=find_dummy_arguments(stack.parameters,args,object.get_free_variables(),stochastic_variables);
4694 for (
const process_identifier& p: pCRLprocs)
4702 return processencoding(i,t,stack);
4709 const std::set < process_identifier >& pcrlprcs,
4710 const bool singlestate,
4711 const variable_list& stochastic_variables)
4717 throw mcrl2::runtime_error(
"Process is not regular, as it has stacking vars: " + process::pp(t) +
".");
4722 const process_identifier& procId=atermpp::down_cast<process_instance_assignment>(t).identifier();
4723 const assignment_list& t1=atermpp::down_cast<process_instance_assignment>(t).assignments();
4724 return push_regular(procId,
4729 stochastic_variables);
4732 throw mcrl2::runtime_error(
"Expect seq or name constructing a recursive invocation: " + process::pp(t) +
".");
4737 const assignment_list& args,
4738 const data_expression_list& t2,
4740 const std::set < process_identifier >& pCRLprocs,
4741 const variable_list& vars,
4742 const variable_list& stochastic_variables)
4745 const data_expression_list t=findarguments(object.parameters,
4748 object.get_free_variables(),
4749 stochastic_variables);
4752 for (
const process_identifier& p: pCRLprocs)
4760 const data_expression_list l=processencoding(i,t,stack);
4761 assert(l.size()==function_sort(stack.opns->push.sort()).domain().size());
4762 return application(stack.opns->push,l);
4768 const std::set < process_identifier >& pcrlprcs,
4769 const variable_list& vars,
4770 const variable_list& stochastic_variables)
4783 const data_expression stackframe=make_procargs_stack(process2,stack,pcrlprcs, vars,stochastic_variables);
4784 return push_stack(procId,t1, data_expression_list({ stackframe }),stack,pcrlprcs,vars,stochastic_variables);
4787 return push_stack(procId,t1, data_expression_list({ data_expression(stack.opns->emptystack) }),
4788 stack,pcrlprcs,vars,stochastic_variables);
4794 const assignment_list t1=process_instance_assignment(t).assignments();
4798 return push_stack(procId,
4800 data_expression_list({ data_expression(application(stack.opns->pop,stack.stackvar)) }),
4804 stochastic_variables);
4806 return push_stack(procId,
4808 data_expression_list({ data_expression(stack.opns->emptystack) }),
4812 stochastic_variables);
4815 throw mcrl2::runtime_error(
"Expect seq or name putting processes on a stack: " + process::pp(t) +
".");
4821 const std::set < process_identifier >& pcrlprcs,
4822 const variable_list& vars,
4824 const bool singlestate,
4825 const variable_list& stochastic_variables)
4829 return make_procargs_regular(t,stack,pcrlprcs,singlestate,stochastic_variables);
4832 data_expression sf=make_procargs_stack(t,stack,pcrlprcs,vars,stochastic_variables);
4833 return assignment_list({ assignment(stack.stackvar,sf) });
4838 const variable_list& pars)
4841 for (
const variable& v: pars)
4843 if (name.name()==v.name())
4853 const variable_list& pars,
4857
4858
4859
4861 data_expression_vector result;
4862 for(
const variable& par: stack.parameters)
4865
4866
4867
4868
4869
4870
4871 if (std::find(pars.begin(),pars.end(),par)!=pars.end())
4873 result.push_back(par);
4876
4879 result.push_back(representative_generator_internal(par.sort()));
4882 return data_expression_list(result.begin(), result.end());
4886 const variable_list& pars,
4888 const variable_list& stochastic_variables)
4891
4892
4893
4895 assignment_vector result;
4896 for(
const variable& par: stack.parameters)
4899 if (std::find(stochastic_variables.begin(),stochastic_variables.end(),par)!=pars.end())
4901 result.emplace_back(par, par);
4904 else if (std::find(pars.begin(),pars.end(),par)!=pars.end())
4908
4911 result.emplace_back(par, representative_generator_internal(par.sort()));
4914 return assignment_list(result.begin(), result.end());
4918 const variable_list& totalpars,
4919 const variable_list& pars,
4921 const variable_list& stochastic_variables)
4924
4925
4926
4928 if (totalpars.empty())
4930 return data_expression_list({ data_expression(stack.opns->emptystack) });
4933 const variable& par=totalpars.front();
4934 if (std::find(pars.begin(),pars.end(),par)!=pars.end())
4936 data_expression_list result=pushdummyrec_stack(totalpars.tail(),pars,stack,stochastic_variables);
4937 result.push_front(par);
4941 if (std::find(stochastic_variables.begin(),stochastic_variables.end(),par)!=pars.end())
4943 data_expression_list result=pushdummyrec_stack(totalpars.tail(),pars,stack,stochastic_variables);
4944 result.push_front(par);
4948
4949
4950 data_expression_list result=pushdummyrec_stack(totalpars.tail(),pars,stack,stochastic_variables);
4951 result.push_front(representative_generator_internal(par.sort()));
4956 const variable_list& parameters,
4958 const variable_list& stochastic_variables)
4960 return pushdummyrec_stack(stack.parameters,parameters,stack,stochastic_variables);
4966 const std::set < process_identifier >& pcrlprcs,
4968 const bool singlecontrolstate,
4972 for (
const process_identifier& p: pcrlprcs)
4974 if (p==initialProcId)
4984 data_expression_list result=
4985 pushdummy_regular_data_expressions(objectIndex(initialProcId).parameters,
4987 if (!singlecontrolstate)
4989 return processencoding(i,result,stack);
4995 data_expression_list result=
4996 pushdummy_stack(objectIndex(initialProcId).parameters,
4998 initial_stochastic_distribution.variables());
4999 const data_expression_list l=processencoding(i,result,stack);
5000 assert(l.size()==function_sort(stack.opns->push.sort()).domain().size());
5001 return data_expression_list({ application(stack.opns->push,l) });
5008 const bool singlestate)
5012 return assignment_list();
5015 return processencoding(1,assignment_list(),stack);
5020 stochastic_action_summand_vector& action_summands,
5021 deadlock_summand_vector& deadlock_summands,
5022 const variable_list& sumvars,
5024 const action_list& multiAction,
5027 const assignment_list& procargs,
5028 const bool has_time,
5029 const bool is_deadlock_summand)
5032 assert(std::is_sorted(multiAction.begin(), multiAction.end()));
5040 if (is_deadlock_summand)
5042 insert_timed_delta_summand(action_summands,
5044 deadlock_summand(sumvars,
5045 rewritten_condition,
5046 has_time?deadlock(actTime):deadlock()),options.ignore_time);
5050 action_summands.emplace_back(sumvars,
5051 rewritten_condition,
5052 has_time ? multi_action(multiAction, actTime) : multi_action(multiAction),
5054 stochastic_distribution(distribution.variables(), RewriteTerm(distribution.distribution())));
5061 stochastic_action_summand_vector& action_summands,
5062 deadlock_summand_vector& deadlock_summands,
5064 const std::set < process_identifier >& pCRLprocs,
5067 const bool singlestate,
5068 const variable_list& process_parameters)
5072 action_list multiAction;
5073 bool is_delta_summand=
false;
5074 bool has_time=
false;
5083
5085 variable_list sumvars;
5088 sumvars=sum(summandterm).variables() + sumvars;
5094 maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma;
5095 alphaconvert(sumvars,local_sigma,process_parameters,data_expression_list());
5096 summandterm=substitute_pCRLproc(summandterm, local_sigma);
5102 if (regular && singlestate)
5108 condition1=correctstatecond(procId,pCRLprocs,stack,regular);
5119 if (!(regular && singlestate))
5121 condition1=lazy::and_(
5123 ((regular)?localcondition:
5124 adapt_term_to_stack(
5128 cumulative_distribution.variables())));
5139 const stochastic_operator& sto=atermpp::down_cast<
const stochastic_operator>(summandterm);
5148 if (!cumulative_distribution.variables().empty() && !sumvars.empty())
5150 throw mcrl2::runtime_error(
"Cannot permute sum operator and stochastic distribution in " + data::pp(summandterm));
5167 is_delta_summand=
true;
5172 multiAction=to_sorted_action_list(t1);
5183 const assignment_list procargs=make_procargs(t2_new,stack,pCRLprocs,sumvars,regular,singlestate,distribution.variables());
5187 if (!is_delta_summand)
5189 multiAction=adapt_multiaction_to_stack(
5190 multiAction,stack,sumvars);
5194 atTime=adapt_term_to_stack(
5195 atTime,stack,sumvars,variable_list());
5197 distribution=stochastic_distribution(
5198 distribution.variables(),
5199 adapt_term_to_stack(distribution.distribution(),stack,sumvars,distribution.variables()));
5201 insert_summand(action_summands,deadlock_summands,
5202 sumvars,condition1,multiAction,
5203 atTime,distribution,procargs,
5204 has_time,is_delta_summand);
5222 is_delta_summand=
true;
5230 assert(multiAction.empty());
5231 multiAction.push_front(action(summandterm));
5235 multiAction=to_sorted_action_list(summandterm);
5239 throw mcrl2::runtime_error(
"expected multiaction " + process::pp(summandterm) +
".");
5244 if (!is_delta_summand)
5246
5248 throw mcrl2::runtime_error(
"terminating processes should not exist when using the regular flag");
5250 insert_summand(action_summands,
5256 stochastic_distribution(variable_list(),sort_real::real_one()),
5257 dummyparameterlist(stack,singlestate),
5263 multiAction=adapt_multiaction_to_stack(multiAction,stack,sumvars);
5264 assignment_list procargs ({ assignment(stack.stackvar,application(stack.opns->pop,stack.stackvar)) });
5273 stochastic_distribution(variable_list(),sort_real::real_one()),
5284 stochastic_action_summand_vector& action_summands,
5285 deadlock_summand_vector& deadlock_summands,
5287 const variable_list& pars,
5290 const bool singlestate,
5291 const std::set < process_identifier >& pCRLprocs)
5298 collectsumlistterm(procId,action_summands,deadlock_summands,t1,pars,stack,
5299 regular,singlestate,pCRLprocs);
5300 collectsumlistterm(procId,action_summands,deadlock_summands,t2,pars,stack,
5301 regular,singlestate,pCRLprocs);
5307
5309 collectsumlistterm(procId,action_summands,deadlock_summands,sto.operand(),pars,stack,
5310 regular,singlestate,pCRLprocs);
5314 add_summands(procId,
5327 stochastic_action_summand_vector& action_summands,
5328 deadlock_summand_vector& deadlock_summands,
5329 const std::set < process_identifier >& pCRLprocs,
5330 const variable_list& pars,
5335 for (
const process_identifier& p: pCRLprocs)
5337 objectdatatype& object=objectIndex(p);
5370 elementnames = data_expression_list({ sort_bool::false_(), sort_bool::true_()});
5375 basic_sort sort_id(spec.fresh_identifier_generator(
"Enum" + std::to_string(n)));
5379 structured_sort_constructor_list struct_conss;
5380 for (std::size_t j=0 ; (j<n) ; j++)
5383 const identifier_string s=spec.fresh_identifier_generator(
"e" + std::to_string(j) +
"_" + std::to_string(n));
5384 const structured_sort_constructor struct_cons(s,
"");
5386 struct_conss.push_front(struct_cons);
5391 spec.data.add_alias(
alias(sort_id
, sort_struct
));
5395 const function_symbol_vector& constructors=spec.data.constructors(sort_id);
5396 assert(constructors.size()==n);
5397 elementnames = data::data_expression_list(constructors.begin(),constructors.end());
5405 elementnames=e.elementnames;
5406 functions=e.functions;
5419 for (w=0; ((w<enumeratedtypes.size()) && (enumeratedtypes[w].size!=n)); ++w) {};
5421 if (w==enumeratedtypes.size())
5423 enumeratedtypes.emplace_back(n, *
this);
5430 for (
const data::function_symbol& f: enumeratedtypes[index].functions)
5432 sort_expression_list domain = function_sort(f.sort()).domain();
5433 assert(domain.size() >= 2);
5434 if (*(++domain.begin())==sort)
5440 throw mcrl2::runtime_error(
"searching for a nonexisting case function on sort " + data::pp(sort) +
".");
5445 const std::size_t index,
5450 data_expression_list args;
5451 data_expression_list xxxterm;
5453 const variable v1=get_fresh_variable(
"x",sort);
5454 const std::size_t n=enumeratedtypes[index].size;
5455 for (std::size_t j=0; (j<n); j++)
5457 const variable v=get_fresh_variable(
"y",sort);
5460 xxxterm.push_front(v1);
5464
5466 const variable v=get_fresh_variable(
"e",s);
5470 xxxterm.push_front(data_expression(v));
5473 variable_list({ v1, v }),
5474 application(functionname,xxxterm),
5478 variable_list auxvars=vars;
5480 const data_expression_list& elementnames=enumeratedtypes[index].elementnames;
5481 for (
const data_expression& w: elementnames)
5483 assert(auxvars.size()>0);
5485 data.add_equation(data_equation(
5487 application(functionname,args),
5491 auxvars.pop_front();
5497 const std::size_t enumeratedtype_index)
5499 assert(enumeratedtype_index<enumeratedtypes.size());
5501
5503 const function_symbol_list& functions=enumeratedtypes[enumeratedtype_index].functions;
5504 const function_symbol_list::const_iterator i = std::find_if(functions.begin(), functions.end(), [&sort](
const data::function_symbol& w){
5505 const function_sort& w1sort(down_cast<function_sort>(w.sort()));
5506 assert(function_sort(w1sort).domain().size()>1);
5508 return *(++(w1sort.domain().begin())) == sort;
5510 if(i != functions.end()) {
5514
5516 if (enumeratedtypes[enumeratedtype_index].sortId==sort_bool::bool_())
5519 enumeratedtypes[enumeratedtype_index].functions.push_front(if_(sort));
5523 sort_expression_list newsortlist;
5524 const std::size_t n=enumeratedtypes[enumeratedtype_index].size;
5525 for (std::size_t j=0; j<n ; ++j)
5527 newsortlist.push_front(sort);
5529 const sort_expression& sid=enumeratedtypes[enumeratedtype_index].sortId;
5530 newsortlist.push_front(sid);
5534 fresh_identifier_generator(
"C" + std::to_string(n) +
"_" +
5535 (!is_basic_sort(newsort)?
"":std::string(basic_sort(sort).name()))), newsort);
5536 data.add_mapping(casefunction);
5537 enumeratedtypes[enumeratedtype_index].functions.push_front(casefunction);
5539 define_equations_for_case_function(enumeratedtype_index,casefunction,sort);
5554 const sort_expression_list& fsorts,
5555 const sort_expression_list& gsorts,
5558 enumeratedtype_index=spec.create_enumeratedtype(n);
5560 var=variable(spec.fresh_identifier_generator(
"e"),spec.enumeratedtypes[enumeratedtype_index].sortId);
5563 for (
const sort_expression& f: fsorts)
5565 spec.create_case_function_on_enumeratedtype(f,enumeratedtype_index);
5568 for (
const sort_expression& f: gsorts)
5570 spec.create_case_function_on_enumeratedtype(f,enumeratedtype_index);
5573 spec.create_case_function_on_enumeratedtype(sort_bool::bool_(),enumeratedtype_index);
5577 spec.create_case_function_on_enumeratedtype(sort_real::real_(),enumeratedtype_index);
5586
5587
5588
5589
5590
5591
5592
5593
5594
5599 const variable_list& v,
5600 variable_list& matchinglist,
5601 variable_list& pars,
5602 data_expression_list& args,
5603 const variable_list& process_parameters)
5605 variable_list auxmatchinglist;
5608
5611
5613 for (variable_list::const_iterator i=matchinglist.begin();
5614 i!=matchinglist.end(); ++i)
5617 if (var.sort()==var1.sort())
5622 pars.push_front(var);
5623 args.push_front(data_expression(var1));
5626 for (++i ; i!=matchinglist.end(); ++i)
5628 auxmatchinglist.push_front(*i);
5630 matchinglist=reverse(auxmatchinglist);
5635 auxmatchinglist.push_front(var1);
5640
5642 matchinglist=reverse(auxmatchinglist);
5645
5646
5647
5648 for (
const variable& var1 : v)
5650 if (var.name() == var1.name())
5652 pars.push_front(var);
5653 var=get_fresh_variable(var.name(),var.sort());
5654 args.push_front(data_expression(var));
5660
5661 for (
const variable& var1: process_parameters)
5663 if (var.name()==var1.name())
5665 pars.push_front(var);
5666 var=get_fresh_variable(var.name(),var.sort());
5667 args.push_front(data_expression(var));
5678 return data_expression_list(cl.begin(),
5680 [&c](
const data_expression& e)->data_expression {
return lazy::and_(c,e);} );
5687 for(
const variable& v: vl)
5689 const data_expression unique=representative_generator_internal(v.sort(),
false);
5690 result=lazy::and_(result,equal_to(v,unique));
5698 const data_expression_list& conditionlist)
5704 return extend(newcondition,conditionlist);
5706 catch (mcrl2::runtime_error&)
5712 return conditionlist;
5720 for(
const variable& v: matchinglist)
5724 data_expression unique=representative_generator_internal(v.sort(),
false);
5725 result=lazy::and_(result, equal_to(v,unique));
5727 catch (mcrl2::runtime_error&)
5737 const variable_list& matchinglist,
5738 const data_expression_list& conditionlist)
5740 data_expression_list result=conditionlist;
5741 result.push_front(transform_matching_list(matchinglist));
5746
5747
5748
5749
5750
5753 const variable_list& v1,
5754 const variable_list& v2,
5755 std::vector < variable_list>& renamings_pars,
5756 std::vector < data_expression_list>& renamings_args,
5757 data_expression_list& conditionlist,
5758 const variable_list& process_parameters)
5760 data_expression_list renamingargs;
5761 variable_list renamingpars;
5762 variable_list matchinglist=v2;
5765
5766
5768 variable_list v1h=(v2.empty()?reverse(v1):v1);
5770 variable_list result=v2;
5771 for (
const variable& v_: v1h)
5774 if (!mergeoccursin(v,v2,
5775 matchinglist,renamingpars,renamingargs,process_parameters))
5777 result.push_front(v);
5778 conditionlist=extend_conditions(v,conditionlist);
5781 conditionlist=addcondition(matchinglist,conditionlist);
5782 renamings_pars.push_back(renamingpars);
5783 renamings_args.push_back(renamingargs);
5791 const variable_list& tail)
5793 variable_list result;
5798 for (result=tail ; (n>0) ; n=n/2)
5800 variable sumvar=get_fresh_variable(
"e",enumtypename);
5801 result.push_front(sumvar);
5804 condition=lazy::and_(sumvar,condition);
5808 condition=lazy::or_(sumvar,condition);
5816 const variable_list& sums,
5817 data_expression_list& terms,
5821 assert(!terms.empty());
5825 assert(!terms.empty());
5831 assert(!sums.empty());
5832 const variable& casevar=sums.front();
5834 const data_expression t=construct_binary_case_tree_rec(n / 2,sums.tail(),terms,termsort,e);
5841 const data_expression t1=construct_binary_case_tree_rec(n / 2,sums.tail(),terms,termsort,e);
5847 return application(find_case_function(e.enumeratedtype_index, termsort), casevar, t, t1);
5859 for(++i ; i!=l.end(); ++i)
5871 const variable_list& sums,
5872 data_expression_list terms,
5876 return construct_binary_case_tree_rec(n-1,sums,terms,termsort,e);
5890
5893
5894
5895
5896
5898 const action_list multiactionlist1=summand1.multi_action().actions();
5899 const action_list multiactionlist2=summand2.multi_action().actions();
5900 action_list::const_iterator i2=multiactionlist2.begin();
5901 for (action_list::const_iterator i1=multiactionlist1.begin(); i1!=multiactionlist1.end(); ++i1,++i2)
5903 if (i2==multiactionlist2.end())
5907 if (i1->label()!=i2->label())
5912 return i2 == multiactionlist2.end();
5918 for (
const assignment& a: as)
5934 const data_expression_list& resultnextstate,
5935 const variable_list& sum_vars,
5936 const variable_list& stoch_vars)
5938 assert(parameters.size()==resultnextstate.size());
5940 data_expression_list::const_iterator i=resultnextstate.begin();
5941 return assignment_list(parameters.begin(),
5943 [&i](
const variable& p){
return assignment(p, *i++); },
5944 [&sum_vars, &stoch_vars](
const assignment& p)
5945 {
return p.lhs()!=p.rhs() ||
5946 std::find(sum_vars.begin(),sum_vars.end(),p.rhs())!=sum_vars.end() ||
5947 std::find(stoch_vars.begin(),stoch_vars.end(),p.rhs())!=stoch_vars.end(); });
5954 const stochastic_action_summand_vector& action_summands,
5955 const variable_list& parameters)
5958
5959
5960
5961
5962
5964 std::size_t n=action_summands.size();
5965 variable_list resultsum;
5967 action_list resultmultiaction;
5970 std::vector < variable_list > rename_list_pars;
5971 std::vector < data_expression_list > rename_list_args;
5973 data_expression_list conditionlist;
5975 int equaluptillnow=1;
5977 std::set<variable> all_sum_variables;
5978 for (
const stochastic_action_summand& smmnd: action_summands)
5980 const variable_list sumvars=smmnd.summation_variables();
5981 resultsum=merge_var(sumvars,resultsum,rename_list_pars,rename_list_args,conditionlist,parameters);
5982 all_sum_variables.insert(sumvars.begin(),sumvars.end());
5987 resultsum=make_binary_sums(
5989 enumeratedtypes[e.enumeratedtype_index].sortId,
5995 resultsum.push_front(e.var);
5999 data_expression_list auxresult;
6000 std::vector < variable_list >::const_iterator auxrename_list_pars=rename_list_pars.begin();
6001 std::vector < data_expression_list >::const_iterator auxrename_list_args=rename_list_args.begin();
6005 for (
const stochastic_action_summand& smmnd: action_summands)
6007 const data_expression& condition=smmnd.condition();
6008 assert(auxrename_list_pars!=rename_list_pars.end());
6009 assert(auxrename_list_args!=rename_list_args.end());
6010 const variable_list auxpars= *auxrename_list_pars;
6011 ++auxrename_list_pars;
6012 const data_expression_list auxargs= *auxrename_list_args;
6013 ++auxrename_list_args;
6014 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
6015 data_expression_list::const_iterator j=auxargs.begin();
6016 for (variable_list::const_iterator i=auxpars.begin();
6017 i!=auxpars.end(); ++i, ++j)
6025 maintain_variables_in_rhs< mutable_map_substitution<> > mutable_sigma(sigma);
6027 const data_expression auxresult1=replace_variables_capture_avoiding_alt(condition,mutable_sigma);
6028 if (equalterm==data_expression()||is_global_variable(equalterm))
6030 equalterm=auxresult1;
6036 equaluptillnow=((auxresult1==equalterm)||is_global_variable(auxresult1));
6039 auxresult.push_front(auxresult1);
6043 resultcondition=construct_binary_case_tree(n,
6044 resultsum,auxresult,sort_bool::bool_(),e);
6046 resultcondition=lazy::and_(
6047 construct_binary_case_tree(n,
6048 resultsum,conditionlist,sort_bool::bool_(),e),
6055 if (all_equal(conditionlist))
6057 resultcondition=lazy::and_(conditionlist.front(), equalterm);
6061 data_expression_list tempconditionlist=conditionlist;
6062 tempconditionlist.push_front(data_expression(e.var));
6063 resultcondition=lazy::and_(
6065 find_case_function(e.enumeratedtype_index,sort_bool::bool_()),
6072 data_expression_list tempauxresult=auxresult;
6073 tempauxresult.push_front(data_expression(e.var));
6074 resultcondition=application(
6075 find_case_function(e.enumeratedtype_index,sort_bool::bool_()),
6077 if (all_equal(conditionlist))
6079 resultcondition=lazy::and_(conditionlist.front(),resultcondition);
6083 data_expression_list tempconditionlist=conditionlist;
6084 tempconditionlist.push_front(data_expression(e.var));
6085 resultcondition=lazy::and_(
6087 find_case_function(e.enumeratedtype_index,sort_bool::bool_()),
6096
6097 std::vector < action_list > multiActionList;
6099 for (
const stochastic_action_summand& smmnd: action_summands)
6101 multiActionList.push_back(smmnd.multi_action().actions());
6104 action_list resultmultiactionlist;
6105 std::size_t multiactioncount= multiActionList[0].size();
6106 for (; multiactioncount>0 ; multiactioncount--)
6108 data_expression_list resultf;
6110 action_list::const_iterator a=multiActionList[0].begin();
6111 for (std::size_t i=1 ; i<multiactioncount ; ++i,++a) {}
6112 std::size_t fcnt=(a->arguments()).size();
6115 for (; fcnt>0 ; fcnt--)
6117 data_expression_list auxresult;
6118 data_expression equalterm;
6119 bool equaluptillnow=
true;
6120 std::vector < variable_list > ::const_iterator auxrename_list_pars=rename_list_pars.begin();
6121 std::vector < data_expression_list >::const_iterator auxrename_list_args=rename_list_args.begin();
6122 std::vector<action_list>::const_iterator multiactionwalker=multiActionList.begin();
6123 for (stochastic_action_summand_vector::const_iterator walker=action_summands.begin(); walker!=action_summands.end();
6124 ++walker,++multiactionwalker)
6126 assert(auxrename_list_pars!=rename_list_pars.end());
6127 assert(auxrename_list_args!=rename_list_args.end());
6128 const variable_list auxpars= *auxrename_list_pars;
6129 ++auxrename_list_pars;
6130 const data_expression_list auxargs= *auxrename_list_args;
6131 ++auxrename_list_args;
6133 action_list::const_iterator a1=multiactionwalker->begin();
6134 for (std::size_t i=1; i<multiactioncount; ++i, ++a1) {};
6135 data_expression_list::const_iterator d1=(a1->arguments()).begin();
6136 for (std::size_t i=1; i<fcnt; ++i, ++d1) {};
6138 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
6139 data_expression_list::const_iterator j=auxargs.begin();
6140 for (variable_list::const_iterator i=auxpars.begin();
6141 i!=auxpars.end(); ++i, ++j)
6150 maintain_variables_in_rhs< mutable_map_substitution<> > mutable_sigma(sigma);
6151 const data_expression auxresult1=replace_variables_capture_avoiding_alt(f,mutable_sigma);
6153 if (equalterm==data_expression()||is_global_variable(equalterm))
6155 equalterm=auxresult1;
6161 equaluptillnow=((equalterm==auxresult1)||is_global_variable(auxresult1));
6164 auxresult.push_front(auxresult1);
6168 resultf.push_front(equalterm);
6172 if (!options.binary)
6174 data_expression_list tempauxresult=auxresult;
6175 tempauxresult.push_front(data_expression(e.var));
6176 resultf.push_front(data_expression(application(
6177 find_case_function(e.enumeratedtype_index,f.sort()),
6182 data_expression temp=construct_binary_case_tree(
6188 resultf.push_front(temp);
6192 a=multiActionList[0].begin();
6193 for (std::size_t i=1 ; i<multiactioncount ; ++i,++a) {}
6194 resultmultiactionlist.push_front(action(a->label(),resultf));
6199 equaluptillnow=
true;
6201 bool some_summand_has_time=
false;
6202 bool all_summands_have_time=
true;
6205 for (
const stochastic_action_summand& smmnd: action_summands)
6207 if (smmnd.has_time())
6209 some_summand_has_time=
true;
6213 all_summands_have_time=
false;
6217 if (some_summand_has_time)
6220 if (!all_summands_have_time)
6223 dummy_time_variable=get_fresh_variable(
"dt",sort_real::real_());
6224 resultsum.push_front(dummy_time_variable);
6226 std::vector < variable_list >::const_iterator auxrename_list_pars=rename_list_pars.begin();
6227 std::vector < data_expression_list >::const_iterator auxrename_list_args=rename_list_args.begin();
6228 data_expression_list auxresult;
6229 for (
const stochastic_action_summand& smmnd: action_summands)
6231 if (smmnd.has_time())
6233 const data_expression& actiontime=smmnd.multi_action().time();
6235 assert(auxrename_list_pars!=rename_list_pars.end());
6236 assert(auxrename_list_args!=rename_list_args.end());
6237 const variable_list auxpars= *auxrename_list_pars;
6238 ++auxrename_list_pars;
6239 const data_expression_list auxargs= *auxrename_list_args;
6240 ++auxrename_list_args;
6242 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
6243 data_expression_list::const_iterator j=auxargs.begin();
6244 for (variable_list::const_iterator i=auxpars.begin();
6245 i!=auxpars.end(); ++i, ++j)
6254 maintain_variables_in_rhs< mutable_map_substitution<> > mutable_sigma(sigma);
6255 const data_expression auxresult1=replace_variables_capture_avoiding_alt(actiontime, mutable_sigma);
6256 if (equalterm==data_expression()||is_global_variable(equalterm))
6258 equalterm=auxresult1;
6264 equaluptillnow=((auxresult1==equalterm)||is_global_variable(auxresult1));
6267 auxresult.push_front(auxresult1);
6272 auxresult.push_front(data_expression(dummy_time_variable));
6273 equaluptillnow=
false;
6276 if (options.binary==1)
6278 resulttime=construct_binary_case_tree(n,
6279 resultsum,auxresult,sort_real::real_(),e);
6285 resulttime
=equalterm;
6289 data_expression_list tempauxresult=auxresult;
6290 tempauxresult.push_front(data_expression(e.var));
6291 resulttime=application(
6292 find_case_function(e.enumeratedtype_index,sort_real::real_()),
6301 variable_list resulting_stochastic_variables;
6302 std::vector < variable_list > stochastic_rename_list_pars;
6303 std::vector < data_expression_list > stochastic_rename_list_args;
6306 data_expression_list stochastic_conditionlist;
6307 for (
const stochastic_action_summand& smmnd: action_summands)
6309 const variable_list stochastic_vars=smmnd.distribution().variables();
6310 resulting_stochastic_variables=merge_var(stochastic_vars,resulting_stochastic_variables,
6311 stochastic_rename_list_pars,stochastic_rename_list_args,stochastic_conditionlist,
6312 parameters + variable_list(all_sum_variables.begin(),all_sum_variables.end()));
6315 std::vector < variable_list >::const_iterator auxrename_list_pars=rename_list_pars.begin();
6316 std::vector < data_expression_list >::const_iterator auxrename_list_args=rename_list_args.begin();
6318 std::vector < variable_list >::const_iterator stochastic_auxrename_list_pars=stochastic_rename_list_pars.begin();
6319 std::vector < data_expression_list >::const_iterator stochastic_auxrename_list_args=stochastic_rename_list_args.begin();
6321 data_expression_list aux_result;
6324 for (
const stochastic_action_summand& smmnd: action_summands)
6326 const data_expression& dist=smmnd.distribution().distribution();
6327 const variable_list stochastic_variables=smmnd.distribution().variables();
6328 assert(auxrename_list_pars!=rename_list_pars.end());
6329 assert(auxrename_list_args!=rename_list_args.end());
6330 assert(stochastic_auxrename_list_pars!=stochastic_rename_list_pars.end());
6331 assert(stochastic_auxrename_list_args!=stochastic_rename_list_args.end());
6333 const variable_list auxpars= *auxrename_list_pars;
6334 ++auxrename_list_pars;
6335 const data_expression_list auxargs= *auxrename_list_args;
6336 ++auxrename_list_args;
6337 const variable_list stochastic_auxpars= *stochastic_auxrename_list_pars;
6338 ++stochastic_auxrename_list_pars;
6339 const data_expression_list stochastic_auxargs= *stochastic_auxrename_list_args;
6340 ++stochastic_auxrename_list_args;
6341 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
6342 data_expression_list::const_iterator j=stochastic_auxargs.begin();
6343 for (variable_list::const_iterator i=stochastic_auxpars.begin();
6344 i!=stochastic_auxpars.end(); ++i, ++j)
6353 for (variable_list::const_iterator i=auxpars.begin();
6354 i!=auxpars.end(); ++i, ++j)
6362 maintain_variables_in_rhs< mutable_map_substitution<> > mutable_sigma(sigma);
6364 const data_expression auxresult1=replace_variables_capture_avoiding_alt(dist,mutable_sigma);
6365 if (equalterm==data_expression()||is_global_variable(equalterm))
6367 equalterm=auxresult1;
6373 equaluptillnow=((auxresult1==equalterm)||is_global_variable(auxresult1));
6376 aux_result.push_front(auxresult1);
6380 resulting_distribution=construct_binary_case_tree(n,
6381 resultsum,aux_result,sort_real::real_(),e);
6382 resulting_distribution=lazy::and_(
6383 construct_binary_case_tree(n,
6384 resultsum,stochastic_conditionlist,sort_bool::bool_(),e),
6385 resulting_distribution);
6391 if (all_equal(stochastic_conditionlist))
6393 if (stochastic_conditionlist.front()==sort_bool::true_())
6395 resulting_distribution
=equalterm;
6399 resulting_distribution=real_times_optimized(
6400 if_(stochastic_conditionlist.front(),sort_real::real_one(),sort_real::real_zero()),
6406 data_expression_list temp_stochastic_conditionlist=stochastic_conditionlist;
6407 temp_stochastic_conditionlist.push_front(data_expression(e.var));
6408 resulting_distribution=real_times_optimized(
6410 find_case_function(e.enumeratedtype_index,sort_bool::bool_()),
6411 temp_stochastic_conditionlist),
6412 sort_real::real_one(),
6413 sort_real::real_zero()),
6419 data_expression_list tempauxresult=aux_result;
6420 tempauxresult.push_front(data_expression(e.var));
6421 resulting_distribution=application(
6422 find_case_function(e.enumeratedtype_index,sort_real::real_()),
6424 if (all_equal(stochastic_conditionlist))
6426 if (stochastic_conditionlist.front()==sort_bool::true_())
6428 resulting_distribution=real_times_optimized(
6429 if_(stochastic_conditionlist.front(),sort_real::real_one(),sort_real::real_zero()),
6430 resulting_distribution);
6434 resulting_distribution=real_times_optimized(
6435 if_(stochastic_conditionlist.front(),sort_real::real_one(),sort_real::real_zero()),
6436 resulting_distribution);
6441 data_expression_list temp_stochastic_conditionlist=stochastic_conditionlist;
6442 temp_stochastic_conditionlist.push_front(data_expression(e.var));
6443 resulting_distribution=real_times_optimized(
6445 find_case_function(e.enumeratedtype_index,sort_bool::bool_()),
6446 temp_stochastic_conditionlist),
6447 sort_real::real_one(),
6448 sort_real::real_zero()),
6449 resulting_distribution);
6455
6456 data_expression_list resultnextstate;
6458 for (
const variable& var: parameters)
6460 equalterm=data_expression();
6462 std::vector < variable_list >::const_iterator auxrename_list_pars=rename_list_pars.begin();
6463 std::vector < data_expression_list >::const_iterator auxrename_list_args=rename_list_args.begin();
6464 std::vector < variable_list >::const_iterator stochastic_auxrename_list_pars=stochastic_rename_list_pars.begin();
6465 std::vector < data_expression_list >::const_iterator stochastic_auxrename_list_args=stochastic_rename_list_args.begin();
6466 data_expression_list auxresult;
6467 for (
const stochastic_action_summand& smmnd: action_summands)
6469 const assignment_list nextstate=smmnd.assignments();
6470 assert(auxrename_list_pars!=rename_list_pars.end());
6471 assert(auxrename_list_args!=rename_list_args.end());
6472 assert(stochastic_auxrename_list_pars!=stochastic_rename_list_pars.end());
6473 assert(stochastic_auxrename_list_args!=stochastic_rename_list_args.end());
6474 const variable_list auxpars= *auxrename_list_pars;
6475 ++auxrename_list_pars;
6476 const data_expression_list auxargs= *auxrename_list_args;
6477 ++auxrename_list_args;
6478 const variable_list stochastic_auxpars= *stochastic_auxrename_list_pars;
6479 ++stochastic_auxrename_list_pars;
6480 const data_expression_list stochastic_auxargs= *stochastic_auxrename_list_args;
6481 ++stochastic_auxrename_list_args;
6483 data_expression nextstateparameter;
6484 nextstateparameter=getRHSassignment(var,nextstate);
6486 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
6487 data_expression_list::const_iterator j=stochastic_auxargs.begin();
6488 for (variable_list::const_iterator i=stochastic_auxpars.begin();
6489 i!=stochastic_auxpars.end(); ++i, ++j)
6498 for (variable_list::const_iterator i=auxpars.begin();
6499 i!=auxpars.end(); ++i, ++j)
6508 maintain_variables_in_rhs< mutable_map_substitution<> > mutable_sigma(sigma);
6509 data_expression auxresult1=replace_variables_capture_avoiding_alt(nextstateparameter, mutable_sigma);
6510 if (equalterm==data_expression())
6515 equalterm=auxresult1;
6517 else if (equaluptillnow)
6524 equaluptillnow=((equalterm==auxresult1)||
6525 ((equalterm==data_expression()||is_global_variable(equalterm)) &&
6526 is_global_variable(auxresult1)));
6529 auxresult.push_front(auxresult1);
6533 resultnextstate.push_front(equalterm);
6537 if (!options.binary)
6539 data_expression_list tempauxresult=auxresult;
6540 tempauxresult.push_front(data_expression(e.var));
6541 resultnextstate.push_front(
6542 data_expression(application(
6544 e.enumeratedtype_index,
6550 data_expression temp=construct_binary_case_tree(
6556 resultnextstate.push_front(temp);
6561 resultnextstate=reverse(resultnextstate);
6563
6564 const assignment_list final_resultnextstate=make_optimised_assignment_list(parameters,resultnextstate,resultsum,resulting_stochastic_variables);
6565 return stochastic_action_summand(
6568 some_summand_has_time?multi_action(resultmultiactionlist,resulttime):multi_action(resultmultiactionlist),
6569 final_resultnextstate,
6570 stochastic_distribution(resulting_stochastic_variables,resulting_distribution));
6575 const deadlock_summand_vector& deadlock_summands,
6576 const variable_list& parameters)
6579
6580
6581
6582
6583
6585 std::size_t n=deadlock_summands.size();
6586 variable_list resultsum;
6588 action_list resultmultiaction;
6591 std::vector < variable_list > rename_list_pars;
6592 std::vector < data_expression_list > rename_list_args;
6594 data_expression_list conditionlist;
6596 int equaluptillnow=1;
6598 for (
const deadlock_summand& smmnd: deadlock_summands)
6600 const variable_list sumvars=smmnd.summation_variables();
6601 resultsum=merge_var(sumvars,resultsum,rename_list_pars,rename_list_args,conditionlist,parameters);
6606 resultsum=make_binary_sums(
6608 enumeratedtypes[e.enumeratedtype_index].sortId,
6614 resultsum.push_front(e.var);
6618 data_expression_list auxresult;
6619 std::vector < variable_list >::const_iterator auxrename_list_pars=rename_list_pars.begin();
6620 std::vector < data_expression_list >::const_iterator auxrename_list_args=rename_list_args.begin();
6624 for (
const deadlock_summand& smmnd: deadlock_summands)
6626 const data_expression& condition=smmnd.condition();
6627 assert(auxrename_list_pars!=rename_list_pars.end());
6628 assert(auxrename_list_args!=rename_list_args.end());
6629 const variable_list auxpars= *auxrename_list_pars;
6630 ++auxrename_list_pars;
6631 const data_expression_list auxargs= *auxrename_list_args;
6632 ++auxrename_list_args;
6633 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
6634 data_expression_list::const_iterator j=auxargs.begin();
6635 for (variable_list::const_iterator i=auxpars.begin();
6636 i!=auxpars.end(); ++i, ++j)
6645 maintain_variables_in_rhs< mutable_map_substitution<> > mutable_sigma(sigma);
6646 const data_expression auxresult1=replace_variables_capture_avoiding_alt(condition, mutable_sigma);
6647 if (equalterm==data_expression()||is_global_variable(equalterm))
6649 equalterm=auxresult1;
6655 equaluptillnow=((auxresult1==equalterm)||is_global_variable(auxresult1));
6658 auxresult.push_front(auxresult1);
6662 resultcondition=construct_binary_case_tree(n,
6663 resultsum,auxresult,sort_bool::bool_(),e);
6665 resultcondition=lazy::and_(
6666 construct_binary_case_tree(n,
6667 resultsum,conditionlist,sort_bool::bool_(),e),
6674 if (all_equal(conditionlist))
6676 resultcondition=lazy::and_(conditionlist.front(),equalterm);
6680 data_expression_list tempconditionlist=conditionlist;
6681 tempconditionlist.push_front(data_expression(e.var));
6682 resultcondition=lazy::and_(
6684 find_case_function(e.enumeratedtype_index,sort_bool::bool_()),
6691 data_expression_list tempauxresult=auxresult;
6692 tempauxresult.push_front(data_expression(e.var));
6693 resultcondition=application(
6694 find_case_function(e.enumeratedtype_index,sort_bool::bool_()),
6696 if (all_equal(conditionlist))
6698 resultcondition=lazy::and_(conditionlist.front(),resultcondition);
6702 data_expression_list tempconditionlist=conditionlist;
6703 tempconditionlist.push_front(data_expression(e.var));
6704 resultcondition=lazy::and_(
6706 find_case_function(e.enumeratedtype_index,sort_bool::bool_()),
6715
6716 std::vector < action_list > multiActionList;
6718 action_list resultmultiactionlist;
6722 equaluptillnow=
true;
6724 bool some_summand_has_time=
false;
6725 bool all_summands_have_time=
true;
6728 for (
const deadlock_summand& smmnd: deadlock_summands)
6730 if (smmnd.deadlock().has_time())
6732 some_summand_has_time=
true;
6736 all_summands_have_time=
false;
6740 if ((some_summand_has_time))
6743 if (!all_summands_have_time)
6746 dummy_time_variable=get_fresh_variable(
"dt",sort_real::real_());
6747 resultsum.push_front(dummy_time_variable);
6749 std::vector < variable_list >::const_iterator auxrename_list_pars=rename_list_pars.begin();
6750 std::vector < data_expression_list >::const_iterator auxrename_list_args=rename_list_args.begin();
6751 data_expression_list auxresult;
6752 for (
const deadlock_summand& smmnd: deadlock_summands)
6754 if (smmnd.deadlock().has_time())
6756 const data_expression& actiontime=smmnd.deadlock().time();
6758 assert(auxrename_list_pars!=rename_list_pars.end());
6759 assert(auxrename_list_args!=rename_list_args.end());
6760 const variable_list auxpars= *auxrename_list_pars;
6761 ++auxrename_list_pars;
6762 const data_expression_list auxargs= *auxrename_list_args;
6763 ++auxrename_list_args;
6765 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
6766 data_expression_list::const_iterator j=auxargs.begin();
6767 for (variable_list::const_iterator i=auxpars.begin();
6768 i!=auxpars.end(); ++i, ++j)
6777 maintain_variables_in_rhs< mutable_map_substitution<> > mutable_sigma(sigma);
6778 const data_expression auxresult1=replace_variables_capture_avoiding_alt(actiontime, mutable_sigma);
6779 if (equalterm==data_expression()||is_global_variable(equalterm))
6781 equalterm=auxresult1;
6787 equaluptillnow=((auxresult1==equalterm)||is_global_variable(auxresult1));
6790 auxresult.push_front(auxresult1);
6795 auxresult.push_front(data_expression(dummy_time_variable));
6796 equaluptillnow=
false;
6799 if (options.binary==1)
6801 resulttime=construct_binary_case_tree(n,
6802 resultsum,auxresult,sort_real::real_(),e);
6808 resulttime
=equalterm;
6812 data_expression_list tempauxresult=auxresult;
6813 tempauxresult.push_front(data_expression(e.var));
6814 resulttime=application(
6815 find_case_function(e.enumeratedtype_index,sort_real::real_()),
6821 return deadlock_summand(resultsum,
6823 some_summand_has_time?deadlock(resulttime):deadlock());
6829 sort_expression_list resultsorts;
6831 for (
const action& act: actionlist)
6833 resultsorts=act.label().sorts()+resultsorts;
6839 stochastic_action_summand_vector& action_summands,
6840 deadlock_summand_vector& deadlock_summands,
6841 const variable_list& pars)
6845
6846
6848 stochastic_action_summand_vector result;
6849 stochastic_action_summand_vector reducible_sumlist=action_summands;
6851 for (
const stochastic_action_summand& summand1: action_summands)
6853 stochastic_action_summand_vector w1;
6854 stochastic_action_summand_vector w2;
6855 for (
const stochastic_action_summand& summand2: reducible_sumlist)
6857 if (summandsCanBeClustered(summand1,summand2))
6859 w1.push_back(summand2);
6863 w2.push_back(summand2);
6866 reducible_sumlist.swap(w2);
6869
6870
6871 std::size_t n=w1.size();
6877 const action_list multiaction=w1.front().multi_action().actions();
6878 sort_expression_list actionsorts;
6879 actionsorts=getActionSorts(multiaction);
6881 const enumtype enumeratedtype_(options.binary?2:n,actionsorts,get_sorts(pars),*
this);
6883 result.push_back(collect_sum_arg_arg_cond(enumeratedtype_,w1,pars));
6887 for(
const stochastic_action_summand& summand: result)
6889 w1.push_back(summand);
6895 action_summands=result;
6899 deadlock_summand_vector result;
6900 deadlock_summand_vector reducible_sumlist=deadlock_summands;
6902 for (
const deadlock_summand& summand1: deadlock_summands)
6904 deadlock_summand_vector w1;
6905 deadlock_summand_vector w2;
6906 for (
const deadlock_summand& summand2: reducible_sumlist)
6908 if (summand1.deadlock().has_time()==summand2.deadlock().has_time())
6910 w1.push_back(summand2);
6914 w2.push_back(summand2);
6917 reducible_sumlist.swap(w2);
6920
6921
6922 const std::size_t n=w1.size();
6928 sort_expression_list actionsorts;
6930 const enumtype enumeratedtype_(options.binary?2:n,actionsorts,get_sorts(pars),*
this);
6932 result.push_back(collect_sum_arg_arg_cond(enumeratedtype_,w1,pars));
6936 assert(w1.size()==1);
6937 result.push_back(w1.front());
6941 assert(reducible_sumlist.empty());
6942 deadlock_summands.swap(result);
6950
6953 deadlock_summand_vector& deadlock_summands,
6955 const bool containstime,
6957 variable_list& parameters,
6958 data_expression_list& init,
6961
6964 assert(action_summands.empty());
6965 assert(deadlock_summands.empty());
6967 bool singlecontrolstate=
false;
6968 std::set< process_identifier > reachable_process_identifiers;
6969 make_pCRL_procs(procId, reachable_process_identifiers);
6972
6973
6974
6975
6976
6977
6978 const std::set< process_identifier > reduced_set_of_process_identifiers =
6979 minimize_set_of_reachable_process_identifiers(reachable_process_identifiers,procId);
6982
6983
6984
6985
6988 std::set< process_identifier > stochastic_normalized_process_identifiers =
6989 remove_stochastic_operators_from_front(reduced_set_of_process_identifiers, initial_proc_id, initial_stochastic_distribution);
6992
6993 if (stochastic_normalized_process_identifiers.size()==1)
6995 singlecontrolstate=
true;
6997 parameters=collectparameterlist(stochastic_normalized_process_identifiers);
6999 if ((!regular)||((!singlecontrolstate) && (options.newstate) && (!options.binary)))
7001 declare_control_state(stochastic_normalized_process_identifiers);
7003 stacklisttype stack(parameters,*
this,regular,stochastic_normalized_process_identifiers,singlecontrolstate);
7007 if ((options.binary) && (options.newstate))
7009 parameters=stack.parameters;
7010 if (!singlecontrolstate)
7012 parameters=reverse(stack.booleanStateVariables) + parameters;
7017 variable_list tempparameters=stack.parameters;
7018 tempparameters.push_front(stack.stackvar);
7020 ((!singlecontrolstate)?tempparameters:stack.parameters);
7025 parameters = variable_list({ stack
.stackvar });
7027 init=make_initialstate(initial_proc_id,stack,stochastic_normalized_process_identifiers,regular,singlecontrolstate,initial_stochastic_distribution);
7028 assert(init.size()==parameters.size());
7029 collectsumlist(action_summands,deadlock_summands,stochastic_normalized_process_identifiers,parameters,stack,regular,singlecontrolstate);
7031 if (!options.no_intermediate_cluster)
7033 cluster_actions(action_summands,deadlock_summands,parameters);
7036 if ((!containstime) || options.ignore_time)
7039
7040
7041
7042
7043
7044
7045
7046
7047 deadlock_summands.emplace_back(variable_list(), sort_bool::true_(), deadlock());
7074 throw mcrl2::runtime_error(
"variable conflict " + data::pp(var) +
":" + data::pp(var.sort()) +
" versus " +
7075 data::pp(var1) +
":" + data::pp(var1.sort()) +
".");
7079 vl.push_front(var1);
7086 const variable_list& pars1,
7087 const variable_list& pars2,
7088 variable_list& pars3,
7089 variable_list& pars4,
7090 const bool unique=
true)
7093
7094
7095
7096
7097
7098
7099
7100
7101
7102
7103
7104
7105
7106
7114 pars3=variable_list();
7115 pars4=variable_list();
7119 const variable& var2=pars2.front();
7123 var3=get_fresh_variable(var2.name(),var2.sort(),(unique?-1:
static_cast<
int>(i)));
7127 t1=construct_renaming(pars1,pars2.tail(),t,t2,unique);
7128 t1.push_front(var3);
7131 pars4.push_front(var2);
7133 pars3.push_front(var3);
7137 t1=construct_renaming(pars1,pars2.tail(),t,pars4,unique);
7139 pars3.push_front(var2);
7148 template <
typename List>
7151 return sort_expression_list(l.begin(), l.end(), [](
const typename List::value_type& d) -> sort_expression {
return d.sort();});
7156 const variable_list& sumvars,
7161
7162
7166 const variable& t = atermpp::down_cast<variable>(actiontime);
7183 const variable_list& sumvars,
7184 const variable_list& freevars,
7186 const bool has_time,
7189 variable_list& used_sumvars)
7192
7193
7194
7195
7196
7197
7198
7199
7200
7201
7202
7203
7204
7205
7206
7207
7208
7209
7210
7211
7212
7213
7214
7215
7216
7218 assert(used_sumvars.empty());
7220 variable_list variables;
7231 variables.push_front(timevariable);
7233 for (
const variable& v: freevars)
7235 if (occursinterm(result, v))
7237 variables.push_front(v);
7241 for (
const variable& v: global_variables)
7243 if (occursinterm(result, v))
7245 variables.push_front(v);
7249 for (
const variable& v: sumvars)
7251 if (occursinterm(result, v))
7253 used_sumvars.push_front(v);
7256 used_sumvars = reverse(used_sumvars);
7262 const stochastic_action_summand_vector& action_summands,
7263 const deadlock_summand_vector& deadlock_summands,
7264 const variable_list& freevars)
7267
7268
7269
7271 variable time_variable=get_fresh_variable(
"timevar",sort_real::real_());
7272 for (
const deadlock_summand& summand: deadlock_summands)
7274 if ((!summand.deadlock().has_time()) && (summand.condition()==sort_bool::true_()))
7276 return lps::detail::ultimate_delay(time_variable);
7280 for (
const stochastic_action_summand& summand: action_summands)
7282 if ((!summand.multi_action().has_time()) && (summand.condition()==sort_bool::true_()))
7284 return lps::detail::ultimate_delay(time_variable);
7289
7290
7292 data_expression_list results;
7293 data_expression_list condition_list;
7294 std::vector < variable_list> renamings_pars;
7295 std::vector < data_expression_list> renamings_args;
7296 variable_list existentially_quantified_variables;
7297 for (
const deadlock_summand& s: deadlock_summands)
7299 variable_list new_existentially_quantified_variables;
7300 const data_expression ult_del_condition=
7301 makesingleultimatedelaycondition(
7302 s.summation_variables(),
7305 s.deadlock().has_time(),
7307 s.deadlock().time(),
7308 new_existentially_quantified_variables);
7309 existentially_quantified_variables=merge_var(
7310 new_existentially_quantified_variables,
7311 existentially_quantified_variables,
7316 results.push_front(ult_del_condition);
7319 for (
const stochastic_action_summand& s: action_summands)
7321 variable_list new_existentially_quantified_variables;
7322 const data_expression ult_del_condition=
7323 makesingleultimatedelaycondition(
7324 s.summation_variables(),
7327 s.multi_action().has_time(),
7329 s.multi_action().time(),
7330 new_existentially_quantified_variables);
7331 existentially_quantified_variables=merge_var(
7332 new_existentially_quantified_variables,
7333 existentially_quantified_variables,
7338 results.push_front(ult_del_condition);
7343 assert(results.size()==condition_list.size());
7344 assert(results.size()==renamings_pars.size());
7345 assert(results.size()==renamings_args.size());
7347 std::vector < variable_list>::const_iterator renamings_par=renamings_pars.begin();
7348 std::vector < data_expression_list>::const_iterator renamings_arg=renamings_args.begin();
7349 condition_list=reverse(condition_list);
7350 results=reverse(results);
7351 data_expression_list::const_iterator j=condition_list.begin();
7352 for(data_expression_list::const_iterator i=results.begin();
7353 i!=results.end(); ++i,++j,++renamings_par,++renamings_arg)
7355 const variable_list& auxpars=*renamings_par;
7356 const data_expression_list& auxargs=*renamings_arg;
7358 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
7359 data_expression_list::const_iterator j1=auxargs.begin();
7360 for (variable_list::const_iterator i1=auxpars.begin();
7361 i1!=auxpars.end(); ++i1, ++j1)
7364 if (sigma(*i1)==*i1)
7371 maintain_variables_in_rhs< mutable_map_substitution<> > mutable_sigma(sigma);
7372 result=lazy::or_(result,replace_variables_capture_avoiding_alt(lazy::and_(*i,*j), mutable_sigma));
7374 return lps::detail::ultimate_delay(time_variable, existentially_quantified_variables, RewriteTerm(result));
7385
7387 data::maintain_variables_in_rhs< data::mutable_map_substitution<> > sigma;
7389 for(
const variable& var: var_list)
7391 const data::variable v =
7392 get_fresh_variable(std::string(var.name()) + ((hint.empty())?
"":
"_") + hint, var.sort());
7401 stochastic_action_summand_vector& action_summands,
7402 deadlock_summand_vector& deadlock_summands,
7403 variable_list& pars,
7405 const std::string& hint=
"")
7407 stochastic_action_summand_vector result_action_summands;
7409 data::maintain_variables_in_rhs<data::mutable_map_substitution<> > sigma=make_unique_variables(pars, hint);
7410 const variable_list unique_pars=data::replace_variables(pars, sigma);
7412 if (!options.ignore_time)
7415 maintain_variables_in_rhs< data::mutable_map_substitution<> > local_sigma=sigma;
7416 for(
const variable& v: ultimate_delay_condition.variables())
7420 ultimate_delay_condition.constraint()=replace_variables_capture_avoiding_alt(
7421 ultimate_delay_condition.constraint(),
7424 for (
const stochastic_action_summand& smmnd: action_summands)
7426 const variable_list& sumvars=smmnd.summation_variables();
7427 data::maintain_variables_in_rhs<data::mutable_map_substitution<> > sigma_sumvars=make_unique_variables(sumvars,hint);
7428 const variable_list unique_sumvars=data::replace_variables(sumvars, sigma_sumvars);
7430 stochastic_distribution distribution=smmnd.distribution();
7431 const variable_list stochastic_vars=distribution.variables();
7432 data::maintain_variables_in_rhs<data::mutable_map_substitution<> > sigma_stochastic_vars=
7433 make_unique_variables(stochastic_vars,hint);
7434 const variable_list unique_stochastic_vars=data::replace_variables(stochastic_vars, sigma_stochastic_vars);
7436 data_expression condition=smmnd.condition();
7437 action_list multiaction=smmnd.multi_action().actions();
7438 data_expression actiontime=smmnd.multi_action().time();
7439 assignment_list nextstate=smmnd.assignments();
7441 condition=replace_variables_capture_avoiding_alt(condition, sigma_sumvars);
7442 condition=replace_variables_capture_avoiding_alt(condition, sigma);
7444 actiontime=replace_variables_capture_avoiding_alt(actiontime, sigma_sumvars);
7445 actiontime=replace_variables_capture_avoiding_alt(actiontime, sigma);
7446 multiaction=lps::replace_variables_capture_avoiding_with_an_identifier_generator(multiaction, sigma_sumvars, fresh_identifier_generator);
7447 multiaction=lps::replace_variables_capture_avoiding_with_an_identifier_generator(multiaction, sigma, fresh_identifier_generator);
7449 distribution=stochastic_distribution(
7450 unique_stochastic_vars,
7451 replace_variables_capture_avoiding_alt(distribution.distribution(), sigma_sumvars));
7452 distribution=stochastic_distribution(
7453 unique_stochastic_vars,
7454 replace_variables_capture_avoiding_alt(distribution.distribution(), sigma_stochastic_vars));
7455 distribution=stochastic_distribution(
7456 distribution.variables(),
7457 replace_variables_capture_avoiding_alt(distribution.distribution(), sigma));
7459 nextstate=substitute_assignmentlist(nextstate,pars,
false,
true,sigma_sumvars);
7460 nextstate=substitute_assignmentlist(nextstate,pars,
false,
true,sigma_stochastic_vars);
7461 nextstate=substitute_assignmentlist(nextstate,pars,
true,
true,sigma);
7463 result_action_summands.emplace_back(unique_sumvars,
7465 smmnd.multi_action().has_time() ? multi_action(multiaction, actiontime) : multi_action(multiaction),
7470 action_summands.swap(result_action_summands);
7472 deadlock_summand_vector result_deadlock_summands;
7474 assert(unique_pars.size()==pars.size());
7476 for (
const deadlock_summand& smmnd: deadlock_summands)
7478 const variable_list& sumvars=smmnd.summation_variables();
7479 maintain_variables_in_rhs<data::mutable_map_substitution<> > sigma_sumvars=make_unique_variables(sumvars,hint);
7480 const variable_list unique_sumvars=data::replace_variables(sumvars, sigma_sumvars);
7482 assert(unique_sumvars.size()==sumvars.size());
7483 data_expression condition=smmnd.condition();
7484 data_expression actiontime=smmnd.deadlock().time();
7486 condition=replace_variables_capture_avoiding_alt(condition, sigma_sumvars);
7487 condition=replace_variables_capture_avoiding_alt(condition, sigma);
7489 actiontime=replace_variables_capture_avoiding_alt(actiontime, sigma_sumvars);
7490 actiontime=replace_variables_capture_avoiding_alt(actiontime, sigma);
7492 result_deadlock_summands.emplace_back(unique_sumvars,
7494 smmnd.deadlock().has_time() ? deadlock(actiontime) : deadlock());
7497 result_deadlock_summands.swap(deadlock_summands);
7515 variable_list renameable_variables=delay2.variables();
7516 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
7517 alphaconvert(renameable_variables, sigma, delay1.variables(), data_expression_list());
7519 sigma[delay2.time_var()]=delay1.time_var();
7521 make_optimized_and(new_constraint, delay1.constraint(), replace_variables_capture_avoiding_alt(delay2.constraint(),sigma));
7522 variable_list new_existential_variables = delay1.variables()+renameable_variables;
7525 return lps::detail::ultimate_delay(
7527 new_existential_variables,
7533 const stochastic_action_summand_vector& action_summands1,
7534 const action_name_multiset_list& allowlist,
7535 const bool is_allow,
7536 const bool is_block,
7537 stochastic_action_summand_vector& action_summands)
7539 lps::detail::allow_list_cache allow_cache;
7542 allow_cache = lps::detail::make_allow_list_cache(allowlist);
7544 for (
const stochastic_action_summand& summand1: action_summands1)
7546 variable_list sumvars=ultimate_delay_condition.variables();
7547 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
7548 alphaconvert(sumvars,sigma,summand1.summation_variables(),data_expression_list());
7550 variable_list sumvars1 = summand1.summation_variables() + sumvars;
7551 const action_list& multiaction1 = summand1.multi_action().actions();
7552 assert(std::is_sorted(multiaction1.begin(), multiaction1.end()));
7553 data_expression actiontime1 = summand1.multi_action().time();
7554 data_expression condition1 = summand1.condition();
7555 const assignment_list& nextstate1 = summand1.assignments();
7556 const stochastic_distribution& distribution1=summand1.distribution();
7557 bool has_time = summand1.has_time();
7559 if (multiaction1 != action_list({ terminationAction }))
7561 if (is_allow && !allow_(allow_cache,multiaction1,terminationAction))
7565 if (is_block && encap(allowlist,multiaction1))
7570 if (!options.ignore_time)
7574 if (ultimate_delay_condition.constraint()!=sort_bool::true_())
7576 actiontime1=ultimate_delay_condition.time_var();
7577 sumvars1.push_front(ultimate_delay_condition.time_var());
7578 condition1=lazy::and_(condition1,
7579 replace_variables_capture_avoiding_alt(ultimate_delay_condition.constraint(), sigma));
7586
7587 const std::set<variable> variables_in_actiontime1=find_free_variables(actiontime1);
7588 sigma[ultimate_delay_condition.time_var()]=actiontime1;
7589 const data_expression intermediateultimatedelaycondition=
7590 replace_variables_capture_avoiding_alt(ultimate_delay_condition.constraint(),sigma);
7591 make_optimized_and(condition1, condition1, intermediateultimatedelaycondition);
7594 condition1=RewriteTerm(condition1);
7597 if (condition1!=sort_bool::false_())
7599 action_summands.emplace_back(sumvars1,
7601 has_time ? multi_action(multiaction1, actiontime1) : multi_action(multiaction1),
7611 const deadlock_summand_vector& deadlock_summands1,
7612 const bool is_allow,
7613 const bool is_block,
7614 const stochastic_action_summand_vector& action_summands,
7615 deadlock_summand_vector& deadlock_summands)
7617 bool inline_allow = is_allow || is_block;
7621 for (
const deadlock_summand& summand1: deadlock_summands1)
7623 variable_list sumvars=ultimate_delay_condition.variables();
7624 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
7625 alphaconvert(sumvars,sigma,summand1.summation_variables(),data_expression_list());
7627 variable_list sumvars1=summand1.summation_variables() + sumvars;
7628 data_expression actiontime1=summand1.deadlock().time();
7629 data_expression condition1=summand1.condition();
7630 bool has_time=summand1.deadlock().has_time();
7632 if (!options.ignore_time)
7636 if (ultimate_delay_condition.constraint()!=sort_bool::true_())
7638 actiontime1=ultimate_delay_condition.time_var();
7639 sumvars1.push_front(ultimate_delay_condition.time_var());
7640 make_optimized_and(condition1, condition1,
7641 replace_variables_capture_avoiding_alt(ultimate_delay_condition.constraint(),
7649
7650 const std::set<variable> variables_in_actiontime1=find_free_variables(actiontime1);
7651 sigma[ultimate_delay_condition.time_var()]=actiontime1;
7652 const data_expression intermediateultimatedelaycondition=
7653 replace_variables_capture_avoiding_alt(ultimate_delay_condition.constraint(),sigma);
7654 make_optimized_and(condition1, condition1, intermediateultimatedelaycondition);
7657 condition1=RewriteTerm(condition1);
7660 if (condition1!=sort_bool::false_() && !options.ignore_time)
7662 insert_timed_delta_summand(action_summands,
7664 deadlock_summand(sumvars1,condition1, has_time?deadlock(actiontime1):deadlock()),
7665 options.ignore_time);
7671#ifdef MCRL2_LOG_LPS_LINEARISE_STATISTICS
7710 const stochastic_action_summand_vector& action_summands1,
7711 const deadlock_summand_vector& deadlock_summands1,
7713 const action_name_multiset_list& allowlist,
7714 const bool is_allow,
7715 const bool is_block,
7716 stochastic_action_summand_vector& action_summands,
7717 deadlock_summand_vector& deadlock_summands)
7719#ifdef MCRL2_LOG_LPS_LINEARISE_STATISTICS
7720 lps_statistics_t lps_statistics_before = get_statistics(action_summands1, deadlock_summands1);
7721 lps_statistics_t lps_statistics_result_before = get_statistics(action_summands, deadlock_summands);
7724 calculate_left_merge_deadlock(ultimate_delay_condition2, deadlock_summands1,
7725 is_allow, is_block, action_summands, deadlock_summands);
7726 calculate_left_merge_action(ultimate_delay_condition2, action_summands1,
7727 allowlist, is_allow, is_block, action_summands);
7729#ifdef MCRL2_LOG_LPS_LINEARISE_STATISTICS
7730 lps_statistics_t lps_statistics_result_after = get_statistics(action_summands, deadlock_summands);
7732 std::cout << log_leftmerge_application(lps_statistics_before,
7733 lps_statistics_result_before,
7734 lps_statistics_result_after,
7737 (is_block ? allowlist.front().size() : allowlist.size()), 4);
7743 const stochastic_action_summand_vector& action_summands1,
7744 const stochastic_action_summand_vector& action_summands2,
7745 const action_name_multiset_list& allowlist,
7746 const bool is_allow,
7747 const bool is_block,
7748 stochastic_action_summand_vector& action_summands)
7750 lps::detail::allow_list_cache allow_cache;
7753 allow_cache = lps::detail::make_allow_list_cache(allowlist);
7757 for (
const stochastic_action_summand& summand1: action_summands1)
7759 const variable_list& sumvars1=summand1.summation_variables();
7760 const action_list multiaction1=summand1.multi_action().actions();
7761 const data_expression& actiontime1=summand1.multi_action().time();
7762 const data_expression& condition1=summand1.condition();
7763 const assignment_list& nextstate1=summand1.assignments();
7764 const stochastic_distribution& distribution1=summand1.distribution();
7766 for (
const stochastic_action_summand& summand2: action_summands2)
7768 const variable_list& sumvars2=summand2.summation_variables();
7769 const action_list multiaction2=summand2.multi_action().actions();
7770 const data_expression& actiontime2=summand2.multi_action().time();
7771 const data_expression& condition2=summand2.condition();
7772 const assignment_list& nextstate2=summand2.assignments();
7773 const stochastic_distribution& distribution2=summand2.distribution();
7775 if ((multiaction1 == action_list({ terminationAction })) == (multiaction2 == action_list({ terminationAction })))
7777 action_list multiaction3;
7778 if ((multiaction1 == action_list({ terminationAction })) && (multiaction2 == action_list({ terminationAction })))
7780 multiaction3.push_front(terminationAction);
7784 multiaction3=linMergeMultiActionList(multiaction1,multiaction2);
7787 if (is_allow && !allow_(allow_cache,multiaction3,terminationAction))
7791 if (is_block && encap(allowlist,multiaction3))
7796 const variable_list allsums=sumvars1+sumvars2;
7797 data_expression condition3= lazy::and_(condition1,condition2);
7798 data_expression action_time3;
7799 bool has_time3=summand1.has_time()||summand2.has_time();
7801 if (!summand1.has_time())
7803 if (summand2.has_time())
7806 action_time3=actiontime2;
7812 if (!summand2.has_time())
7814 action_time3=actiontime1;
7819 action_time3=actiontime1;
7820 condition3=lazy::and_(
7822 equal_to(actiontime1,actiontime2));
7826 const assignment_list nextstate3=nextstate1+nextstate2;
7827 const stochastic_distribution distribution3(
7828 distribution1.variables()+distribution2.variables(),
7829 real_times_optimized(distribution1.distribution(),distribution2.distribution()));
7831 condition3=RewriteTerm(condition3);
7832 if (condition3!=sort_bool::false_())
7834 assert(std::is_sorted(multiaction3.begin(), multiaction3.end()));
7835 action_summands.emplace_back(allsums,
7837 has_time3 ? multi_action(multiaction3, action_time3) : multi_action(multiaction3),
7847 const stochastic_action_summand_vector& action_summands1,
7848 const deadlock_summand_vector& deadlock_summands1,
7849 const stochastic_action_summand_vector& action_summands,
7850 deadlock_summand_vector& deadlock_summands)
7852 for (
const stochastic_action_summand& summand1: action_summands1)
7854 const variable_list& sumvars1=summand1.summation_variables();
7855 const data_expression& actiontime1=summand1.multi_action().time();
7856 const data_expression& condition1=summand1.condition();
7858 for (
const deadlock_summand& summand2: deadlock_summands1)
7860 const variable_list& sumvars2=summand2.summation_variables();
7861 const data_expression& actiontime2=summand2.deadlock().time();
7862 const data_expression& condition2=summand2.condition();
7864 const variable_list allsums=sumvars1+sumvars2;
7865 const data_expression condition3= lazy::and_(condition1,condition2);
7866 data_expression action_time3;
7867 bool has_time3=summand1.has_time()||summand2.has_time();
7869 if (!summand1.has_time())
7871 if (summand2.has_time())
7874 action_time3=actiontime2;
7880 if (!summand2.has_time())
7882 action_time3=actiontime1;
7887 action_time3=RewriteTerm(sort_real::minimum(actiontime1,actiontime2));
7891 if (condition3!=sort_bool::false_() && !options.ignore_time)
7893 insert_timed_delta_summand(action_summands,
7895 deadlock_summand(allsums,
7897 has_time3?deadlock(action_time3):deadlock()),
7898 options.ignore_time);
7906 const deadlock_summand_vector& deadlock_summands1,
7907 const deadlock_summand_vector& deadlock_summands2,
7908 const stochastic_action_summand_vector& action_summands,
7909 deadlock_summand_vector& deadlock_summands)
7911 for (
const deadlock_summand& summand1: deadlock_summands1)
7913 const variable_list& sumvars1=summand1.summation_variables();
7914 const data_expression& actiontime1=summand1.deadlock().time();
7915 const data_expression& condition1=summand1.condition();
7917 for (
const deadlock_summand& summand2: deadlock_summands2)
7919 const variable_list& sumvars2=summand2.summation_variables();
7920 const data_expression& actiontime2=summand2.deadlock().time();
7921 const data_expression& condition2=summand2.condition();
7923 const variable_list allsums=sumvars1+sumvars2;
7924 const data_expression condition3= lazy::and_(condition1,condition2);
7925 data_expression action_time3;
7926 bool has_time3=summand1.has_time()||summand2.has_time();
7928 if (!summand1.has_time())
7930 if (summand2.has_time())
7933 action_time3=actiontime2;
7939 if (!summand2.has_time())
7941 action_time3=actiontime1;
7946 action_time3=RewriteTerm(sort_real::minimum(actiontime1,actiontime2));
7950 if (condition3!=sort_bool::false_() && !options.ignore_time)
7952 insert_timed_delta_summand(action_summands,
7954 deadlock_summand(allsums,
7956 has_time3?deadlock(action_time3):deadlock()),
7957 options.ignore_time);
7964#ifdef MCRL2_LOG_LPS_LINEARISE_STATISTICS
8002 const stochastic_action_summand_vector& action_summands1,
8003 const deadlock_summand_vector& deadlock_summands1,
8004 const stochastic_action_summand_vector& action_summands2,
8005 const deadlock_summand_vector& deadlock_summands2,
8006 const action_name_multiset_list& allowlist,
8007 const bool is_allow,
8008 const bool is_block,
8009 stochastic_action_summand_vector& action_summands,
8010 deadlock_summand_vector& deadlock_summands)
8012#ifdef MCRL2_LOG_LPS_LINEARISE_STATISTICS
8013 lps_statistics_t lps1_statistics_before = get_statistics(action_summands1, deadlock_summands1);
8014 lps_statistics_t lps2_statistics_before = get_statistics(action_summands2, deadlock_summands2);
8015 lps_statistics_t lps_result_statistics_before = get_statistics(action_summands, deadlock_summands);
8018 calculate_communication_merge_action_summands(action_summands1, action_summands2, allowlist, is_allow, is_block, action_summands);
8019 calculate_communication_merge_action_deadlock_summands(action_summands1, deadlock_summands2, action_summands, deadlock_summands);
8020 calculate_communication_merge_action_deadlock_summands(action_summands2, deadlock_summands1, action_summands, deadlock_summands);
8021 calculate_communication_merge_deadlock_summands(deadlock_summands1, deadlock_summands2, action_summands, deadlock_summands);
8023#ifdef MCRL2_LOG_LPS_LINEARISE_STATISTICS
8024 lps_statistics_t lps_statistics_after = get_statistics(action_summands, deadlock_summands);
8026 std::cout << log_communicationmerge_application(lps1_statistics_before, lps2_statistics_before, lps_result_statistics_before,
8027 lps_statistics_after, is_allow, is_block, (is_block ? allowlist.front().size() : allowlist.size()), 4);
8033 const stochastic_action_summand_vector& action_summands1,
8034 const deadlock_summand_vector& deadlock_summands1,
8036 const stochastic_action_summand_vector& action_summands2,
8037 const deadlock_summand_vector& deadlock_summands2,
8039 const variable_list& par1,
8040 const variable_list& par3,
8041 const action_name_multiset_list& allowlist1,
8042 const bool is_allow,
8043 const bool is_block,
8044 stochastic_action_summand_vector& action_summands,
8045 deadlock_summand_vector& deadlock_summands)
8047 assert(action_summands.size()==0);
8048 assert(deadlock_summands.size()==0);
8050 variable_list allpars = par1 + par3;
8052 if (is_allow || is_block)
8056 assert(!options.nodeltaelimination && options.ignore_time);
8057 deadlock_summands.emplace_back(variable_list(), sort_bool::true_(), deadlock());
8062 action_name_multiset_list allowlist(allowlist1);
8063 calculate_left_merge(action_summands1, deadlock_summands1,
8064 ultimate_delay_condition2, allowlist, is_allow, is_block,
8065 action_summands, deadlock_summands);
8068 calculate_left_merge(action_summands2, deadlock_summands2,
8069 ultimate_delay_condition1, allowlist, is_allow, is_block,
8070 action_summands, deadlock_summands);
8074 calculate_communication_merge(action_summands1, deadlock_summands1, action_summands2, deadlock_summands2,
8075 allowlist, is_allow, is_block, action_summands, deadlock_summands);
8079#ifdef MCRL2_LOG_LPS_LINEARISE_STATISTICS
8131 const stochastic_action_summand_vector& action_summands1,
8132 const deadlock_summand_vector& deadlock_summands1,
8133 const variable_list& pars1,
8134 const data_expression_list& init1,
8137 const stochastic_action_summand_vector& action_summands2,
8138 const deadlock_summand_vector& deadlock_summands2,
8139 const variable_list& pars2,
8140 const data_expression_list& init2,
8143 const action_name_multiset_list& allowlist1,
8144 const bool is_allow,
8145 const bool is_block,
8146 stochastic_action_summand_vector& action_summands,
8147 deadlock_summand_vector& deadlock_summands,
8148 variable_list& pars_result,
8149 data_expression_list& init_result,
8153 mCRL2log(mcrl2::log::log_level_t::verbose) <<
8154 (is_allow ?
"- calculating the parallel composition modulo the allow operator: " :
8155 is_block ?
"- calculating the parallel composition modulo the block operator: " :
8156 "- calculating the parallel composition: ") <<
8157 action_summands1.size() <<
8158 " action summands + " << deadlock_summands1.size() <<
8159 " deadlock summands || " << action_summands2.size() <<
8160 " action summands + " << deadlock_summands2.size() <<
" deadlock summands = ";
8165#ifdef MCRL2_LOG_LPS_LINEARISE_STATISTICS
8166 lps_statistics_t lps1_statistics_before = get_statistics(action_summands1, deadlock_summands1);
8167 lps_statistics_t lps2_statistics_before = get_statistics(action_summands2, deadlock_summands2);
8169 std::cout << log_parallelcomposition_application_start(lps1_statistics_before, lps2_statistics_before, is_allow, is_block, (is_block?allowlist1.front().size():allowlist1.size()));
8172 variable_list pars3;
8173 for (
const variable& v: pars2)
8175 if (std::find(pars1.begin(),pars1.end(),v)==pars1.end())
8178 pars3.push_front(v);
8182 pars3=reverse(pars3);
8183 assert(action_summands.size()==0);
8184 assert(deadlock_summands.size()==0);
8185 combine_summand_lists(action_summands1,deadlock_summands1,ultimate_delay_condition1,
8186 action_summands2,deadlock_summands2,ultimate_delay_condition2,
8187 pars1,pars3,allowlist1,is_allow,is_block,action_summands,deadlock_summands);
8189 mCRL2log(mcrl2::log::log_level_t::verbose) << action_summands.size() <<
" actions and " << deadlock_summands.size() <<
" delta summands.\n";
8190 pars_result=pars1+pars3;
8191 init_result=init1 + init2;
8196 if (!options.ignore_time)
8201#ifdef MCRL2_LOG_LPS_LINEARISE_STATISTICS
8202 lps_statistics_t lps_statistics_after = get_statistics(action_summands, deadlock_summands);
8204 std::cout << log_parallelcomposition_application_end(lps_statistics_after);
8216 stochastic_action_summand_vector& action_summands,
8217 deadlock_summand_vector& deadlock_summands,
8220 const bool rename_variables,
8221 variable_list& pars,
8222 data_expression_list& init,
8228 generateLPEmCRL(action_summands,deadlock_summands,process_instance_assignment(t).identifier(),
8229 regular,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8234 maintain_variables_in_rhs<mutable_map_substitution<> > sigma;
8235 for (
const assignment& a: process_instance_assignment(t).assignments())
8237 sigma[a.lhs()]=a.rhs();
8240 init=replace_variables_capture_avoiding_alt(init,sigma);
8241 initial_stochastic_distribution =
8242 stochastic_distribution(
8243 initial_stochastic_distribution.variables(),
8244 replace_variables_capture_avoiding_alt(initial_stochastic_distribution.distribution(), sigma));
8252 make_parameters_and_sum_variables_unique(action_summands,deadlock_summands,pars,ultimate_delay_condition,std::string(object.objectname));
8256 if (rename_variables)
8258 make_parameters_and_sum_variables_unique(action_summands,deadlock_summands,pars,ultimate_delay_condition);
8262 if (regular && !options.do_not_apply_constelm)
8278 data::mutable_map_substitution<> sigma = alg.compute_constant_parameters(
true);
8279 alg.remove_parameters(sigma);
8280 alg.remove_trivial_summands();
8282 if (!options.ignore_time)
8284 ultimate_delay_condition.constraint()=data::replace_variables_capture_avoiding(ultimate_delay_condition.constraint(),sigma);
8288 init=temporary_spec.initial_process().expressions();
8289 pars=temporary_spec.process().process_parameters();
8290 assert(init.size()==pars.size());
8295 std::set <variable> variable_list = lps::find_free_variables(temporary_spec.process().action_summands());
8296 const std::set <variable> variable_list1 = lps::find_free_variables(temporary_spec.process().deadlock_summands());
8297 variable_list.insert(variable_list1.begin(),variable_list1.end());
8298 for (
const variable& v: variable_list)
8300 if (std::find(pars.begin(),pars.end(),v)==pars.end() &&
8301 global_variables.find(v)==global_variables.end()
8309 action_summands=temporary_spec.process().action_summands();
8310 deadlock_summands=temporary_spec.process().deadlock_summands();
8318 variable_list pars1;
8319 variable_list pars2;
8320 data_expression_list init1;
8321 data_expression_list init2;
8324 stochastic_action_summand_vector action_summands1;
8325 stochastic_action_summand_vector action_summands2;
8326 deadlock_summand_vector deadlock_summands1;
8327 deadlock_summand_vector deadlock_summands2;
8330 generateLPEmCRLterm(action_summands1,deadlock_summands1,process::merge(t).left(),
8331 regular,rename_variables,pars1,init1,initial_stochastic_distribution1,ultimate_delay_condition1);
8332 generateLPEmCRLterm(action_summands2,deadlock_summands2,process::merge(t).right(),
8333 regular,
true,pars2,init2,initial_stochastic_distribution2,ultimate_delay_condition2);
8334 parallelcomposition(action_summands1,deadlock_summands1,pars1,init1,initial_stochastic_distribution1,ultimate_delay_condition1,
8335 action_summands2,deadlock_summands2,pars2,init2,initial_stochastic_distribution2,ultimate_delay_condition2,
8336 action_name_multiset_list(),
false,
false,
8337 action_summands,deadlock_summands,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8343 generateLPEmCRLterm(action_summands,deadlock_summands,hide(t).operand(),
8344 regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8345 hidecomposition(hide(t).hide_set(),action_summands);
8352 if (!options.nodeltaelimination && options.ignore_time && is_merge(par))
8355 variable_list pars1;
8356 variable_list pars2;
8357 data_expression_list init1;
8358 data_expression_list init2;
8361 stochastic_action_summand_vector action_summands1;
8362 stochastic_action_summand_vector action_summands2;
8363 deadlock_summand_vector deadlock_summands1;
8364 deadlock_summand_vector deadlock_summands2;
8367 generateLPEmCRLterm(action_summands1,deadlock_summands1,process::merge(par).left(),
8368 regular,rename_variables,pars1,init1,initial_stochastic_distribution1,ultimate_delay_condition1);
8369 generateLPEmCRLterm(action_summands2,deadlock_summands2,process::merge(par).right(),
8370 regular,
true,pars2,init2,initial_stochastic_distribution2,ultimate_delay_condition2);
8371 parallelcomposition(action_summands1,deadlock_summands1,pars1,init1,initial_stochastic_distribution1,ultimate_delay_condition1,
8372 action_summands2,deadlock_summands2,pars2,init2,initial_stochastic_distribution2,ultimate_delay_condition2,
8373 allow(t).allow_set(),
true,
false,
8374 action_summands,deadlock_summands,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8377 else if (!options.nodeltaelimination && options.ignore_time && is_comm(par))
8379 generateLPEmCRLterm(action_summands,deadlock_summands,comm(par).operand(),
8380 regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8381 communicationcomposition(comm(par).comm_set(),allow(t).allow_set(),
true,
false,action_summands,deadlock_summands,terminationAction,options.nosumelm,options.nodeltaelimination,options.ignore_time,[
this](
const data::data_expression& e) {
return RewriteTerm(e); });
8385 generateLPEmCRLterm(action_summands,deadlock_summands,par,regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8386 allowblockcomposition(allow(t).allow_set(),
true,action_summands,deadlock_summands,terminationAction,options.ignore_time,options.nodeltaelimination);
8393 if (!options.nodeltaelimination && options.ignore_time && is_merge(par))
8396 variable_list pars1;
8397 variable_list pars2;
8398 data_expression_list init1;
8399 data_expression_list init2;
8402 stochastic_action_summand_vector action_summands1;
8403 stochastic_action_summand_vector action_summands2;
8404 deadlock_summand_vector deadlock_summands1;
8405 deadlock_summand_vector deadlock_summands2;
8408 generateLPEmCRLterm(action_summands1,deadlock_summands1,process::merge(par).left(),
8409 regular,rename_variables,pars1,init1,initial_stochastic_distribution1,ultimate_delay_condition1);
8410 generateLPEmCRLterm(action_summands2,deadlock_summands2,process::merge(par).right(),
8411 regular,
true,pars2,init2,initial_stochastic_distribution2,ultimate_delay_condition2);
8413 parallelcomposition(action_summands1,deadlock_summands1,pars1,init1,initial_stochastic_distribution1,ultimate_delay_condition1,
8414 action_summands2,deadlock_summands2,pars2,init2,initial_stochastic_distribution2,ultimate_delay_condition2,
8415 action_name_multiset_list({action_name_multiset(block(t).block_set())}),
false,
true,
8416 action_summands,deadlock_summands,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8419 else if (!options.nodeltaelimination && options.ignore_time && is_comm(par))
8421 generateLPEmCRLterm(action_summands,deadlock_summands,comm(par).operand(),
8422 regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8424 communicationcomposition(comm(par).comm_set(),action_name_multiset_list( { action_name_multiset(block(t).block_set())} ),
8425 false,
true,action_summands,deadlock_summands,terminationAction,options.nosumelm,options.nodeltaelimination,options.ignore_time,[
this](
const data::data_expression& e) {
return RewriteTerm(e); });
8429 generateLPEmCRLterm(action_summands,deadlock_summands,par,regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8431 allowblockcomposition(action_name_multiset_list({action_name_multiset(block(t).block_set())}),
false,action_summands,deadlock_summands,terminationAction,options.ignore_time,options.nodeltaelimination);
8437 generateLPEmCRLterm(action_summands,deadlock_summands,process::rename(t).operand(),
8438 regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8439 lps::rename(process::rename(t).rename_set(),action_summands);
8445 generateLPEmCRLterm(action_summands,deadlock_summands,comm(t).operand(),
8446 regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8447 communicationcomposition(comm(t).comm_set(),action_name_multiset_list(),
false,
false,action_summands,deadlock_summands,terminationAction,options.nosumelm,options.nodeltaelimination,options.ignore_time,[
this](
const data::data_expression& e) {
return RewriteTerm(e); });
8454 generateLPEmCRLterm(action_summands,deadlock_summands,sto.operand(),
8455 regular,rename_variables,pars,init,initial_stochastic_distribution,ultimate_delay_condition);
8456 variable_list stochvars=sto.variables();
8457 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
8458 alphaconvert(stochvars,sigma,pars + initial_stochastic_distribution.variables(), data_expression_list());
8459 initial_stochastic_distribution=stochastic_distribution(
8460 stochvars+initial_stochastic_distribution.variables(),
8461 sort_real::times(replace_variables_capture_avoiding_alt(
8462 sto.distribution(), sigma),
8463 initial_stochastic_distribution.distribution()));
8465 for(
const variable& v: initial_stochastic_distribution.variables())
8469 init=replace_variables_capture_avoiding_alt(init,sigma);
8473 throw mcrl2::runtime_error(
"Internal error. Expect an mCRL term " + process::pp(t) +
".");
8479
8480
8481
8482
8483
8486 stochastic_action_summand_vector& action_summands,
8487 deadlock_summand_vector& deadlock_summands,
8490 variable_list& pars,
8491 data_expression_list& init,
8496
8505 generateLPEpCRL(action_summands,deadlock_summands,procIdDecl,
8506 object.containstime,regular,pars,init,initial_stochastic_distribution);
8507 if (options.ignore_time)
8513 ultimate_delay_condition=getUltimateDelayCondition(action_summands,deadlock_summands,pars);
8519 variable_list reduced_sumvars;
8521 fourier_motzkin(ultimate_delay_condition.constraint(),
8522 ultimate_delay_condition.variables(),
8523 simplified_ultimate_delay_condition,
8527 std::swap(ultimate_delay_condition.variables(), reduced_sumvars);
8529 catch (mcrl2::runtime_error& e)
8532 mCRL2log(mcrl2::log::log_level_t::debug) <<
"Simplifying a condition using Fourier-Motzkin reduction failed (I). \n" << e.what() << std::endl;
8536 assert(init.size() == pars.size());
8545 generateLPEmCRLterm(action_summands, deadlock_summands, object.processbody,
8546 regular,
false, pars, init, initial_stochastic_distribution, ultimate_delay_condition);
8547 assert(init.size() == pars.size());
8551 throw mcrl2::runtime_error(
"laststatus: " + std::to_string(object.processstatus));
8558 const variable_list& parameters,
8559 maintain_variables_in_rhs<mutable_map_substitution<> > sigma)
8564 alphaconversionterm(choice(t).left(),parameters,sigma),
8565 alphaconversionterm(choice(t).right(),parameters,sigma));
8571 alphaconversionterm(seq(t).left(),parameters,sigma),
8572 alphaconversionterm(seq(t).right(),parameters,sigma));
8577 return process::sync(
8578 alphaconversionterm(process::sync(t).left(),parameters,sigma),
8579 alphaconversionterm(process::sync(t).right(),parameters,sigma));
8584 return bounded_init(
8585 alphaconversionterm(bounded_init(t).left(),parameters,sigma),
8586 alphaconversionterm(bounded_init(t).right(),parameters,sigma));
8591 return process::merge(
8592 alphaconversionterm(process::merge(t).left(),parameters,sigma),
8593 alphaconversionterm(process::merge(t).right(),parameters,sigma));
8599 alphaconversionterm(left_merge(t).left(),parameters,sigma),
8600 alphaconversionterm(left_merge(t).right(),parameters,sigma));
8605 return at(alphaconversionterm(at(t).operand(),parameters,sigma),
8606 replace_variables_capture_avoiding_alt(at(t).time_stamp(),sigma));
8612 replace_variables_capture_avoiding_alt(if_then(t).condition(), sigma),
8613 alphaconversionterm(if_then(t).then_case(),parameters,sigma));
8618 variable_list sumvars=sum(t).variables();
8619 maintain_variables_in_rhs<mutable_map_substitution<> > local_sigma=sigma;
8621 alphaconvert(sumvars,local_sigma,variable_list(),variable_list_to_data_expression_list(parameters));
8622 return sum(sumvars,alphaconversionterm(sum(t).operand(), sumvars+parameters, local_sigma));
8628 variable_list sumvars=sto.variables();
8629 maintain_variables_in_rhs<mutable_map_substitution<> > local_sigma=sigma;
8631 alphaconvert(sumvars,local_sigma,variable_list(),variable_list_to_data_expression_list(parameters));
8632 return stochastic_operator(
8634 replace_variables_capture_avoiding_alt(sto.distribution(), sigma),
8635 alphaconversionterm(sto.operand(), sumvars+parameters, local_sigma));
8643 const variable_list instance_parameters=object.parameters;
8644 alphaconversion(procId,instance_parameters);
8647 substitute_assignmentlist(process_instance_assignment(t).assignments(),
8648 instance_parameters,
false,
true,sigma));
8655 return action(action(t).label(), replace_variables_capture_avoiding_alt(action(t).arguments(), sigma));
8666 return alphaconversionterm(hide(t).operand(),parameters,sigma);
8671 return alphaconversionterm(process::rename(t).operand(),parameters,sigma);
8676 return alphaconversionterm(comm(t).operand(),parameters,sigma);
8681 return alphaconversionterm(allow(t).operand(),parameters,sigma);
8686 return alphaconversionterm(block(t).operand(),parameters,sigma);
8689 throw mcrl2::runtime_error(
"unexpected process format in alphaconversionterm " + process::pp(t) +
".");
8703 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
8704 const process_expression tempvar=alphaconversionterm(object.processbody,parameters,sigma);
8709 maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
8710 alphaconversionterm(object.processbody,parameters,sigma);
8719 throw mcrl2::runtime_error(
"unknown type " + std::to_string(object.processstatus) +
8720 " in alphaconversion of " + process::pp(procId) +
".");
8730 std::set < process_identifier >& visited,
8731 bool allowrecursion,
8732 bool& contains_if_then)
8737
8738 bool r1=containstimebody(process::merge(t).left(),stable,visited,allowrecursion,contains_if_then);
8739 bool r2=containstimebody(process::merge(t).right(),stable,visited,allowrecursion,contains_if_then);
8747 return (containstime_rec(process_instance_assignment(t).identifier(),stable,visited,contains_if_then));
8754 return containstimebody(hide(t).operand(),stable,visited,allowrecursion,contains_if_then);
8759 return containstimebody(process::rename(t).operand(),stable,visited,allowrecursion,contains_if_then);
8764 return containstimebody(allow(t).operand(),stable,visited,allowrecursion,contains_if_then);
8769 return containstimebody(block(t).operand(),stable,visited,allowrecursion,contains_if_then);
8774 return containstimebody(comm(t).operand(),stable,visited,allowrecursion,contains_if_then);
8779 bool r1=containstimebody(choice(t).left(),stable,visited,allowrecursion,contains_if_then);
8780 bool r2=containstimebody(choice(t).right(),stable,visited,allowrecursion,contains_if_then);
8786 bool r1=containstimebody(seq(t).left(),stable,visited,allowrecursion,contains_if_then);
8787 bool r2=containstimebody(seq(t).right(),stable,visited,allowrecursion,contains_if_then);
8796 contains_if_then=
true;
8797 if (options.ignore_time)
8799 return containstimebody(if_then(t).then_case(),stable,visited,allowrecursion,contains_if_then);
8809 bool r1=containstimebody(if_then_else(t).then_case(),stable,visited,allowrecursion,contains_if_then);
8810 bool r2=containstimebody(if_then_else(t).else_case(),stable,visited,allowrecursion,contains_if_then);
8816 return containstimebody(sum(t).operand(),stable,visited,allowrecursion,contains_if_then);
8821 return containstimebody(stochastic_operator(t).operand(),stable,visited,allowrecursion,contains_if_then);
8838 bool r1=containstimebody(process::sync(t).left(),stable,visited,allowrecursion,contains_if_then);
8839 bool r2=containstimebody(process::sync(t).right(),stable,visited,allowrecursion,contains_if_then);
8843 throw mcrl2::runtime_error(
"unexpected process format in containstime " + process::pp(t) +
".");
8850 std::set < process_identifier >& visited,
8851 bool& contains_if_then)
8855 if (visited.count(procId)==0)
8857 visited.insert(procId);
8858 const bool ct=containstimebody(object.processbody,stable,visited,
true,contains_if_then);
8859 static bool show_only_once=
true;
8860 if (ct && options.ignore_time && show_only_once)
8862 mCRL2log(mcrl2::log::log_level_t::warning) <<
"process " << procId.name() <<
8863 " contains time, which is now not preserved. \n" <<
8864 "Use --timed or -T, or untick `add deadlocks' for a correct timed linearisation...\n";
8865 show_only_once=
false;
8870 if (stable!=
nullptr)
8881 std::set < process_identifier > visited;
8883 bool contains_if_then;
8884 return containstimebody(t,&stable,visited,
false,contains_if_then);
8891
8892
8893
8894
8896 bool contains_if_then=
false;
8900 std::set < process_identifier > visited;
8902 containstime_rec(procId,&stable,visited,contains_if_then);
8904 return contains_if_then;
8910 const std::map < process_identifier, process_pid_pair >& processes_with_initial_distribution)
8915 const process_expression new_process=processes_with_initial_distribution.at(u.identifier()).process_body();
8919 const process_identifier& new_identifier=processes_with_initial_distribution.at(u.identifier()).process_id();
8921 const variable_list new_parameters=object.parameters;
8923 assignment_list new_assignments;
8925 const variable_list relevant_stochastic_variables=parameters_that_occur_in_body(sto.variables(),object.processbody);
8926 assert(relevant_stochastic_variables.size()<=new_parameters.size());
8928 variable_list renamed_sto_variables=sto.variables();
8929 mutable_indexed_substitution<> local_sigma1;
8930 alphaconvertprocess(renamed_sto_variables, local_sigma1, t);
8933 variable_list::const_iterator i=new_parameters.begin();
8934 for(
const variable& v: relevant_stochastic_variables)
8936 new_assignments=push_back(new_assignments,assignment(*i,local_sigma1(v)));
8939 data_expression new_distribution = data::replace_variables_capture_avoiding(sto.distribution(),local_sigma1);
8943 new_assignments=filter_assignments(new_assignments + u.assignments(),object.parameters);
8949 mutable_indexed_substitution<> local_sigma;
8950 for(
const assignment& a:u.assignments())
8952 local_sigma[a.lhs()]=a.rhs();
8954 return stochastic_operator(renamed_sto_variables,
8955 data::replace_variables_capture_avoiding(new_distribution, local_sigma),
8956 process_instance_assignment(new_identifier,new_assignments));
8964 const process_expression r1_=transform_initial_distribution_term(choice(t).left(),processes_with_initial_distribution);
8965 const process_expression r2_=transform_initial_distribution_term(choice(t).right(),processes_with_initial_distribution);
8975 variable_list stochvars=r2.variables();
8976 maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma;
8977 alphaconvert(stochvars,local_sigma, r1.variables(),data_expression_list());
8978 new_body2=substitute_pCRLproc(new_body2, local_sigma);
8980 process::replace_variables_capture_avoiding_with_an_identifier_generator(r2.distribution(),local_sigma,fresh_identifier_generator);
8982 return stochastic_operator(r1.variables() + stochvars,
8983 real_times_optimized(r1.distribution(),new_distribution),
8984 choice(new_body1,new_body2));
9001 const process_expression r1=transform_initial_distribution_term(seq(t).left(),processes_with_initial_distribution);
9002 const process_expression r2=transform_initial_distribution_term(seq(t).right(),processes_with_initial_distribution);
9013 const if_then& t_=atermpp::down_cast<if_then>(t);
9014 const process_expression r=transform_initial_distribution_term(t_.then_case(),processes_with_initial_distribution);
9027 const if_then_else& t_=atermpp::down_cast<if_then_else>(t);
9028 const process_expression r1_=transform_initial_distribution_term(t_.then_case(),processes_with_initial_distribution);
9029 const process_expression r2_=transform_initial_distribution_term(t_.else_case(),processes_with_initial_distribution);
9040 variable_list stochvars=r2.variables();
9041 maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma;
9042 alphaconvert(stochvars,local_sigma, r1.variables(),data_expression_list());
9043 new_body2=substitute_pCRLproc(new_body2, local_sigma);
9045 process::replace_variables_capture_avoiding_with_an_identifier_generator(r2.distribution(),local_sigma,fresh_identifier_generator);
9047 return stochastic_operator(r1.variables() + stochvars,
9049 lazy::and_(variables_are_equal_to_default_values(stochvars),r1.distribution()),
9050 lazy::and_(variables_are_equal_to_default_values(r1.variables()),new_distribution)),
9051 if_then_else(t_.condition(),new_body1,new_body2));
9076 const sum& s=down_cast<
const sum>(t);
9077 const process_expression r_= transform_initial_distribution_term(s.operand(),processes_with_initial_distribution);
9081 std::set <variable> variables_in_distribution=find_all_variables(r.distribution());
9082 for(
const variable& v: s.variables())
9084 if (variables_in_distribution.count(v)>0)
9086 throw mcrl2::runtime_error(
"Cannot commute a sum operator over a stochastic operator in " +
9087 process::pp(t) +
".\n" +
9088 "The problematic variable is " + pp(v) +
":" + pp(v.sort()) +
".");
9101 const process_expression r_= transform_initial_distribution_term(sto.operand(),processes_with_initial_distribution);
9130 const process_expression r_=transform_initial_distribution_term(at(t).operand(),processes_with_initial_distribution);
9144 throw mcrl2::runtime_error(
"unexpected process format in transform_initial_distribution_term " + process::pp(t) +
".");
9171 variable_list stochvars=r2.variables();
9172 maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma;
9173 alphaconvert(stochvars,local_sigma, r1.variables(),data_expression_list());
9174 new_body2=substitute_pCRLproc(new_body2, local_sigma);
9176 process::replace_variables_capture_avoiding_with_an_identifier_generator(r2.distribution(),local_sigma,fresh_identifier_generator);
9178 return stochastic_operator(r1.variables() + stochvars,
9179 real_times_optimized(r1.distribution(),new_distribution),
9180 choice(new_body1,new_body2));
9211 const if_then& t_if_then=atermpp::down_cast<if_then>(t);
9234 variable_list stochvars=r2.variables();
9235 maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma;
9236 alphaconvert(stochvars,local_sigma, r1.variables(),data_expression_list());
9237 new_body2=substitute_pCRLproc(new_body2, local_sigma);
9239 process::replace_variables_capture_avoiding_with_an_identifier_generator(r2.distribution(),local_sigma,fresh_identifier_generator);
9241 return stochastic_operator(r1.variables() + stochvars,
9242 if_(if_then_else(t).condition(),
9243 lazy::and_(variables_are_equal_to_default_values(stochvars),r1.distribution()),
9244 lazy::and_(variables_are_equal_to_default_values(r1.variables()),new_distribution)),
9245 if_then_else(if_then_else(t).condition(),new_body1,new_body2));
9270 const sum& s=down_cast<
const sum>(t);
9275 std::set <variable> variables_in_distribution=find_all_variables(r.distribution());
9276 for(
const variable& v: s.variables())
9278 if (variables_in_distribution.count(v)>0)
9280 throw mcrl2::runtime_error(
"Cannot commute a sum operator over a stochastic operator in " +
9281 process::pp(t) +
".\n" +
9282 "The problematic variable is " + pp(v) +
":" + pp(v.sort()) +
".");
9338 throw mcrl2::runtime_error(
"unexpected process format in canterminate " + process::pp(t) +
".");
9362 return initial_distribution;
9370 std::set < process_identifier >& visited,
9371 const bool allowrecursion)
9376
9377 const bool r1=canterminatebody(process::merge(t).left(),stable,visited,allowrecursion);
9378 const bool r2=canterminatebody(process::merge(t).right(),stable,visited,allowrecursion);
9387 return (canterminate_rec(u.identifier(),stable,visited));
9394 return (canterminatebody(hide(t).operand(),stable,visited,allowrecursion));
9399 return (canterminatebody(process::rename(t).operand(),stable,visited,allowrecursion));
9404 return (canterminatebody(allow(t).operand(),stable,visited,allowrecursion));
9409 return (canterminatebody(block(t).operand(),stable,visited,allowrecursion));
9414 return (canterminatebody(comm(t).operand(),stable,visited,allowrecursion));
9419 const bool r1=canterminatebody(choice(t).left(),stable,visited,allowrecursion);
9420 const bool r2=canterminatebody(choice(t).right(),stable,visited,allowrecursion);
9426 const bool r1=canterminatebody(seq(t).left(),stable,visited,allowrecursion);
9427 const bool r2=canterminatebody(seq(t).right(),stable,visited,allowrecursion);
9433 return canterminatebody(if_then(t).then_case(),stable,visited,allowrecursion);
9438 const bool r1=canterminatebody(if_then_else(t).then_case(),stable,visited,allowrecursion);
9439 const bool r2=canterminatebody(if_then_else(t).else_case(),stable,visited,allowrecursion);
9445 return (canterminatebody(sum(t).operand(),stable,visited,allowrecursion));
9450 return (canterminatebody(stochastic_operator(t).operand(),stable,visited,allowrecursion));
9470 return canterminatebody(at(t).operand(),stable,visited,allowrecursion);
9475 const bool r1=canterminatebody(process::sync(t).left(),stable,visited,allowrecursion);
9476 const bool r2=canterminatebody(process::sync(t).right(),stable,visited,allowrecursion);
9480 throw mcrl2::runtime_error(
"unexpected process format in canterminate " + process::pp(t) +
".");
9487 std::set < process_identifier >& visited)
9491 if (visited.count(procId)==0)
9493 visited.insert(procId);
9494 const bool ct=canterminatebody(object.processbody,stable,visited,
true);
9506 std::set < process_identifier > visited;
9508 return canterminatebody(t,stable,visited,
false);
9516 std::set < process_identifier > visited;
9518 canterminate_rec(procId,stable,visited);
9525 std::map < process_identifier,process_identifier >& visited_id,
9526 std::map < process_expression,process_expression >& visited_proc)
9528 if (visited_id.count(procId)>0)
9530 return visited_id[procId];
9544 visited_id[procId]=procId;
9545 object.processbody = split_body(object.processbody,
9546 visited_id,visited_proc,
9552 fresh_identifier_generator(procId.name()),
9554 visited_id[procId]=newProcId;
9571
9572
9576 std::set<process_identifier>& visited_processes)
9578 if (visited_processes.count(t.identifier())>0)
9580 throw mcrl2::runtime_error(
"Process " + pp(t.identifier()) +
" is unguardedly defined in itself");
9583 visited_processes.insert(t.identifier());
9588 down_cast<process_instance_assignment>(object.processbody),
9591 maintain_variables_in_rhs<mutable_map_substitution<> > sigma;
9593 for (
const assignment& a: assign.assignments())
9595 sigma[a.lhs()]=a.rhs();
9598 return down_cast<process_instance_assignment>(substitute_pCRLproc(q,sigma));
9605 std::set<process_identifier> visited_processes;
9606 return expand_process_instance_assignment(t,visited_processes);
9610
9611
9612
9613
9614
9615
9616
9617
9618
9619
9620
9621
9625
9626
9629 std::set<process_identifier>& visited_processes)
9631 if (visited_processes.count(procId)==0)
9633 visited_processes.insert(procId);
9635 const std::set<variable> bound_variables;
9636 object.processbody=transform_process_arguments_body(
9644
9647 std::set<process_identifier> visited_processes;
9648 transform_process_arguments(procId,visited_processes);
9652
9655 const std::set<variable>& bound_variables,
9656 std::set<process_identifier>& visited_processes)
9660 transform_process_arguments(process_instance(t).identifier(),visited_processes);
9661 process_instance_assignment t1=transform_process_instance_to_process_instance_assignment(atermpp::down_cast<process_instance>(t),bound_variables);
9666 transform_process_arguments(process_instance_assignment(t).identifier(),visited_processes);
9669 assert(check_valid_process_instance_assignment(u.identifier(),
9670 sort_assignments(u.assignments(),object.parameters)));
9672 sort_assignments(u.assignments(),object.parameters));
9677 return hide(hide(t).hide_set(),
9678 transform_process_arguments_body(hide(t).operand(),bound_variables,visited_processes));
9682 return process::rename(
9683 process::rename(t).rename_set(),
9684 transform_process_arguments_body(process::rename(t).operand(),bound_variables,visited_processes));
9688 return allow(allow(t).allow_set(),
9689 transform_process_arguments_body(allow(t).operand(),bound_variables,visited_processes));
9693 return block(block(t).block_set(),
9694 transform_process_arguments_body(block(t).operand(),bound_variables,visited_processes));
9698 return comm(comm(t).comm_set(),
9699 transform_process_arguments_body(comm(t).operand(),bound_variables,visited_processes));
9704 transform_process_arguments_body(merge(t).left(),bound_variables,visited_processes),
9705 transform_process_arguments_body(merge(t).right(),bound_variables,visited_processes));
9710 transform_process_arguments_body(choice(t).left(),bound_variables,visited_processes),
9711 transform_process_arguments_body(choice(t).right(),bound_variables,visited_processes));
9716 transform_process_arguments_body(seq(t).left(),bound_variables,visited_processes),
9717 transform_process_arguments_body(seq(t).right(),bound_variables,visited_processes));
9721 return if_then_else(
9722 if_then_else(t).condition(),
9723 transform_process_arguments_body(if_then_else(t).then_case(),bound_variables,visited_processes),
9724 transform_process_arguments_body(if_then_else(t).else_case(),bound_variables,visited_processes));
9729 if_then(t).condition(),
9730 transform_process_arguments_body(if_then(t).then_case(),bound_variables,visited_processes));
9734 std::set<variable> bound_variables1=bound_variables;
9735 const variable_list sum_vars=sum(t).variables();
9736 bound_variables1.insert(sum_vars.begin(),sum_vars.end());
9739 transform_process_arguments_body(sum(t).operand(),bound_variables1,visited_processes));
9756 transform_process_arguments_body(at(t).operand(),bound_variables,visited_processes),
9757 at(t).time_stamp());
9761 return process::sync(
9762 transform_process_arguments_body(process::sync(t).left(),bound_variables,visited_processes),
9763 transform_process_arguments_body(process::sync(t).right(),bound_variables,visited_processes));
9769 variable_list vars = tso.variables();
9775 vars = vars + tso1.variables();
9779 return stochastic_operator(
9782 transform_process_arguments_body(body,bound_variables,visited_processes));
9784 throw mcrl2::runtime_error(
"unexpected process format in transform_process_arguments_body " + process::pp(t) +
".");
9791 std::map < process_identifier,process_identifier >& visited_id,
9792 std::map < process_expression,process_expression>& visited_proc,
9793 const variable_list& parameters)
9796
9797
9798
9799
9800
9801
9805 if (visited_proc.count(t)>0)
9807 return visited_proc[t];
9812 result=process::merge(
9813 split_body(process::merge(t).left(),visited_id,visited_proc,parameters),
9814 split_body(process::merge(t).right(),visited_id,visited_proc,parameters));
9820 assert(check_valid_process_instance_assignment(split_process(u.identifier(),visited_id,visited_proc),
9821 sort_assignments(u.assignments(),object.parameters)));
9822 result=process_instance_assignment(
9823 split_process(u.identifier(),visited_id,visited_proc),
9824 sort_assignments(u.assignments(),object.parameters));
9828 result=hide(hide(t).hide_set(),
9829 split_body(hide(t).operand(),visited_id,visited_proc,parameters));
9833 result=process::rename(
9834 process::rename(t).rename_set(),
9835 split_body(process::rename(t).operand(),visited_id,visited_proc,parameters));
9839 result=allow(allow(t).allow_set(),
9840 split_body(allow(t).operand(),visited_id,visited_proc,parameters));
9844 result=block(block(t).block_set(),
9845 split_body(block(t).operand(),visited_id,visited_proc,parameters));
9849 result=comm(comm(t).comm_set(),
9850 split_body(comm(t).operand(),visited_id,visited_proc,parameters));
9855 result=stochastic_operator(t1.variables(),
9857 split_body(t1.operand(),visited_id,visited_proc,parameters));
9880 visited_proc[t]=result;
9887 visited_proc[t]=result;
9892 throw mcrl2::runtime_error(
"unexpected process format in split process " + process::pp(t) +
".");
9901 std::map < process_identifier,process_identifier> visited_id;
9902 std::map < process_expression,process_expression> visited_proc;
9903 return split_process(procId,visited_id,visited_proc);
9910 for (
const stochastic_action_summand& smd: summands)
9912 const action_list multiaction=smd.multi_action().actions();
9913 if (multiaction == action_list({ terminationAction }))
9915 acts.push_front(terminationAction.label());
9916 mCRL2log(mcrl2::log::log_level_t::warning) <<
"The action " << process::pp(terminationAction) <<
9917 " followed by a deadlock is added to signal termination of the linear process. \n";
9927 const std::set <variable>& vars,
9928 const stochastic_action_summand_vector& action_summands,
9929 const deadlock_summand_vector& deadlock_summands,
9930 const variable_list& parameters)
9933
9934
9935
9936
9938 std::set < variable > vars_set(vars.begin(),vars.end());
9939 std::set < variable > vars_result_set;
9941 for (
const deadlock_summand& smd: deadlock_summands)
9943 if (smd.deadlock().has_time())
9945 filter_vars_by_term(smd.deadlock().time(),vars_set,vars_result_set);
9947 filter_vars_by_term(smd.condition(),vars_set,vars_result_set);
9949 for (
const stochastic_action_summand& smd: action_summands)
9951 filter_vars_by_multiaction(smd.multi_action().actions(),vars_set,vars_result_set);
9952 filter_vars_by_assignmentlist(smd.assignments(),parameters,vars_set,vars_result_set);
9954 if (smd.multi_action().has_time())
9956 filter_vars_by_term(smd.multi_action().time(),vars_set,vars_result_set);
9958 filter_vars_by_term(smd.condition(),vars_set,vars_result_set);
9959 filter_vars_by_term(smd.distribution().distribution(),vars_set,vars_result_set);
9961 variable_list result;
9962 for (
const mcrl2::data::variable& i: std::ranges::reverse_view(vars_result_set))
9964 result.push_front(i);
9972 const std::set <variable>& vars,
9973 const data_expression_list& initial_state_expressions)
9975 const std::set < variable > vars_set(vars.begin(),vars.end());
9976 std::set < variable > vars_result_set;
9979 filter_vars_by_termlist(initial_state_expressions.begin(),
9980 initial_state_expressions.end(),
9984 variable_list result;
9985 for (
const mcrl2::data::variable& i: std::ranges::reverse_view(vars_result_set))
9987 result.push_front(i);
9997 stochastic_action_summand_vector& action_summands,
9998 deadlock_summand_vector& deadlock_summands,
9999 variable_list& parameters,
10000 data_expression_list& initial_state,
10004
10011 std::vector <process_identifier> pcrlprocesslist;
10012 collectPcrlProcesses(init_,pcrlprocesslist);
10014 if (pcrlprocesslist.size()==0)
10016 throw mcrl2::runtime_error(
"There are no processes to be linearised. This is most likely due to the use of unguarded recursion in process equations");
10022
10023 procstovarheadGNF(pcrlprocesslist);
10026
10027 procstorealGNF(init_,options.lin_method!=t_lin_method::lmStack);
10030 generateLPEmCRL(action_summands,
10033 options.lin_method!=t_lin_method::lmStack,
10036 initial_stochastic_distribution,
10037 dummy_ultimate_delay_condition);
10038 allowblockcomposition(action_name_multiset_list({action_name_multiset()}),
false,action_summands,deadlock_summands,terminationAction,options.ignore_time,options.nodeltaelimination);
10039 if (options.final_cluster)
10041 cluster_actions(action_summands,deadlock_summands,parameters);
10044 AddTerminationActionIfNecessary(action_summands);
10055 mCRL2log(mcrl2::log::log_level_t::verbose) <<
"linearising the process specification using the '" << lin_options.lin_method <<
"' method.\n";
10063 balance_summands(input_process);
10071 std::set<data::sort_expression> s;
10072 process::find_sort_expressions(input_process.action_labels(), std::inserter(s, s.end()));
10073 process::find_sort_expressions(input_process.equations(), std::inserter(s, s.end()));
10074 process::find_sort_expressions(input_process.init(), std::inserter(s, s.end()));
10075 s.insert(sort_real::real_());
10076 data_spec.add_context_sorts(s);
10079 input_process.equations(),
10080 data::variable_list(input_process.global_variables().begin(),input_process.global_variables().end()),
10082 input_process.global_variables(),
10088 variable_list parameters;
10089 data_expression_list initial_state;
10090 stochastic_action_summand_vector action_summands;
10091 deadlock_summand_vector deadlock_summands;
10095 spec.transform(init,action_summands,deadlock_summands,parameters,initial_state,initial_distribution);
10098 data::variable_list globals1 = spec.SieveProcDataVarsSummands(spec.global_variables,action_summands,deadlock_summands,parameters);
10099 data::variable_list globals2 = spec.SieveProcDataVarsAssignments(spec.global_variables,initial_state);
10100 std::set<data::variable> global_variables;
10101 global_variables.insert(globals1.begin(), globals1.end());
10102 global_variables.insert(globals2.begin(), globals2.end());
10111 stochastic_process_initializer(initial_state,initial_distribution));
aterm_string & operator=(const aterm_string &t) noexcept=default
A unordered_map class in which aterms can be stored.
An abstraction expression.
const variable_list & variables() const
const data_expression & body() const
const binder_type & binding_operator() const
alias(const basic_sort &name, const sort_expression &reference)
\brief Constructor Z12.
\brief Assignment of a data expression to a variable
const data_expression & rhs() const
const variable & lhs() const
data_expression & operator=(const data_expression &) noexcept=default
data_expression()
\brief Default constructor X3.
data_expression & operator=(data_expression &&) noexcept=default
data_expression(const data_expression &) noexcept=default
Move semantics.
function_symbol & operator=(function_symbol &&) noexcept=default
function_symbol()
Default constructor.
Rewriter that operates on data expressions.
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
sort_expression & operator=(const sort_expression &) noexcept=default
\brief A constructor for a structured sort
function_symbol constructor_function(const sort_expression &s) const
Returns the constructor function for this constructor, assuming it is internally represented with sor...
function_symbol recogniser_function(const sort_expression &s) const
Returns the function corresponding to the recogniser of this constructor, such that it is usable in t...
const core::identifier_string & name() const
variable & operator=(variable &&) noexcept=default
const sort_expression & sort() const
\brief A where expression
where_clause(const atermpp::aterm &term)
bool has_time() const
Returns true if time is available.
Algorithm class for elimination of constant parameters.
LPS summand containing a deadlock.
ultimate_delay()
Constructor.
data_expression & constraint()
Obtain a reference to the constraint.
LPS summand containing a multi-action.
\brief A stochastic distribution
stochastic_distribution & operator=(stochastic_distribution &&) noexcept=default
stochastic_distribution()
\brief Default constructor X3.
const data::variable_list & variables() const
stochastic_distribution(const data::variable_list &variables, const data::data_expression &distribution)
\brief Constructor Z12.
const data::data_expression & distribution() const
A stochastic process initializer.
stochastic_process_initializer(const data::data_expression_list &expressions, const stochastic_distribution &distribution)
Constructor.
Linear process specification.
const core::identifier_string & name() const
action(const atermpp::aterm &term)
const data::data_expression_list & arguments() const
const action_label & label() const
\brief The allow operator
allow(const atermpp::aterm &term)
const process_expression & operand() const
at(const atermpp::aterm &term)
at(const process_expression &operand, const data::data_expression &time_stamp)
\brief Constructor Z14.
const data::data_expression & time_stamp() const
const process_expression & operand() const
\brief The block operator
const process_expression & operand() const
block(const atermpp::aterm &term)
\brief The choice operator
choice(const atermpp::aterm &term)
const process_expression & left() const
choice(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
const process_expression & right() const
\brief The communication operator
comm(const atermpp::aterm &term)
const process_expression & operand() const
delta()
\brief Default constructor X3.
hide(const atermpp::aterm &term)
const process_expression & operand() const
\brief The if-then-else operator
const process_expression & else_case() const
const process_expression & then_case() const
if_then_else(const atermpp::aterm &term)
const data::data_expression & condition() const
if_then_else(const data::data_expression &condition, const process_expression &then_case, const process_expression &else_case)
\brief Constructor Z14.
\brief The if-then operator
const process_expression & then_case() const
if_then(const data::data_expression &condition, const process_expression &then_case)
\brief Constructor Z14.
if_then(const atermpp::aterm &term)
const data::data_expression & condition() const
\brief The merge operator
merge(const atermpp::aterm &term)
const process_expression & right() const
const process_expression & left() const
\brief A process expression
process_expression & operator=(const process_expression &) noexcept=default
process_expression(const process_expression &) noexcept=default
Move semantics.
process_expression()
\brief Default constructor X3.
process_expression & operator=(process_expression &&) noexcept=default
\brief A process identifier
process_identifier(const process_identifier &) noexcept=default
Move semantics.
process_identifier & operator=(const process_identifier &) noexcept=default
const core::identifier_string & name() const
process_identifier & operator=(process_identifier &&) noexcept=default
process_identifier()
Default constructor.
\brief A process assignment
process_instance_assignment(const process_instance_assignment &) noexcept=default
Move semantics.
process_instance_assignment(const process_identifier &identifier, const data::assignment_list &assignments)
\brief Constructor Z14.
const data::assignment_list & assignments() const
process_instance_assignment(const atermpp::aterm &term)
const process_identifier & identifier() const
const data::data_expression_list & actual_parameters() const
const process_identifier & identifier() const
Process specification consisting of a data specification, action labels, a sequence of process equati...
process_expression & init()
Returns the initialization of the process specification.
process::action_label_list & action_labels()
Returns the action label specification.
\brief The rename operator
rename(const atermpp::aterm &term)
const process_expression & operand() const
\brief The sequential composition
const process_expression & right() const
seq(const atermpp::aterm &term)
const process_expression & left() const
seq(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
\brief The distribution operator
const data::variable_list & variables() const
const data::data_expression & distribution() const
const process_expression & operand() const
stochastic_operator(const data::variable_list &variables, const data::data_expression &distribution, const process_expression &operand)
\brief Constructor Z14.
const process_expression & operand() const
sum(const data::variable_list &variables, const process_expression &operand)
\brief Constructor Z14.
sum(const atermpp::aterm &term)
const data::variable_list & variables() const
\brief The synchronization operator
const process_expression & left() const
sync(const process_expression &left, const process_expression &right)
\brief Constructor Z14.
const process_expression & right() const
sync(const atermpp::aterm &term)
tau()
\brief Default constructor X3.
process_expression processbody
objectdatatype(const objectdatatype &o)=default
process_expression representedprocess
~objectdatatype()=default
process::action_label_list multi_action_names
processstatustype processstatus
identifier_string objectname
std::set< variable > get_free_variables() const
objectdatatype & operator=(const objectdatatype &o)=default
process_identifier process_representing_action
function_symbol_list functions
data_expression_list elementnames
enumeratedtype(const enumeratedtype &e)
enumeratedtype(const std::size_t n, specification_basic_type &spec)
enumeratedtype & operator=(const enumeratedtype &e)=default
~enumeratedtype()=default
enumtype(const enumtype &)=delete
enumtype & operator=(const enumtype &)=delete
std::size_t enumeratedtype_index
enumtype(std::size_t n, const sort_expression_list &fsorts, const sort_expression_list &gsorts, specification_basic_type &spec)
process_expression m_process_body
process_pid_pair & operator=(const process_pid_pair &other)=default
const process_expression & process_body() const
const process_identifier & process_id() const
process_pid_pair(const process_pid_pair &other)=default
process_pid_pair & operator=(process_pid_pair &&other)=default
process_pid_pair(const process_expression &process_body, const process_identifier &pid)
process_pid_pair(process_pid_pair &&other)=default
variable_list booleanStateVariables
static stackoperations * find_suitable_stack_operations(const variable_list ¶meters, stackoperations *stack_operations_list)
stacklisttype & operator=(const stacklisttype &)=delete
stacklisttype(const variable_list &parlist, specification_basic_type &spec, const bool regular, const std::set< process_identifier > &pCRLprocs, const bool singlecontrolstate)
Constructor.
stacklisttype(const stacklisttype &)=delete
stackoperations & operator=(const stackoperations &)=delete
data::function_symbol pop
data::function_symbol push
stackoperations(const stackoperations &)=delete
sort_expression_list sorts
data::function_symbol empty
data::function_symbol getstate
variable_list parameter_list
~stackoperations()=default
data::function_symbol emptystack
stackoperations(const variable_list &pl, specification_basic_type &spec)
sort_expression stacksort
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)
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::maintain_variables_in_rhs< data::mutable_map_substitution<> > make_unique_variables(const variable_list &var_list, const std::string &hint)
variable_list parscollect(const process_expression &oldbody, process_expression &newbody)
stochastic_action_summand collect_sum_arg_arg_cond(const enumtype &e, const stochastic_action_summand_vector &action_summands, const variable_list ¶meters)
action_list linMergeMultiActionList(const action_list &ma1, const action_list &ma2)
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 ¶meters, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution)
variable get_fresh_variable(const std::string &s, const sort_expression &sort, const int reuse_index=-1)
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)
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)
static void complete_proc_identifier_map(std::map< process_identifier, process_identifier > &identifier_identifier_map)
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)
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)
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 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 insertvariable(const variable &var, const bool mustbenew)
process_identifier storeinit(const process_expression &init)
static action_list to_sorted_action_list(const process_expression &p)
Convert the process expression to a sorted action list.
process_expression pCRLrewrite(const process_expression &t)
data_expression_list pushdummy_regular_data_expressions(const variable_list &pars, const stacklisttype &stack)
void define_equations_for_case_function(const std::size_t index, const data::function_symbol &functionname, const sort_expression &sort)
void alphaconvert(variable_list &sumvars, MutableSubstitution &sigma, const variable_list &occurvars, const data_expression_list &occurterms)
bool canterminatebody(const process_expression &t)
data_expression transform_matching_list(const variable_list &matchinglist)
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)
bool isDeltaAtZero(const process_expression &t)
data::function_symbol find_case_function(std::size_t index, const sort_expression &sort) const
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)
static bool summandsCanBeClustered(const stochastic_action_summand &summand1, const stochastic_action_summand &summand2)
static sort_expression_list getActionSorts(const action_list &actionlist)
void filter_vars_by_multiaction(const action_list &multiaction, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
static process_identifier get_last(const process_identifier &id, const std::map< process_identifier, process_identifier > &identifier_identifier_map)
static bool check_real_variable_occurrence(const variable_list &sumvars, const data_expression &actiontime, const data_expression &condition)
process_identifier newprocess(const variable_list ¶meters, const process_expression &body, const processstatustype ps, const bool canterminate, const bool containstime)
void make_pCRL_procs(const process_identifier &id, std::set< process_identifier > &reachable_process_identifiers)
void filter_vars_by_term(const data_expression &t, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
data_expression_list pushdummy_stack(const variable_list ¶meters, const stacklisttype &stack, const variable_list &stochastic_variables)
void procstorealGNFrec(const process_identifier &procIdDecl, const variableposition v, std::vector< process_identifier > &todo, const bool regular)
static action_label_list getnames(const process_expression &multiAction)
variable_list getparameters_rec(const process_expression &multiAction, std::set< variable > &occurs_set)
static int match_sequence(const std::vector< process_instance_assignment > &s1, const std::vector< process_instance_assignment > &s2, const bool regular2)
assignment_list argscollect_regular2(const process_expression &t, variable_list &vl)
assignment_list make_optimised_assignment_list(const variable_list ¶meters, const data_expression_list &resultnextstate, const variable_list &sum_vars, const variable_list &stoch_vars)
bool fresh_equation_added
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)
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 ¶meters)
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)
bool occursintermlist(const variable &var, const assignment_list &r, const process_identifier &proc_name) const
void transform_process_arguments(const process_identifier &procId)
objectdatatype & insert_process_declaration(const process_identifier &procId, const variable_list ¶meters, const process_expression &body, processstatustype s, const bool canterminate, const bool containstime)
static void set_proc_identifier_map(std::map< process_identifier, process_identifier > &identifier_identifier_map, const process_identifier &id1_, const process_identifier &id2_, const process_identifier &initial_process)
bool canterminate_rec(const process_identifier &procId, bool &stable, std::set< process_identifier > &visited)
set_identifier_generator fresh_identifier_generator
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)
void filter_vars_by_termlist(Iterator begin, const Iterator &end, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
bool searchProcDeclaration(const variable_list ¶meters, const process_expression &body, const processstatustype s, const bool canterminate, const bool containstime, process_identifier &p) const
process_identifier splitmCRLandpCRLprocsAndAddTerminatedAction(const process_identifier &procId)
action_list linMergeMultiActionListProcess(const process_expression &ma1, const process_expression &ma2)
std::vector< process_equation > procs
action_list adapt_multiaction_to_stack(const action_list &multiAction, const stacklisttype &stack, const variable_list &vars)
void determinewhetherprocessescanterminate(const process_identifier &procId)
process_expression distribute_condition(const process_expression &body1, const data_expression &condition)
bool containstime_rec(const process_identifier &procId, bool *stable, std::set< process_identifier > &visited, bool &contains_if_then)
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)
data_expression correctstatecond(const process_identifier &procId, const std::set< process_identifier > &pCRLproc, const stacklisttype &stack, int regular)
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)
processstatustype determine_process_statusterm(const process_expression &body, const processstatustype status)
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)
data_expression getvar(const variable &var, const stacklisttype &stack) const
variable_list initdatavars
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,...
process_expression distributeTime(const process_expression &body, const data_expression &time, const variable_list &freevars, data_expression &timecondition)
data_expression_list pushdummyrec_stack(const variable_list &totalpars, const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)
static action_list to_action_list(const process_expression &p)
std::set< data::variable > sigma_variables(const Substitution &sigma)
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)
process_expression cut_off_unreachable_tail(const process_expression &t)
std::vector< enumeratedtype > enumeratedtypes
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)
process::action_label_list acts
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)
std::size_t create_enumeratedtype(const std::size_t n)
void generateLPEmCRL(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const process_identifier &procIdDecl, const bool regular, variable_list &pars, data_expression_list &init, stochastic_distribution &initial_stochastic_distribution, lps::detail::ultimate_delay &ultimate_delay_condition)
process_instance_assignment expand_process_instance_assignment(const process_instance_assignment &t)
static process_expression delta_at_zero()
assignment_list rewrite_assignments(const assignment_list &t)
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)
void transform_process_arguments(const process_identifier &procId, std::set< process_identifier > &visited_processes)
std::set< process_identifier > minimize_set_of_reachable_process_identifiers(const std::set< process_identifier > &reachable_process_identifiers, const process_identifier &initial_process)
void collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)
variable_list make_binary_sums(std::size_t n, const sort_expression &enumtypename, data_expression &condition, const variable_list &tail)
variable_list SieveProcDataVarsAssignments(const std::set< variable > &vars, const data_expression_list &initial_state_expressions)
data_expression_list extend_conditions(const variable &var, const data_expression_list &conditionlist)
bool check_valid_process_instance_assignment(const process_identifier &id, const assignment_list &assignments)
void calculate_left_merge_deadlock(const lps::detail::ultimate_delay &ultimate_delay_condition, const deadlock_summand_vector &deadlock_summands1, const bool is_allow, const bool is_block, const stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands)
void addString(const identifier_string &str)
void procstovarheadGNF(const std::vector< process_identifier > &procs)
static process_expression action_list_to_process(const action_list &ma)
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)
void alphaconvertprocess(variable_list &sumvars, MutableSubstitution &sigma, const process_expression &p)
process_expression obtain_initial_distribution_term(const process_expression &t)
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)
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)
bool stochastic_operator_is_being_used
void declare_control_state(const std::set< process_identifier > &pCRLprocs)
void create_case_function_on_enumeratedtype(const sort_expression &sort, const std::size_t enumeratedtype_index)
variable_list SieveProcDataVarsSummands(const std::set< variable > &vars, const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands, const variable_list ¶meters)
static data_expression_list extend(const data_expression &c, const data_expression_list &cl)
specification_basic_type & operator=(const specification_basic_type &)=delete
static bool occursinvarandremove(const variable &var, 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)
process_identifier terminatedProcId
process_expression distribute_sum(const variable_list &sumvars, const process_expression &body1)
data_expression variables_are_equal_to_default_values(const variable_list &vl)
void procstorealGNF(const process_identifier &procsIdDecl, const bool regular)
static bool check_assignment_list(const assignment_list &assignments, const variable_list ¶meters)
data_expression RewriteTerm(const data_expression &t)
void alphaconversion(const process_identifier &procId, const variable_list ¶meters)
bool all_equal(const atermpp::term_list< T > &l)
void cluster_actions(stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, const variable_list &pars)
process_expression transform_initial_distribution_term(const process_expression &t, const std::map< process_identifier, process_pid_pair > &processes_with_initial_distribution)
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 transform_process_arguments_body(const process_expression &t, const std::set< variable > &bound_variables, std::set< process_identifier > &visited_processes)
static assignment_list parameters_to_assignment_list(const variable_list ¶meters, const std::set< variable > &variables_bound_in_sum)
assignment_list dummyparameterlist(const stacklisttype &stack, const bool singlestate)
mcrl2::data::rewriter rewr
void make_pCRL_procs(const process_expression &t, std::set< process_identifier > &reachable_process_identifiers)
stackoperations * stack_operations_list
process_expression wraptime(const process_expression &body, const data_expression &time, const variable_list &freevars)
objectdatatype & objectIndex(const process_identifier &o)
process_identifier split_process(const process_identifier &procId, std::map< process_identifier, process_identifier > &visited_id, std::map< process_expression, process_expression > &visited_proc)
bool mergeoccursin(variable &var, const variable_list &v, variable_list &matchinglist, variable_list &pars, data_expression_list &args, const variable_list &process_parameters)
static bool occursintermlist(const variable &var, const data_expression_list &r)
bool exists_variable_for_sequence(const std::vector< process_instance_assignment > &process_names, process_identifier &result)
std::set< variable > find_free_variables_process(const process_expression &p)
process_expression alphaconversionterm(const process_expression &t, const variable_list ¶meters, maintain_variables_in_rhs< mutable_map_substitution<> > sigma)
process_expression putbehind(const process_expression &body1, const process_expression &body2)
assignment_list substitute_assignmentlist(const assignment_list &assignments, const variable_list ¶meters, const bool replacelhs, const bool replacerhs, Substitution &sigma)
process_instance_assignment transform_process_instance_to_process_instance_assignment(const process_instance &procId, const std::set< variable > &bound_variables=std::set< variable >())
process_instance_assignment RewriteProcess(const process_instance_assignment &t)
process_identifier delta_process
const objectdatatype & objectIndex(const process_identifier &o) const
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)
bool alreadypresent(variable &var, const variable_list &vl, mutable_indexed_substitution<> ¶meter_renaming)
variable_list parameters_that_occur_in_body(const variable_list ¶meters, const process_expression &body)
process_expression enumerate_distribution_and_sums(const variable_list &sumvars, const variable_list &stochvars, const data_expression &distribution, const process_expression &body)
bool containstimebody(const process_expression &t)
assignment_list make_procargs(const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const variable_list &vars, const bool regular, const bool singlestate, const variable_list &stochastic_variables)
data_expression adapt_term_to_stack(const data_expression &t, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)
data_expression_list processencoding(std::size_t i, const data_expression_list &t1, const stacklisttype &stack)
process_expression RewriteMultAct(const process_expression &t)
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.
~specification_basic_type()
variable_list make_pars(const sort_expression_list &sortlist)
specification_basic_type(const specification_basic_type &)=delete
static data_expression real_times_optimized(const data_expression &r1, const data_expression &r2)
bool occursinpCRLterm(const variable &var, const process_expression &p, const bool strict)
void collectPcrlProcesses(const process_identifier &procDecl, std::vector< process_identifier > &pcrlprocesses)
static std::size_t upperpowerof2(std::size_t i)
void extract_names(const process_expression &sequence, std::vector< process_instance_assignment > &result)
std::map< aterm, objectdatatype > objectdata
action RewriteAction(const action &t)
data_expression_vector adapt_termlist_to_stack(Iterator begin, const Iterator &end, const stacklisttype &stack, const variable_list &vars, const variable_list &stochastic_variables)
data_expression make_procargs_stack(const process_expression &t, const stacklisttype &stack, const std::set< process_identifier > &pcrlprcs, const variable_list &vars, const variable_list &stochastic_variables)
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)
variable_list getparameters(const process_expression &multiAction)
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)
void collectPcrlProcesses_term(const process_expression &body, std::vector< process_identifier > &pcrlprocesses, std::set< process_identifier > &visited)
data_expression representative_generator_internal(const sort_expression &s, const bool allow_dont_care_var=true)
assignment_list processencoding(std::size_t i, const assignment_list &t1, const stacklisttype &stack)
objectdatatype & addMultiAction(const process_expression &multiAction, bool &isnew)
void storeprocs(const std::vector< process_equation > &procs)
process_expression substitute_pCRLproc(const process_expression &p, Substitution &sigma)
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="")
std::set< variable > global_variables
static data_expression getRHSassignment(const variable &var, const assignment_list &as)
variable_list construct_renaming(const variable_list &pars1, const variable_list &pars2, variable_list &pars3, variable_list &pars4, const bool unique=true)
void determine_process_status(const process_identifier &procDecl, const processstatustype status)
static action_list makemultiaction(const process::action_label_list &actionIds, const data_expression_list &args)
void insertvariables(const variable_list &vars, const bool mustbenew)
variable_list collectparameterlist(std::set< process_identifier > &pCRLprocs)
data_expression_list RewriteTermList(const data_expression_list &t)
variable_list make_parameters_rec(const data_expression_list &l, std::set< variable > &occurs_set)
void detail_check_objectdata(const process_identifier &o) const
static assignment_list filter_assignments(const assignment_list &assignments, const variable_list ¶meters)
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 containstimebody(const process_expression &t, bool *stable, std::set< process_identifier > &visited, bool allowrecursion, bool &contains_if_then)
static assignment_list sort_assignments(const assignment_list &ass, const variable_list ¶meters)
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)
process_identifier tau_process
static sort_expression_list get_sorts(const List &l)
std::vector< process_identifier > seq_varnames
void storeact(const process::action_label_list &acts)
bool is_global_variable(const data_expression &d) const
variable_list joinparameters(const variable_list &par1, const variable_list &par2, mutable_indexed_substitution<> ¶meter_renaming)
static bool occursin(const variable &name, const variable_list &pars)
bool canterminatebody(const process_expression &t, bool &stable, std::set< process_identifier > &visited, const bool allowrecursion)
void AddTerminationActionIfNecessary(const stochastic_action_summand_vector &summands)
bool determinewhetherprocessescontaintime(const process_identifier &procId)
void filter_vars_by_assignmentlist(const assignment_list &assignments, const variable_list ¶meters, const std::set< variable > &vars_set, std::set< variable > &vars_result_set)
data_expression_list addcondition(const variable_list &matchinglist, const data_expression_list &conditionlist)
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 transform(const process_identifier &init, stochastic_action_summand_vector &action_summands, deadlock_summand_vector &deadlock_summands, variable_list ¶meters, data_expression_list &initial_state, stochastic_distribution &initial_stochastic_distribution)
process_expression obtain_initial_distribution(const process_identifier &procId)
objectdatatype & insertAction(const action_label &actionId)
Expression replace_variables_capture_avoiding_alt(const Expression &e, Substitution &sigma)
process_instance_assignment expand_process_instance_assignment(const process_instance_assignment &t, std::set< process_identifier > &visited_processes)
assignment_list pushdummy_regular(const variable_list &pars, const stacklisttype &stack, const variable_list &stochastic_variables)
assignment_list argscollect_regular(const process_expression &t, const variable_list &vl, const std::set< variable > &variables_bound_in_sum)
static data_expression_list getarguments(const action_list &multiAction)
lps::detail::ultimate_delay getUltimateDelayCondition(const stochastic_action_summand_vector &action_summands, const deadlock_summand_vector &deadlock_summands, const variable_list &freevars)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
A collection of utilities for lazy expression construction.
data_expression and_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p or q.
Namespace for system defined sort bool_.
const basic_sort & bool_()
Constructor for sort expression Bool.
const function_symbol & false_()
Constructor for function symbol false.
const function_symbol & true_()
Constructor for function symbol true.
Namespace for system defined sort real_.
data_expression & real_one()
bool is_plus_application(const atermpp::aterm &e)
Recogniser for application of +.
data_expression & real_zero()
application times(const data_expression &arg0, const data_expression &arg1)
Application of function symbol *.
bool is_application(const data_expression &t)
Returns true if the term t is an application.
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
application less(const data_expression &arg0, const data_expression &arg1)
Application of function symbol <.
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
application if_(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
Application of function symbol if.
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
const data_expression_list & variable_list_to_data_expression_list(const variable_list &l)
Transform a variable_list into a data_expression_list.
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
The main namespace for the LPS library.
void complete_data_specification(stochastic_specification &spec)
Adds all sorts that appear in the process of l to the data specification of l.
bool occursinterm(const data::data_expression &t, const data::variable &var)
mcrl2::lps::stochastic_specification linearise(const mcrl2::process::process_specification &type_checked_spec, const mcrl2::lps::t_lin_options &lin_options=t_lin_options())
Linearises a process specification.
The main namespace for the Process library.
bool is_at(const atermpp::aterm &x)
bool is_process_instance(const atermpp::aterm &x)
bool is_process_instance_assignment(const atermpp::aterm &x)
bool is_tau(const atermpp::aterm &x)
bool is_seq(const atermpp::aterm &x)
bool is_merge(const atermpp::aterm &x)
bool is_allow(const atermpp::aterm &x)
bool is_bounded_init(const atermpp::aterm &x)
bool is_delta(const atermpp::aterm &x)
bool is_sum(const atermpp::aterm &x)
bool is_block(const atermpp::aterm &x)
bool is_if_then_else(const atermpp::aterm &x)
bool is_comm(const atermpp::aterm &x)
void alphabet_reduce(process_specification &procspec, std::size_t duplicate_equation_limit=(std::numeric_limits< size_t >::max)())
Applies alphabet reduction to a process specification.
bool is_action(const atermpp::aterm &x)
bool is_left_merge(const atermpp::aterm &x)
bool is_hide(const atermpp::aterm &x)
bool is_if_then(const atermpp::aterm &x)
bool is_choice(const atermpp::aterm &x)
bool is_stochastic_operator(const atermpp::aterm &x)
bool is_rename(const atermpp::aterm &x)
bool is_sync(const atermpp::aterm &x)
void swap(atermpp::aterm &t1, atermpp::aterm &t2) noexcept
Swaps two term_applss.
Options for linearisation.
bool apply_alphabet_axioms
make_substitution(const std::map< process_identifier, process_identifier > &map)
process_identifier operator()(const process_identifier &id) const
const std::map< process_identifier, process_identifier > & m_map