/*this program generates the epistemic model for Russian card problem in DEMO*/
#include <stdio.h>
int main()
{
 int d0,d1,d2,d3,d4,d5,d6;
 int i,j,k,d_index=0;
 int deal[140][7],anne[140][140],bill[140][140],cath[140][140];
 int newline;

//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++;
		  }
		}
	     }
	 }


//find out the accessible relation.
for(i=0;i<140;i++)
  for(j=0;j<140;j++)
   { 
    if (deal[i][0]==deal[j][0] &&deal[i][1]==deal[j][1] && deal[i][2]==deal[j][2]) 
		anne[i][j]=1; 
    if (deal[i][3]==deal[j][3] &&deal[i][4]==deal[j][4] && deal[i][5]==deal[j][5]) 
		bill[i][j]=1; 
    if (deal[i][6]==deal[j][6]) 
		cath[i][j]=1; 
   }

//Now output the epistemic model

printf("rus :: EpistM\n");
printf("rus = (Pmod [0..139] val acc [0])\n");
printf(" where\n");
printf(" val = [\n"); 
printf("	"); 

//output states, eg. (0  ,[P 0,P 1,P 2,Q 3,Q 4,Q 5,R 6]),
newline=1;
for(i=0;i<139;i++)
{
  printf("(%3d,[P %d,P %d,P %d,Q %d,Q %d,Q %d,R %d]),",
	i,deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);
  if (newline%2 == 0) printf("\n	");
  newline++;
}
printf("(%3d,[P %d,P %d,P %d,Q %d,Q %d,Q %d,R %d])]\n",
	i,deal[i][0],deal[i][1],deal[i][2],deal[i][3],deal[i][4],deal[i][5],deal[i][6]);

//output relations, eg.	(a, 0, 0),
newline=1;
printf(" acc = [ \n"); 	
printf("	"); 	
for(i=0;i<140;i++)
  for(j=0;j<140;j++)
	if (anne[i][j]==1) 
		{ printf("(a,%d,%d),",i,j);
	  	  if (newline%6 == 0) printf("\n	");
	  	  newline++;
		}
	
for(i=0;i<140;i++)
  for(j=0;j<140;j++)
	if (bill[i][j]==1) 
	  {printf("(b,%d,%d),",i,j);
	   if (newline%6 == 0) printf("\n	");
	   newline++;
	  }

	
for(i=0;i<140;i++)
  for(j=0;j<140;j++)
        if (i==139 && j==139) printf("(c,%d,%d)]",i,j);
	else if (cath[i][j]==1) 
		{printf("(c,%d,%d),",i,j);
		if (newline%6 == 0) printf("\n	");
		newline++;
		}


}