neverclaim.cc 5.35 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2012, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
5
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
6
7
8
9
10
11
// 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
12
// the Free Software Foundation; either version 3 of the License, or
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/>.
22

23
#include <ostream>
24
25
#include <sstream>
#include "bdd.h"
26
#include "tgba/tgbagraph.hh"
27
28
29
30
31
32
33
34
#include "neverclaim.hh"
#include "tgba/bddprint.hh"
#include "reachiter.hh"
#include "ltlvisit/tostring.hh"
#include "tgba/formula2bdd.hh"

namespace spot
{
35
  namespace
36
  {
37
    class never_claim_bfs : public tgba_reachable_iterator_breadth_first
38
    {
39
    public:
40
      never_claim_bfs(const tgba* a, std::ostream& os,
41
		      const ltl::formula* f, bool comments)
42
	: tgba_reachable_iterator_breadth_first(a),
43
	  os_(os), f_(f), accept_all_(-1), fi_needed_(false),
44
	  comments_(comments), all_acc_conds_(a->all_acceptance_conditions()),
45
	  sba_(dynamic_cast<const tgba_digraph*>(a))
46
      {
47
	assert(!sba_ || sba_->get_bprop(tgba_digraph::StateBasedAcc));
48
      }
49

50
51
52
53
54
55
56
57
58
59
      void
      start()
      {
	os_ << "never {";
	if (f_)
	  {
	    os_ << " /* ";
	    to_string(f_, os_);
	    os_ << " */";
	  }
60
	os_ << '\n';
61
	init_ = aut_->get_init_state();
62
      }
63

64
65
66
67
      void
      end()
      {
	if (fi_needed_)
68
	  os_ << "  fi;\n";
69
	if (accept_all_ != -1)
70
	  os_ << "accept_all:\n  skip\n";
71
	os_ << '}' << std::endl;
72
	init_->destroy();
73
      }
74

75
76
77
      bool
      state_is_accepting(const state *s)
      {
78
79
80
81
	// If the automaton is a SBA, it's easier to just query the
	// state_is_accepting() method.
	if (sba_)
	  return sba_->state_is_accepting(s);
82
83
84
85
86
87
88

	// 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.
89
	tgba_succ_iterator* it = aut_->succ_iter(s);
90
	bool accepting =
91
	  it->first() && it->current_acceptance_conditions() == all_acc_conds_;
92
	aut_->release_iter(it);
93
	return accepting;
94
      }
95

96
97
98
99
100
101
102
103
104
105
106
107
108
109
      std::string
      get_state_label(const state* s, int n)
      {
	std::string label;
	if (s->compare(init_) == 0)
	  if (state_is_accepting(s))
	    label = "accept_init";
	  else
	    label = "T0_init";
	else
	  {
	    std::ostringstream ost;
	    ost << n;
	    std::string ns(ost.str());
110

111
112
	    if (state_is_accepting(s))
	      {
113
		tgba_succ_iterator* it = aut_->succ_iter(s);
114
		if (!it->first())
115
116
117
118
119
120
121
122
123
		  label = "accept_S" + ns;
		else
		  {
		    state* current = it->current_state();
		    if (it->current_condition() != bddtrue
			|| s->compare(current) != 0)
		      label = "accept_S" + ns;
		    else
		      label = "accept_all";
124
		    current->destroy();
125
		  }
126
		aut_->release_iter(it);
127
128
129
130
131
132
	      }
	    else
	      label = "T0_S" + ns;
	  }
	  return label;
      }
133

134
135
136
      void
      process_state(const state* s, int n, tgba_succ_iterator*)
      {
137
	tgba_succ_iterator* it = aut_->succ_iter(s);
138
	if (!it->first())
139
140
	  {
	    if (fi_needed_ != 0)
141
	      os_ << "  fi;\n";
142
	    os_ << get_state_label(s, n) << ':';
143
	    if (comments_)
144
	      os_ << " /* " << aut_->format_state(s) << " */";
145
146
	    os_ << "\n  if\n  :: (0) -> goto "
		<< get_state_label(s, n) << '\n';
147
148
149
150
	    fi_needed_ = true;
	  }
	else
	  {
151
	    state* current = it->current_state();
152
153
154
155
156
157
158
159
	    if (state_is_accepting(s)
		&& it->current_condition() == bddtrue
		&& s->compare(init_) != 0
		&& s->compare(current) == 0)
	      accept_all_ = n;
	    else
	      {
		if (fi_needed_)
160
		  os_ << "  fi;\n";
161
		os_ << get_state_label(s, n) << ':';
162
		if (comments_)
163
		  os_ << " /* " << aut_->format_state(s) << " */";
164
		os_ << "\n  if\n";
165
166
		fi_needed_ = true;
	      }
167
	    current->destroy();
168
	  }
169
170
	aut_->release_iter(it);
      }
171

172
      void
173
174
      process_link(const state*, int in, const state*, int out,
		   const tgba_succ_iterator* si)
175
176
177
178
179
      {
	if (in != accept_all_)
	  {
	    os_ << "  :: (";
	    const ltl::formula* f = bdd_to_formula(si->current_condition(),
180
						   aut_->get_dict());
181
	    to_spin_string(f, os_, true);
182
	    f->destroy();
183
	    state* current = si->current_state();
184
	    os_ << ") -> goto " << get_state_label(current, out) << '\n';
185
	    current->destroy();
186
187
	  }
      }
188

189
190
191
192
193
194
    private:
      std::ostream& os_;
      const ltl::formula* f_;
      int accept_all_;
      bool fi_needed_;
      state* init_;
195
      bool comments_;
196
      bdd all_acc_conds_;
197
      const tgba_digraph* sba_;
198
199
    };
  } // anonymous
200
201

  std::ostream&
202
  never_claim_reachable(std::ostream& os, const tgba* g,
203
			const ltl::formula* f, bool comments)
204
  {
205
    assert(g->number_of_acceptance_conditions() <= 1);
206
    never_claim_bfs n(g, os, f, comments);
207
208
209
210
    n.run();
    return os;
  }
}