spot 2.11.2.dev
gtec.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2008, 2013-2016, 2018-2020 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
30namespace spot
31{
34
46
121 SPOT_API emptiness_check_ptr
122 couvreur99(const const_twa_ptr& a, option_map options = option_map());
123
124#ifndef SWIG
128 class SPOT_API couvreur99_check:
129 // We inherit from ec_statistics first to work around GCC bug #90309.
130 // https://gcc.gnu.org/bugzilla/show_bug.cgi?id=90309#c6
131 public ec_statistics, public emptiness_check
132 {
133 public:
134 couvreur99_check(const const_twa_ptr& a, option_map o = option_map());
135
136 virtual ~couvreur99_check();
137
139 virtual emptiness_check_result_ptr check() override;
140
141 virtual std::ostream& print_stats(std::ostream& os) const override;
142
151 std::shared_ptr<const couvreur99_check_status> result() const;
152
153 protected:
154 std::shared_ptr<couvreur99_check_status> ecs_;
160 void remove_component(const state* start_delete);
161
166
167 unsigned get_removed_components() const;
168 unsigned get_vmsize() const;
169 };
170
175 class SPOT_API couvreur99_check_shy final: public couvreur99_check
176 {
177 public:
178 couvreur99_check_shy(const const_twa_ptr& a, option_map o = option_map());
179 virtual ~couvreur99_check_shy();
180
181 virtual emptiness_check_result_ptr check() override;
182
183 protected:
184 struct successor {
186 const spot::state* s;
187 successor(acc_cond::mark_t acc, const spot::state* s) noexcept
188 : acc(acc), s(s) {}
189 };
190
191 // We use five main data in this algorithm:
192 // * couvreur99_check::root, a stack of strongly connected components (SCC),
193 // * couvreur99_check::h, a hash of all visited nodes, with their order,
194 // (it is called "Hash" in Couvreur's paper)
195 // * arc, a stack of acceptance conditions between each of these SCC,
196 std::stack<acc_cond::mark_t> arc;
197 // * num, the number of visited nodes. Used to set the order of each
198 // visited node,
199 int num;
200 // * todo, the depth-first search stack. This holds pairs of the
201 // form (STATE, SUCCESSORS) where SUCCESSORS is a list of
202 // (ACCEPTANCE_CONDITIONS, STATE) pairs.
203 typedef std::list<successor> succ_queue;
204
205 // Position in the loop seeking known successors.
206 succ_queue::iterator pos;
207
209 {
210 const state* s;
211 int n;
212 succ_queue q; // Unprocessed successors of S
213 todo_item(const state* s, int n, couvreur99_check_shy* shy);
214 };
215
216 typedef std::list<todo_item> todo_list;
217 todo_list todo;
218
219 void clear_todo();
220
222 bool group_;
223 // If the "group2" option is set (it implies "group"), we
224 // reprocess the successor states of SCC that have been merged.
225 bool group2_;
226 };
227#endif
228
230}
A version of spot::couvreur99_check that tries to visit known states first.
Definition: gtec.hh:176
bool group_
Whether successors should be grouped for states in the same SCC.
Definition: gtec.hh:222
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:132
bool poprem_
Whether to store the state to be removed.
Definition: gtec.hh:163
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 emptiness_check_result_ptr check() override
Check whether the automaton's language is empty.
virtual std::ostream & print_stats(std::ostream &os) const override
Print statistics, if any.
unsigned removed_components
Number of dead SCC removed by the algorithm.
Definition: gtec.hh:165
Emptiness-check statistics.
Definition: emptiness_stats.hh:61
Common interface to emptiness check algorithms.
Definition: emptiness.hh:145
Manage a map of options.
Definition: optionmap.hh:38
Abstract class for states.
Definition: twa.hh:51
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:27
An acceptance mark.
Definition: acc.hh:90

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.4