/* *****************************************************************

Parameters:
-help
-model
-process

-trace = trace minimization
-weak = weak minimization
-strong = strong minimization

****************************************************************** */

#include <bdd.h>
#include <pa.h>
#include <versis.h>
#include <ccs.h>

#define PROGNAME "min"

static void concat(char **s1, const char *s2);

void hello() {
  printf("=======================================================================\n");
  printf("   Minimization (from EST project)\n");
  printf("=======================================================================\n");
}

int main(int argc, char **argv)
{
  int i;
  int mctype;
  Est_Boolean help;
  int type;
  Est_String ccsname,procname,outname;
  int p;

  ccsname = NULL;
  procname = NULL;

  if (argc == 1) {
    help = TRUE;
  } else {
    help = FALSE;
  }

  type = -1;

  i = 1;
  while (i<argc) {

    if (!strcmp(argv[i],"-help")) {
      help = TRUE;
    }

    if (!strcmp(argv[i],"-model")) {
      ccsname = strdup(argv[++i]);
    }

    if (!strcmp(argv[i],"-process")) {
      procname = strdup(argv[++i]);
    }

    if (!strcmp(argv[i],"-strong")) {
      if (type == -1) {
  	outname = strdup("STRONG_");
        type = 0;
      } else {
        help = TRUE;
      }
    }

    if (!strcmp(argv[i],"-weak")) {
      if (type == -1) {
  	outname = strdup("WEAK_");
        type = 1;
      } else {
        help = TRUE;
      }
    }

    if (!strcmp(argv[i],"-trace")) {
      if (type == -1) {
  	outname = strdup("TRACE_");
        type = 3;
      } else {
        help = TRUE;
      }
    }

    i++;
  }

  hello();

  if (type == -1) {
    help = TRUE;
  }

  if (help) {
    printf("Usage: %s -trace -model ccsname -process procname\n",PROGNAME);
    printf("Parameters:\n");
    printf("  -model ccsname    the file with CCS model description\n");
    printf("  -process procname the name of process to be minimized\n");
    printf("Morevover, you must add one of the following parameters:\n");
    printf("  -trace = trace minimization\n");
    printf("  -weak = weak minimization\n");
    printf("  -strong = strong minimization\n");
    return 1;
  }

  if (!ccsname) {
    printf("\nERROR: The file with CCS model description must be specified.\n");
    printf("HELP: Use: -model ccsname\n");
    return 1;
  }

  if (!procname) {
    printf("\nERROR: The name of the process must be specified.\n");
    printf("HELP: Use: -process procname\n");
    return 1;
  }

  /* *********************************************************************** */
  /* *********************************************************************** */

  Bdd_InitPkg();
  Pa_InitPkg();
  Versis_InitPkg();
  Ccs_InitPkg();
 
  /* *********************************************************************** */
  printf("Loading the model ...");
  /* *********************************************************************** */

  Ccs_ParseCCS(ccsname,TRUE); /* TRUE is used to make it quiet */ 

  p = Pa_FindProcess(procname);
  if (p == -1) {
    printf("\nProcess %s does not exist.\n",procname);
  } else {

    /* *********************************************************************** */
    printf("Encoding the model ...\n");
    /* *********************************************************************** */

    Pa_EncodeProcess(procname);

    printf("  Process %s has %d states.\n",procname,Pa_DecodeProcessStates(
              &pa_processTable[p],pa_processTable[p].stateBDD,FALSE));
    printf("    State table has %d records.\n",
              pa_processTable[p].numStates);
    printf("    Transition relation includes %d states.\n",Pa_DecodeProcessStates(
              &pa_processTable[p],
              Bdd_ITE(Bdd_RelOpSimple(pa_processTable[p].d,"Ex xA xS",TRUE),
                   bdd_termTrue,
                   Bdd_RelOpSimple(pa_processTable[p].d,"Ex xA xR S2R",TRUE)),
              FALSE));
    printf("    States are encoded using %d state variables.\n",
           pa_processTable[p].numVar);
    printf("  Process %s has %d actions.\n",procname,
              pa_sortTable[pa_processTable[p].sort].numActions);
    printf("    Transition relation includes %d actions.\n",Pa_DecodeSortActions(
	      &pa_sortTable[pa_processTable[p].sort],
              Bdd_RelOpSimple(pa_processTable[p].d,"Ex xR xS",TRUE),
              FALSE));
    printf("    Actions are encoded using %d action variables.\n",
              pa_sortTable[pa_processTable[p].sort].numVar);
    printf("  Process %s has %d transitions.\n",procname,Pa_DecodeProcessTR(
           &pa_processTable[p],pa_processTable[p].d,FALSE));

    /* *********************************************************************** */
    printf("Minimizing the model ...\n");
    /* *********************************************************************** */

    Versis_Minimization(type,0,procname);
    concat(&outname,procname);
    p = Pa_FindProcess(outname);

    printf("  Minimized process has %d states.\n",Pa_DecodeProcessStates(
              &pa_processTable[p],pa_processTable[p].stateBDD,FALSE));
    printf("    State table has %d records.\n",
              pa_processTable[p].numStates);
    printf("    Transition relation includes %d states.\n",Pa_DecodeProcessStates(
              &pa_processTable[p],
              Bdd_ITE(Bdd_RelOpSimple(pa_processTable[p].d,"Ex xA xS",TRUE),
                   bdd_termTrue,
                   Bdd_RelOpSimple(pa_processTable[p].d,"Ex xA xR S2R",TRUE)),
              FALSE));
    printf("    States are encoded using %d state variables.\n",
           pa_processTable[p].numVar);
    printf("  Minimized process has %d actions.\n",
              pa_sortTable[pa_processTable[p].sort].numActions);
    printf("    Transition relation includes %d actions.\n",Pa_DecodeSortActions(
	      &pa_sortTable[pa_processTable[p].sort],
              Bdd_RelOpSimple(pa_processTable[p].d,"Ex xR xS",TRUE),
              FALSE));
    printf("    Actions are encoded using %d action variables.\n",
              pa_sortTable[pa_processTable[p].sort].numVar);
    printf("  Minimized process has %d transitions.\n",Pa_DecodeProcessTR(
           &pa_processTable[p],pa_processTable[p].d,FALSE));

    /* *********************************************************************** */
    printf("\nRESULT\n");
    /* *********************************************************************** */

    Pa_WriteProcessCCS(outname,1);
  }

  /* *********************************************************************** */
  /* *********************************************************************** */

  Ccs_ExitPkg();
  Versis_ExitPkg();
  Pa_ExitPkg();
  Bdd_ExitPkg();

  return(0);
}

/* ******************************************************* */
/* LOCAL FUNCTIONS - it is a good idea to make them static */
/* ******************************************************* */

static void
concat(char **s1, const char *s2)
{
   *s1 = (char*) realloc(*s1,strlen(*s1)+strlen(s2)+1);
   strcat(*s1,s2);
}
