emptiness.hh 16.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011, 2013, 2014, 2015, 2016, 2017, 2018 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
7
8
9
10
11
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// 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
14
15
16
17
18
19
20
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// 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
27
#include <list>
#include <iosfwd>
28
#include <bddx.h>
29
30
31
#include <spot/misc/optionmap.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/emptiness_stats.hh>
32
33
34

namespace spot
{
35
36
37
  struct twa_run;
  typedef std::shared_ptr<twa_run> twa_run_ptr;
  typedef std::shared_ptr<const twa_run> const_twa_run_ptr;
38

39
  /// \addtogroup emptiness_check Emptiness-checks
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
40
  /// \ingroup twa_algorithms
41
  ///
42
43
44
45
46
47
48
49
50
  /// You can create an emptiness check either by instantiating it
  /// explicitly (calling one of the functions of \ref
  /// emptiness_check_algorithms "this list"), or indirectly via
  /// spot::make_emptiness_check_instantiator().  The latter function
  /// allows user-options to influence the choice of the
  /// emptiness-check algorithm used, and the intermediate
  /// instantiator object can be used to query to properties of the
  /// emptiness check selected.
  ///
51
52
  /// All emptiness-check algorithms follow the same interface.
  /// Basically once you have constructed an instance of
53
  /// spot::emptiness_check, you should call
54
  /// spot::emptiness_check::check() to check the automaton.
55
  ///
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
  /// If spot::emptiness_check::check() returns 0, then the automaton
  /// was found empty.  Otherwise the automaton accepts some run.
  /// (Beware that some algorithms---those using bit-state
  /// hashing---may found the automaton to be empty even if it is not
  /// actually empty.)
  ///
  /// When spot::emptiness_check::check() does not return 0, it
  /// returns an instance of spot::emptiness_check_result.  You can
  /// try to call spot::emptiness_check_result::accepting_run() to
  /// obtain an accepting run.  For some emptiness-check algorithms,
  /// spot::emptiness_check_result::accepting_run() will require some
  /// extra computation.  Most emptiness-check algorithms are able to
  /// return such an accepting run, however this is not mandatory and
  /// spot::emptiness_check_result::accepting_run() can return 0 (this
  /// does not means by anyway that no accepting run exist).
  ///
  /// The acceptance run returned by
  /// spot::emptiness_check_result::accepting_run(), if any, is of
74
  /// type spot::twa_run.  \ref twa_run "This page" gathers existing
75
76
77
  /// operations on these objects.
  ///
  /// @{
78
79
80
81
82
83

  /// \brief The result of an emptiness check.
  ///
  /// Instances of these class should not last longer than the
  /// instances of emptiness_check that produced them as they
  /// may reference data internal to the check.
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
90
91
92
93
94
      : a_(a), o_(o)
    {
    }

    virtual
    ~emptiness_check_result()
95
96
97
    {
    }

98
99
100
101
102
103
104
105
106
107
108
109
    /// \brief Return a run accepted by the automata passed to
    /// the emptiness check.
    ///
    /// This method might actually compute the acceptance run.  (Not
    /// all emptiness check algorithms actually produce a
    /// counter-example as a side-effect of checking emptiness, some
    /// need some post-processing.)
    ///
    /// This can also return 0 if the emptiness check algorithm
    /// cannot produce a counter example (that does not mean there
    /// is no counter-example; the mere existence of an instance of
    /// this class asserts the existence of a counter-example).
110
    virtual twa_run_ptr accepting_run();
111
112

    /// The automaton on which an accepting_run() was found.
113
    const const_twa_ptr&
114
115
116
117
    automaton() const
    {
      return a_;
    }
118

119
120
121
122
123
124
125
    /// Return the options parametrizing how the accepting run is computed.
    const option_map&
    options() const
    {
      return o_;
    }

126
127
    /// Modify the algorithm options.
    const char* parse_options(char* options);
128

129
130
131
    /// Return statistics, if available.
    virtual const unsigned_statistics* statistics() const;

132
  protected:
133
134
    /// Notify option updates.
    virtual void options_updated(const option_map& old);
135

136
137
    const_twa_ptr a_;                ///< The automaton.
    option_map o_;                ///< The options.
138
139
  };

140
141
  typedef std::shared_ptr<emptiness_check_result> emptiness_check_result_ptr;

142
  /// Common interface to emptiness check algorithms.
143
144
  class SPOT_API emptiness_check:
    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
152
    virtual ~emptiness_check();

153
    /// The automaton that this emptiness-check inspects.
154
    const const_twa_ptr&
155
156
157
158
159
    automaton() const
    {
      return a_;
    }

160
161
162
163
164
165
166
    /// Return the options parametrizing how the emptiness check is realized.
    const option_map&
    options() const
    {
      return o_;
    }

167
168
169
170
171
    /// Modify the algorithm options.
    const char* parse_options(char* options);

    /// Return false iff accepting_run() can return 0 for non-empty automata.
    virtual bool safe() const;
172

173
174
    /// \brief Check whether the automaton contain an accepting run.
    ///
175
    /// Return 0 if the automaton accepts no run.  Return an instance
176
177
178
179
180
181
182
    /// of emptiness_check_result otherwise.  This instance might
    /// allow to obtain one sample acceptance run.  The result has to
    /// be destroyed before the emptiness_check instance that
    /// generated it.
    ///
    /// Some emptiness_check algorithms may allow check() to be called
    /// several time, but generally you should not assume that.
183
184
185
186
    ///
    /// Some emptiness_check algorithms, especially those using bit state
    /// hashing may return 0 even if the automaton is not empty.
    /// \see safe()
187
    virtual emptiness_check_result_ptr check() = 0;
188

189
190
191
    /// Return statistics, if available.
    virtual const unsigned_statistics* statistics() const;

192
193
194
    /// Return emptiness check statistics, if available.
    virtual const ec_statistics* emptiness_check_statistics() const;

195
196
    /// Print statistics, if any.
    virtual std::ostream& print_stats(std::ostream& os) const;
197

198
199
    /// Notify option updates.
    virtual void options_updated(const option_map& old);
200

201
  protected:
202
203
    const_twa_ptr a_;                ///< The automaton.
    option_map o_;                ///< The options
204
205
  };

206
207
208
209
210
  typedef std::shared_ptr<emptiness_check> emptiness_check_ptr;

  class emptiness_check_instantiator;
  typedef std::shared_ptr<emptiness_check_instantiator>
    emptiness_check_instantiator_ptr;
211

212
  /// Dynamically create emptiness checks.  Given their name and options.
213
  class SPOT_API emptiness_check_instantiator
214
215
216
  {
  public:
    /// Actually instantiate the emptiness check, for \a a.
217
    emptiness_check_ptr instantiate(const const_twa_ptr& a) const;
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233

    /// Accessor to the options.
    /// @{
    const option_map&
    options() const
    {
      return o_;
    }

    option_map&
    options()
    {
      return o_;
    }
    /// @}

234
    /// \brief Minimum number of acceptance sets supported by
235
    /// the emptiness check.
236
    unsigned int min_sets() const;
237
238
239
240
241

    /// \brief Maximum number of acceptance conditions supported by
    /// the emptiness check.
    ///
    /// \return \c -1U if no upper bound exists.
242
    unsigned int max_sets() const;
243
  protected:
244
    emptiness_check_instantiator(option_map o, void* i);
245

246
247
248
249
    option_map o_;
    void *info_;
  };

250
251
252
  /// \brief Create an emptiness-check instantiator, given the name
  /// of an emptiness check.
  ///
253
254
255
256
  /// This is a convenient entry point to instantiate an emptiness
  /// check with user-supplied options.
  ///
  /// \param name should have the form \c "name" or \c "name(options)".
257
  ///
258
259
260
  /// \return Return an emptiness-check instantiator.  On error, the
  /// function returns \c nullptr.  If the name of the algorithm was
  /// unknown, \c *err will be set to \c name.  If some fragment of
261
262
  /// the options could not be parsed, \c *err will point to that
  /// fragment.
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
  ///
  /// The following names supported and correspond to different emptiness
  /// check algorithms:
  /// - `Cou99` uses `spot::couvreur99()`, that works with Fin-less
  ///       acceptance conditions, with any number of acceptance sets.
  ///       The following options can be used:
  ///     - `shy` Compute all successors of each state, then explore already
  ///       visited states first. This usually helps to merge SCCs, and
  ///       thus exit sooner. However because all successors have to be
  ///       computed and stored, it often consume more memory.
  ///     - `group` Setting this option is meaningful only when shy is
  ///       used. If set (the default), the successors of all the states
  ///       that belong to the same SCC will be considered when choosing
  ///       a successor. Otherwise, only the successor of the topmost
  ///       state on the DFS stack are considered.
  ///     - `poprem` Specifies how the algorithm should handle the
  ///       destruction of non-accepting maximal strongly connected
  ///       components. If poprem is set, the algorithm will keep a list
  ///       of all states of a SCC that are fully processed and should be
  ///       removed once the MSCC is popped. If poprem is unset (the
  ///       default), the MSCC will be traversed again (i.e. generating
  ///       the successors of the root recursively) for deletion. This
  ///       is a choice between memory and speed.
  ///
  ///   Examples:
  ///   \code
  ///   Cou99
  ///   Cou99(shy !group)
  ///   Cou99(shy group)
  ///   Cou99(poprem)
  ///   Cou99(poprem shy !group)
  ///   Cou99(poprem shy group)
  ///   \endcode
  ///
  /// - `GC04` uses `spot::explicit_gv04_check()` and works on automata
  ///   with Fin-less acceptance conditions using at most one acceptance
  ///   set.  No options are supported.
  ///
  ///   Example:
  ///   \code
  ///   GC04
  ///   \endcode
  ///
  /// - `CVWY90` uses `spot::magic_search()` and work on automata with
  ///   Fin-less acceptance conditions using at most one acceptance
  ///   set.  Set option `bsh` to the size of a hash-table if you want
  ///   to activate bit-state hashing.
  ///
  ///   Examples:
  ///   \code
  ///   CVWY90
  ///   CVWY90(bsh=4M)
  ///   \endcode
  ///
  /// - `SE05` uses `spot::se05()` and works on work on automata with
  ///   Fin-less acceptance conditions using at most one acceptance
  ///   set.  Set option `bsh` to the size of a hash-table if you want
  ///   to activate bit-state hashing.
  ///
  ///   Examples:
  ///   \code
  ///   SE05
  ///   SE05(bsh=4M)
  ///   \endcode
  ///
  /// - `Tau03` uses `spot::explicit_tau03_search()` and work on automata with
  ///   Fin-less acceptance conditions using at least one acceptance
  ///   set.  No options are supported.
  ///
  ///   Example:
  ///   \code
  ///   Tau03
  ///   \endcode
  ///
  /// - `Tau03_opt` uses `spot::explicit_tau03_opt_search()` and work on
  /// automata with any Fin-less acceptance.  The following options are
  /// supported:
  ///   - `weights` This option is set by default and activates the usage
  ///     of weights in the top-level DFS as well as in nested DFSs.
  ///   - `redweights` This option is set by default, and activates the
  ///     usage of weights in nested DFSs. It is meaningful only if
  ///     weights is set.
  ///   - `condstack` This option is unset by default, and activates
  ///     the use of the "conditional stack" optimization described by
  ///     Heikki Tauriainen.
  ///   - ordering This option is unset by default, and activates the
  ///     use of the "ordering" heuristic described by Heikki Tauriainen
  ///     in Research Report A96 from the Helsinki University of Technology.
  ///
  ///   Example:
  ///   \code
  ///   Tau03_opt
  ///   Tau03_opt(!weights)
  ///   Tau03_opt(!redweights)
  ///   Tau03_opt(condstack)
  ///   Tau03_opt(condstack !weights)
  ///   Tau03_opt(condstack !redweights)
  ///   \endcode
361
362
  SPOT_API emptiness_check_instantiator_ptr
  make_emptiness_check_instantiator(const char* name, const char** err);
363

364
365
  /// @}

366
367
368
369

  /// \addtogroup emptiness_check_algorithms Emptiness-check algorithms
  /// \ingroup emptiness_check

370
  /// \addtogroup twa_run TωA runs and supporting functions
371
372
373
  /// \ingroup emptiness_check
  /// @{

374
375
  /// An accepted run, for a twa.
  struct SPOT_API twa_run final
376
377
378
379
  {
    struct step {
      const state* s;
      bdd label;
380
      acc_cond::mark_t acc;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
381
382

      step(const state* s, bdd label, acc_cond::mark_t acc)
383
        : s(s), label(label), acc(acc)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
384
385
386
387
388
      {
      }
      step()
      {
      }
389
390
391
392
393
394
    };

    typedef std::list<step> steps;

    steps prefix;
    steps cycle;
395
    const_twa_ptr aut;
396

397
    ~twa_run();
398
399
    twa_run(const const_twa_ptr& aut)
      : aut(aut)
400
    {
401
    }
402
403
    twa_run(const twa_run& run);
    twa_run& operator=(const twa_run& run);
404

405
406
407
408
409
410
411
412
413
    /// \brief Raise an exception of the cycle is empty.
    ///
    /// It is OK for a twa_run to have an empty cycle while the run is
    /// being filled by some procedure.  But after that, we expect
    /// cycles to be non-empty.  Calling this function will raise an
    /// std::runtime_error if the cycle is empty, giving \a where
    /// (usually the name of the calling function) as context.
    void ensure_non_empty_cycle(const char* where) const;

414
415
416
417
418
419
    /// \brief Reduce an accepting run.
    ///
    /// Return a run which is still accepting for <code>aut</code>,
    /// but is no longer than this one.
    twa_run_ptr reduce() const;

420
421
422
423
424
425
426
427
428
429
    /// \brief Project an accepting run
    ///
    /// This only works if the automaton associated to this run has
    /// been created with otf_product() or product(), and \a other is
    /// one of the two operands of the product.
    ///
    /// Use the \a right Boolean to specify whether \a other was a
    /// left or right operand.
    twa_run_ptr project(const const_twa_ptr& other, bool right = false);

430
431
432
433
    /// \brief Replay a run.
    ///
    /// This is similar to <code>os << run;</code>, except that the
    /// run is actually replayed on the automaton while it is printed.
434
    /// The output will stop if the run cannot be completed.
435
436
437
438
439
440
441
    ///
    /// \param os the stream on which the replay should be traced
    /// \param debug if set the output will be more verbose and extra
    ///              debugging informations will be output on failure
    /// \return true iff the run could be completed
    bool replay(std::ostream& os, bool debug = false) const;

442
443
444
445
446
    /// \brief Highlight the accepting run on the automaton.
    ///
    /// Note that this works only if the automaton is a twa_graph_ptr.
    void highlight(unsigned color);

447
448
449
    /// \brief Return a twa_graph_ptr corresponding to \a run
    ///
    /// Identical states are merged.
450
451
452
453
    ///
    /// If \a preserve_names is set, the created states are named
    /// using the format_state() result from the original state.
    twa_graph_ptr as_twa(bool preserve_names = false) const;
454

455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
    /// \brief Display a twa_run.
    ///
    /// Output the prefix and cycle parts of the twa_run \a run on \a os.
    ///
    /// The automaton object (stored by \a run) is used only to format
    /// the states, and to know how to print the BDDs describing the
    /// conditions and acceptance conditions of the run; it is
    /// <b>not</b> used to replay the run.  In other words this
    /// function will work even if the twa_run you are trying to print
    /// appears to connect states that are not connected.
    ///
    /// This is unlike replay_twa_run(), which will ensure the run
    /// actually exists in the automaton (and will also display any
    /// transition annotation).
    SPOT_API
470
    friend std::ostream& operator<<(std::ostream& os, const twa_run& run);
471
  };
472
  /// @}
473
474
475

  /// \addtogroup emptiness_check_stats Emptiness-check statistics
  /// \ingroup emptiness_check
476
}