spot  2.12.2
emptiness.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 <map>
22 #include <list>
23 #include <iosfwd>
24 #include <bddx.h>
25 #include <spot/misc/optionmap.hh>
26 #include <spot/twa/twagraph.hh>
27 #include <spot/twaalgos/emptiness_stats.hh>
28 
29 namespace spot
30 {
31  struct twa_run;
32  typedef std::shared_ptr<twa_run> twa_run_ptr;
33  typedef std::shared_ptr<const twa_run> const_twa_run_ptr;
34 
74 
80  class SPOT_API emptiness_check_result
81  {
82  public:
83  emptiness_check_result(const const_twa_ptr& a,
84  option_map o = option_map())
85  : a_(a), o_(o)
86  {
87  }
88 
89  virtual
91  {
92  }
93 
106  virtual twa_run_ptr accepting_run();
107 
109  const const_twa_ptr&
110  automaton() const
111  {
112  return a_;
113  }
114 
115  // / Return the options parameterizing how the accepting run is computed.
116  const option_map&
117  options() const
118  {
119  return o_;
120  }
121 
123  const char* parse_options(char* options);
124 
126  virtual const unsigned_statistics* statistics() const;
127 
128  protected:
130  virtual void options_updated(const option_map& old);
131 
132  const_twa_ptr a_;
134  };
135 
136  typedef std::shared_ptr<emptiness_check_result> emptiness_check_result_ptr;
137 
139  class SPOT_API emptiness_check:
140  public std::enable_shared_from_this<emptiness_check>
141  {
142  public:
143  emptiness_check(const const_twa_ptr& a, option_map o = option_map())
144  : a_(a), o_(o)
145  {
146  }
147  virtual ~emptiness_check();
148 
150  const const_twa_ptr&
151  automaton() const
152  {
153  return a_;
154  }
155 
157  const option_map&
158  options() const
159  {
160  return o_;
161  }
162 
164  const char* parse_options(char* options);
165 
167  virtual bool safe() const;
168 
183  virtual emptiness_check_result_ptr check() = 0;
184 
186  virtual const unsigned_statistics* statistics() const;
187 
190 
192  virtual std::ostream& print_stats(std::ostream& os) const;
193 
195  virtual void options_updated(const option_map& old);
196 
197  protected:
198  const_twa_ptr a_;
200  };
201 
202  typedef std::shared_ptr<emptiness_check> emptiness_check_ptr;
203 
205  typedef std::shared_ptr<emptiness_check_instantiator>
206  emptiness_check_instantiator_ptr;
207 
210  {
211  public:
213  emptiness_check_ptr instantiate(const const_twa_ptr& a) const;
214 
217  const option_map&
218  options() const
219  {
220  return o_;
221  }
222 
223  option_map&
225  {
226  return o_;
227  }
229 
232  unsigned int min_sets() const;
233 
238  unsigned int max_sets() const;
239  protected:
241 
242  option_map o_;
243  void *info_;
244  };
245 
357  SPOT_API emptiness_check_instantiator_ptr
358  make_emptiness_check_instantiator(const char* name, const char** err);
359 
361 
362 
365 
369 
371  struct SPOT_API twa_run final
372  {
373  struct step {
374  const state* s;
375  bdd label;
376  acc_cond::mark_t acc;
377 
378  step(const state* s, bdd label, acc_cond::mark_t acc) noexcept
379  : s(s), label(label), acc(acc)
380  {
381  }
382  step() = default;
383  };
384 
385  typedef std::list<step> steps;
386 
387  steps prefix;
388  steps cycle;
389  const_twa_ptr aut;
390 
391  ~twa_run();
392  twa_run(const const_twa_ptr& aut) noexcept
393  : aut(aut)
394  {
395  }
396  twa_run(const twa_run& run);
397  twa_run& operator=(const twa_run& run);
398 
406  void ensure_non_empty_cycle(const char* where) const;
407 
421  twa_run_ptr reduce() const;
422 
431  twa_run_ptr project(const const_twa_ptr& other, bool right = false);
432 
443  bool replay(std::ostream& os, bool debug = false) const;
444 
448  void highlight(unsigned color);
449 
456  twa_graph_ptr as_twa(bool preserve_names = false) const;
457 
472  SPOT_API
473  friend std::ostream& operator<<(std::ostream& os, const twa_run& run);
474  };
476 
479 }
Emptiness-check statistics.
Definition: emptiness_stats.hh:57
Dynamically create emptiness checks. Given their name and options.
Definition: emptiness.hh:210
const option_map & options() const
Definition: emptiness.hh:218
emptiness_check_ptr instantiate(const const_twa_ptr &a) const
Actually instantiate the emptiness check, for a.
option_map & options()
Definition: emptiness.hh:224
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:81
virtual void options_updated(const option_map &old)
Notify option updates.
option_map o_
The options.
Definition: emptiness.hh:133
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:110
const_twa_ptr a_
The automaton.
Definition: emptiness.hh:132
Common interface to emptiness check algorithms.
Definition: emptiness.hh:141
const_twa_ptr a_
The automaton.
Definition: emptiness.hh:198
option_map o_
The options.
Definition: emptiness.hh:199
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 parameterizing how the emptiness check is realized.
Definition: emptiness.hh:158
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:151
virtual emptiness_check_result_ptr check()=0
Check whether the automaton contain an accepting run.
Manage a map of options.
Definition: optionmap.hh:34
Abstract class for states.
Definition: twa.hh:47
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:26
An acceptance mark.
Definition: acc.hh:84
Definition: emptiness.hh:373
An accepted run, for a twa.
Definition: emptiness.hh:372
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:32

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