spot  2.1.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
mask.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
3 // de l'Epita (LRDE).
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 <spot/twa/twagraph.hh>
23 
24 namespace spot
25 {
40 
41  template<typename Trans>
42  void transform_accessible(const const_twa_graph_ptr& old,
43  twa_graph_ptr& cpy,
44  Trans trans, unsigned int init)
45  {
46  std::vector<unsigned> todo;
47  std::vector<unsigned> seen(old->num_states(), -1U);
48 
49  auto new_state =
50  [&](unsigned old_state) -> unsigned
51  {
52  unsigned tmp = seen[old_state];
53  if (tmp == -1U)
54  {
55  tmp = cpy->new_state();
56  seen[old_state] = tmp;
57  todo.push_back(old_state);
58  }
59  return tmp;
60  };
61 
62  cpy->set_init_state(new_state(init));
63  while (!todo.empty())
64  {
65  unsigned old_src = todo.back();
66  todo.pop_back();
67 
68  unsigned new_src = seen[old_src];
69  SPOT_ASSERT(new_src != -1U);
70 
71  for (auto& t: old->out(old_src))
72  {
73  bdd cond = t.cond;
74  acc_cond::mark_t acc = t.acc;
75  trans(t.src, cond, acc, t.dst);
76 
77  if (cond != bddfalse)
78  cpy->new_edge(new_src,
79  new_state(t.dst),
80  cond, acc);
81  }
82  }
83  }
84 
99  template<typename Trans>
100  void transform_copy(const const_twa_graph_ptr& old,
101  twa_graph_ptr& cpy,
102  Trans trans, unsigned int init)
103  {
104  // Each state in cpy corresponds to a unique state in old.
105  cpy->new_states(old->num_states());
106  cpy->set_init_state(init);
107 
108  for (auto& t: old->edges())
109  {
110  bdd cond = t.cond;
111  acc_cond::mark_t acc = t.acc;
112  trans(t.src, cond, acc, t.dst);
113  // Having the same number of states should assure that state ids are
114  // equivilent in old and cpy.
115  SPOT_ASSERT(t.src < cpy->num_states() && t.dst < cpy->num_states());
116  if (cond != bddfalse)
117  cpy->new_edge(t.src, t.dst, cond, acc);
118  }
119  }
120 
121  template<typename Trans>
122  void transform_accessible(const const_twa_graph_ptr& old,
123  twa_graph_ptr& cpy,
124  Trans trans)
125  {
126  transform_accessible(old, cpy, trans, old->get_init_state_number());
127  }
128  template<typename Trans>
129  void transform_copy(const const_twa_graph_ptr& old,
130  twa_graph_ptr& cpy,
131  Trans trans)
132  {
133  transform_copy(old, cpy, trans, old->get_init_state_number());
134  }
135 
137  SPOT_API
138  twa_graph_ptr mask_acc_sets(const const_twa_graph_ptr& in,
139  acc_cond::mark_t to_remove);
140 
145  SPOT_API
146  twa_graph_ptr mask_keep_states(const const_twa_graph_ptr& in,
147  std::vector<bool>& to_keep,
148  unsigned int init);
149 }
Definition: graph.hh:32

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Tue Sep 20 2016 07:13:02 for spot by doxygen 1.8.8