dra2ba.cc 11.6 KB
Newer Older
1 2 3 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 51 52 53 54 55 56
// Copyright (C) 2013 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// 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"
#include "ltlast/constant.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
  tgba* nra_to_nba(const dstar_aut* nra, const tgba* aut);

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

57 58 59 60 61 62 63 64
    // 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.

65 66 67 68 69 70 71 72 73 74 75 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 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
    static bool
    filter_states(const tgba* aut,
		  const dstar_aut* dra,
		  const state_list& sl,
		  state_list& final,
		  state_list& nonfinal);

    static bool
    filter_scc(const tgba* aut,
	       const dstar_aut* dra,
	       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
    filter_states(const tgba* aut,
		  const dstar_aut* dra,
		  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();
      int num = dra->aut->get_label(*it++);
      bitvect* l = dra->accsets->at(num * 2).clone();
      bitvect* u = dra->accsets->at(num * 2 + 1).clone();
      for (; it != sl.end(); ++it)
	{
	  num = dra->aut->get_label(*it);
	  *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());
	    const tgba* masked =
	      build_tgba_mask_keep(dra->aut, keep, sl.front());
	    const tgba* nba = nra_to_nba(dra, masked);
	    emptiness_check* ec = couvreur99(nba);
	    emptiness_check_result* ecr = ec->check();
	    delete ecr;
	    delete ec;
	    delete nba;
	    delete masked;
	    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)
	{
	  num = dra->aut->get_label(*it);
	  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.
	  const tgba* scc_mask =
	    build_tgba_mask_keep(aut, unknown, *unknown.begin());
	  state_list local_final;
	  state_list local_nonfinal;
	  bool dbarealizable =
	    filter_scc(scc_mask, dra, local_final, local_nonfinal);
	  delete scc_mask;
	  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;
    }



223
    class dra_to_ba_worker: public tgba_reachable_iterator_depth_first
224 225
    {
    public:
226 227 228 229 230
      dra_to_ba_worker(const dstar_aut* a,
		       const state_set& final,
		       const scc_map& sm,
		       const std::vector<bool>& realizable):
	tgba_reachable_iterator_depth_first(a->aut),
231
	in_(a),
232 233 234 235 236
	out_(new tgba_explicit_number(a->aut->get_dict())),
	final_(final),
	num_states_(a->aut->num_states()),
	sm_(sm),
	realizable_(realizable)
237
      {
238 239
	bdd_dict* bd = a->aut->get_dict();
	bd->register_all_variables_of(a->aut, out_);
240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259

	// Invent a new acceptance set for the degeneralized automaton.
	int accvar =
	  bd->register_acceptance_variable(ltl::constant::true_instance(),
					   out_);
	acc_ = bdd_ithvar(accvar);
	out_->set_acceptance_conditions(acc_);
      }

      tgba_explicit_number*
      result()
      {
	return out_;
      }

      void
      process_link(const state* sin, int,
		   const state* sout, int,
		   const tgba_succ_iterator* si)
      {
260 261 262
	int in = in_->aut->get_label(sin);
	int out = in_->aut->get_label(sout);
	unsigned in_scc = sm_.scc_of_state(sin);
263 264 265 266 267

	typedef state_explicit_number::transition trans;
	trans* t = out_->create_transition(in, out);
	bdd cond = t->condition = si->current_condition();

268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308
	if (realizable_[in_scc])
	  {
	    if (final_.find(sin) != final_.end())
	      t->acceptance_conditions = acc_;
	  }
	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.
		    trans* t1 = out_->create_transition(in, out + shift);
		    t1->condition = cond;

		    trans* t2 = out_->create_transition(in + shift,
							out + shift);
		    t2->condition = cond;
		    // In the Li set. (Löding's Fi set.)
		    if (l.get(i))
		      t2->acceptance_conditions = acc_;
		  }
	      }
	  }
309 310 311
      }

    protected:
312
      const dstar_aut* in_;
313 314
      tgba_explicit_number* out_;
      const state_set& final_;
315
      size_t num_states_;
316
      bdd acc_;
317 318
      const scc_map& sm_;
      const std::vector<bool>& realizable_;
319 320 321 322 323
    };

  }


324
  tgba* dra_to_ba(const dstar_aut* dra, bool* dba)
325 326 327 328 329
  {
    assert(dra->type == Rabin);

    state_list final;
    state_list nonfinal;
330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357

    // 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;
	//std::cerr << "realizable[" << scc << "] = " << scc_realizable << "\n";
      }

    if (dba)
      *dba = dba_realizable;
358 359 360 361 362 363 364 365 366

    // 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());
367
    dra_to_ba_worker w(dra, fs, sm, realizable);
368 369 370 371 372 373 374 375
    w.run();
    tgba_explicit_number* res1 = w.result();
    tgba* res2 = scc_filter_states(res1);
    delete res1;
    return res2;
  }

}