spot  2.3.2
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
gtec.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2008, 2013, 2014, 2015, 2016 Laboratoire de Recherche
3 // et Développement de l'Epita (LRDE).
4 // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
5 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
6 // Université Pierre et Marie Curie.
7 //
8 // This file is part of Spot, a model checking library.
9 //
10 // Spot is free software; you can redistribute it and/or modify it
11 // under the terms of the GNU General Public License as published by
12 // the Free Software Foundation; either version 3 of the License, or
13 // (at your option) any later version.
14 //
15 // Spot is distributed in the hope that it will be useful, but WITHOUT
16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
18 // License for more details.
19 //
20 // You should have received a copy of the GNU General Public License
21 // along with this program. If not, see <http://www.gnu.org/licenses/>.
22 
23 #pragma once
24 
25 #include <stack>
26 #include <spot/twaalgos/gtec/status.hh>
27 #include <spot/twaalgos/emptiness.hh>
28 #include <spot/twaalgos/emptiness_stats.hh>
29 
30 namespace spot
31 {
34 
38 
55 
93  SPOT_API emptiness_check_ptr
139  couvreur99(const const_twa_ptr& a, option_map options = option_map());
140 
141 #ifndef SWIG
142  class SPOT_API couvreur99_check: public emptiness_check, public ec_statistics
146  {
147  public:
148  couvreur99_check(const const_twa_ptr& a, option_map o = option_map());
149 
150  virtual ~couvreur99_check();
151 
153  virtual emptiness_check_result_ptr check() override;
154 
155  virtual std::ostream& print_stats(std::ostream& os) const override;
156 
165  std::shared_ptr<const couvreur99_check_status> result() const;
166 
167  protected:
168  std::shared_ptr<couvreur99_check_status> ecs_;
174  void remove_component(const state* start_delete);
175 
177  bool poprem_;
180  unsigned get_removed_components() const;
181  unsigned get_vmsize() const;
182  };
183 
188  class SPOT_API couvreur99_check_shy final: public couvreur99_check
189  {
190  public:
191  couvreur99_check_shy(const const_twa_ptr& a, option_map o = option_map());
192  virtual ~couvreur99_check_shy();
193 
194  virtual emptiness_check_result_ptr check() override;
195 
196  protected:
197  struct successor {
198  acc_cond::mark_t acc;
199  const spot::state* s;
200  successor(acc_cond::mark_t acc, const spot::state* s): acc(acc), s(s) {}
201  };
202 
203  // We use five main data in this algorithm:
204  // * couvreur99_check::root, a stack of strongly connected components (SCC),
205  // * couvreur99_check::h, a hash of all visited nodes, with their order,
206  // (it is called "Hash" in Couvreur's paper)
207  // * arc, a stack of acceptance conditions between each of these SCC,
208  std::stack<acc_cond::mark_t> arc;
209  // * num, the number of visited nodes. Used to set the order of each
210  // visited node,
211  int num;
212  // * todo, the depth-first search stack. This holds pairs of the
213  // form (STATE, SUCCESSORS) where SUCCESSORS is a list of
214  // (ACCEPTANCE_CONDITIONS, STATE) pairs.
215  typedef std::list<successor> succ_queue;
216 
217  // Position in the loop seeking known successors.
218  succ_queue::iterator pos;
219 
220  struct todo_item
221  {
222  const state* s;
223  int n;
224  succ_queue q; // Unprocessed successors of S
225  todo_item(const state* s, int n, couvreur99_check_shy* shy);
226  };
227 
228  typedef std::list<todo_item> todo_list;
229  todo_list todo;
230 
231  void clear_todo();
232 
234  void dump_queue(std::ostream& os = std::cerr);
235 
237  bool group_;
238  // If the "group2" option is set (it implies "group"), we
239  // reprocess the successor states of SCC that have been merged.
240  bool group2_;
241  };
242 #endif
243 
245 }
Definition: graph.hh:33
Manage a map of options.
Definition: optionmap.hh:37
A version of spot::couvreur99_check that tries to visit known states first.
Definition: gtec.hh:188
An implementation of the Couvreur99 emptiness-check algorithm.
Definition: gtec.hh:145
Abstract class for states.
Definition: twa.hh:50
unsigned removed_components
Number of dead SCC removed by the algorithm.
Definition: gtec.hh:179
bool poprem_
Whether to store the state to be removed.
Definition: gtec.hh:177
emptiness_check_ptr couvreur99(const const_twa_ptr &a, option_map options=option_map())
Check whether the language of an automate is empty.
bool group_
Whether successors should be grouped for states in the same SCC.
Definition: gtec.hh:237
Definition: acc.hh:34

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Wed Mar 15 2017 09:26:50 for spot by doxygen 1.8.8