1 #include <math.h>
2 #include <unistd.h>
3 #include <stdlib.h>
4 #include <iostream>
5 #include "bddx.h"
6 using std::cout;
7 using std::endl;
8 using std::flush;
9
10 float dummyStateNum; // Use to remove the number of states defined by the
11 // next-state variables
12
13 #define SIZE 33 // Size of the board
14 #define CENTER 16 // Location of the center place
15
16 bdd boardC[SIZE]; // Current state variables
17 bdd boardN[SIZE]; // Next state variables
18 bdd I; // Initial state
19 bdd T; // Transition relation
20
21 bdd currentvar; // All current state variables
22 bddPair *pair; // Renaming pair
23
24
25 // All the possible moves. Note that the numbering starts from '1'
26 int moves[][3] =
27 { {1,4,9}, {1,2,3},
28 {2,5,10},
29 {3,2,1}, {3,6,11},
30 {4,5,6}, {4,9,16},
31 {5,10,17},
32 {6,5,4}, {6,11,18},
33 {7,8,9}, {7,14,21},
34 {8,9,10}, {8,15,22},
35 {9,8,7}, {9,10,11}, {9,4,1}, {9,16,23},
36 {10,9,8}, {10,11,12}, {10,5,2}, {10,17,24},
37 {11,10,9}, {11,12,13}, {11,6,3}, {11,18,25},
38 {12,11,10}, {12,19,26},
39 {13,12,11}, {13,20,27},
40 {14,15,16},
41 {15,16,17},
42 {16,15,14}, {16,17,18}, {16,9,4}, {16,23,28},
43 {17,16,15}, {17,18,19}, {17,10,5}, {17,24,29},
44 {18,17,16}, {18,19,20}, {18,11,6}, {18,25,30},
45 {19,18,17},
46 {20,19,18},
47 {21,22,23}, {21,14,7},
48 {22,23,24}, {22,15,8},
49 {23,22,21}, {23,24,25}, {23,16,9}, {23,28,31},
50 {24,23,22}, {24,25,26}, {24,17,10}, {24,29,32},
51 {25,24,23}, {25,26,27}, {25,18,11}, {25,30,33},
52 {26,25,24}, {26,19,12},
53 {27,26,25}, {27,20,13},
54 {28,29,30}, {28,23,16},
55 {29,24,17},
56 {30,29,28}, {30,25,18},
57 {31,32,33}, {31,28,23},
58 {32,29,24},
59 {33,32,31}, {33,30,25},
60 {0,0,0}
61 };
62
63
64
65
66
67 // Setup the variables needed for the board
make_board(void)68 void make_board(void)
69 {
70 bdd_setvarnum(SIZE*2);
71
72 for (int n=0 ; n<SIZE ; n++)
73 {
74 boardC[n] = bdd_ithvar(n*2);
75 boardN[n] = bdd_ithvar(n*2+1);
76 }
77 }
78
79
80 // Make the initial state predicate
make_initial_state(void)81 void make_initial_state(void)
82 {
83 I = bddtrue;
84
85 for (int n=0 ; n<SIZE ; n++)
86 if (n == CENTER)
87 I &= !boardC[n];
88 else
89 I &= boardC[n];
90 }
91
92
93 // Make sure all other places does nothing when
94 // there's a move from 'src' to 'dst' over 'tmp'
all_other_idle(int src,int tmp,int dst)95 bdd all_other_idle(int src, int tmp, int dst)
96 {
97 bdd idle = bddtrue;
98
99 for (int n=0 ; n<SIZE ; n++)
100 {
101 if (n != src && n != tmp && n != dst)
102 idle &= bdd_biimp(boardC[n], boardN[n]);
103 }
104
105 return idle;
106 }
107
108
109 // Encode one move from 'src' to 'dst' over 'tmp'
make_move(int src,int tmp,int dst)110 bdd make_move(int src, int tmp, int dst)
111 {
112 bdd move = boardC[src] & boardC[tmp] & !boardC[dst] &
113 !boardN[src] & !boardN[tmp] & boardN[dst];
114
115 move &= all_other_idle(src, tmp, dst);
116
117 return move;
118 }
119
120
make_transition_relation(void)121 void make_transition_relation(void)
122 {
123 using namespace std ;
124 T = bddfalse;
125
126 for (int n=0 ; moves[n][0]!=moves[n][1] ; n++)
127 T |= make_move(moves[n][0]-1, moves[n][1]-1, moves[n][2]-1);
128
129 cout << "Transition relation: " << bdd_nodecount(T) << " nodes, "
130 << bdd_satcount(T)/dummyStateNum << " states\n";
131 }
132
133
134 // Make renaming pair and current state variables
make_itedata(void)135 void make_itedata(void)
136 {
137 pair = bdd_newpair();
138 for (int n=0 ; n<SIZE ; n++)
139 bdd_setpair(pair, n*2+1, n*2);
140
141 currentvar = bddtrue;
142 for (int n=0 ; n<SIZE ; n++)
143 currentvar &= boardC[n];
144 }
145
146
147 // Do the forward iteration
iterate(void)148 void iterate(void)
149 {
150 bdd tmp;
151 bdd reachable = I;
152 int cou = 1;
153
154 make_itedata();
155
156 do
157 {
158 tmp = reachable;
159 bdd next = bdd_appex(reachable, T, bddop_and, currentvar);
160 next = bdd_replace(next, pair);
161 reachable |= next;
162
163 std::cout << cou << ": " << bdd_nodecount(reachable)
164 << " nodes, " << bdd_satcount(reachable)/dummyStateNum
165 << " states\n" << std::endl ;
166 cou++;
167 }
168 while (tmp != reachable);
169 }
170
171
iterate_front(void)172 void iterate_front(void)
173 {
174 bdd tmp;
175 bdd reachable = I;
176 bdd front = reachable;
177 int cou = 1;
178
179 make_itedata();
180
181 do
182 {
183 tmp = reachable;
184 bdd next = bdd_appex(front, T, bddop_and, currentvar);
185 next = bdd_replace(next, pair);
186 front = next - reachable;
187 reachable |= front;
188
189 std::cout << cou << ": " << bdd_nodecount(reachable)
190 << " , " << bdd_satcount(reachable)/dummyStateNum << std::endl;
191 std::cout << cou << ": " << bdd_nodecount(front)
192 << " , " << bdd_satcount(front)/dummyStateNum << std::endl;
193 cou++;
194 }
195 while (tmp != reachable);
196 }
197
198
setup(void)199 void setup(void)
200 {
201 bdd_init(100000,1000);
202 bdd_setcacheratio(64);
203 bdd_setmaxincrease(500000);
204
205 dummyStateNum = pow(2.0, SIZE);
206
207 make_board();
208 make_transition_relation();
209 make_initial_state();
210 }
211
212
main(void)213 int main(void)
214 {
215 setup();
216 iterate();
217
218 system("ps aux | grep \"./solitare\" | grep -v \"grep\"");
219 }
220