tgbabddconcrete.cc 5.89 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* local_state,
97
98
			       const state* global_state,
			       const tgba* global_automaton) const
99
  {
100
    const state_bdd* s = down_cast<const state_bdd*>(local_state);
101
    assert(s);
102
    bdd succ_set = data_.relation & s->as_bdd();
103
104
105
106
107
108
109
110
    // If we are in a product, inject the local conditions of
    // all other automata to limit the number of successors.
    if (global_automaton)
      {
	bdd varused = bdd_support(succ_set);
	bdd global_conds = global_automaton->support_conditions(global_state);
	succ_set = bdd_appexcomp(succ_set, global_conds, bddop_and, varused);
      }
111
112
113
114
115
116
117
118
119
    // 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;
      }
120
121
122
    return new tgba_succ_iterator_concrete(data_, succ_set);
  }

123
124
125
  bdd
  tgba_bdd_concrete::compute_support_conditions(const state* st) const
  {
126
    const state_bdd* s = down_cast<const state_bdd*>(st);
127
128
129
130
131
132
133
    assert(s);
    return bdd_relprod(s->as_bdd(), data_.relation, data_.notvar_set);
  }

  bdd
  tgba_bdd_concrete::compute_support_variables(const state* st) const
  {
134
    const state_bdd* s = down_cast<const state_bdd*>(st);
135
136
137
138
139
    assert(s);
    bdd succ_set = data_.relation & s->as_bdd();
    // bdd_support must be called BEFORE bdd_exist
    // because bdd_exist(bdd_support((a&Next[f])|(!a&Next[g])),Next[*])
    // is obviously not the same as bdd_support(a|!a).
140
    // In other words: we cannot reuse compute_support_conditions() for
141
    // this computation.
142
143
144
145
146
147
148
149
    //
    // Also we need to inject the support of acceptance conditions, because a
    // "Next[f]" that looks like one transition might in fact be two
    // transitions if the acceptance condition distinguish between
    // letters, e.g. "Next[f] & ((a & Acc[1]) | (!a))"
    return bdd_exist(bdd_support(succ_set)
		     & data_.acceptance_conditions_support,
		     data_.notvar_set);
150
151
  }

152
153
154
  std::string
  tgba_bdd_concrete::format_state(const state* state) const
  {
155
    const state_bdd* s = down_cast<const state_bdd*>(state);
156
    assert(s);
157
    return bdd_format_set(get_dict(), s->as_bdd());
158
159
  }

160
  bdd_dict*
161
162
  tgba_bdd_concrete::get_dict() const
  {
163
    return data_.dict;
164
165
  }

166
  bdd
167
  tgba_bdd_concrete::all_acceptance_conditions() const
168
  {
169
    return data_.all_acceptance_conditions;
170
171
172
  }

  bdd
173
  tgba_bdd_concrete::neg_acceptance_conditions() const
174
175
176
177
  {
    return data_.negacc_set;
  }

178
179
180
181
182
183
  const tgba_bdd_core_data&
  tgba_bdd_concrete::get_core_data() const
  {
    return data_;
  }

184
185
186
187
188
189
190
  void
  tgba_bdd_concrete::delete_unaccepting_scc()
  {
    data_.delete_unaccepting_scc(init_);
    set_init_state(init_);
  }

191
}