magic.cc 3.24 KB
Newer Older
1
#include <iterator>
2
#include <cassert>
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
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
#include "magic.hh"
#include "tgba/bddprint.hh"

namespace spot
{

  const unsigned char seen_without_magic = 1;
  const unsigned char seen_with_magic = 2;

  magic_search::magic_search(const tgba_tba_proxy* a)
    : a(a), x(0)
  {
  }

  magic_search::~magic_search()
  {
    for (hash_type::iterator i = h.begin(); i != h.end(); ++i)
      delete i->first;
    if (x)
      delete x;
  }

  void
  magic_search::push(const state* s, bool m)
  {
    tgba_succ_iterator* i = a->succ_iter(s);
    i->first();

    hash_type::iterator hi = h.find(s);
    if (hi == h.end())
      {
	magic d = { !m, m };
	h[s] = d;
      }
    else
      {
	hi->second.seen_without |= !m;
	hi->second.seen_with |= m;
	if (hi->first != s)
	  delete s;
	s = hi->first;
      }

    magic_state ms = { s, m };
    stack.push_front(state_iter_pair(ms, i));
  }

  bool
  magic_search::has(const state* s, bool m) const
  {
    hash_type::const_iterator i = h.find(s);
    if (i == h.end())
      return false;
    if (!m && i->second.seen_without)
      return true;
    if (m && i->second.seen_with)
      return true;
    return false;
  }

  bool
  magic_search::check()
  {
    if (stack.empty())
      // It's a new search.
      push(a->get_init_state(), false);
    else
      // Remove the transition to the cycle root.
      tstack.pop_front();

    assert(stack.size() == 1 + tstack.size());

    while (! stack.empty())
      {
      recurse:
	magic_search::state_iter_pair& p = stack.front();
	tgba_succ_iterator* i = p.second;
	const bool magic = p.first.m;

	while (! i->done())
	  {
	    const state* s_prime = i->current_state();
	    bdd c = i->current_condition();
	    i->next();
	    if (magic && 0 == s_prime->compare(x))
	      {
		delete s_prime;
		tstack.push_front(c);
		assert(stack.size() == tstack.size());
		return true;
	      }
	    if (! has(s_prime, magic))
	      {
		push(s_prime, magic);
		tstack.push_front(c);
		goto recurse;
	      }
	    delete s_prime;
	  }

	const state* s = p.first.s;
	stack.pop_front();

	if (! magic && a->state_is_accepting(s))
	  {
	    if (! has(s, true))
	      {
		if (x)
		  delete x;
		x = s->clone();
		push(s, true);
		continue;
	      }
	  }
	if (! stack.empty())
	  tstack.pop_front();
      }

    assert(tstack.empty());
    return false;
  }

  std::ostream&
126
  magic_search::print_result(std::ostream& os, const tgba* restrict) const
127
128
129
130
131
  {
    stack_type::const_reverse_iterator i;
    tstack_type::const_reverse_iterator ti;
    os << "Prefix:" << std::endl;
    const bdd_dict* d = a->get_dict();
132
    for (i = stack.rbegin(), ti = tstack.rbegin();
133
134
135
136
	 i != stack.rend(); ++i, ++ti)
      {
	if (i->first.s->compare(x) == 0)
	  os <<"Cycle:" <<std::endl;
137
138
139
140
141
142
143
144
145
146
147
148
149

	const state* s = i->first.s;
	if (restrict)
	  {
	    s = a->project_state(s, restrict);
	    assert(s);
	    os << "  " << restrict->format_state(s) << std::endl;
	    delete s;
	  }
	else
	  {
	    os << "  " << a->format_state(s) << std::endl;
	  }
150
151
	os << "    | " << bdd_format_set(d, *ti) << std::endl;
      }
152
153
154
155
156
157
158
159
160
161
162
163

    if (restrict)
      {
	const state* s = a->project_state(x, restrict);
	assert(s);
	os << "  " << restrict->format_state(s) << std::endl;
	delete s;
      }
    else
      {
	os << "  " << a->format_state(x) << std::endl;
      }
164
165
166
167
    return os;
  }

}