sccfilter.cc 6.06 KB
Newer Older
1
2
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et
// 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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
    static
    tgba_explicit::transition*
    create_transition(const tgba* aut, tgba_explicit_string* out_aut,
		      const state* in_s, int in,
		      const state* out_s, int out)
    {
      std::ostringstream in_name;
      in_name << "(#" << in << ") " << aut->format_state(in_s);
      std::ostringstream out_name;
      out_name << "(#" << out << ") " << aut->format_state(out_s);
      return out_aut->create_transition(in_name.str(), out_name.str());
    }

    static
    tgba_explicit::transition*
    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();
56
      if ((in_f != out_f) && !out_aut->has_state(out_f))
57
58
59
60
61
	out_f->clone();
      return out_aut->create_transition(in_f, out_f);
    }

    template<class T>
62
63
64
65
66
    class filter_iter: public tgba_reachable_iterator_depth_first
    {
    public:
      filter_iter(const tgba* a,
		  const scc_map& sm,
67
		  const std::vector<bool>& useless,
68
		  bdd useful, bdd strip, bool remove_all_useless)
69
	: tgba_reachable_iterator_depth_first(a),
70
	  out_(new T(a->get_dict())),
71
	  sm_(sm),
72
73
	  useless_(useless),
	  useful_(useful),
74
75
	  strip_(strip),
	  all_(remove_all_useless)
76
      {
77
	out_->set_acceptance_conditions(useful);
78
79
      }

80
      T*
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
      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)
      {
	tgba_explicit::transition* t =
98
	  create_transition(this->aut_, out_, in_s, in, out_s, out);
99
100
	out_->add_conditions(t, si->current_condition());

101
102
103
104
105
106
107
108
109
110
	// 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)))
111
112
113
	  out_->add_acceptance_conditions
	    (t, (bdd_exist(si->current_acceptance_conditions(), strip_)
		 & useful_));
114
115
116
      }

    private:
117
      T* out_;
118
119
      const scc_map& sm_;
      const std::vector<bool>& useless_;
120
121
      bdd useful_;
      bdd strip_;
122
      bool all_;
123
    };
124

125
126
127
  } // anonymous


128
  tgba* scc_filter(const tgba* aut, bool remove_all_useless)
129
130
131
132
133
  {
    scc_map sm(aut);
    sm.build_map();
    scc_stats ss = build_scc_stats(sm);

134
    bdd useful = ss.useful_acc;
135
136
137
138
139
140
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
    // USEFUL & (x -> a) == USEFUL for some other acceptance
    // condition x.
    bdd allconds = bdd_support(negall);
    bdd allcondscopy = allconds;
    bdd useless = bddtrue;
    while (allconds != bddtrue)
149
      {
150
151
152
153
	bdd a = bdd_ithvar(bdd_var(allconds));
	bdd others = allcondscopy;

	while (others != bddtrue)
154
	  {
155
156
	    bdd x = bdd_ithvar(bdd_var(others));
	    if (x != a)
157
	      {
158
159
160
161
162
163
164
165
		if ((useful & (x >> a)) == useful)
		  {
		    // a is useless
		    useful = bdd_exist(useful, a);
		    useless &= a;
		    allcondscopy = bdd_exist(allcondscopy, a);
		    break;
		  }
166
	      }
167
	    others = bdd_high(others);
168
	  }
169
	allconds = bdd_high(allconds);
170
171
      }

172
173
174
175
    // We never remove ALL acceptance conditions.
    assert(negall == bddtrue || useless != bdd_support(negall));

    useful = compute_all_acceptance_conditions(bdd_exist(negall, useless));
176
177
178
179
180
181
182
183
184
185
186
187

    // 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,
188
					      useful, useless,
189
					      remove_all_useless);
190
191
192
193
194
195
196
197
	fi.run();
	tgba_explicit_formula* res = fi.result();
	res->merge_transitions();
	return res;
      }
    else
      {
	filter_iter<tgba_explicit_string> fi(aut, sm, ss.useless_scc_map,
198
					     useful, useless,
199
					     remove_all_useless);
200
201
202
203
204
	fi.run();
	tgba_explicit_string* res = fi.result();
	res->merge_transitions();
	return res;
      }
205
206
207
  }

}