remprop.cc 4.77 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// l'Epita (LRDE).
//
// 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
#include <spot/twaalgos/remprop.hh>
#include <spot/twaalgos/mask.hh>
#include <spot/misc/casts.hh>
23
24
25
26
27
28
29
30
31
32
33
34
35
#include <ctype.h>
#include <sstream>

namespace spot
{
  namespace
  {
    static
    void unexpected_char(const char* arg, const char* pos)
    {
      std::ostringstream out;
      out << "unexpected ";
      if (isprint(*pos))
36
        out << '\'' << *pos << '\'';
37
      else
38
        out << "character";
39
40
41
42
43
44
45
46
47
48
49
50
      out << " at position " << pos - arg << " in '";
      out << arg << '\'';
      throw std::invalid_argument(out.str());
    }
  }


  void remove_ap::add_ap(const char* arg)
  {
    auto start = arg;
    while (*start)
      {
51
52
53
54
55
56
57
        while (*start == ' ' || *start == '\t')
          ++start;
        if (!*start)
          break;
        if (*start == ',' || *start == '=')
          unexpected_char(arg, start);
        formula the_ap = nullptr;
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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
        if (*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);
            the_ap = formula::ap(ap);
            do
              ++end;
            while (*end == ' ' || *end == '\t');
            start = end;
          }
        else
          {
            auto end = start;
            while (*end && *end != ',' && *end != '=')
              ++end;
            auto rend = end;
            while (rend > start && (rend[-1] == ' ' || rend[-1] == '\t'))
              --rend;
            std::string ap(start, rend - start);
            the_ap = formula::ap(ap);
            start = end;
          }
        if (*start)
          {
            if (!(*start == ',' || *start == '='))
              unexpected_char(arg, start);
            if (*start == '=')
              {
                do
                  ++start;
                while (*start == ' ' || *start == '\t');
                if (*start == '0')
                  props_neg.insert(the_ap);
                else if (*start == '1')
                  props_pos.insert(the_ap);
                else
                  unexpected_char(arg, start);
                the_ap = nullptr;
                do
                  ++start;
                while (*start == ' ' || *start == '\t');
              }
            if (*start)
              {
                if (*start != ',')
                  unexpected_char(arg, start);
                ++start;
              }
          }
        if (the_ap)
          props_exist.insert(the_ap);
122
123
124
      }
  }

125
  twa_graph_ptr remove_ap::strip(const_twa_graph_ptr aut) const
126
127
128
129
130
  {
    bdd restrict = bddtrue;
    bdd exist = bddtrue;
    auto d = aut->get_dict();

131
    twa_graph_ptr res = make_twa_graph(d);
132
133
134
135
136
137
    res->copy_ap_of(aut);
    res->prop_copy(aut, { true, true, false, false });
    res->copy_acceptance_of(aut);

    for (auto ap: props_exist)
      {
138
139
140
141
        int v = d->has_registered_proposition(ap, aut);
        if (v >= 0)
          {
            exist &= bdd_ithvar(v);
142
            res->unregister_ap(v);
143
          }
144
145
146
      }
    for (auto ap: props_pos)
      {
147
148
149
150
        int v = d->has_registered_proposition(ap, aut);
        if (v >= 0)
          {
            restrict &= bdd_ithvar(v);
151
            res->unregister_ap(v);
152
          }
153
154
155
      }
    for (auto ap: props_neg)
      {
156
157
158
159
        int v = d->has_registered_proposition(ap, aut);
        if (v >= 0)
          {
            restrict &= bdd_nithvar(v);
160
            res->unregister_ap(v);
161
          }
162
163
164
      }

    transform_accessible(aut, res, [&](unsigned, bdd& cond,
165
                                       acc_cond::mark_t&, unsigned)
166
                         {
167
168
                           cond = bdd_restrict(bdd_exist(cond, exist),
                                               restrict);
169
170
171
172
                         });
    return res;
  }
}