/* 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 _SCC_
#define _SCC_

#define DEBUG_FSM 0

#define neverstate(x) (((P0 *)hsf_pptr(x,0))->_p)
/* Never state in a PackedState x. */

struct Edge;

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

class SCC{
 public:
  void Classify_SCC(int p); /* classifies scc for FSM p */
  int *scc; /* scc[u] is the SCC to which state u belongs */
  Edge **states_scc; /* states_scc[scc] is set of states of scc */
  int nscc; /* total number of SCC */
  int n_scc(int scc){ return scc_class[scc]&1; };
  int p_scc(int scc){ return scc_class[scc]&2; };
  int f_scc(int scc){ return scc_class[scc]&4; };
  int e_scc(int scc){ return scc_class[scc]&8; };
  
 private:
    int *timef; /* finishing times */
    int time;
    int *visited;
    Edge **invV;
    unsigned char *scc_class;
    int proctype;

    void Compute_Timestamp_and_Transpose_Visit(int u)
      {
	int v;
	Edge *aux;

	visited[u]=1;
	if(DEBUG_FSM) printf("Exploring state %d\n",u);
	for(Trans *t=trans[proctype][u]; t; t=t->nxt){
	  v=t->st;
	  /* insert inverse edge */
	  aux=new Edge;
	  aux->state=u;
	  aux->next=invV[v];
	  invV[v]=aux;
	  if(!visited[v]) Compute_Timestamp_and_Transpose_Visit(v);
	}
	if(DEBUG_FSM) printf("\tState %d stamped with %d\n",u,time);
	timef[time]=u; time++;
      }
    
    void Compute_Timestamp_and_Transpose(void)
      {
	int u;

	timef=new int[nstates_proc[proctype]];
	visited=new int[nstates_proc[proctype]];
	invV=new Edge*[nstates_proc[proctype]];
	for(u=0; u<nstates_proc[proctype]; u++){
	  visited[u]=0;
	  timef[u]=-1;
	  invV[u]=(Edge*)0;
	}
	time=0;
	Compute_Timestamp_and_Transpose_Visit(start_proc[proctype]);
      }
    
    void Visit_SCC(int u)
      {
	int v;
	Edge *aux;

	visited[u]=1;
	if(accpstate[proctype][u]) scc_class[nscc]=0;
	if(DEBUG_FSM) printf("\t\tState %d belongs to SCC-%d\n",u,nscc);
	scc[u]=nscc;
	aux=new 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(!visited[v]) Visit_SCC(v);
	}
      }

    void Compute_SCC()
      {
	int u,v;
	Edge *aux;

	scc=new int[nstates_proc[proctype]];
	states_scc=new Edge*[nstates_proc[proctype]];
	scc_class=new unsigned char[nstates_proc[proctype]];
	for(u=0; u<nstates_proc[proctype]; u++){
	  visited[u]=0;
	  states_scc[u]=(Edge *)0;
	  scc_class[u]=1
; /* n-class */
	}
	nscc=0;
	for(time=nstates_proc[proctype]-1; time>=0; time--){
	  if(timef[time]!=-1 && (!visited[timef[time]])){
	    if(DEBUG_FSM) printf("\tVisiting SCC-%d starting at %d...\n",nscc,timef[time]);
	    if(stopstate[proctype][timef[time]]){
	      if(DEBUG_FSM) printf("\tEndstate found.\n");
	      scc[timef[time]]=nscc;
	      states_scc[nscc]=new Edge;
	      states_scc[nscc]->state=timef[time];
	      states_scc[nscc]->next=(Edge *)0;
	      scc_class[nscc]=8; /* e-class */
	      nscc++;
	      visited[timef[time]]=1;
	    } else{
	      for(aux=invV[timef[time]]; aux; aux=aux->next){
		v=aux->state;
		if(!visited[v]) Visit_SCC(v);
	      }
	      visited[timef[time]]=1;
	      if(states_scc[nscc]) nscc++;
	    }
	  }
	}
      }

    int Detect_Non_Accepting_Cycles2(int u)
      {
	int v;

	if(DEBUG_FSM) printf("\t\tExploring %d in dfs2\n",u);
	visited[u]|=4; /* flag */
	for(Trans *t=trans[proctype][u]; t; t=t->nxt){
	  v=t->st;
	  if(scc[u] != scc[v] || accpstate[proctype][v]) continue;
	  if(visited[v]&2){
	    if(DEBUG_FSM) printf("\t\tNon-accepting cycle found!\n");
	    return 1; /* non accpt cycle detected */
	  }
	  if(!(visited[v]&4)) return Detect_Non_Accepting_Cycles(v);
	}
	return 0;
      }

    int Detect_Non_Accepting_Cycles(int u)
      {
	int rval,v;

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

    void Classify_PF(void)
      {
	for(int u=0; u<nscc; u++){
	  if(DEBUG_FSM) printf("\tClassifying SCC%d...\n",u);
	  if( (!e_scc(u)) && (!n_scc(u)) && (states_scc[u]!=0) ){
	    scc_class[u]=4; /* F class */
	    for(int v=0; v<nstates_proc[proctype]; v++) visited[v]=0;
	    if(DEBUG_FSM) printf("\tSearch for non accepting cycles necessary\n");
	    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 SCC::Classify_SCC(int p)
{
  proctype=p;
  if(DEBUG_FSM) printf("Computing Timestamps and Transpose Graph...\n");
  Compute_Timestamp_and_Transpose();
  if(DEBUG_FSM) printf("Computing Strongly Connected Components...\n");
  Compute_SCC();
  if(DEBUG_FSM) printf("Classifying SCCs...\n");
  Classify_PF();
  if(DEBUG_FSM) printf("Classification done!\n");
  delete timef;
  delete visited;
  
}

#endif // _SCC_
