neverclaim.cc 5.07 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2009, 2011, 2012, 2014, 2015 Laboratoire de Recherche et
3
// 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 26
#include <sstream>
#include "neverclaim.hh"
#include "tgba/bddprint.hh"
27
#include "tgba/tgbagraph.hh"
28 29 30 31 32 33
#include "reachiter.hh"
#include "ltlvisit/tostring.hh"
#include "tgba/formula2bdd.hh"

namespace spot
{
34
  namespace
35
  {
36
    class never_claim_output
37
    {
38
    public:
39 40
      std::ostream& os_;
      bool opt_comments_ = false;
41
      std::vector<std::string>* sn_ = nullptr;
42
      bool opt_624_ = false;
43 44 45
      const_tgba_digraph_ptr aut_;
      bool fi_needed_ = false;
      bool need_accept_all_ = false;
46
      unsigned accept_all_ = 0;
47 48 49 50

    public:
      never_claim_output(std::ostream& os, const char* options)
	: os_(os)
51
      {
52 53 54 55
	if (options)
	  while (char c = *options++)
	    switch (c)
	      {
56 57 58
	      case '6':
		opt_624_ = true;
		break;
59 60 61 62 63 64 65
	      case 'c':
		opt_comments_ = true;
		break;
	      default:
		throw std::runtime_error
		  (std::string("unknown option for never_claim(): ") + c);
	      }
66
      }
67

68
      void
69
      start() const
70 71
      {
	os_ << "never {";
72 73 74
	auto n = aut_->get_named_prop<std::string>("automaton-name");
	if (n)
	  os_ << " /* " << *n << " */";
75
	os_ << '\n';
76
      }
77

78
      void
79
      end() const
80
      {
81
	if (need_accept_all_)
82 83 84 85 86
	  {
	    os_ << "accept_all:";
	    print_comment(accept_all_);
	    os_ << "\n  skip\n";
	  }
87
	os_ << '}' << std::endl;
88
      }
89

90
      bool is_sink(unsigned n) const
91
      {
92 93 94 95
	auto ts = aut_->out(n);
	assert(ts.begin() != ts.end());
	auto it = ts.begin();
	return (it->cond == bddtrue) && (it->dst == n) && (++it == ts.end());
96
      }
97

98 99 100
      void
      print_comment(unsigned n) const
      {
101 102 103
	if (sn_)
	  if (n < sn_->size() && !(*sn_)[n].empty())
	    os_ << " /* " << (*sn_)[n] << " */";
104 105
      }

106 107
      void
      print_state(unsigned n) const
108 109
      {
	std::string label;
110 111
	bool acc = aut_->state_is_accepting(n);
	if (n == aut_->get_init_state_number())
112
	  {
113 114
	    if (acc)
	      os_ << "accept_init";
115
	    else
116
	      os_ << "T0_init";
117 118 119
	  }
	else
	  {
120 121 122 123
	    if (!acc)
	      os_ << "T0_S" << n;
	    else if (is_sink(n))
	      os_ << "accept_all";
124
	    else
125
	      os_ << "accept_S" << n;
126
	  }
127
      }
128

129
      void process_state(unsigned n)
130
      {
131 132
	if (aut_->state_is_accepting(n) && is_sink(n)
	    && n != aut_->get_init_state_number())
133 134 135
	  {
	    // We want the accept_all state at the end of the never claim.
	    need_accept_all_ = true;
136
	    accept_all_ = n;
137 138 139 140 141
	    return;
	  }

	print_state(n);
	os_ << ':';
142 143
	print_comment(n);
	os_ << (opt_624_ ? "\n  do\n" : "\n  if\n");
144
	bool did_output = false;
145
	for (auto& t: aut_->out(n))
146
	  {
147
	    did_output = true;
148 149 150 151 152 153
	    bool atom =
	      opt_624_ && aut_->state_is_accepting(t.dst) && is_sink(t.dst);
	    if (atom)
	      os_ << "  :: atomic { (";
	    else
	      os_ << "  :: (";
154
	    const ltl::formula* f = bdd_to_formula(t.cond, aut_->get_dict());
155
	    to_spin_string(f, os_, true);
156 157 158 159 160 161 162 163 164 165 166
	    if (atom)
	      {
		os_ << ") -> assert(!(";
		to_spin_string(f, os_, true);
		os_ << ")) }";
	      }
	    else
	      {
		os_ << ") -> goto ";
		print_state(t.dst);
	      }
167
	    f->destroy();
168 169 170 171
	    os_ << '\n';
	  }
	if (!did_output)
	  {
172 173 174 175 176 177 178 179 180
	    if (opt_624_)
	      {
		os_ << "  :: atomic { (false) -> assert(!(false)) }";
	      }
	    else
	      {
		os_ << "  :: (false) -> goto ";
		print_state(n);
	      }
181
	    os_ << '\n';
182
	  }
183
	os_ << (opt_624_ ? "  od;\n" : "  fi;\n");
184
      }
185

186 187 188
      void print(const const_tgba_digraph_ptr& aut)
      {
	aut_ = aut;
189 190
	if (opt_comments_)
	  sn_ = aut->get_named_prop<std::vector<std::string>>("state-names");
191 192 193 194 195 196 197 198 199
	start();
	unsigned init = aut_->get_init_state_number();
	unsigned ns = aut_->num_states();
	process_state(init);
	for (unsigned n = 0; n < ns; ++n)
	  if (n != init)
	    process_state(n);
	end();
      }
200
    };
201
  } // anonymous namespace
202 203

  std::ostream&
204
  never_claim_reachable(std::ostream& os, const const_tgba_ptr& g,
205
			const char* options)
206
  {
207 208 209
    if (!(g->acc().is_buchi() || g->acc().is_true()))
      throw std::runtime_error
	("Never claim output only supports Büchi acceptance");
210 211 212
    never_claim_output d(os, options);
    auto aut = std::dynamic_pointer_cast<const tgba_digraph>(g);
    if (!aut)
213
      aut = make_tgba_digraph(g, twa::prop_set::all());
214
    d.print(aut);
215 216 217
    return os;
  }
}