/* $Id: instantiator.c,v 1.4 2001/09/13 14:13:15 bertl Exp $ */

#ifdef HAVE_CONFIG_H
#include "config.h"
#endif

#include <unistd.h>
#include <stdio.h>
#include "rw1.h"
#include "lts.h"
#include "svc.h"
#include "svcerrno.h"
#include <strings.h>

#ifdef BCG
#include "bcg_user.h"
#endif

typedef void (*INIT)(void);
typedef void (*FINAL)(void);
typedef void (*AFTERSTEP) (int state, int n);

typedef struct {
  INIT init;
  LTScallback instep;
  AFTERSTEP afterstep;
  FINAL final;
  } TASK;
   
typedef struct {
   ATerm *action;
   int *from, *depth;
   int nr;
} BACK;

static TASK *task;

char *who = "Instantiator";

ATbool o_flag = ATfalse;

static FILE  *output = NULL;

static ATermList  actions = NULL;
 
#define P(msg)  fprintf(stderr,"%s\n",msg)
#define BUFLEN 1024

static char filename[BUFLEN], outputfile[BUFLEN], inputfile[BUFLEN];

static BACK back = {NULL,NULL,0};

static unsigned int explored = 0, visited = 0, transitions = 0, 
hash = 1;
static SVCbool svc_num = 0;
static SVCfile svcFile[1];
static SVCparameterIndex parameterIndex = 0;

static ATbool monitor = ATfalse, cadp = ATfalse;

static void helpmsg(void) 
    {  
    P("Usage: instantiator [options] [input file]");
    P("");
    P("The following options can be used");
    P("-help:\t\tyields this message");
    P("-version:\tget the version number of this release");
    P("-i:\t\ttau replaced by i (Needed for CADP)");
    P("-simple:\truns an instantiator without extra features.");
    P("\t\tThis instantiator runs fast on \"small\" specifications");
    P("\t\tinstead of a compiled rewrite system.");
    P("-nohash:\tno hash tables will be used");
    P("-deadlock:\tonly print the deadlock states, and an account of how states");
    P("\t\thave been visited. Use a .dlk file instead of a .aut file");
    P("-trace [:]<action>[,[:]<action>]*:");
    P("\t\tprints the traces to each action in the list of actions.");
    P("\t\tIf the action is prefixed by a colon then the process halts");
    P("\t\tafter printing the trace.");
    P("-monitor:\tMonitor function on"); 
    P("-svc-term:\twrites transition system in SVC format");
    P("-svc-num:\tsee -svc-term, either states are represented by numbers");
    P("\t\t(instead of statevectors)"); 
#ifdef BCG
    P("-bcg:\t\twrites transition system in BCG format");
#endif
    P("-prerewr:\tThe conditions in the summands will be rewritten first");
    P("-alt <label>:\tUse an alternative rewriter which does not");
    P("\t\tcompile the rewrite system first. <label> stands for:");
    P("\t\t\"strictleft\" or \"innermost\", which defines the stategy.");
    LTShelp(); 
    }
    
static void help(void)
    {
    P("");
    helpmsg();
    P("");
    P("");
    }

static void version(void)
    {
    char buf[100];
    sprintf(buf,"%s: version %s",who, VERSION);
    P(buf);
    }
#undef P     

#define max(x,y) ((x)<(y)?(y):(x))

#define INITIAL_SIZE 100

/* --- BEGIN TRACE DETECTION --- */


static ATermList ParseTraceActions(char* actnames) {
    ATermList result = ATmakeList0();
    char *actname = strtok(actnames, ",");
    do  {
        if (strlen(actname)>0 && *actname !='%') {
            result = ATinsert(result, 
            *actname ==':'?(ATerm) ATmakeList1(ATmake("<str>",++actname)):
                        (ATerm) ATmake("<str>",actname));
            }
        } while ((actname = strtok(NULL, ",")));
    return result;
}


static void reset_from(BACK back, int from, int nr) {
     int i = from;
     for (i=from;i<nr;i++) {
         back.action[i] = NULL;
         back.from[i] = -1;
         back.depth[i] = -1;
         }
     }

static BACK enlarge_back(BACK back, int to) {
      while (back.nr <= to+1) {
       long old_nr=back.nr;
       if (old_nr==0) {
            back.nr = INITIAL_SIZE;
            if (!(back.action = (ATerm*) calloc(back.nr,sizeof(ATerm))))
                   ATerror("Cannot allocate action array (%d)", back.nr);
            if (!(back.from = (int*) calloc(back.nr,sizeof(int))))
                   ATerror("Cannot allocate from array (%d)", back.nr); 
            if (!(back.depth = (int*) calloc(back.nr,sizeof(int))))
                   ATerror("Cannot allocate from array (%d)", back.nr);       
            }
       else {
            ATunprotectArray(back.action);
            back.nr *= 2;
            /* if (monitor) ATwarning("Enlarge trace array %d",back.nr); */
            if (!(back.action = (ATerm*) realloc(back.action, back.nr*sizeof(ATerm))))
                   ATerror("Cannot reallocate term array (%d)", back.nr);
            if (!(back.from = (int*) realloc(back.from, back.nr*sizeof(int))))
                   ATerror("Cannot reallocate term array (%d)", back.nr);
            if (!(back.depth = (int*) realloc(back.from, back.nr*sizeof(int))))
                   ATerror("Cannot reallocate term array (%d)", back.nr);
            }
            reset_from(back, old_nr, back.nr);
            ATprotectArray(back.action, back.nr);
       }
       return back;
}

static PrintTrace(int to) {
    ATermList  actnames = ATmakeList0(); 
    int init = LTSgetInitialState();
    for (;to!=init;to=back.from[to]) {
   /* ATwarning("QQ to = %d act = %t",to, back.action[to]); */
         actnames = ATinsert(actnames, back.action[to]); 
    }
    ATfprintf(output, "%t\n",actnames);
}

static void CheckActions(ATermList trace_actions, BACK back, int to) {
  ATbool stop = ATfalse;
  ATerm act = back.action[to];
  char *actname = ATgetName(ATgetSymbol(act));
  for (;!ATisEmpty(trace_actions);trace_actions=ATgetNext(trace_actions))
     {ATerm trace_action = ATgetFirst(trace_actions);
     char *trace_actname = NULL, *found = NULL;
     if (ATgetType(trace_action)==AT_LIST) {
         trace_action = ATgetFirst((ATermList) trace_action);
         stop = ATtrue;
         }
     trace_actname = ATgetName(ATgetSymbol(trace_action));
     found = strstr(actname, trace_actname);
     if (found == actname) {
        ATfprintf(output, "Action %t encountered. Trace:\n", trace_action);
        if (monitor) ATwarning("Action %t encountered", trace_action);
        PrintTrace(to);
        if (stop) {
            ATfprintf(output,"Searching for traces is halted\n");
            ATwarning("Searching for traces is halted");
            exit(0);
            } 
        else return;
        }
     }    
}

static void StepTrace(int from,  ATerm action, int to) {
     int depth =  -1;
     back = enlarge_back(back, to);
     depth = back.depth[from] + 1;
     if (back.depth[to]==-1 || depth<back.depth[to]) { 
         back.action[to] = action; back.from[to] = from;
         back.depth[to] = depth;
         }
     if (to>0) CheckActions(actions, back, to); 
     visited = max(visited, to);
     }
     
static void FinalTrace(void) {
     fprintf(output,"Searching for traces has been finished.\n");
     fprintf(output,"Explored %d states and generated %d transitions\n",
     explored, transitions);
     fclose(output);
     }
     
static void InitTrace(void) {
     back = enlarge_back(back,0);
     back.depth[0] = 0;
     if (!o_flag) strcat(outputfile,".dlk"); 
     if (!(output = fopen(outputfile,"w")))
           ATerror("File %s cannot be opened", outputfile);
     ATfprintf(output,"Searching traces to one of the actions in:\n%t\n",
            actions);
     }
     
static void AfterStepTrace(int state, int n) {
     if (n==0) {
        fprintf(output, "Deadlock in state %d\n", state);
        if (monitor) ATwarning("Deadlock in state %d\n", state);
        PrintTrace(state);
        }
     }
           
static TASK taskTrace = {InitTrace, StepTrace, AfterStepTrace, FinalTrace};         
/* --- END TRACE DETECTION --- */

/* BEGIN TRANSITION AUT */
    
static void StepTransitionAut(int from,  ATerm action, int to) {
     ATerm actionterm = (cadp && ATisEqual(action, MCRLterm.tau)?
              MCRLterm.i: action);
     fprintf(output, "(%d,",from);
     ATfprintf(output,"%t",actionterm); 
     fprintf(output,",%d)\n",to);
     fflush(output);
     visited = max(visited, to);
     }
     
static void FinalTransitionAut(void) {
     rewind(output);
     fprintf (output, "des (0, %d, %d)", transitions, explored);
     fclose(output);
     }
      
static void InitTransitionAut(void) {
     if (!o_flag) strcat(outputfile,".aut");
     if (!(output = fopen(outputfile,"w")))
           ATerror("File %s cannot be opened", outputfile);
     fprintf (output, "des (0, ?, ?)                     \n");
     fflush(output);
     }

static TASK taskTransitionAut = {InitTransitionAut, StepTransitionAut, 
       (AFTERSTEP) NULL, FinalTransitionAut};

/* END TRANSITION AUT */

/* BEGIN DEADLOCK */

static void InitDeadlock(void) {
     back = enlarge_back(back,0); 
     back.depth[0] = 0; 
     if (!o_flag) strcat(outputfile,".dlk"); 
     if (!(output = fopen(outputfile,"w")))
           ATerror("File %s cannot be opened", outputfile);
     fprintf(output,"Searching deadlocks\n"); 
     }
                                           
static void StepDeadlock(int from,  ATerm action, int to) {
     int depth = -1;
     back = enlarge_back(back,to);
     depth = back.depth[from] + 1;
     if (back.depth[to]==-1 || depth<back.depth[to]) { 
         back.action[to] = action; back.from[to] = from;
         back.depth[to] = depth;
         }
     if (ATisEqual(LTSgetState(to), MCRLterm.terminated)) { 
     if (monitor) ATwarning("Action %t in state %d leads to termination", action, to);
       ATfprintf(output, "Action %t in state %d leads to termination\n",
       action, to);
       }
     visited = max(visited, to);
     }
     
static void AfterStepDeadlock(int state, int n) {
     if (n==0) {
        fprintf(output, "Deadlock in state %d\n", state);
        if (monitor) ATwarning("Deadlock in state %d", state);
        if (state>0) PrintTrace(state);
        }
     }
          
static void FinalDeadlock(void) {
     fprintf(output,"Searching for deadlock has been finished.\n");
     fprintf(output,"Explored %d states and generated %d transitions\n",
     explored, transitions);
     fclose(output);
     }
     
static TASK taskDeadlock = {InitDeadlock, StepDeadlock, AfterStepDeadlock, 
       FinalDeadlock};
            
/* END DEADLOCK */ 

/* BEGIN TRANSITION SVC */
                    
static void StepTransitionSVC(int from, ATerm action, int to) {
     SVCbool new;
     ATerm actionterm = (cadp && ATisEqual(action, MCRLterm.tau)?
          MCRLterm.i: action);
     SVClabelIndex labelIndex = SVCnewLabel(svcFile, actionterm, &new);
     ATerm froms = svc_num? (ATerm) ATmakeInt(from):LTSgetPrintState(from), 
           tos = svc_num?(ATerm) ATmakeInt(to):LTSgetPrintState(to);
     SVCstateIndex toIndex = SVCnewState(svcFile, tos, &new), 
                  fromIndex =SVCaterm2State(svcFile, froms); 
     if (!svc_num) {
         parameterIndex = SVCnewParameter(svcFile, 
             (ATerm) ATmakeInt(LTSgetSmdIndex()+1), &new);
     }
     SVCputTransition(svcFile, fromIndex, labelIndex, toIndex,
          parameterIndex);
     visited = max(visited,to);
     }

static void InitTransitionSVC(void) {
     SVCbool new;
     if (!o_flag) strcat(outputfile,".svc");
     if (SVCopen(svcFile,  outputfile, SVCwrite, &svc_num)<0)
            ATwarning("%s",SVCerror(SVCerrno));
     SVCsetCreator(svcFile , who);
     SVCsetVersion(svcFile , VERSION);
     SVCsetInitialState(svcFile ,SVCnewState(svcFile, 
            (svc_num?(ATerm) ATmakeInt(0):
            LTSgetPrintState(LTSgetInitialState())), &new));
     parameterIndex=SVCnewParameter(svcFile,(ATerm) ATmakeList0(),&new);
     }
     
static void FinalTransitionSVC(void) {     
     SVCclose(svcFile);
     }
      
static TASK taskTransitionSVC = {InitTransitionSVC, StepTransitionSVC, NULL,  
                                 FinalTransitionSVC}; 
                                                                        
/* BEGIN TRANSITION SVC */

/* BEGIN TRANSITION BCG */

#ifdef BCG
static void StepTransitionBCG(int from, ATerm action, int to) {
     BCG_IO_WRITE_BCG_EDGE(from, cadp && ATisEqual(action,
        MCRLterm.tau)?"i":ATwriteToString(action), to);
     visited = max(visited,to);
     }

static void InitTransitionBCG(void) {
     /* Strange bug on solaris when author is not static, even if bcg mode
        is not activated. Don't remove ! */
     static char author[BUFLEN];
     if (!o_flag) strcat(outputfile,".bcg");
     BCG_INIT();
     BCG_IO_WRITE_BCG_SURVIVE(BCG_TRUE);
     snprintf(author, BUFLEN, "Created by %s %s", who, VERSION);
     if (BCG_IO_WRITE_BCG_BEGIN(outputfile, 0, 1, author, monitor))
        ATerror("File %s cannot be opened", outputfile);
     monitor = ATfalse;
     }

static void FinalTransitionBCG(void) {     
     BCG_IO_WRITE_BCG_END();
     }

static TASK taskTransitionBCG = {InitTransitionBCG, StepTransitionBCG, 
                                 (AFTERSTEP) NULL, FinalTransitionBCG};
#endif
/* END TRANSITION BCG */
    
static void CheckRemainingFlags(int argc, char *argv[]) {
    int i; ATbool stop = ATfalse; 
    for (i=1;i<argc;i++) { 
        if (argv[i][0] =='-' && strncmp(argv[i],"-at-",4)) {
           ATwarning("\"%s\" is unknown flag\n", argv[i]);
           stop = ATtrue; 
           }
        }
        if (stop) {helpmsg(); exit(-1);}
    }
    
static void FileNames(char *filename) {
    char *lastdot = strrchr(filename,'.');
    if (lastdot && !strcmp(lastdot,".tbf")) *lastdot ='\0';
    strcpy(inputfile, filename); strcat(inputfile,".tbf");
    if (!outputfile[0]) strcpy(outputfile, filename);
    }
                             
static void Init(int argc, char *argv[]) {
    ATprotect((ATerm*) &actions);
    FileNames(filename);
    if (!MCRLinitNamedFile(inputfile)) ATerror("Error initialise");
    if (RWgetRewriter()==RW_UNDEF) RWsetRewriter(RW_NORMAL);
    LTSsetArguments(&argc,&argv, task->instep);
    CheckRemainingFlags(argc, argv);
    if (!RWinitialiseRewriter(MCRLgetAdt(), 0, hash)) 
          ATerror("Initialize rewriter");
    LTSinitialize(); 
    if (task && task->init) task->init();   
    }
    
static void Monitor(void) {
     if (explored % 1000 == 0) 
     ATwarning("Explored %d and visited %d states and %d transitions",
          explored, visited+1, transitions);
}



static void EndMessage() {
     ATwarning("Finished.");
     if (monitor) {
          int n = ATgetLength(MCRLgetListOfSummands()),
          cnt = LTSnumberOfUsedSummands();
          if (cnt<n) 
          ATwarning("Number of summands: %d - Number of used summands: %d",
              n, cnt);
          }
     ATwarning("Explored %d states and generated %d transitions",
          explored, transitions);
     if (task && task->final) task->final();       
#ifdef INSTRUMENTED
     LTSreport(); 
#endif 
     }
     
static void Instantiator(void) {
   for (explored=0;explored<=visited;explored++) {
     int r = 0;
     if (monitor) Monitor();
     r = LTSstep(explored);
     if (r<0) ATerror("Error.");
     if (task && task->afterstep) task->afterstep(explored, r);  
     transitions += r; 
   }
   EndMessage();
}
                   
static void WarningHandler(const char *format, va_list args) {
     fprintf(stderr,"%s: ", who);
     ATvfprintf(stderr, format, args);
     fprintf(stderr,"\n");
     }
     
static void ErrorHandler(const char *format, va_list args) {
     fprintf(stderr,"%s: ", who);
     ATvfprintf(stderr, format, args);
     fprintf(stderr,"\n");
     exit(-1);
     }

static void setTask(TASK *taskPar) {
     if (task) ATerror("Illegal combination of flags");
     task = taskPar;
     }
              
int main(int argc, char *argv[])
     {
     int i, j = 0;
     char **newargv = (char**) calloc(argc + 1, sizeof(char*));
     if (!newargv) ATerror("Cannot allocate array argv"); 
     newargv[j++] = argv[0];
     ATinitialize(argc, argv);
     ATsetWarningHandler(WarningHandler);
     ATsetErrorHandler(ErrorHandler);
     if (argc > 1 && argv[argc-1][0]!='-') {
          strncpy(filename, argv[argc-1],BUFLEN-5);
          argc--;
          }
     else filename[0] = '\0';
     outputfile[0]='\0';
     for (i=1;i<argc;i++) {
          if (!strcmp(argv[i],"-help"))
               {
               help();
               exit(0);
               }
          if (!strcmp(argv[i],"-version"))
               {
               version();
               exit(0);
               }
          
          if (!strcmp(argv[i],"-monitor"))
               {
               monitor = ATtrue;
               continue;
               }
          if (!strcmp(argv[i],"-alt"))
            {
            if ((++i)<argc && strncmp(argv[i],"-",1)) {
                char *code = argv[i];
                RWsetRewriter(RW_VDPOL);
                if (!strcmp(code,"innermost"));
                else
                if (!strcmp(code,"strictleft"))
                     {if (hash<2) hash+=2;}
                else
                ATerror("Illegal strategy");
                continue;
                }
            else
               ATerror("After flag -alt argument expected");
            }
          if (!strcmp(argv[i],"-o")) {
            if ((++i)<argc && strncmp(argv[i],"-",1))
                {
                char *file = argv[i];
                strncpy(outputfile, file, BUFLEN); 
                o_flag = ATtrue;
                continue;
                }
            else
               ATerror("After flag -o filename expected");
            }
          if (!strcmp(argv[i],"-simple"))
               {
               RWsetRewriter(RW_SIMPLE);
               hash = 0;
               continue;
               }
          if (!strcmp(argv[i],"-nohash"))
               {
               hash = (hash/2)*2;
               if (RWgetRewriter()==RW_NORMAL) 
                    RWsetRewriter(RW_SIMPLE);
               continue;
               }
          if (!strcmp(argv[i],"-deadlock")) {
               setTask(&taskDeadlock);
               continue;
               }
         if (!strcmp(argv[i],"-aut")) {
               setTask(&taskTransitionAut);
               continue;
               }
         if (!strcmp(argv[i],"-trace")) {
               if ((++i)<argc && strncmp(argv[i],"-",1)) {
                actions = ParseTraceActions(argv[i]);
                setTask(&taskTrace); 
                continue;
                }
            else
               ATerror("After flag -trace trace-expression expected");
            }
#ifdef BCG
          if (!strcmp(argv[i],"-bcg")) {
               cadp = BCG_TRUE;
               setTask(&taskTransitionBCG);
               continue;
               }
#endif
          if (!strcmp(argv[i],"-svc-term") || !strcmp(argv[i],"-svc-all")) {
               setTask(&taskTransitionSVC);
               continue;
               }
          if (!strcmp(argv[i],"-svc-num") || !strcmp(argv[i],"-svc")) {
               svc_num = 1;
               setTask(&taskTransitionSVC);
               continue;
               }
          if (!strcmp(argv[i],"-i")) {
               cadp = ATtrue;
               continue;
               }
          newargv[j++] = argv[i];
          }
     if (filename[0]=='\0') ATerror("Last argument must be a file name\n");
     if (!task) task = &taskTransitionAut;
     Init(j, newargv);
     Instantiator();
     exit(0);
     }