twa.cc 2.99 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2011, 2014, 2015, 2016 Laboratoire de Recherche et
// Developpement de l'EPITA (LRDE).
4
// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23
24
25
26
#include <spot/twa/twa.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/remfin.hh>
27
#include <utility>
28
29
30

namespace spot
{
31
  twa::twa(const bdd_dict_ptr& d)
32
    : iter_cache_(nullptr),
33
      dict_(d)
34
  {
35
    props = 0U;
36
    bddaps_ = bddtrue;
37
  }
38

39
  twa::~twa()
40
  {
41
    delete iter_cache_;
42
    release_named_properties();
43
    get_dict()->unregister_all_my_variables(this);
44
  }
45
46

  state*
47
  twa::project_state(const state* s,
48
                      const const_twa_ptr& t) const
49
  {
50
    if (t.get() == this)
51
      return s->clone();
52
    return nullptr;
53
54
  }

55
  bool
56
  twa::is_empty() const
57
58
59
60
  {
    // FIXME: This should be improved based on properties of the
    // automaton.  For instance we do not need couvreur99 is we know
    // the automaton is weak.
61
62
63
    auto a = shared_from_this();
    if (a->acc().uses_fin_acceptance())
      {
64
65
66
67
        auto aa = std::dynamic_pointer_cast<const twa_graph>(a);
        if (!aa)
          aa = make_twa_graph(a, prop_set::all());
        a = remove_fin(aa);
68
69
      }
    return !couvreur99(a)->check();
70
71
  }

72
  void
73
  twa::set_named_prop(std::string s,
74
                      void* val, std::function<void(void*)> destructor)
75
76
  {
    auto p = named_prop_.emplace(std::piecewise_construct,
77
78
                                 std::forward_as_tuple(s),
                                 std::forward_as_tuple(val, destructor));
79
80
    if (!p.second)
      {
81
82
        p.first->second.second(p.first->second.first);
        p.first->second = std::make_pair(val, destructor);
83
84
85
86
      }
  }

  void*
87
  twa::get_named_prop_(std::string s) const
88
89
90
91
92
93
94
  {
    auto i = named_prop_.find(s);
    if (i == named_prop_.end())
      return nullptr;
    return i->second.first;
  }

95
96
97
98
99
100
101
102
103
104
105
  void
  twa::unregister_ap(int b)
  {
    auto d = get_dict();
    assert(d->bdd_map[b].type == bdd_dict::var);
    auto pos = std::find(aps_.begin(), aps_.end(), d->bdd_map[b].f);
    assert(pos != aps_.end());
    aps_.erase(pos);
    d->unregister_variable(b, this);
    bddaps_ = bdd_exist(bddaps_, bdd_ithvar(b));
  }
106
107
108



109
}