tgbabddconcrete.cc 4.61 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
4
// Copyright (C) 2003 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
#include "tgbabddconcrete.hh"
24
#include "bddprint.hh"
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
25
#include <cassert>
26
27
28
29

namespace spot
{
  tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact)
30
    : data_(fact.get_core_data())
31
  {
32
    get_dict()->register_all_variables_of(&fact, this);
33
34
35
  }

  tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init)
36
    : data_(fact.get_core_data())
37
  {
38
    get_dict()->register_all_variables_of(&fact, this);
39
    set_init_state(init);
40
41
42
43
  }

  tgba_bdd_concrete::~tgba_bdd_concrete()
  {
44
    get_dict()->unregister_all_my_variables(this);
45
46
47
48
49
  }

  void
  tgba_bdd_concrete::set_init_state(bdd s)
  {
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
78
79
    // Usually, the ltl2tgba translator will return an
    // initial state which does not include all true Now variables,
    // even though the truth of some Now variables is garanteed.
    //
    // For instance, when building the automata for the formula GFa,
    // the translator will define the following two equivalences
    //    Now[Fa] <=> a | (Prom[a] & Next[Fa])
    //    Now[GFa] <=> Now[Fa] & Next[GFa]
    // and return Now[GFa] as initial state.
    //
    // Starting for state Now[GFa], we could then build
    // the following automaton:
    //    In state Now[GFa]:
    //        if `a', go to state Now[GFa] & Now[Fa]
    //        if `!a', go to state Now[GFa] & Now[Fa] with Prom[a]
    //    In state Now[GFa] & Now[Fa]:
    //        if `a', go to state Now[GFa] & Now[Fa]
    //        if `!a', go to state Now[GFa] & Now[Fa] with Prom[a]
    //
    // As we can see, states Now[GFa] and Now[GFa] & Now[Fa] share
    // the same actions.  This is no surprise, because
    // Now[GFa] <=> Now[GFa] & Now[Fa] according to the equivalences
    // defined by the translator.
    //
    // This happens because we haven't completed the initial
    // state with the value of other Now variables.  We can
    // complete this state with the other equivalant Now variables
    // here, but we can't do anything about the remaining unknown
    // variables.
    s &= bdd_relprod(s, data_.relation, data_.notnow_set);
80
81
82
    init_ = s;
  }

83
  state_bdd*
84
  tgba_bdd_concrete::get_init_state() const
85
86
87
88
89
90
  {
    return new state_bdd(init_);
  }

  bdd
  tgba_bdd_concrete::get_init_bdd() const
91
92
93
94
95
  {
    return init_;
  }

  tgba_succ_iterator_concrete*
96
  tgba_bdd_concrete::succ_iter(const state* state) const
97
  {
98
    const state_bdd* s = down_cast<const state_bdd*>(state);
99
    assert(s);
100
    bdd succ_set = data_.relation & s->as_bdd();
101
102
103
104
105
106
107
108
109
    // Do not allocate an iterator if we can reuse one.
    if (iter_cache_)
      {
	tgba_succ_iterator_concrete* res =
	  down_cast<tgba_succ_iterator_concrete*>(iter_cache_);
	iter_cache_ = nullptr;
	res->recycle(succ_set);
	return res;
      }
110
111
112
    return new tgba_succ_iterator_concrete(data_, succ_set);
  }

113
114
115
  bdd
  tgba_bdd_concrete::compute_support_conditions(const state* st) const
  {
116
    const state_bdd* s = down_cast<const state_bdd*>(st);
117
118
119
120
    assert(s);
    return bdd_relprod(s->as_bdd(), data_.relation, data_.notvar_set);
  }

121
122
123
  std::string
  tgba_bdd_concrete::format_state(const state* state) const
  {
124
    const state_bdd* s = down_cast<const state_bdd*>(state);
125
    assert(s);
126
    return bdd_format_set(get_dict(), s->as_bdd());
127
128
  }

129
  bdd_dict*
130
131
  tgba_bdd_concrete::get_dict() const
  {
132
    return data_.dict;
133
134
  }

135
  bdd
136
  tgba_bdd_concrete::all_acceptance_conditions() const
137
  {
138
    return data_.all_acceptance_conditions;
139
140
141
  }

  bdd
142
  tgba_bdd_concrete::neg_acceptance_conditions() const
143
144
145
146
  {
    return data_.negacc_set;
  }

147
148
149
150
151
152
  const tgba_bdd_core_data&
  tgba_bdd_concrete::get_core_data() const
  {
    return data_;
  }

153
154
155
156
157
158
159
  void
  tgba_bdd_concrete::delete_unaccepting_scc()
  {
    data_.delete_unaccepting_scc(init_);
    set_init_state(init_);
  }

160
}