tgbagraph.hh 11.2 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
// de l'Epita.
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
//
// 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
// the Free Software Foundation; either version 3 of the License, or
// (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
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

20
#pragma once
21

22
#include "fwd.hh"
23
#include "graph/graph.hh"
24
#include "graph/ngraph.hh"
25 26
#include "tgba/bdddict.hh"
#include "tgba/tgba.hh"
27
#include "tgbaalgos/dupexp.hh"
28 29 30 31 32 33 34 35
#include <sstream>

namespace spot
{

  struct SPOT_API tgba_graph_state: public spot::state
  {
  public:
36 37 38 39 40
    tgba_graph_state():
      spot::state()
    {
    }

41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77
    virtual ~tgba_graph_state() noexcept
    {
    }

    virtual int compare(const spot::state* other) const
    {
      auto o = down_cast<const tgba_graph_state*>(other);
      assert(o);

      // Do not simply return "other - this", it might not fit in an int.
      if (o < this)
	return -1;
      if (o > this)
	return 1;
      return 0;
    }

    virtual size_t hash() const
    {
      return
	reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
    }

    virtual tgba_graph_state*
    clone() const
    {
      return const_cast<tgba_graph_state*>(this);
    }

    virtual void destroy() const
    {
    }
  };

  struct SPOT_API tgba_graph_trans_data
  {
    bdd cond;
78
    acc_cond::mark_t acc;
79 80

    explicit tgba_graph_trans_data()
81
      : cond(bddfalse), acc(0)
82 83 84
    {
    }

85
    tgba_graph_trans_data(bdd cond, acc_cond::mark_t acc = 0U)
86 87 88
      : cond(cond), acc(acc)
    {
    }
89 90 91 92 93 94 95 96 97

    bool operator<(const tgba_graph_trans_data& other) const
    {
      if (cond.id() < other.cond.id())
	return true;
      if (cond.id() > other.cond.id())
	return false;
      return acc < other.acc;
    }
98 99 100 101 102 103

    bool operator==(const tgba_graph_trans_data& other) const
    {
      return cond.id() == other.cond.id() &&
        acc == other.acc;
    }
104 105 106 107
  };


  template<class Graph>
108
  class SPOT_API twa_graph_succ_iterator final:
109
    public twa_succ_iterator
110 111 112 113 114 115 116 117 118
  {
  private:
    typedef typename Graph::transition transition;
    typedef typename Graph::state_data_t state;
    const Graph* g_;
    transition t_;
    transition p_;

  public:
119
    twa_graph_succ_iterator(const Graph* g, transition t)
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
      : g_(g), t_(t)
    {
    }

    virtual void recycle(transition t)
    {
      t_ = t;
    }

    virtual bool first()
    {
      p_ = t_;
      return p_;
    }

    virtual bool next()
    {
      p_ = g_->trans_storage(p_).next_succ;
      return p_;
    }

    virtual bool done() const
    {
      return !p_;
    }

    virtual tgba_graph_state* current_state() const
    {
      assert(!done());
      return const_cast<tgba_graph_state*>
	(&g_->state_data(g_->trans_storage(p_).dst));
    }

    virtual bdd current_condition() const
    {
      assert(!done());
      return g_->trans_data(p_).cond;
    }

159
    virtual acc_cond::mark_t current_acceptance_conditions() const
160 161 162 163 164 165 166 167 168 169 170 171
    {
      assert(!done());
      return g_->trans_data(p_).acc;
    }

    transition pos() const
    {
      return p_;
    }

  };

172
  class SPOT_API twa_graph final: public twa
173
  {
174
  public:
175
    typedef digraph<tgba_graph_state, tgba_graph_trans_data> graph_t;
176
    typedef graph_t::trans_storage_t trans_storage_t;
177 178

  protected:
179
    graph_t g_;
180
    mutable unsigned init_number_;
181 182

  public:
183
    twa_graph(const bdd_dict_ptr& dict)
184
      : twa(dict),
185
	init_number_(0)
186 187 188
    {
    }

189
    explicit twa_graph(const const_twa_graph_ptr& other, prop_set p)
190
      : twa(other->get_dict()),
191 192
        g_(other->g_), init_number_(other->init_number_)
      {
193
	copy_acceptance_of(other);
194
	copy_ap_of(other);
195
	prop_copy(other, p);
196 197
      }

198
    virtual ~twa_graph()
199
    {
200
      get_dict()->unregister_all_my_variables(this);
201
      // Prevent this state from being destroyed by ~twa(),
202 203 204 205
      // as the state will be destroyed when g_ is destroyed.
      last_support_conditions_input_ = 0;
    }

206 207
    // FIXME: Once we ditch GCC 4.6, we can using a template aliases
    // (supported from GCC 4.7 onward) instead of this.
208 209 210
    template <typename State_Name,
	      typename Name_Hash = std::hash<State_Name>,
	      typename Name_Equal = std::equal_to<State_Name>>
211 212 213 214 215 216 217 218 219
    struct namer
    {
      typedef named_graph<graph_t, State_Name, Name_Hash, Name_Equal> type;
    };

    template <typename State_Name,
	      typename Name_Hash = std::hash<State_Name>,
	      typename Name_Equal = std::equal_to<State_Name>>
    typename namer<State_Name, Name_Hash, Name_Equal>::type*
220 221 222 223 224
    create_namer()
    {
      return new named_graph<graph_t, State_Name, Name_Hash, Name_Equal>(g_);
    }

225 226 227 228 229
    graph_t& get_graph()
    {
      return g_;
    }

230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
    const graph_t& get_graph() const
    {
      return g_;
    }

    unsigned num_states() const
    {
      return g_.num_states();
    }

    unsigned num_transitions() const
    {
      return g_.num_transitions();
    }

    void set_init_state(graph_t::state s)
    {
247 248
      assert(s < num_states());
      init_number_ = s;
249 250 251 252
    }

    void set_init_state(const state* s)
    {
253
      set_init_state(state_number(s));
254 255
    }

256
    graph_t::state get_init_state_number() const
257 258 259
    {
      if (num_states() == 0)
	const_cast<graph_t&>(g_).new_state();
260
      return init_number_;
261 262
    }

263 264
    // FIXME: The return type ought to be const.
    virtual tgba_graph_state* get_init_state() const
265 266 267
    {
      if (num_states() == 0)
	const_cast<graph_t&>(g_).new_state();
268
      return const_cast<tgba_graph_state*>(state_from_number(init_number_));
269 270
    }

271
    virtual twa_succ_iterator*
272 273 274 275
    succ_iter(const state* st) const
    {
      auto s = down_cast<const typename graph_t::state_storage_t*>(st);
      assert(s);
276
      assert(!s->succ || g_.valid_trans(s->succ));
277 278 279 280

      if (this->iter_cache_)
	{
	  auto it =
281
	    down_cast<twa_graph_succ_iterator<graph_t>*>(this->iter_cache_);
282 283 284 285
	  it->recycle(s->succ);
	  this->iter_cache_ = nullptr;
	  return it;
	}
286
      return new twa_graph_succ_iterator<graph_t>(&g_, s->succ);
287 288 289 290 291 292 293 294 295 296
    }

    graph_t::state
    state_number(const state* st) const
    {
      auto s = down_cast<const typename graph_t::state_storage_t*>(st);
      assert(s);
      return s - &g_.state_storage(0);
    }

297
    const tgba_graph_state*
298 299 300 301 302
    state_from_number(graph_t::state n) const
    {
      return &g_.state_data(n);
    }

303
    std::string format_state(unsigned n) const
304 305
    {
      std::stringstream ss;
306
      ss << n;
307 308 309
      return ss.str();
    }

310 311 312 313 314
    virtual std::string format_state(const state* st) const
    {
      return format_state(state_number(st));
    }

315
    tgba_graph_trans_data& trans_data(const twa_succ_iterator* it)
316
    {
317
      auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
318 319 320
      return g_.trans_data(i->pos());
    }

321 322 323 324
    tgba_graph_trans_data& trans_data(unsigned t)
    {
      return g_.trans_data(t);
    }
325

326
    const tgba_graph_trans_data& trans_data(const twa_succ_iterator* it) const
327
    {
328
      auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
329 330 331 332 333 334 335 336
      return g_.trans_data(i->pos());
    }

    const tgba_graph_trans_data& trans_data(unsigned t) const
    {
      return g_.trans_data(t);
    }

337
    trans_storage_t& trans_storage(const twa_succ_iterator* it)
338
    {
339
      auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
340 341 342
      return g_.trans_storage(i->pos());
    }

343
    trans_storage_t& trans_storage(unsigned t)
344 345 346 347
    {
      return g_.trans_storage(t);
    }

348
    const trans_storage_t
349
      trans_storage(const twa_succ_iterator* it) const
350
    {
351
      auto* i = down_cast<const twa_graph_succ_iterator<graph_t>*>(it);
352 353 354
      return g_.trans_storage(i->pos());
    }

355
    const trans_storage_t trans_storage(unsigned t) const
356 357 358 359
    {
      return g_.trans_storage(t);
    }

360 361 362 363 364 365 366 367 368 369 370
    unsigned new_state()
    {
      return g_.new_state();
    }

    unsigned new_states(unsigned n)
    {
      return g_.new_states(n);
    }

    unsigned new_transition(unsigned src, unsigned dst,
371
			    bdd cond, acc_cond::mark_t acc = 0U)
372 373 374 375
    {
      return g_.new_transition(src, dst, cond, acc);
    }

376 377 378 379
    unsigned new_acc_transition(unsigned src, unsigned dst,
				bdd cond, bool acc = true)
    {
      if (acc)
380
	return g_.new_transition(src, dst, cond, acc_.all_sets());
381 382 383 384
      else
	return g_.new_transition(src, dst, cond);
    }

385
#ifndef SWIG
386 387 388 389 390 391 392 393 394 395 396 397 398 399
    auto out(unsigned src) const
      SPOT_RETURN(g_.out(src));
    auto out(unsigned src)
      SPOT_RETURN(g_.out(src));

    auto states() const
      SPOT_RETURN(g_.states());
    auto states()
      SPOT_RETURN(g_.states());

    auto transitions() const
      SPOT_RETURN(g_.transitions());
    auto transitions()
      SPOT_RETURN(g_.transitions());
400

401 402 403 404 405
    auto transition_vector() const
      SPOT_RETURN(g_.transition_vector());
    auto transition_vector()
      SPOT_RETURN(g_.transition_vector());

406
    auto is_dead_transition(const graph_t::trans_storage_t& t) const
407
      SPOT_RETURN(g_.is_dead_transition(t));
408
#endif
409

410
    virtual bdd compute_support_conditions(const state* s) const
411
    {
412 413 414 415
      bdd sum = bddfalse;
      for (auto& t: out(state_number(s)))
	sum |= t.cond;
      return sum;
416
    }
417 418 419

    /// Iterate over all transitions, and merge those with compatible
    /// extremities and acceptance.
420
    void merge_transitions();
421

422 423 424
    /// Remove all states without successors.
    void purge_dead_states();

425 426 427
    /// Remove all unreachable states.
    void purge_unreachable_states();

428 429
    bool state_is_accepting(unsigned s) const
    {
430
      assert(has_state_based_acc() || acc_.num_sets() == 0);
431 432 433
      for (auto& t: g_.out(s))
	// Stop at the first transition, since the remaining should be
	// labeled identically.
434
	return acc_.accepting(t.acc);
435 436 437 438 439 440 441 442
      return false;
    }

    bool state_is_accepting(const state* s) const
    {
      return state_is_accepting(state_number(s));
    }

443
    bool operator==(const twa_graph& aut) const
444 445 446 447 448 449 450 451 452 453
    {
      if (num_states() != aut.num_states() ||
          num_transitions() != aut.num_transitions() ||
          acc().num_sets() != aut.acc().num_sets())
        return false;
      auto& trans1 = transition_vector();
      auto& trans2 = aut.transition_vector();
      return std::equal(trans1.begin() + 1, trans1.end(),
                        trans2.begin() + 1);
    }
454 455
  };

456
  inline twa_graph_ptr make_twa_graph(const bdd_dict_ptr& dict)
457
  {
458
    return std::make_shared<twa_graph>(dict);
459
  }
460

461
  inline twa_graph_ptr make_twa_graph(const twa_graph_ptr& aut,
462
					    twa::prop_set p)
463
  {
464
    return std::make_shared<twa_graph>(aut, p);
465 466
  }

467
  inline twa_graph_ptr make_twa_graph(const const_twa_graph_ptr& aut,
468
					    twa::prop_set p)
469
  {
470
    return std::make_shared<twa_graph>(aut, p);
471 472
  }

473
  inline twa_graph_ptr make_twa_graph(const const_twa_ptr& aut,
474
					    twa::prop_set p)
475
  {
476
    auto a = std::dynamic_pointer_cast<const twa_graph>(aut);
477
    if (a)
478
      return std::make_shared<twa_graph>(a, p);
479
    else
480
      return tgba_dupexp_dfs(aut, p);
481
  }
482
}