emptiness.hh 10 KB
Newer Older
1
// -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et
3
// 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
#include "misc/optionmap.hh"
30
#include "twa/twagraph.hh"
31
#include "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
  /// All emptiness-check algorithms follow the same interface.
  /// Basically once you have constructed an instance of
  /// spot::emptiness_check (by instantiating a subclass, or calling a
  /// functions construct such instance; see \ref
  /// emptiness_check_algorithms "this list"), you should call
  /// spot::emptiness_check::check() to check the automaton.
48
  ///
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
  /// 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
67
  /// type spot::twa_run.  \ref twa_run "This page" gathers existing
68 69 70
  /// operations on these objects.
  ///
  /// @{
71 72 73 74 75 76

  /// \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.
77
  class SPOT_API emptiness_check_result
78 79
  {
  public:
80
    emptiness_check_result(const const_twa_ptr& a,
81
			   option_map o = option_map())
82 83 84 85 86 87
      : a_(a), o_(o)
    {
    }

    virtual
    ~emptiness_check_result()
88 89 90
    {
    }

91 92 93 94 95 96 97 98 99 100 101 102
    /// \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).
103
    virtual twa_run_ptr accepting_run();
104 105

    /// The automaton on which an accepting_run() was found.
106
    const const_twa_ptr&
107 108 109 110
    automaton() const
    {
      return a_;
    }
111

112 113 114 115 116 117 118
    /// Return the options parametrizing how the accepting run is computed.
    const option_map&
    options() const
    {
      return o_;
    }

119 120
    /// Modify the algorithm options.
    const char* parse_options(char* options);
121

122 123 124
    /// Return statistics, if available.
    virtual const unsigned_statistics* statistics() const;

125
  protected:
126 127
    /// Notify option updates.
    virtual void options_updated(const option_map& old);
128

129
    const_twa_ptr a_;		///< The automaton.
130
    option_map o_;		///< The options.
131 132
  };

133 134
  typedef std::shared_ptr<emptiness_check_result> emptiness_check_result_ptr;

135
  /// Common interface to emptiness check algorithms.
136 137
  class SPOT_API emptiness_check:
    public std::enable_shared_from_this<emptiness_check>
138 139
  {
  public:
140
    emptiness_check(const const_twa_ptr& a, option_map o = option_map())
141
      : a_(a), o_(o)
142 143
    {
    }
144 145
    virtual ~emptiness_check();

146
    /// The automaton that this emptiness-check inspects.
147
    const const_twa_ptr&
148 149 150 151 152
    automaton() const
    {
      return a_;
    }

153 154 155 156 157 158 159
    /// Return the options parametrizing how the emptiness check is realized.
    const option_map&
    options() const
    {
      return o_;
    }

160 161 162 163 164
    /// 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;
165

166 167
    /// \brief Check whether the automaton contain an accepting run.
    ///
168
    /// Return 0 if the automaton accepts no run.  Return an instance
169 170 171 172 173 174 175
    /// 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.
176 177 178 179
    ///
    /// Some emptiness_check algorithms, especially those using bit state
    /// hashing may return 0 even if the automaton is not empty.
    /// \see safe()
180
    virtual emptiness_check_result_ptr check() = 0;
181

182 183 184
    /// Return statistics, if available.
    virtual const unsigned_statistics* statistics() const;

185 186 187
    /// Return emptiness check statistics, if available.
    virtual const ec_statistics* emptiness_check_statistics() const;

188 189
    /// Print statistics, if any.
    virtual std::ostream& print_stats(std::ostream& os) const;
190

191 192
    /// Notify option updates.
    virtual void options_updated(const option_map& old);
193

194
  protected:
195
    const_twa_ptr a_;		///< The automaton.
196
    option_map o_;		///< The options
197 198
  };

199 200 201 202 203
  typedef std::shared_ptr<emptiness_check> emptiness_check_ptr;

  class emptiness_check_instantiator;
  typedef std::shared_ptr<emptiness_check_instantiator>
    emptiness_check_instantiator_ptr;
204 205

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

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

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

    /// \brief Minimum number of acceptance conditions supported by
    /// the emptiness check.
    unsigned int min_acceptance_conditions() const;

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

239 240 241
    option_map o_;
    void *info_;
  };
242
  /// @}
243

244 245 246 247 248 249 250 251 252 253 254
  /// \brief Create an emptiness-check instantiator, given the name
  /// of an emptiness check.
  ///
  /// \a name should have the form \c "name" or \c "name(options)".
  ///
  /// On error, the function returns 0.  If the name of the algorithm
  /// was unknown, \c *err will be set to \c name.  If some fragment of
  /// the options could not be parsed, \c *err will point to that
  /// fragment.
  SPOT_API emptiness_check_instantiator_ptr
  make_emptiness_check_instantiator(const char* name, const char** err);
255

256 257 258 259 260

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


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
261
  /// \addtogroup twa_run TGBA runs and supporting functions
262 263 264 265
  /// \ingroup emptiness_check
  /// @{

  /// An accepted run, for a tgba.
266
  struct SPOT_API twa_run
267 268 269 270
  {
    struct step {
      const state* s;
      bdd label;
271
      acc_cond::mark_t acc;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
272 273 274 275 276 277 278 279

      step(const state* s, bdd label, acc_cond::mark_t acc)
	: s(s), label(label), acc(acc)
      {
      }
      step()
      {
      }
280 281 282 283 284 285 286
    };

    typedef std::list<step> steps;

    steps prefix;
    steps cycle;

287 288
    ~twa_run();
    twa_run()
289 290
    {
    };
291 292
    twa_run(const twa_run& run);
    twa_run& operator=(const twa_run& run);
293 294
  };

295
  /// \brief Display a twa_run.
296
  ///
297
  /// Output the prefix and cycle parts of the twa_run \a run on \a os.
298
  ///
299 300 301 302
  /// The automaton \a a 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
303
  /// the twa_run you are trying to print appears to connect states
304
  /// of \a a that are not connected.
305
  ///
306
  /// This is unlike replay_twa_run(), which will ensure the run
307 308
  /// actually exists in the automaton (and will also display any
  /// transition annotation).
309
  SPOT_API std::ostream&
310
  print_twa_run(std::ostream& os,
311
		 const const_twa_ptr& a,
312
		 const const_twa_run_ptr& run);
313

314 315 316 317
  /// \brief Return an explicit_tgba corresponding to \a run (i.e. comparable
  /// states are merged).
  ///
  /// \pre \a run must correspond to an actual run of the automaton \a a.
318
  SPOT_API twa_graph_ptr
319
  twa_run_to_tgba(const const_twa_ptr& a, const const_twa_run_ptr& run);
320

321
  /// @}
322 323 324

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