word.cc 7.32 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
3
// 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
#include "config.h"
21
22
23
#include <spot/twaalgos/word.hh>
#include <spot/twa/bddprint.hh>
#include <spot/twa/bdddict.hh>
24
25
26
#include <spot/tl/parse.hh>
#include <spot/tl/simplify.hh>
#include <spot/tl/apcollect.hh>
27

28
29
using namespace std::string_literals;

30
31
namespace spot
{
32
  twa_word::twa_word(const twa_run_ptr& run) noexcept
33
    : dict_(run->aut->get_dict())
34
  {
35
    for (auto& i: run->prefix)
36
      prefix.emplace_back(i.label);
37
    for (auto& i: run->cycle)
38
      cycle.emplace_back(i.label);
39
    dict_->register_all_variables_of(run->aut, this);
40
41
  }

42
  twa_word::twa_word(const bdd_dict_ptr& dict) noexcept
43
44
45
46
    : dict_(dict)
  {
  }

47
  void
48
  twa_word::simplify()
49
50
51
52
53
54
55
56
57
58
  {
    // If all the formulas on the cycle are compatible, reduce the
    // cycle to a simple conjunction.
    //
    // For instance
    //   !a|!b; b; a&b; cycle{a; b; a&b}
    // can be reduced to
    //   !a|!b; b; a&b; cycle{a&b}
    {
      bdd all = bddtrue;
59
      for (auto& i: cycle)
60
        all &= i;
61
      if (all != bddfalse)
62
63
        {
          cycle.clear();
64
          cycle.emplace_back(all);
65
        }
66
67
68
69
70
71
72
73
74
75
76
    }
    // If the last formula of the prefix is compatible with the
    // last formula of the cycle, we can shift the cycle and
    // reduce the prefix.
    //
    // For instance
    //   !a|!b; b; a&b; cycle{a&b}
    // can be reduced to
    //   !a|!b; cycle{a&b}
    while (!prefix.empty())
      {
77
78
79
80
81
82
        bdd a = prefix.back() & cycle.back();
        if (a == bddfalse)
          break;
        prefix.pop_back();
        cycle.pop_back();
        cycle.push_front(a);
83
84
85
86
87
88
89
      }
    // Get rid of any disjunction.
    //
    // For instance
    //   !a|!b; cycle{a&b}
    // can be reduced to
    //   !a&!b; cycle{a&b}
90
91
92
93
    for (auto& i: prefix)
      i = bdd_satone(i);
    for (auto& i: cycle)
      i = bdd_satone(i);
94
95
96
  }

  std::ostream&
97
  operator<<(std::ostream& os, const twa_word& w)
98
  {
99
100
    if (w.cycle.empty())
      throw std::runtime_error("a twa_word may not have an empty cycle");
101
102
103
    auto d = w.get_dict();
    if (!w.prefix.empty())
      for (auto& i: w.prefix)
104
105
106
107
        {
          bdd_print_formula(os, d, i);
          os << "; ";
        }
108
109
    bool notfirst = false;
    os << "cycle{";
110
    for (auto& i: w.cycle)
111
      {
112
113
114
115
        if (notfirst)
          os << "; ";
        notfirst = true;
        bdd_print_formula(os, d, i);
116
      }
117
    os << '}';
118
119
    return os;
  }
120
121
122
123

  namespace
  {
    static void word_parse_error(const std::string& word,
124
                                 size_t i, parsed_formula pf)
125
126
    {
      std::ostringstream os;
127
      pf.format_errors(os, word, i);
128
129
130
131
      throw parse_error(os.str());
    }

    static void word_parse_error(const std::string& word, size_t i,
132
                                 const std::string& message)
133
134
    {
      if (i == std::string::npos)
135
        i = word.size();
136
137
138
      std::ostringstream s;
      s << ">>> " << word << '\n';
      for (auto j = i + 4; j > 0; --j)
139
        s << ' ';
140
141
142
143
144
145
146
147
148
149
      s << '^' << '\n';
      s << message << '\n';
      throw parse_error(s.str());
    }

    static size_t skip_next_formula(const std::string& word, size_t begin)
    {
      bool quoted = false;
      auto size = word.size();
      for (auto j = begin; j < size; ++j)
150
151
152
153
154
155
156
157
158
        {
          auto c = word[j];
          if (!quoted && (c == ';' || c == '}'))
            return j;
          if (c == '"')
            quoted = !quoted;
          else if (quoted && c == '\\')
            ++j;
        }
159
      if (quoted)
160
        word_parse_error(word, word.size(), "Unclosed string");
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
      return std::string::npos;
    }
  }

  twa_word_ptr parse_word(const std::string& word, const bdd_dict_ptr& dict)
  {
    atomic_prop_set aps;
    tl_simplifier tls(dict);
    twa_word_ptr tw = make_twa_word(dict);
    size_t i = 0;
    auto ind = i;

    auto extract_bdd =
      [&](typename twa_word::seq_t& seq)
      {
176
177
178
179
180
        auto sub = word.substr(i, ind - i);
        auto pf = spot::parse_infix_boolean(sub);
        if (!pf.errors.empty())
          word_parse_error(word, i, pf);
        atomic_prop_collect(pf.f, &aps);
181
        seq.emplace_back(tls.as_bdd(pf.f));
182
183
184
185
186
        if (word[ind] == '}')
          return true;
        // Skip blanks after semi-colon
        i = word.find_first_not_of(' ', ind + 1);
        return false;
187
188
189
      };

    // Parse the prefix part. Can be empty.
190
    while (word.substr(i, 6) != "cycle{"s)
191
      {
192
193
194
195
196
197
198
199
200
201
202
        ind = skip_next_formula(word, i);
        if (ind == std::string::npos)
          word_parse_error(word, word.size(),
                           "A twa_word must contain a cycle");
        if (word[ind] == '}')
          word_parse_error(word, ind, "Expected ';' delimiter: "
                           "'}' stands for ending a cycle");
        // Exract formula, convert it to bdd and add it to the prefix sequence
        extract_bdd(tw->prefix);
        if (i == std::string::npos)
          word_parse_error(word, ind + 1, "Missing cycle in formula");
203
204
205
206
207
      }
    // Consume "cycle{"
    i += 6;
    while (true)
      {
208
209
210
211
212
213
214
215
216
217
218
        ind = skip_next_formula(word, i);
        if (ind == std::string::npos)
          word_parse_error(word, word.size(),
                           "Missing ';' or '}' after formula");
        // Extract formula, convert it to bdd and add it to the cycle sequence
        // Break if an '}' is encountered
        if (extract_bdd(tw->cycle))
          break;
        if (i == std::string::npos)
          word_parse_error(word, ind + 1,
                           "Missing end of cycle character: '}'");
219
220
221
222
223
224
225
226
227
228
229
230
231
      }
    if (ind != word.size() - 1)
      word_parse_error(word, ind + 1, "Input should be finished after cycle");
    for (auto ap: aps)
      dict->register_proposition(ap, tw.get());
    return tw;
  }

  twa_graph_ptr twa_word::as_automaton() const
  {
    twa_graph_ptr aut = make_twa_graph(dict_);

    aut->prop_weak(true);
232
    aut->prop_universal(true);
233

234
235
236
237
    // Register the atomic propositions used in the word.
    {
      bdd support = bddtrue;
      for (auto b: prefix)
238
        support &= bdd_support(b);
239
      for (auto b: cycle)
240
        support &= bdd_support(b);
241
      while (support != bddtrue)
242
243
244
245
246
        {
          int v = bdd_var(support);
          support = bdd_high(support);
          aut->register_ap(dict_->bdd_map[v].f);
        }
247
248
    }

249
250
251
252
    size_t i = 0;
    aut->new_states(prefix.size() + cycle.size());
    for (auto b: prefix)
      {
253
254
        aut->new_edge(i, i + 1, b);
        ++i;
255
256
257
258
259
260
      }
    size_t j = i;
    auto b = cycle.begin();
    auto end = --cycle.end();
    for (; b != end; ++b)
      {
261
262
        aut->new_edge(i, i + 1, *b);
        ++i;
263
264
265
266
267
      }
    // Close the loop
    aut->new_edge(i, j, *b);
    return aut;
  }
268
}