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

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.1