/* 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   */

/*#define DEBUG_SCC*/

typedef struct Edge{
  int state;
  struct Edge *next;
}Edge;

void Classify_SCC(void); /* classifies scc for FSM p */
unsigned char *scc; /* scc[u] is the SCC to which state u belongs */
Edge **states_scc; /* states_scc[scc] is set of states of scc */
unsigned char nscc; /* total number of SCC */
unsigned char *scc_class;
#define n_scc(x) (scc_class[x]&1)
#define p_scc(x) (scc_class[x]&2)
#define f_scc(x) (scc_class[x]&4)
#define e_scc(x) (scc_class[x]&8)
#define N_SCC(x) (n_scc(scc[x]))
#define P_SCC(x) (p_scc(scc[x]))
#define F_SCC(x) (f_scc(scc[x]))
#define E_SCC(x) (e_scc(scc[x]))

int *timef; /* finishing times */
int timec;
int *scc_visited;
Edge **invV;

void Compute_Timestamp_and_Transpose_Visit(unsigned char u);
void Compute_Timestamp_and_Transpose(void);
void Visit_SCC(unsigned char u);
void Compute_SCC();
int Detect_Non_Accepting_Cycles2(unsigned char u);
int Detect_Non_Accepting_Cycles(unsigned char u);
void Classify_PF(void);
void Classify_SCC(void);

void Compute_Timestamp_and_Transpose_Visit(unsigned char u)
{
  unsigned char v;
  Edge *aux;
  Trans *t;
  
  scc_visited[u]=1;
#ifdef DEBUG_SCC
  printf("Exploring state %d\n",u);
#endif //
  for(t=trans[VERI][u]; t; t=t->nxt){
    v=t->st;
    /* insert inverse edge */
    aux=(Edge*) malloc(sizeof(Edge));
    aux->state=u;
    aux->next=invV[v];
    invV[v]=aux;
    if(!scc_visited[v]) Compute_Timestamp_and_Transpose_Visit(v);
  }
#ifdef DEBUG_SCC
  printf("\tState %d stamped with %d\n",u,timec);
#endif //
  timef[timec]=u; timec++;
}

void Compute_Timestamp_and_Transpose(void)
{
  int u;
  
  timef=(int *) malloc(sizeof(unsigned char)*nstates_claim);
  scc_visited=(int *) malloc(sizeof(int)*nstates_claim);
  invV=(Edge**) malloc(sizeof(Edge*)*nstates_claim);
  for(u=0; u<nstates_claim; u++){
#ifdef DEBUG_SCC
    printf("\tInit for %d\n",u);
#endif //
    scc_visited[u]=0;
    timef[u]=-1;
    invV[u]=(Edge*)0;
  }
  timec=0;
  Compute_Timestamp_and_Transpose_Visit(start_claim);
}

void Visit_SCC(unsigned char u)
{
  unsigned char v;
  Edge *aux;
  
  scc_visited[u]=1;
  if(accpstate[VERI][u]) scc_class[nscc]=0;
#ifdef DEBUG_SCC
  printf("\t\tState %d belongs to SCC-%d\n",u,nscc);
#endif //
  scc[u]=nscc;
  aux=(Edge*) malloc(sizeof(Edge));
  aux->state=u;
  aux->next=states_scc[nscc];
  states_scc[nscc]=aux;
  for(aux=invV[u]; aux; aux=aux->next){
    v=aux->state;
    if(!scc_visited[v]) Visit_SCC(v);
  }
}

void Compute_SCC()
{
  unsigned char u,v;
  Edge *aux;
  
  states_scc=(Edge**) malloc(sizeof(Edge)*nstates_claim);
  for(u=0; u<nstates_claim; u++){
    scc_visited[u]=0;
    states_scc[u]=(Edge *)0;
    scc_class[u]=1; /* n-class */
  }
  nscc=0;
  for(timec=nstates_claim-1; timec>=0; timec--){
    if(timef[timec]!=-1 && (!scc_visited[timef[timec]])){
#ifdef DEBUG_SCC
      printf("\tVisiting SCC-%d starting at %d...\n",nscc,timef[timec]);
#endif //
      if(stopstate[VERI][timef[timec]]){
#ifdef DEBUG_SCC
	printf("\tEndstate found.\n");
#endif //
	scc[timef[timec]]=nscc;
	states_scc[nscc]=(Edge *) malloc(sizeof(Edge));
	states_scc[nscc]->state=timef[timec];
	states_scc[nscc]->next=(Edge *)0;
	scc_class[nscc]=8; /* e-class */
	nscc++;
	scc_visited[timef[timec]]=1;
      } else{
#ifdef DEBUG_SCC
	printf("\tNot endstate. Expanding...\n");
#endif //
	for(aux=invV[timef[timec]]; aux; aux=aux->next){
	  v=aux->state;
	  if(!scc_visited[v]) Visit_SCC(v);
	}
	scc_visited[timef[timec]]=1;
	if(states_scc[nscc]) nscc++;
      }
    }
  }
}

int Detect_Non_Accepting_Cycles2(unsigned char u)
{
  unsigned char v;
  Trans *t;
  
#ifdef DEBUG_SCC
  printf("\t\tExploring %d in dfs2\n",u);
#endif //
  scc_visited[u]|=4; /* flag */
  for(t=trans[VERI][u]; t; t=t->nxt){
    v=t->st;
    if(scc[u] != scc[v] || accpstate[VERI][v]) continue;
    if(scc_visited[v]&2){
#ifdef DEBUG_SCC
      printf("\t\tNon-accepting cycle found!\n");
#endif //
      return 1; /* non accepting cycle detected */
    }
    if(!(scc_visited[v]&4)) return Detect_Non_Accepting_Cycles(v);
  }
  return 0;
}

int Detect_Non_Accepting_Cycles(unsigned char u)
{
  unsigned char rval,v;
  Trans *t;
  
#ifdef DEBUG_SCC
  printf("\t\tExploring %d in dfs1\n",u);
#endif //
  scc_visited[u]=3; /* mark as scc_visited and on stack */
  for(t=trans[VERI][u]; t; t=t->nxt){
    v=t->st;
    if(scc[u] != scc[v]) continue;
    if(!(scc_visited[v]&1)) rval=Detect_Non_Accepting_Cycles(v);
    else rval=0;
    if(rval) return 1;
  }
  if(!accpstate[VERI][u]) return Detect_Non_Accepting_Cycles2(u);
  scc_visited[u]&~2; /* state no more on dfs1 stack */
  return 0;
}

void Classify_PF(void)
{
  unsigned char u,v;

  for(u=0; u<nscc; u++){
#ifdef DEBUG_SCC
    printf("\tClassifying SCC%d...\n",u);
#endif //
    if( (!e_scc(u)) && (!n_scc(u)) && (states_scc[u]!=0) ){
      scc_class[u]=4; /* F class */
      for(v=0; v<nstates_claim; v++) scc_visited[v]=0;
#ifdef DEBUG_SCC
      printf("\tSearch for non accepting cycles necessary\n");
#endif //
      if(!states_scc[u]) printf("Unexpected void SCC!!!\n");
      if(Detect_Non_Accepting_Cycles(states_scc[u]->state)){
	scc_class[u]=2; /* P class */
      }
    }
  }
}

void Classify_SCC(void)
{
  Edge *aux_edge;
  unsigned char u;
  scc=(unsigned char*) emalloc(nstates_claim);
  scc_class=(unsigned char*) emalloc(nstates_claim);
#ifdef DEBUG_SCC
  printf("Computing Timestamps and Transpose Graph...\n");
#endif //
  Compute_Timestamp_and_Transpose();
#ifdef DEBUG_SCC
  printf("Computing Strongly Connected Components...\n");
#endif //
  Compute_SCC();
#ifdef DEBUG_SCC
  printf("Classifying SCCs...\n");
#endif //
  Classify_PF();
#ifdef DEBUG_SCC
  printf("Classification done!\n");
#endif //
  free(timef);
  free(scc_visited);
  for(u=0; u<nstates_claim; u++){
    aux_edge=invV[u];
    while(invV[u]){
      aux_edge=invV[u];
      invV[u]=invV[u]->next;
      free(aux_edge);
    }
  }
#ifdef DEBUG_SCC
  printf("Classification of SCCs of Never Claim:\n");
  for(u=0; u<nscc; u++){
    printf("\t");
    if(n_scc(u))
      printf("N-");
    else if(p_scc(u))
      printf("P-");
    else if(f_scc(u))
      printf("F-");
    else if(e_scc(u))
      printf("E-");
    printf("SCC-%d = \{ ",u);
    for(aux_edge=states_scc[u]; aux_edge; aux_edge=aux_edge->next){
      if(!(aux_edge->next))
	printf("S%d }\n",aux_edge->state);
      else
	printf("S%d , ",aux_edge->state);
    }
  }
#endif //
}
