spot  2.11.6
emptiness.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2011, 2013-2018, 2020-2021, 2023 Laboratoire de
3 // Recherche et Developpement de l'Epita (LRDE).
4 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
5 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
6 // 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 <map>
26 #include <list>
27 #include <iosfwd>
28 #include <bddx.h>
29 #include <spot/misc/optionmap.hh>
30 #include <spot/twa/twagraph.hh>
31 #include <spot/twaalgos/emptiness_stats.hh>
32 
33 namespace spot
34 {
35  struct twa_run;
36  typedef std::shared_ptr<twa_run> twa_run_ptr;
37  typedef std::shared_ptr<const twa_run> const_twa_run_ptr;
38 
78 
84  class SPOT_API emptiness_check_result
85  {
86  public:
87  emptiness_check_result(const const_twa_ptr& a,
88  option_map o = option_map())
89  : a_(a), o_(o)
90  {
91  }
92 
93  virtual
95  {
96  }
97 
110  virtual twa_run_ptr accepting_run();
111 
113  const const_twa_ptr&
114  automaton() const
115  {
116  return a_;
117  }
118 
120  const option_map&
121  options() const
122  {
123  return o_;
124  }
125 
127  const char* parse_options(char* options);
128 
130  virtual const unsigned_statistics* statistics() const;
131 
132  protected:
134  virtual void options_updated(const option_map& old);
135 
136  const_twa_ptr a_;
138  };
139 
140  typedef std::shared_ptr<emptiness_check_result> emptiness_check_result_ptr;
141 
143  class SPOT_API emptiness_check:
144  public std::enable_shared_from_this<emptiness_check>
145  {
146  public:
147  emptiness_check(const const_twa_ptr& a, option_map o = option_map())
148  : a_(a), o_(o)
149  {
150  }
151  virtual ~emptiness_check();
152 
154  const const_twa_ptr&
155  automaton() const
156  {
157  return a_;
158  }
159 
161  const option_map&
162  options() const
163  {
164  return o_;
165  }
166 
168  const char* parse_options(char* options);
169 
171  virtual bool safe() const;
172 
187  virtual emptiness_check_result_ptr check() = 0;
188 
190  virtual const unsigned_statistics* statistics() const;
191 
194 
196  virtual std::ostream& print_stats(std::ostream& os) const;
197 
199  virtual void options_updated(const option_map& old);
200 
201  protected:
202  const_twa_ptr a_;
204  };
205 
206  typedef std::shared_ptr<emptiness_check> emptiness_check_ptr;
207 
209  typedef std::shared_ptr<emptiness_check_instantiator>
210  emptiness_check_instantiator_ptr;
211 
214  {
215  public:
217  emptiness_check_ptr instantiate(const const_twa_ptr& a) const;
218 
221  const option_map&
222  options() const
223  {
224  return o_;
225  }
226 
227  option_map&
229  {
230  return o_;
231  }
233 
236  unsigned int min_sets() const;
237 
242  unsigned int max_sets() const;
243  protected:
245 
246  option_map o_;
247  void *info_;
248  };
249 
361  SPOT_API emptiness_check_instantiator_ptr
362  make_emptiness_check_instantiator(const char* name, const char** err);
363 
365 
366 
369 
373 
375  struct SPOT_API twa_run final
376  {
377  struct step {
378  const state* s;
379  bdd label;
380  acc_cond::mark_t acc;
381 
382  step(const state* s, bdd label, acc_cond::mark_t acc) noexcept
383  : s(s), label(label), acc(acc)
384  {
385  }
386  step() = default;
387  };
388 
389  typedef std::list<step> steps;
390 
391  steps prefix;
392  steps cycle;
393  const_twa_ptr aut;
394 
395  ~twa_run();
396  twa_run(const const_twa_ptr& aut) noexcept
397  : aut(aut)
398  {
399  }
400  twa_run(const twa_run& run);
401  twa_run& operator=(const twa_run& run);
402 
410  void ensure_non_empty_cycle(const char* where) const;
411 
425  twa_run_ptr reduce() const;
426 
435  twa_run_ptr project(const const_twa_ptr& other, bool right = false);
436 
447  bool replay(std::ostream& os, bool debug = false) const;
448 
452  void highlight(unsigned color);
453 
460  twa_graph_ptr as_twa(bool preserve_names = false) const;
461 
476  SPOT_API
477  friend std::ostream& operator<<(std::ostream& os, const twa_run& run);
478  };
480 
483 }
Emptiness-check statistics.
Definition: emptiness_stats.hh:61
Dynamically create emptiness checks. Given their name and options.
Definition: emptiness.hh:214
const option_map & options() const
Definition: emptiness.hh:222
emptiness_check_ptr instantiate(const const_twa_ptr &a) const
Actually instantiate the emptiness check, for a.
option_map & options()
Definition: emptiness.hh:228
unsigned int min_sets() const
Minimum number of acceptance sets supported by the emptiness check.
unsigned int max_sets() const
Maximum number of acceptance conditions supported by the emptiness check.
The result of an emptiness check.
Definition: emptiness.hh:85
virtual void options_updated(const option_map &old)
Notify option updates.
option_map o_
The options.
Definition: emptiness.hh:137
const option_map & options() const
Return the options parametrizing how the accepting run is computed.
Definition: emptiness.hh:121
virtual twa_run_ptr accepting_run()
Return a run accepted by the automata passed to the emptiness check.
const char * parse_options(char *options)
Modify the algorithm options.
virtual const unsigned_statistics * statistics() const
Return statistics, if available.
const const_twa_ptr & automaton() const
The automaton on which an accepting_run() was found.
Definition: emptiness.hh:114
const_twa_ptr a_
The automaton.
Definition: emptiness.hh:136
Common interface to emptiness check algorithms.
Definition: emptiness.hh:145
const_twa_ptr a_
The automaton.
Definition: emptiness.hh:202
option_map o_
The options.
Definition: emptiness.hh:203
virtual std::ostream & print_stats(std::ostream &os) const
Print statistics, if any.
virtual const ec_statistics * emptiness_check_statistics() const
Return emptiness check statistics, if available.
virtual bool safe() const
Return false iff accepting_run() can return 0 for non-empty automata.
virtual void options_updated(const option_map &old)
Notify option updates.
const option_map & options() const
Return the options parametrizing how the emptiness check is realized.
Definition: emptiness.hh:162
const char * parse_options(char *options)
Modify the algorithm options.
virtual const unsigned_statistics * statistics() const
Return statistics, if available.
const const_twa_ptr & automaton() const
The automaton that this emptiness-check inspects.
Definition: emptiness.hh:155
virtual emptiness_check_result_ptr check()=0
Check whether the automaton contain an accepting run.
Manage a map of options.
Definition: optionmap.hh:38
Abstract class for states.
Definition: twa.hh:51
emptiness_check_instantiator_ptr make_emptiness_check_instantiator(const char *name, const char **err)
Create an emptiness-check instantiator, given the name of an emptiness check.
Definition: automata.hh:27
An acceptance mark.
Definition: acc.hh:85
Definition: emptiness.hh:377
An accepted run, for a twa.
Definition: emptiness.hh:376
void highlight(unsigned color)
Highlight the accepting run on the automaton.
twa_run_ptr project(const const_twa_ptr &other, bool right=false)
Project an accepting run.
void ensure_non_empty_cycle(const char *where) const
Raise an exception of the cycle is empty.
twa_graph_ptr as_twa(bool preserve_names=false) const
Convert the run into a lasso-shaped automaton.
twa_run_ptr reduce() const
Reduce an accepting run.
friend std::ostream & operator<<(std::ostream &os, const twa_run &run)
Display a twa_run.
bool replay(std::ostream &os, bool debug=false) const
Replay a run.
Definition: emptiness_stats.hh:36

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