emptiness.cc 9.05 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
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 <sstream>
24
#include "emptiness.hh"
25
26
#include "twa/twa.hh"
#include "twa/bddprint.hh"
27
28
29
30
31
32
#include "twaalgos/gtec/gtec.hh"
#include "twaalgos/gv04.hh"
#include "twaalgos/magic.hh"
#include "twaalgos/se05.hh"
#include "twaalgos/tau03.hh"
#include "twaalgos/tau03opt.hh"
33
34
35

namespace spot
{
36
37
38
39

  // tgba_run
  //////////////////////////////////////////////////////////////////////

40
41
42
  tgba_run::~tgba_run()
  {
    for (steps::const_iterator i = prefix.begin(); i != prefix.end(); ++i)
43
      i->s->destroy();
44
    for (steps::const_iterator i = cycle.begin(); i != cycle.end(); ++i)
45
      i->s->destroy();
46
47
48
49
50
51
52
  }

  tgba_run::tgba_run(const tgba_run& run)
  {
    for (steps::const_iterator i = run.prefix.begin();
	 i != run.prefix.end(); ++i)
      {
53
	step s = { i->s->clone(), i->label, i->acc };
54
55
56
57
58
	prefix.push_back(s);
      }
    for (steps::const_iterator i = run.cycle.begin();
	 i != run.cycle.end(); ++i)
      {
59
	step s = { i->s->clone(), i->label, i->acc };
60
61
62
63
	cycle.push_back(s);
      }
  }

64
65
66
67
68
69
70
71
72
73
74
75
76
77
  tgba_run&
  tgba_run::operator=(const tgba_run& run)
  {
    if (&run != this)
      {
	this->~tgba_run();
	new(this) tgba_run(run);
      }
    return *this;
  }

  // print_tgba_run
  //////////////////////////////////////////////////////////////////////

78
79
  std::ostream&
  print_tgba_run(std::ostream& os,
80
		 const const_twa_ptr& a,
81
		 const const_tgba_run_ptr& run)
82
  {
83
    bdd_dict_ptr d = a->get_dict();
84
85
86
87
88
89
    os << "Prefix:" << std::endl;
    for (tgba_run::steps::const_iterator i = run->prefix.begin();
	 i != run->prefix.end(); ++i)
      {
	os << "  " << a->format_state(i->s) << std::endl;
	os << "  |  ";
90
	bdd_print_formula(os, d, i->label);
91
	os << '\t';
92
	os << a->acc().format(i->acc);
93
94
95
96
97
98
99
100
	os << std::endl;
      }
    os << "Cycle:" << std::endl;
    for (tgba_run::steps::const_iterator i = run->cycle.begin();
	 i != run->cycle.end(); ++i)
      {
	os << "  " << a->format_state(i->s) << std::endl;
	os << "  |  ";
101
	bdd_print_formula(os, d, i->label);
102
	os << '\t';
103
	os << a->acc().format(i->acc);
104
	os << '\n';
105
106
107
108
      }
    return os;
  }

109
110
  // emptiness_check_result
  //////////////////////////////////////////////////////////////////////
111

112
  tgba_run_ptr
113
114
  emptiness_check_result::accepting_run()
  {
115
    return nullptr;
116
117
  }

118
119
120
121
122
123
  const unsigned_statistics*
  emptiness_check_result::statistics() const
  {
    return dynamic_cast<const unsigned_statistics*>(this);
  }

124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
  const char*
  emptiness_check_result::parse_options(char* options)
  {
    option_map old(o_);
    const char* s = o_.parse_options(options);
    options_updated(old);
    return s;
  }

  void
  emptiness_check_result::options_updated(const option_map&)
  {
  }


139
140
141
  // emptiness_check
  //////////////////////////////////////////////////////////////////////

142
143
144
145
  emptiness_check::~emptiness_check()
  {
  }

146
147
148
149
150
151
  const unsigned_statistics*
  emptiness_check::statistics() const
  {
    return dynamic_cast<const unsigned_statistics*>(this);
  }

152
153
154
155
156
157
  const ec_statistics*
  emptiness_check::emptiness_check_statistics() const
  {
    return dynamic_cast<const ec_statistics*>(this);
  }

158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
  const char*
  emptiness_check::parse_options(char* options)
  {
    option_map old(o_);
    const char* s = o_.parse_options(options);
    options_updated(old);
    return s;
  }

  void
  emptiness_check::options_updated(const option_map&)
  {
  }

  bool
  emptiness_check::safe() const
  {
    return true;
  }

178
179
180
181
182
  std::ostream&
  emptiness_check::print_stats(std::ostream& os) const
  {
    return os;
  }
183

184
185
186
187
188
189
190
191
  // emptiness_check_instantiator
  //////////////////////////////////////////////////////////////////////

  namespace
  {
    struct ec_algo
    {
      const char* name;
192
      emptiness_check_ptr(*construct)(const const_twa_ptr&,
193
				      spot::option_map);
194
195
196
197
198
199
      unsigned int min_acc;
      unsigned int max_acc;
    };

    ec_algo ec_algos[] =
      {
200
201
202
203
204
205
	{ "Cou99",     couvreur99,                    0, -1U },
	{ "CVWY90",    magic_search,                  0,   1 },
	{ "GV04",      explicit_gv04_check,           0,   1 },
	{ "SE05",      se05,                          0,   1 },
	{ "Tau03",     explicit_tau03_search,         1, -1U },
	{ "Tau03_opt", explicit_tau03_opt_search,     0, -1U },
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
      };
  }

  emptiness_check_instantiator::emptiness_check_instantiator(option_map o,
							     void* i)
    : o_(o), info_(i)
  {
  }

  unsigned int
  emptiness_check_instantiator::min_acceptance_conditions() const
  {
    return static_cast<ec_algo*>(info_)->min_acc;
  }

  unsigned int
  emptiness_check_instantiator::max_acceptance_conditions() const
  {
    return static_cast<ec_algo*>(info_)->max_acc;
  }

227
  emptiness_check_ptr
228
  emptiness_check_instantiator::instantiate(const const_twa_ptr& a) const
229
230
231
232
  {
    return static_cast<ec_algo*>(info_)->construct(a, o_);
  }

233
234
  emptiness_check_instantiator_ptr
  make_emptiness_check_instantiator(const char* name, const char** err)
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
  {
    // Skip spaces.
    while (*name && strchr(" \t\n", *name))
      ++name;

    const char* opt_str = strchr(name, '(');
    option_map o;
    if (opt_str)
      {
	const char* opt_start = opt_str + 1;
	const char* opt_end = strchr(opt_start, ')');
	if (!opt_end)
	  {
	    *err = opt_start;
	    return 0;
	  }
	std::string opt(opt_start, opt_end);

	const char* res = o.parse_options(opt.c_str());
	if (res)
	  {
	    *err  = opt.c_str() - res + opt_start;
	    return 0;
	  }
      }

    if (!opt_str)
      opt_str = name + strlen(name);

    // Ignore spaces before `(' (or trailing spaces).
    while (opt_str > name && strchr(" \t\n", *--opt_str))
      continue;
    std::string n(name, opt_str + 1);


    ec_algo* info = ec_algos;
    for (unsigned i = 0; i < sizeof(ec_algos)/sizeof(*ec_algos); ++i, ++info)
      if (n == info->name)
273
274
	{
	  *err = 0;
275
276
277
278
279
280
281
282
283
284

	  struct emptiness_check_instantiator_aux:
            public emptiness_check_instantiator
	  {
	    emptiness_check_instantiator_aux(option_map o, void* i):
	      emptiness_check_instantiator(o, i)
	    {
	    }
	  };
	  return std::make_shared<emptiness_check_instantiator_aux>(o, info);
285
	}
286
    *err = name;
287
    return nullptr;
288
289
290
291
292
  }

  // tgba_run_to_tgba
  //////////////////////////////////////////////////////////////////////

293
  twa_graph_ptr
294
  tgba_run_to_tgba(const const_twa_ptr& a, const const_tgba_run_ptr& run)
295
  {
296
    auto d = a->get_dict();
297
    auto res = make_twa_graph(d);
298
    res->copy_ap_of(a);
299
    res->copy_acceptance_of(a);
300
301

    const state* s = a->get_init_state();
302
303
    unsigned src;
    unsigned dst;
304
    const tgba_run::steps* l;
305
    acc_cond::mark_t seen_acc = 0U;
306

307
    typedef std::unordered_map<const state*, unsigned,
308
			       state_ptr_hash, state_ptr_equal> state_map;
309
310
311
312
313
314
315
316
317
318
    state_map seen;

    if (run->prefix.empty())
        l = &run->cycle;
    else
        l = &run->prefix;

    tgba_run::steps::const_iterator i = l->begin();

    assert(s->compare(i->s) == 0);
319
    src = res->new_state();
320
    seen.emplace(i->s, src);
321

322
    for (; i != l->end();)
323
324
325
      {
        // expected outgoing transition
        bdd label = i->label;
326
	acc_cond::mark_t acc = i->acc;
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344

        // compute the next expected state
        const state* next;
        ++i;
        if (i != l->end())
          {
            next = i->s;
          }
        else
          {
            if (l == &run->prefix)
              {
                l = &run->cycle;
                i = l->begin();
              }
            next = l->begin()->s;
          }

345
346
347
348
        // browse the actual outgoing transitions and
	// look for next;
	const state* the_next = nullptr;
	for (auto j: a->succ(s))
349
350
351
352
353
354
          {
            if (j->current_condition() != label
                || j->current_acceptance_conditions() != acc)
              continue;

            const state* s2 = j->current_state();
355
            if (s2->compare(next) == 0)
356
              {
357
358
359
360
		the_next = s2;
		break;
	      }
	    s2->destroy();
361
          }
362
363
364
        assert(res);
        s->destroy();
	s = the_next;
365
366


367
	auto p = seen.emplace(next, 0);
368
	if (p.second)
369
	  p.first->second = res->new_state();
370
371
	dst = p.first->second;

372
	res->new_transition(src, dst, label, acc);
373
	src = dst;
374
375
376

        // Sum acceptance conditions.
        if (l == &run->cycle && i != l->begin())
377
	  seen_acc |= acc;
378
      }
379

380
    s->destroy();
381

382
    assert(a->acc().accepting(seen_acc));
383
384
385
    return res;
  }

386
}