fairkripke.hh 3.58 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2009, 2010, 2013, 2014, 2015 Laboratoire de Recherche et
3
// Developpement de l'Epita
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 "twa/twa.hh"
23
#include "fwd.hh"
24

25
/// \addtogroup kripke Kripke Structures
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
26
/// \ingroup twa
27

28
29
namespace spot
{
30
  /// \ingroup kripke
31
  /// \brief Iterator code for a Fair Kripke structure.
32
33
34
35
36
37
38
39
40
41
42
43
44
45
  ///
  /// This iterator can be used to simplify the writing
  /// of an iterator on a Fair Kripke structure (or lookalike).
  ///
  /// If you inherit from this iterator, you should only
  /// redefine
  ///
  ///   - fair_kripke_succ_iterator::first()
  ///   - fair_kripke_succ_iterator::next()
  ///   - fair_kripke_succ_iterator::done()
  ///   - fair_kripke_succ_iterator::current_state()
  ///
  /// This class implements fair_kripke_succ_iterator::current_condition(),
  /// and fair_kripke_succ_iterator::current_acceptance_conditions().
46
  class SPOT_API fair_kripke_succ_iterator : public twa_succ_iterator
47
48
  {
  public:
49
50
51
52
53
    /// \brief Constructor
    ///
    /// The \a cond and \a acc_cond arguments will be those returned
    /// by fair_kripke_succ_iterator::current_condition(),
    /// and fair_kripke_succ_iterator::current_acceptance_conditions().
54
    fair_kripke_succ_iterator(const bdd& cond, acc_cond::mark_t acc_cond);
55
56
    virtual ~fair_kripke_succ_iterator();

57
    virtual bdd current_condition() const;
58
    virtual acc_cond::mark_t current_acceptance_conditions() const;
59
  protected:
60
    bdd cond_;
61
    acc_cond::mark_t acc_cond_;
62
63
  };

64
  /// \ingroup kripke
65
  /// \brief Interface for a Fair Kripke structure.
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
  ///
  /// A Kripke structure is a graph in which each node (=state) is
  /// labeled by a conjunction of atomic proposition, and a set of
  /// acceptance conditions.
  ///
  /// Such a structure can be seen as spot::tgba by pushing all labels
  /// to the outgoing transitions.
  ///
  /// A programmer that develops an instance of Fair Kripke structure
  /// needs just provide an implementation for the following methods:
  ///
  ///   - kripke::get_init_state()
  ///   - kripke::succ_iter()
  ///   - kripke::state_condition()
  ///   - kripke::state_acceptance_conditions()
  ///   - kripke::format_state()
  ///   - and optionally kripke::transition_annotation()
  ///
  /// The other methods of the tgba interface are supplied by this
  /// class and need not be defined.
  ///
  /// See also spot::fair_kripke_succ_iterator.
88
  class SPOT_API fair_kripke: public twa
89
90
  {
  public:
91
    fair_kripke(const bdd_dict_ptr& d)
92
      : twa(d)
93
94
95
      {
      }

96
97
98
99
100
101
    /// \brief The condition that label the state \a s.
    ///
    /// This should be a conjunction of atomic propositions.
    virtual bdd state_condition(const state* s) const = 0;

    /// \brief The set of acceptance conditions that label the state \a s.
102
103
    virtual acc_cond::mark_t
      state_acceptance_conditions(const state* s) const = 0;
104

105
106
107
108
  protected:
    virtual bdd compute_support_conditions(const state* s) const;
  };
}