ltsmin.cc 56.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011, 2012, 2014-2018 Laboratoire de
3
// Recherche et 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
#include "config.h"
21
22
23
24
#include <ltdl.h>
#include <cstring>
#include <cstdlib>
#include <vector>
25
#include <sstream>
26
27
#include <sys/stat.h>
#include <unistd.h>
28

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

34
#include <spot/ltsmin/ltsmin.hh>
35
36
37
38
39
#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>
40

Etienne Renault's avatar
Etienne Renault committed
41
42
43
44
45
#include <spot/twaalgos/reachiter.hh>
#include <string.h>
#include <spot/twacube/cube.hh>
#include <spot/mc/utils.hh>

46
47
48
#include <bricks/brick-hashset.h>
#include <bricks/brick-hash.h>

49
50
namespace spot
{
51
52
  namespace
  {
53
    ////////////////////////////////////////////////////////////////////////
54
    // spins interface
55
56
57
58
59
60
61

    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,
62
63
                                 transition_info_t *transition_info,
                                 int *dst);
64
  }
65

66
67
  struct spins_interface
  {
68
    lt_dlhandle handle;        // handle to the dynamic library
69
70
71
72
73
74
75
76
77
78
79
80
    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()
81
    {
82
      if (handle)
83
        lt_dlclose(handle);
84
85
86
87
88
89
90
      lt_dlexit();
    }
  };

  namespace
  {
    typedef std::shared_ptr<const spins_interface> spins_interface_ptr;
91
92
93
94

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

95
    struct spins_state final: public state
96
    {
97
      spins_state(int s, fixed_size_pool* p)
98
        : pool(p), size(s), count(1)
99
100
101
102
103
      {
      }

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

109
      spins_state* clone() const override
110
      {
111
112
        ++count;
        return const_cast<spins_state*>(this);
113
114
      }

115
      void destroy() const override
116
      {
117
118
119
        if (--count)
          return;
        pool->deallocate(this);
120
121
      }

122
      size_t hash() const override
123
      {
124
        return hash_value;
125
126
      }

127
      int compare(const state* other) const override
128
      {
129
130
131
132
133
134
135
136
        if (this == other)
          return 0;
        const spins_state* o = down_cast<const spins_state*>(other);
        if (hash_value < o->hash_value)
          return -1;
        if (hash_value > o->hash_value)
          return 1;
        return memcmp(vars, o->vars, size * sizeof(*vars));
137
138
139
140
      }

    private:

141
      ~spins_state()
142
143
144
      {
      }

145
146
    public:
      fixed_size_pool* pool;
147
148
149
      size_t hash_value: 32;
      int size: 16;
      mutable unsigned count: 16;
150
      int vars[1];
151
152
    };

153
    struct spins_compressed_state final: public state
154
    {
155
      spins_compressed_state(int s, multiple_size_pool* p)
156
        : pool(p), size(s), count(1)
157
158
159
160
161
      {
      }

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

167
      spins_compressed_state* clone() const override
168
      {
169
170
        ++count;
        return const_cast<spins_compressed_state*>(this);
171
172
      }

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

181
      size_t hash() const override
182
      {
183
        return hash_value;
184
185
      }

186
      int compare(const state* other) const override
187
      {
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
        if (this == other)
          return 0;
        const spins_compressed_state* o =
          down_cast<const spins_compressed_state*>(other);
        if (hash_value < o->hash_value)
          return -1;
        if (hash_value > o->hash_value)
          return 1;

        if (size < o->size)
          return -1;
        if (size > o->size)
          return 1;

        return memcmp(vars, o->vars, size * sizeof(*vars));
203
204
205
206
      }

    private:

207
      ~spins_compressed_state()
208
209
210
211
      {
      }

    public:
212
      multiple_size_pool* pool;
213
214
215
      size_t hash_value: 32;
      int size: 16;
      mutable unsigned count: 16;
216
      int vars[1];
217
218
    };

219
220
221
222
223
    ////////////////////////////////////////////////////////////////////////
    // CALLBACK FUNCTION for transitions.

    struct callback_context
    {
224
      typedef std::list<state*> transitions_t;
225
226
      transitions_t transitions;
      int state_size;
227
228
      void* pool;
      int* compressed;
229
      void (*compress)(const int*, size_t, int*, size_t&);
230
231
232

      ~callback_context()
      {
233
234
        for (auto t: transitions)
          t->destroy();
235
      }
236
237
238
239
240
    };

    void transition_callback(void* arg, transition_info_t*, int *dst)
    {
      callback_context* ctx = static_cast<callback_context*>(arg);
241
      fixed_size_pool* p = static_cast<fixed_size_pool*>(ctx->pool);
242
      spins_state* out =
243
        new(p->allocate()) spins_state(ctx->state_size, p);
244
245
      memcpy(out->vars, dst, ctx->state_size * sizeof(int));
      out->compute_hash();
246
      ctx->transitions.emplace_back(out);
247
248
    }

249
250
251
    void transition_callback_compress(void* arg, transition_info_t*, int *dst)
    {
      callback_context* ctx = static_cast<callback_context*>(arg);
252
253
254
      multiple_size_pool* p = static_cast<multiple_size_pool*>(ctx->pool);

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

257
      void* mem = p->allocate(sizeof(spins_compressed_state)
258
                              - sizeof(spins_compressed_state::vars)
259
                              + sizeof(int) * csize);
260
      spins_compressed_state* out = new(mem) spins_compressed_state(csize, p);
261
      memcpy(out->vars, ctx->compressed, csize * sizeof(int));
262
      out->compute_hash();
263
      ctx->transitions.emplace_back(out);
264
265
    }

266
267
268
    ////////////////////////////////////////////////////////////////////////
    // SUCC_ITERATOR

269
    class spins_succ_iterator final: public kripke_succ_iterator
270
271
272
    {
    public:

273
      spins_succ_iterator(const callback_context* cc,
274
275
                         bdd cond)
        : kripke_succ_iterator(cond), cc_(cc)
276
277
278
      {
      }

279
280
      void recycle(const callback_context* cc, bdd cond)
      {
281
282
283
        delete cc_;
        cc_ = cc;
        kripke_succ_iterator::recycle(cond);
284
285
      }

286
      ~spins_succ_iterator()
287
      {
288
        delete cc_;
289
290
      }

291
      virtual bool first() override
292
      {
293
294
        it_ = cc_->transitions.begin();
        return it_ != cc_->transitions.end();
295
296
      }

297
      virtual bool next() override
298
      {
299
300
        ++it_;
        return it_ != cc_->transitions.end();
301
302
      }

303
      virtual bool done() const override
304
      {
305
        return it_ == cc_->transitions.end();
306
307
      }

308
      virtual state* dst() const override
309
      {
310
        return (*it_)->clone();
311
312
313
314
315
316
317
      }

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

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,
329
                   // else its negation
330
331
332
    };
    typedef std::vector<one_prop> prop_set;

333
334
335
336
337
338
339
340

    struct var_info
    {
      int num;
      int type;
    };


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

351
      int state_size = d->get_state_size();
352
353
354
      typedef std::map<std::string, var_info> val_map_t;
      val_map_t val_map;

355
      for (int i = 0; i < state_size; ++i)
356
357
358
359
360
361
        {
          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;
        }
362

363
      int type_count = d->get_type_count();
364
365
366
      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)
367
368
369
370
371
        {
          int enum_count = d->get_type_value_count(i);
          for (int j = 0; j < enum_count; ++j)
            enum_map[i].emplace(d->get_type_value_name(i, j), j);
        }
372

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
373
      for (atomic_prop_set::const_iterator ap = aps->begin();
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
           ap != aps->end(); ++ap)
        {
          if (*ap == dead)
            continue;

          const std::string& str = ap->ap_name();
          const char* s = str.c_str();

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


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

              if (*s == ' ' || *s == '\t')
                ++s;
              else
                {
                  if (*s == '.')
                    lastdot = name_p;
                  *name_p++ = *s++;
                }
            }
          *name_p = 0;

          if (name == name_p)
            {
              err << "Proposition `" << str << "' cannot be parsed.\n";
              free(name);
              ++errors;
              continue;
            }

          // Lookup the name
          val_map_t::const_iterator ni = val_map.find(name);
          if (ni == val_map.end())
            {
              // 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())
                {
                  err << "No variable `" << name
                      << "' found in model (for proposition `"
                      << str << "').\n";
                  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())
                {
                  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';

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

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

              // Record that X.Y must be equal to Z.
              int v = dict->register_proposition(*ap, d.get());
              one_prop p = { ni->second.num, OP_EQ, ei->second, v };
473
              out.emplace_back(p);
474
475
476
477
478
479
480
481
482
483
              free(name);
              continue;
            }

          int var_num = ni->second.num;

          if (!*s)                // No operator?  Assume "!= 0".
            {
              int v = dict->register_proposition(*ap, d);
              one_prop p = { var_num, OP_NE, 0, v };
484
              out.emplace_back(p);
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
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
              free(name);
              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] == '=')
                {
                  op = OP_GE;
                  s += 2;
                }
              else
                {
                  op = OP_GT;
                  ++s;
                }
              break;
            default:
            report_error:
              err << "Unexpected `" << s
                  << "' while parsing atomic proposition `" << str
                  << "'.\n";
              ++errors;
              free(name);
              continue;
            }

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

          int val = 0; // Initialize to kill a warning from old compilers.
          int type_num = ni->second.type;
          if (type_num == 0 || (*s >= '0' && *s <= '9') || *s == '-')
            {
              char* s_end;
              val = strtol(s, &s_end, 10);
              if (s == s_end)
                {
                  err << "Failed to parse `" << s << "' as an integer.\n";
                  ++errors;
                  free(name);
                  continue;
                }
              s = s_end;
            }
          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())
                {
                  err << "No state `" << st << "' known for variable `"
                      << name << "'.\n";
                  err << "Possible states are:";
                  for (ei = enum_map[type_num].begin();
                       ei != enum_map[type_num].end(); ++ei)
                    err << ' ' << ei->first;
                  err << '\n';

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

          free(name);

          while (*s && (*s == ' ' || *s == '\t'))
            ++s;
          if (*s)
            {
              err << "Unexpected `" << s
                  << "' while parsing atomic proposition `" << str
                  << "'.\n";
              ++errors;
              continue;
            }


          int v = dict->register_proposition(*ap, d);
          one_prop p = { var_num, op, val, v };
602
          out.emplace_back(p);
603
        }
604

605
      if (errors)
606
        throw std::runtime_error(err.str());
607
608
    }

609
610
611
    ////////////////////////////////////////////////////////////////////////
    // KRIPKE

612
    class spins_kripke final: public kripke
613
614
615
    {
    public:

616
      spins_kripke(spins_interface_ptr d, const bdd_dict_ptr& dict,
617
618
619
620
621
622
623
624
625
626
627
628
629
630
                   const spot::prop_set* ps, formula dead,
                   int compress)
        : kripke(dict),
          d_(d),
          state_size_(d_->get_state_size()),
          ps_(ps),
          compress_(compress == 0 ? nullptr
                    : compress == 1 ? int_array_array_compress
                    : int_array_array_compress2),
          decompress_(compress == 0 ? nullptr
                      : compress == 1 ? int_array_array_decompress
                      : int_array_array_decompress2),
          uncompressed_(compress ? new int[state_size_ + 30] : nullptr),
          compressed_(compress ? new int[state_size_ * 2] : nullptr),
631
632
633
634
635
          statepool_(compress ?
                     (sizeof(spins_compressed_state)
                      - sizeof(spins_compressed_state::vars)) :
                     (sizeof(spins_state) - sizeof(spins_state::vars)
                      + (state_size_ * sizeof(int)))),
636
637
          state_condition_last_state_(nullptr),
          state_condition_last_cc_(nullptr)
638
      {
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
        vname_ = new const char*[state_size_];
        format_filter_ = new bool[state_size_];
        for (int i = 0; i < state_size_; ++i)
          {
            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] =
              (d->get_type_value_count(type) != 1);
          }

        // 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.
        if (dead.is_ff())
          {
            alive_prop = bddtrue;
            dead_prop = bddfalse;
          }
        else if (dead.is_tt())
          {
            alive_prop = bddtrue;
            dead_prop = bddtrue;
          }
        else
          {
            int var = dict->register_proposition(dead, d_);
            dead_prop = bdd_ithvar(var);
            alive_prop = bdd_nithvar(var);
          }
681
682
      }

683
      ~spins_kripke()
684
      {
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
        if (iter_cache_)
          {
            delete iter_cache_;
            iter_cache_ = nullptr;
          }
        delete[] format_filter_;
        delete[] vname_;
        if (compress_)
          {
            delete[] uncompressed_;
            delete[] compressed_;
          }
        dict_->unregister_all_my_variables(d_.get());

        delete ps_;

        if (state_condition_last_state_)
          state_condition_last_state_->destroy();
        delete state_condition_last_cc_; // Might be 0 already.
704
705
      }

706
      virtual state* get_init_state() const override
707
      {
708
709
710
711
712
713
714
715
716
        if (compress_)
          {
            d_->get_initial_state(uncompressed_);
            size_t csize = state_size_ * 2;
            compress_(uncompressed_, state_size_, compressed_, csize);

            multiple_size_pool* p =
              const_cast<multiple_size_pool*>(&compstatepool_);
            void* mem = p->allocate(sizeof(spins_compressed_state)
717
                                    - sizeof(spins_compressed_state::vars)
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
                                    + sizeof(int) * csize);
            spins_compressed_state* res = new(mem)
              spins_compressed_state(csize, p);
            memcpy(res->vars, compressed_, csize * sizeof(int));
            res->compute_hash();
            return res;
          }
        else
          {
            fixed_size_pool* p = const_cast<fixed_size_pool*>(&statepool_);
            spins_state* res = new(p->allocate()) spins_state(state_size_, p);
            d_->get_initial_state(res->vars);
            res->compute_hash();
            return res;
          }
733
734
      }

735
      bdd
736
      compute_state_condition_aux(const int* vars) const
737
      {
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
        bdd res = bddtrue;
        for (auto& i: *ps_)
          {
            int l = vars[i.var_num];
            int r = i.val;

            bool cond = false;
            switch (i.op)
              {
              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;
              }

            if (cond)
              res &= bdd_ithvar(i.bddvar);
            else
              res &= bdd_nithvar(i.bddvar);
          }
        return res;
773
774
      }

775
776
      callback_context* build_cc(const int* vars, int& t) const
      {
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
        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_));
        cc->compress = compress_;
        cc->compressed = compressed_;
        t = d_->get_successors(nullptr, const_cast<int*>(vars),
                               compress_
                               ? transition_callback_compress
                               : transition_callback,
                               cc);
        assert((unsigned)t == cc->transitions.size());
        return cc;
792
793
      }

794
795
796
      bdd
      compute_state_condition(const state* st) const
      {
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
        // 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.
            state_condition_last_cc_ = nullptr;
          }

        const int* vars = get_vars(st);

        bdd res = compute_state_condition_aux(vars);
        int t;
        callback_context* cc = build_cc(vars, t);

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

            // Add a self-loop to dead-states if we care about these.
            if (res != bddfalse)
824
              cc->transitions.emplace_back(st->clone());
825
826
827
828
829
830
831
          }

        state_condition_last_cc_ = cc;
        state_condition_last_cond_ = res;
        state_condition_last_state_ = st->clone();

        return res;
832
833
      }

834
835
836
      const int*
      get_vars(const state* st) const
      {
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
        const int* vars;
        if (compress_)
          {
            const spins_compressed_state* s =
              down_cast<const spins_compressed_state*>(st);

            decompress_(s->vars, s->size, uncompressed_, state_size_);
            vars = uncompressed_;
          }
        else
          {
            const spins_state* s = down_cast<const spins_state*>(st);
            vars = s->vars;
          }
        return vars;
852
853
854
      }


855
      virtual
856
      spins_succ_iterator* succ_iter(const state* st) const override
857
      {
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
        // This may also compute successors in state_condition_last_cc
        bdd scond = compute_state_condition(st);

        callback_context* cc;
        if (state_condition_last_cc_)
          {
            cc = state_condition_last_cc_;
            state_condition_last_cc_ = nullptr; // Now owned by the iterator.
          }
        else
          {
            int t;
            cc = build_cc(get_vars(st), t);

            // Add a self-loop to dead-states if we care about these.
            if (t == 0 && scond != bddfalse)
874
              cc->transitions.emplace_back(st->clone());
875
876
877
878
879
880
881
882
883
884
885
          }

        if (iter_cache_)
          {
            spins_succ_iterator* it =
              down_cast<spins_succ_iterator*>(iter_cache_);
            it->recycle(cc, scond);
            iter_cache_ = nullptr;
            return it;
          }
        return new spins_succ_iterator(cc, scond);
886
887
888
      }

      virtual
889
      bdd state_condition(const state* st) const override
890
      {
891
        return compute_state_condition(st);
892
893
894
      }

      virtual
895
      std::string format_state(const state *st) const override
896
      {
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
        const int* vars = get_vars(st);

        std::stringstream res;

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

        int i = 0;
        for (;;)
          {
            if (!format_filter_[i])
              {
                ++i;
                if (i == state_size_)
                  break;
                continue;
              }
            res << vname_[i] << '=' << vars[i];
            ++i;
            if (i == state_size_)
              break;
            res << ", ";
          }
        return res.str();
921
922
923
      }

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

938
939
940
941
942
      // 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.
943
      mutable const state* state_condition_last_state_;
944
945
      mutable bdd state_condition_last_cond_;
      mutable callback_context* state_condition_last_cc_;
946
947
948
    };


949
950
    //////////////////////////////////////////////////////////////////////////
    // LOADER
951

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

960
961
962
963
964
965
      if (ext == ".gal")
        {
          command = "gal2c " + filename;
          compiled_ext = "2C";
        }
      else if (ext == ".prom" || ext == ".pm" || ext == ".pml")
966
967
968
969
        {
          command = "spins " + filename;
          compiled_ext = ".spins";
        }
970
      else if (ext == ".dve")
971
972
        {
          command = "divine compile --ltsmin " + filename;
Etienne Renault's avatar
Etienne Renault committed
973
          command += " 2> /dev/null"; // FIXME needed for Clang on MacOSX
974
975
          compiled_ext = "2C";
        }
976
      else
977
978
979
        {
          throw std::runtime_error(std::string("Unknown extension '")
                                   + ext + "'.  Use '.prom', '.pm', '.pml', "
980
981
                                   "'.dve', '.dve2C', '.gal', '.gal2C' or "
                                   "'.prom.spins'.");
982
        }
983

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

988
      filename += compiled_ext;
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)
994
        filename = "./" + filename.substr(pos + 1);
995

996
997
      struct stat d;
      if (stat(filename.c_str(), &d) == 0)
998
        if (s.st_mtime < d.st_mtime)
999
          // The .spins or .dve2C or .gal2C is up-to-date, no need to compile.
1000
          return;
1001

1002
1003
      int res = system(command.c_str());
      if (res)
1004
1005
1006
        throw std::runtime_error(std::string("Execution of '")
                                 + command.c_str() + "' returned exit code "
                                 + std::to_string(WEXITSTATUS(res)));
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" && ext != ".gal2C")
1021
1022
1023
1024
      {
        compile_model(file, ext);
        ext = file.substr(file.find_last_of("."));
      }
1025

1026
    if (lt_dlinit())
1027
      throw std::runtime_error("Failed to initialize libltldl.");
1028
1029
1030
1031

    lt_dlhandle h = lt_dlopen(file.c_str());
    if (!h)
      {
1032
        std::string lt_error = lt_dlerror();
1033
1034
        lt_dlexit();
        throw std::runtime_error(std::string("Failed to load '")
1035
                                 + file + "'.\n" + lt_error);
1036
1037
      }

1038
    auto d = std::make_shared<spins_interface>();
1039
1040
    assert(d); // Superfluous, but Debian's GCC 7 snapshot 20161207-1 warns
               // about potential null pointer dereference on the next line.
1041
1042
    d->handle = h;

1043

1044
    auto sym = [&](auto* dst, const char* name)
1045
      {
1046
1047
1048
        // Work around -Wpendantic complaining that pointer-to-objects
        // should not be converted to pointer-to-functions (we have to
        // assume they can for POSIX).
1049
1050
        *reinterpret_cast<void**>(dst) = lt_dlsym(h, name);
        if (dst == nullptr)
1051
1052
1053
1054
          throw std::runtime_error(std::string("Failed to resolve symbol '")
                                   + name + "' in '" + file + "'.");
      };

1055
    // SpinS interface.
1056
    if (ext == ".spins")
1057
      {
1058
        sym(&d->get_initial_state, "spins_get_initial_state");
1059
        d->have_property = nullptr;
1060
1061
1062
1063
1064
1065
1066
1067
        sym(&d->get_successors, "spins_get_successor_all");
        sym(&d->get_state_size, "spins_get_state_size");
        sym(&d->get_state_variable_name, "spins_get_state_variable_name");
        sym(&d->get_state_variable_type, "spins_get_state_variable_type");
        sym(&d->get_type_count, "spins_get_type_count");
        sym(&d->get_type_name, "spins_get_type_name");
        sym(&d->get_type_value_count, "spins_get_type_value_count");
        sym(&d->get_type_value_name, "spins_get_type_value_name");
1068
      }
1069
    // dve2 and gal2C interfaces.
1070
1071
    else
      {
1072
        sym(&d->get_initial_state, "get_initial_state");
1073
        *reinterpret_cast<void**>(&d->have_property) =
1074
          lt_dlsym(h, "have_property");
1075
1076
1077
1078
1079
1080
1081
1082
        sym(&d->get_successors, "get_successors");
        sym(&d->get_state_size, "get_state_variable_count");
        sym(&d->get_state_variable_name, "get_state_variable_name");
        sym(&d->get_state_variable_type, "get_state_variable_type");
        sym(&d->get_type_count, "get_state_variable_type_count");
        sym(&d->get_type_name, "get_state_variable_type_name");
        sym(&d->get_type_value_count, "get_state_variable_type_value_count");
        sym(&d->get_type_value_name, "get_state_variable_type_value");
1083
1084
1085
      }

    if (d->have_property && d->have_property())
1086
      throw std::runtime_error("Models with embedded properties "
1087
                               "are not supported.");
1088

1089
1090
1091
    return { d };
  }

Etienne Renault's avatar
Etienne Renault committed
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
  ////////////////////////////////////////////////////////////////////////
  // CSpins comparison functions & definitions


  struct cspins_state_equal
  {
    bool
    operator()(const cspins_state lhs,
               const cspins_state rhs) const
    {
      return 0 == memcmp(lhs, rhs, (2+rhs[1])* sizeof(int));
    }
  };

  struct cspins_state_hash
  {
    size_t
    operator()(const cspins_state that) const
    {
      return that[0];
    }
  };

1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
  struct both
  {
    cspins_state first;
    int second;
  };

  struct cspins_state_hasher
  {
    cspins_state_hasher(cspins_state&)
    { }

    cspins_state_hasher() = default;

    brick::hash::hash128_t
    hash(cspins_state t) const
    {
      // FIXME we should compute a better hash value for this particular
      // case. Shall we use two differents hash functions?
      return std::make_pair(t[0], t[0]);
    }
Etienne Renault's avatar
Etienne Renault committed
1135

1136
1137
1138
1139
1140
    bool equal(cspins_state lhs, cspins_state rhs) const
    {
      return 0 == memcmp(lhs, rhs, (2+rhs[1])* sizeof(int));
    }
  };
Etienne Renault's avatar
Etienne Renault committed
1141

1142
1143
1144
  //brick::hashset::FastConcurrent<both , both_hasher> ht2;
  typedef brick::hashset::FastConcurrent<cspins_state,
					 cspins_state_hasher>  cspins_state_map;
Etienne Renault's avatar
Etienne Renault committed
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278

  ////////////////////////////////////////////////////////////////////////
  // A manager for Cspins states.

  class cspins_state_manager final
  {
  public:
    cspins_state_manager(unsigned int state_size,
                        int compress)
      : p_((state_size+2)*sizeof(int)), compress_(compress),
      /* reserve one integer for the hash value and size */
      state_size_(state_size),
      fn_compress_(compress == 0 ? nullptr
                   : compress == 1 ? int_array_array_compress
                   : int_array_array_compress2),
      fn_decompress_(compress == 0 ? nullptr
                     : compress == 1 ? int_array_array_decompress
                     : int_array_array_decompress2)
        { }

    int* unbox_state(cspins_state s) const
    {
      return s+2;
    }

    // cmp is the area we can use to compute the compressed rep of dst.
    cspins_state alloc_setup(int *dst, int* cmp, size_t cmpsize)
    {
      cspins_state out = nullptr;
      size_t size = state_size_;
      int* ref = dst;
      if (compress_)
        {
          size_t csize = cmpsize;
          fn_compress_(dst, state_size_, cmp, csize);
          ref = cmp;
          size = csize;
          out = (cspins_state) msp_.allocate((size+2)*sizeof(int));
        }
      else
        out = (cspins_state) p_.allocate();
      int hash_value = 0;
      memcpy(unbox_state(out), ref, size * sizeof(int));
      for (unsigned int i = 0; i < state_size_; ++i)
        hash_value = wang32_hash(hash_value ^ dst[i]);
      out[0] = hash_value;
      out[1] = size;
      return out;
    }

    void decompress(cspins_state s, int* uncompressed, unsigned size) const
    {
      fn_decompress_(s+2, s[1], uncompressed, size);
    }

    void  dealloc(cspins_state s)
    {
      if (compress_)
  	msp_.deallocate(s, (s[1]+2)*sizeof(int));
      else
	p_.deallocate(s);
    }

    unsigned int size() const
    {
      return state_size_;
    }

  private:
    fixed_size_pool p_;
    multiple_size_pool msp_;
    bool compress_;
    const unsigned int state_size_;
    void (*fn_compress_)(const int*, size_t, int*, size_t&);
    void (*fn_decompress_)(const int*, size_t, int*, size_t);
  };


  ////////////////////////////////////////////////////////////////////////
  // Iterator over Cspins states

  // This structure is used as a parameter during callback when
  // generating states from the shared librarie produced by LTSmin
  struct inner_callback_parameters
  {
    cspins_state_manager* manager;   // The state manager
    std::vector<cspins_state>* succ; // The successors of a state
    cspins_state_map* map;
    int* compressed_;
    int* uncompressed_;
    int default_value_;
    bool compress;
    bool selfloopize;
  };

  // This class provides an iterator over the successors of a state.
  // All successors are computed once when an iterator is recycled or
  // created.
  class cspins_iterator final
  {
  public:
    cspins_iterator(cspins_state s,
		   const spot::spins_interface* d,
		   cspins_state_manager& manager,
		   cspins_state_map& map,
		   inner_callback_parameters& inner,
		   int defvalue,
		   cube cond,
		   bool compress,
		   bool selfloopize,
		   cubeset& cubeset, int dead_idx)
      :  current_(0), cond_(cond)
    {
      successors_.reserve(10);
      inner.manager = &manager;
      inner.map = &map;
      inner.succ = &successors_;
      inner.default_value_ = defvalue;
      inner.compress = compress;
      inner.selfloopize = selfloopize;
      int* ref = s;

      if (compress)
	// already filled by compute_condition
	ref = inner.uncompressed_;

      int n = d->get_successors
	(nullptr, manager.unbox_state(ref),
	 [](void* arg, transition_info_t*, int *dst){
	  inner_callback_parameters* inner =
	  static_cast<inner_callback_parameters*>(arg);
	  cspins_state s =
	  inner->manager->alloc_setup(dst, inner->compressed_,
				      inner->manager->size() * 2);
1279
1280
1281
1282
	  auto it = inner->map->insert({s});
	  inner->succ->push_back(*it);
	  if (!it.isnew())
	    inner->manager->dealloc(s);
Etienne Renault's avatar
Etienne Renault committed
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
	},
	 &inner);
      if (!n && selfloopize)
	{
	  successors_.push_back(s);
	  if (dead_idx != -1)
	    cubeset.set_true_var(cond, dead_idx);
	}
    }

    void recycle(cspins_state s,
  		 const spot::spins_interface* d,
  		 cspins_state_manager& manager,
  		 cspins_state_map& map,
		 inner_callback_parameters& inner,
		 int defvalue,
		 cube cond,
		 bool compress,
		 bool selfloopize,
		 cubeset& cubeset, int dead_idx)
    {
      cond_ = cond;
      current_ = 0;
      // Constant time since int* is is_trivially_destructible
      successors_.clear();
      inner.manager = &manager;
      inner.succ = &successors_;
      inner.map = &map;
      inner.default_value_ = defvalue;
      inner.compress = compress;
      inner.selfloopize = selfloopize;
      int* ref  = s;

      if (compress)
	// Already filled by compute_condition
	ref = inner.uncompressed_;

      int n = d->get_successors
	(nullptr, manager.unbox_state(ref),
	 [](void* arg, transition_info_t*, int *dst){
	  inner_callback_parameters* inner =
	  static_cast<inner_callback_parameters*>(arg);
	  cspins_state s =
	  inner->manager->alloc_setup(dst, inner->compressed_,
				      inner->manager->size() * 2);
1328
1329
1330
	  auto it = inner->map->insert({s});
	  inner->succ->push_back(*it);
	  if (!it.isnew())
Etienne Renault's avatar
Etienne Renault committed
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
	    inner->manager->dealloc(s);
	},
	 &inner);
      if (!n && selfloopize)
	{
	  successors_.push_back(s);
	  if (dead_idx != -1)
	    cubeset.set_true_var(cond, dead_idx);
	}
    }

    ~cspins_iterator()
      {
	// Do not release successors states, the manager
	// will do it on time.
      }

    void next()
    {
      ++current_;
    }

    bool done() const
    {
      return current_ >= successors_.size();
    }

    cspins_state state() const
    {
      return successors_[current_];
    }

    cube condition() const
    {
      return cond_;
    }

  private:
    std::vector<cspins_state> successors_;
    unsigned int current_;
    cube cond_;
  };

  ////////////////////////////////////////////////////////////////////////
  // Concrete definition of the system

  // A specialisation of the template class kripke
  template<>
  class kripkecube<cspins_state, cspins_iterator> final
  {

    typedef enum {
      OP_EQ_VAR, OP_NE_VAR, OP_LT_VAR, OP_GT_VAR, OP_LE_VAR, OP_GE_VAR,
      VAR_OP_EQ, VAR_OP_NE, VAR_OP_LT, VAR_OP_GT, VAR_OP_LE, VAR_OP_GE,
      VAR_OP_EQ_VAR, VAR_OP_NE_VAR, VAR_OP_LT_VAR,
      VAR_OP_GT_VAR, VAR_OP_LE_VAR, VAR_OP_GE_VAR, VAR_DEAD
    } relop;

    // Structure for complex atomic proposition
    struct one_prop
    {
      int lval;
      relop op;
      int rval;
    };

    // Data structure to store complex atomic propositions
    typedef std::vector<one_prop> prop_set;
    prop_set pset_;

  public:
    kripkecube(spins_interface_ptr sip, bool compress,
               std::vector<std::string> visible_aps,
               bool selfloopize, std::string dead_prop)
      : sip_(sip), d_(sip.get()), manager_(d_->get_state_size(), compress),
      compress_(compress), cubeset_(visible_aps.size()),
      selfloopize_(selfloopize), aps_(visible_aps)
    {
1409
      map_.setSize(2000000);
Etienne Renault's avatar
Etienne Renault committed
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509