mCRL2
Searching...
No Matches
probabilistic_lts.h
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg, Jan Friso Groote
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
6// (See accompanying file LICENSE_1_0.txt or copy at
8//
9
18#ifndef MCRL2_LTS_PROBABILISTIC_LTS_H
19#define MCRL2_LTS_PROBABILISTIC_LTS_H
20
21#include "mcrl2/lts/lts.h"
23
24
25namespace mcrl2
26{
27
28namespace lts
29{
30
45template < class STATE_LABEL_T, class ACTION_LABEL_T, class PROBABILISTIC_STATE_T, class LTS_BASE >
46class probabilistic_lts: public lts<STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE>
47{
48 public:
49
51
54 typedef PROBABILISTIC_STATE_T probabilistic_state_t;
55
58 typedef typename super::base_t base_t ;
62
65 static constexpr bool is_probabilistic_lts=true;
66
67 protected:
68
69 std::vector<PROBABILISTIC_STATE_T> m_probabilistic_states;
70 PROBABILISTIC_STATE_T m_init_probabilistic_state;
71
72 /* This function is made protected to prevent its use in a probabilistic transition system */
74 {
75 return super::initial_state();
76 }
77
78 /* This function is made protected to prevent its use in a probabilistic transition system */
80 {
82 }
83
84 public:
85
89 {}
90
93 probabilistic_lts(const probabilistic_lts& other) = default;
94
98
102
106
109 bool operator==(const probabilistic_lts& other) const
110 {
111 return super::operator==(static_cast<const super&>(other)) &&
114 }
115
119 {
120 super::swap(other);
123 }
124
127 const PROBABILISTIC_STATE_T& initial_probabilistic_state() const
128 {
130 }
131
135 void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T& state)
136 {
137 // Prevent that the initial state of the lts, which is not used in a probabilistic state
138 // has an arbitrary value.
141 }
142
143
147 {
148 return m_probabilistic_states.size();
149 }
150
155 states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T& s)
156 {
157 const states_size_type label_index=m_probabilistic_states.size();
158 m_probabilistic_states.push_back(s);
159 return label_index;
160 }
161
168 {
169 const states_size_type label_index=m_probabilistic_states.size();
170 m_probabilistic_states.emplace_back();
171 m_probabilistic_states.back().swap(s);
172 return label_index;
173 }
174
178 void set_probabilistic_state(const states_size_type index, const PROBABILISTIC_STATE_T& s)
179 {
180 assert(index<m_probabilistic_states.size());
181 m_probabilistic_states[index] = s;
182 }
183
187 const PROBABILISTIC_STATE_T& probabilistic_state(const states_size_type index) const
188 {
189 assert(index < m_probabilistic_states.size());
190 return m_probabilistic_states[index];
191 }
192
196 {
198 }
199
203 void clear()
204 {
205 super::clear();
207 m_probabilistic_states.shrink_to_fit();
208 }
209};
210
211}
212}
213
214#endif // MCRL2_LTS_LTS_H
Read-only balanced binary tree of terms.
A class that contains a labelled transition system.
Definition lts.h:83
ACTION_LABEL_T action_label_t
The type of action labels.
Definition lts.h:92
void set_initial_state(const states_size_type state)
Sets the initial state number of this LTS.
Definition lts.h:334
std::vector< STATE_LABEL_T >::size_type states_size_type
The sort that contains the indices of states.
Definition lts.h:100
std::vector< ACTION_LABEL_T >::size_type labels_size_type
The sort that represents the indices of labels.
Definition lts.h:104
STATE_LABEL_T state_label_t
The type of state labels.
Definition lts.h:88
void clear()
Clear the transitions system.
Definition lts.h:514
bool operator==(const lts &other) const
Standard equality operator.
Definition lts.h:209
LTS_BASE base_t
The type of the used lts base.
Definition lts.h:96
std::vector< transition >::size_type transitions_size_type
The sort that contains indices of transitions.
Definition lts.h:108
states_size_type initial_state() const
Gets the initial state number of this LTS.
Definition lts.h:326
void swap(lts &l)
Swap this lts with the supplied supplied LTS.
Definition lts.h:222
A class that contains a labelled transition system.
probabilistic_lts(probabilistic_lts &&other)=default
Standard move constructor.
void set_initial_probabilistic_state(const PROBABILISTIC_STATE_T &state)
Sets the probabilistic initial state number of this LTS.
const PROBABILISTIC_STATE_T & initial_probabilistic_state() const
Gets the initial state number of this LTS.
super::transitions_size_type transitions_size_type
bool operator==(const probabilistic_lts &other) const
Standard equality operator.
void swap(probabilistic_lts &other)
Swap this lts with the supplied supplied LTS.
super::states_size_type states_size_type
labels_size_type num_probabilistic_states() const
Gets the number of probabilistic states of this LTS.
static constexpr bool is_probabilistic_lts
An indicator that this is a probabilistic lts.
void clear_probabilistic_states()
Clear the probabilistic states in this probabilistic transitions system.
lts< STATE_LABEL_T, ACTION_LABEL_T, LTS_BASE > super
Adds a probabilistic state to this LTS and resets the state to empty.
void set_initial_state(const states_size_type s)
void clear()
Clear the transitions system.
probabilistic_lts & operator=(probabilistic_lts &&other)=default
Standard assignment move operator.
PROBABILISTIC_STATE_T probabilistic_state_t
The type of probabilistic labels.
probabilistic_lts & operator=(const probabilistic_lts &other)=default
Standard assignment operator.
std::vector< PROBABILISTIC_STATE_T > m_probabilistic_states
probabilistic_lts(const probabilistic_lts &other)=default
Standard copy constructor.
states_size_type add_probabilistic_state(const PROBABILISTIC_STATE_T &s)
Adds a probabilistic state to this LTS.
super::state_label_t state_label_t
states_size_type initial_state() const
PROBABILISTIC_STATE_T m_init_probabilistic_state
super::labels_size_type labels_size_type
super::action_label_t action_label_t
const PROBABILISTIC_STATE_T & probabilistic_state(const states_size_type index) const
Gets the probabilistic label of an index.
probabilistic_lts()
Creates an empty LTS.
void set_probabilistic_state(const states_size_type index, const PROBABILISTIC_STATE_T &s)
Sets the probabilistic label corresponding to some index.
The file containing the core class for transition systems.
atermpp::term_balanced_tree< data::data_expression > state
Definition state.h:24
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72