sccfilter.cc 6.47 KB
Newer Older
1
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
2
// Développement de l'Epita (LRDE).
3
4
5
6
7
//
// 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
8
// the Free Software Foundation; either version 3 of the License, or
9
10
11
12
13
14
15
16
// (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
17
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
18
19
20
21
22

#include "sccfilter.hh"
#include "tgba/tgbaexplicit.hh"
#include "reachiter.hh"
#include "tgbaalgos/scc.hh"
23
#include "misc/bddop.hh"
24
25
26
27
28
29
#include <sstream>

namespace spot
{
  namespace
  {
30
31
32
33
34
35
36
37
    static
    state_explicit_number::transition*
    create_transition(const tgba*, tgba_explicit_number* out_aut,
		      const state*, int in, const state*, int out)
    {
      return out_aut->create_transition(in, out);
    }

38
    static
Pierre PARUTTO's avatar
Pierre PARUTTO committed
39
    state_explicit_string::transition*
40
    create_transition(const tgba* aut, tgba_explicit_string* out_aut,
41
		      const state* in_s, int, const state* out_s, int)
42
    {
43
44
45
46
      const tgba_explicit_string* a =
	static_cast<const tgba_explicit_string*>(aut);
      return out_aut->create_transition(a->get_label(in_s),
					a->get_label(out_s));
47
48
49
    }

    static
Pierre PARUTTO's avatar
Pierre PARUTTO committed
50
    state_explicit_formula::transition*
51
52
53
54
55
56
57
58
59
    create_transition(const tgba* aut, tgba_explicit_formula* out_aut,
		      const state* in_s, int, const state* out_s, int)
    {
      const tgba_explicit_formula* a =
	static_cast<const tgba_explicit_formula*>(aut);
      const ltl::formula* in_f = a->get_label(in_s);
      const ltl::formula* out_f = a->get_label(out_s);
      if (!out_aut->has_state(in_f))
	in_f->clone();
60
      if ((in_f != out_f) && !out_aut->has_state(out_f))
61
62
63
64
65
	out_f->clone();
      return out_aut->create_transition(in_f, out_f);
    }

    template<class T>
66
67
68
    class filter_iter: public tgba_reachable_iterator_depth_first
    {
    public:
Pierre PARUTTO's avatar
Pierre PARUTTO committed
69
70
      typedef T output_t;

71
72
      filter_iter(const tgba* a,
		  const scc_map& sm,
73
		  const std::vector<bool>& useless,
74
		  bdd useful, bdd strip, bool remove_all_useless)
75
	: tgba_reachable_iterator_depth_first(a),
76
	  out_(new T(a->get_dict())),
77
	  sm_(sm),
78
79
	  useless_(useless),
	  useful_(useful),
80
81
	  strip_(strip),
	  all_(remove_all_useless)
82
      {
83
	out_->set_acceptance_conditions(useful);
84
85
      }

86
      T*
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
      result()
      {
	return out_;
      }

      bool
      want_state(const state* s) const
      {
	return !useless_[sm_.scc_of_state(s)];
      }

      void
      process_link(const state* in_s, int in,
		   const state* out_s, int out,
		   const tgba_succ_iterator* si)
      {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
103
	typename output_t::state::transition* t =
104
	  create_transition(this->aut_, out_, in_s, in, out_s, out);
105
106
	out_->add_conditions(t, si->current_condition());

107
108
109
110
111
112
113
114
115
116
	// Regardless of all_, do not output any acceptance condition
	// if the destination is not in an accepting SCC.
	//
	// If all_ is set, do not output any acceptance condition if the
	// source is not in the same SCC as dest.
	//
	// (See the documentation of scc_filter() for a rational.)
	unsigned u = sm_.scc_of_state(out_s);
	if (sm_.accepting(u)
	    && (!all_ || u == sm_.scc_of_state(in_s)))
117
118
119
	  out_->add_acceptance_conditions
	    (t, (bdd_exist(si->current_acceptance_conditions(), strip_)
		 & useful_));
120
121
122
      }

    private:
123
      T* out_;
124
125
      const scc_map& sm_;
      const std::vector<bool>& useless_;
126
127
      bdd useful_;
      bdd strip_;
128
      bool all_;
129
    };
130

131
132
133
  } // anonymous


134
  tgba* scc_filter(const tgba* aut, bool remove_all_useless)
135
136
137
138
139
  {
    scc_map sm(aut);
    sm.build_map();
    scc_stats ss = build_scc_stats(sm);

140
    bdd useful = ss.useful_acc;
141
142
143
144
145
146
147
148
    bdd negall = aut->neg_acceptance_conditions();
    // Compute a set of useless acceptance conditions.
    // If the acceptance combinations occurring in
    // the automata are  { a, ab, abc, bd }, then
    // USEFUL contains (a&!b&!c&!d)|(a&b&!c&!d)|(a&b&c&!d)|(!a&b&!c&d)
    // and we want to find that 'a' and 'b' are useless because
    // they always occur with 'c'.
    // The way we check if 'a' is useless that is to look whether
149
    // USEFUL implies (x -> a) for some other acceptance condition x.
150
151
152
153
    bdd allconds = bdd_support(negall);
    bdd allcondscopy = allconds;
    bdd useless = bddtrue;
    while (allconds != bddtrue)
154
      {
155
156
157
158
	bdd a = bdd_ithvar(bdd_var(allconds));
	bdd others = allcondscopy;

	while (others != bddtrue)
159
	  {
160
161
	    bdd x = bdd_ithvar(bdd_var(others));
	    if (x != a)
162
	      {
163
		if (bdd_implies(useful, x >> a))
164
165
166
167
168
169
170
		  {
		    // a is useless
		    useful = bdd_exist(useful, a);
		    useless &= a;
		    allcondscopy = bdd_exist(allcondscopy, a);
		    break;
		  }
171
	      }
172
	    others = bdd_high(others);
173
	  }
174
	allconds = bdd_high(allconds);
175
176
      }

177
178
179
180
    // We never remove ALL acceptance conditions.
    assert(negall == bddtrue || useless != bdd_support(negall));

    useful = compute_all_acceptance_conditions(bdd_exist(negall, useless));
181
182
183
184
185
186
187
188
189
190
191
192

    // In most cases we will create a tgba_explicit_string copy of the
    // initial tgba, but this is not very space efficient as the
    // labels are built using the "format_state()" string output of
    // the original automaton.  In the case where the source automaton is
    // a tgba_explicit_formula (typically after calling ltl2tgba_fm())
    // we can create another tgba_explicit_formula instead.
    const tgba_explicit_formula* af =
      dynamic_cast<const tgba_explicit_formula*>(aut);
    if (af)
      {
	filter_iter<tgba_explicit_formula> fi(af, sm, ss.useless_scc_map,
193
					      useful, useless,
194
					      remove_all_useless);
195
196
197
198
199
	fi.run();
	tgba_explicit_formula* res = fi.result();
	res->merge_transitions();
	return res;
      }
200
201
202
    const tgba_explicit_string* as =
      dynamic_cast<const tgba_explicit_string*>(aut);
    if (as)
203
204
      {
	filter_iter<tgba_explicit_string> fi(aut, sm, ss.useless_scc_map,
205
					     useful, useless,
206
					     remove_all_useless);
207
208
209
210
211
	fi.run();
	tgba_explicit_string* res = fi.result();
	res->merge_transitions();
	return res;
      }
212
213
214
215
216
217
218
219
220
221
    else
      {
	filter_iter<tgba_explicit_number> fi(aut, sm, ss.useless_scc_map,
					     useful, useless,
					     remove_all_useless);
	fi.run();
	tgba_explicit_number* res = fi.result();
	res->merge_transitions();
	return res;
      }
222
223
224
  }

}