spot  2.3.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
mask.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015, 2016, 2017 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  if (!old->is_existential())
47  throw std::runtime_error
48  ("transform_accessible() does not support alternation");
49 
50  std::vector<unsigned> todo;
51  std::vector<unsigned> seen(old->num_states(), -1U);
52 
53  auto new_state =
54  [&](unsigned old_state) -> unsigned
55  {
56  unsigned tmp = seen[old_state];
57  if (tmp == -1U)
58  {
59  tmp = cpy->new_state();
60  seen[old_state] = tmp;
61  todo.emplace_back(old_state);
62  }
63  return tmp;
64  };
65 
66  cpy->set_init_state(new_state(init));
67  while (!todo.empty())
68  {
69  unsigned old_src = todo.back();
70  todo.pop_back();
71 
72  unsigned new_src = seen[old_src];
73  SPOT_ASSERT(new_src != -1U);
74 
75  for (auto& t: old->out(old_src))
76  {
77  bdd cond = t.cond;
78  acc_cond::mark_t acc = t.acc;
79  trans(t.src, cond, acc, t.dst);
80 
81  if (cond != bddfalse)
82  cpy->new_edge(new_src,
83  new_state(t.dst),
84  cond, acc);
85  }
86  }
87  }
88 
103  template<typename Trans>
104  void transform_copy(const const_twa_graph_ptr& old,
105  twa_graph_ptr& cpy,
106  Trans trans, unsigned int init)
107  {
108  if (!old->is_existential())
109  throw std::runtime_error
110  ("transform_copy() does not support alternation");
111 
112  // Each state in cpy corresponds to a unique state in old.
113  cpy->new_states(old->num_states());
114  cpy->set_init_state(init);
115 
116  for (auto& t: old->edges())
117  {
118  bdd cond = t.cond;
119  acc_cond::mark_t acc = t.acc;
120  trans(t.src, cond, acc, t.dst);
121  // Having the same number of states should assure that state ids are
122  // equivilent in old and cpy.
123  SPOT_ASSERT(t.src < cpy->num_states() && t.dst < cpy->num_states());
124  if (cond != bddfalse)
125  cpy->new_edge(t.src, t.dst, cond, acc);
126  }
127  }
128 
129  template<typename Trans>
130  void transform_accessible(const const_twa_graph_ptr& old,
131  twa_graph_ptr& cpy,
132  Trans trans)
133  {
134  transform_accessible(old, cpy, trans, old->get_init_state_number());
135  }
136  template<typename Trans>
137  void transform_copy(const const_twa_graph_ptr& old,
138  twa_graph_ptr& cpy,
139  Trans trans)
140  {
141  transform_copy(old, cpy, trans, old->get_init_state_number());
142  }
143 
145  SPOT_API
146  twa_graph_ptr mask_acc_sets(const const_twa_graph_ptr& in,
147  acc_cond::mark_t to_remove);
148 
159  SPOT_API
160  twa_graph_ptr mask_keep_states(const const_twa_graph_ptr& in,
161  std::vector<bool>& to_keep,
162  unsigned int init);
163 
172  SPOT_API
173  twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr& in,
174  std::vector<bool>& to_keep,
175  unsigned int init);
176 }
Definition: graph.hh:33

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Feb 20 2017 07:08:25 for spot by doxygen 1.8.8