/ Defining Principal known keys table
 
static struct ky {
       char *ID1;
       char *ID2;
       int  Inv;
       };
 
typedef struct ky  Keys;
 
struct prnc {
       char *ID;
       int  nk;
       Keys kys[0];
       };
 
static struct prnc principal_know_key[0];
 
 
//********************************************************
// Traverse the tree to check a number of constraints
//********************************************************
 
void traverse_sem(Ast a){
	Ast *t;
	int i;
	int n;
	int sflag;
	int rflag;
	char *message_sr_id;
	char *message_rc_id;
 
 
    switch(NKIND(a))
    {
		case PROTOCOL: 
			t = PROTOCOL_PRINCIPALS(a);
			num_principals = PROTOCOL_NB_PRINCIPALS(a);
			fprintf(outS,"\tNumber: %d\n", num_principals);
			// Traverse Principals
                                      for (i=0;i<num_principals;i++) 
				traverse_sem(t[i]);
			// Ensure that at least two principals are present
                                       fprintf(outS,"\tViolations: ");
                                      if (principal_counter < 2 )
                                         printf("Yes \n\t\t Less than two principals are   declared.\n\n");
                                     else
                                     if (num_principals > principal_counter)
                                         fprintf(outS,"\nExcessive declaration of principals");
                                     else
                                         fprintf(outS," No \n\n");
 
			// Traverse Messages
			fprintf(outS,"Messages:\n");
                                      num_messages = PROTOCOL_NB_MESSAGES(a);
			fprintf(outS,"\tNumber: %d\n", num_messages);
			t = PROTOCOL_MESSAGES(a);
			for (i=0;i<num_messages;i++)
				traverse_sem(t[i]);
 
 
            break;
 
        case PRINCIPAL:
            principals_list[principal_counter]= PRINCIPAL_ID(a); 
            principal_know_key[principal_counter].ID = PRINCIPAL_ID(a);
            printf("\n Principal Name: %s", principal_know_key[principal_counter].ID); //delete here
            fprintf(outS,"\tPrincipal %d : %s \n", principal_counter+1, principals_list[principal_counter]);
            t = PRINCIPAL_KNOW(a);
            n = PRINCIPAL_NB_KNOWS(a);
            principal_know_key[principal_counter].nk= n;
            for (i=0;i<n;i++)
          		traverse_sem(t[i]);
			key_counter =0;
			++principal_counter; 
			break;
 
		case KEY:
             printf("\n\t Key # %d", key_counter+1);
             principal_know_key[principal_counter].kys[key_counter].ID1 = KEY_ID1(a);
             printf("\n\t\t\t ID1 : %s", principal_know_key[principal_counter].kys[key_counter].ID1);
             principal_know_key[principal_counter].kys[key_counter].ID2 = KEY_ID2(a);
             printf("\n\t\t\t ID2 : %s", principal_know_key[principal_counter].kys[key_counter].ID2);
             principal_know_key[principal_counter].kys[key_counter].Inv = KEY_INV(a);
             printf("\n\t\t\t Inv : %d", principal_know_key[principal_counter].kys[key_counter].Inv);
             ++key_counter;
        break;
 
 
        case MESSAGE:
            t = MESSAGE_SENT_DATA(a);
	n = MESSAGE_NB_SENT_DATA(a);
            ++message_counter;
            fprintf(outS,"\n\tMessage %d\n", message_counter);
 
            message_sr_id = MESSAGE_SENDER_ID(a);
            fprintf(outS,"\t\tSender: %s\n", message_sr_id);
            message_rc_id = MESSAGE_RECEIVER_ID(a);
            fprintf(outS,"\t\tReceiver: %s\n",message_rc_id);
 
            fprintf(outS,"\t\tViolations: ");
 
            //Check for sender validity
            sflag = PrincipalPresense("Sender", message_sr_id,0);
 
            //Check for reciever validity            
            rflag = PrincipalPresense("Receiver", message_rc_id,sflag);
 
            if ((sflag ==0) && (rflag == 0))
               fprintf(outS," No \n\n");
 
            for (i=0;i<n;i++){
	  traverse_sem(t[i]);
                }   
 
	break;
 
    }
}
 
 
/ A test function to display the contents of the array principal_know_key
 
void printkey(){
     int i;
     int j;
     int numkeys;
 
     for(i =0; i < principal_counter ; i++)
     {
           printf("\n Principal Name: %s", principal_know_key[i].ID);
           numkeys = principal_know_key[i].nk;
           printf("\n\t Number of known keys: %d", numkeys);
 
           for (j=0; j < numkeys ; j++)
               {
                     printf("\n\t\t Key # %d: ", j+1);
                     printf("\n\t\t\t ID1 : %s", principal_know_key[i].kys[j].ID1);
                     printf("\n\t\t\t ID2 : %s", principal_know_key[i].kys[j].ID2);
                     printf("\n\t\t\t Inv : %d", principal_know_key[i].kys[j].Inv);
                }
     }
}