taatgba.hh 10 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
4 5 6 7 8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10 11 12 13 14 15 16 17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
#pragma once
21 22

#include <set>
Damien Lefortier's avatar
Damien Lefortier committed
23
#include <iosfwd>
24
#include <vector>
25
#include <string>
26 27 28 29
#include "misc/hash.hh"
#include "ltlast/formula.hh"
#include "bdddict.hh"
#include "tgba.hh"
30
#include "ltlvisit/tostring.hh"
31 32 33

namespace spot
{
34 35
  /// \brief A self-loop Transition-based Alternating Automaton (TAA)
  /// which is seen as a TGBA (abstract class, see below).
36
  class SPOT_API taa_tgba: public twa
37 38
  {
  public:
39
    taa_tgba(const bdd_dict_ptr& dict);
40 41 42 43 44 45 46 47 48

    struct transition;
    typedef std::list<transition*> state;
    typedef std::set<state*> state_set;

    /// Explicit transitions.
    struct transition
    {
      bdd condition;
49
      acc_cond::mark_t acceptance_conditions;
50 51 52 53
      const state_set* dst;
    };

    void add_condition(transition* t, const ltl::formula* f);
Damien Lefortier's avatar
Damien Lefortier committed
54

55
    /// TGBA interface.
56
    virtual ~taa_tgba();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
57 58
    virtual spot::state* get_init_state() const final;
    virtual tgba_succ_iterator* succ_iter(const spot::state* state) const final;
59
    virtual std::string format_state(const spot::state* state) const = 0;
60 61

  protected:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
62 63
    virtual bdd compute_support_conditions(const spot::state* state)
      const final;
64

65
    typedef std::vector<taa_tgba::state_set*> ss_vec;
66

67
    taa_tgba::state_set* init_;
68 69
    ss_vec state_set_vec_;

70 71 72
    std::map<const ltl::formula*, acc_cond::mark_t,
	     ltl::formula_ptr_less_than> acc_map_;

73 74
  private:
    // Disallow copy.
75 76
    taa_tgba(const taa_tgba& other) SPOT_DELETED;
    taa_tgba& operator=(const taa_tgba& other) SPOT_DELETED;
77 78 79
  };

  /// Set of states deriving from spot::state.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
80
  class SPOT_API set_state final: public spot::state
81 82
  {
  public:
83
    set_state(const taa_tgba::state_set* s, bool delete_me = false)
84
      : s_(s), delete_me_(delete_me)
85 86 87 88 89
    {
    }

    virtual int compare(const spot::state*) const;
    virtual size_t hash() const;
90
    virtual set_state* clone() const;
91

92
    virtual ~set_state()
93
    {
94 95
      if (delete_me_)
	delete s_;
96 97
    }

98
    const taa_tgba::state_set* get_state() const;
99
  private:
100
    const taa_tgba::state_set* s_;
101
    bool delete_me_;
102 103
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
104
  class SPOT_API taa_succ_iterator final: public tgba_succ_iterator
105 106
  {
  public:
107
    taa_succ_iterator(const taa_tgba::state_set* s, const acc_cond& acc);
Damien Lefortier's avatar
Damien Lefortier committed
108
    virtual ~taa_succ_iterator();
109

110 111
    virtual bool first();
    virtual bool next();
112 113
    virtual bool done() const;

114
    virtual set_state* current_state() const;
115
    virtual bdd current_condition() const;
116
    virtual acc_cond::mark_t current_acceptance_conditions() const;
117 118

  private:
119 120
    /// Those typedefs are used to generate all possible successors in
    /// the constructor using a cartesian product.
121
    typedef taa_tgba::state::const_iterator iterator;
122 123
    typedef std::pair<iterator, iterator> iterator_pair;
    typedef std::vector<iterator_pair> bounds_t;
124 125 126
    typedef std::unordered_map<const spot::set_state*,
			       std::vector<taa_tgba::transition*>,
			       state_ptr_hash, state_ptr_equal> seen_map;
127 128 129 130 131 132 133 134 135 136 137 138

    struct distance_sort :
      public std::binary_function<const iterator_pair&,
				  const iterator_pair&, bool>
    {
      bool
      operator()(const iterator_pair& lhs, const iterator_pair& rhs) const
      {
	return std::distance(lhs.first, lhs.second) <
	       std::distance(rhs.first, rhs.second);
      }
    };
139

140 141
    std::vector<taa_tgba::transition*>::const_iterator i_;
    std::vector<taa_tgba::transition*> succ_;
Damien Lefortier's avatar
Damien Lefortier committed
142
    seen_map seen_;
143
    const acc_cond& acc_;
144
  };
145 146 147

  /// A taa_tgba instance with states labeled by a given type.
  /// Still an abstract class, see below.
148
  template<typename label>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
149
  class SPOT_API taa_tgba_labelled: public taa_tgba
150 151
  {
  public:
152
    taa_tgba_labelled(const bdd_dict_ptr& dict) : taa_tgba(dict) {};
153

154 155 156 157 158 159 160
    ~taa_tgba_labelled()
      {
	auto i = acc_map_.begin();
	while (i != acc_map_.end())
	  (i++)->first->destroy();
      }

161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
    void set_init_state(const label& s)
    {
      std::vector<label> v(1);
      v[0] = s;
      set_init_state(v);
    }
    void set_init_state(const std::vector<label>& s)
    {
      init_ = add_state_set(s);
    }

    transition*
    create_transition(const label& s,
		      const std::vector<label>& d)
    {
      state* src = add_state(s);
      state_set* dst = add_state_set(d);
      transition* t = new transition;
      t->dst = dst;
      t->condition = bddtrue;
181
      t->acceptance_conditions = 0U;
182 183 184
      src->push_back(t);
      return t;
    }
185

186 187 188 189 190 191 192 193 194 195
    transition*
    create_transition(const label& s, const label& d)
    {
      std::vector<std::string> vec;
      vec.push_back(d);
      return create_transition(s, vec);
    }

    void add_acceptance_condition(transition* t, const ltl::formula* f)
    {
196 197 198 199 200 201
      auto p = acc_map_.emplace(f, 0);
      if (p.second)
	p.first->second = acc_.marks({acc_.add_set()});
      else
	f->destroy();
      t->acceptance_conditions |= p.first->second;
202 203 204 205
    }

    /// \brief Format the state as a string for printing.
    ///
206
    /// If state is a spot::set_state of only one element, then the
207 208 209
    /// string corresponding to state->get_state() is returned.
    ///
    /// Otherwise a string composed of each string corresponding to
210
    /// each state->get_state() in the spot::set_state is returned,
211 212 213
    /// e.g. like {string_1,...,string_n}.
    virtual std::string format_state(const spot::state* s) const
    {
214
      const spot::set_state* se = down_cast<const spot::set_state*>(s);
215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
      assert(se);
      const state_set* ss = se->get_state();
      return format_state_set(ss);
    }

    /// \brief Output a TAA in a stream.
    void output(std::ostream& os) const
    {
      typename ns_map::const_iterator i;
      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
      {
	taa_tgba::state::const_iterator i2;
	os << "State: " << label_to_string(i->first) << std::endl;
	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
	{
230
	  os << ' ' << format_state_set((*i2)->dst)
231 232 233 234 235 236 237
	     << ", C:" << (*i2)->condition
	     << ", A:" << (*i2)->acceptance_conditions << std::endl;
	}
      }
    }

  protected:
238 239
    typedef label label_t;

240
    typedef std::unordered_map<label, taa_tgba::state*> ns_map;
241
    typedef std::unordered_map<const taa_tgba::state*, label,
242
			       ptr_hash<taa_tgba::state> > sn_map;
243 244 245 246 247

    ns_map name_state_map_;
    sn_map state_name_map_;

    /// \brief Return a label as a string.
248 249 250 251 252
    virtual std::string label_to_string(const label_t& lbl) const = 0;

    /// \brief Clone the label if necessary to assure it is owned by
    /// this, avoiding memory issues when label is a pointer.
    virtual label_t clone_if(const label_t& lbl) const = 0;
253 254 255 256 257 258 259 260 261

  private:
    /// \brief Return the taa_tgba::state for \a name, creating it
    /// when it does not exist already.
    taa_tgba::state* add_state(const label& name)
    {
      typename ns_map::iterator i = name_state_map_.find(name);
      if (i == name_state_map_.end())
      {
262
	const label& name_ = clone_if(name);
263
	taa_tgba::state* s = new taa_tgba::state;
264 265
	name_state_map_[name_] = s;
	state_name_map_[s] = name_;
266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308
	return s;
      }
      return i->second;
    }

    /// \brief Return the taa::state_set for \a names.
    taa_tgba::state_set* add_state_set(const std::vector<label>& names)
    {
      state_set* ss = new state_set;
      for (unsigned i = 0; i < names.size(); ++i)
	ss->insert(add_state(names[i]));
      state_set_vec_.push_back(ss);
      return ss;
    }

    std::string format_state_set(const taa_tgba::state_set* ss) const
    {
      state_set::const_iterator i1 = ss->begin();
      typename sn_map::const_iterator i2;
      if (ss->empty())
	return std::string("{}");
      if (ss->size() == 1)
      {
	i2 = state_name_map_.find(*i1);
	assert(i2 != state_name_map_.end());
	return "{" + label_to_string(i2->second) + "}";
      }
      else
      {
	std::string res("{");
	while (i1 != ss->end())
	{
	  i2 = state_name_map_.find(*i1++);
	  assert(i2 != state_name_map_.end());
	  res += label_to_string(i2->second);
	  res += ",";
	}
	res[res.size() - 1] = '}';
	return res;
      }
    }
  };

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
309
  class SPOT_API taa_tgba_string final:
310
#ifndef SWIG
311
    public taa_tgba_labelled<std::string>
312 313 314
#else
    public taa_tgba
#endif
315 316
  {
  public:
317
    taa_tgba_string(const bdd_dict_ptr& dict) :
318
      taa_tgba_labelled<std::string>(dict) {};
319
    ~taa_tgba_string();
320
  protected:
321 322
    virtual std::string label_to_string(const std::string& label) const;
    virtual std::string clone_if(const std::string& label) const;
323 324
  };

325 326 327 328 329 330 331 332
  typedef std::shared_ptr<taa_tgba_string> taa_tgba_string_ptr;
  typedef std::shared_ptr<const taa_tgba_string> const_taa_tgba_string_ptr;

  inline taa_tgba_string_ptr make_taa_tgba_string(const bdd_dict_ptr& dict)
  {
    return std::make_shared<taa_tgba_string>(dict);
  }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
333
  class SPOT_API taa_tgba_formula final:
334
#ifndef SWIG
335
    public taa_tgba_labelled<const ltl::formula*>
336 337 338
#else
    public taa_tgba
#endif
339 340
  {
  public:
341
    taa_tgba_formula(const bdd_dict_ptr& dict) :
342
      taa_tgba_labelled<const ltl::formula*>(dict) {};
343
    ~taa_tgba_formula();
344
  protected:
345
    virtual std::string label_to_string(const label_t& label) const;
346
    virtual const ltl::formula* clone_if(const label_t& label) const;
347
  };
348 349 350 351 352 353 354 355

  typedef std::shared_ptr<taa_tgba_formula> taa_tgba_formula_ptr;
  typedef std::shared_ptr<const taa_tgba_formula> const_taa_tgba_formula_ptr;

  inline taa_tgba_formula_ptr make_taa_tgba_formula(const bdd_dict_ptr& dict)
  {
    return std::make_shared<taa_tgba_formula>(dict);
  }
356
}