spot  2.12.1
gtec.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 <stack>
22 #include <spot/twaalgos/gtec/status.hh>
23 #include <spot/twaalgos/emptiness.hh>
24 #include <spot/twaalgos/emptiness_stats.hh>
25 
26 namespace spot
27 {
30 
42 
117  SPOT_API emptiness_check_ptr
118  couvreur99(const const_twa_ptr& a, option_map options = option_map());
119 
120 #ifndef SWIG
124  class SPOT_API couvreur99_check:
125  // We inherit from ec_statistics first to work around GCC bug #90309.
126  // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=90309#c6
127  public ec_statistics, public emptiness_check
128  {
129  public:
130  couvreur99_check(const const_twa_ptr& a, option_map o = option_map());
131 
132  virtual ~couvreur99_check();
133 
135  virtual emptiness_check_result_ptr check() override;
136 
137  virtual std::ostream& print_stats(std::ostream& os) const override;
138 
147  std::shared_ptr<const couvreur99_check_status> result() const;
148 
149  protected:
150  std::shared_ptr<couvreur99_check_status> ecs_;
156  void remove_component(const state* start_delete);
157 
159  bool poprem_;
162 
163  unsigned get_removed_components() const;
164  unsigned get_vmsize() const;
165  };
166 
171  class SPOT_API couvreur99_check_shy final: public couvreur99_check
172  {
173  public:
174  couvreur99_check_shy(const const_twa_ptr& a, option_map o = option_map());
175  virtual ~couvreur99_check_shy();
176 
177  virtual emptiness_check_result_ptr check() override;
178 
179  protected:
180  struct successor {
181  acc_cond::mark_t acc;
182  const spot::state* s;
183  successor(acc_cond::mark_t acc, const spot::state* s) noexcept
184  : acc(acc), s(s) {}
185  };
186 
187  // We use five main data in this algorithm:
188  // * couvreur99_check::root, a stack of strongly connected components (SCC),
189  // * couvreur99_check::h, a hash of all visited nodes, with their order,
190  // (it is called "Hash" in Couvreur's paper)
191  // * arc, a stack of acceptance conditions between each of these SCC,
192  std::stack<acc_cond::mark_t> arc;
193  // * num, the number of visited nodes. Used to set the order of each
194  // visited node,
195  int num;
196  // * todo, the depth-first search stack. This holds pairs of the
197  // form (STATE, SUCCESSORS) where SUCCESSORS is a list of
198  // (ACCEPTANCE_CONDITIONS, STATE) pairs.
199  typedef std::list<successor> succ_queue;
200 
201  // Position in the loop seeking known successors.
202  succ_queue::iterator pos;
203 
204  struct todo_item
205  {
206  const state* s;
207  int n;
208  succ_queue q; // Unprocessed successors of S
209  todo_item(const state* s, int n, couvreur99_check_shy* shy);
210  };
211 
212  typedef std::list<todo_item> todo_list;
213  todo_list todo;
214 
215  void clear_todo();
216 
218  bool group_;
219  // If the "group2" option is set (it implies "group"), we
220  // reprocess the successor states of SCC that have been merged.
221  bool group2_;
222  };
223 #endif
224 
226 }
A version of spot::couvreur99_check that tries to visit known states first.
Definition: gtec.hh:172
bool group_
Whether successors should be grouped for states in the same SCC.
Definition: gtec.hh:218
virtual emptiness_check_result_ptr check() override
Check whether the automaton's language is empty.
An implementation of the Couvreur99 emptiness-check algorithm.
Definition: gtec.hh:128
bool poprem_
Whether to store the state to be removed.
Definition: gtec.hh:159
void remove_component(const state *start_delete)
Remove a strongly component from the hash.
std::shared_ptr< const couvreur99_check_status > result() const
Return the status of the emptiness-check.
virtual std::ostream & print_stats(std::ostream &os) const override
Print statistics, if any.
virtual emptiness_check_result_ptr check() override
Check whether the automaton's language is empty.
unsigned removed_components
Number of dead SCC removed by the algorithm.
Definition: gtec.hh:161
Emptiness-check statistics.
Definition: emptiness_stats.hh:57
Common interface to emptiness check algorithms.
Definition: emptiness.hh:141
Manage a map of options.
Definition: optionmap.hh:34
Abstract class for states.
Definition: twa.hh:47
emptiness_check_ptr couvreur99(const const_twa_ptr &a, option_map options=option_map())
Check whether the language of an automate is empty.
Definition: automata.hh:26
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