/* $Id: inst.c,v 1.24 2001/06/06 13:53:18 bertl Exp $ */

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

#include <unistd.h>
#include "rw1.h"

#include "rw2.h"
#define ROBUST 0

#ifdef SVC
#include "svc.h"
#include "svcerrno.h"
#endif

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

/* #define CASEFUNCTION 1 */

char *who = "Instantiator";

static FILE  *out = NULL;


 
#define P(msg)  fprintf(stderr,"%s\n",msg)
#define ERRORLENGTH 1024

static char filename[ERRORLENGTH], outputfile[ERRORLENGTH];
static ATerm  false_term, true_term, term_terminated, tau_term, i_term;

char* ctau_name;
ATbool CRreducing=ATfalse;
extern int tarjan;

static unsigned int cursor = 0, explored = 0, deadlock = 0,
order = 1, hash = 1, prerewrite = 0, caseflag = 0;
#ifdef SVC
static unsigned int svc = 0;
static SVCbool svc_num = 0;
static SVCfile svcFile[1];
static SVCparameterIndex parameterIndex;
#endif
#ifdef BCG
static BCG_TYPE_BOOLEAN bcg = BCG_FALSE;
#endif

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("-case:\t\tchecks case functions during rewriting");
    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("-monitor:\tMonitor function on");
    P("-confluent <action>:\t Declares <action> as the confluent tau action and");
    P("\t\t\t enables confluent tau reduction using an algorithm");
    P("\t\t\t derived from the Tarjan SCC algorithm.");
    P("-confluent-old <action>: Declares <action> as the confluent tau action and");
    P("\t\t\t enables confluent tau reduction using the old algorithm.");
    P("\t\t\t The old algorithm may fail for confluent tau loops.");
    P("\t\t\t This option is provided for testing only.");
    P("\t\t\t WARNING: This tool does not check if that action is confluent"); 
    P("-svc:\t\twrites transition system in SVC format");
    P("-svc-num:\tsee -svc, 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("-order <label>:\tdefinition kind of ordening of sum variables");
    P("\t\tin a summand in which <label> stands for:");
    P("\t\t\"no\",\"enum_big_freq\",\"big_freq\", or \"min_depth\"");
    P("\t\t\"big_freq\" means that the sumvariable which occurs at most");
    P("\t\tin the condition of that summand will be enumerated first.");
    P("\t\tDefault is \"enum_big_freq\" which means that first the variables");
    P("\t\tof enumerated type will be enumerated (conform \"big_freq\") and");
    P("\t\tthen the others (conform \"big_freq\").");
    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."); 
    }
    
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

     
static int print_term (FILE *f, ATerm t);

static int print_terms (FILE *f, ATermList terms)
{ 
  for (;!ATisEmpty(terms);terms=ATgetNext(terms),
       !ATisEmpty(terms)? (cursor += fprintf(f,",")):0)
       {
       ATerm term = ATgetFirst(terms);
       cursor = print_term(f, term);
       }
  return cursor;
}

static int print_term (FILE *f, ATerm t)
{
 ATermList terms = ATgetArguments((ATermAppl) t);
 int n = ATgetLength(terms);
 char *name =  RWgetName(t);
 cursor += fprintf(f, "%s",name);
 if (n) 
      {
      cursor+= fprintf(f,"(");
      cursor = print_terms (f, terms);
      cursor+= fprintf(f,")");
      }
 return cursor;
 }

static int PrintAction(FILE *f, ATerm actname, ATermList actargs)
     {
     cursor = 0;
     if (cadp && ATisEqual(actname, tau_term)) 
          {
          cursor += fprintf(f,"i");
          return cursor;
          }
     fprintf(f, "\"%s",RWgetName(actname));
     if (!ATisEmpty(actargs))
          {
          cursor += fprintf(f,"(");
          cursor = print_terms(f, actargs);
          cursor += fprintf(f,")");
          }
     fprintf(f,"\"");
     return cursor;
     }

static void PrintTransition(int from, int to, ATerm actname, ATermList actargs)
     {
     fprintf(out, "(%d,",from);
     PrintAction(out, actname,  RWrewriteList(actargs));   
     fprintf(out,",%d)\n",to);
     fflush(out);
     }
      
#ifdef BCG
static void OutputTransitionBCG (int from, int to, ATerm actname, 
     ATermList actargs)
     {     
     /* snprint is more secured than strncpy when overflow occurs */
     snprintf(filename, ERRORLENGTH, "%s",
	cadp && ATisEqual(actname, tau_term)?"i":
	  ATwriteToString(RWprint((ATerm) ATmakeApplList(
	    ATmakeSymbol(ATgetName(ATgetSymbol(actname)),ATgetLength(actargs),
	    ATtrue), RWrewriteList(actargs)))));
     BCG_IO_WRITE_BCG_EDGE(from, filename, to);
     }
#endif

#ifdef SVC           
static void OutputTransitionSVC(int from, int to, ATerm actname, 
     ATermList actargs)
     {
     SVCbool new;
     strncpy(filename, 
     ATwriteToString(
     RWprint((ATerm) ATmakeApplList(
      ATmakeSymbol(ATgetName(ATgetSymbol(actname)),ATgetLength(actargs), ATtrue),
      RWrewriteList(actargs)))),ERRORLENGTH);
     {
     ATerm action = cadp && ATisEqual(actname, tau_term)?
          i_term: ATmake("<str>", filename);
     SVClabelIndex labelIndex = SVCnewLabel(svcFile, action, &new);
     if (svc_num)
     {
     ATerm tos = (ATerm) ATmakeInt(to), froms = (ATerm) ATmakeInt(from);
     SVCstateIndex toIndex = SVCnewState(svcFile, tos, &new),
          fromIndex = SVCaterm2State(svcFile, froms);
          SVCputTransition(svcFile, fromIndex, labelIndex, toIndex,
               parameterIndex);
     }
     else
     {
     ATermList froms = RWprintList(RWgetState(from)),
     tos = RWgetState(to);
     if (!ATisEqual(ATgetFirst(tos), term_terminated)) 
          tos = RWprintList(tos);
	  /*
	  ATwarning("%t %t",ATelementAt(tos,2),tos);
	  */
          {
          SVCstateIndex toIndex = SVCnewState(svcFile, (ATerm) tos, &new),
          fromIndex = SVCaterm2State(svcFile, (ATerm) froms);
          SVCputTransition(svcFile, fromIndex, labelIndex, toIndex,
               parameterIndex);
          }
     }
     }
     }
#endif 
               
static int Init(int argc, char *argv[])
    {
    char *lastdot = NULL;
    if (argc > 1 && argv[argc-1][0]!='-')
          {
          strncpy(filename, argv[argc-1],ERRORLENGTH-5);
          }
    else filename[0] = '\0';
    lastdot = strrchr(filename,'.');
    if (!lastdot || strcmp(lastdot,".tbf"))
         {
         /* filename without extension means filename.tbf */
         lastdot = filename + strlen(filename); 
         strcat(filename, ".tbf");
         }
#ifdef SVC
    if (svc)
         {
         if (!RWinitStepper(filename, hash, OutputTransitionSVC, order, 
              prerewrite, argc, argv))  return 0;
         }
    else
#endif
#ifdef BCG
    if (bcg)
         {
         if (!RWinitStepper(filename, hash, OutputTransitionBCG, order, 
              prerewrite, argc, argv))  return 0;
         }
    else
#endif
     if (!RWinitStepper(filename, hash, deadlock?NULL:PrintTransition, order, 
         prerewrite, argc, argv))  return 0;
     if (outputfile[0]) strcpy(filename, outputfile);
     lastdot = strrchr(filename,'.');
#ifdef SVC
     if (svc)
          {
          if (lastdot) 
	      strcpy(lastdot,".svc");
	  else
	      strcat(filename,".svc");
          if (SVCopen(svcFile,  filename, SVCwrite, &svc_num)<0)
               ATwarning("%s",SVCerror(SVCerrno));
          SVCsetCreator(svcFile , who);
          SVCsetVersion(svcFile , VERSION);
          }
#endif
#ifdef BCG
     if (bcg)
	  {
          /* Strange bug on solaris when author is not static, even if bcg mode
             is not activated. Don't remove ! */
	  static char author[ERRORLENGTH];
	  if (lastdot) 
	      strcpy(lastdot,".bcg");
	  else
	      strcat(filename,".bcg");
	  BCG_INIT();
	  BCG_IO_WRITE_BCG_SURVIVE(BCG_TRUE);
	  snprintf(author, ERRORLENGTH, "Created by %s %s", who, VERSION);
	  if (BCG_IO_WRITE_BCG_BEGIN(filename, 0, 1, author, monitor))
	      ATerror("Can't write file %s", filename);
          monitor = ATfalse;
	  }
#endif

    ATprotect(&false_term);
    ATprotect(&true_term);
    ATprotect(&tau_term);
    ATprotect(&i_term);
    ATprotect(&term_terminated);
    term_terminated = ATmake("<appl>","terminated");
    false_term= ATmake("<str>","F#");
    true_term= ATmake("<str>","T#");
    /* Needed for reading old 2gen tbf files */
    if (!RWgetSort(false_term))
	{
        false_term= ATmake("<str>","F");
        true_term= ATmake("<str>","T");
	}
    tau_term= ATmake("<str>","tau");
    i_term= ATmake("<appl>","i");
#ifdef SVC
    if (!svc)
#endif
#ifdef BCG
    if (!bcg)
#endif
    {
    if (lastdot)
	if (deadlock) strcpy(lastdot,".dlk");else strcpy(lastdot,".aut");
    else
	if (deadlock) strcat(filename,".dlk");else strcat(filename,".aut");
    if (!(out = fopen(filename,"w")))
	{
        ATerror("File %s cannot be opened", filename);
	return 0;
	}
    if (deadlock)
         fprintf(out,"Searching deadlocks\n");
    else
         fprintf (out, "des (0, ?, ?)                     \n");
    fflush(out);
    }
    return 1;
    }    
          
static void Step(void)
/*
Computes from the entered states the next states 
which are not explored earlier\n")
*/
     { 
     int n = RWgetVisited(),  step_result = 0;
     for (;explored <= n ; explored++)
          {
          if (monitor && explored % 1000 == 0)
                {
          ATwarning("Explored %d and visited %d states and %d transitions",
          explored, RWgetVisited()+1, RWgetTransitions());
                }       
          step_result = RWstepper(explored);  
          if (step_result < -1) /*error */ return;
          if (deadlock) 
               if (step_result == 0)
               { 
               fprintf(out,"%d\n",explored);
               fflush(out);
               }
               else if (step_result == -1)
               {
               fprintf(out, "TERMINATED %d\n",explored);
               fflush(out);
               } 
          }
     }

              
static void Instantiator(void)
     {
#ifdef SVC
     if (svc)
          {
          SVCbool new;
          {
          if (svc_num)
               {
               SVCstateIndex newState = SVCnewState(svcFile, (ATerm)
                    (ATerm) ATmakeInt(0), &new);
               SVCsetInitialState(svcFile, newState);
               }
          else
               {
               SVCstateIndex newState = SVCnewState(svcFile, (ATerm)
                         RWprintList(RWgetState(0)), &new);
               SVCsetInitialState(svcFile, newState);
               }
          parameterIndex=SVCnewParameter(svcFile,(ATerm) ATmakeList0(),&new);
          }
          }     
#endif
     while (explored <= RWgetVisited()) 
          {
          Step();
          }
          
#ifdef SVC
     if (!svc)
#endif
#ifdef BCG
     if (!bcg)
#endif
     if (deadlock)
          {
          fprintf(out,
          "Searching for deadlocks has been finished. \n");
          fprintf(out,"Visited %d states and generated %d transitions\n",
               RWgetVisited()+1, RWgetTransitions());
          fclose(out);
          }
     else
          {
          rewind(out);
          fprintf (out, "des (0, %d, %d)", (int) RWgetTransitions(), (int)
               RWgetVisited()+1);
          fclose(out);
          } 
     ATwarning("Finished.");
     if (monitor) {
          int cnt = RWgetNumberOfVisitedSummands();
          if (cnt>0) 
          ATwarning("From the %d summands of the LPE are not used: %d summands\n", 
              RWgetNumberOfSummands(), cnt);
          }
     ATwarning("Visited %d states and generated %d transitions",
          RWgetVisited()+1, RWgetTransitions());
#ifdef SVC
     if (svc) SVCclose(svcFile);
#endif
#ifdef BCG
     if (bcg) BCG_IO_WRITE_BCG_END();
#endif
     } 
         
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);
     }
         
int main(int argc, char *argv[])
     {
     int i;
     outputfile[0]='\0';
     for (i=1;i<argc;i++)
     if (strlen(argv[i]))
          {
          if (!strcmp(argv[i],"-help"))
               {
               help();
               exit(0);
               }
          if (!strcmp(argv[i],"-version"))
               {
               version();
               exit(0);
               }
          if (!strcmp(argv[i],"-case"))
               {
	       /* case functions are in front of condition */
               order = 2;
               caseflag = 1;
               argv[i]="";
               continue;
               }
          if (!strcmp(argv[i],"-monitor"))
               {
               monitor = ATtrue;
               argv[i] = "";
               continue;
               }
          if (!strcmp(argv[i],"-alt"))
            {
            if (i<argc-2 && strncmp(argv[i+1],"-",1))
                {
                char *code = argv[i+1];
                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");
            continue;
            }
          if (!strcmp(argv[i],"-o"))
            {
            if (i<argc-2 && strncmp(argv[i+1],"-",1))
                {
                char *file = argv[i+1];
                strncpy(outputfile, file, ERRORLENGTH);
                continue;
                }
            else
               ATerror("After flag -o filename expected");
            continue;
            }
          if (!strcmp(argv[i],"-simple"))
               {
               RWsetRewriter(RW_SIMPLE);
               hash = 0;
               continue;
               }
          if (!strcmp(argv[i],"-confluent") || !strcmp(argv[i],"-confluent-old"))
               {
		tarjan = !strcmp(argv[i],"-confluent");
               CRreducing = ATtrue;
               argv[i] = "";
		i++;
		if(i>=argc) ATerror("Option %s needs argument.\n",argv[i]);
		ctau_name=argv[i];
               argv[i] = "";
               continue;
               }
          if (!strcmp(argv[i],"-nohash"))
               {
               hash = (hash/2)*2;
               if (RWgetRewriter()==RW_NORMAL) 
                    RWsetRewriter(RW_SIMPLE);
               argv[i] = "";
               continue;
               }
          if (!strcmp(argv[i],"-deadlock"))
               {
               deadlock = ATtrue;
               argv[i] = "";
               continue;
               }
#ifdef BCG
          if (!strcmp(argv[i],"-bcg"))
               {
               bcg = BCG_TRUE;
               cadp = BCG_TRUE;
               argv[i] = "";
               continue;
               }
#endif
#ifdef SVC
          if (!strcmp(argv[i],"-svc") || !strcmp(argv[i],"-svc-all"))
               {
               svc = 1;
               argv[i] = "";
               continue;
               }
          if (!strcmp(argv[i],"-svc-num"))
               {
               svc = 1; svc_num = 1;
               argv[i] = "";
               continue;
               }
#endif
          if (!strcmp(argv[i],"-i"))
               {
               cadp = ATtrue;
               argv[i]="";
               continue;
               }
          if (!strcmp(argv[i],"-prerewr"))
               {
               prerewrite = 1;
               argv[i]="";
               continue;
               }
          if (!strcmp(argv[i],"-order"))
            {
            if (i<argc-2 && strncmp(argv[i+1],"-",1))
                {
                char *code = argv[i+1];
                if (!strcmp(code,"no"))
                     order = 0;
                else 
                if (!strcmp(code,"enum_big_freq"))
                     order = 1;
                else
                if (!strcmp(code,"big_freq")) 
                     order = 3;
                else
                if (!strcmp(code,"min_depth"))
                     order = 2;
                else
                ATerror("Illegal order key");
                continue;
                }
            else
               ATerror("After flag -order argument expected");
            continue;
            }
          if (!strncmp(argv[i],"-at",3))
               {
               continue;
               }
         /* if (!strcmp(argv[i],"-regular") || !strcmp(argv[i],"-cluster")
              || !strcmp(argv[i],"-nocluster"))
               {
               continue;
               } */
          if (argv[i][0] =='-')
               {
               ATwarning("\"%s\" is unknown flag\n", argv[i]);
               helpmsg();
               exit(1);
               }
          }
     ATsetWarningHandler(WarningHandler);
     ATsetErrorHandler(ErrorHandler);
     if (!Init(argc, argv)) exit(1);
     Instantiator();
	RWprintStats();
     exit(0);
     }