dra2ba.cc 11.3 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
//
// 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.

#include "public.hh"
#include "tgba/tgbamask.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/reachiter.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/sccfilter.hh"

namespace spot
{

  // IMPORTANT NOTE: If you attempt to follow Krishnan et
  // al. (ISAAC'94) paper while reading this code, make sure you
  // understand the difference between their Rabin acceptance
  // definition and the one we are using.
  //
  // Here, a cycle is accepting in a Rabin automaton if there exists
  // an acceptance pair (Lᵢ, Uᵢ) such that some states from Lᵢ are
  // visited while no states from Uᵢ are visited.   This is the
  // same definition used by ltl2dstar.
  //
  // In the Krishnan et al. paper, a cycle is accepting in a Rabin
  // automaton if there exists an acceptance pair (Lᵢ, Uᵢ) such that
  // some states from Lᵢ are visited and all visited states belongs to
  // Uᵢ.  In other words, you can switch from one definition to
  // the other by complementing the Uᵢ set.
  //
  // This is a source of confusion; you have been warned.


  // This function is defined in nra2nba.cc, and used only here.
  SPOT_LOCAL
51
52
  tgba_digraph_ptr nra_to_nba(const const_dstar_aut_ptr& nra,
			      const const_tgba_ptr& aut);
53
54
55
56
57

  namespace
  {
    typedef std::list<const state*> state_list;

58
59
60
61
62
63
64
65
    // The function that takes aut and dra is first arguments are
    // either called on the main automaton, in which case dra->aut ==
    // aut, or it is called on a sub-automaton in which case aut is a
    // masked version of dra->aut.  So we should always explore the
    // automaton aut, but because the state of aut are states of
    // dra->aut, we can use dra->aut to get labels, and dra->acccs to
    // retrive acceptances.

66
    static bool
67
68
    filter_states(const const_tgba_ptr& aut,
		  const const_dstar_aut_ptr& dra,
69
70
71
72
73
		  const state_list& sl,
		  state_list& final,
		  state_list& nonfinal);

    static bool
74
75
    filter_scc(const const_tgba_ptr& aut,
	       const const_dstar_aut_ptr& dra,
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
	       state_list& final,
	       state_list& nonfinal)
    {
      // Iterate over all non-trivial SCCs.
      scc_map sm(aut);
      sm.build_map();
      for (unsigned scc_max = sm.scc_count(), scc = 0;
	   scc < scc_max; ++scc)
	{
	  if (sm.trivial(scc))
	    {
	      nonfinal.push_back(sm.one_state_of(scc));
	      continue;
	    }

	  // Get the list of states of that SCC
	  const std::list<const state*>& sl = sm.states_of(scc);
	  assert(!sl.empty());
	  if (!filter_states(aut, dra, sl, final, nonfinal))
	    return false;
      }
      return true;
    }

    static bool
101
102
    filter_states(const const_tgba_ptr& aut,
		  const const_dstar_aut_ptr& dra,
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
		  const state_list& sl,
		  state_list& final,
		  state_list& nonfinal)
    {
      // Check whether the SCC composed of all states in sl contains
      // non-accepting cycles.
      //
      // A cycle is accepting (in a Rabin automaton) if there exists
      // an acceptance pair (Lᵢ, Uᵢ) such that some states from Lᵢ
      // are visited while no states from Uᵢ are visited.
      //
      // Consequently, a cycle is non-accepting if for all acceptance
      // pairs (Lᵢ, Uᵢ), either no states from Lᵢ are visited or some
      // states from Uᵢ are visited.  (This corresponds to an
      // accepting cycle with Streett acceptance.)
      //
      // Now we consider the SCC as one large cycle and check its
      // intersection with all Lᵢs and Uᵢs.  Let l=[l₁,l₂,...] and
      // u=[u₁,u₂,...] be bitvectors where bit lᵢ (resp. uᵢ)
      // indicates that Lᵢ (resp. Uᵢ) has been visited in the SCC.
      state_list::const_iterator it = sl.begin();
124
      int num = dra->aut->state_number(*it++);
125
126
127
128
      bitvect* l = dra->accsets->at(num * 2).clone();
      bitvect* u = dra->accsets->at(num * 2 + 1).clone();
      for (; it != sl.end(); ++it)
	{
129
	  num = dra->aut->state_number(*it);
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
	  *l |= dra->accsets->at(num * 2);
	  *u |= dra->accsets->at(num * 2 + 1);
	}
      // If we have l&!u = [0,0,...] that means that the cycle formed
      // by the entire SCC is not accepting.  However that does not
      // necessarily imply that all cycles in the SCC are also
      // non-accepting.  We may have a smaller cycle that is
      // accepting, but which becomes non-accepting when extended with
      // more states.
      *l -= *u;
      delete u;
      if (l->is_fully_clear())
	{
	  delete l;
	  // Check whether the SCC is accepting.  We do that by simply
	  // converting that SCC into a TGBA and running our emptiness
	  // check.  This is not a really smart implementation and
	  // could be improved.
	  {
	    state_set keep(sl.begin(), sl.end());
150
151
	    auto masked = build_tgba_mask_keep(dra->aut, keep, sl.front());
	    emptiness_check* ec = couvreur99(nra_to_nba(dra, masked));
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
	    emptiness_check_result* ecr = ec->check();
	    delete ecr;
	    delete ec;
	    if (ecr)
	      {
		// This SCC is not DBA-realizable.
		//std::cerr << "not DBA-realizable\n";
		return false;
	      }
	  }
	  //std::cerr << "non-accepting\n";
	  for (state_list::const_iterator i = sl.begin();
	       i != sl.end(); ++i)
	    nonfinal.push_back(*i);
	  return true;
	}
      // The bits sets in *l corresponds to Lᵢs that have been seen
      // without seeing the matching Uᵢ.  In this SCC, any state in Lᵢ
      // is therefore final.  Otherwise we do not know: it is possible
      // that there is a non-accepting cycle in the SCC that do not
      // visit Lᵢ.
      state_set unknown;
      for (it = sl.begin(); it != sl.end(); ++it)
	{
176
	  num = dra->aut->state_number(*it);
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
	  bitvect* l2 = dra->accsets->at(num * 2).clone();
	  *l2 &= *l;
	  if (!l2->is_fully_clear())
	    {
	      final.push_back(*it);
	    }
	  else
	    {
	      unknown.insert(*it);
	    }
	  delete l2;
	}
      delete l;
      // Check whether it is possible to build non-accepting cycles
      // using only the "unknown" states.
      while (!unknown.empty())
	{
	  //std::cerr << "unknown\n";
	  // Build a sub-automaton for just the unknown states,
	  // starting from any state in the SCC.
197
	  auto scc_mask = build_tgba_mask_keep(aut, unknown, *unknown.begin());
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
	  state_list local_final;
	  state_list local_nonfinal;
	  bool dbarealizable =
	    filter_scc(scc_mask, dra, local_final, local_nonfinal);
	  if (!dbarealizable)
	    return false;
	  for (state_list::const_iterator i = local_final.begin();
	       i != local_final.end(); ++i)
	    unknown.erase(*i);
	  final.splice(final.end(), local_final);
	  for (state_list::const_iterator i = local_nonfinal.begin();
	       i != local_nonfinal.end(); ++i)
	    unknown.erase(*i);
	  nonfinal.splice(nonfinal.end(), local_nonfinal);
	}
      return true;
    }



218
    class dra_to_ba_worker: public tgba_reachable_iterator_depth_first
219
220
    {
    public:
221
      dra_to_ba_worker(const const_dstar_aut_ptr& a,
222
223
224
225
		       const state_set& final,
		       const scc_map& sm,
		       const std::vector<bool>& realizable):
	tgba_reachable_iterator_depth_first(a->aut),
226
	in_(a),
227
	out_(make_tgba_digraph(a->aut->get_dict())),
228
229
230
231
	final_(final),
	num_states_(a->aut->num_states()),
	sm_(sm),
	realizable_(realizable)
232
      {
233
	out_->copy_ap_of(a->aut);
234
	out_->set_bprop(tgba_digraph::StateBasedAcc);
235
	acc_ = out_->set_single_acceptance_set();
236
237
	out_->new_states(num_states_ * (a->accpair_count + 1));
	out_->set_init_state(a->aut->get_init_state_number());
238
239
      }

240
      tgba_digraph_ptr
241
242
243
244
245
246
247
248
249
250
      result()
      {
	return out_;
      }

      void
      process_link(const state* sin, int,
		   const state* sout, int,
		   const tgba_succ_iterator* si)
      {
251
252
	int in = in_->aut->state_number(sin);
	int out = in_->aut->state_number(sout);
253
	unsigned in_scc = sm_.scc_of_state(sin);
254

255
256
	bdd cond = si->current_condition();
	unsigned t = out_->new_transition(in, out, cond);
257

258
259
260
	if (realizable_[in_scc])
	  {
	    if (final_.find(sin) != final_.end())
261
	      out_->trans_data(t).acc = acc_;
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
	  }
	else if (sm_.scc_of_state(sout) == in_scc)
	  {
	    // Create one clone of the SCC per accepting pair,
	    // removing states from the Ui part of the (Li, Ui) pairs.
	    // (Or the Ei part of Löding's (Ei, Fi) pairs.)
	    bitvect& l = in_->accsets->at(2 * in);
	    bitvect& u = in_->accsets->at(2 * in + 1);
	    for (size_t i = 0; i < in_->accpair_count; ++i)
	      {
		int shift = num_states_ * (i + 1);
		// In the Ui set. (Löding's Ei set.)
		if (!u.get(i))
		  {
		    // Transition t1 is a non-deterministic jump
		    // from the original automaton to the i-th clone.
		    //
		    // Transition t2 constructs the clone.
		    //
		    // Löding creates transition t1 regardless of the
		    // acceptance set.  We restrict it to the non-Li
		    // states.  Both his definition and this
		    // implementation create more transitions than needed:
		    // we do not need more than one transition per
		    // accepting cycle.
287
288
		    out_->new_transition(in, out + shift, cond);

289
290
		    // Acceptance transitions are those in the Li
		    // set. (Löding's Fi set.)
291
292
		    out_->new_acc_transition(in + shift, out + shift, cond,
					     l.get(i));
293
294
295
		  }
	      }
	  }
296
297
298
      }

    protected:
299
300
      const const_dstar_aut_ptr& in_;
      tgba_digraph_ptr out_;
301
      const state_set& final_;
302
      size_t num_states_;
303
      bdd acc_;
304
305
      const scc_map& sm_;
      const std::vector<bool>& realizable_;
306
307
308
309
310
    };

  }


311
  tgba_digraph_ptr dra_to_ba(const const_dstar_aut_ptr& dra, bool* dba)
312
313
314
315
316
  {
    assert(dra->type == Rabin);

    state_list final;
    state_list nonfinal;
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339

    // Iterate over all non-trivial SCCs.
    scc_map sm(dra->aut);
    sm.build_map();
    unsigned scc_max = sm.scc_count();

    bool dba_realizable = true;
    std::vector<bool> realizable(scc_max);

    for (unsigned scc = 0; scc < scc_max; ++scc)
      {
	if (sm.trivial(scc))
	  {
	    realizable[scc] = true;
	    continue;
	  }

	// Get the list of states of that SCC
	const std::list<const state*>& sl = sm.states_of(scc);
	assert(!sl.empty());
	bool scc_realizable = filter_states(dra->aut, dra, sl, final, nonfinal);
	dba_realizable &= scc_realizable;
	realizable[scc] = scc_realizable;
340
	//std::cerr << "realizable[" << scc << "] = " << scc_realizable << '\n';
341
342
343
344
      }

    if (dba)
      *dba = dba_realizable;
345
346
347
348
349
350
351
352
353

    // for (state_list::const_iterator i = final.begin();
    // 	 i != final.end(); ++i)
    //   std::cerr << dra->aut->get_label(*i) << " is final\n";
    // for (state_list::const_iterator i = nonfinal.begin();
    // 	 i != nonfinal.end(); ++i)
    //   std::cerr << dra->aut->get_label(*i) << " is non-final\n";

    state_set fs(final.begin(), final.end());
354
    dra_to_ba_worker w(dra, fs, sm, realizable);
355
    w.run();
356
    return scc_filter_states(w.result());
357
358
359
  }

}