lbtt.cc 3.92 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
4
5
6
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7
8
9
10
11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13
14
15
16
17
18
19
20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23
#include "lbtt.hh"
24
25
#include <map>
#include <string>
26
#include <ostream>
27
#include "tgba/formula2bdd.hh"
28
#include "reachiter.hh"
29
#include "misc/bddlt.hh"
30
#include "priv/accmap.hh"
31
#include "ltlvisit/lbt.hh"
32
#include "ltlparse/public.hh"
33
34
35

namespace spot
{
36
  namespace
37
  {
38
    class lbtt_bfs : public tgba_reachable_iterator_breadth_first
39
    {
40
    public:
41
      lbtt_bfs(const const_tgba_ptr& a, std::ostream& os, bool sba_format)
42
43
	: tgba_reachable_iterator_breadth_first(a),
	  os_(os),
44
	  sba_format_(sba_format),
45
	  sba_(nullptr)
46
      {
47
48
49
50
51
	// Check if the automaton can be converted into a
	// tgba_digraph. This makes the state_is_accepting() function
	// more efficient.
	if (a->is_sba())
	  sba_ = std::dynamic_pointer_cast<const tgba_digraph>(a);
52
53
54
55
      }

      bool
      state_is_accepting(const state *s) const
56
      {
57
58
59
60
61
62
63
64
65
66
67
68
	// If the automaton has a SBA type, it's easier to just query the
	// state_is_accepting() method.
	if (sba_)
	  return sba_->state_is_accepting(s);

	// Otherwise, since we are dealing with a degeneralized
	// automaton nonetheless, the transitions leaving an accepting
	// state are either all accepting, or all non-accepting.  So
	// we just check the acceptance of the first transition.  This
	// is not terribly efficient since we have to create the
	// iterator.
	tgba_succ_iterator* it = aut_->succ_iter(s);
69
	bool accepting = it->first()
70
	  && aut_->acc().accepting(it->current_acceptance_conditions());
71
	aut_->release_iter(it);
72
	return accepting;
73
74
      }

75

76
      void
77
      process_state(const state* s, int n, tgba_succ_iterator*)
78
79
80
      {
	--n;
	if (n == 0)
81
	  body_ << "0 1";
82
	else
83
84
85
86
87
88
89
90
91
92
93
	  body_ << "-1\n" << n << " 0";
	// Do we have state-based acceptance?
	if (sba_format_)
	  {
	    // We support only one acceptance condition in the
	    // state-based format.
	    if (state_is_accepting(s))
	      body_ << " 0 -1";
	    else
	      body_ << " -1";
	  }
94
	body_ << '\n';
95
      }
96

97
      void
98
99
      process_link(const state*, int,
		   const state*, int out, const tgba_succ_iterator* si)
100
      {
101
	body_ << out - 1 << ' ';
102
103
	if (!sba_format_)
	  {
104
105
	    for (auto s: aut_->acc().sets(si->current_acceptance_conditions()))
	      body_ << s << ' ';
106
107
108
109
110
111
	    body_ << "-1 ";
	  }
	const ltl::formula* f = bdd_to_formula(si->current_condition(),
					       aut_->get_dict());
	to_lbt_string(f, body_);
	f->destroy();
112
	body_ << '\n';
113
      }
114

115
116
117
      void
      end()
      {
118
	os_ << seen.size() << ' ';
119
	if (sba_format_)
120
	  os_ << '1';
121
	else
122
	  os_ << aut_->acc().num_sets() << 't';
123
	os_ << '\n' << body_.str() << "-1" << std::endl;
124
125
126
127
128
      }

    private:
      std::ostream& os_;
      std::ostringstream body_;
129
130
      bdd all_acc_conds_;
      bool sba_format_;
131
      const_tgba_digraph_ptr sba_;
132
    };
133
  }
134

135
  std::ostream&
136
  lbtt_reachable(std::ostream& os, const const_tgba_ptr& g, bool sba)
137
  {
138
139
140
141
    if (!g->acc().is_generalized_buchi())
      throw std::runtime_error
	("LBTT only supports generalized Büchi acceptance");

142
    lbtt_bfs b(g, os, sba);
143
144
145
    b.run();
    return os;
  }
146
}