ce.cc 6.02 KB
Newer Older
1
// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

#include "ce.hh"
23
#include "tgbaalgos/bfssteps.hh"
24
#include "misc/hash.hh"
25
26
27

namespace spot
{
28
  namespace
29
  {
30
31
32
33
34
35
36
    typedef Sgi::hash_set<const state*,
			  state_ptr_hash, state_ptr_equal> state_set;
    class shortest_path: public bfs_steps
    {
    public:
      shortest_path(const state_set* t, const couvreur99_check_status* ecs)
        : bfs_steps(ecs->aut), target(t), ecs(ecs)
37
38
39
      {
      }

40
41
      const state*
      search(const state* start, tgba_run::steps& l)
42
      {
43
	return this->bfs_steps::search(filter(start), l);
44
      }
45

46
47
48
49
50
51
      const state*
      filter(const state* s)
      {
	numbered_state_heap::state_index_p sip = ecs->h->find(s);
	// Ignore unknown states ...
	if (!sip.first)
52
	  {
53
54
	    delete s;
	    return 0;
55
	  }
56
57
58
59
	// ... as well as dead states.
	if (*sip.second == -1)
	  return 0;
	return sip.first;
60
61
      }

62
63
64
65
66
      bool
      match(tgba_run::step&, const state* dest)
      {
        return target->find(dest) != target->end();
      }
67

68
69
70
71
72
73
    private:
      state_set seen;
      const state_set* target;
      const couvreur99_check_status* ecs;
    };
  }
74

75
76
77
78
  couvreur99_check_result::couvreur99_check_result
  (const couvreur99_check_status* ecs)
    : emptiness_check_result(ecs->aut), ecs_(ecs)
  {
79
80
  }

81
82
83
84
85
86
87
88
89
90
91
92
93
  int
  couvreur99_check_result::acss_states() const
  {
    int count = 0;
    int scc_root = ecs_->root.s.top().index;

    numbered_state_heap_const_iterator* i = ecs_->h->iterator();
    for (i->first(); !i->done(); i->next())
      if (i->get_index() >= scc_root)
	++count;
    return count;
  }

94
95
  tgba_run*
  couvreur99_check_result::accepting_run()
96
  {
97
    run_ = new tgba_run;
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
    assert(!ecs_->root.empty());

    // Compute an accepting cycle.
    accepting_cycle();

    // Compute the prefix: it's the shortest path from the initial
    // state of the automata to any state of the cycle.

    // Register all states from the cycle as target of the BFS.
    state_set ss;
    for (tgba_run::steps::const_iterator i = run_->cycle.begin();
	 i != run_->cycle.end(); ++i)
      ss.insert(i->s);
    shortest_path shpath(&ss, ecs_);

    const state* prefix_start = ecs_->aut->get_init_state();
    // There are two cases: either the initial state is already on
    // the cycle, or it is not.  If it is, we will have to rotate
    // the cycle so it begins on this position.  Otherwise we will shift
    // the cycle so it begins on the state that follows the prefix.
    // cycle_entry_point is that state.
    const state* cycle_entry_point;
    state_set::const_iterator ps = ss.find(prefix_start);
    if (ps != ss.end())
123
      {
124
125
126
	// The initial state is on the cycle.
	delete prefix_start;
	cycle_entry_point = *ps;
127
      }
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
    else
      {
	// This initial state is outside the cycle.  Compute the prefix.
        cycle_entry_point = shpath.search(prefix_start, run_->prefix);
      }

    // Locate cycle_entry_point on the cycle.
    tgba_run::steps::iterator cycle_ep_it;
    for (cycle_ep_it = run_->cycle.begin();
	 cycle_ep_it != run_->cycle.end()
	   && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it)
      continue;
    assert(cycle_ep_it != run_->cycle.end());

    // Now shift the cycle so it starts on cycle_entry_point.
    run_->cycle.splice(run_->cycle.end(), run_->cycle,
		       run_->cycle.begin(), cycle_ep_it);
145

146
    return run_;
147
148
  }

martinez's avatar
martinez committed
149
  void
150
  couvreur99_check_result::accepting_cycle()
martinez's avatar
martinez committed
151
  {
152
    bdd acc_to_traverse = ecs_->aut->all_acceptance_conditions();
153
154
155
156
157
    // Compute an accepting cycle using successive BFS that are
    // restarted from the point reached after we have discovered a
    // transition with a new acceptance conditions.
    //
    // This idea is taken from Product<T>::findWitness in LBTT 1.1.2.
158
    const state* substart = ecs_->cycle_seed;
159
    do
martinez's avatar
martinez committed
160
      {
161
162
	struct scc_bfs: bfs_steps
	{
163
	  const couvreur99_check_status* ecs;
164
	  bdd& acc_to_traverse;
165
166
167
168
169
	  int scc_root;
	  scc_bfs(const couvreur99_check_status* ecs,
		  bdd& acc_to_traverse)
	    : bfs_steps(ecs->aut), ecs(ecs), acc_to_traverse(acc_to_traverse),
	      scc_root(ecs->root.s.top().index)
170
171
	  {
	  }
172

173
174
175
	  virtual const state*
	  filter(const state* s)
	  {
176
177
178
179
180
181
182
183
184
185
186
	    numbered_state_heap::state_index_p sip = ecs->h->find(s);
	    // Ignore unknown states.
	    if (!sip.first)
	      {
		delete s;
		return 0;
	      }
	    // Stay in the final SCC.
	    if (*sip.second < scc_root)
	      return 0;
	    return sip.first;
187
	  }
martinez's avatar
martinez committed
188

189
190
	  virtual bool
	  match(tgba_run::step& st, const state* s)
martinez's avatar
martinez committed
191
	  {
192
193
194
	    bdd less_acc = acc_to_traverse - st.acc;
	    if (less_acc != acc_to_traverse
		|| (acc_to_traverse == bddfalse
195
		    && s == ecs->cycle_seed))
martinez's avatar
martinez committed
196
	      {
197
198
		acc_to_traverse = less_acc;
		return true;
martinez's avatar
martinez committed
199
	      }
200
	    return false;
martinez's avatar
martinez committed
201
	  }
202

203
	} b(ecs_, acc_to_traverse);
204
205

	substart = b.search(substart, run_->cycle);
martinez's avatar
martinez committed
206
      }
207
    while (acc_to_traverse != bddfalse || substart != ecs_->cycle_seed);
208
209
210
  }

  void
211
  couvreur99_check_result::print_stats(std::ostream& os) const
212
213
  {
    ecs_->print_stats(os);
214
215
216
217
    // FIXME: This is bogusly assuming run_ exists.  (Even if we
    // created it, the user might have delete it.)
    os << run_->prefix.size() << " states in run_->prefix" << std::endl;
    os << run_->cycle.size() << " states in run_->cycle" << std::endl;
218
219
220
  }

}