milner.cxx 3.89 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
#include <stdio.h>
#include <stdlib.h>
#include <math.h>
4
#include "bddx.h"
5
6
#include <iostream>
using namespace std;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7
8
9
10
11
12
13
14
15
16
17
18
19

int N;                // Number of cyclers
bdd normvar;          // Current state variables
bdd primvar;          // Next state variables
bddPair *renamepair;  // Variable pairs for renaming


/* Build a BDD expressing that all other variables than 'z' is unchanged.
 */
bdd A(bdd* x, bdd* y, int z)
{
   bdd res = bddtrue;
   int i;
20

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
21
22
23
   for(i=0 ; i<N ; i++)
      if(i != z)
	 res &= bdd_apply(x[i],y[i],bddop_biimp);
24

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
25
26
27
28
29
30
31
32
33
34
35
36
37
   return res;
}


/* Loop through all cyclers and create the transition relation for each
   of them.
*/
bdd transitions(bdd* t, bdd* tp, bdd* h, bdd* hp, bdd* c, bdd* cp)
{
   int i;
   bdd P;            // Cycler i's handling of the token
   bdd E;            // Cycler i's handling of it's task
   bdd T = bddfalse; // The monolithic transition relation
38

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
39
40
41
42
43
44
   for(i=0 ; i<N ; i++)
   {
      P = ((c[i]>cp[i]) & (tp[i]>t[i]) & hp[i] & A(c,cp,i)
	   & A(t,tp,i) & A(h,hp,i))
	 | ((h[i]>hp[i]) & cp[(i+1)%N] & A(c,cp,(i+1)%N) & A(h,hp,i)
	    & A(t,tp,N));
45

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
46
      E = t[i] & !tp[i] & A(t,tp,i) & A(h,hp,N) & A(c,cp,N);
47

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
48
49
      T |= P | E;
   }
50

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
51
52
53
54
55
56
57
58
59
60
   return T;
}


/* Create a BDD for the initial state.
 */
bdd initial_state(bdd* t, bdd* h, bdd* c)
{
   int i;
   bdd I = c[0] & !h[0] & !t[0];
61

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
62
63
   for(i=1; i<N; i++)
      I &= !c[i] & !h[i] & !t[i];
64

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
   return I;
}


/* Calculate the reachable states.
 */
bdd reachable_states(bdd I, bdd T)
{
   bdd R = I, // Reachable state space
       prevR, // Previously reached state space
       tmp;

   do
   {
      prevR = R;

#if 0
         // Apply and exist as different operations => slow
      tmp = T & bx;
      tmp = bdd_exist(tmp, normvar);
#else
         // Apply and exist as one operation => fast
      tmp = bdd_appex(R, T, bddop_and, normvar);
#endif
      tmp = bdd_replace(tmp, renamepair);
      R |= tmp;
   }
   while(prevR != R);
93

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
94
95
96
97
98
99
   return R;
}


int main(int argc, char** argv)
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
100
   using namespace std ;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
101
102
103
104
105
106
107
   int n;
   if(argc < 2)
   {
      cerr << "usage: milner N\n";
      cerr << "       N  number of cyclers\n";
      exit(1);
   }
108

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
109
110
111
112
113
114
   N = atoi(argv[1]);
   if (N <= 0)
   {
      cerr << "The number of cyclers must be more than zero\n";
      exit(2);
   }
115

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
116
117
   bdd_init(500000, 50000);
   bdd_setvarnum(N*6);
118

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
119
120
121
122
123
124
   bdd* c  = new bdd[N];
   bdd* cp = new bdd[N];
   bdd* t  = new bdd[N];
   bdd* tp = new bdd[N];
   bdd* h  = new bdd[N];
   bdd* hp = new bdd[N];
125

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
126
127
   int *nvar = new int[N*3];
   int *pvar = new int[N*3];
128

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
129
130
131
132
133
   for (n=0 ; n<N*3 ; n++)
   {
      nvar[n] = n*2;
      pvar[n] = n*2+1;
   }
134

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
135
136
137
138
   normvar = bdd_makeset(nvar, N*3);
   primvar = bdd_makeset(pvar, N*3);
   renamepair = bdd_newpair();
   bdd_setpairs(renamepair, pvar, nvar, N*3);
139

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
   for (n=0 ; n<N ; n++)
   {
      c[n]  = bdd_ithvar(n*6);
      cp[n] = bdd_ithvar(n*6+1);
      t[n]  = bdd_ithvar(n*6+2);
      tp[n] = bdd_ithvar(n*6+3);
      h[n]  = bdd_ithvar(n*6+4);
      hp[n] = bdd_ithvar(n*6+5);

#if 0
      bdd_addvarblock(c[n], BDD_REORDER_FIXED);
      bdd_addvarblock(cp[n], BDD_REORDER_FIXED);
      bdd_addvarblock(t[n], BDD_REORDER_FIXED);
      bdd_addvarblock(tp[n], BDD_REORDER_FIXED);
      bdd_addvarblock(h[n], BDD_REORDER_FIXED);
      bdd_addvarblock(hp[n], BDD_REORDER_FIXED);
      bdd_addvarblock(c[n] & cp[n] & t[n] & tp[n] & h[n] & hp[n],
		      BDD_REORDER_FREE);
#endif
   }

   bdd I = initial_state(t,h,c);
   bdd T = transitions(t,tp,h,hp,c,cp);
   bdd R = reachable_states(I,T);
164

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
165
166
167
168
169
170
171
172
173
174
175
176
177
178
   bddStat s;
   bdd_stats(&s);

   cout << "SatCount R = " << bdd_satcount(R) << endl;
   cout << "Calc       = " << (double)N*pow(2.0,1.0+N)*pow(2.0,3.0*N) << endl;
   cout << "Nodes      = " << s.produced << endl;
   cout << endl << "Number of nodes in T is " << bdd_nodecount( T ) << endl;
   cout << "Number of nodes in R is " << bdd_nodecount( R ) << endl << endl;

   //bdd_printstat();
   cout << "Nodenum: " << bdd_getnodenum() << endl;
   bdd_done();
   return 0;
}