stutter.cc 16 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
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 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 "stutter.hh"
#include "tgba/tgba.hh"
#include "dupexp.hh"
#include "misc/hash.hh"
#include "misc/hashfunc.hh"
#include "ltlvisit/apcollect.hh"
#include "translate.hh"
#include "ltlast/unop.hh"
28
#include "ltlast/binop.hh"
29 30
#include "ltlvisit/remove_x.hh"
#include "tgbaalgos/product.hh"
31
#include "tgbaalgos/ltl2tgba_fm.hh"
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 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 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
#include "tgba/tgbaproduct.hh"
#include "tgba/bddprint.hh"
#include <deque>
#include <unordered_map>
#include <unordered_set>
#include <vector>

namespace spot
{
  namespace
  {
    class state_tgbasl: public state
    {
    public:
      state_tgbasl(state* s, bdd cond) : s_(s), cond_(cond)
      {
      }

      virtual
      ~state_tgbasl()
      {
        s_->destroy();
      }

      virtual int
      compare(const state* other) const
      {
        const state_tgbasl* o =
          down_cast<const state_tgbasl*>(other);
        assert(o);
        int res = s_->compare(o->real_state());
        if (res != 0)
          return res;
        return cond_.id() - o->cond_.id();
      }

      virtual size_t
      hash() const
      {
        return wang32_hash(s_->hash()) ^ wang32_hash(cond_.id());
      }

      virtual
      state_tgbasl* clone() const
      {
        return new state_tgbasl(*this);
      }

      state*
      real_state() const
      {
        return s_;
      }

      bdd
      cond() const
      {
        return cond_;
      }

    private:
      state* s_;
      bdd cond_;
    };

    class tgbasl_succ_iterator : public tgba_succ_iterator
    {
    public:
      tgbasl_succ_iterator(tgba_succ_iterator* it, const state_tgbasl* state,
			   bdd_dict_ptr d, bdd atomic_propositions)
        : it_(it), state_(state), aps_(atomic_propositions), d_(d)
      {
      }

      virtual
      ~tgbasl_succ_iterator()
      {
        delete it_;
      }

      // iteration

      bool
      first()
      {
        loop_ = false;
        done_ = false;
        need_loop_ = true;
        if (it_->first())
          {
            cond_ = it_->current_condition();
            next_edge();
          }
        return true;
      }

      bool
      next()
      {
        if (cond_ != bddfalse)
          {
            next_edge();
            return true;
          }
        if (!it_->next())
          {
            if (loop_ || !need_loop_)
              done_ = true;
            loop_ = true;
            return !done_;
          }
        else
          {
            cond_ = it_->current_condition();
            next_edge();
            return true;
          }
      }

      bool
      done() const
      {
        return it_->done() && done_;
      }

      // inspection

      state_tgbasl*
      current_state() const
      {
        if (loop_)
          return new state_tgbasl(state_->real_state(), state_->cond());
        return new state_tgbasl(it_->current_state(), one_);
      }

      bdd
      current_condition() const
      {
        if (loop_)
          return state_->cond();
        return one_;
      }

      acc_cond::mark_t
      current_acceptance_conditions() const
      {
        if (loop_)
          return 0U;
        return it_->current_acceptance_conditions();
      }

    private:
      void
      next_edge()
      {
        one_ = bdd_satoneset(cond_, aps_, bddtrue);
        cond_ -= one_;
        if (need_loop_ && (state_->cond() == one_)
            && (state_ == it_->current_state()))
          need_loop_ = false;
      }

      tgba_succ_iterator* it_;
      const state_tgbasl* state_;
      bdd cond_;
      bdd one_;
      bdd aps_;
      bdd_dict_ptr d_;
      bool loop_;
      bool need_loop_;
      bool done_;
    };


206
    class tgbasl final : public twa
207 208 209
    {
    public:
      tgbasl(const const_tgba_ptr& a, bdd atomic_propositions)
210
	: twa(a->get_dict()), a_(a), aps_(atomic_propositions)
211 212 213 214
      {
	get_dict()->register_all_propositions_of(&a_, this);
	assert(acc_.num_sets() == 0);
	acc_.add_sets(a_->acc().num_sets());
215
	acc_.set_generalized_buchi();
216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 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 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318
      }

      virtual ~tgbasl()
      {
	get_dict()->unregister_all_my_variables(this);
      }

      virtual state* get_init_state() const override
      {
	return new state_tgbasl(a_->get_init_state(), bddfalse);
      }

      virtual tgba_succ_iterator* succ_iter(const state* state) const override
      {
	const state_tgbasl* s = down_cast<const state_tgbasl*>(state);
	assert(s);
	return new tgbasl_succ_iterator(a_->succ_iter(s->real_state()), s,
					a_->get_dict(), aps_);
      }

      virtual std::string format_state(const state* state) const override
      {
	const state_tgbasl* s = down_cast<const state_tgbasl*>(state);
	assert(s);
	return (a_->format_state(s->real_state())
		+ ", "
		+ bdd_format_formula(a_->get_dict(), s->cond()));
      }

    protected:
      virtual bdd compute_support_conditions(const state*) const override
      {
	return bddtrue;
      }

    private:
      const_tgba_ptr a_;
      bdd aps_;
    };

    typedef std::shared_ptr<tgbasl> tgbasl_ptr;

    inline tgbasl_ptr make_tgbasl(const const_tgba_ptr& aut, bdd ap)
    {
      return std::make_shared<tgbasl>(aut, ap);
    }



    typedef std::pair<unsigned, bdd> stutter_state;

    struct stutter_state_hash
    {
      size_t
      operator()(const stutter_state& s) const
      {
	return wang32_hash(s.first) ^ wang32_hash(s.second.id());
      }
    };

    // Associate the stutter state to its number.
    typedef std::unordered_map<stutter_state, unsigned,
			       stutter_state_hash> ss2num_map;

    // Queue of state to be processed.
    typedef std::deque<stutter_state> queue_t;

    static bdd
    get_all_ap(const const_tgba_digraph_ptr& a)
    {
      bdd res = bddtrue;
      for (auto& i: a->transitions())
	res &= bdd_support(i.cond);
      return res;
    }

  }

  tgba_digraph_ptr
  sl(const const_tgba_digraph_ptr& a, const ltl::formula* f)
  {
    bdd aps = f
      ? atomic_prop_collect_as_bdd(f, a)
      : get_all_ap(a);
    return sl(a, aps);
  }

  tgba_digraph_ptr
  sl2(const const_tgba_digraph_ptr& a, const ltl::formula* f)
  {
    bdd aps = f
      ? atomic_prop_collect_as_bdd(f, a)
      : get_all_ap(a);
    return sl2(a, aps);
  }

  tgba_digraph_ptr
  sl(const const_tgba_digraph_ptr& a, bdd atomic_propositions)
  {
    // The result automaton uses numbered states.
    tgba_digraph_ptr res = make_tgba_digraph(a->get_dict());
    // We use the same BDD variables as the input.
    res->copy_ap_of(a);
319
    res->copy_acceptance_of(a);
320 321 322 323 324 325 326 327 328 329 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 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382
    // These maps make it possible to convert stutter_state to number
    // and vice-versa.
    ss2num_map ss2num;

    queue_t todo;

    unsigned s0 = a->get_init_state_number();
    stutter_state s(s0, bddfalse);
    ss2num[s] = 0;
    res->new_state();
    todo.push_back(s);

    while (!todo.empty())
      {
	s = todo.front();
	todo.pop_front();
	unsigned src = ss2num[s];

	bool self_loop_needed = true;

	for (auto& t : a->out(s.first))
	  {
	    bdd all = t.cond;
	    while (all != bddfalse)
	      {
		bdd one = bdd_satoneset(all, atomic_propositions, bddtrue);
		all -= one;

		stutter_state d(t.dst, one);

		auto r = ss2num.emplace(d, ss2num.size());
		unsigned dest = r.first->second;

		if (r.second)
		  {
		    todo.push_back(d);
		    unsigned u = res->new_state();
		    assert(u == dest);
		    (void)u;
		  }

		// Create the transition.
		res->new_transition(src, dest, one, t.acc);

		if (src == dest)
		  self_loop_needed = false;
	      }
	  }

	if (self_loop_needed && s.second != bddfalse)
	  res->new_transition(src, src, s.second, 0U);
      }
    res->merge_transitions();
    return res;
  }

  tgba_digraph_ptr
  sl2(tgba_digraph_ptr&& a, bdd atomic_propositions)
  {
    if (atomic_propositions == bddfalse)
      atomic_propositions = get_all_ap(a);
    unsigned num_states = a->num_states();
    unsigned num_transitions = a->num_transitions();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
383 384 385 386 387 388 389 390
    std::vector<bdd> selfloops(num_states, bddfalse);
    std::map<std::pair<unsigned, int>, unsigned> newstates;
    // Record all the conditions for which we can selfloop on each
    // state.
    for (auto& t: a->transitions())
      if (t.src == t.dst)
	selfloops[t.src] |= t.cond;
    for (unsigned t = 1; t <= num_transitions; ++t)
391
      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430
	auto& td = a->trans_storage(t);
	if (a->is_dead_transition(td))
	  continue;

	unsigned src = td.src;
	unsigned dst = td.dst;
	if (src != dst)
	  {
	    bdd all = td.cond;
	    // If there is a self-loop with the whole condition on
	    // either end of the transition, do not bother with it.
	    if (bdd_implies(all, selfloops[src])
		|| bdd_implies(all, selfloops[dst]))
	      continue;
	    // Do not use td in the loop because the new_transition()
	    // might invalidate it.
	    auto acc = td.acc;
	    while (all != bddfalse)
	      {
		bdd one = bdd_satoneset(all, atomic_propositions, bddtrue);
		all -= one;
		// Skip if there is a loop for this particular letter.
		if (bdd_implies(one, selfloops[src])
		    || bdd_implies(one, selfloops[dst]))
		  continue;
		auto p = newstates.emplace(std::make_pair(dst, one.id()), 0);
		if (p.second)
		  p.first->second = a->new_state();
		unsigned tmp = p.first->second; // intermediate state
		unsigned i = a->new_transition(src, tmp, one, acc);
		assert(i > num_transitions);
		i = a->new_transition(tmp, tmp, one, 0U);
		assert(i > num_transitions);
		// No acceptance here to preserve the state-based property.
		i = a->new_transition(tmp, dst, one, 0U);
		assert(i > num_transitions);
		(void)i;
	      }
	  }
431 432 433 434 435
      }
    if (num_states != a->num_states())
      a->prop_keep({true,	// state_based
	            false,	// inherently_weak
	            false,	// deterministic
436
	            false,      // stutter inv.
437 438 439 440 441 442 443 444
	           });
    a->merge_transitions();
    return a;
  }

  tgba_digraph_ptr
  sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions)
  {
445
    return sl2(make_tgba_digraph(a, twa::prop_set::all()),
446 447 448 449 450 451 452 453 454 455
	       atomic_propositions);
  }


  tgba_digraph_ptr
  closure(tgba_digraph_ptr&& a)
  {
    a->prop_keep({false,	// state_based
	          false,	// inherently_weak
	          false,	// deterministic
456
	          false,        // stutter inv.
457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491
	         });

    unsigned n = a->num_states();
    std::vector<unsigned> todo;
    std::vector<std::vector<unsigned> > dst2trans(n);

    for (unsigned state = 0; state < n; ++state)
      {
	auto trans = a->out(state);

	for (auto it = trans.begin(); it != trans.end(); ++it)
	  {
	    todo.push_back(it.trans());
	    dst2trans[it->dst].push_back(it.trans());
	  }

	while (!todo.empty())
	  {
	    auto t1 = a->trans_storage(todo.back());
	    todo.pop_back();

	    for (auto& t2 : a->out(t1.dst))
	      {
		bdd cond = t1.cond & t2.cond;
		if (cond != bddfalse)
		  {
                    bool need_new_trans = true;
		    acc_cond::mark_t acc = t1.acc | t2.acc;
                    for (auto& t: dst2trans[t2.dst])
                      {
                        auto& ts = a->trans_storage(t);
                        if (acc == ts.acc)
                          {
                            if (!bdd_implies(cond, ts.cond))
                              {
492
                                ts.cond |= cond;
493 494 495 496 497
                                if (std::find(todo.begin(), todo.end(), t)
                                    == todo.end())
                                  todo.push_back(t);
                              }
                            need_new_trans = false;
498
			    break;
499
                          }
500 501 502 503 504 505 506 507 508 509 510 511 512
			else if (cond == ts.cond)
			  {
			    acc |= ts.acc;
			    if (ts.acc != acc)
			      {
				ts.acc = acc;
				if (std::find(todo.begin(), todo.end(), t)
				    == todo.end())
				  todo.push_back(t);
			      }
                            need_new_trans = false;
			    break;
			  }
513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534
                      }
                    if (need_new_trans)
                      {
			// Load t2.dst first, because t2 can be
			// invalidated by new_transition().
			auto dst = t2.dst;
                        auto i = a->new_transition(state, dst, cond, acc);
                        dst2trans[dst].push_back(i);
                        todo.push_back(i);
                      }
		  }
	      }
	  }
        for (auto& it: dst2trans)
          it.clear();
      }
    return a;
  }

  tgba_digraph_ptr
  closure(const const_tgba_digraph_ptr& a)
  {
535
    return closure(make_tgba_digraph(a, {true, true, true, false}));
536 537 538 539 540 541 542 543 544 545 546
  }

  // The stutter check algorithm to use can be overridden via an
  // environment variable.
  static int default_stutter_check_algorithm()
  {
    static const char* stutter_check = getenv("SPOT_STUTTER_CHECK");
    if (stutter_check)
      {
	char* endptr;
	long res = strtol(stutter_check, &endptr, 10);
547
	if (*endptr || res < 0 || res > 9)
548 549 550 551 552 553 554 555 556 557 558 559 560
	  throw
	    std::runtime_error("invalid value for SPOT_STUTTER_CHECK.");
	return res;
      }
    else
      {
	return 8;     // The best variant, according to our benchmarks.
      }
  }

  bool
  is_stutter_invariant(const ltl::formula* f)
  {
561
    if (f->is_ltl_formula() && f->is_syntactic_stutter_invariant())
562 563 564 565
      return true;

    int algo = default_stutter_check_algorithm();

566 567
    if (algo == 0 || algo == 9)
      // Etessami's check via syntactic transformation.
568 569 570 571 572 573
      {
	if (!f->is_ltl_formula())
	  throw std::runtime_error("Cannot use the syntactic "
				   "stutter-invariance check "
				   "for non-LTL formulas");
	const ltl::formula* g = remove_x(f);
574 575 576 577 578 579 580 581 582 583 584 585 586 587
	bool res;
	if (algo == 0)		// Equivalence check
	  {
	    ltl::ltl_simplifier ls;
	    res = ls.are_equivalent(f, g);
	    g->destroy();
	  }
	else
	  {
	    const ltl::formula* h = ltl::binop::instance(ltl::binop::Xor,
							 f->clone(), g);
	    res = ltl_to_tgba_fm(h, make_bdd_dict())->is_empty();
	    h->destroy();
	  }
588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640
	return res;
      }

    // Prepare for an automata-based check.
    const ltl::formula* nf = ltl::unop::instance(ltl::unop::Not, f->clone());
    translator trans;
    auto aut_f = trans.run(f);
    auto aut_nf = trans.run(nf);
    bdd aps = atomic_prop_collect_as_bdd(f, aut_f);
    nf->destroy();
    return is_stutter_invariant(std::move(aut_f), std::move(aut_nf), aps, algo);
  }

  bool
  is_stutter_invariant(tgba_digraph_ptr&& aut_f,
                       tgba_digraph_ptr&& aut_nf, bdd aps, int algo)
  {
    if (algo == 0)
      algo = default_stutter_check_algorithm();

    switch (algo)
      {
      case 1: // sl(aut_f) x sl(aut_nf)
	return product(sl(std::move(aut_f), aps),
		       sl(std::move(aut_nf), aps))->is_empty();
      case 2: // sl(cl(aut_f)) x aut_nf
	return product(sl(closure(std::move(aut_f)), aps),
		       std::move(aut_nf))->is_empty();
      case 3: // (cl(sl(aut_f)) x aut_nf
	return product(closure(sl(std::move(aut_f), aps)),
		       std::move(aut_nf))->is_empty();
      case 4: // sl2(aut_f) x sl2(aut_nf)
	return product(sl2(std::move(aut_f), aps),
		       sl2(std::move(aut_nf), aps))->is_empty();
      case 5: // sl2(cl(aut_f)) x aut_nf
	return product(sl2(closure(std::move(aut_f)), aps),
		       std::move(aut_nf))->is_empty();
      case 6: // (cl(sl2(aut_f)) x aut_nf
	return product(closure(sl2(std::move(aut_f), aps)),
		       std::move(aut_nf))->is_empty();
      case 7: // on-the-fly sl(aut_f) x sl(aut_nf)
	return otf_product(make_tgbasl(aut_f, aps),
			   make_tgbasl(aut_nf, aps))->is_empty();
      case 8: // cl(aut_f) x cl(aut_nf)
	return product(closure(std::move(aut_f)),
		       closure(std::move(aut_nf)))->is_empty();
      default:
	throw std::runtime_error("invalid algorithm number for "
				 "is_stutter_invariant()");
	SPOT_UNREACHABLE();
      }
  }
}