lbtt.cc 3.88 KB
Newer Older
1
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

22
#include "lbtt.hh"
23
24
#include <map>
#include <string>
25
#include <ostream>
26
27
#include <sstream>
#include "tgba/bddprint.hh"
28
#include "reachiter.hh"
29
#include "misc/bddlt.hh"
30
31
32

namespace spot
{
33
34
35
  // At some point we'll need to print an acceptance set into LBTT's
  // format.  LBTT expects numbered acceptance sets, so first we'll
  // number each acceptance condition, and latter when we have to print
36
  // them we'll just have to look up each of them.
37
  class acceptance_cond_splitter
38
39
  {
  public:
40
    acceptance_cond_splitter(bdd all_acc)
41
42
43
44
45
    {
      unsigned count = 0;
      while (all_acc != bddfalse)
	{
	  bdd acc = bdd_satone(all_acc);
46
	  all_acc -= acc;
47
48
49
50
51
52
53
54
55
56
	  sm[acc] = count++;
	}
    }

    std::ostream&
    split(std::ostream& os, bdd b)
    {
      while (b != bddfalse)
	{
	  bdd acc = bdd_satone(b);
57
	  b -= acc;
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
	  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
78
  bdd_to_lbtt(bdd b, const bdd_dict* d)
79
80
81
82
83
84
85
86
  {
    if (b == bddfalse)
      return "f";
    else if (b == bddtrue)
      return "t";
    else
      {
	bdd cube = bdd_satone(b);
87
	b -= cube;
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
	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);
	  }
      }

  }

103
  class lbtt_bfs : public tgba_reachable_iterator_breadth_first
104
105
  {
  public:
106
107
108
109
110
111
    lbtt_bfs(const tgba* a, std::ostream& os)
      : tgba_reachable_iterator_breadth_first(a),
	os_(os),
	acc_count_(0),
	acs_(a->all_acceptance_conditions())

112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
    {
      // Count the number of acceptance_conditions.
      bdd all = a->all_acceptance_conditions();
      while (all != bddfalse)
	{
	  bdd one = bdd_satone(all);
	  all -= one;
	  ++acc_count_;
	}
    }

    void
    process_state(const state*, int n, tgba_succ_iterator*)
    {
      --n;
      if (n == 0)
128
	body_ << "0 1" << std::endl;
129
      else
130
	body_ << "-1" << std::endl << n << " 0" << std::endl;
131
132
133
134
135
    }

    void
    process_link(int, int out, const tgba_succ_iterator* si)
    {
136
137
138
139
      body_ << out - 1 << " ";
      acs_.split(body_, si->current_acceptance_conditions());
      body_ << "-1 " << bdd_to_lbtt(si->current_condition(),
				    automata_->get_dict()) << std::endl;
140
141
142
143
144
    }

    void
    end()
    {
145
      os_ << seen.size() << " " << acc_count_ << "t" << std::endl
146
147
148
149
150
151
152
	  << body_.str() << "-1" << std::endl;
    }

  private:
    std::ostream& os_;
    std::ostringstream body_;
    unsigned acc_count_;
153
    acceptance_cond_splitter acs_;
154
155
156
157
  };


  std::ostream&
158
  lbtt_reachable(std::ostream& os, const tgba* g)
159
  {
160
    lbtt_bfs b(g, os);
161
162
163
164
165
    b.run();
    return os;
  }


166
}