exclusive.cc 5.83 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
//
// 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/>.

20
21
22
23
24
#include <spot/tl/exclusive.hh>
#include <spot/twaalgos/mask.hh>
#include <spot/misc/casts.hh>
#include <spot/misc/minato.hh>
#include <spot/tl/apcollect.hh>
25
26
27
28
29

namespace spot
{
  namespace
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
30
    static const std::vector<formula>
31
32
    split_aps(const char* arg)
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
33
      std::vector<formula> group;
34
35
      auto start = arg;
      while (*start)
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
        {
          while (*start == ' ' || *start == '\t')
            ++start;
          if (!*start)
            break;
          if (*start == ',')
            {
              std::string s = "unexpected ',' in ";
              s += arg;
              throw std::invalid_argument(s);
            }
          if (*start == '"')
            {
              ++start;
              auto end = start;
              while (*end && *end != '"')
                {
                  if (*end == '\\')
                    ++end;
                  ++end;
                }
              if (!*end)
                {
                  std::string s = "missing closing '\"' in ";
                  s += arg;
                  throw std::invalid_argument(s);
                }
              std::string ap(start, end - start);
              group.emplace_back(formula::ap(ap));
              do
                ++end;
              while (*end == ' ' || *end == '\t');
              if (*end && *end != ',')
                {
                  std::string s = "unexpected character '";
                  s += *end;
                  s += "' in ";
                  s += arg;
                  throw std::invalid_argument(s);
                }
              if (*end == ',')
                ++end;
              start = end;
            }
          else
            {
              auto end = start;
              while (*end && *end != ',')
                ++end;
              auto rend = end;
              while (rend > start && (rend[-1] == ' ' || rend[-1] == '\t'))
                --rend;
              std::string ap(start, rend - start);
              group.emplace_back(formula::ap(ap));
              if (*end == ',')
                start = end + 1;
              else
                break;
            }
        }
96
97
98
99
100
101
102
103
104
      return group;
    }
  }

  void exclusive_ap::add_group(const char* ap_csv)
  {
    add_group(split_aps(ap_csv));
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
105
  void exclusive_ap::add_group(std::vector<formula> ap)
106
107
108
109
110
111
  {
    groups.push_back(ap);
  }

  namespace
  {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
112
113
    formula
    nand(formula lhs, formula rhs)
114
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
115
      return formula::Not(formula::And({lhs, rhs}));
116
117
118
    }
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
119
120
  formula
  exclusive_ap::constrain(formula f) const
121
  {
122
    auto* s = atomic_prop_collect(f);
123

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
124
125
    std::vector<formula> group;
    std::vector<formula> v;
126
127
128

    for (auto& g: groups)
      {
129
        group.clear();
130

131
132
133
        for (auto ap: g)
          if (s->find(ap) != s->end())
            group.push_back(ap);
134

135
136
137
138
        unsigned s = group.size();
        for (unsigned j = 0; j < s; ++j)
          for (unsigned k = j + 1; k < s; ++k)
            v.push_back(nand(group[j], group[k]));
139
140
141
      };

    delete s;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
142
    return formula::And({f, formula::G(formula::And(v))});
143
  }
144

145
  twa_graph_ptr exclusive_ap::constrain(const_twa_graph_ptr aut,
146
                                           bool simplify_guards) const
147
148
149
150
151
  {
    // Compute the support of the automaton.
    bdd support = bddtrue;
    {
      std::set<int> bdd_seen;
152
      for (auto& t: aut->edges())
153
154
        if (bdd_seen.insert(t.cond.id()).second)
          support &= bdd_support(t.cond);
155
156
157
158
159
160
161
162
    }

    bdd restrict = bddtrue;
    auto d = aut->get_dict();

    std::vector<bdd> group;
    for (auto& g: groups)
      {
163
164
165
166
167
168
169
170
171
172
173
174
175
        group.clear();

        for (auto ap: g)
          {
            int v = d->has_registered_proposition(ap, aut);
            if (v >= 0)
              group.push_back(bdd_nithvar(v));
          }

        unsigned s = group.size();
        for (unsigned j = 0; j < s; ++j)
          for (unsigned k = j + 1; k < s; ++k)
            restrict &= group[j] | group[k];
176
177
      }

178
    twa_graph_ptr res = make_twa_graph(aut->get_dict());
179
180
181
    res->copy_ap_of(aut);
    res->prop_copy(aut, { true, true, true, true });
    res->copy_acceptance_of(aut);
182
183
    if (simplify_guards)
      {
184
185
186
187
188
189
190
191
192
193
194
195
        transform_accessible(aut, res, [&](unsigned, bdd& cond,
                                           acc_cond::mark_t&, unsigned)
                             {
                               minato_isop isop(cond & restrict,
                                                cond | !restrict,
                                                true);
                               bdd res = bddfalse;
                               bdd cube = bddfalse;
                               while ((cube = isop.next()) != bddfalse)
                                 res |= cube;
                               cond = res;
                             });
196
        res->remove_unused_ap();
197
198
199
      }
    else
      {
200
201
202
203
204
        transform_accessible(aut, res, [&](unsigned, bdd& cond,
                                           acc_cond::mark_t&, unsigned)
                             {
                               cond &= restrict;
                             });
205
      }
206
207
    return res;
  }
208
}