/*this program generates input file for Russian card problem in MCMAS*/
#include <stdio.h>
int main()
{
 int d0,d1,d2,d3,d4,d5,d6;
 int i,j,k,lt,lf,m,n,d_index=0;
 int deal[140][7];//anne[140][140],bill[140][140],cath[140][140];
 int newline;
 int subdeal[35][3];
 char ntf[3]={'n','t','f'};

//incialization
 for(i=0; i<140; i++)
  for(j=0; j<7; j++)
	{deal[i][j]=0; }
// for(i=0;i<140;i++)
//  for(j=0;j<140;j++)
//	{anne[i][j]=0;bill[i][j]=0;cath[i][j]=0;}
//generate the states with valuation
for(d0=0; d0<7; d0++)
 for(d1=d0+1; d1<7; d1++)
  for(d2=d1+1; d2<7; d2++)
	for(d3=0; d3<7; d3++)
	 { if (d3==d0 ||d3==d1 ||d3==d2)  continue;
	   for(d4=d3+1; d4<7; d4++)
	    { if (d4==d0 ||d4==d1 ||d4==d2)  continue;
	      for(d5=d4+1;d5<7;d5++)
	       { if (d5==d0 ||d5==d1 ||d5==d2)  continue;
		 for(d6=0;d6<7;d6++)
		  { if (d6==d0||d6==d1||d6==d2||d6==d3||d6==d4||d6==d5)  continue;
		    deal[d_index][0]=d0;
		    deal[d_index][1]=d1;
		    deal[d_index][2]=d2;
		    deal[d_index][3]=d3;
		    deal[d_index][4]=d4;
		    deal[d_index][5]=d5;
		    deal[d_index][6]=d6;
		    d_index++;
		    //printf("%d,%d,%d,%d,%d,%d,%d,%d\n",d_index-1,d0,d1,d2,d3,d4,d5,d6);
		  }
		}
	     }
	 }

//generate subdeal for Anne and Bill
d_index=0;
for(d0=0; d0<7; d0++)
 for(d1=d0+1; d1<7; d1++)
  for(d2=d1+1; d2<7; d2++)
	{ subdeal[d_index][0]=d0;
	  subdeal[d_index][1]=d1;
	  subdeal[d_index][2]=d2;
	//printf("%d,%d,%d,%d\n",d_index,d0,d1,d2);
		  d_index++;
	}

printf("--Russian Cards in MCMAS (v0.6)\n");
printf("--three agents Anne,Bill,Cath, Seven cards 0-6.\n");
printf("--Assume each agent only knows her own card.\n");
printf("--step 1 Dealing 3 cards to Anne, 3 cards to Bill, 1 card to Cath. \n");
printf("--step 2 Anne makes an announcement.\n");
printf("--step 3 Bill makes an announcement.\n\n");

printf("--Now We verify that the following is a solution for Russian Cards problem:");
printf("--Suppose the actual deal is 012.345.6 and\n");
printf("--Anne announces \"my hand is in {012,034,056,135,246}\".\n");
printf("--Bill announces \"Cath has card 6\".\n");
printf("--We verify this is a solution for Russian Cards problem.\n");


printf("--variable for agent Anne: axxxnn\n");
printf("--var1-3: axxx the cards that Anne holds.\n");
printf("--var4: n, t, f for A announces nothing, true, false respectively\n");
printf("--var5: n, t, f for B announces nothing, true, false respectively\n");
printf("--Similar for Bill. For Cath, we use cxnn\n");
printf("--We also introduce an enviroment agent Env which encodes the actual deals.\n\n");


printf("Agent Anne\n");
printf("Lstate = { annnnn,\n");
newline=0;
for(i=0; i<35; i++)
  for(j=0; j<3; j++)
    for(k=0; k<3; k++)
    {	if (i==34 && j==2 && k==2 ) 
	printf("a%d%d%d%c%c};\n",subdeal[i][0],subdeal[i][1],subdeal[i][2],ntf[j],ntf[k]);
	else  
	printf("a%d%d%d%c%c,",subdeal[i][0],subdeal[i][1],subdeal[i][2],ntf[j],ntf[k]);
	newline++;
	if(newline%8==0) printf("\n");
    }


printf("Lgreen = { annnnn,\n");
newline=0;
for(i=0; i<35; i++)
  for(j=0; j<3; j++)
    for(k=0; k<3; k++)
    {	if (i==34 && j==2 && k==2 ) 
	printf("a%d%d%d%c%c};\n",subdeal[i][0],subdeal[i][1],subdeal[i][2],ntf[j],ntf[k]);
	else  
	printf("a%d%d%d%c%c,",subdeal[i][0],subdeal[i][1],subdeal[i][2],ntf[j],ntf[k]);
	newline++;
	if(newline%8==0) printf("\n");
    }


printf("\n Action ={null, Announce};\n\n");

printf("Protocol: annnnn:{null};\n");
newline=0;
for(i=0; i<35; i++)
  for(j=0; j<3; j++)
    for(k=0; k<3; k++)
    {	printf("a%d%d%d%c%c:{null};",subdeal[i][0],subdeal[i][1],subdeal[i][2],ntf[j],ntf[k]);
	newline++;
	if(newline%5==0) printf("\n");
    }
printf("end Protocol\n\n");

printf("Ev:\n");
printf("-----1 Reveal cards to Anne:annnnn->axxxnn------\n");
for(j=0; j<35; j++)
 {
	printf("a%d%d%dnn if (Lstate=annnnn and (\n",subdeal[j][0],subdeal[j][1],subdeal[j][2]);
	newline=0;//a stupid error newline==0;
	for(i=0; i<140; i++)
	{  
	   if ( deal[i][0]==subdeal[j][0] && deal[i][1]==subdeal[j][1] 
		&& deal[i][2]==subdeal[j][2]) 
              {	printf( " Env.Lstate=e%d%d%d%d%d%d%d ",
		deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
		newline++;
		//printf("newline= \n%d",newline);
	      	if (newline==4) printf ("));\n\n");
	  	  else printf(" or ");

              }
        }

  }

printf("\n-----2 Anne's Announcement:axxxnn->axxxxn------\n");
for(i=0; i<35; i++)
{ if ( (subdeal[i][0]==0 && subdeal[i][1]==1 && subdeal[i][2]==2) ||
       (subdeal[i][0]==0 && subdeal[i][1]==3 && subdeal[i][2]==4) ||
       (subdeal[i][0]==0 && subdeal[i][1]==5 && subdeal[i][2]==6) ||
       (subdeal[i][0]==1 && subdeal[i][1]==3 && subdeal[i][2]==5) ||
       (subdeal[i][0]==2 && subdeal[i][1]==4 && subdeal[i][2]==6) )
	printf("a%d%d%dtn if (Lstate=a%d%d%dnn);\n",
		subdeal[i][0],subdeal[i][1],subdeal[i][2],
		subdeal[i][0],subdeal[i][1],subdeal[i][2]);
  else
	printf("a%d%d%dfn if (Lstate=a%d%d%dnn);\n",
		subdeal[i][0],subdeal[i][1],subdeal[i][2],
		subdeal[i][0],subdeal[i][1],subdeal[i][2]);
}


printf("\n-----2 Bill's Announcement:axxxxn->axxxxx------\n");
/*
for(i=0; i<140; i++)
{ if ( (deal[i][0]==0 && deal[i][1]==1 && deal[i][2]==2) ||
       (deal[i][0]==0 && deal[i][1]==3 && deal[i][2]==4) ||
       (deal[i][0]==0 && deal[i][1]==5 && deal[i][2]==6) ||
       (deal[i][0]==1 && deal[i][1]==3 && deal[i][2]==5) ||
       (deal[i][0]==2 && deal[i][1]==4 && deal[i][2]==6) )
    { if (deal[i][6]==6) 
	    printf("a%d%d%dtt if (Lstate=a%d%d%dtn and Env.Lstate=e%d%d%d%d%d%d%d);\n",
		deal[i][0],deal[i][1],deal[i][2],
		deal[i][0],deal[i][1],deal[i][2],
		deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
	else printf("a%d%d%dtf if (Lstate=a%d%d%dtn and Env.Lstate=e%d%d%d%d%d%d%d);\n",
		deal[i][0],deal[i][1],deal[i][2],
		deal[i][0],deal[i][1],deal[i][2],
		deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
    }
  //now, we don't care the states which do not survive from Anne's announcement.
}
*/

printf("a012tt if (Lstate=a012tn and Env.Lstate=e0123456);\n");

printf("a012tf if (Lstate=a012tn and ( \n");
printf("Env.Lstate=e0123465 or Env.Lstate=e0123564 or Env.Lstate=e0124563));\n");

printf("a034tt if (Lstate=a034tn and Env.Lstate=e0341256);\n");

printf("a034tf if (Lstate=a034tn and (\n");
printf("Env.Lstate=e0341265 or Env.Lstate=e0341562 or Env.Lstate=e0342561));\n");

printf("a056tf if (Lstate=a056tn and (\n");
printf("Env.Lstate=e0561234 or Env.Lstate=e0561243 or\n");
printf("Env.Lstate=e0561342 or Env.Lstate=e0562341));\n");

printf("a135tt if (Lstate=a135tn and Env.Lstate=e1350246);\n");

printf("a135tf if (Lstate=a135tn and (\n");
printf("Env.Lstate=e1350264 or Env.Lstate=e1350462 or Env.Lstate=e1352460));\n");

printf("a246tf if (Lstate=a246tn and (\n");
printf("Env.Lstate=e2460135 or Env.Lstate=e2460153 or \n");
printf("Env.Lstate=e2460351 or Env.Lstate=e2461350));\n");

printf("\n");

printf("\nend Ev\n");
printf("end Agent\n");
//end of Agent Anne

printf("Agent Bill\n");
printf("Lstate = { bnnnnn,\n");
newline=0;
for(i=0; i<35; i++)
  for(j=0; j<3; j++)
    for(k=0; k<3; k++)
    {	if (i==34 && j==2 && k==2 ) 
	printf("b%d%d%d%c%c};\n",subdeal[i][0],subdeal[i][1],subdeal[i][2],ntf[j],ntf[k]);
	else  
	printf("b%d%d%d%c%c,",subdeal[i][0],subdeal[i][1],subdeal[i][2],ntf[j],ntf[k]);
	newline++;
	if(newline%8==0) printf("\n");
    }


printf("Lgreen = { bnnnnn,\n");
newline=0;
for(i=0; i<35; i++)
  for(j=0; j<3; j++)
    for(k=0; k<3; k++)
    {	if (i==34 && j==2 && k==2 ) 
	printf("b%d%d%d%c%c};\n",subdeal[i][0],subdeal[i][1],subdeal[i][2],ntf[j],ntf[k]);
	else  
	printf("b%d%d%d%c%c,",subdeal[i][0],subdeal[i][1],subdeal[i][2],ntf[j],ntf[k]);
	newline++;
	if(newline%8==0) printf("\n");
    }


printf("\n Action ={null, Announce};\n\n");

printf("Protocol: bnnnnn:{null};\n");
newline=0;
for(i=0; i<35; i++)
  for(j=0; j<3; j++)
    for(k=0; k<3; k++)
    {	printf("b%d%d%d%c%c:{null};",subdeal[i][0],subdeal[i][1],subdeal[i][2],ntf[j],ntf[k]);
	newline++;
	if(newline%5==0) printf("\n");
    }
printf("end Protocol\n\n");

printf("Ev:\n");
printf("-----1 Reveal cards to Bill:bnnnnn->bxxxnn------\n");
for(j=0; j<35; j++)
 {
	printf("b%d%d%dnn if (Lstate=bnnnnn and (\n",subdeal[j][0],subdeal[j][1],subdeal[j][2]);
	newline=0;//a stupid error newline==0;
	for(i=0; i<140; i++)
	{  
	   if ( deal[i][3]==subdeal[j][0] && deal[i][4]==subdeal[j][1] 
		&& deal[i][5]==subdeal[j][2]) 
              {	printf( " Env.Lstate=e%d%d%d%d%d%d%d ",
		deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
		newline++;
		//printf("newline= \n%d",newline);
	      	if (newline==4) printf ("));\n\n");
	  	  else printf(" or ");

              }
        }

  }


printf("\n-----2 Anne's Announcement:bxxxnn->bxxxxn------\n");
for (j=0; j<35; j++)
{
	lt=0; lf=0;
	for(i=0; i<140; i++)
	{ if(subdeal[j][0]==deal[i][3] && subdeal[j][1]==deal[i][4] &&
             subdeal[j][2]==deal[i][5]) 
	  { if ( (deal[i][0]==0 && deal[i][1]==1 && deal[i][2]==2) ||
       	       (deal[i][0]==0 && deal[i][1]==3 && deal[i][2]==4) ||
       	       (deal[i][0]==0 && deal[i][1]==5 && deal[i][2]==6) ||
       	       (deal[i][0]==1 && deal[i][1]==3 && deal[i][2]==5) ||
       	       (deal[i][0]==2 && deal[i][1]==4 && deal[i][2]==6) )
			lt++;//announcement is true

	     else 	lf++;//announcement is false
	  }
	}
	if (lt!=0)
	  { printf("b%d%d%dtn if (Lstate=b%d%d%dnn and (\n", 
		subdeal[j][0],subdeal[j][1],subdeal[j][2],
		subdeal[j][0],subdeal[j][1],subdeal[j][2]);
	   for(i=0;i<140;i++)
		if ((subdeal[j][0]==deal[i][3] && subdeal[j][1]==deal[i][4] &&
             	     subdeal[j][2]==deal[i][5]) && 
	     	   ((deal[i][0]==0 && deal[i][1]==1 && deal[i][2]==2) ||
       	       	    (deal[i][0]==0 && deal[i][1]==3 && deal[i][2]==4) ||
       	       	    (deal[i][0]==0 && deal[i][1]==5 && deal[i][2]==6) ||
       	       	    (deal[i][0]==1 && deal[i][1]==3 && deal[i][2]==5) ||
       	       	    (deal[i][0]==2 && deal[i][1]==4 && deal[i][2]==6)) )
		 { lt--;
			if(lt==0) printf("Env.Lstate=e%d%d%d%d%d%d%d));\n",
		  deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
			else printf("Env.Lstate=e%d%d%d%d%d%d%d or ",
		  deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
		 }
	   }

	 if (lf!=0)
	  { printf("b%d%d%dfn if (Lstate=b%d%d%dnn and (\n", 
		subdeal[j][0],subdeal[j][1],subdeal[j][2],
		subdeal[j][0],subdeal[j][1],subdeal[j][2]);
	   for(i=0;i<140;i++)
		if ((subdeal[j][0]==deal[i][3] && subdeal[j][1]==deal[i][4] &&
             	     subdeal[j][2]==deal[i][5]) && 
	     	   ((deal[i][0]!=0 || deal[i][1]!=1 || deal[i][2]!=2) &&
       	       	    (deal[i][0]!=0 || deal[i][1]!=3 || deal[i][2]!=4) &&
       	       	    (deal[i][0]!=0 || deal[i][1]!=5 || deal[i][2]!=6) &&
       	       	    (deal[i][0]!=1 || deal[i][1]!=3 || deal[i][2]!=5) &&
       	       	    (deal[i][0]!=2 || deal[i][1]!=4 || deal[i][2]!=6)) )
		 { 	lf--;
			if(lf==0) printf("Env.Lstate=e%d%d%d%d%d%d%d));\n",
		  deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
			else printf("Env.Lstate=e%d%d%d%d%d%d%d or ",
		  deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
		 }

	   }
}


printf("\n-----2 Bill's Announcement:bxxxxn->bxxxxx------\n");
for(i=0; i<140; i++)
{ if ( (deal[i][0]==0 && deal[i][1]==1 && deal[i][2]==2) ||
       (deal[i][0]==0 && deal[i][1]==3 && deal[i][2]==4) ||
       (deal[i][0]==0 && deal[i][1]==5 && deal[i][2]==6) ||
       (deal[i][0]==1 && deal[i][1]==3 && deal[i][2]==5) ||
       (deal[i][0]==2 && deal[i][1]==4 && deal[i][2]==6) )
    { if (deal[i][6]==6) 
	    printf("b%d%d%dtt if (Lstate=b%d%d%dtn and Env.Lstate=e%d%d%d%d%d%d%d);\n",
		deal[i][3],deal[i][4],deal[i][5],
		deal[i][3],deal[i][4],deal[i][5],
		deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
	else printf("b%d%d%dtf if (Lstate=b%d%d%dtn and Env.Lstate=e%d%d%d%d%d%d%d);\n",
		deal[i][3],deal[i][4],deal[i][5],
		deal[i][3],deal[i][4],deal[i][5],
		deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
    }
  //now, we don't care the states which do not survive from Anne's announcement.
}

printf("\nend Ev\n");
printf("end Agent\n");
//end of Agent Bill

printf("Agent Cath\n");
printf("Lstate = { cnnn,\n");
newline=0;
for(i=0; i<7; i++)
  for(j=0; j<3; j++)
    for(k=0; k<3; k++)
    {	if (i==6 && j==2 && k==2 ) 
	printf("c%d%c%c};\n",i,ntf[j],ntf[k]);
	else  
	printf("c%d%c%c,",i,ntf[j],ntf[k]);
	newline++;
	if(newline%8==0) printf("\n");
    }


printf("Lgreen = { cnnn,\n");
newline=0;
for(i=0; i<7; i++)
  for(j=0; j<3; j++)
    for(k=0; k<3; k++)
    {	if (i==6 && j==2 && k==2 ) 
	printf("c%d%c%c};\n",i,ntf[j],ntf[k]);
	else  
	printf("c%d%c%c,",i,ntf[j],ntf[k]);
	newline++;
	if(newline%8==0) printf("\n");
    }


printf("\n Action ={null};\n\n");

printf("Protocol: cnnn:{null};\n");
newline=0;
for(i=0; i<7; i++)
  for(j=0; j<3; j++)
    for(k=0; k<3; k++)
    {		printf("c%d%c%c:{null};",i,ntf[j],ntf[k]);
	newline++;
	if(newline%5==0) printf("\n");
    }
printf("\n end Protocol\n\n");

printf("Ev:\n");
printf("-----1 Reveal cards to Cath:cnnn->cxnn------\n");
for(j=0;j<7;j++)
 { k=20;
   printf("c%dnn if (Lstate=cnnn and (\n",j);
   for(i=0; i<140; i++)
	{ if (j==deal[i][6]) 
	    {printf("Env.Lstate=e%d%d%d%d%d%d%d ",
		deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
	  	k--;
	  	if(k==0) printf ("));\n");
	  	else {printf(" or "); if (k%4==0) printf("\n");}
            }
        }
  }

printf("\n-----2 Anne's Announcement:cxnn->cxxn------\n");


for (j=0; j<7; j++)
{
	lt=0; lf=0;
	for(i=0; i<140; i++)
	{ if(j==deal[i][6])
	  { if ( (deal[i][0]==0 && deal[i][1]==1 && deal[i][2]==2) ||
       	       (deal[i][0]==0 && deal[i][1]==3 && deal[i][2]==4) ||
       	       (deal[i][0]==0 && deal[i][1]==5 && deal[i][2]==6) ||
       	       (deal[i][0]==1 && deal[i][1]==3 && deal[i][2]==5) ||
       	       (deal[i][0]==2 && deal[i][1]==4 && deal[i][2]==6) )
			lt++;//announcement is true

	     else 	lf++;//announcement is false
	  }
	}
	if (lt!=0)
	  { printf("c%dtn if (Lstate=c%dnn and (\n", j,j);
	   for(i=0;i<140;i++)
		if (deal[i][6]==j && 
	     	   ((deal[i][0]==0 && deal[i][1]==1 && deal[i][2]==2) ||
       	       	    (deal[i][0]==0 && deal[i][1]==3 && deal[i][2]==4) ||
       	       	    (deal[i][0]==0 && deal[i][1]==5 && deal[i][2]==6) ||
       	       	    (deal[i][0]==1 && deal[i][1]==3 && deal[i][2]==5) ||
       	       	    (deal[i][0]==2 && deal[i][1]==4 && deal[i][2]==6)) )
		 { lt--;
			if(lt==0) printf("Env.Lstate=e%d%d%d%d%d%d%d));\n",
		  deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
			else {printf("Env.Lstate=e%d%d%d%d%d%d%d or ",
		  deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
			      if(lt%4==0) printf("\n");}
		 }
	   }

	 if (lf!=0)
	  { printf("c%dfn if (Lstate=c%dnn and (\n", j,j);
	   for(i=0;i<140;i++)
		if (deal[i][6]==j && 
	     	   ((deal[i][0]!=0 || deal[i][1]!=1 || deal[i][2]!=2) &&
       	       	    (deal[i][0]!=0 || deal[i][1]!=3 || deal[i][2]!=4) &&
       	       	    (deal[i][0]!=0 || deal[i][1]!=5 || deal[i][2]!=6) &&
       	       	    (deal[i][0]!=1 || deal[i][1]!=3 || deal[i][2]!=5) &&
       	       	    (deal[i][0]!=2 || deal[i][1]!=4 || deal[i][2]!=6)) )
		 { 	lf--;
			if(lf==0) printf("Env.Lstate=e%d%d%d%d%d%d%d));\n",
		  deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
			else {printf("Env.Lstate=e%d%d%d%d%d%d%d or ",
		  deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
			      if(lf%4==0) printf("\n");}
		 }

	   }
}

printf("\n-----2 Bill's Announcement:cxxn->cxxx------\n");
for(i=0; i<7; i++)
{ if ( i==6 ) printf("c6tt if (Lstate=c6tn);\n");
  else printf("c%dtf if (Lstate=c%dtn);\n",i,i);
}

printf("\n end Ev\n");
printf("end Agent\n");
//end of Agent Cath

printf("");
printf("Agent Env\n");
printf("Lstate={\n");
printf("--Introduce 7 variables for the card deal\n");
newline=0;
for (i=0;i<140;i++)
{ if (i==139) printf("e%d%d%d%d%d%d%d};\n",
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
  else printf("e%d%d%d%d%d%d%d,",
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
newline++;
if (newline%6==0) printf("\n");
}

printf("Lgreen={\n");
newline=0;
for (i=0;i<140;i++)
{if (i==139) printf("e%d%d%d%d%d%d%d};\n",
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
  else printf("e%d%d%d%d%d%d%d,",
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);

newline++;
if (newline%6==0) printf("\n");
}


printf("\nAction={null};\n\n");

printf("Protocol:\n");
newline=0;
for (i=0;i<140;i++)
{printf("e%d%d%d%d%d%d%d:{null};",
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
newline++;
if (newline%4==0) printf("\n");
}
printf("\nend Protocol\n");
printf("Ev:\n");

for (i=0;i<140;i++)
 printf("e%d%d%d%d%d%d%d if (Lstate=e%d%d%d%d%d%d%d);\n",
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6],
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
	
printf("end Ev\n");	
printf("end Agent\n");	

printf("\n");

//Evaluation part
printf("Evaluation\n");


for(j=0;j<7;j++)
{
printf("a%d if (\n",j); 

k=0;
for(i=0;i<140;i++)
 if (deal[i][0]==j || deal[i][1]==j || deal[i][2]==j) 
  { k++; }//k records the number of deals

newline=0;
for(i=0;i<140;i++)
 if (deal[i][0]==j || deal[i][1]==j || deal[i][2]==j) 
  {	k--;
	if (k!=0) 
	  printf("Env.Lstate = e%d%d%d%d%d%d%d or ",
	    deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
	else 
	  printf("Env.Lstate = e%d%d%d%d%d%d%d);\n",
	    deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
	newline++;
	if (newline%3==0) printf("\n");  
  }
printf("\n");
}

for(j=0;j<7;j++)
{
printf("b%d if (\n",j); 

for(i=0;i<140;i++)
 if (deal[i][3]==j || deal[i][4]==j || deal[i][5]==j) 
  { k++; }//k records the number of deals

newline=0;
for(i=0;i<140;i++)
 if (deal[i][3]==j || deal[i][4]==j || deal[i][5]==j) //different from Anne
  {	k--;
	if (k!=0) 
	  printf("Env.Lstate = e%d%d%d%d%d%d%d or ",
	    deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
	else 
	  printf("Env.Lstate = e%d%d%d%d%d%d%d);\n",
	    deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
	newline++;
	if (newline%3==0) printf("\n");  
  }
printf("\n");
}

for(j=0;j<7;j++)
{
printf("c%d if (\n",j); 

for(i=0;i<140;i++)
 if (deal[i][6]==j ) 
  { k++; }//k records the number of deals

newline=0;
for(i=0;i<140;i++)
 if (deal[i][6]==j) //different from Anne/Bill
  {	k--;
	if (k!=0) 
	  printf("Env.Lstate = e%d%d%d%d%d%d%d or ",
	    deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
	else 
	  printf("Env.Lstate = e%d%d%d%d%d%d%d);\n",
	    deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
	newline++;
	if (newline%3==0) printf("\n");  
  }
printf("\n");
}

printf("init if (\n");
printf("(Anne.Lstate=annnnn and Bill.Lstate=bnnnnn and Cath.Lstate=cnnn)\n");
printf("and\n");
printf("(");
newline=0;
for (i=0;i<139;i++)
{ printf("Env.Lstate=e%d%d%d%d%d%d%d or ",
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
  newline++;
  if (newline%3==0) printf("\n");
}
printf("Env.Lstate=e%d%d%d%d%d%d%d));\n",
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);


printf("ab_d0123456 if (Anne.Lstate=a012tt and Bill.Lstate=b345tt and Cath.Lstate=c6tt and \n");
printf("		Env.Lstate=e0123456);\n");

printf("a_d0123456 if (Anne.Lstate=a012tn and Bill.Lstate=b345tn and Cath.Lstate=c6tn and \n");
printf("		Env.Lstate=e0123456);\n");
printf("n_d0123456 if (Anne.Lstate=a012nn and Bill.Lstate=b345nn and Cath.Lstate=c6nn and \n");
printf("		Env.Lstate=e0123456);\n");
printf("init0123456 if (Anne.Lstate=annnnn and Bill.Lstate=bnnnnn and Cath.Lstate=cnnn and \n");
printf("		Env.Lstate=e0123456);\n");

printf("\n");
printf("\n");

printf("end Evaluation\n\n");

printf("InitStates \n");
printf("(Anne.Lstate=annnnn and Bill.Lstate=bnnnnn and Cath.Lstate=cnnn)\n");
printf("and\n");
printf("(");
newline=0;
for (i=0;i<139;i++)
{ printf("Env.Lstate=e%d%d%d%d%d%d%d or ",
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
  newline++;
  if (newline%3==0) printf("\n");
}
printf("Env.Lstate=e%d%d%d%d%d%d%d);\n",
	deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);

printf("end InitStates\n\n");

printf("Groups\n");
printf("	AB={Anne,Bill};\n");
printf("	AC={Anne,Cath};\n");
printf("	BC={Bill, Cath};\n");
printf("	ABC={Anne, Bill, Cath};\n");
printf("end Groups\n");


printf("Formulae\n");

printf("--We take 012.345.6 as the actual deal. \n");
printf("--Then checking some postconditions of (A)nne and (B)ill's announcements.\n");
printf("--prefix a_ denotes After Anne's announcement\n");
printf("--prefix ab_ denotes After Anne and Bill's announcements\n");
printf("\n");
printf("--After A's announcement, Bill know Cath holds 6.\n");
printf("a_d0123456 -> K(Bill, c6);\n");
printf("\n");
printf("--After A's announcement, it is not the case that a_knows_bs.\n");
printf("a_d0123456 -> !(\n");
printf("( K(Anne,b0) or K(Anne,!b0) ) and\n");
printf("( K(Anne,b1) or K(Anne,!b1) ) and \n");
printf("( K(Anne,b2) or K(Anne,!b2) ) and \n");
printf("( K(Anne,b3) or K(Anne,!b3) ) and \n");
printf("( K(Anne,b4) or K(Anne,!b4) ) and \n");
printf("( K(Anne,b5) or K(Anne,!b5) ) and \n");
printf("( K(Anne,b6) or K(Anne,!b6) ) );\n");
printf("\n");
printf("--After A and B's announcement, \n");
printf("--it is common knowledge among Anne and Bill that a_knows_bs.\n");
printf("ab_d0123456 -> GCK(AB, (\n");
printf("( K(Anne,b0) or K(Anne,!b0) ) and\n");
printf("( K(Anne,b1) or K(Anne,!b1) ) and \n");
printf("( K(Anne,b2) or K(Anne,!b2) ) and \n");
printf("( K(Anne,b3) or K(Anne,!b3) ) and \n");
printf("( K(Anne,b4) or K(Anne,!b4) ) and \n");
printf("( K(Anne,b5) or K(Anne,!b5) ) and \n");
printf("( K(Anne,b6) or K(Anne,!b6) ) ));\n");
printf("\n");
printf("--After A's announcement, it is common knowledge that cignorant:\n");
printf("a_d0123456 -> GCK(ABC,(\n");
printf(" !c0-> ( !K(Cath,a0) and !K(Cath,b0) ) and\n");
printf(" !c1-> ( !K(Cath,a1) and !K(Cath,b1) ) and\n");
printf(" !c2-> ( !K(Cath,a2) and !K(Cath,b2) ) and\n");
printf(" !c3-> ( !K(Cath,a3) and !K(Cath,b3) ) and\n");
printf(" !c4-> ( !K(Cath,a4) and !K(Cath,b4) ) and\n");
printf(" !c5-> ( !K(Cath,a5) and !K(Cath,b5) ) and\n");
printf(" !c6-> ( !K(Cath,a6) and !K(Cath,b6) ) ));\n");
printf("\n");
printf("--After B's announcement, it is common knowledge that cignorant.\n");
printf("ab_d0123456 -> GCK(ABC,(\n");
printf(" !c0-> ( !K(Cath,a0) and !K(Cath,b0) ) and\n");
printf(" !c1-> ( !K(Cath,a1) and !K(Cath,b1) ) and\n");
printf(" !c2-> ( !K(Cath,a2) and !K(Cath,b2) ) and\n");
printf(" !c3-> ( !K(Cath,a3) and !K(Cath,b3) ) and\n");
printf(" !c4-> ( !K(Cath,a4) and !K(Cath,b4) ) and\n");
printf(" !c5-> ( !K(Cath,a5) and !K(Cath,b5) ) and\n");
printf(" !c6-> ( !K(Cath,a6) and !K(Cath,b6) ) ));\n");


printf("\n");
printf("\n");
printf("end Formulae\n");


}