mCRL2
Loading...
Searching...
No Matches
lts2lps.h
Go to the documentation of this file.
1// Author(s): Frank Stappers, Jan Friso Groote
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
12
13
14#ifndef MCRL2_LTS_LTS2LPS_H
15#define MCRL2_LTS_LTS2LPS_H
16
17#include "mcrl2/lps/io.h"
19
20
21namespace mcrl2
22{
23namespace lts
24{
25
26using namespace mcrl2::lps;
27using namespace mcrl2::data;
28
33{
34 action_summand_vector action_summands;
35 const variable process_parameter("x",mcrl2::data::sort_pos::pos());
36 const variable_list process_parameters = { process_parameter };
37 const std::set< data::variable> global_variables;
38 // Add a single delta.
41 );
42
43 const std::vector<transition>& trans=l.get_transitions();
44 for (std::vector<transition>::const_iterator r=trans.begin(); r!=trans.end(); ++r)
45 {
46 const lps::multi_action actions=l.action_label(r->label());
47
48 assignment_list assignments;
49 if (r->from()!=r->to())
50 {
51 assignments=push_back(assignments,assignment(process_parameter,sort_pos::pos(r->to()+1)));
52 }
53
54 const action_summand summand(variable_list(),
55 equal_to(process_parameter,sort_pos::pos(r->from()+1)),
56 actions,
57 assignments);
58 action_summands.push_back(summand);
59 }
60
61 const linear_process lps1(process_parameters,deadlock_summands,action_summands);
62 const specification spec(l.data(),l.action_label_declarations(),global_variables,lps1,initial_process);
63
64 return spec;
65}
66
74 const data_specification& data,
75 const process::action_label_list& action_labels,
76 const variable_list& process_parameters)
77{
78 lts_lts_t l2;
79 mcrl2::lts::detail::lts_convert(l1,l2,data,action_labels,process_parameters);
80 return transform_lts2lps(l2);
81}
82
89
91 const data_specification& data,
92 const process::action_label_list& action_labels,
93 const variable_list& process_parameters)
94{
95 lts_lts_t l2;
96 mcrl2::lts::detail::lts_convert(l1,l2,data,action_labels,process_parameters);
97 return transform_lts2lps(l2);
98}
99
100} // namespace lts
101} // namespace mcrl2
102
103#endif // MCRL2_LTS_LTS2LPS_H
\brief Assignment of a data expression to a variable
Definition assignment.h:91
\brief A data variable
Definition variable.h:28
LPS summand containing a multi-action.
LPS summand containing a deadlock.
Represents a deadlock.
Definition deadlock.h:26
\brief A timed multi-action
Linear process specification.
const data::data_specification & data() const
Returns the mCRL2 data specification of this LTS.
Definition lts_lts.h:307
const process::action_label_list & action_label_declarations() const
Return action label declarations stored in this LTS.
Definition lts_lts.h:314
A simple labelled transition format with only strings as action labels.
Definition lts_aut.h:70
The class lts_fsm_t contains labelled transition systems in .fsm format.
Definition lts_fsm.h:248
This class contains labelled transition systems in .lts format.
Definition lts_lts.h:374
ACTION_LABEL_T action_label(const labels_size_type action) const
Gets the label of an action.
Definition lts.h:470
const std::vector< transition > & get_transitions() const
Gets a const reference to the vector of transitions of the current lts.
Definition lts.h:526
states_size_type initial_state() const
Gets the initial state number of this LTS.
Definition lts.h:326
IO routines for linear process specifications.
This file contains lts_convert routines that translate different lts formats into each other.
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos.h:45
Namespace for all data library functionality.
Definition abstraction.h:22
atermpp::term_list< variable > variable_list
\brief list of variables
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
The main namespace for the LPS library.
std::vector< deadlock_summand > deadlock_summand_vector
\brief vector of deadlock_summands
std::vector< action_summand > action_summand_vector
\brief vector of action_summands
void lts_convert(const lts< STATE_LABEL1, ACTION_LABEL1, LTS_BASE1 > &lts_in, lts< STATE_LABEL2, ACTION_LABEL2, LTS_BASE2 > &lts_out)
lps::specification transform_lts2lps(const lts_lts_t &l)
transform an lts in lts format into a linear process.
Definition lts2lps.h:32
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72