gv04.cc 9.85 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2008, 2010, 2011, 2013, 2014, 2015 Laboratoire de
// recherche et développement de l'Epita (LRDE).
4
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6
5
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
6
// Pierre et Marie Curie.
7 8 9 10 11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
13 14 15 16 17 18 19 20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
22 23 24 25 26 27 28 29 30 31 32 33

//#define TRACE

#include <iostream>
#ifdef TRACE
#define trace std::cerr
#else
#define trace while (0) std::cerr
#endif

#include <cassert>
#include <utility>
34
#include <vector>
35
#include "twa/twa.hh"
36 37
#include "misc/hash.hh"
#include "emptiness.hh"
38
#include "emptiness_stats.hh"
39
#include "gv04.hh"
40
#include "bfssteps.hh"
41 42 43 44 45 46 47 48

namespace spot
{
  namespace
  {
    struct stack_entry
    {
      const state* s;		  // State stored in stack entry.
49
      twa_succ_iterator* lasttr; // Last transition explored from this state.
50 51 52 53 54
      int lowlink;		  // Lowlink value if this entry.
      int pre;			  // DFS predecessor.
      int acc;			  // Accepting state link.
    };

55
    struct gv04: public emptiness_check, public ec_statistics
56 57
    {
      // Map of visited states.
58 59
      typedef std::unordered_map<const state*, size_t,
				 state_ptr_hash, state_ptr_equal> hash_type;
60 61 62 63 64 65 66 67 68 69
      hash_type h;

      // Stack of visited states on the path.
      typedef std::vector<stack_entry> stack_type;
      stack_type stack;

      int top;			// Top of SCC stack.
      int dftop;		// Top of DFS stack.
      bool violation;		// Whether an accepting run was found.

70
      gv04(const const_twa_ptr& a, option_map o)
71
	: emptiness_check(a, o)
72
      {
73
	assert(a->num_sets() <= 1);
74 75 76 77 78
      }

      ~gv04()
      {
	for (stack_type::iterator i = stack.begin(); i != stack.end(); ++i)
79
	  a_->release_iter(i->lasttr);
80 81 82 83 84 85
	hash_type::const_iterator s = h.begin();
	while (s != h.end())
	  {
	    // Advance the iterator before deleting the "key" pointer.
	    const state* ptr = s->first;
	    ++s;
86
	    ptr->destroy();
87 88 89
	  }
      }

90
      virtual emptiness_check_result_ptr
91 92 93 94
      check()
      {
	top = dftop = -1;
	violation = false;
95
	push(a_->get_init_state(), false);
96 97 98 99 100

	while (!violation && dftop >= 0)
	  {
	    trace << "Main iteration (top = " << top
		  << ", dftop = " << dftop
101
		  << ", s = " << a_->format_state(stack[dftop].s)
102
		  << ')' << std::endl;
103

104
	    twa_succ_iterator* iter = stack[dftop].lasttr;
105
	    bool cont;
106 107
	    if (!iter)
	      {
108
		iter = stack[dftop].lasttr = a_->succ_iter(stack[dftop].s);
109
		cont = iter->first();
110 111 112
	      }
	    else
	      {
113
		cont = iter->next();
114 115
	      }

116
	    if (!cont)
117 118 119 120 121 122 123
	      {
		trace << " No more successors" << std::endl;
		pop();
	      }
	    else
	      {
		const state* s_prime = iter->current_state();
124 125
		bool acc =
		  a_->acc().accepting(iter->current_acceptance_conditions());
126
		inc_transitions();
127 128

		trace << " Next successor: s_prime = "
129
		      << a_->format_state(s_prime)
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
		      << (acc ? " (with accepting link)" : "");

		hash_type::const_iterator i = h.find(s_prime);

		if (i == h.end())
		  {
		    trace << " is a new state." << std::endl;
		    push(s_prime, acc);
		  }
		else
		  {
		    if (i->second < stack.size()
			&& stack[i->second].s->compare(s_prime) == 0)
		      {
			// s_prime has a clone on stack
			trace << " is on stack." << std::endl;
			// This is an addition to GV04 to support TBA.
			violation |= acc;
			lowlinkupdate(dftop, i->second);
		      }
		    else
		      {
			trace << " has been seen, but is no longer on stack."
			      << std::endl;
		      }

156
		    s_prime->destroy();
157 158
		  }
	      }
159
	    set_states(h.size());
160 161
	  }
	if (violation)
162
	  return std::make_shared<result>(*this);
163
	return nullptr;
164 165 166 167 168
      }

      void
      push(const state* s, bool accepting)
      {
169
	trace << "  push(s = " << a_->format_state(s)
170
	      << ", accepting = " << accepting << ")\n";
171 172 173

	h[s] = ++top;

174
	stack_entry ss = { s, nullptr, top, dftop, 0 };
175 176

	if (accepting)
177
	  ss.acc = top - 1;	// This differs from GV04 to support TBA.
178 179 180 181 182
	else if (dftop >= 0)
	  ss.acc = stack[dftop].acc;
	else
	  ss.acc = -1;

183 184
	trace << "    s.lowlink = " << top << std::endl
	      << "    s.acc = " << ss.acc << std::endl;
185 186 187

	stack.push_back(ss);
	dftop = top;
188
	inc_depth();
189 190 191 192 193
      }

      void
      pop()
      {
194
	trace << "  pop()\n";
195 196 197 198 199 200 201 202 203

	int p = stack[dftop].pre;
	if (p >= 0)
	  lowlinkupdate(p, dftop);
	if (stack[dftop].lowlink == dftop)
	  {
	    assert(static_cast<unsigned int>(top + 1) == stack.size());
	    for (int i = top; i >= dftop; --i)
	      {
204
		a_->release_iter(stack[i].lasttr);
205
		stack.pop_back();
206
		dec_depth();
207 208 209 210 211 212 213 214 215 216
	      }
	    top = dftop - 1;
	  }
	dftop = p;
      }

      void
      lowlinkupdate(int f, int t)
      {
	trace << "  lowlinkupdate(f = " << f << ", t = " << t
217 218 219
	      << ")\n    t.lowlink = " << stack[t].lowlink
	      << "\n    f.lowlink = " << stack[f].lowlink
	      << "\n    f.acc = " << stack[f].acc << '\n';
220 221 222 223 224 225 226
	int stack_t_lowlink = stack[t].lowlink;
	if (stack_t_lowlink <= stack[f].lowlink)
	  {
	    if (stack_t_lowlink <= stack[f].acc)
	      violation = true;
	    stack[f].lowlink = stack_t_lowlink;
	    trace << "    f.lowlink updated to "
227
		  << stack[f].lowlink << '\n';
228 229 230 231 232 233
	  }
      }

      virtual std::ostream&
      print_stats(std::ostream& os) const
      {
234 235 236
	os << h.size() << " unique states visited\n";
	os << transitions() << " transitions explored\n";
	os << max_depth() << " items max on stack\n";
237 238 239
	return os;
      }

240 241
      struct result:
	public emptiness_check_result,
242
	public acss_statistics
243
      {
244 245
	gv04& data;

246
	result(gv04& data)
247 248
	  : emptiness_check_result(data.automaton(), data.options()),
	    data(data)
249 250 251
	{
	}

252 253
	void
	update_lowlinks()
254 255
	{
	  // Transitively update the lowlinks, so we can use them in
256
	  // to check SCC inclusion
257 258 259 260 261 262 263 264 265 266
	  for (int i = 0; i <= data.top; ++i)
	    {
	      int l = data.stack[i].lowlink;
	      if (l < i)
		{
		  int ll = data.stack[i].lowlink = data.stack[l].lowlink;
		  for (int j = i - 1; data.stack[j].lowlink != ll; --j)
		    data.stack[j].lowlink = ll;
		}
	    }
267 268
	}

269
	virtual unsigned
270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286
	acss_states() const
	{
	  // Gross!
	  const_cast<result*>(this)->update_lowlinks();

	  int scc = data.stack[data.dftop].lowlink;
	  int j = data.dftop;
	  int s = 0;
	  while (j >= 0 && data.stack[j].lowlink == scc)
	    {
	      --j;
	      ++s;
	    }
	  assert(s > 0);
	  return s;
	}

287
	virtual twa_run_ptr
288 289
	accepting_run()
	{
290
	  auto res = std::make_shared<twa_run>();
291 292

	  update_lowlinks();
293 294 295 296
#ifdef TRACE
	  for (int i = 0; i <= data.top; ++i)
	    {
	      trace << "state " << i << " ("
297
		    << data.a_->format_state(data.stack[i].s)
298 299 300 301 302 303 304 305 306 307 308 309 310 311
		    << ") has lowlink = " << data.stack[i].lowlink << std::endl;
	    }
#endif

	  // We will use the root of the last SCC as the start of the
	  // cycle.
	  int scc_root = data.stack[data.dftop].lowlink;
	  assert(scc_root >= 0);

	  // Construct the prefix by unwinding the DFS stack before
	  // scc_root.
	  int father = data.stack[scc_root].pre;
	  while (father >= 0)
	    {
312
	      twa_run::step st =
313 314 315 316 317 318 319 320 321
		{
		  data.stack[father].s->clone(),
		  data.stack[father].lasttr->current_condition(),
		  data.stack[father].lasttr->current_acceptance_conditions()
		};
	      res->prefix.push_front(st);
	      father = data.stack[father].pre;
	    }

322
	  // Construct the cycle in two phases.  A first BFS finds the
323 324 325 326
	  // shortest path from scc_root to an accepting transition.
	  // A second BFS then search a path back to scc_root.  If
	  // there is no acceptance conditions we just use the second
	  // BFS to find a cycle around scc_root.
327 328 329 330 331

	  struct first_bfs: bfs_steps
	  {
	    const gv04& data;
	    int scc_root;
332
	    result* r;
333

334 335 336
	    first_bfs(result* r, int scc_root)
	      : bfs_steps(r->data.automaton()), data(r->data),
		scc_root(scc_root), r(r)
337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353
	    {
	    }

	    virtual const state*
	    filter(const state* s)
	    {
	      // Do not escape the SCC
	      hash_type::const_iterator j = data.h.find(s);
	      if (// This state was never visited so far.
		  j == data.h.end()
		  // Or it was discarded
		  || j->second >= data.stack.size()
		  // Or it was discarded (but its stack slot reused)
		  || data.stack[j->second].s->compare(s)
		  // Or it is still on the stack but not in the SCC
		  || data.stack[j->second].lowlink < scc_root)
		{
354
		  s->destroy();
355
		  return nullptr;
356
		}
357
	      r->inc_ars_cycle_states();
358
	      s->destroy();
359 360 361 362
	      return j->first;
	    }

	    virtual bool
363
	    match(twa_run::step& step, const state*)
364
	    {
365
	      return step.acc != 0U;
366 367 368 369 370 371
	    }
	  };

	  struct second_bfs: first_bfs
	  {
	    const state* target;
372 373
	    second_bfs(result* r, int scc_root, const state* target)
	      : first_bfs(r, scc_root), target(target)
374 375 376 377
	    {
	    }

	    virtual bool
378
	    match(twa_run::step&, const state* s)
379 380 381 382 383
	    {
	      return s == target;
	    }
	  };

384 385
	  const state* bfs_start = data.stack[scc_root].s;
	  const state* bfs_end = bfs_start;
386
	  if (a_->num_sets() > 0)
387
	    {
388
	      first_bfs b1(this, scc_root);
389 390
	      bfs_start = b1.search(bfs_start, res->cycle);
	      assert(bfs_start);
391 392 393
	    }
	  if (bfs_start != bfs_end || res->cycle.empty())
	    {
394
	      second_bfs b2(this, scc_root, bfs_end);
395 396
	      bfs_start = b2.search(bfs_start, res->cycle);
	      assert(bfs_start == bfs_end);
397 398 399 400 401 402 403 404
	    }

	  assert(res->cycle.begin() != res->cycle.end());
	  return res;
	}
      };


405 406 407 408
    };

  } // anonymous

409
  emptiness_check_ptr
410
  explicit_gv04_check(const const_twa_ptr& a, option_map o)
411
  {
412
    return std::make_shared<gv04>(a, o);
413 414
  }
}