sccfilter.cc 6.55 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
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
//
// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

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

namespace spot
{
  namespace
  {
32
33
34
35
36
37
38
39
    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);
    }

40
    static
Pierre PARUTTO's avatar
Pierre PARUTTO committed
41
    state_explicit_string::transition*
42
    create_transition(const tgba* aut, tgba_explicit_string* out_aut,
43
		      const state* in_s, int, const state* out_s, int)
44
    {
45
46
47
48
      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));
49
50
51
    }

    static
Pierre PARUTTO's avatar
Pierre PARUTTO committed
52
    state_explicit_formula::transition*
53
54
55
56
57
58
59
60
61
    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();
62
      if ((in_f != out_f) && !out_aut->has_state(out_f))
63
64
65
66
67
	out_f->clone();
      return out_aut->create_transition(in_f, out_f);
    }

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

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

88
      T*
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
      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
105
	typename output_t::state::transition* t =
106
	  create_transition(this->aut_, out_, in_s, in, out_s, out);
107
108
	out_->add_conditions(t, si->current_condition());

109
110
111
112
113
114
115
116
117
118
	// 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)))
119
120
121
	  out_->add_acceptance_conditions
	    (t, (bdd_exist(si->current_acceptance_conditions(), strip_)
		 & useful_));
122
123
124
      }

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

133
134
135
  } // anonymous


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

142
    bdd useful = ss.useful_acc;
143
144
145
146
147
148
149
150
    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
151
    // USEFUL implies (x -> a) for some other acceptance condition x.
152
153
154
155
    bdd allconds = bdd_support(negall);
    bdd allcondscopy = allconds;
    bdd useless = bddtrue;
    while (allconds != bddtrue)
156
      {
157
158
159
160
	bdd a = bdd_ithvar(bdd_var(allconds));
	bdd others = allcondscopy;

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

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

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

    // 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,
195
					      useful, useless,
196
					      remove_all_useless);
197
198
199
200
201
	fi.run();
	tgba_explicit_formula* res = fi.result();
	res->merge_transitions();
	return res;
      }
202
203
204
    const tgba_explicit_string* as =
      dynamic_cast<const tgba_explicit_string*>(aut);
    if (as)
205
206
      {
	filter_iter<tgba_explicit_string> fi(aut, sm, ss.useless_scc_map,
207
					     useful, useless,
208
					     remove_all_useless);
209
210
211
212
213
	fi.run();
	tgba_explicit_string* res = fi.result();
	res->merge_transitions();
	return res;
      }
214
215
216
217
218
219
220
221
222
223
    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;
      }
224
225
226
  }

}