spot 2.11.2.dev
ngraph.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
3// de l'Epita.
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <unordered_map>
23#include <vector>
24#include <spot/graph/graph.hh>
25
26namespace spot
27{
28 template <typename Graph,
29 typename State_Name,
30 typename Name_Hash = std::hash<State_Name>,
31 typename Name_Equal = std::equal_to<State_Name>>
32 class SPOT_API named_graph
33 {
34 protected:
35 Graph& g_;
36 public:
37
38 typedef typename Graph::state state;
39 typedef typename Graph::edge edge;
40 typedef State_Name name;
41
42 typedef std::unordered_map<name, state,
43 Name_Hash, Name_Equal> name_to_state_t;
44 name_to_state_t name_to_state;
45 typedef std::vector<name> state_to_name_t;
46 state_to_name_t state_to_name;
47
48 named_graph(Graph& g)
49 : g_(g)
50 {
51 }
52
53 Graph& graph()
54 {
55 return g_;
56 }
57
58 Graph& graph() const
59 {
60 return g_;
61 }
62
63 template <typename... Args>
64 state new_state(name n, Args&&... args)
65 {
66 auto p = name_to_state.emplace(n, 0U);
67 if (p.second)
68 {
69 unsigned s = g_.new_state(std::forward<Args>(args)...);
70 p.first->second = s;
71 if (state_to_name.size() < s + 1)
72 state_to_name.resize(s + 1);
73 state_to_name[s] = n;
74 return s;
75 }
76 return p.first->second;
77 }
78
84 bool alias_state(state s, name newname)
85 {
86 auto p = name_to_state.emplace(newname, s);
87 if (!p.second)
88 {
89 // The state already exists. Change its number.
90 auto old = p.first->second;
91 p.first->second = s;
92 // Add the successor of OLD to those of S.
93 auto& trans = g_.edge_vector();
94 auto& states = g_.states();
95 trans[states[s].succ_tail].next_succ = states[old].succ;
96 states[s].succ_tail = states[old].succ_tail;
97 states[old].succ = 0;
98 states[old].succ_tail = 0;
99 // Remove all references to old in edges:
100 unsigned tend = trans.size();
101 for (unsigned t = 1; t < tend; ++t)
102 {
103 if (trans[t].src == old)
104 trans[t].src = s;
105 if (trans[t].dst == old)
106 trans[t].dst = s;
107 }
108 }
109 return !p.second;
110 }
111
112 state get_state(name n) const
113 {
114 return name_to_state.at(n);
115 }
116
117 name get_name(state s) const
118 {
119 return state_to_name.at(s);
120 }
121
122 bool has_state(name n) const
123 {
124 return name_to_state.find(n) != name_to_state.end();
125 }
126
127 const state_to_name_t& names() const
128 {
129 return state_to_name;
130 }
131
132 template <typename... Args>
133 edge
134 new_edge(name src, name dst, Args&&... args)
135 {
136 return g_.new_edge(get_state(src), get_state(dst),
137 std::forward<Args>(args)...);
138 }
139
140 template <typename I, typename... Args>
141 edge
142 new_univ_edge(name src, I dst_begin, I dst_end, Args&&... args)
143 {
144 std::vector<unsigned> d;
145 d.reserve(std::distance(dst_begin, dst_end));
146 while (dst_begin != dst_end)
147 d.emplace_back(get_state(*dst_begin++));
148 return g_.new_univ_edge(get_state(src), d.begin(), d.end(),
149 std::forward<Args>(args)...);
150 }
151
152 template <typename... Args>
153 edge
154 new_univ_edge(name src,
155 const std::initializer_list<State_Name>& dsts, Args&&... args)
156 {
157 return new_univ_edge(src, dsts.begin(), dsts.end(),
158 std::forward<Args>(args)...);
159 }
160 };
161}
Definition: ngraph.hh:33
bool alias_state(state s, name newname)
Give an alternate name to a state.
Definition: ngraph.hh:84
Abstract class for states.
Definition: twa.hh:51
@ U
until
Definition: automata.hh:27

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4