ce.cc 6.64 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
4
// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
6 7 8 9 10 11
// 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
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

#include "ce.hh"
24
#include "twaalgos/bfssteps.hh"
25
#include "misc/hash.hh"
26 27 28

namespace spot
{
29
  namespace
30
  {
31 32 33
    class shortest_path: public bfs_steps
    {
    public:
34
      shortest_path(const state_set* t,
35
		    const std::shared_ptr<const couvreur99_check_status>& ecs,
36 37
		    couvreur99_check_result* r)
        : bfs_steps(ecs->aut), target(t), ecs(ecs), r(r)
38 39 40
      {
      }

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

47 48 49
      const state*
      filter(const state* s)
      {
50
	r->inc_ars_prefix_states();
51 52
	auto i = ecs->h.find(s);
	s->destroy();
53
	// Ignore unknown states ...
54 55
	if (i == ecs->h.end())
	  return nullptr;
56
	// ... as well as dead states.
57 58 59
	if (i->second == -1)
	  return nullptr;
	return i->first;
60 61
      }

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

68 69 70
    private:
      state_set seen;
      const state_set* target;
71
      std::shared_ptr<const couvreur99_check_status> ecs;
72
      couvreur99_check_result* r;
73 74
    };
  }
75

76
  couvreur99_check_result::couvreur99_check_result
77 78
  (const std::shared_ptr<const couvreur99_check_status>& ecs,
   option_map o)
79
    : emptiness_check_result(ecs->aut, o), ecs_(ecs)
80
  {
81 82
  }

83
  unsigned
84 85
  couvreur99_check_result::acss_states() const
  {
86
    int scc_root = ecs_->root.top().index;
87 88 89
    unsigned count = 0;
    for (auto i: ecs_->h)
      if (i.second >= scc_root)
90 91 92 93
	++count;
    return count;
  }

94
  twa_run_ptr
95
  couvreur99_check_result::accepting_run()
96
  {
97
    run_ = std::make_shared<twa_run>();
98

99 100 101 102 103 104 105 106 107 108
    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;
109
    for (twa_run::steps::const_iterator i = run_->cycle.begin();
110 111
	 i != run_->cycle.end(); ++i)
      ss.insert(i->s);
112
    shortest_path shpath(&ss, ecs_, this);
113 114 115 116 117 118 119 120 121 122

    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
	// The initial state is on the cycle.
125
	prefix_start->destroy();
126
	cycle_entry_point = *ps;
127
      }
128 129 130 131 132 133 134
    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.
135
    twa_run::steps::iterator cycle_ep_it;
136 137 138 139 140 141 142 143 144
    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 153
    acc_cond::mark_t acc_to_traverse =
      ecs_->aut->acc().accepting_sets(ecs_->root.top().condition);
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.
    //
158 159 160 161 162 163 164 165 166 167 168 169
    // This idea is taken from Product<T>::findWitness in LBTT 1.1.2,
    // which in turn is probably inspired from
    // @Article{	  latvala.00.fi,
    //   author	= {Timo Latvala and Keijo Heljanko},
    //   title		= {Coping With Strong Fairness},
    //   journal	= {Fundamenta Informaticae},
    //   year		= {2000},
    //   volume	= {43},
    //   number	= {1--4},
    //   pages		= {1--19},
    //   publisher	= {IOS Press}
    // }
170
    const state* substart = ecs_->cycle_seed;
171
    do
martinez's avatar
martinez committed
172
      {
173 174
	struct scc_bfs: bfs_steps
	{
175
	  const couvreur99_check_status* ecs;
176
	  couvreur99_check_result* r;
177
	  acc_cond::mark_t& acc_to_traverse;
178
	  int scc_root;
179

180
	  scc_bfs(const couvreur99_check_status* ecs,
181
		  couvreur99_check_result* r, acc_cond::mark_t& acc_to_traverse)
182 183
	    : bfs_steps(ecs->aut), ecs(ecs), r(r),
	      acc_to_traverse(acc_to_traverse),
184
	      scc_root(ecs->root.top().index)
185 186
	  {
	  }
187

188 189 190
	  virtual const state*
	  filter(const state* s)
	  {
191 192
	    auto i = ecs->h.find(s);
	    s->destroy();
193
	    // Ignore unknown states.
194
	    if (i == ecs->h.end())
195
	      return nullptr;
196
	    // Stay in the final SCC.
197
	    if (i->second < scc_root)
198
	      return nullptr;
199
	    r->inc_ars_cycle_states();
200
	    return i->first;
201
	  }
martinez's avatar
martinez committed
202

203
	  virtual bool
204
	  match(twa_run::step& st, const state* s)
martinez's avatar
martinez committed
205
	  {
206 207
	    acc_cond::mark_t less_acc =
	      acc_to_traverse - st.acc;
208
	    if (less_acc != acc_to_traverse
209
		|| (acc_to_traverse == 0U
210
		    && s == ecs->cycle_seed))
martinez's avatar
martinez committed
211
	      {
212 213
		acc_to_traverse = less_acc;
		return true;
martinez's avatar
martinez committed
214
	      }
215
	    return false;
martinez's avatar
martinez committed
216
	  }
217

218
	} b(ecs_.get(), this, acc_to_traverse);
219 220

	substart = b.search(substart, run_->cycle);
221
	assert(substart);
martinez's avatar
martinez committed
222
      }
223
    while (acc_to_traverse != 0U || substart != ecs_->cycle_seed);
224 225 226
  }

  void
227
  couvreur99_check_result::print_stats(std::ostream& os) const
228 229
  {
    ecs_->print_stats(os);
230
    // FIXME: This is bogusly assuming run_ exists.  (Even if we
231
    // created it, the user might have deleted it.)
232 233
    os << run_->prefix.size() << " states in run_->prefix" << std::endl;
    os << run_->cycle.size() << " states in run_->cycle" << std::endl;
234 235 236
  }

}