1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
6
7 This program is free software; you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation; either version 2 of the License, or
10 (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software
19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
20
21 */
22
23 //
24 // Implementation for class TransitionSet.
25 //
26 #include <set>
27
28 // utility stuff
29 #include "macros.hh"
30 #include "vector.hh"
31 #include "indent.hh"
32 #include "bddUser.hh" // for dump()
33
34 // temporal class definitions
35 #include "transitionSet.hh"
36
37 void
insert(const Transition & transition)38 TransitionSet::insert(const Transition& transition)
39 {
40 Bdd formula = transition.second;
41 if (formula == bdd_false())
42 return; // for robustness
43 const TransitionMap::iterator e = transitionMap.end();
44 TransitionMap::iterator equal = e;
45 for (TransitionMap::iterator i = transitionMap.begin(); i != e;)
46 {
47 TransitionMap::iterator t = i++;
48 if (t->first == transition.first)
49 equal = t;
50 else if (t->first.contains(transition.first))
51 {
52 t->second = bdd_and(t->second, bdd_not(formula));
53 if (t->second == bdd_false())
54 transitionMap.erase(t); // existing pair completely subsumed
55 }
56 else if (transition.first.contains(t->first))
57 {
58 formula = bdd_and(formula, bdd_not(t->second));
59 if (formula == bdd_false())
60 return; // new transition completely subsumed
61 }
62 }
63 if (equal == e)
64 {
65 pair<TransitionMap::iterator, bool> p = transitionMap.insert(transition);
66 Assert(p.second, "failed to insert");
67 p.first->second = formula;
68 }
69 else
70 equal->second = bdd_or(equal->second, formula);
71 }
72
73 void
insert(const TransitionSet & transitionSet)74 TransitionSet::insert(const TransitionSet& transitionSet)
75 {
76 const TransitionMap::const_iterator e = transitionSet.transitionMap.end();
77 for (TransitionMap::const_iterator i = transitionSet.transitionMap.begin(); i != e; ++i)
78 insert(*i);
79 }
80
81 void
product(const TransitionSet & ts1,const TransitionSet & ts2)82 TransitionSet::product(const TransitionSet& ts1, const TransitionSet& ts2)
83 {
84 transitionMap.clear();
85 const TransitionMap::const_iterator ie = ts1.transitionMap.end();
86 const TransitionMap::const_iterator je = ts2.transitionMap.end();
87 Transition newTransition;
88 for (TransitionMap::const_iterator i = ts1.transitionMap.begin(); i != ie; ++i)
89 {
90 for (TransitionMap::const_iterator j = ts2.transitionMap.begin(); j != je; ++j)
91 {
92 newTransition.second = bdd_and(i->second, j->second);
93 if (newTransition.second != bdd_false())
94 {
95 newTransition.first = i->first;
96 newTransition.first.insert(j->first);
97 insert(newTransition);
98 }
99 }
100 }
101 }
102
103 void
rename(const TransitionSet & original,const Vector<int> & renaming)104 TransitionSet::rename(const TransitionSet& original, const Vector<int>& renaming)
105 {
106 //
107 // Renaming must be injective: no two old states must map to
108 // the name new state. We make use of that to do a fast insertion
109 // of the renamed state sets.
110 //
111 transitionMap.clear();
112 const TransitionMap::const_iterator ei = original.transitionMap.end();
113 for (TransitionMap::const_iterator i = original.transitionMap.begin(); i != ei; ++i)
114 {
115 Transition t;
116 const NatSet::const_iterator ej = i->first.end();
117 for (NatSet::const_iterator j = i->first.begin(); j != ej; ++j)
118 {
119 Assert(renaming[*j] != NONE, "no renaming for " << *j);
120 t.first.insert(renaming[*j]);
121 }
122 t.second = i->second;
123 transitionMap.insert(t);
124 }
125 }
126
127 void
dump(ostream & s,int indentLevel) const128 TransitionSet::dump(ostream& s, int indentLevel) const
129 {
130 const TransitionMap::const_iterator e = transitionMap.end();
131 for (TransitionMap::const_iterator i = transitionMap.begin(); i != e; ++i)
132 {
133 s << Indent(indentLevel) << i->first << '\t';
134 BddUser::dump(s, i->second);
135 s << '\n';
136 }
137 }
138