compsusp.cc 10.9 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2012, 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
//
// 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 "compsusp.hh"
#include "sccfilter.hh"
22
#include "sccinfo.hh"
23
#include "tgba/tgbagraph.hh"
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
#include "ltl2tgba_fm.hh"
#include "minimize.hh"
#include "simulation.hh"
#include "safety.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/clone.hh"
#include <queue>
#include <sstream>
#include "ltlenv/environment.hh"

namespace spot
{
  namespace
  {
    typedef std::map<const ltl::formula*, bdd> formula_bdd_map;

    // An environment to store atomic proposition associated to
    // suspended variable.  (We don't use the default environment to
    // avoid conflicts with user-defined atomic propositions that
    // would share the same name.)
    class suspended_environment: public ltl::environment
    {
    public:
      const ltl::formula*
      require(const std::string& s)
      {
	return ltl::atomic_prop::instance(s, *this);
      }

      const std::string&
55
      name() const
56 57 58 59 60 61 62 63 64 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
      {
	static std::string name("suspended environment");
	return name;
      }
    };
    static suspended_environment suspenv;

    // Rewrite the suspendable subformulae "s" of an LTL formula in
    // the form Gg where "g" is an atomic proposition representing
    // "s".  At the same time, populate maps that associate "s" to "g"
    // and vice-versa.
    class ltl_suspender_visitor: public ltl::clone_visitor
    {
    public:
      typedef std::map<const ltl::formula*, const ltl::formula*> fmap_t;
      ltl_suspender_visitor(fmap_t& g2s, fmap_t& a2o, bool oblig)
	: g2s_(g2s), a2o_(a2o), oblig_(oblig)
      {
      }

      void
      visit(const ltl::multop* mo)
      {
	ltl::multop::type op = mo->op();
	switch (op)
	  {
	  case ltl::multop::Or:
	  case ltl::multop::And:
	    {
	      ltl::multop::vec* res = new ltl::multop::vec;
	      ltl::multop::vec* oblig = oblig_ ? new ltl::multop::vec : 0;
	      ltl::multop::vec* susp = new ltl::multop::vec;
	      unsigned mos = mo->size();
	      for (unsigned i = 0; i < mos; ++i)
		{
		  const ltl::formula* c = mo->nth(i);
		  if (c->is_boolean())
		    res->push_back(c->clone());
		  else if (oblig_ && c->is_syntactic_obligation())
		    oblig->push_back(c->clone());
		  else if (c->is_eventual() && c->is_universal())
		    susp->push_back(c->clone());
		  else
		    res->push_back(recurse(c));
		}
	      if (!oblig_ || oblig->empty())
		{
		  delete oblig;
		}
	      else
		{
		  const ltl::formula* o = ltl::multop::instance(op, oblig);
		  res->push_back(recurse(o));
		  o->destroy();
		}
	      if (susp->empty())
		{
		  delete susp;
		}
	      else
		{
		  const ltl::formula* o = ltl::multop::instance(op, susp);
		  // Rewrite 'o' as 'G"o"'
		  const ltl::formula* g = recurse(o);
		  o->destroy();
		  if (op == ltl::multop::And)
		    {
		      res->push_back(g);
		    }
		  else
		    {
		      // res || susp -> (res && G![susp]) || G[susp])
		      const ltl::formula* r = ltl::multop::instance(op, res);
		      const ltl::unop* u =
			down_cast<const ltl::unop*>(g);
		      const ltl::formula* gn =
			ltl::unop::instance
			(ltl::unop::G, ltl::unop::instance
			 (ltl::unop::Not, u->child()->clone()));
		      result_ = ltl::multop::instance
			(ltl::multop::Or, ltl::multop::instance
			 (ltl::multop::And, r, gn),
			 g);
		      return;
		    }
		}
	      result_ = ltl::multop::instance(op, res);
	    }
	    break;
	  case ltl::multop::OrRat:
	  case ltl::multop::AndRat:
	  case ltl::multop::AndNLM:
	  case ltl::multop::Concat:
	  case ltl::multop::Fusion:
	    this->ltl::clone_visitor::visit(mo);
	    break;
	  }
      }


      const ltl::formula*
      recurse(const ltl::formula* f)
      {
	const ltl::formula* res;
	if (f->is_boolean())
	  return f->clone();
	if (oblig_ && f->is_syntactic_obligation())
	  {
	    fmap_t::const_iterator i = assoc_.find(f);
	    if (i != assoc_.end())
	      return i->second->clone();

	    std::ostringstream s;
	    s << "〈";
	    to_string(f, s);
	    s << "〉";
	    res = suspenv.require(s.str());
	    // We have to clone f, because it is not always a sub-tree
	    // of the original formula.  (Think n-ary operators.)
	    a2o_[res] = f->clone();
	    assoc_[f] = res;
	    return res;
	  }
	if (f->is_eventual() && f->is_universal())
	  {
	    fmap_t::const_iterator i = assoc_.find(f);
	    if (i != assoc_.end())
	      return ltl::unop::instance(ltl::unop::G, i->second->clone());

	    std::ostringstream s;
186
	    s << '[';
187
	    to_string(f, s);
188
	    s << ']';
189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
	    res = suspenv.require(s.str());
	    // We have to clone f, because it is not always a sub-tree
	    // of the original formula.  (Think n-ary operators.)
	    g2s_[res] = f->clone();
	    assoc_[f] = res;
	    return ltl::unop::instance(ltl::unop::G, res);
	  }
	f->accept(*this);
	return result_;
      }

    private:
      fmap_t& g2s_;
      fmap_t assoc_;		// This one is only needed by the visitor.
      fmap_t& a2o_;
      bool oblig_;
    };


    typedef std::pair<const state*, const state*> state_pair;

210
    typedef std::map<state_pair, unsigned> pair_map;
211 212 213
    typedef std::deque<state_pair> pair_queue;

    static
214
    twa_graph_ptr
215
    susp_prod(const const_twa_ptr& left, const ltl::formula* f, bdd v)
216
    {
217
      bdd_dict_ptr dict = left->get_dict();
218 219 220
      auto right =
	iterated_simulations(scc_filter(ltl_to_tgba_fm(f, dict, true, true),
					false));
221

222
      twa_graph_ptr res = make_twa_graph(dict);
223 224 225 226
      dict->register_all_variables_of(left, res);
      dict->register_all_variables_of(right, res);
      dict->unregister_variable(bdd_var(v), res);

227 228
      const acc_cond& la = left->acc();
      const acc_cond& ra = right->acc();
229
      res->set_generalized_buchi(la.num_sets() + ra.num_sets());
230

231
      acc_cond::mark_t radd = ra.all_sets();
232 233 234 235 236 237 238

      pair_map seen;
      pair_queue todo;

      state_pair p(left->get_init_state(), 0);
      state* ris = right->get_init_state();
      p.second = ris;
239 240
      unsigned i = res->new_state();
      seen[p] = i;
241
      todo.push_back(p);
242
      res->set_init_state(i);
243 244 245 246 247 248 249 250 251

      while (!todo.empty())
	{
	  p = todo.front();
	  todo.pop_front();
	  const state* ls = p.first;
	  const state* rs = p.second;
	  int src = seen[p];

252
	  for (auto li: left->succ(ls))
253 254 255 256
	    {
	      state_pair d(li->current_state(), ris);
	      bdd lc = li->current_condition();

257
	      twa_succ_iterator* ri = 0;
258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277
	      // Should we reset the right automaton?
	      if ((lc & v) == lc)
		{
		  // No.
		  ri = right->succ_iter(rs);
		  ri->first();
		}
	      // Yes.  Reset the right automaton.
	      else
		{
		  p.second = ris;
		}

	      // This loops over all the right transitions
	      // if RI is defined.  Otherwise this just makes
	      // one iteration as if the right automaton was
	      // looping in state 0 with "true".
	      while (!ri || !ri->done())
		{
		  bdd cond = lc;
278
		  acc_cond::mark_t racc = radd;
279 280 281 282 283 284 285 286 287 288
		  if (ri)
		    {
		      cond = lc & ri->current_condition();
		      // Skip incompatible transitions.
		      if (cond == bddfalse)
			{
			  ri->next();
			  continue;
			}
		      d.second = ri->current_state();
289
		      racc = ri->current_acceptance_conditions();
290 291
		    }

292
		  int dest;
293
		  pair_map::const_iterator i = seen.find(d);
294
		  if (i != seen.end()) // Is this an existing state?
295 296 297 298 299
		    {
		      dest = i->second;
		    }
		  else
		    {
300
		      dest = res->new_state();
301 302 303 304
		      seen[d] = dest;
		      todo.push_back(d);
		    }

305 306 307 308
		  acc_cond::mark_t a =
		    res->acc().join(la, li->current_acceptance_conditions(),
				    ra, racc);
		  res->new_transition(src, dest, bdd_exist(cond, v), a);
309 310 311 312 313 314

		  if (ri)
		    ri->next();
		  else
		    break;
		}
315 316
	      if (ri)
		right->release_iter(ri);
317 318 319 320 321 322
	    }
	}
      return res;
    }
  }

323

324
  twa_graph_ptr
325
  compsusp(const ltl::formula* f, const bdd_dict_ptr& dict,
326 327 328 329 330 331 332 333 334
	   bool no_wdba, bool no_simulation,
	   bool early_susp, bool no_susp_product, bool wdba_smaller,
	   bool oblig)
  {
    ltl_suspender_visitor::fmap_t g2s;
    ltl_suspender_visitor::fmap_t a2o;
    ltl_suspender_visitor v(g2s, a2o, oblig);
    const ltl::formula* g = v.recurse(f);

335
    // Translate the patched formula, and remove useless SCCs.
336
    twa_graph_ptr res =
337 338
      scc_filter(ltl_to_tgba_fm(g, dict, true, true, false, false, 0, 0),
		 false);
339 340 341

    if (!no_wdba)
      {
342
	twa_graph_ptr min = minimize_obligation(res, g, 0, wdba_smaller);
343 344
	if (min != res)
	  {
345
	    res = min;
346 347 348 349 350
	    no_simulation = true;
	  }
      }

    if (!no_simulation)
351
      res = iterated_simulations(res);
352

353
    // Create a map of suspended formulae to BDD variables.
354
    spot::formula_bdd_map susp;
355
    for (auto& it: g2s)
356
      {
357 358 359 360 361 362 363 364 365
	auto j = dict->var_map.find(it.first);
	// If no BDD variable of this suspended formula exist in the
	// BDD dict, it means the suspended subformulae was never
	// actually used in the automaton.  Just skip it.  FIXME: It
	// would be better if we had a way to check that the variable
	// is used in this automaton, and not in some automaton
	// (sharing the same dictionary.)
	if (j != dict->var_map.end())
	  susp[it.second] = bdd_ithvar(j->second);
366 367 368 369 370 371 372 373 374 375
      }

    // Remove suspendable formulae from non-accepting SCCs.
    bdd suspvars = bddtrue;
    for (formula_bdd_map::const_iterator i = susp.begin();
	 i != susp.end(); ++i)
      suspvars &= i->second;

    bdd allaccap = bddtrue; // set of atomic prop used in accepting SCCs.
    {
376
      scc_info si(res);
377 378 379

      // Restrict suspvars to the set of suspension labels that occur
      // in accepting SCC.
380
      unsigned sn = si.scc_count();
381
      for (unsigned n = 0; n < sn; n++)
382 383
	if (si.is_accepting_scc(n))
	  allaccap &= si.scc_ap_support(n);
384 385 386

      bdd ignored = bdd_exist(suspvars, allaccap);
      suspvars = bdd_existcomp(suspvars, allaccap);
387
      res = scc_filter_susp(res, false, suspvars, ignored, early_susp, &si);
388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407
    }

    // Do we need to synchronize any suspended formula?
    if (!susp.empty() && !no_susp_product)
      for (formula_bdd_map::const_iterator i = susp.begin();
	   i != susp.end(); ++i)
	if ((allaccap & i->second) == allaccap)
	  res = susp_prod(res, i->first, i->second);

    g->destroy();

    for (ltl_suspender_visitor::fmap_t::iterator i = g2s.begin();
	 i != g2s.end(); ++i)
      i->second->destroy();
    for (ltl_suspender_visitor::fmap_t::iterator i = a2o.begin();
	 i != a2o.end(); ++i)
      i->second->destroy();
    return res;
  }
}