nsa2tgba.cc 5.42 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 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
20
21
22
23
24
//
// 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 <sstream>
#include <deque>
#include "public.hh"
#include "tgbaalgos/sccfilter.hh"
#include "ltlenv/defaultenv.hh"
25
#include "priv/accmap.hh"
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
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

namespace spot
{
  // Christof Löding's Diploma Thesis: Methods for the
  // Transformation of ω-Automata: Complexity and Connection to
  // Second Order Logic.  Section 3.4.3, gives a transition
  // from Streett with |Q| states to BA with |Q|*(4^n-3^n+2)
  // states, if n is the number of acceptance pairs.
  //
  // Duret-Lutz et al. (ATVA'2009): On-the-fly Emptiness Check of
  // Transition-based Streett Automata.  Section 3.3 contains a
  // conversion from transition-based Streett Automata to TGBA using
  // the generalized Büchi acceptance to limit the explosion.  It goes
  // from Streett with |Q| states to (T)GBA with |Q|*(2^n+1) states.
  // However the definition of the number of acceptance sets in that
  // paper is suboptimal: only n are needed, not 2^n.
  //
  // This implements this second version.

  namespace
  {
    // A state in the resulting automaton corresponds is either a
    // state of the original automaton (in which case bv == 0) or a
    // state of the original automaton associated to a set of pending
    // acceptance represented by a bitvect.

    struct build_state
    {
      int s;
      const bitvect* pend;

      build_state(int st, const bitvect* bv = 0):
	s(st),
	pend(bv)
      {
      }
    };

    struct build_state_hash
    {
      size_t
      operator()(const build_state& s) const
      {
	if (!s.pend)
	  return s.s;
	else
	  return s.s ^ s.pend->hash();
      }
    };

    struct build_state_equal
    {
      bool
      operator()(const build_state& left,
                 const build_state& right) const
      {
	if (left.s != right.s)
	  return false;
	if (left.pend == right.pend)
	  return true;
	if (!right.pend || !left.pend)
	  return false;
        return *left.pend == *right.pend;
      }
    };

    // Associate the build state to its number.
93
94
    typedef std::unordered_map<build_state, int,
			       build_state_hash, build_state_equal> bs2num_map;
95
96
97
98
99
100
101
102
103
104

    // Queue of state to be processed.
    typedef std::deque<build_state> queue_t;

  }

  SPOT_API
  tgba* nsa_to_tgba(const dstar_aut* nsa)
  {
    assert(nsa->type == Streett);
105
    tgba_digraph* a = nsa->aut;
106
107
    bdd_dict* dict = a->get_dict();

108
    tgba_digraph* res = new tgba_digraph(dict);
109
110
    dict->register_all_variables_of(a, res);

111
112
113
    // Create accpair_count acceptance sets for the output.
    unsigned npairs = nsa->accpair_count;
    acc_mapper_consecutive_int acc_b(res, npairs);
114
115
116
117
118
119
120

    // These maps make it possible to convert build_state to number
    // and vice-versa.
    bs2num_map bs2num;

    queue_t todo;

121
122
    build_state s(a->get_init_state_number());
    bs2num[s] = res->new_state();
123
124
125
126
127
128
129
130
    todo.push_back(s);

    while (!todo.empty())
      {
        s = todo.front();
        todo.pop_front();
        int src = bs2num[s];

131
	for (auto& t: a->out(s.s))
132
133
134
135
136
137
	  {
	    bitvect* pend = 0;
	    bdd acc = bddfalse;
	    if (s.pend)
	      {
		pend = s.pend->clone();
138
139
		*pend |= nsa->accsets->at(2 * t.dst); // L
		*pend -= nsa->accsets->at(2 * t.dst + 1); // U
140
141
142

		for (size_t i = 0; i < npairs; ++i)
		  if (!pend->get(i))
143
		    acc |= acc_b.lookup(i).second;
144
145
146
	      }


147
	    build_state d(t.dst, pend);
148
149
            // Have we already seen this destination?
            int dest;
150
	    auto dres = bs2num.emplace(d, 0);
151
152
153
154
155
            if (!dres.second)
              {
                dest = dres.first->second;
		delete d.pend;
              }
156
            else		// No, this is a new state
157
              {
158
		dest = dres.first->second = res->new_state();
159
160
                todo.push_back(d);
	      }
161
	    res->new_transition(src, dest, t.cond, acc);
162
163
164
165
166

	    // Jump to level ∅
	    if (s.pend == 0)
	      {
		bitvect* pend = make_bitvect(npairs);
167
		build_state d(t.dst, pend);
168
169
		// Have we already seen this destination?
		int dest;
170
		auto dres = bs2num.emplace(d, 0);
171
172
173
174
175
		if (!dres.second)
		  {
		    dest = dres.first->second;
		    delete d.pend;
		  }
176
		else		// No, this is a new state
177
		  {
178
		    dest = dres.first->second = res->new_state();
179
180
		    todo.push_back(d);
		  }
181
		res->new_transition(src, dest, t.cond);
182
183
184
185
186
187
188
189
190
	      }
	  }
      }


    // {
    //   bs2num_map::iterator i = bs2num.begin();
    //   while (i != bs2num.end())
    // 	{
191
    // 	  std::cerr << i->second << ": (" << i->first.s << ',';
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
    // 	  if (i->first.pend)
    // 	    std::cerr << *i->first.pend << ")\n";
    // 	  else
    // 	    std::cerr << "-)\n";
    // 	  ++i;
    // 	}
    // }

    // Cleanup the bs2num map.
    bs2num_map::iterator i = bs2num.begin();
    while (i != bs2num.end())
      delete (i++)->first.pend;

    return res;
  }

}