mCRL2
Loading...
Searching...
No Matches
transition.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//
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
10
11#ifndef MCRL2_LTS_DETAIL_TRANSITION_H
12#define MCRL2_LTS_DETAIL_TRANSITION_H
13
14#include <set>
16
17namespace mcrl2
18{
19namespace lts
20{
21
22namespace detail
23{
24
25inline std::size_t apply_hidden_labels(const std::size_t n, const std::set<std::size_t>& hidden_action_set)
26{
27 if (hidden_action_set.count(n)==0)
28 {
29 return n;
30 }
31 return lts::const_tau_label_index; // 0 is the index of the internal action.
32}
33
35{
36 protected:
37 const std::set<std::size_t>& m_hide_action_set;
38
39 public:
40 compare_transitions_slt(const std::set<std::size_t>& hide_action_set)
41 : m_hide_action_set(hide_action_set)
42 {}
43
44 bool operator()(const transition& t1, const transition& t2)
45 {
46 if (t1.from() != t2.from())
47 {
48 return t1.from() < t2.from();
49 }
50 else
51 {
52 const std::size_t n1=apply_hidden_labels(t1.label(), m_hide_action_set);
53 const std::size_t n2=apply_hidden_labels(t2.label(), m_hide_action_set);
54 if (n1 != n2)
55 {
56 return n1 < n2;
57 }
58 else
59 {
60 return t1.to() < t2.to();
61 }
62 }
63 }
64};
65
67{
68 protected:
69 const std::set<std::size_t>& m_hide_action_set;
70
71 public:
72 compare_transitions_lts(const std::set<std::size_t>& hide_action_set)
73 : m_hide_action_set(hide_action_set)
74 {}
75
76 bool operator()(const transition& t1, const transition& t2)
77 {
78 const std::size_t n1=apply_hidden_labels(t1.label(), m_hide_action_set);
79 const std::size_t n2=apply_hidden_labels(t2.label(), m_hide_action_set);
80 if (n1 != n2)
81 {
82 return n1 < n2;
83 }
84 else if (t1.to() != t2.to())
85 {
86 return t1.to() < t2.to();
87 }
88 else
89 {
90 return t1.from() < t2.from();
91 }
92 }
93};
94
95} // detail
96} // lts
97} // mcrl2
98
99#endif
compare_transitions_lts(const std::set< std::size_t > &hide_action_set)
Definition transition.h:72
bool operator()(const transition &t1, const transition &t2)
Definition transition.h:76
const std::set< std::size_t > & m_hide_action_set
Definition transition.h:69
const std::set< std::size_t > & m_hide_action_set
Definition transition.h:37
bool operator()(const transition &t1, const transition &t2)
Definition transition.h:44
compare_transitions_slt(const std::set< std::size_t > &hide_action_set)
Definition transition.h:40
A class containing triples, source label and target representing transitions.
Definition transition.h:43
size_type from() const
The source of the transition.
Definition transition.h:77
size_type label() const
The label of the transition.
Definition transition.h:83
size_type to() const
The target of the transition.
Definition transition.h:90
std::size_t apply_hidden_labels(const std::size_t n, const std::set< std::size_t > &hidden_action_set)
Definition transition.h:25
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.