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

//..
//..

#include <stdio.h>
#include <global.h>
#include <scc.h>

void main(int argc, char *argv[]) {
  SCC My_FSM;
  int p;

  if(argc<2){
    printf("Usage: %s <proctype>\n",argv[0]);
    printf("<proctype>::=%d..%d\n",0,_NP_-1);
    for(p=0; p<_NP_; p++)
      printf("%d = %s\n",p,procname[p]);
    return 0;
  }
  p=atoi(argv[1]);
  if(p<0 || p>=_NP_){
    printf("No valid proctype!\n");
    printf("Usage: %s <proctype>\n",argv[0]);
    printf("<proctype>::=%d..%d\n",0,_NP_);
    for(p=0; p<_NP_; p++)
      printf("%d = %s\n",p,procname[p]);
    return 0;
  }

  run();
  My_FSM.Classify_SCC(p);
  printf("Classification of SCCs of %s:\n",procname[p]);
  for(int i=0; i<My_FSM.nscc; i++){
    printf("\t");
    if(My_FSM.n_scc(i))
      printf("N-");
    else if(My_FSM.p_scc(i))
      printf("P-");
    else if(My_FSM.f_scc(i))
      printf("F-");
    else if(My_FSM.e_scc(i))
      printf("E-");
    printf("SCC-%d = \{ ",i);
    for(Edge *e=My_FSM.states_scc[i]; e; e=e->next){
      if(accpstate[p][e->state])
	printf("[%d]",e->state);
      else
	printf("%d",e->state);
      if(!(e->next))
	printf(" }\n",e->state);
      else
	printf(" , ",e->state);
    }
  }
}
