lts2lps.h

Go to the documentation of this file.

// Author(s): Frank Stappers, 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)
//
 
 
#ifndef MCRL2_LTS_LTS2LPS_H
#define MCRL2_LTS_LTS2LPS_H
 
#include "mcrl2/lps/io.h"
#include "mcrl2/lts/detail/lts_convert.h"
 
 
namespace mcrl2
{
namespace lts
{
 
using namespace mcrl2::lps;
using namespace mcrl2::data;
 
lps::specification transform_lts2lps(const lts_lts_t& l)
{
  action_summand_vector action_summands;
  const variable process_parameter("x",mcrl2::data::sort_pos::pos());
  const variable_list process_parameters = { process_parameter };
  const std::set< data::variable> global_variables;
  // Add a single delta.
  const deadlock_summand_vector deadlock_summands(1,deadlock_summand(variable_list(), sort_bool::true_(), deadlock()));
  const process_initializer initial_process(data::data_expression_list{sort_pos::pos(l.initial_state()+1)}
  );
 
  const std::vector<transition>& trans=l.get_transitions();
  for (std::vector<transition>::const_iterator r=trans.begin(); r!=trans.end(); ++r)
  {
    const lps::multi_action actions=l.action_label(r->label());
  
    assignment_list assignments;
    if (r->from()!=r->to())
    {
      assignments=push_back(assignments,assignment(process_parameter,sort_pos::pos(r->to()+1)));
    }
  
    const action_summand summand(variable_list(),
                                 equal_to(process_parameter,sort_pos::pos(r->from()+1)),
                                 actions,
                                 assignments);
    action_summands.push_back(summand);
  }
  
  const linear_process lps1(process_parameters,deadlock_summands,action_summands);
  const specification spec(l.data(),l.action_label_declarations(),global_variables,lps1,initial_process);
  
  return spec;
}
 
lps::specification transform_lts2lps(const lts_aut_t& l1, 
                                     const data_specification& data, 
                                     const process::action_label_list& action_labels,
                                     const variable_list& process_parameters)
{
  lts_lts_t l2;
  mcrl2::lts::detail::lts_convert(l1,l2,data,action_labels,process_parameters);  
  return transform_lts2lps(l2);
}
 
 
lps::specification transform_lts2lps(const lts_fsm_t& l1, 
                                     const data_specification& data, 
                                     const process::action_label_list& action_labels,
                                     const variable_list& process_parameters)
{
  lts_lts_t l2;
  mcrl2::lts::detail::lts_convert(l1,l2,data,action_labels,process_parameters);  
  return transform_lts2lps(l2);
}
 
} // namespace lts
} // namespace mcrl2
 
#endif // MCRL2_LTS_LTS2LPS_H