linearise.cpp

Go to the documentation of this file.

// Author(s): Jan Friso Groote
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
/* This file contains the implementation of an mCRL2 lineariser.
 
   It is based on the implementation of the mCRL lineariser, on which work
   started on 12 juli 1997.  This lineariser was based on the CWI technical
   report "The Syntax and Semantics of Timed mCRL", by J.F. Groote.
 
   Everybody is free to use this software, provided it is not changed.
 
   In case problems are encountered when using this software, please report
   them to J.F. Groote, TU/e, Eindhoven, J.F.Groote@tue.nl
 
   This software comes as it is. I.e. the author assumes no responsibility for
   the use of this software.
*/
 
//mCRL2 data
#include "mcrl2/data/substitutions/maintain_variables_in_rhs.h"
#include "mcrl2/data/fourier_motzkin.h"
#include "mcrl2/data/enumerator.h" 
#include "mcrl2/data/real_utilities.h"
 
// linear process libraries.
#include "mcrl2/lps/detail/ultimate_delay.h"
#include "mcrl2/lps/linearise.h"
#include "mcrl2/lps/sumelm.h"
#include "mcrl2/lps/constelm.h"
#include "mcrl2/lps/replace_capture_avoiding_with_an_identifier_generator.h"
 
// Process libraries.
#include "mcrl2/process/alphabet_reduce.h"
#include "mcrl2/process/balance_nesting_depth.h"
 
 
// For Aterm library extension functions
using namespace atermpp;
using namespace mcrl2;
using namespace mcrl2::core;
using namespace mcrl2::core::detail;
using namespace mcrl2::data;
using namespace mcrl2::data::detail;
using namespace mcrl2::lps;
using namespace mcrl2::process;
 
/*  Preamble */
 
typedef enum { unknown,
               mCRL,
               mCRLdone,
               mCRLbusy,
               mCRLlin,
               pCRL,
               multiAction,
               GNF,
               GNFalpha,
               GNFbusy,
               error
             } processstatustype;
 
 
 
/**************** Definitions of object class  ***********************/
 
typedef enum { none,
               _map,
               func,
               act,
               proc,
               variable_,
               sorttype,
               multiact
             } objecttype;
 
class objectdatatype
{
  public:
    identifier_string objectname;
    process::action_label_list multi_action_names;
    bool constructor;
    process_expression representedprocess;
    process_identifier process_representing_action; /* for actions target sort is used to
                                                       indicate the process representing this action. */
    process_expression processbody;
    std::set <variable> free_variables;
    bool free_variables_defined;
    variable_list parameters;
    variable_list old_parameters;
    processstatustype processstatus;
    objecttype object;
    bool canterminate;
    bool containstime;
 
    objectdatatype()
    {
      constructor=false;
      processstatus=unknown;
      object=none;
      canterminate=0;
      containstime=false;
    }
 
    objectdatatype(const objectdatatype& o)
    {
      objectname=o.objectname;
      multi_action_names=o.multi_action_names;
      constructor=o.constructor;
      representedprocess=o.representedprocess;
      process_representing_action=o.process_representing_action;
      processbody=o.processbody;
      free_variables=o.free_variables;
      free_variables_defined=o.free_variables_defined;
      parameters=o.parameters;
      processstatus=o.processstatus;
      object=o.object;
      canterminate=o.canterminate;
      containstime=o.containstime;
    }
 
    const objectdatatype& operator=(const objectdatatype& o)
    {
      objectname=o.objectname;
      multi_action_names=o.multi_action_names;
      constructor=o.constructor;
      representedprocess=o.representedprocess;
      process_representing_action=o.process_representing_action;
      processbody=o.processbody;
      free_variables=o.free_variables;
      free_variables_defined=o.free_variables_defined;
      parameters=o.parameters;
      processstatus=o.processstatus;
      object=o.object;
      canterminate=o.canterminate;
      containstime=o.containstime;
      return (*this);
    }
 
    ~objectdatatype()
    {
    }
};
 
 
class specification_basic_type
{
  public:
    process::action_label_list acts;     /* storage place for actions */
    std::set < variable > global_variables; /* storage place for free variables occurring
                                   in processes ranging over data */
    variable_list initdatavars; /* storage place for free variables in
                                   init clause */
    data_specification data;    /* contains the data specification for the current process.  */
 
    specification_basic_type(const specification_basic_type& )=delete;
    specification_basic_type& operator=(const specification_basic_type&)=delete;
 
  private:
    class stackoperations;
    class stacklisttype;
    class enumtype;
    class enumeratedtype;
 
    std::vector < process_equation > procs;
    /* storage place for processes,
       uses alt, seq, par, lmer, cond,sum,
       com, bound, at, name, delta,
       tau, hide, rename, encap */
    mcrl2::data::rewriter rewr; /* The rewriter used while linearising */
    action terminationAction;   /* A list of length one with the action that denotes termination */
    process_identifier terminatedProcId; /* A process identifier of which the body consists of the termination
                                            action */
    process_identifier tau_process;
    process_identifier delta_process;
    std::vector < process_identifier > seq_varnames; /* Contains names of processes which represent a sequence
                                                            of process variables */
    std::vector < std::vector < process_instance_assignment > > representedprocesses; /* contains the sequences of process
                                                         instances that are represented by the variables in seq_varnames */
    t_lin_options options;
    bool timeIsBeingUsed;
    bool stochastic_operator_is_being_used;
    bool fresh_equation_added;
    std::map < aterm, objectdatatype > objectdata; // It is important to guarantee that the objects will not
                                                   // be moved to another place when the object data structure grows. This
                                                   // is because objects in this datatype  are passed around by reference.
 
    set_identifier_generator fresh_identifier_generator;
    std::vector < enumeratedtype > enumeratedtypes;
    stackoperations* stack_operations_list;
 
  public:
    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):
      acts(),
      global_variables(glob_vars),
      data(ds),
      rewr(data,opt.rewrite_strategy),
      options(opt),
      timeIsBeingUsed(false),
      stochastic_operator_is_being_used(false),
      fresh_equation_added(false)
    {
      // find_identifiers does not find the identifiers in the enclosed data specification.
      fresh_identifier_generator.add_identifiers(process::find_identifiers(procspec));
      // So, the identifiers in the data type must be added explicitly.
      fresh_identifier_generator.add_identifiers(data::find_identifiers(ds.equations()));
      fresh_identifier_generator.add_identifiers(data::find_identifiers(ds.user_defined_aliases()));
      fresh_identifier_generator.add_identifiers(data::find_identifiers(ds.sorts()));
      fresh_identifier_generator.add_identifiers(data::find_identifiers(ds.constructors()));
      fresh_identifier_generator.add_identifiers(data::find_identifiers(ds.mappings()));
 
      stack_operations_list=nullptr;
      acts=as;
      storeact(acts);
      procs=ps;
      storeprocs(procs);
      initdatavars=idvs;
      // The terminationAction and the terminatedProcId must be defined after initialisation of
      // data as otherwise fresh name does not work properly.
      terminationAction=action(action_label(fresh_identifier_generator("Terminate"),sort_expression_list()),data_expression_list());
      terminatedProcId=process_identifier(fresh_identifier_generator("Terminated**"), variable_list());
// /* Changed delta() to DeltaAtZero on 24/12/2006. Moved back in spring 2007, as this introduces unwanted time constraints. */
      insert_process_declaration(
        terminatedProcId,
        variable_list(),
        seq(terminationAction,delta()),
        pCRL,0,false);
      delta_process=newprocess(variable_list(),delta(),pCRL,false,false);
      tau_process=newprocess(variable_list(),tau(),pCRL,true,false);
    }
 
    ~specification_basic_type()
    {
      for (; stack_operations_list!=nullptr;)
      {
        stackoperations* temp=stack_operations_list->next;
        delete stack_operations_list;
        stack_operations_list=temp;
      }
 
    }
 
  private:
    /* data_expression real_zero()
    {
      static data_expression zero=sort_real::creal(sort_int::cint(sort_nat::c0()),sort_pos::c1());
      return zero;
    }
 
    data_expression real_one()
    {
      static data_expression one=sort_real::creal(sort_int::cint(sort_nat::cnat(sort_pos::c1())),sort_pos::c1());
      return one;
    } */
 
    data_expression real_times_optimized(const data_expression& r1, const data_expression& r2)
    {
      if (r1==sort_real::real_zero() || r2==sort_real::real_zero())
      {
        return sort_real::real_zero();
      }
      if (r1==sort_real::real_one())
      {
        return r2;
      }
      if (r2==sort_real::real_one())
      {
        return r1;
      }
      return sort_real::times(r1,r2);
    }
 
    process_expression delta_at_zero(void)
    {
      return at(delta(), sort_real::real_(0));
    }
 
    bool isDeltaAtZero(const process_expression& t)
    {
      if (!is_at(t))
      {
        return false;
      }
      if (!is_delta(at(t).operand()))
      {
        return false;
      }
      return RewriteTerm(at(t).time_stamp())==sort_real::real_one();
    }
 
    /***************** temporary helper function to compare substitutions ******************/
 
    template <class Expression, class Substitution>
    Expression replace_variables_capture_avoiding_alt(const Expression& e, Substitution& sigma)
    {
      return process::replace_variables_capture_avoiding_with_an_identifier_generator(e, sigma, fresh_identifier_generator);
    }
 
 
    /*****************  retrieve basic objects  ******************/
 
    void detail_check_objectdata(const aterm& o) const
    {
      if (objectdata.count(o)==0)
      {
        if (is_process_identifier(o))
        {
          throw mcrl2::runtime_error("Fail to recognize " + process::pp(process_identifier(o)) + ". Most likely due to unguarded recursion in a process equation. ");
        }
        else
        {
          throw mcrl2::runtime_error("Fail to recognize " + process::pp(o) + ". This is an internal error in the lineariser. ");
        }
      }
    }
    objectdatatype& objectIndex(const aterm& o) 
    {
      detail_check_objectdata(o);
      return objectdata.find(o)->second;
    } 
 
    const objectdatatype& objectIndex(const aterm& o) const
    {
      detail_check_objectdata(o);
      return objectdata.find(o)->second;
    } 
 
    void addString(const identifier_string& str)
    {
      fresh_identifier_generator.add_identifier(str);
    }
 
    process_expression action_list_to_process(const action_list& ma)
    {
      if (ma.size()==0)
      {
        return tau();
      }
      if (ma.size()==1)
      {
        return ma.front();
      }
      return process::sync(ma.front(),action_list_to_process(ma.tail()));
    }
 
    action_list to_action_list(const process_expression& p)
    {
      if (is_tau(p))
      {
        return action_list();
      }
 
      if (is_action(p))
      {
        return action_list({ action(p) });
      }
 
      if (is_sync(p))
      {
        return to_action_list(process::sync(p).left())+to_action_list(process::sync(p).right());
      }
      assert(0);
      return action_list();
    }
 
    process::action_label_list getnames(const process_expression& multiAction)
    {
      if (is_action(multiAction))
      {
        return action_label_list({ action(multiAction).label() });
      }
      assert(is_sync(multiAction));
      return getnames(process::sync(multiAction).left())+getnames(process::sync(multiAction).right());
    }
 
    // Returns a list of variables with the same sort as the expressions in the list.
    // If the expression is a variable not occurring in the occurs_set that variable
    // is used.
    variable_list make_parameters_rec(const data_expression_list& l,
                                      std::set < variable>& occurs_set)
    {
      variable_list result;
      for (const data_expression& e: l)
      {
        /* if the current argument of the multi-action is a variable that does
         not occur in result, use this variable. This is advantageous, when joining
         processes to one linear process where variable names are joined. If this
         is not being done (as happened before 4/1/2008) very long lists of parameters
         can occur when linearising using regular2 */
        if (is_variable(e) && std::find(occurs_set.begin(),occurs_set.end(),e)==occurs_set.end())
        {
          const variable& v = atermpp::down_cast<variable>(e);
          result.push_front(v);
          occurs_set.insert(v);
        }
        else
        {
          result.push_front(variable(get_fresh_variable("a",e.sort())));
        }
      }
      return reverse(result);
    }
 
    variable_list getparameters_rec(const process_expression& multiAction,
                                    std::set < variable>& occurs_set)
    {
      if (is_action(multiAction))
      {
        return make_parameters_rec(action(multiAction).arguments(),occurs_set);
      }
      assert(is_sync(multiAction));
      return getparameters_rec(process::sync(multiAction).left(),occurs_set)+
             getparameters_rec(process::sync(multiAction).right(),occurs_set);
    }
 
    variable_list getparameters(const process_expression& multiAction)
    {
      std::set < variable > occurs_set;
      return getparameters_rec(multiAction,occurs_set);
    }
 
    data_expression_list getarguments(const action_list& multiAction)
    {
      data_expression_list result;
      for (const action& a: multiAction)
      {
        result=reverse(a.arguments()) + result;
      }
      return reverse(result);
    }
 
    action_list makemultiaction(const process::action_label_list& actionIds, const data_expression_list& args)
    {
      action_list result;
      data_expression_list::const_iterator e_walker=args.begin();
      for (const process::action_label& l: actionIds)
      {
        std::size_t arity=l.sorts().size();
        data_expression_list temp_args;
        for (std::size_t i=0 ; i< arity; ++i,++e_walker)
        {
          assert(e_walker!=args.end());
          temp_args.push_front(*e_walker);
        }
        temp_args=reverse(temp_args);
        result.push_front(action(l,temp_args));
      }
      assert(e_walker==args.end());
      return reverse(result);
    }
 
    objectdatatype& addMultiAction(const process_expression& multiAction, bool& isnew)
    {
      const process::action_label_list actionnames=getnames(multiAction);
 
      isnew=(objectdata.count(actionnames)==0);
 
      if (isnew)
      {
        objectdatatype object;
              
        // tempvar is needed as objectdata can change during a call
        // of getparameters.
        const variable_list templist=getparameters(multiAction);
        object.parameters=templist;
        object.object=multiact;
        // must separate assignment below as
        // objectdata may change as a side effect of make
        // multiaction.
        const action_list tempvar=makemultiaction(actionnames, variable_list_to_data_expression_list(object.parameters));
        object.processbody=action_list_to_process(tempvar);
        object.free_variables=std::set<variable>(object.parameters.begin(), object.parameters.end());
        object.free_variables_defined=true;
        
        objectdata[actionnames]=object;
      }
      return objectdata.find(actionnames)->second;
    }
 
    const std::set<variable>& get_free_variables(objectdatatype& object)
    {
      if (!object.free_variables_defined)
      {
        object.free_variables=find_free_variables_process(object.processbody);
        object.free_variables_defined=true;
      }
      return object.free_variables;
    }
 
    void insertvariable(const variable& var, const bool mustbenew)
    {
      addString(var.name());
 
      if (objectdata.count(var.name())>0  && mustbenew)
      {
        throw mcrl2::runtime_error("Variable " + data::pp(var) + " already exists. ");
      }
 
      objectdatatype object;
      object.objectname=var.name();
      object.object=variable_;
      objectdata[var.name()]=object;
    }
 
    void insertvariables(const variable_list& vars, const bool mustbenew)
    {
      for (const variable& v: vars)
      {
        insertvariable(v,mustbenew);
      }
    }
 
    template <class SUBSTITUTION>
    std::set<data::variable> sigma_variables(const SUBSTITUTION& sigma)
    {
      std::set<data::variable> result;
      for (typename SUBSTITUTION::const_iterator i = sigma.begin(); i != sigma.end(); ++i)
      {
        std::set<data::variable> V = data::find_free_variables(i->second);
        V.erase(i->first);
        result.insert(V.begin(), V.end());
      }
      return result;
    }
 
 
    /************ upperpowerof2 *********************************************/
 
    std::size_t upperpowerof2(std::size_t i)
    /* function yields n for the smallest value n such that
       2^n>=i. This constitutes the number of bits necessary
       to represent a number smaller than i. i is assumed to
       be at least 1. */
    {
      std::size_t n=0;
      std::size_t powerof2=1;
      for (; powerof2< i ; n++)
      {
        powerof2=2*powerof2;
      }
      return n;
    }
 
    data_expression RewriteTerm(const data_expression& t)
    {
      if (!options.norewrite)
      {
        if (fresh_equation_added)
        {
          rewr=rewriter(data,options.rewrite_strategy);
          fresh_equation_added=false;
        }
        return rewr(t);
      }
      return t;
    }
 
    data_expression_list RewriteTermList(const data_expression_list& t)
    {
      data_expression_vector v;
      for(const data_expression& d: t)
      {
        v.push_back(RewriteTerm(d));
      }
      return data_expression_list(v.begin(),v.end());
    }
 
    assignment_list rewrite_assignments(const assignment_list& t)
    {
      assignment_vector v;
      for(const assignment& a: t)
      {
        v.push_back(assignment(a.lhs(), RewriteTerm(a.rhs())));
      }
      return assignment_list(v.begin(),v.end());
    }
 
    action RewriteAction(const action& t)
    {
      return action(t.label(),RewriteTermList(t.arguments()));
    }
 
    process_instance_assignment RewriteProcess(const process_instance_assignment& t)
    {
      return process_instance_assignment(t.identifier(),rewrite_assignments(t.assignments()));
    }
 
    process_expression RewriteMultAct(const process_expression& t)
    {
      if (is_tau(t))
      {
        return t;
      }
 
      if (is_action(t))
      {
        return RewriteAction(action(t));
      }
 
      assert(is_sync(t));  // A multi action is a sequence of actions with a sync operator in between.
      return process::sync(RewriteMultAct(process::sync(t).left()),RewriteMultAct(process::sync(t).right()));
    }
 
 
    process_expression pCRLrewrite(const process_expression& t)
    {
      if (options.norewrite)
      {
        return t;
      }
 
      if (is_if_then(t))
      {
        const data_expression new_cond=RewriteTerm(down_cast<if_then>(t).condition());
        const process_expression new_then_case=pCRLrewrite(down_cast<if_then>(t).then_case());
        if (new_cond==sort_bool::true_())
        {
          return new_then_case;
        }
        return if_then(new_cond,new_then_case);
      }
 
      if (is_seq(t))
      {
        /* only one summand is needed */
        return seq(
                 pCRLrewrite(seq(t).left()),
                 pCRLrewrite(seq(t).right()));
      }
 
      if (is_at(t))
      {
        const data_expression& atTime=RewriteTerm(down_cast<at>(t).time_stamp());
        const process_expression t1=pCRLrewrite(down_cast<at>(t).operand());
        return at(t1,atTime);
      }
 
      if (is_stochastic_operator(t))
      {
        const stochastic_operator& sto=atermpp::down_cast<const stochastic_operator>(t);
        return stochastic_operator(sto.variables(),RewriteTerm(sto.distribution()),pCRLrewrite(sto.operand()));
      }
 
      if (is_delta(t) || is_tau(t))
      {
        return t;
      }
 
      if (is_action(t))
      {
        return RewriteAction(atermpp::down_cast<process::action>(t));
      }
 
      if (is_process_instance_assignment(t))
      {
        return RewriteProcess(process_instance_assignment(t));
      }
 
      if (is_sync(t))
      {
        return RewriteMultAct(t);
      }
 
      assert(0); // Expected a term in pCRL format, using only basic process operators.
      return t;
    }
 
    /************ storeact ****************************************************/
 
    objectdatatype& insertAction(const action_label& actionId)
    {
      if (objectdata.count(actionId)>0)
      {
        throw mcrl2::runtime_error("Action " + process::pp(actionId) + " is added twice. This is an internal error in the lineariser. Please report. ");
      }
 
      const identifier_string& str=actionId.name();
      addString(str);
 
      objectdatatype object;
      object.objectname=str;
      object.object=act;
      object.process_representing_action=process_identifier();
      
      objectdata[actionId]=object;
      return objectdata.find(actionId)->second;
    }
 
    void storeact(const process::action_label_list& acts)
    {
      for (const process::action_label& l: acts)
      {
        insertAction(l);
      }
    }
 
    /************ storeprocs *************************************************/
 
    objectdatatype& insert_process_declaration(
      const process_identifier& procId, 
      const variable_list& parameters,  
      const process_expression& body,
      processstatustype s,
      const bool canterminate,
      const bool containstime)
    {
      assert(procId.variables().size()==parameters.size());
      const std::string str=procId.name();
      addString(str);
 
      if (objectdata.count(procId)>0)
      {
        throw mcrl2::runtime_error("Process " + process::pp(procId) + " is added twice. This is an internal error in the lineariser. Please report. ");
      }
 
      objectdatatype object;
      object.objectname=procId.name();
      object.object=proc;
      object.processbody=body;
      object.free_variables_defined=false;
      object.canterminate=canterminate;
      object.containstime=containstime;
      object.processstatus=s;
      object.parameters=parameters;
      insertvariables(parameters,false);
      objectdata[procId]=object;
      return objectdata.find(procId)->second;
    }
 
    void storeprocs(const std::vector< process_equation >& procs)
    {
      for (const process_equation& e: procs)
      {
        insert_process_declaration(
          e.identifier(),
          e.formal_parameters(),
          e.expression(),
          unknown,0,false);
      }
    }
 
    bool searchProcDeclaration(
      const variable_list& parameters,
      const process_expression& body,
      const processstatustype s,
      const bool canterminate,
      const bool containstime,
      process_identifier& p)
    {
      for(const std::pair<const aterm,objectdatatype>& d: objectdata)
      {
        if (d.second.object==proc &&
            d.second.parameters==parameters &&
            d.second.processbody==body &&
            d.second.canterminate==canterminate &&
            d.second.containstime==containstime &&
            d.second.processstatus==s)
        {
          p=process_identifier(d.second.objectname,d.second.parameters);
          return true;
        }
      }
      return false;
    }
 
 
    /************ storeinit *************************************************/
 
  public:
    process_identifier storeinit(const process_expression& init)
    {
      /* init is used as the name of the initial process,
         because it cannot occur as a string in the input */
 
      process_identifier initprocess(std::string("init"), variable_list());
      insert_process_declaration(initprocess,variable_list(),init,unknown,0,false);
      return initprocess;
    }
 
  private:
 
    /********** various functions on action and multi actions  ***************/
    bool actioncompare(const action_label& a1, const action_label& a2)
    {
      /* first compare the strings in the actions */
      if (std::string(a1.name())<std::string(a2.name()))
      {
        return true;
      }
 
      if (a1.name()==a2.name())
      {
        /* the strings are equal; the sorts are used to
           determine the ordering */
        return a1.sorts()<a2.sorts();
      }
 
      return false;
    }
 
    action_list linInsertActionInMultiActionList(
      const action& act,
      action_list multiAction)
    {
      /* store the action in the multiAction, alphabetically
         sorted on the actionname in the actionId. Note that
         the empty multiAction represents tau. */
 
      if (multiAction.empty())
      {
        return action_list({ act });
      }
      const action firstAction=multiAction.front();
 
      /* Actions are compared on the basis of their position
         in memory, to order them. As the aterm library maintains
         pointers to objects that are not garbage collected, this
         is a safe way to do this. */
      if (actioncompare(act.label(),firstAction.label()))
      {
        multiAction.push_front(act);
        return multiAction;
      }
      action_list result= linInsertActionInMultiActionList(
                          act,
                          multiAction.tail());
      result.push_front(firstAction);
      return result;
    }
 
    action_list linMergeMultiActionList(const action_list& ma1, const action_list& ma2)
    {
      action_list result=ma2;
      for (const action& a: ma1) 
      {
        result=linInsertActionInMultiActionList(a,result);
      }
      return result;
    }
 
 
    action_list linMergeMultiActionListProcess(const process_expression& ma1, const process_expression& ma2)
    {
      return linMergeMultiActionList(to_action_list(ma1),to_action_list(ma2));
    }
 
    /************** determine_process_status ********************************/
 
    processstatustype determine_process_statusterm(
      const process_expression& body,  // intentionally not a reference.
      const processstatustype status)
    {
      /* In this procedure it is determined whether a process
         is of type mCRL, pCRL or a multiAction. pCRL processes
         occur strictly within mCRL processes, and multiActions
         occur strictly within pCRL processes. Processes that pass
         this procedure can be linearised. Bounded initialisation,
         the leftmerge and synchronization merge on the highest
         level are filtered out. */
      if (is_choice(body))
      {
        if (status==multiAction)
        {
          throw mcrl2::runtime_error("Choice operator occurs in a multi-action in " + process::pp(body) + ". The lineariser cannot handle such a pattern. ");
        }
        const processstatustype s1=determine_process_statusterm(choice(body).left(),pCRL);
        const processstatustype s2=determine_process_statusterm(choice(body).right(),pCRL);
        if ((s1==mCRL)||(s2==mCRL))
        {
          throw mcrl2::runtime_error("An operator ||, allow, hide, rename, or comm occurs within the scope of a choice operator in " + process::pp(body) +
                                      ". The lineariser cannot handle such processes. ");
        }
        return pCRL;
      }
 
      if (is_seq(body))
      {
        if (status==multiAction)
        {
          throw mcrl2::runtime_error("Sequential operator occurs in a multi-action in " + process::pp(body) +". The lineariser cannot handle such a pattern. ");
        }
        const processstatustype s1=determine_process_statusterm(seq(body).left(),pCRL);
        const processstatustype s2=determine_process_statusterm(seq(body).right(),pCRL);
        if ((s1==mCRL)||(s2==mCRL))
        {
          throw mcrl2::runtime_error("An operator ||, allow, hide, rename, or comm occurs in the scope of a sequential operator in " + process::pp(body) +". "
                                       + "The lineariser cannot handle such processes. ");
        }
        return pCRL;
      }
 
      if (is_merge(body))
      {
        if (status!=mCRL)
        {
          throw mcrl2::runtime_error("The parallel operator occurs in the scope of recursion, or the condition, sequential or choice operator in " +
                                      process::pp(body) + ". The lineariser cannot handle such processes. ");
        }
        determine_process_statusterm(process::merge(body).left(),mCRL);
        determine_process_statusterm(process::merge(body).right(),mCRL);
        return mCRL;
      }
 
      if (is_left_merge(body))
      {
        throw mcrl2::runtime_error("Cannot linearise because the specification contains a leftmerge. ");
      }
 
      if (is_if_then(body))
      {
        if (status==multiAction)
        {
          throw mcrl2::runtime_error("If-then occurs in a multi-action in " + process::pp(body) + ". The lineariser cannot linearise this. ");
        }
        const processstatustype s1=determine_process_statusterm(if_then(body).then_case(),pCRL);
        if (s1==mCRL)
        {
          throw mcrl2::runtime_error("An operator ||, allow, hide, rename, or comm occurs in the scope of the if-then operator in " + process::pp(body) + ". "
                                     + "The lineariser cannot handle such processes. ");
        }
        return pCRL;
      }
 
      if (is_if_then_else(body))
      {
        if (status==multiAction)
        {
          throw mcrl2::runtime_error("If-then-else occurs in a multi-action in " + process::pp(body) +".");
        }
        const processstatustype s1=determine_process_statusterm(if_then_else(body).then_case(),pCRL);
        const processstatustype s2=determine_process_statusterm(if_then_else(body).else_case(),pCRL);
        if ((s1==mCRL)||(s2==mCRL))
        {
          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) +
                                     ". " + "The lineariser cannot handle such processes. ");
        }
        return pCRL;
      }
 
      if (is_sum(body))
      {
        /* insert the variable names of variables, to avoid
           that this variable name will be reused later on */
        insertvariables(sum(body).variables(),false);
        if (status==multiAction)
        {
          throw mcrl2::runtime_error("The sum operator occurs within a multi-action in " + process::pp(body) + ". "
                                      + "The lineariser cannot handle such processes. ");
        }
        const processstatustype s1=determine_process_statusterm(sum(body).operand(),pCRL);
        if (s1==mCRL)
        {
          throw mcrl2::runtime_error("An operator ||, allow, hide, rename, or comm occurs in the scope of the sum operator in " + process::pp(body) + ". "
                                     "The lineariser cannot handle such processes. ");
        }
        return pCRL;
      }
 
      if (is_stochastic_operator(body))
      {
        stochastic_operator_is_being_used=true;
        /* insert the variable names of variables, to avoid
           that this variable name will be reused later on */
        const stochastic_operator& sto=down_cast<const stochastic_operator>(body);
        insertvariables(sto.variables(),false);
        if (status==multiAction)
        {
          throw mcrl2::runtime_error("Stochastic operator occurs within a multi-action in " + process::pp(body) +".");
        }
        const processstatustype s1=determine_process_statusterm(sto.operand(),pCRL);
        if (s1==mCRL)
        {
          throw mcrl2::runtime_error("An operator ||, allow, hide, rename, or comm occurs in the scope of the stochastic operator in " + process::pp(body) + ". "
                                     + "The lineariser cannot handle such processes. ");
        }
        return s1;
      }
 
      if (is_comm(body))
      {
        if (status!=mCRL)
        {
          throw mcrl2::runtime_error("The communication operator occurs in the scope of recursion, the condition, the sequential operation or the choice in "
                                      + process::pp(body) + ". The lineariser cannot linearise such processes. ");
        }
        determine_process_statusterm(comm(body).operand(),mCRL);
        return mCRL;
      }
 
      if (is_bounded_init(body))
      {
        throw mcrl2::runtime_error("Cannot linearise a specification with the bounded initialization operator.");
      }
 
      if (is_at(body))
      {
        timeIsBeingUsed = true;
        if (status==multiAction)
        {
          throw mcrl2::runtime_error("Time operator occurs in a multi-action in " + process::pp(body) +".");
        }
        const processstatustype s1=determine_process_statusterm(at(body).operand(),pCRL);
        if (s1==mCRL)
        {
          throw mcrl2::runtime_error("An operator ||, allow, hide, rename, or comm occurs in the scope of a time operator in " + process::pp(body) + "."
                                     + "The lineariser cannot handle such processes. ");
        }
        return pCRL;
      }
 
      if (is_sync(body))
      {
        const processstatustype s1=determine_process_statusterm(process::sync(body).left(),pCRL);
        const processstatustype s2=determine_process_statusterm(process::sync(body).right(),pCRL);
        if ((s1!=multiAction)||(s2!=multiAction))
        {
          throw mcrl2::runtime_error("Other objects than multi-actions occur in the scope of a synch operator in " + process::pp(body) +".");
        }
        return multiAction;
      }
 
      if (is_action(body))
      {
        return multiAction;
      }
 
      if (is_process_instance_assignment(body))
      {
        determine_process_status(process_instance_assignment(body).identifier(),status);
        return status;
      }
 
      if (is_delta(body))
      {
        return pCRL;
      }
 
      if (is_tau(body))
      {
        return multiAction;
      }
 
      if (is_hide(body))
      {
        if (status!=mCRL)
        {
          throw mcrl2::runtime_error("A hide operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +".");
        }
        determine_process_statusterm(hide(body).operand(),mCRL);
        return mCRL;
      }
 
      if (is_rename(body))
      {
        if (status!=mCRL)
        {
          throw mcrl2::runtime_error("A rename operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +".");
        }
        determine_process_statusterm(process::rename(body).operand(),mCRL);
        return mCRL;
      }
 
      if (is_allow(body))
      {
        if (status!=mCRL)
        {
          throw mcrl2::runtime_error("An allow operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +".");
        }
        determine_process_statusterm(allow(body).operand(),mCRL);
        return mCRL;
      }
 
      if (is_block(body))
      {
        if (status!=mCRL)
        {
          throw mcrl2::runtime_error("A block operator occurs in the scope of recursion, or a condition, choice or sequential operator in " + process::pp(body) +".");
        }
        determine_process_statusterm(block(body).operand(),mCRL);
        return mCRL;
      }
 
      throw mcrl2::runtime_error("Process has unexpected format (2) " + process::pp(body) +".");
      return error;
    }
 
 
    void determine_process_status(
      const process_identifier& procDecl,
      const processstatustype status)
    {
      processstatustype s;
      objectdatatype& object=objectIndex(procDecl);
      s=object.processstatus;
 
      if (s==unknown)
      {
        object.processstatus=status;
        if (status==pCRL)
        {
          determine_process_statusterm(object.processbody,pCRL);
          return;
        }
        /* status==mCRL */
        s=determine_process_statusterm(object.processbody,mCRL);
        if (s!=status)
        {
          /* s==pCRL and status==mCRL */
          object.processstatus=s;
          determine_process_statusterm(object.processbody,pCRL);
        }
      }
      if (s==mCRL)
      {
        if (status==pCRL)
        {
          object.processstatus=pCRL;
          determine_process_statusterm(object.processbody,pCRL);
        }
      }
    }
 
    /***********  collect pcrlprocessen **********************************/
 
    void collectPcrlProcesses_term(const process_expression& body,  // Intentionally not a reference.
                                   std::vector <process_identifier>& pcrlprocesses,
                                   std::set <process_identifier>& visited)
    {
      if (is_if_then(body))
      {
        collectPcrlProcesses_term(if_then(body).then_case(),pcrlprocesses,visited);
        return;
      }
 
      if (is_if_then_else(body))
      {
        collectPcrlProcesses_term(if_then_else(body).then_case(),pcrlprocesses,visited);
        collectPcrlProcesses_term(if_then_else(body).else_case(),pcrlprocesses,visited);
        return;
      }
 
      if (is_choice(body))
      {
        collectPcrlProcesses_term(choice(body).left(),pcrlprocesses,visited);
        collectPcrlProcesses_term(choice(body).right(),pcrlprocesses,visited);
        return ;
      }
 
      if (is_seq(body))
      {
        collectPcrlProcesses_term(seq(body).left(),pcrlprocesses,visited);
        collectPcrlProcesses_term(seq(body).right(),pcrlprocesses,visited);
        return ;
      }
 
      if (is_merge(body))
      {
        collectPcrlProcesses_term(process::merge(body).left(),pcrlprocesses,visited);
        collectPcrlProcesses_term(process::merge(body).right(),pcrlprocesses,visited);
        return ;
      }
 
      if (is_sync(body))
      {
        collectPcrlProcesses_term(process::sync(body).left(),pcrlprocesses,visited);
        collectPcrlProcesses_term(process::sync(body).right(),pcrlprocesses,visited);
        return ;
      }
 
      if (is_sum(body))
      {
        collectPcrlProcesses_term(sum(body).operand(),pcrlprocesses,visited);
        return;
      }
 
      if (is_stochastic_operator(body))
      {
        collectPcrlProcesses_term(stochastic_operator(body).operand(),pcrlprocesses,visited);
        return;
      }
 
      if (is_at(body))
      {
        collectPcrlProcesses_term(at(body).operand(),pcrlprocesses,visited);
        return;
      }
 
      if (is_process_instance_assignment(body))
      {
        collectPcrlProcesses(process_instance_assignment(body).identifier(),pcrlprocesses,visited);
        return;
      }
 
      if (is_hide(body))
      {
        collectPcrlProcesses_term(hide(body).operand(),pcrlprocesses,visited);
        return;
      }
 
      if (is_rename(body))
      {
        collectPcrlProcesses_term(process::rename(body).operand(),pcrlprocesses,visited);
        return;
      }
 
      if (is_allow(body))
      {
        collectPcrlProcesses_term(allow(body).operand(),pcrlprocesses,visited);
        return;
      }
 
      if (is_block(body))
      {
        collectPcrlProcesses_term(block(body).operand(),pcrlprocesses,visited);
        return;
      }
 
      if (is_comm(body))
      {
        collectPcrlProcesses_term(comm(body).operand(),pcrlprocesses,visited);
        return;
      }
 
      if ((is_delta(body))||
          (is_tau(body))||
          (is_action(body)))
      {
        return;
      }
 
      throw mcrl2::runtime_error("process has unexpected format (1) " + process::pp(body) +".");
    }
 
    void collectPcrlProcesses(
      const process_identifier& procDecl,
      std::vector <process_identifier>& pcrlprocesses,
      std::set <process_identifier>& visited)
    {
      if (visited.count(procDecl)==0)
      {
        visited.insert(procDecl);
        objectdatatype& object=objectIndex(procDecl);
        if (object.processstatus==pCRL)
        {
          pcrlprocesses.push_back(procDecl);
        }
        collectPcrlProcesses_term(object.processbody,pcrlprocesses,visited);
      }
    }
 
    void collectPcrlProcesses(
      const process_identifier& procDecl,
      std::vector <process_identifier>& pcrlprocesses)
    {
      std::set <process_identifier> visited;
      collectPcrlProcesses(procDecl, pcrlprocesses, visited);
    }
 
    /****************  occursinterm *** occursintermlist ***********/
 
    bool occursinterm(const variable& var, const data_expression& t) const
    {
      return data::search_free_variable(t, var);
    }
 
    void filter_vars_by_term(
      const data_expression& t,
      const std::set < variable >& vars_set,
      std::set < variable >& vars_result_set)
    {
      if (is_variable(t))
      {
        const variable& v = atermpp::down_cast<variable>(t);
        if (vars_set.find(v)!=vars_set.end())
        {
          vars_result_set.insert(v);
        }
        return;
      }
 
      if (is_function_symbol(t))
      {
        return;
      }
 
      if (is_machine_number(t))
      {
        return;
      }
 
      if (is_abstraction(t))
      {
        // mCRL2log(mcrl2::log::warning) << "filtering of variables expression with binders" << std::endl;
        return;
      }
 
      if (is_where_clause(t))
      {
        // mCRL2log(mcrl2::log::warning) << "filtering of variables expression with where clause" << std::endl;
        return;
      }
 
      if (!is_application(t))
      {
        mCRL2log(mcrl2::log::error) << "term of unexpected type " << t << std::endl;
      }
 
      assert(is_application(t));
 
      const application& a=atermpp::down_cast<const application>(t);
      filter_vars_by_term(a.head(),vars_set,vars_result_set);
      filter_vars_by_termlist(a.begin(),a.end(),vars_set,vars_result_set);
    }
 
    bool occursintermlist(const variable& var, const data_expression_list& r) const
    {
      for (const data_expression& d: r)
      {
        if (occursinterm(var,d))
        {
          return true;
        }
      }
      return false;
    }
 
    bool occursintermlist(const variable& var, const assignment_list& r, const process_identifier& proc_name) const
    {
      std::set<variable> assigned_variables;
      for (const assignment& l: r)
      {
        if (occursinterm(var,l.rhs()))
        {
          return true;
        }
       assigned_variables.insert(l.lhs());
      }
      // Check whether x does not occur in the assignment list. Then variable x is assigned to
      // itself, and it occurs in the process.
      for (const variable& v: objectIndex(proc_name).parameters)
      {
        if (var==v)
        {
          if (assigned_variables.count(var)==0) // This variable is not assigned, so it does occur!
          {
            return true;
          }
        }
      }
      return false;
    }
 
    template <typename Iterator>
    void filter_vars_by_termlist(
      Iterator begin,
      const Iterator& end,
      const std::set < variable >& vars_set,
      std::set < variable >& vars_result_set)
    {
      for (; begin != end; ++begin)
      {
        filter_vars_by_term(*begin,vars_set,vars_result_set);
      }
    }
 
    void filter_vars_by_multiaction(
      const action_list& multiaction,
      const std::set < variable >& vars_set,
      std::set < variable >& vars_result_set)
    {
      for (const action& ma: multiaction)
      {
        filter_vars_by_termlist(ma.arguments().begin(), ma.arguments().end(),vars_set,vars_result_set);
      }
      return;
    }
 
    void filter_vars_by_assignmentlist(
      const assignment_list& assignments,
      const variable_list& parameters,
      const std::set < variable >& vars_set,
      std::set < variable >& vars_result_set)
    {
      const data_expression_list& l=atermpp::container_cast<data_expression_list>(parameters);
      filter_vars_by_termlist(l.begin(),l.end(),vars_set,vars_result_set);
      for (const assignment& a: assignments)
      {
        filter_vars_by_term(a.rhs(),vars_set,vars_result_set);
      }
    }
 
    bool occursinpCRLterm(const variable& var,
                          const process_expression& p,
                          const bool strict)
    {
      if (is_choice(p))
      {
        return occursinpCRLterm(var,choice(p).left(),strict)||
               occursinpCRLterm(var,choice(p).right(),strict);
      }
      if (is_seq(p))
      {
        return occursinpCRLterm(var,seq(p).left(),strict)||
               occursinpCRLterm(var,seq(p).right(),strict);
      }
      if (is_if_then(p))
      {
        return occursinterm(var,if_then(p).condition())||
               occursinpCRLterm(var,if_then(p).then_case(),strict);
      }
 
      if (is_sum(p))
      {
        if (strict)
          return occursintermlist(var,variable_list_to_data_expression_list(sum(p).variables())) ||
                 occursinpCRLterm(var,sum(p).operand(),strict);
        /* below appears better? , but leads
           to errors. Should be investigated. */
        else
          return
            (!occursintermlist(var,variable_list_to_data_expression_list(sum(p).variables()))) &&
            occursinpCRLterm(var,sum(p).operand(),strict);
      }
      if (is_stochastic_operator(p))
      {
        const stochastic_operator& sto=atermpp::down_cast<const stochastic_operator>(p);
        if (strict)
        {
          return occursintermlist(var,variable_list_to_data_expression_list(sto.variables())) ||
                      occursinterm(var,sto.distribution()) ||
                      occursinpCRLterm(var,sto.operand(),strict);
        }
        else
        {
          return (!occursintermlist(var,variable_list_to_data_expression_list(sto.variables()))) &&
                      (occursinterm(var,sto.distribution()) ||
                       occursinpCRLterm(var,sto.operand(),strict));
        }
      }
      if (is_process_instance_assignment(p))
      {
        return occursintermlist(var,process_instance_assignment(p).assignments(),process_instance_assignment(p).identifier());
      }
      if (is_action(p))
      {
        return occursintermlist(var,action(p).arguments());
      }
      if (is_sync(p))
      {
        return occursinpCRLterm(var,process::sync(p).left(),strict)||
               occursinpCRLterm(var,process::sync(p).right(),strict);
      }
      if (is_at(p))
      {
        return occursinterm(var,at(p).time_stamp()) ||
               occursinpCRLterm(var,at(p).operand(),strict);
      }
      if (is_delta(p))
      {
        return false;
      }
      if (is_tau(p))
      {
        return false;
      }
      throw mcrl2::runtime_error("unexpected process format in occursinCRLterm " + process::pp(p));
      return false;
    }
 
    template <class MutableSubstitution>
    void alphaconvertprocess(
      variable_list& sumvars,
      MutableSubstitution& sigma,
      const process_expression& p)
    {
      /* This function replaces the variables in sumvars
         by unique ones if these variables occur in the process expression p.
         The substitution sigma contains the renaming. */
      variable_vector newsumvars;
 
      for (const variable& var: sumvars)
      {
        if (occursinpCRLterm(var,p,true))
        {
          const variable newvar=get_fresh_variable(var.name(),var.sort());
          newsumvars.push_back(newvar);
          sigma[var]=newvar;
        }
        else
        {
          newsumvars.push_back(var);
        }
      }
      sumvars=variable_list(newsumvars.begin(), newsumvars.end());
    }
 
    template <class MutableSubstitution>
    void alphaconvert(
      variable_list& sumvars,
      MutableSubstitution& sigma,
      const variable_list& occurvars,
      const data_expression_list& occurterms)
    {
      /* This function replaces the variables in sumvars
         by unique ones if these variables occur in occurvars
         or occurterms. It extends rename_vars and rename
         terms to rename the replaced variables to new ones. */
      variable_list newsumvars;
 
      for (const variable& var: sumvars)
      {
        if (occursintermlist(var,variable_list_to_data_expression_list(occurvars)) ||
            occursintermlist(var,occurterms))
        {
          const variable newvar=get_fresh_variable(var.name(),var.sort());
          newsumvars.push_front(newvar);
          sigma[var]=newvar;
        }
        else
        {
          newsumvars.push_front(var);
        }
      }
      sumvars=reverse(newsumvars);
    }
 
    /******************* find_free_variables_process *****************************************/
 
 
    /* We define our own variant of the standard function find_free_variables, because
       find_free_variables is not correctly defined on processes, due to process_instance_assignments,
       where variables can occur by not being mentioned. It is necessary to know the parameters of
       a process to retrieve these. Concrete example in P() defined by P(x:Nat)= ..., the variable x
       appears as a free variable, although it is not explicitly mentioned.
       If the standard function find_free_variable on processes is repaired, this function can
       be removed */
    void find_free_variables_process(const process_expression& p, std::set< variable >& free_variables_in_p)
    {
      if (is_choice(p))
      {
         find_free_variables_process(choice(p).left(),free_variables_in_p);
         find_free_variables_process(choice(p).right(),free_variables_in_p);
         return;
      }
      if (is_seq(p))
      {
        find_free_variables_process(seq(p).left(),free_variables_in_p);
        find_free_variables_process(seq(p).right(),free_variables_in_p);
        return;
      }
      if (is_sync(p))
      {
        find_free_variables_process(process::sync(p).left(),free_variables_in_p);
        find_free_variables_process(process::sync(p).right(),free_variables_in_p);
        return;
      }
      if (is_if_then(p))
      {
        for(const variable& v: find_free_variables(if_then(p).condition())) 
        {
          free_variables_in_p.insert(v);
        }
        find_free_variables_process(if_then(p).then_case(),free_variables_in_p);
        return;
      }
      if (is_if_then_else(p))
      {
        for(const variable& v: find_free_variables(if_then(p).condition()))
        {
          free_variables_in_p.insert(v);
        }
        find_free_variables_process(if_then_else(p).then_case(),free_variables_in_p);
        find_free_variables_process(if_then_else(p).else_case(),free_variables_in_p);
        return;
      }
 
      if (is_sum(p))
      {
        find_free_variables_process(sum(p).operand(),free_variables_in_p);
 
        for(const variable& v: static_cast<const sum&>(p).variables())
        {
          free_variables_in_p.erase(v);
        }
        return;
      }
 
      if (is_stochastic_operator(p))
      {
        const stochastic_operator& sto=down_cast<const stochastic_operator>(p);
        find_free_variables_process(sto.operand(),free_variables_in_p);
        for(const variable& v: find_free_variables(sto.distribution()))
        {
          free_variables_in_p.insert(v);
        }
 
        for(const variable& v: sto.variables())
        {
          free_variables_in_p.erase(v);
        }
        return;
      }
 
      if (is_process_instance(p))
      {
        const process_instance q = atermpp::down_cast<process_instance>(p);
        for(const variable& v: find_free_variables(q.actual_parameters()))
        {
          free_variables_in_p.insert(v);
        }
        return;
      }
      if (is_process_instance_assignment(p))
      {
        const process_instance_assignment q(p);
        objectdatatype& object=objectIndex(q.identifier());
        const variable_list parameters=object.parameters;
        std::set<variable> parameter_set(parameters.begin(),parameters.end());
        const assignment_list& assignments=q.assignments();
        for(const assignment& a: assignments)
        {
          for(const variable& v: find_free_variables(a.rhs()))
          {
            free_variables_in_p.insert(v);
          }
          parameter_set.erase(a.lhs());
        }
        // Add all remaining variables in the parameter_set, as they have an identity assignment.
        for(const variable& v: parameter_set)
        {
          free_variables_in_p.insert(v);
        }
        return;
      }
 
      if (is_action(p))
      {
        for(const variable& v: process::find_free_variables(p))
        {
          free_variables_in_p.insert(v);
        }
        return;
      }
 
      if (is_at(p))
      {
        for(const variable& v: data::find_free_variables(at(p).time_stamp()))
        {
          free_variables_in_p.insert(v);
        }
        find_free_variables_process(at(p).operand(),free_variables_in_p);
        return;
      }
 
      if (is_delta(p))
      {
        return;
      }
 
      if (is_tau(p))
      {
        return;
      }
 
      if (is_sync(p))
      {
        find_free_variables_process(process::sync(p).left(),free_variables_in_p);
        find_free_variables_process(process::sync(p).right(),free_variables_in_p);
        return;
      }
 
      if (is_left_merge(p))
      {
        find_free_variables_process(process::left_merge(p).left(),free_variables_in_p);
        find_free_variables_process(process::left_merge(p).right(),free_variables_in_p);
        return;
      }
 
      if (is_merge(p))
      {
        find_free_variables_process(process::merge(p).left(),free_variables_in_p);
        find_free_variables_process(process::merge(p).right(),free_variables_in_p);
        return;
      }
 
      if (is_allow(p))
      {
        find_free_variables_process(process::allow(p).operand(),free_variables_in_p);
        return;
      }
 
      if (is_comm(p))
      {
        find_free_variables_process(process::comm(p).operand(),free_variables_in_p);
        return;
      }
 
      if (is_block(p))
      {
        find_free_variables_process(process::block(p).operand(),free_variables_in_p);
        return;
      }
 
      if (is_hide(p))
      {
        find_free_variables_process(process::hide(p).operand(),free_variables_in_p);
        return;
      }
 
      if (is_rename(p))
      {
        find_free_variables_process(process::rename(p).operand(),free_variables_in_p);
        return;
      }
 
      throw mcrl2::runtime_error("Internal error: expect a pCRL process (1) " + process::pp(p));
    }
 
    std::set< variable > find_free_variables_process(const process_expression& p)
    {
      std::set<variable> free_variables_in_p;
      find_free_variables_process(p,free_variables_in_p);
      return free_variables_in_p;
    }
 
    /* Remove assignments that do not appear in the parameter list. */
    assignment_list filter_assignments(const assignment_list& assignments, const variable_list& parameters)
    {
      assignment_vector result;
      for(const assignment& a: assignments)
      {
        if (std::find(parameters.begin(),parameters.end(),a.lhs())!=parameters.end())   // found.
        {
          result.push_back(a);
        }
      }
      return assignment_list(result.begin(),result.end());
    }
 
    /* Check whether the assignments occur in the same order in the list of parameters */
    static bool check_assignment_list(
              const assignment_list& assignments,
              const variable_list& parameters)
    {
      assignment_list::iterator i=assignments.begin();
      for(const variable& v: parameters)
      {
        if (i!=assignments.end() && v==i->lhs())
        {
          ++i;
        }
      }
      return i==assignments.end();
 
    }
 
    /******************* substitute *****************************************/
 
 
    template <class Substitution>
    assignment_list substitute_assignmentlist(
      const assignment_list& assignments,
      const variable_list& parameters,
      const bool replacelhs,
      const bool replacerhs,
      Substitution& sigma)
    {
      assert(check_assignment_list(assignments, parameters));
      /* precondition: the variables in the assignment occur in
         the same sequence as in the parameters, which stands for the
         total list of parameters.
 
         This function replaces the variables in vars by the terms in terms
         in the right hand side of the assignments if replacerhs holds, and
         in the lefthandside of an assignment if replacelhs holds. If for some variable
         occuring in the parameterlist no assignment is present, whereas
         this variable occurs in vars, an assignment for it is added.
 
         It is not possible to use standard substitution functions to replace substitute_assignmentlis
         because they do not take the parameters of processes into account.
         For instance consider a process P(b:D)=... of which an instance P() exists.
         If the substitution sigma(b)=t is applied to P() the result should be P(b=t).
         The standard substitutions do not take this parameterlist into account, as it stands.
      */
 
      assert(replacelhs==0 || replacelhs==1);
      assert(replacerhs==0 || replacerhs==1);
      if (parameters.empty())
      {
        assert(assignments.empty());
        return assignments;
      }
 
      const variable& parameter=parameters.front();
 
      if (!assignments.empty())
      {
        const assignment& ass=assignments.front();
        variable lhs=ass.lhs();
        if (parameter==lhs)
        {
          /* The assignment refers to parameter par. Substitute its
             left and righthandside */
          data_expression rhs=ass.rhs();
 
          if (replacelhs)
          {
            lhs = atermpp::down_cast<variable>(sigma(lhs));
          }
          if (replacerhs)
          {
            rhs=/* data::*/replace_variables_capture_avoiding_alt(rhs,sigma);
          }
 
          assignment_list result=
                   substitute_assignmentlist(
                     assignments.tail(),
                     parameters.tail(),
                     replacelhs,
                     replacerhs,
                     sigma);
          result.push_front(assignment(lhs,rhs));
          return result;
        }
      }
 
      /* Here the first parameter is not equal to the first
         assignment. So, we must find out whether a value
         for this variable is substituted, that is different
         from the variable, in which case an assignment must
         be added. */
 
      variable lhs=parameter;
      data_expression rhs=parameter;
 
      if (replacelhs)
      {
        lhs = atermpp::down_cast<data::variable>(sigma(lhs));
      }
      if (replacerhs)
      {
        rhs=/* data::*/replace_variables_capture_avoiding_alt(rhs,sigma);
      }
 
      if (lhs==rhs)
      {
        return substitute_assignmentlist(
                 assignments,
                 parameters.tail(),
                 replacelhs,
                 replacerhs,
                 sigma);
      }
      assignment_list result=
               substitute_assignmentlist(
                 assignments,
                 parameters.tail(),
                 replacelhs,
                 replacerhs,
                 sigma);
      result.push_front(assignment(lhs,rhs));
      return result;
    }
 
    // Sort the assignments, such that they have the same order as the parameters
    assignment_list sort_assignments(const assignment_list& ass, const variable_list& parameters)
    {
      std::map<variable,data_expression>assignment_map;
      for(const assignment& a: ass)
      {
        assignment_map[a.lhs()]=a.rhs();
      }
 
      assignment_vector result;
      for(const variable& v: parameters)
      {
        const std::map<variable,data_expression>::const_iterator j=assignment_map.find(v);
        if (j!=assignment_map.end()) // found
        {
          result.push_back(assignment(j->first,j->second));
        }
      }
      return assignment_list(result.begin(),result.end());
    }
 
    bool check_valid_process_instance_assignment(
               const process_identifier& id,
               const assignment_list& assignments)
    {
      objectdatatype& object=objectIndex(id);
      variable_list parameters=object.parameters;
      for(const assignment& a: assignments)
      {
        // Every assignment must occur in the parameter list, in the right sequence.
 
        variable v;
        do
        {
          if (parameters.empty())
          {
            return false;
          }
          v=parameters.front();
          parameters.pop_front();
        }
        while (v!=a.lhs());
 
      }
      return true;
    }
 
    /* The function below calculates sigma(p) and replaces
       all variables that are bound by a sum in p by unique
       variables */
 
   
    /* The function below cannot be replace by replace_variables_capture_avoiding although
     * the interfaces are the same. As yet it is unclear why, but the difference shows itself
     * for instance when linearising lift3_final.mcrl2 and lift3_init.mcrl2 */
    template <class Substitution>
    process_expression substitute_pCRLproc(
      const process_expression& p,
      Substitution& sigma)
    {
      if (is_choice(p))
      {
        process_expression left=substitute_pCRLproc(choice(p).left(),sigma);
        if (left==delta_at_zero())
        {
          return substitute_pCRLproc(choice(p).right(),sigma);
        }
        process_expression right=substitute_pCRLproc(choice(p).right(),sigma);
        if (right==delta_at_zero())
        {
          return left;
        }
        return choice(left,right);
      }
      if (is_seq(p))
      {
        process_expression q=substitute_pCRLproc(seq(p).left(),sigma);
        if (q==delta_at_zero())
        { 
          return q;
        }
        return seq(q, substitute_pCRLproc(seq(p).right(),sigma));
      }
      if (is_sync(p))
      {
        return process::sync(
                 substitute_pCRLproc(process::sync(p).left(),sigma),
                 substitute_pCRLproc(process::sync(p).right(),sigma));
      }
      if (is_if_then(p))
      {
        data_expression condition=RewriteTerm(replace_variables_capture_avoiding_alt(if_then(p).condition(), sigma));
        if (condition==sort_bool::false_())
        {
          return delta_at_zero();
        }
        if (condition==sort_bool::true_())
        {
          return substitute_pCRLproc(if_then(p).then_case(),sigma);
        }
        return if_then(condition,substitute_pCRLproc(if_then(p).then_case(),sigma));
      }
      if (is_if_then_else(p))
      {
        data_expression condition=RewriteTerm(replace_variables_capture_avoiding_alt(if_then_else(p).condition(), sigma));
        if (condition==sort_bool::false_())
        {
          return substitute_pCRLproc(if_then_else(p).else_case(),sigma);
        }
        if (condition==sort_bool::true_())
        {
          return substitute_pCRLproc(if_then_else(p).then_case(),sigma);
        }
        return if_then_else(
                 condition,
                 substitute_pCRLproc(if_then_else(p).then_case(),sigma),
                 substitute_pCRLproc(if_then_else(p).else_case(),sigma));
      }
 
      if (is_sum(p))
      {
        variable_list sumargs=sum(p).variables();
        variable_list vars;
        data_expression_list terms;
 
        for( std::map < variable, data_expression >::const_iterator i=sigma.begin(); i!=sigma.end(); ++i)
        {
          vars=push_back(vars,i->first);
          terms=push_back(terms,i->second);
        }
 
        maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma=sigma;
        alphaconvert(sumargs,local_sigma,vars,terms);
 
        return sum(sumargs,
                   substitute_pCRLproc(sum(p).operand(),local_sigma));
      }
 
      if (is_stochastic_operator(p))
      {
        const stochastic_operator& sto=down_cast<const stochastic_operator>(p);
        variable_list sumargs=sto.variables();
        variable_list vars;
        data_expression_list terms;
 
        for( std::map < variable, data_expression >::const_iterator i=sigma.begin(); i!=sigma.end(); ++i)
        {
          vars=push_back(vars,i->first);
          terms=push_back(terms,i->second);
        }
 
        maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma=sigma;
        alphaconvert(sumargs,local_sigma,vars,terms);
 
        return stochastic_operator(
                            sumargs,
                            replace_variables_capture_avoiding_alt(sto.distribution(),local_sigma),
                            substitute_pCRLproc(sto.operand(),local_sigma));
      }
 
      if (is_process_instance_assignment(p))
      {
        const process_instance_assignment q(p);
        objectdatatype& object=objectIndex(q.identifier());
        const variable_list parameters=object.parameters;
        const assignment_list new_assignments=substitute_assignmentlist(q.assignments(),parameters,false,true,sigma);
        assert(check_valid_process_instance_assignment(q.identifier(),new_assignments));
        return process_instance_assignment(q.identifier(),new_assignments);
      }
 
      if (is_action(p))
      {
        return action(action(p).label(),
                      /* data::*/replace_variables_capture_avoiding_alt(action(p).arguments(), sigma));
      }
 
      if (is_at(p))
      {
        return at(substitute_pCRLproc(at(p).operand(),sigma),
                  /* data::*/replace_variables_capture_avoiding_alt(at(p).time_stamp(),sigma));
      }
 
      if (is_delta(p))
      {
        return p;
      }
 
      if (is_tau(p))
      {
        return p;
      }
 
      if (is_sync(p))
      {
        return process::sync(
                 substitute_pCRLproc(process::sync(p).left(),sigma),
                 substitute_pCRLproc(process::sync(p).right(),sigma));
      }
 
      throw mcrl2::runtime_error("Internal error: expect a pCRL process (2) " + process::pp(p));
      return process_expression();
    }
 
 
    // The function below transforms a ProcessAssignment to a Process, provided
    // that the process is defined in objectnames.
 
    process_instance_assignment transform_process_instance_to_process_instance_assignment(
              const process_instance& procId,
              const std::set<variable>& bound_variables=std::set<variable>())
    {
      objectdatatype& object=objectIndex(procId.identifier());
      const variable_list process_parameters=object.parameters;
      const data_expression_list& rhss=procId.actual_parameters();
 
      assignment_vector new_assignments;
      data_expression_list::const_iterator j=rhss.begin();
      for(variable_list::const_iterator i=process_parameters.begin(); i!=process_parameters.end(); ++i, ++j)
      {
        assert(j!=rhss.end());
        if (*i==*j)
        {
          if (bound_variables.count(*i)>0) // Now *j is a different variable than *i
          {
            new_assignments.push_back(assignment(*i,*j));
          }
        }
        else
        {
          new_assignments.push_back(assignment(*i,*j));
        }
      }
      assert(j==rhss.end());
 
      assert(check_valid_process_instance_assignment(procId.identifier(),assignment_list(new_assignments.begin(),new_assignments.end())));
      process_instance_assignment p(procId.identifier(), assignment_list(new_assignments.begin(),new_assignments.end()));
      return p;
    }
 
    /********************************************************************/
    /*                                                                  */
    /*   BELOW THE PROCEDURES ARE GIVEN TO TRANSFORM PROCESSES TO       */
    /*   LINEAR PROCESSES.                                              */
    /*                                                                  */
    /*                                                                  */
    /*                                                                  */
    /********************************************************************/
 
    typedef enum { first, later } variableposition;
 
    /****************  tovarheadGNF  *********************************/
 
    variable_list parameters_that_occur_in_body(
      const variable_list& parameters,
      const process_expression& body)
    {
      variable_vector result; 
      for(const variable& p: parameters) 
      {
        if (occursinpCRLterm(p,body,false))
        {
          result.push_back(p);
        }
      }
      return variable_list(result.begin(),result.end());
    }
 
    // The variable below is used to count the number of new processes that
    // are made. If this number is very high, it is likely that the regular
    // flag is used, and an unbounded number of new processes are generated.
    // In such a case a warning is printed suggesting to use regular2.
 
    process_identifier newprocess(
      const variable_list& parameters,
      const process_expression& body,
      const processstatustype ps,
      const bool canterminate,
      const bool containstime)
    {
      assert(canterminatebody(body)==canterminate);
      assert(containstimebody(body)==containstime);
 
      process_identifier p1;
      if (searchProcDeclaration(parameters,body,ps, canterminate,containstime,p1))
      {
        return p1;  // The process did already exist. No need to make a new one.
      }
 
      static std::size_t numberOfNewProcesses=0, warningNumber=25;
      numberOfNewProcesses++;
      if (numberOfNewProcesses == warningNumber)
      {
        mCRL2log(mcrl2::log::warning) << "Generated " << numberOfNewProcesses << " new internal processes.";
 
        if (options.lin_method==lmRegular)
        {
          mCRL2log(mcrl2::log::warning) << " A possible unbounded loop can be avoided by using `regular2' or `stack' as linearisation method." << std::endl;
        }
        else if (options.lin_method==lmRegular2)
        {
          mCRL2log(mcrl2::log::warning) << " A possible unbounded loop can be avoided by using `stack' as the linearisation method." << std::endl;
        }
        else
        {
          mCRL2log(mcrl2::log::warning) << std::endl;
        }
        warningNumber=warningNumber*5;
      }
      const variable_list parameters1=parameters_that_occur_in_body(parameters, body);
      const core::identifier_string s=fresh_identifier_generator("P");
      const process_identifier p(s, parameters1);
      assert(std::string(p.name()).size()>0);
      insert_process_declaration(
        p,
        parameters1,
        body,
        ps,
        canterminate,
        containstime);
      return p;
    }
 
 
    process_expression wraptime(
      const process_expression& body,
      const data_expression& time,
      const variable_list& freevars)
    {
      if (is_choice(body))
      {
        return choice(
                 wraptime(choice(body).left(),time,freevars),
                 wraptime(choice(body).right(),time,freevars));
      }
 
      if (is_sum(body))
      {
        variable_list sumvars=sum(body).variables();
        process_expression body1=sum(body).operand();
 
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        alphaconvert(sumvars,sigma,freevars,data_expression_list());
        body1=substitute_pCRLproc(body1, sigma);
        maintain_variables_in_rhs< mutable_map_substitution<> >  sigma_aux(sigma);
        const data_expression time1=/*data::*/replace_variables_capture_avoiding_alt(time, sigma_aux);
        body1=wraptime(body1,time1,sumvars+freevars);
        return sum(sumvars,body1);
      }
 
      if (is_stochastic_operator(body))
      {
        const stochastic_operator& sto=down_cast<const stochastic_operator>(body);
        variable_list sumvars=sto.variables();
        process_expression body1=sto.operand();
 
        maintain_variables_in_rhs<mutable_map_substitution<> > sigma;
        alphaconvert(sumvars,sigma,freevars,data_expression_list());
        body1=substitute_pCRLproc(body1, sigma);
        const data_expression new_distribution=replace_variables_capture_avoiding_alt(sto.distribution(), sigma);
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma_aux(sigma);
        const data_expression time1=replace_variables_capture_avoiding_alt(time, sigma_aux);
        body1=wraptime(body1,time1,sumvars+freevars);
        return stochastic_operator(sumvars,new_distribution,body1);
      }
 
      if (is_if_then(body))
      {
        return if_then(if_then(body).condition(),wraptime(if_then(body).then_case(),time,freevars));
      }
 
      if (is_seq(body))
      {
        return seq(wraptime(seq(body).left(),time,freevars),seq(body).right());
      }
 
      if (is_at(body))
      {
        /* make a new process */
        const process_identifier newproc=newprocess(freevars,body,pCRL,
                                         canterminatebody(body),containstimebody(body));
        assert(check_valid_process_instance_assignment(newproc,assignment_list()));
        return at(process_instance_assignment(
                    newproc,
                    assignment_list()),  //data::data_expression_list(objectdata[objectIndex(newproc)].parameters)),
                  time);
      }
 
      if (// (is_process_instance(body))||
          (is_process_instance_assignment(body))||
          (is_sync(body))||
          (is_action(body))||
          (is_tau(body))||
          (is_delta(body)))
      {
        return at(body,time);
      }
 
      throw mcrl2::runtime_error("Internal error: expect a pCRL process in wraptime " + process::pp(body));
      return process_expression();
    }
 
    typedef enum { alt_state, sum_state, /* cond,*/ seq_state, name_state, multiaction_state } state;
 
    variable get_fresh_variable(const std::string& s, const sort_expression& sort, const int reuse_index=-1)
    {
      /* If reuse_index is smaller than 0 (-1 is the default value), an unused variable name is returned,
         based on the string s with sort `sort'. If reuse_index is larger or equal to
         0 the reuse_index+1 generated variable is returned. If for a particular reuse_index
         this function is called for the first time, it is guaranteed that the returned
         variable is unique, and not used as variable elsewhere. Upon subsequent calls
         get_fresh_variable will return the same variable for the same s,sort and reuse_triple.
         This feature is added to make it possible to avoid generating too many different variables. */
 
 
      if (reuse_index<0)
      {
        variable v(fresh_identifier_generator(s),sort);
        insertvariable(v,true);
        return v;
      }
      else
      {
        static std::map < int , std::map < variable,variable > > generated_variables;
        variable table_index_term(s,sort);
        variable old_variable;
        if (generated_variables[reuse_index].count(table_index_term)>0)
        {
          old_variable=generated_variables[reuse_index][table_index_term];
        }
        else
        {
          /* A new variable must be generated */
          old_variable=get_fresh_variable(s,sort);
          generated_variables[reuse_index][table_index_term]=old_variable;
        }
        return old_variable;
      }
    }
 
    variable_list make_pars(const sort_expression_list& sortlist)
    {
      /* this function returns a list of variables,
         corresponding to the sorts in sortlist */
 
      if (sortlist.empty())
      {
        return variable_list();
      }
 
      const sort_expression& sort=sortlist.front();
 
      variable_list result=make_pars(sortlist.tail());
      result.push_front(get_fresh_variable("a",sort));
      return result;
    }
 
    process_expression distributeActionOverConditions(
      const process_expression& act, // This is a multi-action, actually.
      const data_expression& condition,
      const process_expression& restterm,
      const variable_list& freevars,
      const std::set<variable>& variables_bound_in_sum)
    {
      if (is_if_then(restterm))
      {
        /* Here we check whether the process body has the form
           a (c -> x). For state space generation it turns out
           to be beneficial to rewrite this to c-> a x + !c -> a.delta@0, as in
           certain cases this leads to a reduction of the number
           of states. In this code, we recursively check whether
           the action must be distributed over x. This optimisation
           was observed by Yaroslav Usenko, May 2006. Implemented by JFG.
           On industrial examples, it appears to reduce the state space
           with a factor up to 2.
           Before october 2008 this code was wrong, as it transformed
           an expression to c-> a x, ommitting the a.delta@0. */
 
        const data_expression& c=down_cast<if_then>(restterm).condition();
        const process_expression r=choice(
                                     distributeActionOverConditions(
                                       act,
                                       lazy::and_(condition,c),
                                       if_then(restterm).then_case(),
                                       freevars,variables_bound_in_sum),
                                     distributeActionOverConditions(
                                       act,
                                       lazy::and_(condition,lazy::not_(c)),
                                       delta_at_zero(),
                                       freevars,variables_bound_in_sum));
        return r;
      }
      if (is_if_then_else(restterm))
      {
        /* Here we check whether the process body has the form
           a (c -> x <> y). For state space generation it turns out
           to be beneficial to rewrite this to c-> a x + !c -> a y, as in
           certain cases this leads to a reduction of the number
           of states, despite the duplication of the a action. In this code,
           we recursively check whether the action must be distributed over
           x and y. This optimisation
           was observed by Yaroslav Usenko, May 2006. Implemented by JFG.
           On industrial examples, it appears to reduce the state space
           with a factor up to 2. */
 
        const data_expression& c=down_cast<if_then_else>(restterm).condition();
        const process_expression r=choice(
                                     distributeActionOverConditions(
                                       act,
                                       lazy::and_(condition,c),
                                       if_then_else(restterm).then_case(),
                                       freevars,variables_bound_in_sum),
                                     distributeActionOverConditions(
                                       act,
                                       lazy::and_(condition,lazy::not_(c)),
                                       if_then_else(restterm).else_case(),
                                       freevars,variables_bound_in_sum));
        return r;
      }
      const process_expression restterm1=bodytovarheadGNF(restterm,seq_state,freevars,later,variables_bound_in_sum);
      return if_then(condition,seq(act,restterm1));
    }
 
 
   assignment_list parameters_to_assignment_list(const variable_list& parameters, const std::set<variable>& variables_bound_in_sum)
   {
     assignment_vector result;
     for(const variable& v: parameters)
     {
       if (variables_bound_in_sum.count(v)>0)
       {
         result.push_back(assignment(v,v)); // rhs is another variable than the lhs!!
       }
     }
     return assignment_list(result.begin(),result.end());
   }
 
 
    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)
    {
      /* it is assumed that we only receive processes with
         operators alt, seq, sum_state, cond, name, delta, tau, sync, at and stochastic operator in it */
 
      if (is_choice(body))
      {
        if (alt_state>=s)
        {
          const process_expression body1=bodytovarheadGNF(choice(body).left(),alt_state,freevars,first,variables_bound_in_sum);
          const process_expression body2=bodytovarheadGNF(choice(body).right(),alt_state,freevars,first,variables_bound_in_sum);
          if (isDeltaAtZero(body1))
          {
            return body2;
          }
          if (isDeltaAtZero(body2))
          {
            return body1;
          }
          return choice(body1,body2);
        }
        const process_expression body1=bodytovarheadGNF(body,alt_state,freevars,first,variables_bound_in_sum);
        const process_identifier newproc=newprocess(freevars,body1,pCRL,
                                         canterminatebody(body1),
                                         containstimebody(body1));
        assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
        return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
      }
 
      if (is_sum(body))
      {
        if (sum_state>=s)
        {
          variable_list sumvars=sum(body).variables();
          process_expression body1=sum(body).operand();
 
          maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
          alphaconvert(sumvars,sigma,freevars,data_expression_list());
          body1=substitute_pCRLproc(body1,sigma);
          std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
          variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
          body1=bodytovarheadGNF(body1,sum_state,sumvars+freevars,first,variables_bound_in_sum1);
          /* Due to the optimisation below, suggested by Yaroslav Usenko, bodytovarheadGNF(...,sum_state,...)
             can deliver a process of the form c -> x + !c -> y. In this case, the
             sumvars must be distributed over both summands. */
          if (is_choice(body1))
          {
            return choice(sum(sumvars,choice(body1).left()),
                          sum(sumvars,choice(body1).right()));
          }
          return sum(sumvars,body1);
        }
        const process_expression body1=bodytovarheadGNF(body,alt_state,freevars,first,variables_bound_in_sum);
        const process_identifier newproc=newprocess(freevars,body1,pCRL,
                                         canterminatebody(body1),
                                         containstimebody(body1));
        assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
        return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
      }
 
      if (is_stochastic_operator(body))
      {
        if (seq_state>=s)
        {
          const stochastic_operator& sto=down_cast<const stochastic_operator>(body);
          variable_list sumvars=sto.variables();
          data_expression distribution=sto.distribution();
          process_expression body1=sto.operand();
 
          maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
          alphaconvert(sumvars,sigma,freevars,data_expression_list());
          distribution=/* data::*/replace_variables_capture_avoiding_alt(distribution,sigma);
          body1=substitute_pCRLproc(body1,sigma);
          std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
          variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
          body1=bodytovarheadGNF(body1,name_state,sumvars+freevars,v,variables_bound_in_sum1);
          /* Due to the optimisation below, suggested by Yaroslav Usenko, bodytovarheadGNF(...,sum_state,...)
             can deliver a process of the form c -> x + !c -> y. In this case, the
             sumvars must be distributed over both summands. */
          return stochastic_operator(sumvars,distribution,body1);
        }
        const process_expression body_=bodytovarheadGNF(body,seq_state,freevars,first,variables_bound_in_sum);
        const process_identifier newproc=newprocess(freevars,body_,pCRL,
                                         canterminatebody(body_),
                                         containstimebody(body_));
        assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
        return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
      }
 
      if (is_if_then(body))
      {
        const data_expression& condition=down_cast<if_then>(body).condition();
        const process_expression& body1=down_cast<if_then>(body).then_case();
 
        if (s<=sum_state)
        {
          return if_then(
                   condition,
                   bodytovarheadGNF(body1,seq_state,freevars,first,variables_bound_in_sum));
        }
        const process_expression body2=bodytovarheadGNF(body,alt_state,freevars,first,variables_bound_in_sum);
        const process_identifier newproc=newprocess(freevars,body2,pCRL,
                                         canterminatebody(body2),
                                         containstimebody(body2));
        assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
        return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
 
      }
 
      if (is_if_then_else(body))
      {
        const data_expression& condition=down_cast<if_then_else>(body).condition();
        const process_expression& body1=down_cast<if_then_else>(body).then_case();
        const process_expression& body2=down_cast<if_then_else>(body).else_case();
 
        if (isDeltaAtZero(body1) && isDeltaAtZero(body2))
        {
          return body1;
        }
 
        if ((s<=sum_state) && ((isDeltaAtZero(body1))||(isDeltaAtZero(body2))))
        {
          if (isDeltaAtZero(body2))
          {
            return if_then(
                     condition,
                     bodytovarheadGNF(body1,seq_state,freevars,first,variables_bound_in_sum));
          }
          /* body1=="Delta@0" */
          {
            return if_then(
                     lazy::not_(condition),
                     bodytovarheadGNF(body2,seq_state,freevars,first,variables_bound_in_sum));
          }
        }
        if (alt_state==s) /* body1!=Delta@0 and body2!=Delta@0 */
        {
          return
            choice(
              if_then(
                condition,
                bodytovarheadGNF(body1,seq_state,freevars,first,variables_bound_in_sum)),
              if_then(
                lazy::not_(condition),
                bodytovarheadGNF(body2,seq_state,freevars,first,variables_bound_in_sum)));
        }
        const process_expression body3=bodytovarheadGNF(body,alt_state,freevars,first,variables_bound_in_sum);
        const process_identifier newproc=newprocess(freevars,body3,pCRL,
                                         canterminatebody(body3),
                                         containstimebody(body3));
        assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
        return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
 
      }
 
      if (is_seq(body))
      {
        process_expression body1=seq(body).left();
        process_expression body2=seq(body).right();
 
        if (s<=seq_state)
        {
          body1=bodytovarheadGNF(body1,name_state,freevars,v,variables_bound_in_sum);
          if (!canterminatebody(body1))
          {
            /* In this case there is no need to investigate body2, as it cannot be reached. */
            return body1;
          }
          if ((is_if_then(body2)) && (s<=sum_state))
          {
            /* Here we check whether the process body has the form
               a (c -> x) + !c -> delta@0. For state space generation it turns out
               to be beneficial to rewrite this to c-> a x, as in
               certain cases this leads to a reduction of the number
               of states. An extra change (24/12/2006) is that the
               conditions are distributed recursively over
               all conditions. The optimisation
               was observed by Yaroslav Usenko, May 2006. Implemented by JFG.
               On industrial examples, it appears to reduce the state space
               with a factor up to 2. Until 1/11/2008 this code was incorrect,
               because the summand a (!c -> delta@0) was not forgotten.*/
 
            const data_expression& c=down_cast<if_then>(body2).condition();
 
            const process_expression r= choice(
                                          distributeActionOverConditions(body1,c,if_then(body2).then_case(),freevars,variables_bound_in_sum),
                                          distributeActionOverConditions(body1,lazy::not_(c),delta_at_zero(),freevars,variables_bound_in_sum));
            return r;
          }
          if ((is_if_then_else(body2)) && (s<=sum_state))
          {
 
            /* Here we check whether the process body has the form
               a (c -> x <> y). For state space generation it turns out
               to be beneficial to rewrite this to c-> a x + !c -> a y, as in
               certain cases this leads to a reduction of the number
               of states, despite the duplication of the a action. An extra
               change (24/12/2006) is that the conditions are distributed recursively over
               all conditions. The optimisation
               was observed by Yaroslav Usenko, May 2006. Implemented by JFG.
               On industrial examples, it appears to reduce the state space
               with a factor up to 2. */
 
 
            const data_expression& c=down_cast<if_then_else>(body2).condition();
            const process_expression r= choice(
                                          distributeActionOverConditions(body1,c,if_then_else(body2).then_case(),freevars,variables_bound_in_sum),
                                          distributeActionOverConditions(body1,lazy::not_(c),if_then_else(body2).else_case(),freevars,variables_bound_in_sum));
            return r;
          }
          body2=bodytovarheadGNF(body2,seq_state,freevars,later,variables_bound_in_sum);
          return seq(body1,body2);
        }
        body1=bodytovarheadGNF(body,alt_state,freevars,first,variables_bound_in_sum);
        const process_identifier newproc=newprocess(freevars,body1,pCRL,canterminatebody(body1),
                                         containstimebody(body1));
 
        assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
        return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
      }
 
      if (is_action(body))
      {
        if ((s==multiaction_state)||(v==first))
        {
          return body;
        }
 
        bool isnew=false;
        objectdatatype& object=addMultiAction(action(body),isnew);
 
        if (object.process_representing_action==process_identifier())
        {
          /* this action does not yet have a corresponding process, which
             must be constructed. The resulting process is stored in
             the variable process_representing_action in objectdata. Tempvar below is
             needed as objectdata may be realloced as a side effect
             of newprocess */
          const process_identifier tempvar=newprocess(
                                             object.parameters,
                                             object.processbody,
                                             GNF,true,false);
          object.process_representing_action=tempvar;
        }
        return transform_process_instance_to_process_instance_assignment(
                          process_instance(object.process_representing_action,
                          action(body).arguments()));
      }
 
      if (is_sync(body))
      {
        bool isnew=false;
        const process_expression& body1=down_cast<process::sync>(body).left();
        const process_expression& body2=down_cast<process::sync>(body).right();
        const action_list ma=linMergeMultiActionListProcess(
                               bodytovarheadGNF(body1,multiaction_state,freevars,v,variables_bound_in_sum),
                               bodytovarheadGNF(body2,multiaction_state,freevars,v,variables_bound_in_sum));
 
        const process_expression mp=action_list_to_process(ma);
        if ((s==multiaction_state)||(v==first))
        {
          return mp;
        }
 
        objectdatatype& object=addMultiAction(mp,isnew);
 
        if (object.process_representing_action==process_identifier())
        {
          /* this action does not yet have a corresponding process, which
             must be constructed. The resulting process is stored in
             the variable process_representing_action in objectdata. Tempvar below is needed
             as objectdata may be realloced as a side effect of newprocess */
          process_identifier tempvar=newprocess(
                                       object.parameters,
                                       object.processbody,
                                       GNF,true,false);
          object.process_representing_action=tempvar;
        }
        return transform_process_instance_to_process_instance_assignment(
                      process_instance(
                           process_identifier(object.process_representing_action),
                           getarguments(ma)));
      }
 
      if (is_at(body))
      {
        process_expression body1=bodytovarheadGNF(
                                   at(body).operand(),
                                   s,
                                   freevars,
                                   first,variables_bound_in_sum);
        data_expression time=data_expression(at(body).time_stamp());
        /* put the time operator around the first action or process */
        body1=wraptime(body1,time,freevars);
        if (v==first)
        {
          return body1;
        }
 
        /* make a new process, containing this process */
        const process_identifier newproc=newprocess(freevars,body1,pCRL,
                                         canterminatebody(body1),
                                         containstimebody(body1));
        assert(check_valid_process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum)));
        return process_instance_assignment(newproc,parameters_to_assignment_list(objectIndex(newproc).parameters,variables_bound_in_sum));
      }
 
      if (is_process_instance_assignment(body))
      {
        // return transform_process_assignment_to_process(body);
        return body;
      }
 
 
      if (is_tau(body))
      {
        if (v==first)
        {
          return tau();
        }
        assert(check_valid_process_instance_assignment(tau_process,assignment_list()));
        return process_instance_assignment(tau_process,assignment_list());
      }
 
      if (is_delta(body))
      {
        if (v==first)
        {
          return body;
        }
        assert(check_valid_process_instance_assignment(delta_process,assignment_list()));
        return process_instance_assignment(delta_process,assignment_list());
      }
 
      throw mcrl2::runtime_error("unexpected process format in bodytovarheadGNF " + process::pp(body) +".");
      return process_expression();
    }
 
    void procstovarheadGNF(const std::vector < process_identifier>& procs)
    {
      /* transform the processes in procs into pre-Greibach Normal Form */
      for (const process_identifier& i: procs)
      {
        objectdatatype& object=objectIndex(i);
 
        // The intermediate variable result is needed here
        // because objectdata can be reallocated as a side
        // effect of bodytovarheadGNF.
 
        std::set<variable> variables_bound_in_sum;
        const process_expression result=
          bodytovarheadGNF(
            object.processbody,
            alt_state,
            object.parameters,
            first,
            variables_bound_in_sum);
        object.processbody=result;
      }
    }
 
    /**************** towards real GREIBACH normal form **************/
 
    typedef enum {terminating,infinite} terminationstatus;
 
    process_expression putbehind(const process_expression& body1, const process_expression& body2)
    {
      if (is_choice(body1))
      {
        return choice(
                 putbehind(choice(body1).left(),body2),
                 putbehind(choice(body1).right(),body2));
      }
 
      if (is_seq(body1))
      {
        return seq(seq(body1).left(), putbehind(seq(body1).right(),body2));
      }
 
      if (is_if_then(body1))
      {
        return if_then(if_then(body1).condition(),putbehind(if_then(body1).then_case(),body2));
      }
 
      if (is_sum(body1))
      {
        /* we must take care that no variables in body2 are
            inadvertently bound */
        variable_list sumvars=sum(body1).variables();
 
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        alphaconvertprocess(sumvars,sigma,body2);
        return sum(sumvars,
                   putbehind(substitute_pCRLproc(sum(body1).operand(), sigma),
                             body2));
      }
 
      if (is_stochastic_operator(body1))
      {
        const stochastic_operator& sto=atermpp::down_cast<stochastic_operator>(body1);
        variable_list stochvars=sto.variables();
 
        // See explanation at sum operator above.
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        alphaconvertprocess(stochvars,sigma,body2);
        return stochastic_operator(
                 stochvars,
                 sto.distribution(),
                 putbehind(
                       substitute_pCRLproc(sto.operand(),sigma),
                       body2));
      }
 
 
      if (is_action(body1))
      {
        return seq(body1,body2);
      }
 
      if (is_sync(body1))
      {
        return seq(body1,body2);
      }
 
      if (is_process_instance_assignment(body1))
      {
        return seq(body1,body2);
      }
 
      if (is_delta(body1))
      {
        return body1;
      }
 
      if (is_tau(body1))
      {
        return seq(body1,body2);
        // throw mcrl2::runtime_error("Expect only multiactions, not a tau.");
      }
 
      if (is_at(body1))
      {
        return seq(body1,body2);
      }
 
      throw mcrl2::runtime_error("Internal error. Unexpected process format in putbehind " + process::pp(body1) +".");
      return process_expression();
    }
 
 
    process_expression distribute_condition(
      const process_expression& body1,
      const data_expression& condition)
    {
      if (is_choice(body1))
      {
        return choice(
                 distribute_condition(choice(body1).left(),condition),
                 distribute_condition(choice(body1).right(),condition));
      }
 
      if (is_seq(body1))
      {
        return if_then(condition,body1);
      }
 
      if (is_if_then(body1))
      {
        return if_then(
                 lazy::and_(if_then(body1).condition(),condition),
                 if_then(body1).then_case());
      }
 
      if (is_sum(body1))
      {
        /* we must take care that no variables in condition are
            inadvertently bound */
        variable_list sumvars=sum(body1).variables();
        maintain_variables_in_rhs< mutable_map_substitution<> >  sigma;
        alphaconvert(sumvars,sigma,variable_list(), data_expression_list({ condition }));
        return sum(
                 sumvars,
                 distribute_condition(
                   substitute_pCRLproc(sum(body1).operand(),sigma),
                   condition));
      }
 
      if (is_stochastic_operator(body1))
      {
        /* we must take care that no variables in condition are
            inadvertently bound */
        const stochastic_operator& sto=atermpp::down_cast<stochastic_operator>(body1);
        variable_list stochvars=sto.variables();
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        alphaconvert(stochvars,sigma,variable_list(), data_expression_list({ condition }));
 
        return stochastic_operator(
                 stochvars,
                 if_(condition,
                        replace_variables_capture_avoiding_alt(
                                               sto.distribution(),
                                               sigma),
                        if_(variables_are_equal_to_default_values(stochvars),real_one(),real_zero())),
                 distribute_condition(
                       substitute_pCRLproc(sto.operand(),sigma),
                       condition));
      }
 
      if (is_at(body1)||
          is_action(body1)||
          is_sync(body1)||
          is_process_instance_assignment(body1)||
          is_delta(body1)||
          is_tau(body1))
      {
        return if_then(condition,body1);
      }
 
      throw mcrl2::runtime_error("Internal error. Unexpected process format in distribute condition " + process::pp(body1) +".");
    }
    
    /* This process calculates the equivalent of sum sumvars dist stochvars[distribution] body
       where the distribution occurs in front. This can only be done under limited circumstances.
       Assume we can enumerate the values of sumvars by e1,...,en. Introduce n copies of stochvars,
       i.e., stochvars1,...,stochvarsn. The new process becomes 
 
           dist stochvars1,stochvars2,...,stochvarsn
                [distribution(e1,stochvars1)*distribution(e2,stochvars2)*...*distribution(en,stochvarsn)].
 
           body(e1,stochvars1)+
           body(e2,stochvars2)+
           ...
           body(en,stochvarsn)
    */
 
    process_expression enumerate_distribution_and_sums(
                         const variable_list& sumvars, 
                         const variable_list& stochvars, 
                         const data_expression& distribution,
                         const process_expression& body)
    {
      if (options.norewrite)
      {
        throw mcrl2::runtime_error("The use of the rewriter must be allowed to distribute a sum operator over a distribution.");
      }
 
 
      std::vector < data_expression_vector > data_vector(1,data_expression_vector());
      for(const variable& v:sumvars) 
      {
        std::vector < data_expression_vector > new_data_vector;
 
        if (!data.is_certainly_finite(v.sort()))
        {
          throw mcrl2::runtime_error("Cannot distribute a sum variable of non finite sort " + pp(v.sort()) + " over a distribution, which is required for linearisation.");
        }
 
        for(const data_expression& d: enumerate_expressions(v.sort(),data,rewr))
        {
          for(const data_expression_vector& dv: data_vector)
          {
            data_expression_vector new_dv=dv;
            new_dv.push_back(d);
            new_data_vector.push_back(new_dv);
          }
           
        }
        data_vector.swap(new_data_vector);
        
      } 
      assert(!data_vector.empty());
      
      process_expression resulting_body;
      data_expression resulting_distribution;
      variable_list resulting_stochastic_variables;
      bool result_defined=false;
      for(const data_expression_vector& d: data_vector)
      {
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        variable_list vl = stochvars;
        alphaconvert(vl,sigma,stochvars,data_expression_list());
        data_expression_vector::const_iterator i=d.begin();
        for(const variable& v: sumvars)
        {
          sigma[v] = *i;
          ++i;
        }
        const process_expression d1=substitute_pCRLproc(body,sigma);
        const data_expression new_distribution=replace_variables_capture_avoiding_alt(distribution, sigma);
 
        if (result_defined)
        {
          resulting_body=choice(resulting_body, d1);
          resulting_distribution=sort_real::times(resulting_distribution,new_distribution);
          resulting_stochastic_variables=resulting_stochastic_variables + vl;
        }
        else
        {
          resulting_body=d1;
          resulting_distribution=new_distribution;
          resulting_stochastic_variables=vl;
          result_defined=true;
        }
      } 
      /* Put the distribution in front. */
 
      return stochastic_operator(resulting_stochastic_variables, resulting_distribution, resulting_body);
    }
 
    process_expression distribute_sum_over_a_stochastic_operator(
                         const variable_list& sumvars, 
                         const variable_list& stochastic_variables, 
                         const data_expression& distribution,
                         const process_expression& body)
    {
      if (is_sum(body)||
          is_choice(body)||
          is_seq(body)||
          is_if_then(body)||
          is_sync(body)||
          is_action(body)||
          is_tau(body)||
          is_at(body)||
          is_process_instance_assignment(body)||
          isDeltaAtZero(body))
      {
        return enumerate_distribution_and_sums(sumvars,stochastic_variables,distribution,body);
      }
 
      if (is_delta(body)||
          is_tau(body))
      {
        return body;
      }
 
      if (is_stochastic_operator(body))
      {
        const stochastic_operator& sto=atermpp::down_cast<stochastic_operator>(body);
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        variable_list inner_stoch_vars=sto.variables();
        alphaconvert(inner_stoch_vars,sigma,sumvars,data_expression_list());
        const process_expression new_body=substitute_pCRLproc(sto.operand(), sigma);
        const data_expression new_distribution=replace_variables_capture_avoiding_alt(sto.distribution(), sigma);
        return distribute_sum_over_a_stochastic_operator(sumvars, 
                                                         stochastic_variables + inner_stoch_vars, 
                                                         sort_real::times(distribution,new_distribution), new_body);
      }
 
      throw mcrl2::runtime_error("Internal error. Unexpected process format in distribute_sum " + process::pp(body) +".");
      return process_expression();
    }
 
    process_expression distribute_sum(
      const variable_list& sumvars,
      const process_expression& body1)
    {
      if (is_choice(body1))
      {
        return choice(
                 distribute_sum(sumvars,choice(body1).left()),
                 distribute_sum(sumvars,choice(body1).right()));
      }
 
      if (is_seq(body1)||
          is_if_then(body1)||
          is_sync(body1)||
          is_action(body1)||
          is_tau(body1)||
          is_at(body1)||
          is_process_instance_assignment(body1)||
          isDeltaAtZero(body1))
      {
        return sum(sumvars,body1);
      }
 
      if (is_sum(body1))
      {
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        variable_list inner_sumvars=sum(body1).variables();
        alphaconvert(inner_sumvars,sigma,sumvars,data_expression_list());
        const process_expression new_body1=substitute_pCRLproc(sum(body1).operand(), sigma);
        return sum(sumvars+inner_sumvars,new_body1);
      }
 
      if (is_stochastic_operator(body1))
      {
        const stochastic_operator& sto=atermpp::down_cast<stochastic_operator>(body1);
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        variable_list inner_stoch_vars=sto.variables();
        alphaconvert(inner_stoch_vars,sigma,sumvars,data_expression_list());
        const process_expression new_body1=substitute_pCRLproc(sto.operand(), sigma);
        const data_expression new_distribution=replace_variables_capture_avoiding_alt(sto.distribution(), sigma);
        return distribute_sum_over_a_stochastic_operator(sumvars, inner_stoch_vars, new_distribution, new_body1);
      }
 
      if (is_delta(body1)||
          is_tau(body1))
      {
        return body1;
      }
 
      throw mcrl2::runtime_error("Internal error. Unexpected process format in distribute_sum " + process::pp(body1) +".");
      return process_expression();
    }
 
    int match_sequence(
      const std::vector < process_instance_assignment >& s1,
      const std::vector < process_instance_assignment >& s2,
      const bool regular2)
    {
      /* s1 and s2 are sequences of typed variables of
         the form Process(ProcVarId("P2",[SortId("Bit"),
         SortId("Bit")]),[OpId("b1",SortId("Bit")),OpId("b1",SortId("Bit"))]).
         This function yields true if the names and types of
         the processes in s1 and s2 match. */
 
      std::vector < process_instance_assignment >::const_iterator i2=s2.begin();
      for (std::vector < process_instance_assignment >::const_iterator i1=s1.begin();
           i1!=s1.end(); ++i1,++i2)
      {
        if (i2==s2.end())
        {
          return false;
        }
        if (regular2)
        {
          if (i1->identifier()!=i2->identifier())
          {
            return false;
          }
        }
        else
        {
          if (*i1!=*i2)
          {
            return false;
          }
        }
      }
      if (i2!=s2.end())
      {
        return false;
      }
      return true;
    }
 
    bool exists_variable_for_sequence(
      const std::vector < process_instance_assignment >& process_names,
      process_identifier& result)
    {
      std::vector < std::vector < process_instance_assignment > >::const_iterator rwalker=representedprocesses.begin();
      for (std::vector < process_identifier >::const_iterator walker=seq_varnames.begin();
           walker!=seq_varnames.end(); ++walker,++rwalker)
      {
        assert(rwalker!=representedprocesses.end());
        const process_identifier process=*walker;
        if (match_sequence(process_names,*rwalker,options.lin_method==lmRegular2))
        {
          result=process;
          return true;
        }
      }
      assert(rwalker==representedprocesses.end());
      return false;
    }
 
    void extract_names(
      const process_expression& sequence,
      std::vector < process_instance_assignment >& result)
    {
      if (is_action(sequence)||is_process_instance_assignment(sequence))
      {
        result.push_back(atermpp::down_cast<process_instance_assignment>(sequence));
        return;
      }
 
      if (is_stochastic_operator(sequence))
      {
        const stochastic_operator& sto=atermpp::down_cast<stochastic_operator>(sequence);
        extract_names(sto.operand(),result);
        return;
      }
 
      if (is_seq(sequence))
      {
        const process_expression& first=down_cast<seq>(sequence).left();
        if (is_process_instance_assignment(first))
        {
          result.push_back(atermpp::down_cast<process_instance_assignment>(first));
          objectdatatype& object=objectIndex(atermpp::down_cast<process_instance_assignment>(first).identifier());
          if (object.canterminate)
          {
            extract_names(seq(sequence).right(),result);
          }
          return;
        }
      }
 
      throw mcrl2::runtime_error("Internal error. Expected sequence of process names (1) " + process::pp(sequence) + ".");
    }
 
    variable_list parscollect(const process_expression& oldbody, process_expression& newbody)
    {
      /* we expect that oldbody is a sequence of process instances */
 
      if (is_process_instance_assignment(oldbody))
      {
        const process_identifier procId=process_instance_assignment(oldbody).identifier();
        const variable_list parameters=objectIndex(procId).parameters;
        assert(check_valid_process_instance_assignment(procId,data::assignment_list()));
        newbody=process_instance_assignment(procId,data::assignment_list());
        return parameters;
      }
 
      if (is_seq(oldbody))
      {
        const process_expression& first=down_cast<seq>(oldbody).left();
        if (is_process_instance_assignment(first))
        {
          objectdatatype& object=objectIndex(process_instance_assignment(first).identifier());
          if (object.canterminate)
          {
            const process_identifier procId=process_instance_assignment(first).identifier();
            const variable_list pars=parscollect(seq(oldbody).right(),newbody);
            variable_list pars1, pars2;
            const variable_list new_pars=construct_renaming(pars,objectIndex(procId).parameters,pars1,pars2,false);
            assignment_vector new_assignment;
            for(variable_list::const_iterator i=pars2.begin(), j=new_pars.begin(); i!=pars2.end(); ++i,++j)
            {
              assert(j!=new_pars.end());
              new_assignment.push_back(assignment(*i,*j));
            }
            assert(check_valid_process_instance_assignment(procId,assignment_list(new_assignment.begin(),new_assignment.end())));
            newbody=seq(process_instance_assignment(procId,assignment_list(new_assignment.begin(),new_assignment.end())),newbody);
            const variable_list result=pars1+pars;
            assert(std::set<variable>(result.begin(),result.end()).size()==result.size()); // all elements in the result are unique. 
            return result;
          }
          else
          {
            return parscollect(first,newbody);
          }
        }
      }
 
      throw mcrl2::runtime_error("Internal error. Expected a sequence of process names (2) " + process::pp(oldbody) +".");
      return variable_list();
    }
 
    assignment_list argscollect_regular(
                         const process_expression& t,
                         const variable_list& vl,
                         const std::set<variable>& variables_bound_in_sum)
    {
      assignment_vector result;
      for(const variable& v: vl) 
      {
        if (variables_bound_in_sum.count(v)>0 && occursinpCRLterm(v,t,false))
        {
          result.push_back(assignment(v,v)); // Here an identity assignment is used, as it is possible
                                               // that the *i at the lhs is not the same variable as *i at the rhs.
        }
      }
      return assignment_list(result.begin(),result.end());
    }
 
    assignment_list argscollect_regular2(const process_expression& t, variable_list& vl)
    {
      if (is_process_instance_assignment(t))
      {
        const process_instance_assignment p(t);
        objectdatatype& object=objectIndex(p.identifier());
 
        const variable_list pars=object.parameters; // These are the old parameters of the process.
        assert(pars.size()<=vl.size());
 
        std::map<variable,data_expression>sigma;
        for(const assignment& a: p.assignments())
        {
          sigma[a.lhs()]=a.rhs();
        }
 
        assignment_list result;
        for(variable_list::const_iterator i=pars.begin(); i!=pars.end(); ++i, vl.pop_front())
        {
          assert(!vl.empty());
          const data_expression new_rhs=make_map_substitution(sigma)(*i);
          result.push_front(assignment(vl.front(),new_rhs)); // Identity assignments are stored as lhs and rhs may
                                                             // refer to different variables.
        }
        return reverse(result);
      }
 
      if (is_seq(t))
      {
        const process_instance_assignment firstproc=atermpp::down_cast<process_instance_assignment>(seq(t).left());
        objectdatatype& object=objectIndex(firstproc.identifier());
        const assignment_list first_assignment=argscollect_regular2(firstproc,vl);
        if (object.canterminate)
        {
          return first_assignment + argscollect_regular2(seq(t).right(),vl);
        }
        return first_assignment;
      }
 
      throw mcrl2::runtime_error("Internal error. Expected a sequence of process names (3) " + process::pp(t) +".");
    }
 
    process_expression cut_off_unreachable_tail(const process_expression& t)
    {
      if (is_process_instance_assignment(t)||is_delta(t)||is_action(t)||is_tau(t)||is_sync(t))
      {
        return t;
      }
 
      if (is_stochastic_operator(t))
      {
        const stochastic_operator& sto=atermpp::down_cast<const stochastic_operator>(t);
        return stochastic_operator(sto.variables(),sto.distribution(), cut_off_unreachable_tail(sto.operand()));
      }
 
      if (is_seq(t))
      {
        const process_expression& firstproc=down_cast<seq>(t).left();
        objectdatatype& object=objectIndex(process_instance_assignment(firstproc).identifier());
        if (object.canterminate)
        {
          return seq(firstproc,cut_off_unreachable_tail(seq(t).right()));
        }
        return firstproc;
      }
 
      throw mcrl2::runtime_error("Internal error. Expected a sequence of process names (4) " + process::pp(t) +".");
      return process_expression();
    }
 
    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_identifier new_process;
 
      /* Sequence consists of a sequence of process references,
         concatenated with the sequential composition operator, which may be preceded by
         a stochastic operator.  */
      if (is_stochastic_operator(sequence))
      {
        /* Leave the stochastic operators in place */
        const stochastic_operator& sto=atermpp::down_cast<const stochastic_operator>(sequence);
        std::set<variable> variables_bound_in_sum_new=variables_bound_in_sum;
        variables_bound_in_sum_new.insert(sto.variables().begin(),sto.variables().end());
        return stochastic_operator(sto.variables(),
                                   sto.distribution(), 
                                   create_regular_invocation(sto.operand(),todo,freevars+sto.variables(),variables_bound_in_sum_new));
      }
 
      sequence=cut_off_unreachable_tail(sequence);
      sequence=pCRLrewrite(sequence);
      std::vector < process_instance_assignment > process_names;
      extract_names(sequence,process_names);
      assert(!process_names.empty());
 
      if (process_names.size()==1)
      {
        /* length of list equals 1 */
        if (is_process_instance_assignment(sequence))
        {
          return sequence;
        }
        if (is_seq(sequence))
        {
          return seq(sequence).left();
        }
        throw mcrl2::runtime_error("Internal error. Expected a sequence of process names " + process::pp(sequence) +".");
      }
      /* There is more than one process name in the sequence,
         so, we must replace them by a single name */
 
      /* We first start out by searching whether
         there is already a variable with a matching sequence
         of variables */
      if (!exists_variable_for_sequence(process_names,new_process))
      {
        /* There does not exist an appropriate variable,
           so, make it and return its index in n */
        process_expression newbody;
        if (options.lin_method==lmRegular2)
        {
          variable_list pars=parscollect(sequence,newbody);
          new_process=newprocess(pars,newbody,pCRL,
                                 canterminatebody(newbody),
                                 containstimebody(newbody));
          representedprocesses.push_back(process_names);
        }
        else
        {
          new_process=newprocess(freevars,sequence,pCRL,
                                 canterminatebody(sequence),containstimebody(sequence));
          representedprocesses.push_back(process_names);
        }
        seq_varnames.push_back(new_process);
        todo.push_back(new_process);
      }
      /* now we must construct arguments */
      variable_list parameters=objectIndex(new_process).parameters;
      if (options.lin_method==lmRegular2)
      {
        const assignment_list args=argscollect_regular2(sequence,parameters);
        assert(check_valid_process_instance_assignment(new_process,args));
        const process_expression p=process_instance_assignment(new_process,args);
        return p;
      }
      else
      {
        assert(check_valid_process_instance_assignment(new_process,argscollect_regular(sequence,parameters,variables_bound_in_sum)));
        return process_instance_assignment(new_process,argscollect_regular(sequence,parameters,variables_bound_in_sum));
      }
    }
 
    process_expression to_regular_form(
      const process_expression& t,
      std::vector <process_identifier>& todo,
      const variable_list& freevars,
      const std::set<variable>& variables_bound_in_sum)
    /* t has the form of the sum, and condition over actions
       each followed by a sequence of variables. We replace
       this variable by a single one, putting the new variable
       on the todo list, to be transformed to regular form also. */
    {
      if (is_choice(t))
      {
        const process_expression t1=to_regular_form(choice(t).left(),todo,freevars,variables_bound_in_sum);
        const process_expression t2=to_regular_form(choice(t).right(),todo,freevars,variables_bound_in_sum);
        return choice(t1,t2);
      }
 
      if (is_seq(t))
      {
        const process_expression& firstact=down_cast<seq>(t).left();
        assert(is_at(firstact)||is_tau(firstact)||is_action(firstact)||is_sync(firstact));
        /* the sequence of variables in
                   the second argument must be replaced */
        return seq(firstact,create_regular_invocation(seq(t).right(),todo,freevars,variables_bound_in_sum));
      }
 
      if (is_if_then(t))
      {
        return if_then(if_then(t).condition(),to_regular_form(if_then(t).then_case(),todo,freevars,variables_bound_in_sum));
      }
 
      if (is_sum(t))
      {
        variable_list sumvars=sum(t).variables();
 
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        alphaconvert(sumvars,sigma,freevars,data_expression_list());
        const process_expression body=substitute_pCRLproc(sum(t).operand(), sigma);
 
        std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
        variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
        return sum(sumvars,
                   to_regular_form(
                     body,
                     todo,
                     sumvars+freevars,
                     variables_bound_in_sum1));
      }
 
      if (is_stochastic_operator(t))
      {
        const stochastic_operator& sto=down_cast<const stochastic_operator>(t);
        variable_list sumvars=sto.variables();
 
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        alphaconvert(sumvars,sigma,freevars,data_expression_list());
        const data_expression distribution=replace_variables_capture_avoiding_alt(
                                               sto.distribution(),
                                               sigma);
        const process_expression body=substitute_pCRLproc(sto.operand(),sigma);
 
        std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
        variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
        return stochastic_operator(
                   sumvars,
                   distribution,
                   to_regular_form(
                     body,
                     todo,
                     sumvars+freevars,
                     variables_bound_in_sum1));
      }
 
      if (is_sync(t)||is_action(t)||is_delta(t)||is_tau(t)||is_at(t))
      {
        return t;
      }
 
      throw mcrl2::runtime_error("to regular form expects GNF " + process::pp(t) +".");
      return process_expression();
    }
 
    process_expression distributeTime(
      const process_expression& body,
      const data_expression& time,
      const variable_list& freevars,
      data_expression& timecondition)
    {
      if (is_choice(body))
      {
        return choice(
                 distributeTime(choice(body).left(),time,freevars,timecondition),
                 distributeTime(choice(body).right(),time,freevars,timecondition));
      }
 
      if (is_sum(body))
      {
        variable_list sumvars=sum(body).variables();
        process_expression body1=sum(body).operand();
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        alphaconvert(sumvars,sigma,freevars,data_expression_list());
        body1=substitute_pCRLproc(body1, sigma);
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma_aux(sigma);
        const data_expression time1=replace_variables_capture_avoiding_alt(time,sigma_aux);
        body1=distributeTime(body1,time1,sumvars+freevars,timecondition);
        return sum(sumvars,body1);
      }
 
      if (is_stochastic_operator(body))
      {
        const stochastic_operator& sto=down_cast<const stochastic_operator>(body);
        variable_list sumvars=sto.variables();
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        alphaconvert(sumvars,sigma,freevars,data_expression_list());
        process_expression new_body=substitute_pCRLproc(sto.operand(), sigma);
        data_expression new_distribution=/*data::*/replace_variables_capture_avoiding_alt(sto.distribution(), sigma);
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma_aux(sigma);
        const data_expression time1=/*data::*/replace_variables_capture_avoiding_alt(time,sigma_aux);
        new_body=distributeTime(new_body,time1,sumvars+freevars,timecondition);
        return stochastic_operator(sumvars,new_distribution,new_body);
      }
 
      if (is_if_then(body))
      {
        data_expression timecondition=sort_bool::true_();
        process_expression body1=distributeTime(
                                   if_then(body).then_case(),
                                   time,
                                   freevars,
                                   timecondition);
 
        return if_then(
                 lazy::and_(data_expression(if_then(body).condition()),timecondition),
                 body1);
      }
 
      if (is_seq(body))
      {
        return seq(
                 distributeTime(seq(body).left(), time,freevars,timecondition),
                 seq(body).right());
      }
 
      if (is_at(body))
      {
        /* make a new process */
        timecondition=equal_to(time,data_expression(at(body).time_stamp()));
        return body;
      }
 
      if ((is_sync(body))||
          (is_action(body))||
          (is_tau(body))||
          (is_delta(body)))
      {
        return at(body,time);
      }
 
      throw mcrl2::runtime_error("Internal error: expect a pCRL process in distributeTime " + process::pp(body) +".");
      return process_expression();
    }
 
    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)
    /* This process delivers the transformation of body
       to GNF with actions as a head symbol, or it
       delivers NULL if body is not a pCRL process.
       If regular=1, then an attempt is made to obtain a
       GNF where one action is always followed by a
       variable. */
    {
      if (is_at(body))
      {
        data_expression timecondition=sort_bool::true_();
        process_expression body1=procstorealGNFbody(
                                   at(body).operand(),
                                   first,
                                   todo,
                                   regular,
                                   mode,
                                   freevars,
                                   variables_bound_in_sum);
        return distributeTime(
                 body1,
                 at(body).time_stamp(),
                 freevars,
                 timecondition);
      }
 
      if (is_choice(body))
      {
        const process_expression body1=procstorealGNFbody(choice(body).left(),first,todo,
                                       regular,mode,freevars,variables_bound_in_sum);
        const process_expression body2=procstorealGNFbody(choice(body).right(),first,todo,
                                       regular,mode,freevars,variables_bound_in_sum);
        return choice(body1,body2);
      }
 
      if (is_seq(body))
      {
        const process_expression body1=procstorealGNFbody(seq(body).left(),v,
                                       todo,regular,mode,freevars,variables_bound_in_sum);
        const process_expression body2=procstorealGNFbody(seq(body).right(),later,
                                       todo,regular,mode,freevars,variables_bound_in_sum);
        process_expression t3=putbehind(body1,body2);
        if ((regular) && (v==first))
        {
          /* We must transform t3 to regular form */
          t3=to_regular_form(t3,todo,freevars,variables_bound_in_sum);
        }
        return t3;
      }
 
      if (is_if_then(body))
      {
        const process_expression r=distribute_condition(
                                     procstorealGNFbody(if_then(body).then_case(),first,
                                         todo,regular,mode,freevars,variables_bound_in_sum),
                                     if_then(body).condition());
        return r;
      }
 
      if (is_sum(body))
      {
        const variable_list sumvars=sum(body).variables();
        std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
        variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
        return distribute_sum(sumvars,
                              procstorealGNFbody(sum(body).operand(),first,
                                  todo,regular,mode,sumvars+freevars,variables_bound_in_sum1));
      }
 
      if (is_stochastic_operator(body))
      {
        const stochastic_operator& sto=down_cast<const stochastic_operator>(body);
        const variable_list& sumvars=sto.variables();
        std::set<variable> variables_bound_in_sum1=variables_bound_in_sum;
        variables_bound_in_sum1.insert(sumvars.begin(),sumvars.end());
        return stochastic_operator(
                              sumvars,
                              sto.distribution(),
                              procstorealGNFbody(sto.operand(),v,
                                  todo,regular,mode,sumvars+freevars,variables_bound_in_sum1));
      }
 
      if (is_action(body))
      {
        return body;
      }
 
      if (is_sync(body))
      {
        return body;
      }
 
      if (is_process_instance_assignment(body))
      {
        process_identifier t=process_instance_assignment(body).identifier();
 
        if (v==later)
        {
          if (regular)
          {
            mode=mCRL;
          }
          todo.push_back(t);
          /* if ((!regular)||(mode=mCRL))
              todo.push_back(t);
                / * single = in `mode=mCRL' is important, otherwise crash
                   I do not understand the reason for this at this moment
                   JFG (9/5/2000) */
          return body;
        }
 
        objectdatatype& object=objectIndex(t);
        if (object.processstatus==mCRL)
        {
          todo.push_back(t);
          return process_expression();
        }
        /* The variable is a pCRL process and v==first, so,
           we must now substitute */
        procstorealGNFrec(t,first,todo,regular);
 
        maintain_variables_in_rhs< mutable_map_substitution<> > sigma;
        for(const assignment& a: static_cast<const process_instance_assignment&>(body).assignments())
        {
          sigma[a.lhs()]=a.rhs();
        }
        process_expression t3=substitute_pCRLproc(object.processbody,sigma);
        if (regular)
        {
          t3=to_regular_form(t3,todo,freevars,variables_bound_in_sum);
        }
 
        return t3;
      }
 
      if (is_delta(body))
      {
        return body;
      }
 
      if (is_tau(body))
      {
        return body;
      }
 
      if (is_merge(body))
      {
        procstorealGNFbody(process::merge(body).left(),later,
                           todo,regular,mode,freevars,variables_bound_in_sum);
        procstorealGNFbody(process::merge(body).right(),later,
                           todo,regular,mode,freevars,variables_bound_in_sum);
        return process_expression();
      }
 
      if (is_hide(body))
      {
        procstorealGNFbody(hide(body).operand(),later,todo,regular,mode,freevars,variables_bound_in_sum);
        return process_expression();
      }
 
      if (is_rename(body))
      {
        procstorealGNFbody(process::rename(body).operand(),later,todo,regular,mode,freevars,variables_bound_in_sum);
        return process_expression();
      }
 
      if (is_allow(body))
      {
        procstorealGNFbody(allow(body).operand(),later,todo,regular,mode,freevars,variables_bound_in_sum);
        return process_expression();
      }
 
      if (is_block(body))
      {
        procstorealGNFbody(block(body).operand(),later,todo,regular,mode,freevars,variables_bound_in_sum);
        return process_expression();
      }
 
      if (is_comm(body))
      {
        procstorealGNFbody(comm(body).operand(),later,todo,regular,mode,freevars,variables_bound_in_sum);
        return process_expression();
      }
 
      // The exception below can especially trigger on a process_instance as these ought to have
      // been removed earlier in favour of process_instance_assignments.
      throw mcrl2::runtime_error("unexpected process format in procstorealGNF " + process::pp(body) +".");
      return process_expression();
    }
 
 
    void procstorealGNFrec(
      const process_identifier& procIdDecl,
      const variableposition v,
      std::vector <process_identifier>& todo,
      const bool regular)
 
    /* Do a depth first search on process variables and substitute
       for the headvariable of a pCRL process, in case it is a process,
       such that we obtain a Greibach Normal Form. All pCRL processes will
       be labelled with GNF to indicate that they are in
       Greibach Normal Form. */
 
    {
      objectdatatype& object=objectIndex(procIdDecl);
      if (object.processstatus==pCRL)
      {
        object.processstatus=GNFbusy;
        std::set<variable> variables_bound_in_sum;
        const process_expression t=procstorealGNFbody(object.processbody,first,
                                   todo,regular,pCRL,object.parameters,variables_bound_in_sum);
        if (object.processstatus!=GNFbusy)
        {
          throw mcrl2::runtime_error("There is something wrong with recursion.");
        }
 
        object.processbody=t;
        object.processstatus=GNF;
        return;
      }
 
      if (object.processstatus==mCRL)
      {
        object.processstatus=mCRLbusy;
        std::set<variable> variables_bound_in_sum;
        const process_expression t=procstorealGNFbody(object.processbody,first,todo,
                                   regular,mCRL,object.parameters,variables_bound_in_sum);
        /* if the last result is not equal to NULL,
           the body of this process is itself a processidentifier */
 
        object.processstatus=mCRLdone;
        return;
      }
 
      if ((object.processstatus==GNFbusy) && (v==first))
      {
        throw mcrl2::runtime_error("Unguarded recursion in process " + process::pp(procIdDecl) +".");
      }
 
      if ((object.processstatus==GNFbusy)||
          (object.processstatus==GNF)||
          (object.processstatus==mCRLdone)||
          (object.processstatus==multiAction))
      {
        return;
      }
 
      if (object.processstatus==mCRLbusy)
      {
        throw mcrl2::runtime_error("Unguarded recursion in process " + process::pp(procIdDecl) +".");
      }
 
      throw mcrl2::runtime_error("strange process type: " + std::to_string(object.processstatus));
    }
 
    void procstorealGNF(const process_identifier& procsIdDecl,
                        const bool regular)
    {
      std::vector <process_identifier> todo;
      todo.push_back(procsIdDecl);
      for (; !todo.empty() ;)
      {
        const process_identifier pi=todo.back();
        todo.pop_back();
        procstorealGNFrec(pi,first,todo,regular);
      }
    }
 
 
    /**************** GENERaTE LPE **********************************/
    /*                                                              */
    /*                                                              */
    /*                                                              */
    /*                                                              */
    /*                                                              */
    /*                                                              */
    /****************************************************************/
 
 
    /**************** Make pCRL procs  ******************************/
 
    /* make_pCRL_procs searches for all process identifiers reachable from id in pCRL equations. */
 
    void make_pCRL_procs(const process_identifier& id,
                         std::set<process_identifier>& reachable_process_identifiers)
    {
      if (reachable_process_identifiers.count(id)==0)  // not found
      {
        reachable_process_identifiers.insert(id);
        make_pCRL_procs(objectIndex(id).processbody,reachable_process_identifiers);
      }
      return;
    }
 
    void make_pCRL_procs(const process_expression& t,
                         std::set<process_identifier>& reachable_process_identifiers)
    {
      if (is_choice(t))
      {
        make_pCRL_procs(choice(t).left(),reachable_process_identifiers);
        make_pCRL_procs(choice(t).right(),reachable_process_identifiers);
        return;
      }
 
      if (is_seq(t))
      {
        make_pCRL_procs(seq(t).left(),reachable_process_identifiers);
        make_pCRL_procs(seq(t).right(),reachable_process_identifiers);
        return;
      }
 
      if (is_if_then(t))
      {
        make_pCRL_procs(if_then(t).then_case(),reachable_process_identifiers);
        return;
      }
 
      if (is_sum(t))
      {
        make_pCRL_procs(sum(t).operand(),reachable_process_identifiers);
        return;
      }
 
      if (is_stochastic_operator(t))
      {
        make_pCRL_procs(stochastic_operator(t).operand(),reachable_process_identifiers);
        return;
      }
 
      if (is_process_instance_assignment(t))
      {
        make_pCRL_procs(atermpp::down_cast<process_instance_assignment>(t).identifier(), reachable_process_identifiers);
        return;
      }
 
      if (is_sync(t)||is_action(t)||is_tau(t)||is_delta(t)||is_at(t))
      {
        return;
      }
 
      throw mcrl2::runtime_error("unexpected process format " + process::pp(t) + " in make_pCRL_procs");
    }
 
    /**************** minimize_set_of_reachable_process_identifiers  ******************************/
 
    /* The process identifiers in reachable_process_identifiers have bodies and parameters lists
     * that can be the same. If that is the case, they are identified. The right hand sides are substituted to
     * reflect the identified processes. Example: P1 = a.P2, P3=a.P4, P2=b.Q, P4=b.Q. This reduces to P1 = a.P2, P2 = b.Q.
     * The result is a map from remaining process identifiers to their adapted process bodies.
     * The initial process was part of the reachable_process_identifiers and must be part of the map.
     */
 
    /* set_proc_identifier_map is an auxiliary procedure that effectively sets identfier_identifier_map[id1]:=... or
       identifier_identifier_map[id1]:=... in such a way that they map to the same element. In this way identifier_identifier_map
       acts as a representation of the equivalence set induced by equations id1==id2. A constraint is that
       initial_process may never occur as a left hand side. An invariant of identifier_identifier_map is
       that no id1 that occurs at the right of the map can occur at the left.
    */
 
    process_identifier get_last(const process_identifier& id, const std::map< process_identifier, process_identifier >& identifier_identifier_map)
    {
      process_identifier target_id=id;
      bool ready=false;
      do
      {
        const std::map< process_identifier, process_identifier >::const_iterator i=identifier_identifier_map.find(target_id);
        if (i==identifier_identifier_map.end())
        {
          ready=true;
        }
        else
        {
          target_id=i->second;
        }
      }
      while (!ready);
      return target_id;
    }
 
 
    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)
    {
      assert(id1_!=id2_);
 
      /* Take care that id1 is the last identifier or that id2 is arger than id1. This guarantees
         that there will be no loops in the mapping of identifiers. */
      // make_substitution sigma(identifier_identifier_map);
      process_identifier id1= get_last(id1_,identifier_identifier_map);
      process_identifier id2= get_last(id2_,identifier_identifier_map);
      if (id1==initial_process)
      {
        id1.swap(id2);
      }
      if (id1!=id2)
      {
        identifier_identifier_map[id1]=id2;
      }
    }
 
    void complete_proc_identifier_map(std::map< process_identifier, process_identifier >& identifier_identifier_map)
    {
      std::map< process_identifier, process_identifier > new_identifier_identifier_map;
      for(const std::pair<const process_identifier, process_identifier >& p: identifier_identifier_map)
      {
        new_identifier_identifier_map[p.first]=get_last(p.second,identifier_identifier_map);
      }
      identifier_identifier_map.swap(new_identifier_identifier_map);
#ifndef NDEBUG
      /* In the result no right hand side occurs as the left hand side of identifier_identifier_map */
      typedef std::pair< const process_identifier, process_identifier > identifier_identifier_pair;
      for(const identifier_identifier_pair& p: identifier_identifier_map)
      {
        assert(identifier_identifier_map.count(p.second)==0);
      }
#endif
    }
 
    struct make_substitution
    {
      typedef process_identifier result_type;
      typedef process_identifier argument_type;
      const std::map< process_identifier, process_identifier >& m_map;
 
      make_substitution(const std::map< process_identifier, process_identifier >& map)
        : m_map(map)
      {}
 
      process_identifier operator()(const process_identifier& id) const
      {
        const std::map< process_identifier, process_identifier >::const_iterator i=m_map.find(id);
        if (i==m_map.end()) // Not found
        {
          return id;
        }
        return i->second;
      }
    };
 
    std::set< process_identifier >
          minimize_set_of_reachable_process_identifiers(const std::set<process_identifier>& reachable_process_identifiers,
                                                        const process_identifier& initial_process)
    {
      assert(reachable_process_identifiers.count(initial_process)>0);
      typedef std::pair< variable_list, process_expression > parameters_process_pair;
      typedef std::map< std::pair< variable_list, process_expression >, process_identifier > mapping_type;
      typedef std::pair<const std::pair< variable_list, process_expression >, process_identifier > mapping_type_pair;
 
      /* First put the identifiers in reachable_process_identifiers in the process mapping */
      mapping_type process_mapping;
      std::map< process_identifier, process_identifier > identifier_identifier_map;
      for(const process_identifier& id: reachable_process_identifiers)
      {
        objectdatatype& object=objectIndex(id);
        const parameters_process_pair p(object.parameters,object.processbody);
        mapping_type::const_iterator i=process_mapping.find(p);
        if (i==process_mapping.end())   // Not found.
        {
          process_mapping[p]=id;
        }
        else
        {
          set_proc_identifier_map(identifier_identifier_map,id,i->second,initial_process);
        }
      }
      complete_proc_identifier_map(identifier_identifier_map);
 
      while (!identifier_identifier_map.empty())
      {
        /* Move the elements of process_mapping into new_process_mapping, under application
         * of the identifier_identifier_map. If this yields new process_identifiers to be identified store
         * these in new_proc_identifier_map. Do this until no process_identifiers are mapped onto
         * each other anymore. */
        std::map< process_identifier, process_identifier > new_identifier_identifier_map;
        mapping_type new_process_mapping;
        for(const mapping_type_pair& p: process_mapping)
        {
          const make_substitution sigma(identifier_identifier_map);
          const parameters_process_pair p_new(p.first.first, replace_process_identifiers( p.first.second, sigma));
          mapping_type::const_iterator i=new_process_mapping.find(p_new);
          if (i==new_process_mapping.end())   // Not found.
          {
            new_process_mapping[p_new]=sigma(p.second);
          }
          else
          {
            set_proc_identifier_map(new_identifier_identifier_map,sigma(p.second),sigma(i->second),initial_process);
          }
        }
        complete_proc_identifier_map(new_identifier_identifier_map);
        identifier_identifier_map.swap(new_identifier_identifier_map);
        process_mapping.swap(new_process_mapping);
      }
 
      /* Store the pairs from process mapping into result */
      /* std::map< process_identifier, process_expression > result;
      for(const mapping_type_pair& p: process_mapping)
      {
        result[p.second]=p.first.second;
      }
      assert(result.count(initial_process)>0);
      return result; */
      std::set< process_identifier > result;
      for(const mapping_type_pair& p: process_mapping)
      {
        result.insert(p.second);
        objectdatatype& object=objectIndex(p.second);
        object.processbody=p.first.second;
      }
      assert(result.count(initial_process)>0);
      return result;
    }
 
    /****************   remove_stochastic_operators_from_front **********************/
 
   class process_pid_pair
   {
     protected:
       process_expression m_process_body;
       process_identifier m_pid;
 
     public:
       process_pid_pair(const process_expression& process_body, const process_identifier& pid)
         : m_process_body(process_body), m_pid(pid)
       {}
 
       process_pid_pair(const process_pid_pair& other) = default;
       process_pid_pair(process_pid_pair&& other) = default;
       process_pid_pair& operator=(const process_pid_pair& other) = default;
       process_pid_pair& operator=(process_pid_pair&& other) = default;
 
       const process_expression& process_body() const
       {
         return m_process_body;
       }
 
       const process_identifier& process_id() const
       {
         return m_pid;
       }
    };  // end process_pid_pair
 
    /* Take the process expressions from process_equations and transform these such that
       no process equation has an initial distribution. The changed equations are reported
       back, including adapted parameter lists because sometimes the variables bound in the
       stochastic operators need to be added.
       The initial distribution of the initial process is reported back in
       initial_stochastic_distribution, including if necessary adapted sets of arguments. */
 
    std::set< process_identifier >
              remove_stochastic_operators_from_front(
                   const std::set< process_identifier >& reachable_process_identifiers,
                   process_identifier& initial_process_id, // If parameters change, another initial_process_id will be substituted.
                   stochastic_distribution& initial_stochastic_distribution)
    {
      /* First obtain the stochastic distribution for each process variable. */
      std::map< process_identifier, process_pid_pair > processes_with_stochastic_distribution_first;
      std::set< process_identifier > result;
      for(const process_identifier& p: reachable_process_identifiers)
      {
        objectdatatype& object = objectIndex(p);
        process_expression proc_=obtain_initial_distribution_term(object.processbody);
        if (!is_stochastic_operator(proc_))
        {
          processes_with_stochastic_distribution_first.insert(std::pair< process_identifier, process_pid_pair >(p, process_pid_pair(proc_,p)));
          result.insert(p);
        }
        else
        {
          const stochastic_operator& proc=down_cast<const stochastic_operator>(proc_);
          assert(!is_process_instance_assignment(proc.operand()));
          objectdatatype& object=objectIndex(p);
          maintain_variables_in_rhs< mutable_map_substitution<> > local_sigma;
          variable_list vars=proc.variables();
          alphaconvert(vars,local_sigma, vars + object.parameters, data_expression_list());
 
          const process_identifier newproc=newprocess(
                                           vars + object.parameters,
                                           process::replace_variables_capture_avoiding_with_an_identifier_generator(proc.operand(),
                                                                                       local_sigma,
                                                                                       fresh_identifier_generator),
                                           pCRL,
                                           canterminatebody(proc.operand()),
                                           containstimebody(proc.operand()));
          // calculate the substitution to be applied on proc.distribution() which is moved outside the
          // body the process.
          processes_with_stochastic_distribution_first.insert(
                        std::pair< process_identifier, process_pid_pair >
                                 (p,
                                  process_pid_pair(stochastic_operator(
                                                        vars,
                                                        replace_variables_capture_avoiding_alt(proc.distribution(), local_sigma),
                                                        proc.operand()),
                                                   newproc)));
          result.insert(newproc);
        }
      }
 
      for(const process_identifier& p: reachable_process_identifiers)
      {
        objectdatatype& object=objectIndex(processes_with_stochastic_distribution_first.at(p).process_id());
        assert(!is_stochastic_operator(object.processbody));
        object.processbody=transform_initial_distribution_term(object.processbody,processes_with_stochastic_distribution_first);
        assert(!is_stochastic_operator(object.processbody));
      }
 
      // Adapt the initial process
      process_expression initial_distribution=processes_with_stochastic_distribution_first.at(initial_process_id).process_body();
      if (is_stochastic_operator(initial_distribution))
      {
        const stochastic_operator sto=atermpp::down_cast<stochastic_operator>(initial_distribution);
        initial_stochastic_distribution = stochastic_distribution(sto.variables(), sto.distribution());
        initial_process_id=processes_with_stochastic_distribution_first.at(initial_process_id).process_id();
      }
      else
      {
        initial_stochastic_distribution = stochastic_distribution(variable_list(), sort_real::real_one());
      }
 
      return result;
    }
 
 
    /**************** Collectparameterlist ******************************/
 
    bool alreadypresent(variable& var,const variable_list& vl)
    {
      /* Note: variables can be different, although they have the
         same string, due to different types. If they have the
         same string, but different types, the conflict must
         be resolved by renaming the name of the variable */
 
      if (vl.empty())
      {
        return false;
      }
      const variable& var1=vl.front();
      assert(is_variable(var1));
 
      /* The variable with correct type is present: */
      if (var==var1)
      {
        return true;
      }
 
      assert(var.name()!=var1.name());
 
      /* otherwise it can be present in vl */
      return alreadypresent(var,vl.tail());
    }
 
    variable_list joinparameters(const variable_list& par1,
                                 const variable_list& par2)
    {
      if (par2.empty())
      {
        return par1;
      }
 
      variable var2=par2.front();
      assert(is_variable(var2));
 
      variable_list result=joinparameters(par1,par2.tail());
      if (alreadypresent(var2,par1))
      {
        return result;
      }
 
      result.push_front(var2);
      return result;
    }
 
    variable_list collectparameterlist(const std::set< process_identifier >& pCRLprocs)
    {
      variable_list parameters;
      for (const process_identifier& p: pCRLprocs)
      {
        const objectdatatype& object=objectIndex(p);
        parameters=joinparameters(parameters,object.parameters);
      }
      return parameters;
    }
 
    /****************  Declare local datatypes  ******************************/
 
    void declare_control_state(
      const std::set < process_identifier >& pCRLprocs)
    {
      create_enumeratedtype(pCRLprocs.size());
    }
 
    class stackoperations
    {
      public:
        variable_list parameter_list;
        sort_expression stacksort;
        sort_expression_list sorts;
        function_symbol_list get;
        data::function_symbol push;
        data::function_symbol emptystack;
        data::function_symbol empty;
        data::function_symbol pop;
        data::function_symbol getstate;
        stackoperations* next;
 
        // Stack operations are not supposed to be copied.
        stackoperations(const stackoperations& )=delete;
        stackoperations& operator=(const stackoperations& )=delete;
 
        stackoperations(const variable_list& pl,
                        specification_basic_type& spec)
        {
          parameter_list=pl;
          next=spec.stack_operations_list;
          spec.stack_operations_list=this;
 
          //create structured sort
          //  Stack = struct emptystack?is_empty
          //               | push(getstate: Pos, getx1: S1, ..., getxn: Sn, pop: Stack)
          //               ;
 
          basic_sort stack_sort_alias(spec.fresh_identifier_generator("Stack"));
          structured_sort_constructor_argument_vector sp_push_arguments;
          for (const variable& v: pl)
          {
            sp_push_arguments.push_back(structured_sort_constructor_argument(spec.fresh_identifier_generator("get" + std::string(v.name())), v.sort()));
            sorts.push_front(v.sort());
          }
          sp_push_arguments.push_back(structured_sort_constructor_argument(spec.fresh_identifier_generator("pop"), stack_sort_alias));
          sorts=reverse(sorts);
          structured_sort_constructor sc_push(spec.fresh_identifier_generator("push"), sp_push_arguments);
          structured_sort_constructor sc_emptystack(spec.fresh_identifier_generator("emptystack"),spec.fresh_identifier_generator("isempty"));
 
          structured_sort_constructor_vector constructors(1,sc_push);
          constructors.push_back(sc_emptystack);
          //add data declarations for structured sort
          spec.data.add_alias(alias(stack_sort_alias,structured_sort(constructors)));
          stacksort=data::normalize_sorts(stack_sort_alias,spec.data);
          push=sc_push.constructor_function(stack_sort_alias);
          emptystack=sc_emptystack.constructor_function(stack_sort_alias);
          empty=sc_emptystack.recogniser_function(stack_sort_alias);
          const std::vector< data::function_symbol > projection_functions =
            sc_push.projection_functions(stack_sort_alias);
          pop=projection_functions.back();
          getstate=projection_functions.front();
          get=function_symbol_list(projection_functions.begin()+1,projection_functions.end()-1);
        }
 
        ~stackoperations()
        {
        }
    };
 
    class stacklisttype
    {
      public:
        stackoperations* opns;
        variable_list parameters;
        variable stackvar;
        std::size_t no_of_states;
        /* the boolean state variables occur in reverse
           order, i.e. the least significant first, whereas
           in parameter lists, the order is reversed. */
        variable_list booleanStateVariables;
 
 
        /* All datatypes for different stacks that are being generated
           are stored in the following list, such that it can be investigated
           whether a suitable stacktype already exist, before generating a new
           one */
 
        stacklisttype(const stacklisttype& )=delete;
        stacklisttype& operator=(const stacklisttype& )=delete;
 
 
        stackoperations* find_suitable_stack_operations(
          const variable_list& parameters,
          stackoperations* stack_operations_list)
        {
          if (stack_operations_list==nullptr)
          {
            return nullptr;
          }
          if (parameters==stack_operations_list->parameter_list)
          {
            return stack_operations_list;
          }
          return find_suitable_stack_operations(parameters,stack_operations_list->next);
        }
 
        stacklisttype(const variable_list& parlist,
                      specification_basic_type& spec,
                      const bool regular,
                      const std::set < process_identifier >& pCRLprocs,
                      const bool singlecontrolstate)
        {
          assert(pCRLprocs.size()>0);
          parameters=parlist;
 
          no_of_states=pCRLprocs.size();
          process_identifier last= *pCRLprocs.begin();
          const std::string s3((spec.options.statenames)?std::string(last.name()):std::string("s"));
          if ((spec.options.binary) && (spec.options.newstate))
          {
            std::size_t i=spec.upperpowerof2(no_of_states);
            for (; i>0 ; i--)
            {
              variable name(spec.fresh_identifier_generator("bst"),sort_bool::bool_());
              spec.insertvariable(name,true);
              booleanStateVariables.push_front(name);
            }
          }
 
          if (regular)
          {
            opns=nullptr;
            if (spec.options.newstate)
            {
              if (!spec.options.binary)
              {
                if (!singlecontrolstate)
                {
                  const std::size_t e=spec.create_enumeratedtype(no_of_states);
                  stackvar=variable(spec.fresh_identifier_generator(s3), spec.enumeratedtypes[e].sortId);
                }
                else
                {
                  /* Generate a stackvariable that is never used */
                  stackvar=variable(spec.fresh_identifier_generator("Never_used"), sort_bool::bool_());
                }
              }
              else
              {
                stackvar=variable(spec.fresh_identifier_generator(s3),sort_bool::bool_());
              }
            }
            else
            {
              stackvar=variable(spec.fresh_identifier_generator(s3), sort_pos::pos());
            }
            spec.insertvariable(stackvar,true);
          }
          else
          {
            if (spec.options.newstate)
            {
              throw mcrl2::runtime_error("cannot combine stacks with " +
                                         (spec.options.binary?std::string("binary"):std::string("an enumerated type")));
            }
            opns=find_suitable_stack_operations(parlist,spec.stack_operations_list);
 
            if (opns!=nullptr)
            {
              stackvar=variable(spec.fresh_identifier_generator(s3),opns->stacksort);
              spec.insertvariable(stackvar,true);
            }
            else
            {
              variable_list temp=parlist;
              temp.push_front(variable("state",sort_pos::pos()));
              opns=(stackoperations*) new stackoperations(temp,spec);
              stackvar = variable(spec.fresh_identifier_generator(s3), opns->stacksort);
              spec.insertvariable(stackvar,true);
            }
          }
        }
 
        ~stacklisttype()
        {
        }
 
    };
 
    bool is_global_variable(const data_expression& d) const
    {
      return is_variable(d) && global_variables.count(atermpp::down_cast<variable>(d)) > 0;
    }
 
    data_expression getvar(const variable& var,
                           const stacklisttype& stack)
    {
      /* first search whether the variable is a free process variable */
      if (global_variables.count(var)>0)
      {
        return var;
      }
 
      /* otherwise find out whether the variable matches a parameter */
      function_symbol_list::const_iterator getmappings=stack.opns->get.begin();
      for (variable_list::const_iterator walker=stack.parameters.begin() ;
           walker!=stack.parameters.end() ; ++walker,++getmappings)
      {
        if (*walker==var)
        {
          return application(*getmappings,stack.stackvar);
        }
        assert(getmappings!=stack.opns->get.end());
      }
      assert(0); /* We cannot end up here, because that means that we
                    are looking for in non-existing variable */
      return var;
    }
 
    assignment_list processencoding(
      std::size_t i,
      const assignment_list& t1,
      const stacklisttype& stack)
    {
      assert(i>0);
      assignment_list t(t1);
      if (!options.newstate)
      {
        assignment_list result=t;
        result.push_front(assignment(stack.stackvar,sort_pos::pos(i)));
        return result;
      }
 
      i=i-1; /* below we count from 0 instead from 1 as done in the
                first version of the prover */
 
      if (!options.binary)
      {
        const std::size_t e=create_enumeratedtype(stack.no_of_states);
        data_expression_list l=enumeratedtypes[e].elementnames;
        for (; i>0 ; i--)
        {
          assert(l.size()>0);
          l.pop_front();
        }
        assignment_list result=t;
        assert(l.size()>0);
        result.push_front(assignment(stack.stackvar,l.front()));
        return result;
      }
      /* else a sequence of boolean values needs to be generated,
         representing the value i, when there are l->n elements */
      {
        std::size_t k=upperpowerof2(stack.no_of_states);
        variable_list::const_iterator boolean_state_variables=stack.booleanStateVariables.begin();
        for (; k>0 ; k--, ++boolean_state_variables)
        {
          if ((i % 2)==0)
          {
            t.push_front(assignment(*boolean_state_variables,sort_bool::false_()));
            i=i/2;
          }
          else
          {
            t.push_front(assignment(*boolean_state_variables,sort_bool::true_()));
            i=(i-1)/2;
          }
        }
        return t;
      }
    }
 
    data_expression_list processencoding(
      std::size_t i,
      const data_expression_list& t1,
      const stacklisttype& stack)
    {
      data_expression_list t(t1);
      if (!options.newstate)
      {
        data_expression_list result=t;
        result.push_front(sort_pos::pos(i));
        return result;
      }
 
      i=i-1; /* below we count from 0 instead from 1 as done in the
                first version of the linearizer */
 
      if (!options.binary)
      {
        const std::size_t e=create_enumeratedtype(stack.no_of_states);
        data_expression_list l(enumeratedtypes[e].elementnames);
        for (; i>0 ; i--)
        {
          l.pop_front();
        }
        data_expression_list result=t;
        result.push_front(l.front());
        return result;
      }
      /* else a sequence of boolean values needs to be generated,
         representing the value i, when there are l->n elements */
      {
        std::size_t k=upperpowerof2(stack.no_of_states);
        variable_list::const_iterator boolean_state_variables=stack.booleanStateVariables.begin();
        for (; k>0 ; k--, ++boolean_state_variables)
        {
          if ((i % 2)==0)
          {
            t.push_front(sort_bool::false_());
            i=i/2;
          }
          else
          {
            t.push_front(sort_bool::true_());
            i=(i-1)/2;
          }
        }
        return t;
      }
    }
 
    data_expression correctstatecond(
      const process_identifier& procId,
      const std::set < process_identifier >& pCRLproc,
      const stacklisttype& stack,
      int regular)
    {
      std::size_t i=1;
      for (const process_identifier& p: pCRLproc)
      {
        if (p==procId)
        {
          break;
        }
        ++i;
      }
      /* i is the index of the current process */
 
      if (!options.newstate)
      {
        if (regular)
        {
          return equal_to(stack.stackvar, processencoding(i,assignment_list(),stack).front().rhs());
        }
        return equal_to(
                 application(stack.opns->getstate,stack.stackvar),
                 processencoding(i,assignment_list(),stack).front().rhs());
      }
 
      if (!options.binary) /* Here a state encoding using enumerated types
                              must be declared */
      {
        create_enumeratedtype(stack.no_of_states);
        if (regular)
        {
          return equal_to(stack.stackvar,
                          processencoding(i,assignment_list(),stack).front().rhs());
        }
        return equal_to(
                 application(stack.opns->getstate, stack.stackvar),
                 processencoding(i,assignment_list(),stack).front().rhs());
      }
 
      /* in this case we must encode the condition using
         boolean variables */
 
      const variable_list vars=stack.booleanStateVariables;
 
      i=i-1; /* start counting from 0, instead from 1 */
      data_expression t3(sort_bool::true_());
      for (const variable& v: vars)
      {
        if ((i % 2)==0)
        {
          t3=lazy::and_(lazy::not_(v),t3);
          i=i/2;
        }
        else
        {
          t3=lazy::and_(v,t3);
          i=(i-1)/2;
        }
 
      }
      assert(i==0);
      return t3;
    }
 
    data_expression adapt_term_to_stack(
      const data_expression& t,
      const stacklisttype& stack,
      const variable_list& vars,
      const variable_list& stochastic_variables)
    {
      if (is_function_symbol(t))
      {
        return t;
      }
 
      if (is_machine_number(t))
      {
        return t;
      }
 
      if (is_variable(t))
      {
        if (std::find(vars.begin(),vars.end(),t)!=vars.end())
        {
          /* t occurs in vars, so, t does not have to be reconstructed
             from the stack */
          return t;
        }
        else
        if (std::find(stochastic_variables.begin(),stochastic_variables.end(),t)!=stochastic_variables.end())
        {
          /* t occurs in stochastic_variables, so, t does not have to be reconstructed
             from the stack */
          return t;
        }
        else
        {
          return getvar(atermpp::down_cast<variable>(t), stack);
        }
      }
 
      if (is_application(t))
      {
        const application&a=atermpp::down_cast<application>(t);
        return application(
                 adapt_term_to_stack(a.head(),stack,vars,stochastic_variables),
                 adapt_termlist_to_stack(a.begin(),a.end(),stack,vars,stochastic_variables));
      }
 
      if (is_abstraction(t))
      {
        const abstraction& abs_t=down_cast<abstraction>(t);
        return abstraction(
                 abs_t.binding_operator(),
                 abs_t.variables(),
                 adapt_term_to_stack(abs_t.body(),stack,abs_t.variables() + vars,stochastic_variables));
      }
 
      if (is_where_clause(t))
      {
        const where_clause where_t(t);
        const assignment_list old_assignments=reverse(where_t.assignments());
        variable_list new_vars=vars;
        assignment_list new_assignments;
        for (const assignment& a: old_assignments)
        {
          new_vars.push_front(a.lhs());
          new_assignments.push_front(
                             assignment(
                               a.lhs(),
                               adapt_term_to_stack(a.rhs(),stack,vars,stochastic_variables)));
 
        }
        return where_clause(
                 adapt_term_to_stack(where_t,stack,new_vars,stochastic_variables),
                 new_assignments);
 
      }
 
      assert(0);  // expected a term;
      return t;   // in case of non-debug mode, try to return something as decent as possible.
    }
 
    template <typename Iterator>
    data_expression_vector adapt_termlist_to_stack(
      Iterator begin,
      const Iterator& end,
      const stacklisttype& stack,
      const variable_list& vars,
      const variable_list& stochastic_variables)
    {
      data_expression_vector result;
      for (; begin != end; ++begin)
      {
        result.push_back(adapt_term_to_stack(*begin,stack, vars,stochastic_variables));
      }
      return result;
    }
 
 
    action_list adapt_multiaction_to_stack_rec(
      const action_list& multiAction,
      const stacklisttype& stack,
      const variable_list& vars)
    {
      if (multiAction.empty())
      {
        return multiAction;
      }
 
      const action act=action(multiAction.front());
 
      action_list result=adapt_multiaction_to_stack_rec(multiAction.tail(),stack,vars);
 
      const data_expression_vector vec(adapt_termlist_to_stack(
                            act.arguments().begin(),
                            act.arguments().end(),
                            stack,
                            vars,
                            variable_list()));
      result.push_front(action(act.label(),data_expression_list(vec.begin(),vec.end())));
      return result;
    }
 
    action_list adapt_multiaction_to_stack(
      const action_list& multiAction,
      const stacklisttype& stack,
      const variable_list& vars)
    {
      return adapt_multiaction_to_stack_rec(multiAction,stack,vars);
    }
 
    data_expression representative_generator_internal(const sort_expression& s, const bool allow_dont_care_var=true)
    {
      if ((!options.noglobalvars) && allow_dont_care_var)
      {
        const variable newVariable(fresh_identifier_generator("dc"),s);
        insertvariable(newVariable,true);
        global_variables.insert(newVariable);
        return newVariable;
      }
      return representative_generator(data)(s);
    }
 
    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)
    {
      /* We generate the value for variable s in the list of
         the parameters of the process. If s is equal to some
         variable in pars, it is an argument of the current
         process, and it must be replaced by the corresponding
         argument in args.
           If s does not occur in pars, it must be replaced
         by a dummy value.
      */
      for (const assignment& a: args)
      {
        if (s==a.lhs())
        {
          return adapt_term_to_stack(a.rhs(),stack,vars,stochastic_variables);
        }
      }
 
      if (free_variables_in_body.find(s)==free_variables_in_body.end())
      {
        const data_expression result=representative_generator_internal(s.sort());
        return adapt_term_to_stack(result,stack,vars,stochastic_variables);
      }
      return adapt_term_to_stack(s,stack,vars,stochastic_variables);
    }
 
 
    data_expression_list findarguments(