alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[buddy] * examples/cmilner/cmilner.c (A, transitions, initial_state)

Browse source 
(reachable_states, has_deadlocks): Declare as static functions,
to suppress a GCC warning.
This commit is contained in:
Alexandre Duret-Lutz 2011-06-07 14:50:07 +02:00
parent f4ecb34275
commit b535741a90
2 changed files with 43 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

6
buddy/ChangeLog
View file

@ -1,3 +1,9 @@
2011-06-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* examples/cmilner/cmilner.c (A, transitions, initial_state)
(reachable_states, has_deadlocks): Declare as static functions,
to suppress a GCC warning.
2011-04-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Inline the "is bdd constant" check performed in copies/constructors.

74
buddy/examples/cmilner/cmilner.c
View file

@ -10,11 +10,11 @@ int *primvar; /* Next state variables */
bdd normvarset;
bddPair *pairs;
bdd A(bdd* x, bdd* y, int z)
static bdd A(bdd* x, bdd* y, int z)
{
bdd res = bddtrue, tmp1, tmp2;
int i;
for(i=0 ; i<N ; i++)
if(i != z)
{
@ -25,17 +25,17 @@ bdd A(bdd* x, bdd* y, int z)
bdd_delref(res);
res = tmp2;
}
return res;
}
bdd transitions(bdd* t, bdd* tp, bdd* h, bdd* hp, bdd* c, bdd* cp)
static bdd transitions(bdd* t, bdd* tp, bdd* h, bdd* hp, bdd* c, bdd* cp)
{
int i;
bdd P, E, T = bddfalse;
bdd tmp1, tmp2, tmp3, tmp4, tmp5, tmp6;
for(i=0; i<N; i++)
{
bdd_addref(T);
@ -60,14 +60,14 @@ bdd transitions(bdd* t, bdd* tp, bdd* h, bdd* hp, bdd* c, bdd* cp)
tmp3 = bdd_addref( bdd_apply(tmp2, tmp4, bddop_and) );
bdd_delref(tmp2);
bdd_delref(tmp4);
tmp1 = bdd_addref( bdd_apply(tmp3, tmp5, bddop_and) );
bdd_delref(tmp3);
bdd_delref(tmp5);
tmp4 = bdd_addref( bdd_apply(h[i], hp[i], bddop_diff) );
tmp5 = bdd_addref( bdd_apply(tmp4, cp[(i+1)%N], bddop_and) );
bdd_delref(tmp4);
@ -97,7 +97,7 @@ bdd transitions(bdd* t, bdd* tp, bdd* h, bdd* hp, bdd* c, bdd* cp)
tmp1 = bdd_addref( bdd_apply(t[i], tp[i], bddop_diff) );
tmp2 = bdd_addref( A(t, tp, i) );
tmp3 = bdd_addref( bdd_apply(tmp1, tmp2, bddop_and) );
bdd_delref(tmp1);
bdd_delref(tmp2);
@ -112,7 +112,7 @@ bdd transitions(bdd* t, bdd* tp, bdd* h, bdd* hp, bdd* c, bdd* cp)
E = bdd_addref( bdd_apply(tmp6, tmp5, bddop_and) );
bdd_delref(tmp6);
bdd_delref(tmp5);
tmp1 = bdd_addref( bdd_apply(P, E, bddop_or) );
bdd_delref(P);
@ -126,14 +126,14 @@ bdd transitions(bdd* t, bdd* tp, bdd* h, bdd* hp, bdd* c, bdd* cp)
return T;
}
bdd initial_state(bdd* t, bdd* h, bdd* c)
static bdd initial_state(bdd* t, bdd* h, bdd* c)
{
int i;
bdd I, tmp1, tmp2, tmp3;
tmp1 = bdd_addref( bdd_not(h[0]) );
tmp2 = bdd_addref( bdd_apply(c[0], tmp1, bddop_and) );
bdd_delref(tmp1);
@ -143,7 +143,7 @@ bdd initial_state(bdd* t, bdd* h, bdd* c)
bdd_delref(tmp1);
bdd_delref(tmp2);
for(i=1; i<N; i++)
{
bdd_addref(I);
@ -166,20 +166,20 @@ bdd initial_state(bdd* t, bdd* h, bdd* c)
I = tmp1;
}
return I;
}
bdd reachable_states(bdd I, bdd T)
static bdd reachable_states(bdd I, bdd T)
{
bdd C, by, bx = bddfalse;
bdd tmp1;
do
{
bdd_addref(bx);
by = bx;
#if 1
tmp1 = bdd_addref( bdd_apply(T, bx, bddop_and) );
@ -188,7 +188,7 @@ bdd reachable_states(bdd I, bdd T)
#else
C = bdd_addref( bdd_appex(bx, T, bddop_and, normvar, N*3) );
#endif
tmp1 = bdd_addref( bdd_replace(C, pairs) );
bdd_delref(C);
C = tmp1;
@ -198,27 +198,27 @@ bdd reachable_states(bdd I, bdd T)
bdd_delref(bx);
bx = tmp1;
/*printf("."); fflush(stdout);*/
}
while(bx != by);
printf("\n");
return bx;
}
#if 0
int has_deadlocks(bdd R, bdd T)
static int has_deadlocks(bdd R, bdd T)
{
bdd C = bddtrue;
for(int i=0; i<N; i++)
C &= bdd_exist(T, primvar, N*3);
//C &= bdd_exist(bdd_exist(bdd_exist(T,i*6+3),i*6+5),i*6+1);
if(C != bddfalse && R != bddfalse)
return 0;
return 1;
}
#endif
@ -228,34 +228,34 @@ int main(int argc, char** argv)
bdd *c, *cp, *h, *hp, *t, *tp;
bdd I, T, R;
int n;
if(argc < 2)
{
printf("usage: %s N\n",argv[0]);
printf("\tN number of cyclers\n");
exit(1);
}
N = atoi(argv[1]);
if (N <= 0)
{
printf("The number of cyclers must more than zero\n");
exit(2);
}
bdd_init(100000, 10000);
bdd_setvarnum(N*6);
c = (bdd *)malloc(sizeof(bdd)*N);
cp = (bdd *)malloc(sizeof(bdd)*N);
t = (bdd *)malloc(sizeof(bdd)*N);
tp = (bdd *)malloc(sizeof(bdd)*N);
h = (bdd *)malloc(sizeof(bdd)*N);
hp = (bdd *)malloc(sizeof(bdd)*N);
normvar = (int *)malloc(sizeof(int)*N*3);
primvar = (int *)malloc(sizeof(int)*N*3);
for (n=0 ; n<N*3 ; n++)
{
normvar[n] = n*2;
@ -264,7 +264,7 @@ int main(int argc, char** argv)
normvarset = bdd_addref( bdd_makeset(normvar, N*3) );
pairs = bdd_newpair();
bdd_setpairs(pairs, primvar, normvar, N*3);
for (n=0 ; n<N ; n++)
{
c[n] = bdd_ithvar(n*6);
@ -274,19 +274,19 @@ int main(int argc, char** argv)
h[n] = bdd_ithvar(n*6+4);
hp[n] = bdd_ithvar(n*6+5);
}
I = bdd_addref( initial_state(t,h,c) );
T = bdd_addref( transitions(t,tp,h,hp,c,cp) );
R = bdd_addref( reachable_states(I,T) );
/*if(has_deadlocks(R,T))
printf("Milner's Scheduler has deadlocks!\n"); */
printf("SatCount R = %.0f\n", bdd_satcount(R));
printf("Calc = %.0f\n", (double)N*pow(2.0,1.0+N)*pow(2.0,3.0*N));
bdd_done();
return 0;
}