taexplicit.hh 6.56 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
4 5 6 7 8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10 11 12
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
13
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
15
// License for more details.
16 17
//
// You should have received a copy of the GNU General Public License
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
#pragma once
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37

#include "misc/hash.hh"
#include <list>
#include "tgba/tgba.hh"
#include <set>
#include "ltlast/formula.hh"
#include <cassert>
#include "misc/bddlt.hh"
#include "ta.hh"

namespace spot
{
  // Forward declarations.  See below.
  class state_ta_explicit;
  class ta_explicit_succ_iterator;
  class ta_explicit;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
38 39
  /// Explicit representation of a spot::ta.
  /// \ingroup ta_representation
40
  class SPOT_API ta_explicit : public ta
41 42
  {
  public:
43
    ta_explicit(const const_twa_ptr& tgba,
44
		unsigned n_acc,
45
		state_ta_explicit* artificial_initial_state = 0);
46

47
    const_twa_ptr
48 49 50 51 52
    get_tgba() const;

    state_ta_explicit*
    add_state(state_ta_explicit* s);

53
    void
54
    add_to_initial_states_set(state* s, bdd condition = bddfalse);
55

56 57
    void
    create_transition(state_ta_explicit* source, bdd condition,
58 59 60
		      acc_cond::mark_t acceptance_conditions,
		      state_ta_explicit* dest,
		      bool add_at_beginning = false);
61

62 63 64 65 66
    void
    delete_stuttering_transitions();
    // ta interface
    virtual
    ~ta_explicit();
67
    virtual const states_set_t
68 69 70 71 72
    get_initial_states_set() const;

    virtual ta_succ_iterator*
    succ_iter(const spot::state* s) const;

73 74 75
    virtual ta_succ_iterator*
    succ_iter(const spot::state* s, bdd condition) const;

76
    virtual bdd_dict_ptr
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
    get_dict() const;

    virtual std::string
    format_state(const spot::state* s) const;

    virtual bool
    is_accepting_state(const spot::state* s) const;

    virtual bool
    is_livelock_accepting_state(const spot::state* s) const;

    virtual bool
    is_initial_state(const spot::state* s) const;

    virtual bdd
    get_state_condition(const spot::state* s) const;

94 95 96
    virtual void
    free_state(const spot::state* s) const;

97 98 99 100 101 102 103 104 105 106 107 108 109
    spot::state*
    get_artificial_initial_state() const
    {
      return (spot::state*) artificial_initial_state_;
    }

    void
    set_artificial_initial_state(state_ta_explicit* s)
    {
      artificial_initial_state_ = s;

    }

110 111 112
    virtual void
    delete_stuttering_and_hole_successors(spot::state* s);

113 114 115 116 117 118
    ta::states_set_t
    get_states_set()
    {
      return states_set_;
    }

119 120
  private:
    // Disallow copy.
121 122
    ta_explicit(const ta_explicit& other) SPOT_DELETED;
    ta_explicit& operator=(const ta_explicit& other) SPOT_DELETED;
123

124
    const_twa_ptr tgba_;
125
    state_ta_explicit* artificial_initial_state_;
126 127
    ta::states_set_t states_set_;
    ta::states_set_t initial_states_set_;
128 129 130
  };

  /// states used by spot::ta_explicit.
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
131
  /// \ingroup ta_representation
132
  class SPOT_API state_ta_explicit : public spot::state
133
  {
134
#ifndef SWIG
135 136
  public:

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
137
    /// Explicit transitions.
138 139 140
    struct transition
    {
      bdd condition;
141
      acc_cond::mark_t acceptance_conditions;
142 143 144 145 146 147 148
      state_ta_explicit* dest;
    };

    typedef std::list<transition*> transitions;

    state_ta_explicit(const state* tgba_state, const bdd tgba_condition,
        bool is_initial_state = false, bool is_accepting_state = false,
149
        bool is_livelock_accepting_state = false, transitions* trans = 0) :
150 151 152 153 154 155 156 157 158 159 160 161 162 163
      tgba_state_(tgba_state), tgba_condition_(tgba_condition),
          is_initial_state_(is_initial_state), is_accepting_state_(
              is_accepting_state), is_livelock_accepting_state_(
              is_livelock_accepting_state), transitions_(trans)
    {
    }

    virtual int
    compare(const spot::state* other) const;
    virtual size_t
    hash() const;
    virtual state_ta_explicit*
    clone() const;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
164 165
    virtual void
    destroy() const
166 167 168
    {
    }

169 170 171 172 173 174 175 176
    virtual
    ~state_ta_explicit()
    {
    }

    transitions*
    get_transitions() const;

177 178 179 180
    // return transitions filtred by condition
    transitions*
    get_transitions(bdd condition) const;

181
    void
182
    add_transition(transition* t, bool add_at_beginning = false);
183 184 185 186 187 188 189 190 191 192 193 194 195

    const state*
    get_tgba_state() const;
    const bdd
    get_tgba_condition() const;
    bool
    is_accepting_state() const;
    void
    set_accepting_state(bool is_accepting_state);
    bool
    is_livelock_accepting_state() const;
    void
    set_livelock_accepting_state(bool is_livelock_accepting_state);
196

197 198 199 200
    bool
    is_initial_state() const;
    void
    set_initial_state(bool is_initial_state);
201

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
202
    /// \brief Return true if the state has no successors
203 204 205
    bool
    is_hole_state() const;

Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
206 207
    /// \brief Remove stuttering transitions
    /// and transitions leading to states having no successors
208 209 210 211 212
    void
    delete_stuttering_and_hole_successors();

    void
    free_transitions();
213

214
    state_ta_explicit* stuttering_reachable_livelock;
215 216 217 218 219 220 221
  private:
    const state* tgba_state_;
    const bdd tgba_condition_;
    bool is_initial_state_;
    bool is_accepting_state_;
    bool is_livelock_accepting_state_;
    transitions* transitions_;
222 223
    std::unordered_map<int, transitions*, std::hash<int>>
      transitions_by_condition;
224
#endif // !SWIG
225 226 227
  };

  /// Successor iterators used by spot::ta_explicit.
228
  class SPOT_API ta_explicit_succ_iterator : public ta_succ_iterator
229 230 231 232
  {
  public:
    ta_explicit_succ_iterator(const state_ta_explicit* s);

233 234
    ta_explicit_succ_iterator(const state_ta_explicit* s, bdd condition);

235 236 237
    virtual bool first();
    virtual bool next();
    virtual bool done() const;
238 239 240 241 242 243

    virtual state*
    current_state() const;
    virtual bdd
    current_condition() const;

244
    virtual acc_cond::mark_t
245 246
    current_acceptance_conditions() const;

247 248 249 250 251
  private:
    state_ta_explicit::transitions* transitions_;
    state_ta_explicit::transitions::const_iterator i_;
  };

252 253 254
  typedef std::shared_ptr<ta_explicit> ta_explicit_ptr;
  typedef std::shared_ptr<const ta_explicit> const_ta_explicit_ptr;

255
  inline ta_explicit_ptr make_ta_explicit(const const_twa_ptr& tgba,
256
					  unsigned n_acc,
257 258 259
					  state_ta_explicit*
					  artificial_initial_state = 0)
  {
260
    return std::make_shared<ta_explicit>(tgba, n_acc, artificial_initial_state);
261
  }
262
}