mCRL2
Loading...
Searching...
No Matches
lts.h
Go to the documentation of this file.
1// Author(s): 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//
9
18#ifndef MCRL2_LTS_LTS_H
19#define MCRL2_LTS_LTS_H
20
21#include <string>
22#include <vector>
23#include <cstdio>
24#include <iostream>
25#include <algorithm>
26#include <cassert>
27#include <set>
28#include <map>
30#include "mcrl2/lts/lts_type.h"
31
32
33namespace mcrl2
34{
35
40namespace lts
41{
42
44{
45 public:
48 {
49 return lts_none;
50 }
51
54 {
55 // Does intentionally not provide any action.
56 }
57
60 bool operator==(const lts_default_base&) const
61 {
62 return true;
63 }
64};
65
66
81template < class STATE_LABEL_T, class ACTION_LABEL_T, class LTS_BASE = lts_default_base>
82class lts: public LTS_BASE
83{
84 public:
85
88 typedef STATE_LABEL_T state_label_t;
89
92 typedef ACTION_LABEL_T action_label_t;
93
96 typedef LTS_BASE base_t;
97
100 typedef typename std::vector < STATE_LABEL_T >::size_type states_size_type;
101
104 typedef typename std::vector < ACTION_LABEL_T >::size_type labels_size_type;
105
108 typedef typename std::vector<transition>::size_type transitions_size_type;
109
112 static constexpr bool is_probabilistic_lts=false;
113
114 protected:
115
118 std::vector<transition> m_transitions;
119 std::vector<STATE_LABEL_T> m_state_labels;
120 std::vector<ACTION_LABEL_T> m_action_labels; // At position 0 we always find the label that corresponds to tau.
121 // The following set contains the labels that are recorded as being hidden.
122 // This allows tools to apply reductions assuming that these actions are hidden, but still provide
123 // feedback, for instance using counter examples, using the original action name.
124 std::set<labels_size_type> m_hidden_label_set;
125
126 // Auxiliary function. Rename the labels according to the action_rename_map;
127 void rename_labels(const std::map<labels_size_type, labels_size_type>& action_rename_map)
128 {
129 if (action_rename_map.size()>0) // Check whether there is something to rename.
130 {
132 {
133 auto i = action_rename_map.find(t.label());
134 if (i!=action_rename_map.end())
135 {
136 t=transition(t.from(),i->second,t.to());
137 }
138 }
139 }
140 }
141
142 // Auxiliary function. a is the partially hidden action label of which the original
143 // action label occurred at position i.
144 // If label a exists at position j, set action_rename_map[i]:=j;
145 // if a does not occur, adapt the action labels by setting label i to j.
146 void store_action_label_to_be_renamed(const ACTION_LABEL_T& a,
147 const labels_size_type i,
148 std::map<labels_size_type, labels_size_type>& action_rename_map)
149 {
150 bool found=false;
151 for (labels_size_type j=0; !found && j< num_action_labels(); ++j)
152 {
153 if (a==action_label(j))
154 {
155 if (i!=j)
156 {
157 action_rename_map[i]=j;
158 }
159 found=true;
160 }
161 }
162 if (!found) // a!=action_label(j) for any j, then rename action_label(i) to a.
163 {
164 set_action_label(i,a);
165 }
166 }
167
168 public:
169
173 : m_nstates(0)
174 {
175 m_action_labels.push_back(ACTION_LABEL_T::tau_action());
176 }
177
180 lts(const lts& l):
181 LTS_BASE(l),
188 {
189 assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
190 }
191
194 lts& operator=(const lts& l)
195 {
196 static_cast<LTS_BASE&>(*this)=l;
197 m_nstates = l.m_nstates;
198 m_init_state = l.m_init_state;
199 m_transitions = l.m_transitions;
200 m_state_labels = l.m_state_labels;
201 m_action_labels = l.m_action_labels;
202 m_hidden_label_set = l.m_hidden_label_set;
203 assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
204 return *this;
205 }
206
209 bool operator==(const lts& other) const
210 {
211 return static_cast<const LTS_BASE&>(*this)==static_cast<const LTS_BASE&>(other) &&
212 m_nstates == other.m_nstates &&
213 m_init_state == other.m_init_state &&
214 m_transitions == other.m_transitions &&
215 m_state_labels == other.m_state_labels &&
216 m_action_labels == other.m_action_labels &&
217 m_hidden_label_set == other.m_hidden_label_set;
218 }
219
222 void swap(lts& l)
223 {
224 static_cast<LTS_BASE&>(*this).swap(static_cast<LTS_BASE&>(l));
225 {
227 m_init_state=l.m_init_state;
228 l.m_init_state=aux;
229 }
230 {
231 const states_size_type aux=m_nstates;
232 m_nstates=l.m_nstates;
233 l.m_nstates=aux;
234 }
235 m_transitions.swap(l.m_transitions);
236 m_state_labels.swap(l.m_state_labels);
237 m_action_labels.swap(l.m_action_labels);
238 assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
239 assert(l.m_action_labels.size()>0 && l.m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
240 m_hidden_label_set.swap(l.m_hidden_label_set);
241 }
242
246 {
247 return m_nstates;
248 }
249
253 std::vector<STATE_LABEL_T>& state_labels()
254 {
255 return m_state_labels;
256 }
257
261 const std::vector<STATE_LABEL_T>& state_labels() const
262 {
263 return m_state_labels;
264 }
265
272 {
273 return m_state_labels.size();
274 }
275
280 void set_num_states(const states_size_type n, const bool has_state_labels = true)
281 {
282 m_nstates = n;
283 if (has_state_labels)
284 {
285 if (m_state_labels.size() > 0)
286 {
287 m_state_labels.resize(n);
288 }
289 else
290 {
291 m_state_labels = std::vector<STATE_LABEL_T>(n);
292 }
293 }
294 else
295 {
296 m_state_labels = std::vector<STATE_LABEL_T>();
297 }
298 }
299
303 {
304 return m_transitions.size();
305 }
306
311 {
312 m_action_labels.resize(n);
313 assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
314 }
315
319 {
320 assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
321 return m_action_labels.size();
322 }
323
327 {
328 return m_init_state;
329 }
330
335 {
336 assert(state<m_nstates);
338 }
339
347 states_size_type add_state(const STATE_LABEL_T& label=STATE_LABEL_T())
348 {
349 if (label!=STATE_LABEL_T())
350 {
352 m_state_labels.push_back(label);
353 }
354 return m_nstates++;
355 }
356
361 labels_size_type add_action(const ACTION_LABEL_T& label)
362 {
363 if (label==ACTION_LABEL_T::tau_action())
364 {
366 }
367 assert(std::find(m_action_labels.begin(),m_action_labels.end(),label)==m_action_labels.end()); // Action labels must be unique.
368 const labels_size_type label_index=m_action_labels.size();
369 m_action_labels.push_back(label);
370 return label_index;
371 }
372
377 {
379 }
380
384 void set_state_label(const states_size_type state, const STATE_LABEL_T& label)
385 {
386 assert(state<m_nstates);
387 assert(m_nstates==m_state_labels.size());
389 }
390
393 const std::vector<ACTION_LABEL_T>& action_labels() const
394 {
395 return m_action_labels;
396 }
397
402 void set_action_label(const labels_size_type action, const ACTION_LABEL_T& label)
403 {
404 assert(action<m_action_labels.size());
405 assert((action==const_tau_label_index) == (label==ACTION_LABEL_T::tau_action())); // a tau action is always stored at index 0.
406 assert(m_action_labels[action] == label ||
407 std::find(m_action_labels.begin(),m_action_labels.end(),label)==m_action_labels.end()); // Action labels must be unique.
408 m_action_labels[action] = label;
409 }
410
414 const std::set<labels_size_type>& hidden_label_set() const
415 {
416 return m_hidden_label_set;
417 }
418
422 std::set<labels_size_type>& hidden_label_set()
423 {
424 return m_hidden_label_set;
425 }
426
430 void set_hidden_label_set(const std::set<labels_size_type>& m)
431 {
433 }
434
439 {
440 if (m_hidden_label_set.count(action)>0)
441 {
442 return tau_label_index();
443 }
444 return action;
445 }
446
450 STATE_LABEL_T state_label(const states_size_type state) const
451 {
452 assert(state<m_nstates);
453 assert(m_nstates==m_state_labels.size());
454 return m_state_labels[state];
455 }
456
461 {
462 (void)state; // Suppress an unused variable warning.
463 assert(state<m_nstates);
464 return false;
465 }
466
470 ACTION_LABEL_T action_label(const labels_size_type action) const
471 {
472 assert(action < m_action_labels.size());
473 return m_action_labels[action];
474 }
475
484 void clear_transitions(const std::size_t n=0)
485 {
486 m_transitions = std::vector<transition>();
487 m_transitions.reserve(n);
488 }
489
496 {
497 m_action_labels.clear();
498 m_action_labels.push_back(ACTION_LABEL_T::tau_action());
499 m_hidden_label_set.clear();
500 }
501
507 {
508 m_state_labels.clear();
509 }
510
514 void clear()
515 {
519 m_nstates = 0;
520 }
521
526 const std::vector<transition>& get_transitions() const
527 {
528 return m_transitions;
529 }
530
535 std::vector<transition>& get_transitions()
536 {
537 return m_transitions;
538 }
539
545 {
546 m_transitions.push_back(t);
547 }
548
553 bool is_tau(labels_size_type action) const
554 {
555 assert(m_action_labels.size()>0 && m_action_labels[const_tau_label_index]==ACTION_LABEL_T::tau_action());
556 return (action==const_tau_label_index);
557 }
558
559
570 void record_hidden_actions(const std::vector<std::string>& tau_actions)
571 {
572 if (tau_actions.size()==0)
573 {
574 return;
575 }
576
577 std::map<labels_size_type, labels_size_type> action_rename_map;
578 for (labels_size_type i=0; i< num_action_labels(); ++i)
579 {
580 ACTION_LABEL_T a=action_label(i);
581 a.hide_actions(tau_actions);
582 if (a==ACTION_LABEL_T::tau_action())
583 {
585 {
586 m_hidden_label_set.insert(i);
587 }
588 }
589 else if (a!=action_label(i))
590 {
591 /* In this the action_label i is changed by the tau_actions but not renamed to tau.
592 We check whether a maps onto another action label index. If yes, it is added to
593 the rename map, and we explicitly rename transition labels with this label afterwards.
594 If no, we rename the action label.
595 */
596 store_action_label_to_be_renamed(a, i, action_rename_map);
597 }
598 }
599
600 rename_labels(action_rename_map);
601 }
602
609 void apply_hidden_actions(const std::vector<std::string>& tau_actions)
610 {
611 if (tau_actions.size()==0)
612 {
613 return;
614 }
615
616 std::map<labels_size_type, labels_size_type> action_rename_map;
617 for (labels_size_type i=0; i< num_action_labels(); ++i)
618 {
619 ACTION_LABEL_T a=action_label(i);
620 a.hide_actions(tau_actions);
621#ifndef NDEBUG
622 ACTION_LABEL_T b=a;
623 b.hide_actions(tau_actions);
624 assert(a==b); // hide_actions applied twice yields the same result as applying it once.
625#endif
626 store_action_label_to_be_renamed(a, i, action_rename_map);
627 }
628
629 rename_labels(action_rename_map);
630 }
631
636 bool has_state_info() const
637 {
638 return m_state_labels.size() > 0;
639 }
640
645 bool has_action_info() const
646 {
647 return m_action_labels.size() > 1;
648 }
649};
650
651}
652}
653
654#endif // MCRL2_LTS_LTS_H
Read-only balanced binary tree of terms.
void swap(lts_default_base &)
Standard swap function.
Definition lts.h:53
lts_type type()
Provides the type of this lts, in casu lts_none.
Definition lts.h:47
bool operator==(const lts_default_base &) const
Standard equality function.
Definition lts.h:60
A class that contains a labelled transition system.
Definition lts.h:83
states_size_type num_state_labels() const
Gets the number of state labels of this LTS.
Definition lts.h:271
labels_size_type num_action_labels() const
Gets the number of action labels of this LTS.
Definition lts.h:318
states_size_type m_init_state
Definition lts.h:117
void add_transition(const transition &t)
Add a transition to the lts.
Definition lts.h:544
void set_num_action_labels(const labels_size_type n)
Sets the number of action labels of this LTS.
Definition lts.h:310
bool has_action_info() const
Checks whether this LTS has labels associated with its actions, which are numbers.
Definition lts.h:645
bool is_tau(labels_size_type action) const
Checks whether an action is a tau action.
Definition lts.h:553
std::set< labels_size_type > & hidden_label_set()
Returns the hidden label set that tells for each label what its corresponding hidden label is.
Definition lts.h:422
states_size_type num_states() const
Gets the number of states of this LTS.
Definition lts.h:245
void set_hidden_label_set(const std::set< labels_size_type > &m)
Sets the hidden label map that tells for each label what its corresponding hidden label is.
Definition lts.h:430
void clear_transitions(const std::size_t n=0)
Clear the transitions of an lts.
Definition lts.h:484
void clear_actions()
Clear the action labels of an lts.
Definition lts.h:495
void set_num_states(const states_size_type n, const bool has_state_labels=true)
Sets the number of states of this LTS.
Definition lts.h:280
void store_action_label_to_be_renamed(const ACTION_LABEL_T &a, const labels_size_type i, std::map< labels_size_type, labels_size_type > &action_rename_map)
Definition lts.h:146
static constexpr bool is_probabilistic_lts
An indicator that this is not a probabilistic lts.
Definition lts.h:112
bool is_probabilistic(const states_size_type state) const
Gets the label of a state.
Definition lts.h:460
ACTION_LABEL_T action_label_t
The type of action labels.
Definition lts.h:92
const std::set< labels_size_type > & hidden_label_set() const
Returns the hidden label set that tells for each label what its corresponding hidden label is.
Definition lts.h:414
std::vector< transition > m_transitions
Definition lts.h:118
std::vector< STATE_LABEL_T > & state_labels()
Provides the state labels of an LTS.
Definition lts.h:253
ACTION_LABEL_T action_label(const labels_size_type action) const
Gets the label of an action.
Definition lts.h:470
const labels_size_type tau_label_index() const
Provide the index of the label that represents tau.
Definition lts.h:376
const std::vector< ACTION_LABEL_T > & action_labels() const
The action labels in this lts.
Definition lts.h:393
bool has_state_info() const
Checks whether this LTS has state values associated with its states.
Definition lts.h:636
lts(const lts &l)
Creates a copy of the supplied LTS.
Definition lts.h:180
void set_initial_state(const states_size_type state)
Sets the initial state number of this LTS.
Definition lts.h:334
void set_action_label(const labels_size_type action, const ACTION_LABEL_T &label)
Sets the label of an action.
Definition lts.h:402
void rename_labels(const std::map< labels_size_type, labels_size_type > &action_rename_map)
Definition lts.h:127
std::set< labels_size_type > m_hidden_label_set
Definition lts.h:124
std::vector< STATE_LABEL_T >::size_type states_size_type
The sort that contains the indices of states.
Definition lts.h:100
void apply_hidden_actions(const std::vector< std::string > &tau_actions)
Rename actions in the lts by hiding the actions in the vector tau_actions.
Definition lts.h:609
labels_size_type apply_hidden_label_map(const labels_size_type action) const
If the action label is registered hidden, it returns tau, otherwise the original label.
Definition lts.h:438
std::vector< transition > & get_transitions()
Gets a reference to the vector of transitions of the current lts.
Definition lts.h:535
std::vector< ACTION_LABEL_T >::size_type labels_size_type
The sort that represents the indices of labels.
Definition lts.h:104
lts & operator=(const lts &l)
Standard assignment operator.
Definition lts.h:194
const std::vector< STATE_LABEL_T > & state_labels() const
Provides the state labels of an LTS.
Definition lts.h:261
std::vector< STATE_LABEL_T > m_state_labels
Definition lts.h:119
STATE_LABEL_T state_label(const states_size_type state) const
Gets the label of a state.
Definition lts.h:450
states_size_type add_state(const STATE_LABEL_T &label=STATE_LABEL_T())
Adds a state to this LTS.
Definition lts.h:347
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
lts()
Creates an empty LTS.
Definition lts.h:172
bool operator==(const lts &other) const
Standard equality operator.
Definition lts.h:209
states_size_type m_nstates
Definition lts.h:116
const std::vector< transition > & get_transitions() const
Gets a const reference to the vector of transitions of the current lts.
Definition lts.h:526
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 clear_state_labels()
Clear the labels of an lts.
Definition lts.h:506
void swap(lts &l)
Swap this lts with the supplied supplied LTS.
Definition lts.h:222
void record_hidden_actions(const std::vector< std::string > &tau_actions)
Records all actions with a string that occurs in tau_actions internally.
Definition lts.h:570
std::vector< ACTION_LABEL_T > m_action_labels
Definition lts.h:120
transitions_size_type num_transitions() const
Gets the number of transitions of this LTS.
Definition lts.h:302
void set_state_label(const states_size_type state, const STATE_LABEL_T &label)
Sets the label of a state.
Definition lts.h:384
labels_size_type add_action(const ACTION_LABEL_T &label)
Adds an action with a label to this LTS.
Definition lts.h:361
A class containing triples, source label and target representing transitions.
Definition transition.h:43
The file containing the types of labelled transition systems.
atermpp::term_balanced_tree< data::data_expression > state
Definition state.h:24
lts_type
The enumerated type lts_type contains an index for every type type of labelled transition system that...
Definition lts_type.h:37
std::size_t label(const outgoing_pair_t &p)
Label of a pair of a label and target state.
static const std::size_t const_tau_label_index
Definition transition.h:27
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
A header file defining a transition as a triple from,label,to.