stutter_invariance.cc 4.38 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
// Copyright (C) 2014 Laboratoire de Recherche et Développement
// de l'Epita.
//
// 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
// the Free Software Foundation; either version 3 of the License, or
// (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
// along with this program.  If not, see <http://www.gnu.org/licenses/>.


#include <iostream>
#include "tgba/tgbagraph.hh"
#include "closure.hh"
#include "stutterize.hh"
#include "ltlvisit/remove_x.hh"
#include "tgbaalgos/translate.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/apcollect.hh"
#include "stutter_invariance.hh"
#include "tgba/tgbasl.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/dupexp.hh"

namespace spot
{
  bool
  is_stutter_invariant(const ltl::formula* f)
    {
      const char* stutter_check = getenv("SPOT_STUTTER_CHECK");
      char algo = stutter_check ? stutter_check[0] : '1';
      if (f->is_ltl_formula() && f->is_X_free())
        return true;

      if (algo == '0')
        {
          // Syntactic checking.
          if (f->is_ltl_formula())
            {
              const ltl::formula* g = remove_x(f);
              ltl::ltl_simplifier ls;
              bool res = ls.are_equivalent(f, g);
              g->destroy();
              return res;
            }
          else
            {
              throw std::runtime_error("Cannot use the syntactic-based " \
                                       "approach to stutter-invariance " \
                                       "checking on non-ltl formula");
            }
        }
      const ltl::formula* nf = ltl::unop::instance(ltl::unop::Not, f->clone());
      translator trans;
Thibaud Michaud's avatar
Thibaud Michaud committed
63
64
      tgba_digraph_ptr aut_f = trans.run(f);
      tgba_digraph_ptr aut_nf = trans.run(nf);
65
66
      bdd aps = atomic_prop_collect_as_bdd(f, aut_f);
      nf->destroy();
Thibaud Michaud's avatar
Thibaud Michaud committed
67
      return is_stutter_invariant(std::move(aut_f), std::move(aut_nf), aps);
68
69
70
    }

  bool
Thibaud Michaud's avatar
Thibaud Michaud committed
71
72
  is_stutter_invariant(tgba_digraph_ptr&& aut_f,
                       tgba_digraph_ptr&& aut_nf, bdd aps)
73
74
75
76
77
78
79
80
81
    {
      const char* stutter_check = getenv("SPOT_STUTTER_CHECK");
      char algo = stutter_check ? stutter_check[0] : '8';

      switch (algo)
        {
          // sl(aut_f) x sl(aut_nf)
        case '1':
            {
Thibaud Michaud's avatar
Thibaud Michaud committed
82
83
              return product(sl(std::move(aut_f), aps),
                             sl(std::move(aut_nf), aps))->is_empty();
84
85
86
87
            }
          // sl(cl(aut_f)) x aut_nf
        case '2':
            {
Thibaud Michaud's avatar
Thibaud Michaud committed
88
89
              return product(sl(closure(std::move(aut_f)), aps),
                             std::move(aut_nf))->is_empty();
90
91
92
93
            }
          // (cl(sl(aut_f)) x aut_nf
        case '3':
            {
Thibaud Michaud's avatar
Thibaud Michaud committed
94
95
              return product(closure(sl(std::move(aut_f), aps)),
                             std::move(aut_nf))->is_empty();
96
97
98
99
            }
          // sl2(aut_f) x sl2(aut_nf)
        case '4':
            {
Thibaud Michaud's avatar
Thibaud Michaud committed
100
101
              return product(sl2(std::move(aut_f), aps),
                             sl2(std::move(aut_nf), aps))->is_empty();
102
103
104
105
            }
          // sl2(cl(aut_f)) x aut_nf
        case '5':
            {
Thibaud Michaud's avatar
Thibaud Michaud committed
106
107
              return product(sl2(closure(std::move(aut_f)), aps),
                             std::move(aut_nf))->is_empty();
108
109
110
111
            }
          // (cl(sl2(aut_f)) x aut_nf
        case '6':
            {
Thibaud Michaud's avatar
Thibaud Michaud committed
112
113
              return product(closure(sl2(std::move(aut_f), aps)),
                             std::move(aut_nf))->is_empty();
114
115
116
117
118
119
120
121
122
123
124
            }
          // on-the-fly sl(aut_f) x sl(aut_nf)
        case '7':
            {
              auto slf = std::make_shared<tgbasl>(aut_f, aps);
              auto slnf = std::make_shared<tgbasl>(aut_nf, aps);
              return product(slf, slnf)->is_empty();
            }
          // cl(aut_f) x cl(aut_nf)
        case '8':
            {
Thibaud Michaud's avatar
Thibaud Michaud committed
125
126
              return product(closure(std::move(aut_f)),
                             closure(std::move(aut_nf)))->is_empty();
127
128
129
130
131
132
133
            }
        default:
          throw std::runtime_error("invalid value for SPOT_STUTTER_CHECK.");
          break;
        }
    }
}