tgbabddconcretefactory.hh 3.42 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// 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
// the Free Software Foundation; either version 2 of the License, or
// (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
// along with Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

22
23
24
#ifndef SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH
# define SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH

25
#include "misc/hash.hh"
26
27
28
#include "ltlast/formula.hh"
#include "tgbabddfactory.hh"

29
namespace spot
30
{
31
  /// Helper class to build a spot::tgba_bdd_concrete object.
32
  class tgba_bdd_concrete_factory: public tgba_bdd_factory
33
34
  {
  public:
35
    tgba_bdd_concrete_factory(bdd_dict* dict);
36

37
    virtual ~tgba_bdd_concrete_factory();
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

    /// Create a state variable for formula \a f.
    ///
    /// \param f The formula to create a state for.
    /// \return The variable number for this state.
    ///
    /// The state is not created if it already exists.  Instead its
    /// existing variable number is returned.  Variable numbers
    /// can be turned into BDD using ithvar().
    int create_state(const ltl::formula* f);

    /// Create an atomic proposition variable for formula \a f.
    ///
    /// \param f The formula to create an aotmic proposition for.
    /// \return The variable number for this state.
    ///
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
54
    /// The atomic proposition is not created if it already exists.
55
56
    /// Instead its existing variable number is returned.  Variable numbers
    /// can be turned into BDD using ithvar().
57
    int create_atomic_prop(const ltl::formula* f);
58

59
    /// Declare an acceptance condition.
60
    ///
61
62
63
    /// Formula such as 'f U g' or 'F g' make the promise
    /// that 'g' will be fulfilled eventually.  So once
    /// one of this formula has been translated into a BDD,
64
65
    /// we use declare_acceptance_condition() to associate
    /// all other states to the acceptance set of 'g'.
66
67
    ///
    /// \param b a BDD indicating which variables are in the
68
    ///          acceptance set
69
    /// \param a the formula associated
70
    void declare_acceptance_condition(bdd b, const ltl::formula* a);
71

72
    const tgba_bdd_core_data& get_core_data() const;
73
    bdd_dict* get_dict() const;
74
75

    /// Add a new constraint to the relation.
76
    void constrain_relation(bdd new_rel);
77

78
    /// \brief Perfom final computations before the relation can be used.
79
80
    ///
    /// This function should be called after all propositions, state,
81
    /// acceptance conditions, and constraints have been declared, and
82
    /// before calling get_code_data() or get_dict().
83
84
    void finish();

85
  private:
86
    tgba_bdd_core_data data_;	///< Core data for the new automata.
87

88
89
    typedef Sgi::hash_map<const ltl::formula*, bdd,
			  ptr_hash<ltl::formula> > acc_map_;
90
    acc_map_ acc_;		///< BDD associated to each acceptance condition
91
92
93
94
  };

}
#endif // SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH