tgbabddconcretefactory.cc 4.07 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
#include "ltlvisit/clone.hh"
23
#include "ltlvisit/destroy.hh"
24
#include "tgbabddconcretefactory.hh"
25
namespace spot
26
{
27
28
  tgba_bdd_concrete_factory::tgba_bdd_concrete_factory(bdd_dict* dict)
    : data_(dict)
29
30
31
  {
  }

32
33
  tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory()
  {
34
35
36
    acc_map_::iterator ai;
    for (ai = acc_.begin(); ai != acc_.end(); ++ai)
      destroy(ai->first);
37
    get_dict()->unregister_all_my_variables(this);
38
39
40
41
42
  }

  int
  tgba_bdd_concrete_factory::create_state(const ltl::formula* f)
  {
43
    int num = get_dict()->register_state(f, this);
44
45
    // Keep track of all "Now" variables for easy
    // existential quantification.
46
    data_.declare_now_next (bdd_ithvar(num), bdd_ithvar(num + 1));
47
48
49
50
51
52
    return num;
  }

  int
  tgba_bdd_concrete_factory::create_atomic_prop(const ltl::formula* f)
  {
53
    int num = get_dict()->register_proposition(f, this);
54
55
    // Keep track of all atomic proposition for easy
    // existential quantification.
56
    data_.declare_atomic_prop(bdd_ithvar(num));
57
58
59
    return num;
  }

60
  void
61
  tgba_bdd_concrete_factory::declare_acceptance_condition(bdd b,
62
							 const ltl::formula* a)
63
  {
64
65
66
67
68
    // Maintain a conjunction of BDDs associated to A.  We will latter
    // (in tgba_bdd_concrete_factory::finish()) associate this
    // conjunction to A.
    acc_map_::iterator ai = acc_.find(a);
    if (ai == acc_.end())
69
      {
70
71
	a = clone(a);
	acc_[a] = b;
72
73
74
      }
    else
      {
75
	ai->second &= b;
76
77
      }
  }
78

79
80
81
  void
  tgba_bdd_concrete_factory::finish()
  {
82
83
84
    acc_map_::iterator ai;
    for (ai = acc_.begin(); ai != acc_.end(); ++ai)
      {
85
86
87
	// Register a BDD variable for this acceptance condition.
	int num = get_dict()->register_acceptance_variable(ai->first, this);
	// Keep track of all acceptance conditions for easy
88
	// existential quantification.
89
	data_.declare_acceptance_condition(bdd_ithvar(num));
90
91
      }
    for (ai = acc_.begin(); ai != acc_.end(); ++ai)
92
      {
93
	bdd acc = bdd_ithvar(get_dict()->acc_map[ai->first]);
94

95
	// Complete acc with all the other acceptance conditions negated.
96
97
98
	acc &= bdd_exist(data_.negacc_set, acc);

	// Any state matching the BDD formulae registered is part
99
100
	// of this acceptance set.
	data_.acceptance_conditions |= ai->second & acc;
101

102
103
	// Keep track of all acceptance conditions, so that we can
	// easily check whether a transition satisfies all acceptance
104
	// conditions.
105
	data_.all_acceptance_conditions |= acc;
106
      }
107
108
109
110
111
112
113
114

    // Any constraint between Now variables also exist between Next
    // variables.  Doing this limits the quantity of useless
    // successors we will have to explore.  (By "useless successors"
    // I mean a combination of Next variables that represent a cul de sac
    // state: the combination exists but won't allow further exploration
    // because it fails the constraints.)
    data_.relation &= bdd_replace(bdd_exist(data_.relation, data_.notnow_set),
115
				  get_dict()->now_to_next);
116
117
118
119
120
121
122
123
  }

  const tgba_bdd_core_data&
  tgba_bdd_concrete_factory::get_core_data() const
  {
    return data_;
  }

124
  bdd_dict*
125
126
  tgba_bdd_concrete_factory::get_dict() const
  {
127
    return data_.dict;
128
129
130
  }

  void
131
  tgba_bdd_concrete_factory::constrain_relation(bdd new_rel)
132
133
134
135
  {
    data_.relation &= new_rel;
  }
}