ltsmin.cc 27 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE)
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
21
22
23
#include <ltdl.h>
#include <cstring>
#include <cstdlib>
#include <vector>
24
#include <sstream>
25
26
#include <sys/stat.h>
#include <unistd.h>
27

28
29
30
31
32
// MinGW does not define this.
#ifndef WEXITSTATUS
# define WEXITSTATUS(x) ((x) & 0xff)
#endif

33
#include <spot/ltsmin/ltsmin.hh>
34
35
36
37
38
#include <spot/misc/hashfunc.hh>
#include <spot/misc/fixpool.hh>
#include <spot/misc/mspool.hh>
#include <spot/misc/intvcomp.hh>
#include <spot/misc/intvcmp2.hh>
39
40
41

namespace spot
{
42
43
  namespace
  {
44
45

    ////////////////////////////////////////////////////////////////////////
46
    // spins interface
47
48
49
50
51
52
53
54
55

    typedef struct transition_info {
      int* labels; // edge labels, NULL, or pointer to the edge label(s)
      int  group;  // holds transition group or -1 if unknown
    } transition_info_t;

    typedef void (*TransitionCB)(void *ctx,
				 transition_info_t *transition_info,
				 int *dst);
56
  }
57

58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
  struct spins_interface
  {
    lt_dlhandle handle;	// handle to the dynamic library
    void (*get_initial_state)(void *to);
    int (*have_property)();
    int (*get_successors)(void* m, int *in, TransitionCB, void *arg);
    int (*get_state_size)();
    const char* (*get_state_variable_name)(int var);
    int (*get_state_variable_type)(int var);
    int (*get_type_count)();
    const char* (*get_type_name)(int type);
    int (*get_type_value_count)(int type);
    const char* (*get_type_value_name)(int type, int value);

    ~spins_interface()
73
    {
74
75
76
77
78
79
80
81
82
      if (handle)
	lt_dlclose(handle);
      lt_dlexit();
    }
  };

  namespace
  {
    typedef std::shared_ptr<const spins_interface> spins_interface_ptr;
83
84
85
86

    ////////////////////////////////////////////////////////////////////////
    // STATE

87
    struct spins_state: public state
88
    {
89
      spins_state(int s, fixed_size_pool* p)
90
	: pool(p), size(s), count(1)
91
92
93
94
95
96
97
98
99
100
      {
      }

      void compute_hash()
      {
	hash_value = 0;
	for (int i = 0; i < size; ++i)
	  hash_value = wang32_hash(hash_value ^ vars[i]);
      }

101
      spins_state* clone() const
102
103
      {
	++count;
104
	return const_cast<spins_state*>(this);
105
106
107
108
109
110
      }

      void destroy() const
      {
	if (--count)
	  return;
111
	pool->deallocate(this);
112
113
114
115
116
117
118
119
120
121
122
      }

      size_t hash() const
      {
	return hash_value;
      }

      int compare(const state* other) const
      {
	if (this == other)
	  return 0;
123
	const spins_state* o = down_cast<const spins_state*>(other);
124
125
126
127
128
129
130
131
132
133
	assert(o);
	if (hash_value < o->hash_value)
	  return -1;
	if (hash_value > o->hash_value)
	  return 1;
	return memcmp(vars, o->vars, size * sizeof(*vars));
      }

    private:

134
      ~spins_state()
135
136
137
      {
      }

138
139
    public:
      fixed_size_pool* pool;
140
141
142
      size_t hash_value: 32;
      int size: 16;
      mutable unsigned count: 16;
143
      int vars[0];
144
145
    };

146
    struct spins_compressed_state: public state
147
    {
148
      spins_compressed_state(int s, multiple_size_pool* p)
149
	: pool(p), size(s), count(1)
150
151
152
153
154
155
      {
      }

      void compute_hash()
      {
	hash_value = 0;
156
157
	for (int i = 0; i < size; ++i)
	  hash_value = wang32_hash(hash_value ^ vars[i]);
158
159
      }

160
      spins_compressed_state* clone() const
161
162
      {
	++count;
163
	return const_cast<spins_compressed_state*>(this);
164
165
166
167
168
169
      }

      void destroy() const
      {
	if (--count)
	  return;
170
	pool->deallocate(this, sizeof(*this) + size * sizeof(*vars));
171
172
173
174
175
176
177
178
179
180
181
      }

      size_t hash() const
      {
	return hash_value;
      }

      int compare(const state* other) const
      {
	if (this == other)
	  return 0;
182
183
	const spins_compressed_state* o =
	  down_cast<const spins_compressed_state*>(other);
184
185
186
187
188
189
	assert(o);
	if (hash_value < o->hash_value)
	  return -1;
	if (hash_value > o->hash_value)
	  return 1;

190
	if (size < o->size)
191
	  return -1;
192
	if (size > o->size)
193
194
	  return 1;

195
	return memcmp(vars, o->vars, size * sizeof(*vars));
196
197
198
199
      }

    private:

200
      ~spins_compressed_state()
201
202
203
204
      {
      }

    public:
205
      multiple_size_pool* pool;
206
207
208
      size_t hash_value: 32;
      int size: 16;
      mutable unsigned count: 16;
209
      int vars[0];
210
211
    };

212
213
214
215
216
    ////////////////////////////////////////////////////////////////////////
    // CALLBACK FUNCTION for transitions.

    struct callback_context
    {
217
      typedef std::list<state*> transitions_t;
218
219
      transitions_t transitions;
      int state_size;
220
221
      void* pool;
      int* compressed;
222
      void (*compress)(const int*, size_t, int*, size_t&);
223
224
225

      ~callback_context()
      {
226
227
	for (auto t: transitions)
	  t->destroy();
228
      }
229
230
231
232
233
    };

    void transition_callback(void* arg, transition_info_t*, int *dst)
    {
      callback_context* ctx = static_cast<callback_context*>(arg);
234
      fixed_size_pool* p = static_cast<fixed_size_pool*>(ctx->pool);
235
236
      spins_state* out =
	new(p->allocate()) spins_state(ctx->state_size, p);
237
238
239
240
241
      memcpy(out->vars, dst, ctx->state_size * sizeof(int));
      out->compute_hash();
      ctx->transitions.push_back(out);
    }

242
243
244
    void transition_callback_compress(void* arg, transition_info_t*, int *dst)
    {
      callback_context* ctx = static_cast<callback_context*>(arg);
245
246
247
      multiple_size_pool* p = static_cast<multiple_size_pool*>(ctx->pool);

      size_t csize = ctx->state_size * 2;
248
      ctx->compress(dst, ctx->state_size, ctx->compressed, csize);
249

250
      void* mem = p->allocate(sizeof(spins_compressed_state)
251
			      + sizeof(int) * csize);
252
      spins_compressed_state* out = new(mem) spins_compressed_state(csize, p);
253
      memcpy(out->vars, ctx->compressed, csize * sizeof(int));
254
255
256
257
      out->compute_hash();
      ctx->transitions.push_back(out);
    }

258
259
260
    ////////////////////////////////////////////////////////////////////////
    // SUCC_ITERATOR

261
    class spins_succ_iterator: public kripke_succ_iterator
262
263
264
    {
    public:

265
      spins_succ_iterator(const callback_context* cc,
266
267
268
269
270
			 bdd cond)
	: kripke_succ_iterator(cond), cc_(cc)
      {
      }

271
272
273
274
275
276
277
      void recycle(const callback_context* cc, bdd cond)
      {
	delete cc_;
	cc_ = cc;
	kripke_succ_iterator::recycle(cond);
      }

278
      ~spins_succ_iterator()
279
280
281
282
283
      {
	delete cc_;
      }

      virtual
284
      bool first()
285
286
      {
	it_ = cc_->transitions.begin();
287
	return it_ != cc_->transitions.end();
288
289
290
      }

      virtual
291
      bool next()
292
293
      {
	++it_;
294
	return it_ != cc_->transitions.end();
295
296
297
298
299
300
301
302
303
      }

      virtual
      bool done() const
      {
	return it_ == cc_->transitions.end();
      }

      virtual
304
      state* dst() const
305
306
307
308
309
310
311
312
313
      {
	return (*it_)->clone();
      }

    private:
      const callback_context* cc_;
      callback_context::transitions_t::const_iterator it_;
    };

314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
    ////////////////////////////////////////////////////////////////////////
    // PREDICATE EVALUATION

    typedef enum { OP_EQ, OP_NE, OP_LT, OP_GT, OP_LE, OP_GE } relop;

    struct one_prop
    {
      int var_num;
      relop op;
      int val;
      int bddvar;  // if "var_num op val" is true, output bddvar,
		   // else its negation
    };
    typedef std::vector<one_prop> prop_set;

329
330
331
332
333
334
335
336

    struct var_info
    {
      int num;
      int type;
    };


337
    void
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
338
    convert_aps(const atomic_prop_set* aps,
339
		spins_interface_ptr d,
340
		bdd_dict_ptr dict,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
341
		formula dead,
342
343
344
		prop_set& out)
    {
      int errors = 0;
345
      std::ostringstream err;
346

347
      int state_size = d->get_state_size();
348
349
350
      typedef std::map<std::string, var_info> val_map_t;
      val_map_t val_map;

351
      for (int i = 0; i < state_size; ++i)
352
353
354
355
356
357
358
	{
	  const char* name = d->get_state_variable_name(i);
	  int type = d->get_state_variable_type(i);
	  var_info v = { i , type };
	  val_map[name] = v;
	}

359
      int type_count = d->get_type_count();
360
361
362
363
      typedef std::map<std::string, int> enum_map_t;
      std::vector<enum_map_t> enum_map(type_count);
      for (int i = 0; i < type_count; ++i)
	{
364
	  int enum_count = d->get_type_value_count(i);
365
	  for (int j = 0; j < enum_count; ++j)
366
	    enum_map[i].emplace(d->get_type_value_name(i, j), j);
367
	}
368

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
369
      for (atomic_prop_set::const_iterator ap = aps->begin();
370
371
	   ap != aps->end(); ++ap)
	{
372
373
374
	  if (*ap == dead)
	    continue;

375
	  const std::string& str = ap->ap_name();
376
377
378
379
380
381
382
	  const char* s = str.c_str();

	  // Skip any leading blank.
	  while (*s && (*s == ' ' || *s == '\t'))
	    ++s;
	  if (!*s)
	    {
383
	      err << "Proposition `" << str << "' cannot be parsed.\n";
384
385
386
387
388
389
390
	      ++errors;
	      continue;
	    }


	  char* name = (char*) malloc(str.size() + 1);
	  char* name_p = name;
391
	  char* lastdot = nullptr;
392
393
	  while (*s && (*s != '=') && *s != '<' && *s != '!'  && *s != '>')
	    {
394

395
396
397
	      if (*s == ' ' || *s == '\t')
		++s;
	      else
398
399
400
401
402
		{
		  if (*s == '.')
		    lastdot = name_p;
		  *name_p++ = *s++;
		}
403
404
405
406
407
	    }
	  *name_p = 0;

	  if (name == name_p)
	    {
408
	      err << "Proposition `" << str << "' cannot be parsed.\n";
409
410
411
412
413
414
	      free(name);
	      ++errors;
	      continue;
	    }

	  // Lookup the name
415
416
	  val_map_t::const_iterator ni = val_map.find(name);
	  if (ni == val_map.end())
417
	    {
418
419
420
421
422
423
424
425
426
427
428
	      // We may have a name such as X.Y.Z
	      // If it is not a known variable, it might mean
	      // an enumerated variable X.Y with value Z.
	      if (lastdot)
		{
		  *lastdot++ = 0;
		  ni = val_map.find(name);
		}

	      if (ni == val_map.end())
		{
429
430
431
		  err << "No variable `" << name
		      << "' found in model (for proposition `"
		      << str << "').\n";
432
433
434
435
436
437
438
439
440
441
442
		  free(name);
		  ++errors;
		  continue;
		}

	      // We have found the enumerated variable, and lastdot is
	      // pointing to its expected value.
	      int type_num = ni->second.type;
	      enum_map_t::const_iterator ei = enum_map[type_num].find(lastdot);
	      if (ei == enum_map[type_num].end())
		{
443
444
445
446
447
448
		  err << "No state `" << lastdot << "' known for variable `"
		      << name << "'.\n";
		  err << "Possible states are:";
		  for (auto& ej: enum_map[type_num])
		    err << ' ' << ej.first;
		  err << '\n';
449
450
451
452
453
454
455
456
457

		  free(name);
		  ++errors;
		  continue;
		}

	      // At this point, *s should be 0.
	      if (*s)
		{
458
459
460
		  err << "Trailing garbage `" << s
		      << "' at end of proposition `"
		      << str << "'.\n";
461
462
463
464
465
466
		  free(name);
		  ++errors;
		  continue;
		}

	      // Record that X.Y must be equal to Z.
467
	      int v = dict->register_proposition(*ap, d.get());
468
469
	      one_prop p = { ni->second.num, OP_EQ, ei->second, v };
	      out.push_back(p);
470
471
472
473
	      free(name);
	      continue;
	    }

474
475
	  int var_num = ni->second.num;

476
477
478
	  if (!*s)		// No operator?  Assume "!= 0".
	    {
	      int v = dict->register_proposition(*ap, d);
479
	      one_prop p = { var_num, OP_NE, 0, v };
480
	      out.push_back(p);
481
	      free(name);
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
	      continue;
	    }

	  relop op;

	  switch (*s)
	    {
	    case '!':
	      if (s[1] != '=')
		goto report_error;
	      op = OP_NE;
	      s += 2;
	      break;
	    case '=':
	      if (s[1] != '=')
		goto report_error;
	      op = OP_EQ;
	      s += 2;
	      break;
	    case '<':
	      if (s[1] == '=')
		{
		  op = OP_LE;
		  s += 2;
		}
	      else
		{
		  op = OP_LT;
		  ++s;
		}
	      break;
	    case '>':
	      if (s[1] == '=')
		{
516
		  op = OP_GE;
517
518
519
520
		  s += 2;
		}
	      else
		{
521
		  op = OP_GT;
522
523
524
525
526
		  ++s;
		}
	      break;
	    default:
	    report_error:
527
528
529
	      err << "Unexpected `" << s
		  << "' while parsing atomic proposition `" << str
		  << "'.\n";
530
	      ++errors;
531
	      free(name);
532
533
534
535
536
537
	      continue;
	    }

	  while (*s && (*s == ' ' || *s == '\t'))
	    ++s;

538
	  int val = 0; // Initialize to kill a warning from old compilers.
539
540
	  int type_num = ni->second.type;
	  if (type_num == 0 || (*s >= '0' && *s <= '9') || *s == '-')
541
	    {
542
543
544
545
	      char* s_end;
	      val = strtol(s, &s_end, 10);
	      if (s == s_end)
		{
546
		  err << "Failed to parse `" << s << "' as an integer.\n";
547
548
549
550
551
		  ++errors;
		  free(name);
		  continue;
		}
	      s = s_end;
552
	    }
553
554
555
556
557
558
559
560
561
562
563
564
565
	  else
	    {
	      // We are in a case such as P_0 == S, trying to convert
	      // the string S into an integer.
	      const char* end = s;
	      while (*end && *end != ' ' && *end != '\t')
		++end;
	      std::string st(s, end);

	      // Lookup the string.
	      enum_map_t::const_iterator ei = enum_map[type_num].find(st);
	      if (ei == enum_map[type_num].end())
		{
566
567
568
		  err << "No state `" << st << "' known for variable `"
		      << name << "'.\n";
		  err << "Possible states are:";
569
570
		  for (ei = enum_map[type_num].begin();
		       ei != enum_map[type_num].end(); ++ei)
571
572
		    err << ' ' << ei->first;
		  err << '\n';
573
574
575
576
577
578
579
580
581
582
583

		  free(name);
		  ++errors;
		  continue;
		}
	      s = end;
	      val = ei->second;
	    }

	  free(name);

584
585
586
587
	  while (*s && (*s == ' ' || *s == '\t'))
	    ++s;
	  if (*s)
	    {
588
589
590
591
592
	      err << "Unexpected `" << s
		  << "' while parsing atomic proposition `" << str
		  << "'.\n";
	      ++errors;
	      continue;
593
594
	    }

595

596
	  int v = dict->register_proposition(*ap, d);
597
	  one_prop p = { var_num, op, val, v };
598
599
600
	  out.push_back(p);
	}

601
602
      if (errors)
	throw std::runtime_error(err.str());
603
604
    }

605
606
607
    ////////////////////////////////////////////////////////////////////////
    // KRIPKE

608
    class spins_kripke: public kripke
609
610
611
    {
    public:

612
      spins_kripke(spins_interface_ptr d, const bdd_dict_ptr& dict,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
613
		   const spot::prop_set* ps, formula dead,
614
		   int compress)
615
616
	: kripke(dict),
	  d_(d),
617
	  state_size_(d_->get_state_size()),
618
	  dict_(dict), ps_(ps),
619
	  compress_(compress == 0 ? nullptr
620
621
		    : compress == 1 ? int_array_array_compress
		    : int_array_array_compress2),
622
	  decompress_(compress == 0 ? nullptr
623
624
		      : compress == 1 ? int_array_array_decompress
		      : int_array_array_decompress2),
625
626
	  uncompressed_(compress ? new int[state_size_ + 30] : nullptr),
	  compressed_(compress ? new int[state_size_ * 2] : nullptr),
627
628
	  statepool_(compress ? sizeof(spins_compressed_state) :
		     (sizeof(spins_state) + state_size_ * sizeof(int))),
629
630
	  state_condition_last_state_(nullptr),
	  state_condition_last_cc_(nullptr)
631
      {
632
	vname_ = new const char*[state_size_];
633
	format_filter_ = new bool[state_size_];
634
	for (int i = 0; i < state_size_; ++i)
635
636
637
638
639
640
641
	  {
	    vname_[i] = d_->get_state_variable_name(i);
	    // We don't want to print variables that can take a single
	    // value (e.g. process with a single state) to shorten the
	    // output.
	    int type = d->get_state_variable_type(i);
	    format_filter_[i] =
642
	      (d->get_type_value_count(type) != 1);
643
	  }
644
645
646
647
648
649
650
651
652
653
654
655
656
657

	// Register the "dead" proposition.  There are three cases to
	// consider:
	//  * If DEAD is "false", it means we are not interested in finite
	//    sequences of the system.
	//  * If DEAD is "true", we want to check finite sequences as well
	//    as infinite sequences, but do not need to distinguish them.
	//  * If DEAD is any other string, this is the name a property
	//    that should be true when looping on a dead state, and false
	//    otherwise.
	// We handle these three cases by setting ALIVE_PROP and DEAD_PROP
	// appropriately.  ALIVE_PROP is the bdd that should be ANDed
	// to all transitions leaving a live state, while DEAD_PROP should
	// be ANDed to all transitions leaving a dead state.
658
	if (dead.is_ff())
659
660
661
662
	  {
	    alive_prop = bddtrue;
	    dead_prop = bddfalse;
	  }
663
	else if (dead.is_tt())
664
665
666
667
668
669
670
671
672
673
	  {
	    alive_prop = bddtrue;
	    dead_prop = bddtrue;
	  }
	else
	  {
	    int var = dict->register_proposition(dead, d_);
	    dead_prop = bdd_ithvar(var);
	    alive_prop = bdd_nithvar(var);
	  }
674
675
      }

676
      ~spins_kripke()
677
      {
678
679
680
681
682
	if (iter_cache_)
	  {
	    delete iter_cache_;
	    iter_cache_ = nullptr;
	  }
683
	delete[] format_filter_;
684
	delete[] vname_;
685
	if (compress_)
686
687
688
689
	  {
	    delete[] uncompressed_;
	    delete[] compressed_;
	  }
690
	dict_->unregister_all_my_variables(d_.get());
691
692

	delete ps_;
693
694
695
696

	if (state_condition_last_state_)
	  state_condition_last_state_->destroy();
	delete state_condition_last_cc_; // Might be 0 already.
697
698
699
700
701
      }

      virtual
      state* get_init_state() const
      {
702
703
704
	if (compress_)
	  {
	    d_->get_initial_state(uncompressed_);
705
	    size_t csize = state_size_ * 2;
706
	    compress_(uncompressed_, state_size_, compressed_, csize);
707
708
709

	    multiple_size_pool* p =
	      const_cast<multiple_size_pool*>(&compstatepool_);
710
	    void* mem = p->allocate(sizeof(spins_compressed_state)
711
				    + sizeof(int) * csize);
712
713
	    spins_compressed_state* res = new(mem)
	      spins_compressed_state(csize, p);
714
	    memcpy(res->vars, compressed_, csize * sizeof(int));
715
716
717
718
719
	    res->compute_hash();
	    return res;
	  }
	else
	  {
720
	    fixed_size_pool* p = const_cast<fixed_size_pool*>(&statepool_);
721
	    spins_state* res = new(p->allocate()) spins_state(state_size_, p);
722
723
724
725
	    d_->get_initial_state(res->vars);
	    res->compute_hash();
	    return res;
	  }
726
727
      }

728
      bdd
729
      compute_state_condition_aux(const int* vars) const
730
731
      {
	bdd res = bddtrue;
732
	for (auto& i: *ps_)
733
	  {
734
735
	    int l = vars[i.var_num];
	    int r = i.val;
736
737

	    bool cond = false;
738
	    switch (i.op)
739
	      {
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
	      case OP_EQ:
		cond = (l == r);
		break;
	      case OP_NE:
		cond = (l != r);
		break;
	      case OP_LT:
		cond = (l < r);
		break;
	      case OP_GT:
		cond = (l > r);
		break;
	      case OP_LE:
		cond = (l <= r);
		break;
	      case OP_GE:
		cond = (l >= r);
		break;
758
759
760
	      }

	    if (cond)
761
	      res &= bdd_ithvar(i.bddvar);
762
	    else
763
	      res &= bdd_nithvar(i.bddvar);
764
	  }
765
766
767
	return res;
      }

768
769
770
771
772
773
774
775
      callback_context* build_cc(const int* vars, int& t) const
      {
	callback_context* cc = new callback_context;
	cc->state_size = state_size_;
	cc->pool =
	  const_cast<void*>(compress_
			    ? static_cast<const void*>(&compstatepool_)
			    : static_cast<const void*>(&statepool_));
776
	cc->compress = compress_;
777
	cc->compressed = compressed_;
778
	t = d_->get_successors(nullptr, const_cast<int*>(vars),
779
780
781
782
783
784
785
786
			       compress_
			       ? transition_callback_compress
			       : transition_callback,
			       cc);
	assert((unsigned)t == cc->transitions.size());
	return cc;
      }

787
788
789
790
791
792
793
794
795
796
797
      bdd
      compute_state_condition(const state* st) const
      {
	// If we just computed it, don't do it twice.
	if (st == state_condition_last_state_)
	  return state_condition_last_cond_;

	if (state_condition_last_state_)
	  {
	    state_condition_last_state_->destroy();
	    delete state_condition_last_cc_; // Might be 0 already.
798
	    state_condition_last_cc_ = nullptr;
799
800
801
802
803
	  }

	const int* vars = get_vars(st);

	bdd res = compute_state_condition_aux(vars);
804
805
	int t;
	callback_context* cc = build_cc(vars, t);
806
807
808
809
810
811
812
813
814
815
816

	if (t)
	  {
	    res &= alive_prop;
	  }
	else
	  {
	    res &= dead_prop;

	    // Add a self-loop to dead-states if we care about these.
	    if (res != bddfalse)
817
	      cc->transitions.push_back(st->clone());
818
819
	  }

820
	state_condition_last_cc_ = cc;
821
	state_condition_last_cond_ = res;
822
	state_condition_last_state_ = st->clone();
823

824
825
826
	return res;
      }

827
828
829
830
831
832
      const int*
      get_vars(const state* st) const
      {
	const int* vars;
	if (compress_)
	  {
833
834
	    const spins_compressed_state* s =
	      down_cast<const spins_compressed_state*>(st);
835
836
	    assert(s);

837
	    decompress_(s->vars, s->size, uncompressed_, state_size_);
838
839
840
841
	    vars = uncompressed_;
	  }
	else
	  {
842
	    const spins_state* s = down_cast<const spins_state*>(st);
843
844
845
846
847
848
849
	    assert(s);
	    vars = s->vars;
	  }
	return vars;
      }


850
      virtual
851
      spins_succ_iterator*
852
      succ_iter(const state* st) const
853
      {
854
	// This may also compute successors in state_condition_last_cc
855
	bdd scond = compute_state_condition(st);
856
857
858
859
860

	callback_context* cc;
	if (state_condition_last_cc_)
	  {
	    cc = state_condition_last_cc_;
861
	    state_condition_last_cc_ = nullptr; // Now owned by the iterator.
862
863
864
	  }
	else
	  {
865
	    int t;
866
	    cc = build_cc(get_vars(st), t);
867
868
869

	    // Add a self-loop to dead-states if we care about these.
	    if (t == 0 && scond != bddfalse)
870
	      cc->transitions.push_back(st->clone());
871
	  }
872

873
874
	if (iter_cache_)
	  {
875
876
	    spins_succ_iterator* it =
	      down_cast<spins_succ_iterator*>(iter_cache_);
877
878
879
880
	    it->recycle(cc, scond);
	    iter_cache_ = nullptr;
	    return it;
	  }
881
	return new spins_succ_iterator(cc, scond);
882
883
884
885
      }

      virtual
      bdd
886
      state_condition(const state* st) const
887
      {
888
	return compute_state_condition(st);
889
890
891
      }

      virtual
892
      std::string format_state(const state *st) const
893
      {
894
	const int* vars = get_vars(st);
895
896
897
898
899
900
901
902
903

	std::stringstream res;

	if (state_size_ == 0)
	  return "empty state";

	int i = 0;
	for (;;)
	  {
904
905
906
907
908
	    if (!format_filter_[i])
	      {
		++i;
		continue;
	      }
909
	    res << vname_[i] << '=' << vars[i];
910
911
912
913
914
915
	    ++i;
	    if (i == state_size_)
	      break;
	    res << ", ";
	  }
	return res.str();
916
917
918
      }

      virtual
919
      spot::bdd_dict_ptr get_dict() const
920
921
922
923
924
      {
	return dict_;
      }

    private:
925
      spins_interface_ptr d_;
926
      int state_size_;
927
      bdd_dict_ptr dict_;
928
      const char** vname_;
929
      bool* format_filter_;
930
      const spot::prop_set* ps_;
931
932
      bdd alive_prop;
      bdd dead_prop;
933
934
      void (*compress_)(const int*, size_t, int*, size_t&);
      void (*decompress_)(const int*, size_t, int*, size_t);
935
      int* uncompressed_;
936
      int* compressed_;
937
      fixed_size_pool statepool_;
938
      multiple_size_pool compstatepool_;
939

940
941
942
943
944
      // This cache is used to speedup repeated calls to state_condition()
      // and get_succ().
      // If state_condition_last_state_ != 0, then state_condition_last_cond_
      // contain its (recently computed) condition.  If additionally
      // state_condition_last_cc_ != 0, then it contains the successors.
945
      mutable const state* state_condition_last_state_;
946
947
      mutable bdd state_condition_last_cond_;
      mutable callback_context* state_condition_last_cc_;
948
949
950
    };


951
952
    //////////////////////////////////////////////////////////////////////////
    // LOADER
953
954


955
956
    // Call spins to compile "foo.prom" as "foo.prom.spins" if the latter
    // does not exist already or is older.
957
958
    static void
    compile_model(std::string& filename, std::string& ext)
959
960
961
    {
      std::string command;
      std::string compiled_ext;
962

963
964
965
966
967
968
969
970
971
972
973
974
      if (ext == ".prom" || ext == ".pm" || ext == ".pml")
	{
	  command = "spins " + filename;
	  compiled_ext = ".spins";
	}
      else if (ext == ".dve")
	{
	  command = "divine compile --ltsmin " + filename;
	  compiled_ext = "2C";
	}
      else
	{
975
976
977
	  throw std::runtime_error(std::string("Unknown extension '")
				   + ext + "'.  Use '.prom', '.pm', '.pml', "
				   "'.dve', '.dve2C', or '.prom.spins'.");
978
	}
979

980
981
      struct stat s;
      if (stat(filename.c_str(), &s) != 0)
982
	throw std::runtime_error(std::string("Cannot open ") + filename);
983

984
985
      std::string old = filename;
      filename += compiled_ext;
986

987
988
989
990
991
      // Remove any directory, because the new file will
      // be compiled in the current directory.
      size_t pos = filename.find_last_of("/\\");
      if (pos != std::string::npos)
	filename = "./" + filename.substr(pos + 1);
992

993
994
995
996
      struct stat d;
      if (stat(filename.c_str(), &d) == 0)
	if (s.st_mtime < d.st_mtime)
	  // The .spins or .dve2C is up-to-date, no need to recompile it.
997
	  return;
998

999
1000
      int res = system(command.c_str());
      if (res)
1001
1002
1003
	throw std::runtime_error(std::string("Execution of '")
				 + command.c_str() + "' returned exit code "
				 + std::to_string(WEXITSTATUS(res)));
1004
    }
1005
1006
1007

  }

1008
1009
  ltsmin_model
  ltsmin_model::load(const std::string& file_arg)
1010
  {
1011
1012
1013
1014
1015
1016
    std::string file;
    if (file_arg.find_first_of("/\\") != std::string::npos)
      file = file_arg;
    else
      file = "./" + file_arg;

1017
    std::string ext = file.substr(file.find_last_of("."));
1018
    if (ext != ".spins" && ext != ".dve2C")
1019
      compile_model(file, ext);
1020

1021
    if (lt_dlinit())
1022
      throw std::runtime_error("Failed to initialize libltldl.");
1023
1024
1025
1026
1027

    lt_dlhandle h = lt_dlopen(file.c_str());
    if (!h)
      {
	lt_dlexit();
1028
1029
	throw std::runtime_error(std::string("Failed to load '")
				 + file + "'.");
1030
1031
      }

1032
    auto d = std::make_shared<spins_interface>();
1033
1034
    d->handle = h;

1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
    // SpinS interface.
    if ((d->get_initial_state = (void (*)(void*))
        lt_dlsym(h, "spins_get_initial_state")))
      {
        d->have_property = nullptr;
        d->get_successors = (int (*)(void*, int*, TransitionCB, void*))
        lt_dlsym(h, "spins_get_successor_all");
        d->get_state_size = (int (*)())
        lt_dlsym(h, "spins_get_state_size");
        d->get_state_variable_name = (const char* (*)(int))
        lt_dlsym(h, "spins_get_state_variable_name");
        d->get_state_variable_type = (int (*)(int))
        lt_dlsym(h, "spins_get_state_variable_type");
        d->get_type_count = (int (*)())
        lt_dlsym(h, "spins_get_type_count");
        d->get_type_name = (const char* (*)(int))
        lt_dlsym(h, "spins_get_type_name");
        d->get_type_value_count = (int (*)(int))
        lt_dlsym(h, "spins_get_type_value_count");
        d->get_type_value_name = (const char* (*)(int, int))
        lt_dlsym(h, "spins_get_type_value_name");
      }
    // dve2 interface.
    else
      {
        d->get_initial_state = (void (*)(void*))
        lt_dlsym(h, "get_initial_state");
        d->have_property = (int (*)())
        lt_dlsym(h, "have_property");
        d->get_successors = (int (*)(void*, int*, TransitionCB, void*))
        lt_dlsym(h, "get_successors");
        d->get_state_size = (int (*)())
        lt_dlsym(h, "get_state_variable_count");
        d->get_state_variable_name = (const char* (*)(int))
        lt_dlsym(h, "get_state_variable_name");
        d->get_state_variable_type = (int (*)(int))
        lt_dlsym(h, "get_state_variable_type");
        d->get_type_count = (int (*)())
        lt_dlsym(h, "get_state_variable_type_count");
        d->get_type_name = (const char* (*)(int))
        lt_dlsym(h, "get_state_variable_type_name");
        d->get_type_value_count = (int (*)(int))
        lt_dlsym(h, "get_state_variable_type_value_count");
        d->get_type_value_name = (const char* (*)(int, int))
        lt_dlsym(h, "get_state_variable_type_value");
      }

1082
    if (!(d->get_initial_state
1083
	  && d->get_successors
1084
	  && d->get_state_size
1085
1086
	  && d->get_state_variable_name
	  && d->get_state_variable_type
1087
1088
1089
1090
	  && d->get_type_count
	  && d->get_type_name
	  && d->get_type_value_count
	  && d->get_type_value_name))
1091
1092
      throw std::runtime_error(std::string("Failed resolve some symbol"
					   "while loading '") + file + "'.");
1093

1094
    if (d->have_property && d->have_property())
1095
1096
      throw std::runtime_error("Models with embedded properties "
			       "are not supported.");
1097

1098
1099
1100
1101
1102
1103
1104
1105
1106
    return { d };
  }


  kripke_ptr
  ltsmin_model::kripke(const atomic_prop_set* to_observe,
		       bdd_dict_ptr dict,
		       const formula dead, int compress) const
  {
1107
    spot::prop_set* ps = new spot::prop_set;
1108
1109
1110
1111
1112
    try
      {
	convert_aps(to_observe, iface, dict, dead, *ps);
      }
    catch (std::runtime_error)
1113
1114
      {
	delete ps;
1115
1116
	dict->unregister_all_my_variables(iface.get());
	throw;
1117
1118
      }

1119
1120
1121
1122
1123
    return std::make_shared<spins_kripke>(iface, dict, ps, dead, compress);
  }

  ltsmin_model::~ltsmin_model()
  {
1124
1125
  }
}