lbtt.cc 5.56 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
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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
#include <map>
#include <set>
#include <string>
#include <sstream>
#include "tgba/tgba.hh"
#include "save.hh"
#include "tgba/bddprint.hh"
#include "ltlvisit/tostring.hh"
#include "tgba/bddprint.hh"

namespace spot
{
  struct bdd_less_than
  {
    bool
    operator()(const bdd& left, const bdd& right) const
    {
      return left.id() < right.id();
    }
  };

  // At some point we'll need to print an accepting set into LBTT's
  // forma.  LBTT expect numbered accepting sets, so first we'll
  // number each accepting condition, and latter when we have to print
  // them we'll just have to look up each of them.
  class accepting_cond_splitter
  {
  public:
    accepting_cond_splitter(bdd all_acc)
    {
      unsigned count = 0;
      while (all_acc != bddfalse)
	{
	  bdd acc = bdd_satone(all_acc);
	  all_acc &= !acc;
	  sm[acc] = count++;
	}
    }

    std::ostream&
    split(std::ostream& os, bdd b)
    {
      while (b != bddfalse)
	{
	  bdd acc = bdd_satone(b);
	  b &= !acc;
	  os << sm[acc] << " ";
	}
      return os;
    }

    unsigned
    count() const
    {
      return sm.size();
    }

  private:
    typedef std::map<bdd, unsigned, bdd_less_than> split_map;
    split_map sm;
  };

  // Convert a BDD formula to the syntax used by LBTT's transition guards.
  // Conjunctions are printed by bdd_format_sat, so we just have
  // to handle the other cases.
  static std::string
  bdd_to_lbtt(bdd b, const tgba_bdd_dict& d)
  {
    if (b == bddfalse)
      return "f";
    else if (b == bddtrue)
      return "t";
    else
      {
	bdd cube = bdd_satone(b);
	b &= !cube;
	if (b != bddfalse)
	  {
	    return "| " + bdd_to_lbtt(b, d) + " " + bdd_to_lbtt(cube, d);
	  }
	else
	  {
	    std::string res = "";
	    for (int count = bdd_nodecount(cube); count > 1; --count)
	      res += "& ";
	    return res + bdd_format_sat(d, cube);
	  }
      }

  }

  // Each state in the produced automata corresponds to
  // a (state, accepting set) pair for the source automata.

  typedef std::pair<state*, bdd> state_acc_pair;

  struct state_acc_pair_less_than
  {
    bool
    operator()(const state_acc_pair& left, const state_acc_pair& right) const
    {
      int cmp = left.first->compare(right.first);
      if (cmp < 0)
	return true;
      if (cmp > 0)
	return false;
      return left.second.id() < right.second.id();
    }
  };

  // Each state of the produced automata is numbered.  Map of state seen.
  typedef std::map<state_acc_pair, unsigned, state_acc_pair_less_than> acp_seen_map;

  // Set of states yet to produce.
  typedef std::set<state_acc_pair, state_acc_pair_less_than> todo_set;

  // Each *source* car correspond to several state in the produced
  // automate.  A minmax_pair specify the range of such associated states.
  typedef std::pair<unsigned, unsigned> minmax_pair;
  typedef std::map<state*, minmax_pair, state_ptr_less_than> seen_map;

  // Take a STATE from the source automata, and fill TODO with
  // the list of associated states to output.  Return the correponding
  // range in MMP.  Update SEEN, ACP_SEEN, and STATE_NUMBER.
  void
  fill_todo(todo_set& todo, seen_map& seen, acp_seen_map& acp_seen,
	    state* state, const tgba& g,
	    minmax_pair& mmp, unsigned& state_number)
  {
    typedef std::set<bdd, bdd_less_than> bdd_set;

    seen_map::iterator i = seen.find(state);
    if (i != seen.end())
      {
	mmp = i->second;
	delete state;
	return;
      }

    // Browse the successors of STATE to gather accepting
    // conditions of outgoing transitions.
    bdd_set acc_seen;
    tgba_succ_iterator* si = g.succ_iter(state);
    for (si->first(); !si->done(); si->next())
      {
	acc_seen.insert(si->current_accepting_conditions());
      }
    mmp.first = state_number;
    for (bdd_set::iterator i = acc_seen.begin(); i != acc_seen.end(); ++i)
      {
	state_acc_pair p(state, *i);
	todo.insert(p);
	acp_seen[p] = state_number++;
      }
    mmp.second = state_number;
    seen[state] = mmp;
  }

  std::ostream&
  lbtt_reachable(std::ostream& os, const tgba& g)
  {
    const tgba_bdd_dict& d = g.get_dict();
    std::ostringstream body;

    seen_map seen;
    acp_seen_map acp_seen;
    todo_set todo;
    unsigned state_number = 0;

    minmax_pair mmp;

    fill_todo(todo, seen, acp_seen,
	      g.get_init_state(), g, mmp, state_number);
    accepting_cond_splitter acs(g.all_accepting_conditions());

    while(! todo.empty())
      {
	state_acc_pair sap = *todo.begin();
	todo.erase(todo.begin());
	unsigned number = acp_seen[sap];

	body << number << " "
	     // Mark the initial state.
	     << ((number >= mmp.first && number < mmp.second) ? 1 : 0) << " ";

	acs.split(body, sap.second);
	body << "-1" << std::endl;

	tgba_succ_iterator* si = g.succ_iter(sap.first);
	for (si->first(); !si->done(); si->next())
	  {
	    // We have put the accepting conditions on the state,
	    // so draw only outgoing transition with these accepting
	    // conditions.
	    if (si->current_accepting_conditions() != sap.second)
	      continue;

	    minmax_pair destrange;
	    fill_todo(todo, seen, acp_seen,
		      si->current_state(), g, destrange, state_number);

	    // Link to all instances of the successor.
	    std::string s = bdd_to_lbtt(si->current_condition(), d);
	    for (unsigned i = destrange.first; i < destrange.second; ++i)
	      {
		body << i << " " << s << " " << "-1" << std::endl;
	      }
	  }
	body << "-1" << std::endl;
	delete si;
      }

    os << state_number << " " << acs.count() << std::endl;
    os << body.str();
    // Finally delete all states used as keys in m:
    for (seen_map::iterator i = seen.begin(); i != seen.end(); ++i)
      delete i->first;
    return os;
  }
}