spot  2.12
mask.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 <spot/twa/twagraph.hh>
22 
23 namespace spot
24 {
50  template<typename Trans>
51  void transform_accessible(const const_twa_graph_ptr& old,
52  twa_graph_ptr& cpy,
53  Trans trans, unsigned int init,
54  bool drop_univ_branches = false)
55  {
56  std::vector<unsigned> todo;
57  std::vector<unsigned> seen(old->num_states(), -1U);
58 
59  auto orig_states = new std::vector<unsigned>();
60  orig_states->reserve(old->num_states()); // maybe less are needed.
61  cpy->set_named_prop("original-states", orig_states);
62 
63  auto new_state =
64  [&](unsigned old_state) -> unsigned
65  {
66  unsigned tmp = seen[old_state];
67  if (tmp == -1U)
68  {
69  tmp = cpy->new_state();
70  seen[old_state] = tmp;
71  orig_states->emplace_back(old_state);
72  todo.emplace_back(old_state);
73  }
74  return tmp;
75  };
76 
77  // Deal with alternating automata, possibly.
78  std::map<std::vector<unsigned>, unsigned> uniq;
79  auto new_univ_state =
80  [&](unsigned old_state) -> unsigned
81  {
82  if (!old->is_univ_dest(old_state))
83  return new_state(old_state);
84 
85  std::vector<unsigned> tmp;
86  for (auto s: old->univ_dests(old_state))
87  tmp.emplace_back(new_state(s));
88  std::sort(tmp.begin(), tmp.end());
89  tmp.erase(std::unique(tmp.begin(), tmp.end()), tmp.end());
90  auto p = uniq.emplace(tmp, 0);
91  if (p.second)
92  p.first->second =
93  cpy->get_graph().new_univ_dests(tmp.begin(), tmp.end());
94  return p.first->second;
95  };
96 
97  cpy->set_init_state(new_univ_state(init));
98  if (seen[init] != 0)
99  throw std::runtime_error
100  ("the destination automaton of transform_accessible() should be empty");
101 
102  while (!todo.empty())
103  {
104  unsigned old_src = todo.back();
105  todo.pop_back();
106 
107  unsigned new_src = seen[old_src];
108  SPOT_ASSERT(new_src != -1U);
109 
110  for (auto& t: old->out(old_src))
111  {
112  bdd cond = t.cond;
113  acc_cond::mark_t acc = t.acc;
114  trans(t.src, cond, acc, t.dst);
115  if (cond == bddfalse)
116  continue;
117  if (drop_univ_branches)
118  for (unsigned d: old->univ_dests(t.dst))
119  cpy->new_edge(new_src, new_state(d), cond, acc);
120  else
121  cpy->new_edge(new_src, new_univ_state(t.dst), cond, acc);
122  }
123  }
124  orig_states->shrink_to_fit();
125  }
126 
141  template<typename Trans>
142  void transform_copy(const const_twa_graph_ptr& old,
143  twa_graph_ptr& cpy,
144  Trans trans, unsigned int init)
145  {
146  if (!old->is_existential())
147  throw std::runtime_error
148  ("transform_copy() does not support alternation");
149 
150  // Each state in cpy corresponds to a unique state in old.
151  cpy->new_states(old->num_states());
152  cpy->set_init_state(init);
153 
154  for (auto& t: old->edges())
155  {
156  bdd cond = t.cond;
157  acc_cond::mark_t acc = t.acc;
158  trans(t.src, cond, acc, t.dst);
159  // Having the same number of states should assure that state ids are
160  // equivalent in old and cpy.
161  SPOT_ASSERT(t.src < cpy->num_states() && t.dst < cpy->num_states());
162  if (cond != bddfalse)
163  cpy->new_edge(t.src, t.dst, cond, acc);
164  }
165  }
166 
167  template<typename Trans>
168  void transform_accessible(const const_twa_graph_ptr& old,
169  twa_graph_ptr& cpy,
170  Trans trans)
171  {
172  transform_accessible(old, cpy, trans, old->get_init_state_number());
173  }
174 
175  template<typename Trans>
176  void transform_copy(const const_twa_graph_ptr& old,
177  twa_graph_ptr& cpy,
178  Trans trans)
179  {
180  transform_copy(old, cpy, trans, old->get_init_state_number());
181  }
182 
184  SPOT_API
185  twa_graph_ptr mask_acc_sets(const const_twa_graph_ptr& in,
186  acc_cond::mark_t to_remove);
187 
198  SPOT_API
199  twa_graph_ptr mask_keep_states(const const_twa_graph_ptr& in,
200  std::vector<bool>& to_keep,
201  unsigned int init);
202 
214  SPOT_API
215  twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr& in,
216  std::vector<bool>& to_keep,
217  unsigned int init,
218  bool drop_univ_branches = false);
219 }
Definition: automata.hh:26
twa_graph_ptr mask_acc_sets(const const_twa_graph_ptr &in, acc_cond::mark_t to_remove)
Remove all edges that belong to some given acceptance sets.
twa_graph_ptr mask_keep_accessible_states(const const_twa_graph_ptr &in, std::vector< bool > &to_keep, unsigned int init, bool drop_univ_branches=false)
Keep only the states specified by to_keep that are accessible.
void transform_accessible(const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans, unsigned int init, bool drop_univ_branches=false)
Clone and mask an automaton.
Definition: mask.hh:51
twa_graph_ptr mask_keep_states(const const_twa_graph_ptr &in, std::vector< bool > &to_keep, unsigned int init)
Keep only the states as specified by to_keep.
void transform_copy(const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans, unsigned int init)
Copy an automaton and update each edge.
Definition: mask.hh:142
An acceptance mark.
Definition: acc.hh:84

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