/* Copyright (c) 2001 by the Institute for Computer Science,               */
/* Alberts-Ludwigs-University of Freiburg, Germany.                        */
/* All Rights Reserved.  This software is for educational purposes only.   */
/* Permission is given to distribute this code provided that this intro-   */
/* ductory message is not removed and no monies are exchanged.             */
/* No guarantee is expressed or implied by the distribution of this code.  */
/* Software written by Alberto Lluch Lafuente and Stefan Edelkamp.         */
/* References:                                                             */
/* - Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue,              */
/*   Directed Explicit Model Checking with HSF-SPIN, to appear in:         */
/*   Proc. 8th International SPIN Workshop on Model Checking Software,     */
/*   Springer LNCS 2057, Toronto, May 2001                                 */
/* - Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue,              */
/*   Protocol Verification with Heuristic Search,                          */
/*   Proc. AAAI Spring Symposium on Model-Based Validation of Inteligence, */
/*   AAAI, Stanford, April 2001.                                           */
/* Send bug-reports or questions to: lafuente@informatik.uni-freiburg.de   */

#ifndef _PROTOCOL_
#define _PROTOCOL_

/* Includes */
#include <stdio.h>
#include <global.h>
#include <goals.h>
#include <heuristics.h>

class Protocol{
public:
  char trail_name[40]; /* Name of trail file. */
  Protocol_Goal *My_Goal; /* Error to be checked. */
  Protocol_Heuristic *My_Heuristic; /* Heuristic estimate to be used. */
  int atomic_transitions;
  int rendezvous_boq_states;
  FILE *trail_file;
  
  Protocol(int maxh) {
     My_Goal=new Protocol_Goal;
     My_Heuristic=new Protocol_Heuristic(maxh);
     if(Selected_Heuristic==TRAIL_FILE){
       sprintf(trail_name,"%s.trail",Source);
       printf("Opening trail file %s...\n",trail_name);
       trail_file=fopen(trail_name,"r");
       if(!trail_file){
	 printf("Error! Unable to open trail file %s\n",trail_name);
	 exit(0);
       }
     }

     atomic_transitions=0;
     rendezvous_boq_states=0;

     construct_lextok_wood(); /* Construct lextok trees for each transition. */
     run(); /* Let spin's code perform some things (tables, etc.) . */

     /*     printf("Initializing heuristic...\n");*/
     My_Heuristic->Init();
#ifndef NOREDUCE
     init_po();
#endif // // 
   }

   int Heuristic (State *S) {
     //printf("Calculating heuristic for state %d with father %d",(int)S,(int)S->pred);
     return My_Heuristic->Heuristic(S);
   }

   int goal (State *state, int p){
     return My_Goal->Is_Goal(state,p);
   }

  StateItem *expand (State *index, int root, int bound) {  
    StateItem *successors,*fna,*aux,*first,*prev;
    State *aux_state,*aux_state2;

    /* Applying depth-bound. */
    //if(depth_reached<bound && state->g>=bound)
    //  printf("Warning: max search depth too small\n");
    //if(state->g > depth_reached)
    //  depth_reached=state->g;
    if(index->g>=bound) return (StateItem*)0;

    if(((int)sbrk(0)-old_brk)/(1024*1024) >= 512){
      printf("Run out of memory! Limit is 512 MB\n");
      interrupt(0);
    }

    //printf("Expanding state...\n");
    prev=(StateItem*) 0;
    fna=successors=expandf(index);

    //return fna;
    //if(index->g==6){
    //  print_successors(successors);
    //  exit(0);
    //}


    while(fna){
      if((fna->the_state->move.o_t->atom&2 /* Atomic move */
	  || fna->the_state->ps->boq!=-1) /* Boq state */
	 && !((Selected_Goal==ASSERTION_VIOLATION || Selected_Goal==LTL || Selected_Goal==GIVEN_STATE || Selected_Goal==ORBIT) && goal(fna->the_state,1)) ){
	//printf("Expanding atomic state...\n");
	if (fna->the_state->move.o_t->atom&2) atomic_transitions++;
	first=expand(fna->the_state,0,bound);
	if(first){
	  //printf("Back from expanding setting successors...\n");
	  if(fna==successors){
	    /* Set as first if necessary. */
	    successors=first;
	  }
	  else{
	    /* Link with previous item otherwise. */
	    fna->prev->next=first;
	    first->prev=fna->prev;
	  }
	  /* Link with next item. */
	  aux=first;
	  while(aux->next){
	    aux=aux->next;
	  }
	  aux->next=fna->next;
	  if(fna->next) fna->next->prev=aux;

	  /* delete fna. */
	  delete fna->the_state->ps; fna->the_state->ps=(PackedState *)0;
	  delete fna;
	  fna=aux->next;
	} else{
	  //printf("Back from expanding no successors (%d)!\n", index->g);
	  fna=fna->next;
	}
      } else{
	fna=fna->next;
      }
    }

    if((!root) && successors && successors->next){
      /* Current index is not the father state. */
      /* It is necessary to create copys of moves to avoid undesired deletions */
      //printf("state at depth %d\n",index->g);
      for(aux=successors->next; aux; aux=aux->next){
	for(aux_state=aux->the_state; aux_state->pred!=index; aux_state=aux_state->pred);
	aux_state2=aux_state->pred; /* i.e. index */
	aux_state->pred=new State;
	aux_state->pred->ps=(PackedState *)0;
	aux_state->pred->g=aux_state2->g;
	aux_state->pred->h=aux_state2->h;
	aux_state->pred->move=aux_state2->move;
	aux_state->pred->pred=aux_state2->pred;
#ifdef VERI
	aux_state->pred->cycle_pred=aux_state2->cycle_pred;
	if(aux_state2->pred && aux_state2->pred->move.pr==0){ /* never claim move */
	  //printf("Duplicating never move\n");
	  aux_state=aux_state->pred; aux_state2=aux_state2->pred;
	  aux_state2=aux_state->pred;
	  aux_state->pred=new State;
	  aux_state->pred->ps=(PackedState *)0;
	  aux_state->pred->g=aux_state2->g;
	  aux_state->pred->h=aux_state2->h;
	  aux_state->pred->move=aux_state2->move;
	  aux_state->pred->pred=aux_state2->pred;
	  aux_state->pred->cycle_pred=aux_state2->cycle_pred;
	}
#endif // // 
      }
    }

    /* Compute heuristic only for successors (and not for moves). */
    for(aux=successors; aux; aux=aux->next){
      aux->the_state->h=Heuristic(aux->the_state);
    }
#ifndef NOREDUCE
    if(Selected_Heuristic!=TRAIL_FILE)
      successors=reduce(index, successors);
#endif // // 
#ifdef SYMMETRY
    if(symmetry && Selected_Heuristic!=TRAIL_FILE){
      canonicalize_successors(successors);
      }
#endif // // 

    // reverse successors list
    //fna=(StateItem*) 0; aux=successors; while(aux){ successors=aux->next; aux->next=fna; fna=aux; aux=successors; }  successors=fna;

    return successors;
  }

  StateItem *expandf (State *index) {   
    Trans *t, *t_aux; /* A pointer to a transition */
    unsigned char ot, ot_aux, o_pm_aux, m; /* ot is the state of the current process, m? */
    short II, From, To, tt, II_aux, tt_aux, From_aux, To_aux; /* The first 3 are pid, tt is type of process */
    StateItem *current_item,*aux_item,*first_item;
    unsigned char successor_index,successor_index_aux;
    unsigned char timeout;
    unsigned char exit_atomic=0;
    unsigned char *this_p_aux;
    PackedState claim_ps;
    State *aux_state;

#ifdef DEBUG
    printf("Expanding state at depth %d...\n",index->g);
#endif // //  DEBUG

    /* Global variable now points to (index->ps) for comp. with SPIN */
    now=index->ps;

    /* See if the trans from pred was atomic */
    if(!(index->move.o_t)){ /* No move => root */
      /* Try to exectue all currently active processes */
      From=now->_nr_pr-1;
      To=0;
    } else if(index->move.o_t->atom&2){ /* If transition was atomic...*/
	/* Continue executing the same process as in the previous trans. */
#ifdef DEBUG
	printf("\tPrevious transition was atomic\n");
#endif // //  DEBUG
	II=From=To=index->move.pr;
    } else {
      /* Try to execute all currently active processes */
      From=now->_nr_pr-1;
      To=0;
    }

#ifdef VERI
    if(To==0) To++; /* don't try to execute the claim (asynchronous product) */
#endif // //  VERI
 
    successor_index=0;
    trpt=&(index->move);
    trpt->tau = trpt->tau & ~(16|32|64); /* make sure these are off */
    /* Prepare potential successor */
    current_item=new StateItem;
    first_item=current_item;
    current_item->next=(StateItem*)0;
    current_item->prev=(StateItem*)0;
    current_item->the_state=new State;
    current_item->the_state->ps=new PackedState;
    //memcpy((void*)current_item->the_state->ps,(void*)index->ps,sizeof(PackedState));
    memcpy((void*)current_item->the_state->ps,(void*)index->ps,index->ps->_vsz);
    /* Global variable now points to potential successor for comp. with SPIN */
    now=current_item->the_state->ps;
    vsize=now->_vsz;
    /* Timeout things */
    trpt->tau=(trpt->tau)&(~1);
    /* Loop in processes */
    TRY_AGAIN:
#ifdef DEBUG
    printf("\tLooping in processes %d..%d (main)\n",From,To);
#endif // //  DEBUG

    for(II=From; II>=To; II-=1){
      trpt->o_pm&=~1; /* For else. Process not moved */
      /* Get type and state of the process */
      this_p=pptr(II); /* Get pointer to II within state vector */
      tt=(short) ((P0 *)pptr(II))->_p; /* Get state of II */
      ot=(unsigned char) ((P0 *)pptr(II))->_t; /* Get type of II */

#ifdef DEBUG
      printf("\tLooping in transitions of process %d (%s) ...\n",II,procname[ot]);
#endif // //  DEBUG
      /* Loop in each possible transition for the current process and state */
      for(t=trans[ot][tt]; t; t=t->nxt){
#ifdef DEBUG
	printf("\tTrying to move forward %d (id=%d): %s ...\n",t->forw,t->t_id,t->tp);
#endif // //  DEBUG
	m=do_transit(t,II,0); /* #include FORWARD_MOVES */
	if(!m){
	  vsize=index->ps->_vsz; /* not neccessary at first, but there is a bug somewhere */
	  current_item->the_state->ps->_vsz=vsize;
	  continue;
	}
	if(now->boq!=-1){
	  this_p_aux=this_p; II_aux=II; tt_aux=tt; ot_aux=ot; t_aux=t; o_pm_aux=trpt->o_pm;
	  From_aux=From; To_aux=To;
	  From=index->ps->_nr_pr-1;
	  To=0;
	  /* Prepare potential successor */
	  aux_item=current_item;
	  current_item=new StateItem;
	  current_item->next=(StateItem*)0;
	  current_item->prev=(StateItem*)0;
	  current_item->the_state=new State;
	  current_item->the_state->ps=new PackedState;
	  //memcpy((void*)current_item->the_state->ps,(void*)aux_item->the_state->ps,sizeof(PackedState));
	  memcpy((void*)current_item->the_state->ps,(void*)aux_item->the_state->ps,aux_item->the_state->ps->_vsz);
	  now=current_item->the_state->ps;
	  for(II=From; II>=To; II-=1){
	    trpt->o_pm&=~1; /* For else. Process not moved */
	    /* Get type and state of the process */
	    this_p=pptr(II); /* Get pointer to II within state vector */
	    tt=(short) ((P0 *)pptr(II))->_p; /* Get state of II */
	    ot=(unsigned char) ((P0 *)pptr(II))->_t; /* Get type of II */  
	    for(t=trans[ot][tt]; t; t=t->nxt){
	      m=do_transit(t,II,0); /* #include FORWARD_MOVES */
	      if(!m) continue;
	      rendezvous_boq_states++;
	      delete current_item->the_state;
	      delete current_item;
	      current_item=aux_item;
	      this_p=this_p_aux; II=II_aux; tt=tt_aux; ot=ot_aux; t=t_aux; trpt->o_pm=o_pm_aux;
	      From_aux=From; To_aux=To;
	      now=current_item->the_state->ps;
	      vsize=now->_vsz;
	      this_p=pptr(II); /* Get pointer to II within state vector */
	      goto SUCCESSFULL_MOVE;
	    }
	  }
	  delete current_item->the_state;
	  delete current_item;
	  current_item=aux_item;
	  this_p=this_p_aux; II=II_aux; tt=tt_aux; ot=ot_aux; t=t_aux; trpt->o_pm=o_pm_aux;
	  From=From_aux; To=To_aux;
	  //memcpy((void*)current_item->the_state->ps,(void*)index->ps,sizeof(PackedState));
	  memcpy((void*)current_item->the_state->ps,(void*)index->ps,index->ps->_vsz);
	  now=current_item->the_state->ps;
	  vsize=now->_vsz;
	  this_p=pptr(II); /* Get pointer to II within state vector */
	} else {
	SUCCESSFULL_MOVE: /* state transition of the system */
#ifdef VERI /* Try to match with a transition in the claim */
#ifdef DEBUG
	  printf("\tMove succeded: ");
	  printf("proc %d (%s) (%d--%d-->%d) : %s\n", II, procname[ot], tt, t->t_id, t->st, t->tp);
#endif // //  DEBUG
	  if((index->ps->boq)!=-1 || (index->move.o_t && index->move.o_t->atom&2 && !exit_atomic) ){
#ifdef DEBUG
	    printf("\tNot matching with claim (boq=%d)!\n",index->ps->boq);
#endif // //  DEBUG
	    if (t->st > 0){
	      ((P0 *)pptr(II))->_p = t->st;
	      reached[ot][t->st] = 1;
	    }
	      /* Construct successor */
	      //printf("\tConstruct Successor\n");
	      current_item->the_state->g=index->g+1;
	      current_item->the_state->pred=index;
	      current_item->the_state->move.o_t=t;
	      current_item->the_state->move.st=tt;
	      current_item->the_state->move.pr=II;
	      current_item->the_state->move.tau=0;
	      current_item->the_state->move.o_pm=0;
	      //current_item->the_state->h=Heuristic(current_item->the_state);
	      current_item->the_state->shrink();
	      successor_index++;
	      //if(current_item->the_state->move.o_t->atom&2) atomic_transitions++;
	      /* Prepare potential successor */
	      //printf("\tPrepare potential successor\n");
	      aux_item=new StateItem;
	      current_item->next=aux_item;
	      aux_item->next=(StateItem*)0;
	      aux_item->prev=current_item;
	      current_item=aux_item;
	      current_item->the_state=new State;
	      current_item->the_state->ps=new PackedState;
	      //memcpy((void*)current_item->the_state->ps,(void*)index->ps,sizeof(PackedState));
	      memcpy((void*)current_item->the_state->ps,(void*)index->ps,index->ps->_vsz);
	      /* Global variable now points to potential successor for comp. with SPIN */
	      now=current_item->the_state->ps;
	      vsize=now->_vsz;
	      this_p=pptr(II); /* Get pointer to II within state vector */
	  } else {
	    //memcpy((void*)&claim_ps,(void*)now,sizeof(PackedState));
	    memcpy((void*)&claim_ps,(void*)now,now->_vsz);
	    this_p_aux=this_p; II_aux=II; tt_aux=tt; ot_aux=ot; t_aux=t;
	    II=0; this_p=pptr(II); tt=(short) ((P0 *)pptr(II))->_p; ot=VERI;
#ifdef DEBUG
	    printf("\tTrying to match transition in system with transition in claim ...\n");
#endif // //  DEBUG
	    for(t=trans[VERI][tt]; t; t=t->nxt){
#ifdef DEBUG
	      printf("\tTrying to move forward in claim:  %d (id=%d) ...\n",t->forw,t->t_id);
#endif // //  DEBUG
	      now=index->ps; /* Move in claim from the father */
	      m=do_transit(t,II,0); /* move_forward(II,ot,tt,t) */
	      now=current_item->the_state->ps;
	      if(m){
		trpt->o_pm|=1; /* Process II moved */
#ifdef DEBUG
		printf("\tMove succeded in claim: (%d--%d-->%d) %s\n",tt,t->t_id,t->st,t->tp);
#endif // //  DEBUG
		if (t->st > 0){
		  ((P0 *)pptr(II))->_p = t->st;
		  reached[ot][t->st] = 1;
		}
		if (t_aux->st >= 0){
		  ((P0 *)pptr(II_aux))->_p = t_aux->st;
		  reached[ot_aux][t_aux->st] = 1;
		}
		/* Construct successor */
		//printf("\tConstruct Successor\n");
		aux_state=new State; /* Auxiliary state for never move. */
		aux_state->g=index->g+1;
		aux_state->pred=index;
		aux_state->move.o_t=t;
		aux_state->move.st=tt;
		aux_state->move.pr=II;
		aux_state->ps=(PackedState *)0;
		current_item->the_state->g=aux_state->g+1;
		current_item->the_state->pred=aux_state;
		current_item->the_state->move.o_t=t_aux;
		current_item->the_state->move.st=tt_aux;
		current_item->the_state->move.pr=II_aux;
		current_item->the_state->move.tau=0;
		current_item->the_state->move.o_pm=0;
		current_item->the_state->move.o_pm|=(accpstate[ot_aux][tt_aux]?2:0);
		current_item->the_state->move.o_pm|=(progstate[ot_aux][tt_aux]?4:0);
		//current_item->the_state->h=Heuristic(current_item->the_state);
		current_item->the_state->shrink();
		successor_index++;
		//if(current_item->the_state->move.o_t->atom&2) atomic_transitions++;
		/* Prepare potential successor */
		//printf("\tPrepare potential successor\n");
		aux_item=new StateItem;
		current_item->next=aux_item;
		aux_item->next=(StateItem*)0;
		aux_item->prev=current_item;
		current_item=aux_item;
		current_item->the_state=new State;
		current_item->the_state->ps=new PackedState;
		//memcpy((void*)current_item->the_state->ps,(void*)&claim_ps,sizeof(PackedState));
		memcpy((void*)current_item->the_state->ps,(void*)&claim_ps,claim_ps._vsz);
		/* Global variable now points to potential successor for comp. with SPIN */
		now=current_item->the_state->ps;
		vsize=now->_vsz;
		this_p=pptr(II); /* Get pointer to II within state vector */	    
	      }
	    }
	    //printf("Restoring values after synchronous transition\n");
	    this_p=this_p_aux; II=II_aux; tt=tt_aux; ot=ot_aux; t=t_aux;
	    //memcpy((void*)current_item->the_state->ps,(void*)index->ps,sizeof(PackedState));
	    memcpy((void*)current_item->the_state->ps,(void*)index->ps,index->ps->_vsz);
	    /* Global variable now points to potential successor for comp. with SPIN */
	    now=current_item->the_state->ps;
	    vsize=now->_vsz;
	    this_p=pptr(II); /* Get pointer to II within state vector */	  
	  }
#else /* VERI */
	  trpt->o_pm|=1; /* Process II moved */
#ifdef DEBUG
	  printf("\t\tMove succeded: ");
	  printf("proc %d (%s) (%d--%d-->%d) : %s\n", II, procname[ot], tt, t->t_id, t->st, t->tp);
#endif // //  DEBUG
	  if (t->st > 0){
	    /* Set up new state for the process */
	    ((P0 *)pptr(II))->_p = t->st;
	    reached[ot][t->st] = 1;
	  }
	  /* Construct successor */
	  //printf("\tConstruct Successor\n");
	  current_item->the_state->g=index->g+1;
	  current_item->the_state->pred=index;
	  current_item->the_state->move.o_t=t;
	  current_item->the_state->move.st=tt;
	  current_item->the_state->move.pr=II;
	  current_item->the_state->move.tau=0;
	  current_item->the_state->move.o_pm=0;
	  current_item->the_state->move.o_pm|=(accpstate[ot][tt]?2:0);
	  current_item->the_state->move.o_pm|=(progstate[ot][tt]?4:0);
	  //current_item->the_state->h=Heuristic(current_item->the_state);
	  current_item->the_state->shrink();
	  successor_index++;
	  //if(index->move.o_t && index->move.o_t->atom&2) atomic_transitions++;
	  /* Prepare potential successor */
	  //printf("Prepare potential successor\n");
	  aux_item=new StateItem;
	  current_item->next=aux_item;
	  aux_item->next=(StateItem*)0;
	  aux_item->prev=current_item;
	  current_item=aux_item;
	  current_item->the_state=new State;
	  current_item->the_state->ps=new PackedState;
	  //memcpy((void*)current_item->the_state->ps,(void*)index->ps,sizeof(PackedState));
	  memcpy((void*)current_item->the_state->ps,(void*)index->ps,index->ps->_vsz);
	  /* Global variable now points to potiential successor for comp. with SPIN */
	  now=current_item->the_state->ps;
	  vsize=now->_vsz;
	  this_p=pptr(II); /* Get pointer to II within state vector */
#endif // //  VERI
	}
      }
    }

    if(successor_index==0){
      if(index->move.o_t && (index->move.o_t->atom&2) && !exit_atomic){
#ifdef DEBUG
	printf("\tNo progress posible in atomic sequence. Trying to to execute all processes...\n");
#endif // //  DEBUG
	exit_atomic=1;
	From=now->_nr_pr-1;
	To=0;
#ifdef VERI
	To++; /* don't try to execute the claim (asynchronous product) */
#endif // //  VERI
	now=current_item->the_state->ps;
	goto TRY_AGAIN;
      } else if(!(trpt->tau&1)){
#ifdef DEBUG
	if(DEBUG) printf("\tNo progress posible. Trying to timeout...\n");
#endif // //  DEBUG
	trpt->tau=(trpt->tau)|1;
	now=current_item->the_state->ps;
	goto TRY_AGAIN;
      }
    }

    current_item->next=(StateItem*)0; /* Make sure last (auxiliar) item is recognizable. */
#ifdef DEBUG
    printf("\tExpansion done: %d successor(s) found\n",successor_index);
#endif // // 

    /* Delete last item */
    if(!first_item->next){
      first_item->the_state->pred=(State *)0; /* to avoid problems by recursive delete */
      delete first_item->the_state;
      delete first_item;
      first_item=(StateItem*)0;
    }
    for(current_item=first_item; current_item; current_item=current_item->next){
      if(!current_item->next->next){
	current_item->next->the_state->pred=(State *)0; /* to avoid problems by recursive delete */
	delete current_item->next->the_state;
	delete current_item->next;
	current_item->next=(StateItem*)0;
	break;
      }
    }

    /* Print successors list. */
#ifdef DEBUG
    print_successors(first_item);
#else
    if(Selected_Heuristic==INTERACTIVE) print_successors(first_item);
#endif // // 
    if(Selected_Heuristic==TRAIL_FILE){
      /* Try to follow trail file. */
      first_item=follow_trail(first_item);
    } else if (Selected_Heuristic==INTERACTIVE) {
      /* Try to follow user. */
      first_item=follow_user(first_item,successor_index);
    }

    return first_item;
  }

  StateItem *expand2(State *index, short *process, Trans **transition) {  
    StateItem *successor,*aux_item;

    successor=expandf2(index,process,transition);
    while(successor && (successor->the_state->move.o_t->atom&2 || successor->the_state->ps->boq!=-1)){
      if(successor->the_state->move.o_t->atom&2) atomic_transitions++;
      aux_item=successor;
      successor=expandf(successor->the_state);
      delete aux_item->the_state->ps; aux_item->the_state->ps=(PackedState *)0; delete aux_item;
    }
    /* Compute heuristic only for successor (and not for moves). */
    successor->the_state->h=Heuristic(successor->the_state);
    return successor;
  }

  StateItem *expandf2 (State *index, short *process, Trans **transition) {   
    Trans *t, *t_aux; /* A pointer to a transition */
    unsigned char ot, ot_aux, o_pm_aux, m; /* ot is the state of the current process, m? */
    short II, From, To, tt, II_aux, tt_aux, From_aux, To_aux; /* The first 3 are pid, tt is type of process */
    StateItem *current_item,*aux_item,*first_item;
    unsigned char successor_index,successor_index_aux;
    unsigned char timeout;
    unsigned char exit_atomic=0;
    unsigned char *this_p_aux;
    PackedState claim_ps;
    State *aux_state;

#ifdef DEBUG
    printf("Expanding state at depth %d...\n",index->g);
#endif // //  DEBUG

    /* Global variable now points to (index->ps) for comp. with SPIN */
    now=index->ps;
    /* NEXT */
    /* See if the trans from pred was atomic */
    if(!(index->move.o_t)){ /* No move => root */
      /* Try to exectue all currently active processes */
      From=*process;
      To=0;
    } else if(index->move.o_t->atom&2){ /* If transition was atomic...*/
      /* Continue executing the same process as in the previous trans. */
#ifdef DEBUG
	printf("\tPrevious transition was atomic\n");
#endif // //  DEBUG
	II=From=To=index->move.pr;
    } else {
      /* Try to exectue all currently active processes */
      From=*process;
      To=0;
    }
    From=*process;
    To=0;
    /* END NEXT */
    
#ifdef VERI
    if(To==0) To++; /* don't try to execute the claim (asynchronous product) */
#endif // //  VERI
 
    successor_index=0;
    trpt=&index->move;
    trpt->tau = trpt->tau & ~(16|32|64); /* make sure these are off */
    /* Prepare potential successor */
    current_item=new StateItem;
    first_item=current_item;
    current_item->next=(StateItem*)0;
    current_item->prev=(StateItem*)0;
    current_item->the_state=new State;
    current_item->the_state->ps=new PackedState;
    //memcpy((void*)current_item->the_state->ps,(void*)index->ps,sizeof(PackedState));
    memcpy((void*)current_item->the_state->ps,(void*)index->ps,index->ps->_vsz);
    /* Global variable now points to potential successor for comp. with SPIN */
    now=current_item->the_state->ps;
    vsize=now->_vsz;
    /* Timeout things */
    trpt->tau=(trpt->tau)&(~1);
    /* Loop in processes */
    TRY_AGAIN:
#ifdef DEBUG
    printf("\tLooping in processes %d..%d (main)\n",From,To);
#endif // //  DEBUG

    for(II=From; II>=To; II-=1){

 
      /* Get type and state of the process */
      this_p=pptr(II); /* Get pointer to II within state vector */
      tt=(short) ((P0 *)pptr(II))->_p; /* Get state of II */
      ot=(unsigned char) ((P0 *)pptr(II))->_t; /* Get type of II */
      if(II!=*process) t=trans[ot][tt]; else t=*transition;

      /* NEXT */
      if(t==trans[ot][tt]) /* only mark as not moved if first trans. */
	 trpt->o_pm&=~1; /* For else. Process not moved */
      /* NEXT */

#ifdef DEBUG
      printf("\tLooping in transitions of process %d (%s) ...\n",II,procname[ot]);
#endif // //  DEBUG
      /* Loop in each possible transition for the current process and state */
      /* NEXT */
      for(t; t; t=t->nxt){
	/* END NEXT*/
#ifdef DEBUG
	printf("\tTrying to move forward %d(id=%d): %s ...\n",t->forw,t->t_id,t->tp);
#endif // //  DEBUG
	m=do_transit(t,II,0); /* #include FORWARD_MOVES */
	if(!m){
	  vsize=index->ps->_vsz; /* not neccessary at first, but there is a bug somewhere */
	  current_item->the_state->ps->_vsz=vsize;
	  continue;
	}
	if(now->boq!=-1){
	  this_p_aux=this_p; II_aux=II; tt_aux=tt; ot_aux=ot; t_aux=t; o_pm_aux=trpt->o_pm;
	  From_aux=From; To_aux=To;
	  From=index->ps->_nr_pr-1;
	  To=0;
	  /* Prepare potential successor */
	  aux_item=current_item;
	  current_item=new StateItem;
	  current_item->next=(StateItem*)0;
	  current_item->prev=(StateItem*)0;
	  current_item->the_state=new State;
	  current_item->the_state->ps=new PackedState;
	  //memcpy((void*)current_item->the_state->ps,(void*)aux_item->the_state->ps,sizeof(PackedState));
	  memcpy((void*)current_item->the_state->ps,(void*)aux_item->the_state->ps,aux_item->the_state->ps->_vsz);
	  now=current_item->the_state->ps;
	  for(II=From; II>=To; II-=1){
	    trpt->o_pm&=~1; /* For else. Process not moved */
	    /* Get type and state of the process */
	    this_p=pptr(II); /* Get pointer to II within state vector */
	    tt=(short) ((P0 *)pptr(II))->_p; /* Get state of II */
	    ot=(unsigned char) ((P0 *)pptr(II))->_t; /* Get type of II */  
	    for(t=trans[ot][tt]; t; t=t->nxt){
	      m=do_transit(t,II,0); /* #include FORWARD_MOVES */
	      if(!m) continue;
	      rendezvous_boq_states++;
	      delete current_item->the_state;
	      delete current_item;
	      current_item=aux_item;
	      this_p=this_p_aux; II=II_aux; tt=tt_aux; ot=ot_aux; t=t_aux; trpt->o_pm=o_pm_aux;
	      From_aux=From; To_aux=To;
	      now=current_item->the_state->ps;
	      vsize=now->_vsz;
	      this_p=pptr(II); /* Get pointer to II within state vector */
	      goto SUCCESSFULL_MOVE;
	    }
	  }
	  delete current_item->the_state;
	  delete current_item;
	  current_item=aux_item;
	  this_p=this_p_aux; II=II_aux; tt=tt_aux; ot=ot_aux; t=t_aux; trpt->o_pm=o_pm_aux;
	  From=From_aux; To=To_aux;
	  //memcpy((void*)current_item->the_state->ps,(void*)index->ps,sizeof(PackedState));
	  memcpy((void*)current_item->the_state->ps,(void*)index->ps,index->ps->_vsz);
	  now=current_item->the_state->ps;
	  vsize=now->_vsz;
	  this_p=pptr(II); /* Get pointer to II within state vector */
	} else {
	SUCCESSFULL_MOVE: /* state transition of the system */
#ifdef VERI /* Try to match with a transition in the claim */
#ifdef DEBUG
	  printf("\tMove succeded: ");
	  printf("proc %d (%s) (%d--%d-->%d) : %s\n", II, procname[ot], tt, t->t_id, t->st, t->tp);
#endif // //  DEBUG
	  if((index->ps->boq)!=-1 || (index->move.o_t && index->move.o_t->atom&2 && !exit_atomic) ){
#ifdef DEBUG
	    printf("\tNot matching with claim!\n");
#endif // //  DEBUG
	    if (t->st > 0){
	      ((P0 *)pptr(II))->_p = t->st;
	      reached[ot][t->st] = 1;
	    }
	      /* Construct successor */
	      //printf("\tConstruct Successor\n");
	      current_item->the_state->g=index->g+1;
	      current_item->the_state->pred=index;
	      current_item->the_state->move.o_t=t;
	      current_item->the_state->move.st=tt;
	      current_item->the_state->move.pr=II;
	      current_item->the_state->move.tau=0;
	      current_item->the_state->move.o_pm=0;
	      //current_item->the_state->h=Heuristic(current_item->the_state);
	      current_item->the_state->shrink();
	      successor_index++;
	      //if(current_item->the_state->move.o_t->atom&2) atomic_transitions++;
	      /* Prepare potential successor */
	      //printf("\tPrepare potential successor\n");
	      aux_item=new StateItem;
	      current_item->next=aux_item;
	      aux_item->next=(StateItem*)0;
	      aux_item->prev=current_item;
	      current_item=aux_item;
	      current_item->the_state=new State;
	      current_item->the_state->ps=new PackedState;
	      //memcpy((void*)current_item->the_state->ps,(void*)index->ps,sizeof(PackedState));
	      memcpy((void*)current_item->the_state->ps,(void*)index->ps,index->ps->_vsz);
	      /* Global variable now points to potential successor for comp. with SPIN */
	      now=current_item->the_state->ps;
	      vsize=now->_vsz;
	      this_p=pptr(II); /* Get pointer to II within state vector */
	  } else {
	    //memcpy((void*)&claim_ps,(void*)now,sizeof(PackedState));
	    memcpy((void*)&claim_ps,(void*)now,now->_vsz);
	    this_p_aux=this_p; II_aux=II; tt_aux=tt; ot_aux=ot; t_aux=t;
	    II=0; this_p=pptr(II); tt=(short) ((P0 *)pptr(II))->_p; ot=VERI;
#ifdef DEBUG
	    printf("\tTrying to match transition in system with transition in claim ...\n");
#endif // //  DEBUG
	    for(t=trans[VERI][tt]; t; t=t->nxt){
#ifdef DEBUG
	      printf("\tTrying to move forward in claim: %d (id=%d) ...\n",t->forw,t->t_id);
#endif // //  DEBUG
	      now=index->ps; /* Move in claim from the father */
	      m=do_transit(t,II,0); /* move_forward(II,ot,tt,t) */
	      now=current_item->the_state->ps;
	      if(m){
		trpt->o_pm|=1; /* Process II moved */
#ifdef DEBUG
		printf("\tMove succeded in claim: (%d--%d-->%d) %s\n",tt,t->t_id,t->st,t->tp);
#endif // //  DEBUG
		if (t->st > 0){
		  ((P0 *)pptr(II))->_p = t->st;
		  reached[ot][t->st] = 1;
		}
		if (t_aux->st >= 0){
		  ((P0 *)pptr(II_aux))->_p = t_aux->st;
		  reached[ot_aux][t_aux->st] = 1;
		}
		/* Construct successor */
		//printf("\tConstruct Successor\n");
		aux_state=new State; /* Auxiliary state for never move. */
		aux_state->g=index->g+1;
		aux_state->pred=index;
		aux_state->move.o_t=t;
		aux_state->move.st=tt;
		aux_state->move.pr=II;
		aux_state->ps=(PackedState *)0;
		current_item->the_state->g=aux_state->g+1;
		current_item->the_state->pred=aux_state;
		current_item->the_state->move.o_t=t_aux;
		current_item->the_state->move.st=tt_aux;
		current_item->the_state->move.pr=II_aux;
		current_item->the_state->move.tau=0;
		current_item->the_state->move.o_pm=0;
		current_item->the_state->move.o_pm|=(accpstate[ot_aux][tt_aux]?2:0);
		current_item->the_state->move.o_pm|=(progstate[ot_aux][tt_aux]?4:0);
		//current_item->the_state->h=Heuristic(current_item->the_state);
		current_item->the_state->shrink();
		successor_index++;
		//if(current_item->the_state->move.o_t->atom&2) atomic_transitions++;
		/* Prepare potential successor */
		//printf("\tPrepare potential successor\n");
		aux_item=new StateItem;
		current_item->next=aux_item;
		aux_item->next=(StateItem*)0;
		aux_item->prev=current_item;
		current_item=aux_item;
		current_item->the_state=new State;
		current_item->the_state->ps=new PackedState;
		//memcpy((void*)current_item->the_state->ps,(void*)&claim_ps,sizeof(PackedState));
		memcpy((void*)current_item->the_state->ps,(void*)&claim_ps,claim_ps._vsz);
		/* Global variable now points to potential successor for comp. with SPIN */
		now=current_item->the_state->ps;
		vsize=now->_vsz;
		this_p=pptr(II); /* Get pointer to II within state vector */	    
	      }
	    }
	    //printf("Restoring values after synchronous transition\n");
	    this_p=this_p_aux; II=II_aux; tt=tt_aux; ot=ot_aux; t=t_aux;
	    //memcpy((void*)current_item->the_state->ps,(void*)index->ps,sizeof(PackedState));
	    memcpy((void*)current_item->the_state->ps,(void*)index->ps,index->ps->_vsz);
	    /* Global variable now points to potential successor for comp. with SPIN */
	    now=current_item->the_state->ps;
	    vsize=now->_vsz;
	    this_p=pptr(II); /* Get pointer to II within state vector */	  
	  }
#else /* VERI */
	  trpt->o_pm|=1; /* Process II moved */
#ifdef DEBUG
	  printf("\t\tMove succeded: ");
	  printf("proc %d (%s) (%d--%d-->%d) : %s\n", II, procname[ot], tt, t->t_id, t->st, t->tp);
#endif // //  DEBUG
	  if (t->st > 0){
	    /* Set up new state for the process */
	    ((P0 *)pptr(II))->_p = t->st;
	    reached[ot][t->st] = 1;
	  }
	  /* Construct successor */
	  //printf("\tConstruct Successor\n");
	  current_item->the_state->g=index->g+1;
	  current_item->the_state->pred=index;
	  current_item->the_state->move.o_t=t;
	  current_item->the_state->move.st=tt;
	  current_item->the_state->move.pr=II;
	  current_item->the_state->move.tau=0;
	  current_item->the_state->move.o_pm=0;
	  current_item->the_state->move.o_pm|=(accpstate[ot][tt]?2:0);
	  current_item->the_state->move.o_pm|=(progstate[ot][tt]?4:0);
	  //current_item->the_state->h=Heuristic(current_item->the_state);
	  current_item->the_state->shrink();

	  /* NEXT */
	  if(t->nxt){
	    t=t->nxt;
	    //printf("A next transition exists %d!\n",t->t_id);
	  }
	  else{
	    //printf("Trying with next process. ");
	    II--;
	    if(II>=0){
	      now=index->ps;
	      tt=(short) ((P0 *)pptr(II))->_p; /* Get local state of process */
	      ot=(unsigned char) ((P0 *)pptr(II))->_t; /* Get type of process */	    
	      t=trans[ot][tt];
	      //printf("Transition is %d.\n",t->t_id);
	    }
	  }
	  *process=II; *transition=t;
	  return first_item;
	  /* END NEXT */

	  successor_index++;
	  //if(index->move.o_t && index->move.o_t->atom&2) atomic_transitions++;
	  /* Prepare potential successor */
	  //printf("Prepare potential successor\n");
	  aux_item=new StateItem;
	  current_item->next=aux_item;
	  aux_item->next=(StateItem*)0;
	  aux_item->prev=current_item;
	  current_item=aux_item;
	  current_item->the_state=new State;
	  current_item->the_state->ps=new PackedState;
	  //memcpy((void*)current_item->the_state->ps,(void*)index->ps,sizeof(PackedState));
	  memcpy((void*)current_item->the_state->ps,(void*)index->ps,index->ps->_vsz);
	  /* Global variable now points to potiential successor for comp. with SPIN */
	  now=current_item->the_state->ps;
	  vsize=now->_vsz;
	  this_p=pptr(II); /* Get pointer to II within state vector */
#endif // //  VERI
	}
      }
    }

    if(successor_index==0){
      if(index->move.o_t && (index->move.o_t->atom&2) && !exit_atomic){
#ifdef DEBUG
	printf("\tNo progress posible in atomic sequence. Trying to to execute all processes...\n");
#endif // //  DEBUG
	exit_atomic=1;
	From=now->_nr_pr-1;
	To=0;
#ifdef VERI
	To++; /* don't try to execute the claim (asynchronous product) */
#endif // //  VERI
	now=current_item->the_state->ps;
	goto TRY_AGAIN;
      } else if(!(trpt->tau&1) && *process==(index->ps->_nr_pr-1) && *transition==trans[ot][tt]){
#ifdef DEBUG
	if(DEBUG) printf("\tNo progress posible. Trying to timeout...\n");
#endif // //  DEBUG
	trpt->tau=(trpt->tau)|1;
	now=current_item->the_state->ps;
	goto TRY_AGAIN;
      }
    }

    current_item->next=(StateItem*)0; /* Make sure last (auxiliar) item is recognizable. */
#ifdef DEBUG
    printf("\tExpansion done: %d successor(s) found\n",successor_index);
#endif // // 

    /* Delete last item */
    if(!first_item->next){
      delete first_item->the_state;
      delete first_item;
      first_item=(StateItem*)0;
    }
    for(current_item=first_item; current_item; current_item=current_item->next){
      if(!current_item->next->next){
	delete current_item->next->the_state;
	delete current_item->next;
	current_item->next=(StateItem*)0;
	break;
      }
    }

    /* Print successors list. */
#ifdef DEBUG
    print_successors(first_item);
#else
    if(Selected_Heuristic==INTERACTIVE) print_successors(first_item);
#endif // // 
    if(Selected_Heuristic==TRAIL_FILE){
      /* Try to follow trail file. */
      first_item=follow_trail(first_item);
    } else if (Selected_Heuristic==INTERACTIVE) {
      /* Try to follow user. */
      first_item=follow_user(first_item,successor_index);
    }

    return first_item;
  }

  StateItem *follow_trail(StateItem *successors){
    /* Takes a list of successors and converts it into  a list containing only
       the one selected by the user. */
    int tr_d, tr_p, tr_t, never_t, never_p;
    Trans *t;
    StateItem *current_item,*aux_item;
    State *index=successors?successors->the_state->pred:(State*)0;
    
    do{
      if(fscanf(trail_file,"%d:%d:%d",&tr_d,&tr_p,&tr_t)!=3){
	if(Selected_Goal==GIVEN_STATE || Selected_Goal==ORBIT) return (StateItem*)0;
	if(Selected_Goal!=DEADLOCK && Selected_Goal!=VALID_ENDSTATE){
	  printf("Error! No more moves in trail file.\n");
	  printf("Please make sure that the trail was generated by using the same Promela source file.\n");
	  possible_bug();
	  exit(0);
	} else if(successors && Selected_Goal){
	  printf("Error! Endstate in trail but not in HSF.\n");
	  printf("Please make sure that the trail was generated by using the same Promela source file.\n");
	  possible_bug();
	  exit(0);
	} else {
	  return (StateItem*)0;
	}
      } else if(Selected_Goal!=DEADLOCK && Selected_Goal!=VALID_ENDSTATE && !successors){
	printf("Error! Endstate in HSF but not in trail.\n");
	printf("Please make sure that the trail was generated by using the same Promela source file.\n");
	possible_bug();
	exit(0);
      }
      
#ifdef DEBUG
      printf("\tTrail move read: %d:%d:%d\n",tr_d,tr_p,tr_t);
#endif // //  DEBUG
      never_t=-1;
#ifdef VERI
      if(tr_p==0){
	never_p=tr_p; never_t=tr_t;
	if(fscanf(trail_file,"%d:%d:%d",&tr_d,&tr_p,&tr_t)!=3 && Selected_Goal!=DEADLOCK && Selected_Goal!=LTL){
	  printf("Error! No more moves in trail file.\n");
	  printf("Please make sure that the trail was generated by using the same Promela source file.\n");
	  possible_bug();
	  exit(0);
	}
#ifdef DEBUG
	printf("\tTrail move read: %d:%d:%d\n",tr_d,tr_p,tr_t);
#endif // // 
      }
#endif // //  VERI
      if(tr_d==-1 && tr_p==-1 && tr_t==-1 && Selected_Goal==LTL){
	printf("\tCycle seed found at depth %d.\n",successors->the_state->pred->pred->g);
	Selected_Goal=GIVEN_STATE;
	My_Goal->set_goal(successors->the_state->pred->pred);
      }
    } while(tr_d<0);

    current_item=successors;
    for(current_item=successors; current_item; current_item=current_item->next){
      if( (never_t!=-1 && tr_p==0) && /* last move of trail */
	  (never_p==current_item->the_state->pred->move.pr && never_t==current_item->the_state->pred->move.o_t->t_id) )
	break;
      if( (never_t!=-1) && (current_item->the_state->move.pr==tr_p && current_item->the_state->move.o_t->t_id==tr_t && never_p==current_item->the_state->pred->move.pr && (never_t==current_item->the_state->pred->move.o_t->t_id))){
	break;
      }
      else if( (never_t==-1) && current_item->the_state->move.pr==tr_p && current_item->the_state->move.o_t->t_id==tr_t)
	break;      
    }
    if(!current_item){
      if(never_t!=-1)
	printf("Error! Unable to perform synchronous move %d:%d:%d - 0:%d:%d\n",tr_d,tr_p,tr_t,never_p,never_t);
      else
	printf("Error! Unable to perform move %d:%d:%d\n",tr_d,tr_p,tr_t);
      print_successors(successors);
#ifdef DEBUG
      print_successors(successors);
#endif // // 
      printf("Please make sure that the trail was generated by using the same Promela source file.\n");
      possible_bug(); exit(0);
    }

    /* Delete successors (except the selected one) */
    while(successors){
      aux_item=successors;
      successors=successors->next;
      if(aux_item!=current_item){
	delete aux_item->the_state;
	delete aux_item;
      }
    }

#ifdef DEBUG
    if(current_item){
#ifdef VERI
      if(current_item->the_state->pred->move.pr==0)
	printf("\tSelected: proc %d exec (%d--%d-->%d) : %s\n", current_item->the_state->pred->move.pr,current_item->the_state->pred->move.st, current_item->the_state->pred->move.o_t->t_id, current_item->the_state->pred->move.o_t->st, current_item->the_state->pred->move.o_t->tp);
#endif // // 
      printf("\t          proc %d exec (%d--%d-->%d) : %s\n", current_item->the_state->move.pr,current_item->the_state->move.st, current_item->the_state->move.o_t->t_id, current_item->the_state->move.o_t->st, current_item->the_state->move.o_t->tp);
    }
#endif // // 

    if(current_item){
      current_item->next=(StateItem*)0;
      current_item->prev=(StateItem*)0;
    }
    return current_item;
  }
  
  StateItem *follow_user(StateItem *successors, int successor_index){
    /* Takes a list of successors and returns a list containing only
       the one selected by the user. */
    int successor_index_aux;
    StateItem *current_item,*aux_item;
    
    if(successor_index>1){
      do{
	int selected_successor;
	printf("\tSelect succcessor 1..%d: ",successor_index);
	scanf("%d",&selected_successor);
	successor_index_aux=selected_successor;
      }while(successor_index_aux<1 || successor_index_aux>successor_index);
      current_item=successors;
      for(successor_index=1; current_item && successor_index!=successor_index_aux; successor_index++){
	current_item=current_item->next;
      }
      current_item->next=(StateItem *)0;
      successors=current_item;
      printf("\tSelected: proc %d exec (%d--->%d) : %s\n", current_item->the_state->move.pr,current_item->the_state->move.st, current_item->the_state->move.o_t->st, current_item->the_state->move.o_t->tp);
    } else
      current_item=successors;

    /* Delete successors (except the selected one) */
    while(successors){
      aux_item=successors;
      successors=successors->next;
      if(aux_item!=current_item){
	delete aux_item->the_state;
	delete aux_item;
      }
    }

    if(current_item){
      current_item->next=(StateItem*)0;
      current_item->prev=(StateItem*)0;
    }

    return current_item;
  }
  

  void print_successors(StateItem *first_item)
  {
    int successor_index_aux;
    StateItem* aux_item;
    State *s;
    
    if(!first_item){
      printf("\tNo successors.\n");
      return;
    }
    
    successor_index_aux=1;
    printf("\tSuccessors at depth %d are:\n",first_item->the_state->g-1);
    for(aux_item=first_item; aux_item; aux_item=aux_item->next){
      printf("\t\tSuccessor %d:\n",successor_index_aux);
      s=aux_item->the_state;
      now=aux_item->the_state->ps;
      do{
	/*#ifdef VERI
	  if(aux_item->the_state->pred->move.pr==0)
	  printf("proc %d (%s) (%d--%d-->%d): %s\n",aux_item->the_state->pred->move.pr,procname[((P0*)hsf_pptr(aux_item->the_state->ps,aux_item->the_state->pred->move.pr))->_t],aux_item->the_state->pred->move.st, aux_item->the_state->pred->move.o_t->t_id,aux_item->the_state->pred->move.o_t->st, aux_item->the_state->pred->move.o_t->tp);
	  #endif // //  VERI*/
	printf("\t\t\tproc %d (%s) (%d--%d-->%d): %s\n",s->move.pr,procname[((P0*)hsf_pptr(now,s->move.pr))->_t],s->move.st, s->move.o_t->t_id,s->move.o_t->st, s->move.o_t->tp);
	s=s->pred;
      } while(s && !s->ps);
      successor_index_aux++;
    }
  }

  void initial_state(State *S) {
    int i;

    S->g = 0;
    S->pred=(State*)0;
    S->move.o_t=(Trans *)0;
    S->ps=new PackedState;
    now=S->ps; /* now points to S->ps for comp. with spin (iniglobals, active_procs(), etc. ). */
    memset((char *)now, 0, sizeof(PackedState));
    vsize = sizeof(PackedState)-VECTORSZ;
    iniglobals(); /* Init global variables of the protocol. */
    now->boq=-1; /* Disable rendez-vous. */
    S->move.o_pm=0; /* Unset some flags see typedef struct Trail in hsf-pan.c */
    S->move.o_t=(Trans *)0; /* No move lead to this state. */
    noptr=new unsigned char[Maxbody]; /* A place to point for Pptr of non-running procs: */
#ifdef VERI
    Addproc(VERI); /* Add never claim to state vector if present. */
#endif // //  VERI
    active_procs(); /* Add active processes to state vector. */
    now->_vsz = vsize; /* Set state vector's size */
    S->h = Heuristic(S); /* Set h value. */
    S->shrink(); /* Shrink state. */
    init_compression();
  }

  void print_step(State *S) {
    Trans *transition;
    unsigned char process_type;

    transition=S->move.o_t;
    if(transition){
      if(S->ps) now=S->ps;
      /* I hope now points to a good place, otherwise... */
      printf("\tDepth %d: %s[%d] (%s)\n",S->g,procname[((P0 *)pptr(S->move.pr))->_t],S->move.pr,transition->tp);
    } else {
      printf("\tDepth %d: Start State\n",S->g);
    }
  }

  void add_to_trail(State *S) {
    Trans *transition;
    unsigned char process_type;

    transition=S->move.o_t;
    if(transition){
      depth++;
      transition=S->move.o_t;
      trail[depth]=S->move;
    }
  }

};

#endif // //  _PROTOCOL_
