ltsmin.cc 27.7 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
	    if (!format_filter_[i])
	      {
		++i;
907
908
		if (i == state_size_)
		  break;
909
910
		continue;
	      }
911
	    res << vname_[i] << '=' << vars[i];
912
913
914
915
916
917
	    ++i;
	    if (i == state_size_)
	      break;
	    res << ", ";
	  }
	return res.str();
918
919
920
      }

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

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

942
943
944
945
946
      // 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.
947
      mutable const state* state_condition_last_state_;
948
949
      mutable bdd state_condition_last_cond_;
      mutable callback_context* state_condition_last_cc_;
950
951
952
    };


953
954
    //////////////////////////////////////////////////////////////////////////
    // LOADER
955
956


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

965
966
967
968
969
970
971
972
973
974
975
976
      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
	{
977
978
979
	  throw std::runtime_error(std::string("Unknown extension '")
				   + ext + "'.  Use '.prom', '.pm', '.pml', "
				   "'.dve', '.dve2C', or '.prom.spins'.");
980
	}
981

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

986
987
      std::string old = filename;
      filename += compiled_ext;
988

989
990
991
992
993
      // 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);
994

995
996
997
998
      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.
999
	  return;
1000

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

  }

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

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

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

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

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

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
1082
1083
    // 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");
      }

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

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

1100
1101
1102
1103
1104
1105
1106
1107
1108
    return { d };
  }


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

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

  ltsmin_model::~ltsmin_model()
  {
1126
  }
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163


  int ltsmin_model::state_size() const
  {
    return iface->get_state_size();
  }

  const char* ltsmin_model::state_variable_name(int var) const
  {
    return iface->get_state_variable_name(var);
  }

  int ltsmin_model::state_variable_type(int var) const
  {
    return iface->get_state_variable_type(var);
  }

  int ltsmin_model::type_count() const
  {
    return iface->get_type_count();
  }

  const char* ltsmin_model::type_name(int type) const
  {
    return iface->get_type_name(type);
  }

  int ltsmin_model::type_value_count(int type)
  {
    return iface->get_type_value_count(type);
  }

  const char* ltsmin_model::type_value_name(int type, int val)
  {
    return iface->get_type_value_name(type, val);
  }

1164
}