/**CFile*******************************************************************
  PackageName [versis]
  Synopsis    [Package 'versis' provides basic tools for formal
               verification of concurrent systems]

  FileName    [versisMin.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si),
               Tatjana Kapus (kapus@uni-mb.si)]
  Description [File versisMin.c provides different minimizations.]
  SeeAlso     [versis.h, versisInt.h]

  Copyright   [This file is part of EST (Efficient Symbolic Tools).
               Copyright (C) 2003, 2013
               UM-FERI, Smetanova ulica 17, SI-2000 Maribor, Slovenia

               EST is free software; you can redistribute it and/or modify
               it under the terms of the GNU General Public License as
               published by the Free Software Foundation; either version 2
               of the License, or (at your option) any later version.

               EST is distributed in the hope that it will be useful,
               but WITHOUT ANY WARRANTY; without even the implied warranty of
               MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
               GNU General Public License for more details.

               You should have received a copy of the GNU General Public
               License along with this program; if not, write to the Free
               Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
               Boston, MA 02110-1301 USA.]
  ************************************************************************/

#include "versisInt.h"

/*-----------------------------------------------------------------------*/
/* Structure declarations                                                */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* Variable declarations                                                 */
/*-----------------------------------------------------------------------*/

/**AutomaticStart*********************************************************/

/*-----------------------------------------------------------------------*/
/* Static function prototypes                                            */
/*-----------------------------------------------------------------------*/

static Est_Boolean Minimization(Est_String pref, Bdd_Edge eqv,
                                int par, int n, int type);

/**AutomaticEnd***********************************************************/

/*-----------------------------------------------------------------------*/
/* Definition of exported functions                                      */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    [Function Versis_Minimization.]
  Description [type = 0,1,3,4 - strong, weak, trace, trace_strong
               type = 2 - testing (not implemented)
               type = 5 - minimization of WCA]
  SideEffects [trace minimization returns minimal deterministic LTS]
  SeeAlso     []
  ************************************************************************/

int
Versis_Minimization(int type, int par, Est_String name)
{
  int n = -1;
  Est_String newname;
  int result;

  if (par == 0) {
    n = Pa_FindProcess(name);
    if (n == -1) {
      printf(" Proces %s does not exist.\n",name);
      return -1;
    }
    if ( (!pa_processTable[n].encoded) && (type != 5) ) {
      printf(" Proces %s is not encoded.\n",name);
      return -1;
    }
  }
  if (par == 1) {
    n = Pa_FindComposition(name);
    if (n == -1) {
      printf(" Composition %s does not exist.\n",name);
      return -1;
    }
    if (Bdd_isEqv(pa_compositionTable[n].transitionBDD,bdd_termFalse)) {
      printf(" Composition %s is empty.\n",name);
      return -1;
    }
  }

  result = -1;
  switch (type) {
    case 0: {
              newname = strdup("STRONG_");
              newname = (Est_String)
                            realloc(newname,strlen(newname)+strlen(name)+1);
              strcat(newname,name);

              result = VersisStrongMinimization(newname,par,n);

              free(newname);
              break;
            }

    case 1: {
              newname = strdup("WEAK_");
              newname = (Est_String)
                            realloc(newname,strlen(newname)+strlen(name)+1);
              strcat(newname,name);

              result = VersisWeakMinimization(newname,par,n);

              free(newname);
              break;
            }

    case 2: {
              break;
            }

    case 3: {
              newname = strdup("TRACE_");
              newname = (Est_String)
                            realloc(newname,strlen(newname)+strlen(name)+1);
              strcat(newname,name);

              result = VersisTraceMinimization(0,newname,par,n);

              free(newname);
              break;
            }

    case 4: {
              newname = strdup("TRACE_STRONG_");
              newname = (Est_String)
                            realloc(newname,strlen(newname)+strlen(name)+1);
              strcat(newname,name);

              result = VersisTraceMinimization(1,newname,par,n);

              free(newname);
              break;
            }

    case 5: {
              newname = strdup("MIN_");
              newname = (Est_String)
                            realloc(newname,strlen(newname)+strlen(name)+1);
              strcat(newname,name);

              result = VersisWCAMinimization(newname,par,n);

              free(newname);
              break;
            }
  }

  return result;
}

/*-----------------------------------------------------------------------*/
/* Definition of internal functions                                      */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
VersisStrongMinimization(Est_String name, int par, int n)
{
  Bdd_Edge eqv;

  VersisStrongEquivalence(&eqv,par,n,-1,-1);

  /*
  Pa_DecodeProcProcPair(&pa_processTable[n],&pa_processTable[n],eqv,TRUE);
  */

  Minimization(name,eqv,par,n,0);

  return Pa_FindProcess(name);
}


/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
VersisWeakMinimization(Est_String name, int par, int n)
{
  Bdd_Edge eqv;

  VersisWeakEquivalence(&eqv,par,n,-1,-1);

  /*
  Pa_DecodeProcProcPair(&pa_processTable[n],&pa_processTable[n],eqv,TRUE);
  */

  Minimization(name,eqv,par,n,1);

  return Pa_FindProcess(name);
}


/**Function****************************************************************
  Synopsis    []
  Description [type: 0 = weak = tau is an internal action,
                     1 = strong = tau is not a special action]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
VersisTraceMinimization(int type, Est_String name, int par, int n)
{
  Bdd_Edge D;
  int i,s;
  Bdd_Edge tau, stab, init, Ptau, trcl;
  Est_String inname, name1, orgname;
  Bdd_Edge pom, eps, eps_rp, eps_qs;
  Bdd_Edge eqv;
  int det;

  if (par == 0) {
    D = pa_processTable[n].d;
    inname = pa_processTable[n].name;
    init = pa_processTable[n].tableS[pa_processTable[n].initial].bddR;
    orgname = strdup(inname);
    s = pa_processTable[n].sort;      /* sort */
    tau = pa_sortTable[s].table[0].p; /* tau */
  } else {
    D = pa_compositionTable[n].transitionBDD;
    inname = pa_compositionTable[n].name;
    init = pa_compositionTable[n].initialBDD;
    orgname = NULL;
    s = pa_compositionTable[n].sort;  /* sort */
    tau = pa_sortTable[s].table[0].p; /* tau */
  }

  if (Bdd_isNull(D)) {
    return -1;
  }

  /* NAME OF DETERMINISTIC PROCESS */
  name1 = (Est_String) strdup("DET_");
  name1 = (Est_String) realloc(name1,strlen(name1)+strlen(inname)+1);
  strcat(name1,inname);

  /* dolocimo Ptau - kam vse lahko gres iz posameznega stanja */
  /* eps so tau prehodi v D */

  if (type == 0) {
    pom = Bdd_RelOp(D,tau,"#AND Ex xA",TRUE);
    trcl = VersisTrCl(pom);
    Bdd_Fortify(trcl);
    Bdd_IncCounter();

    if (par == 0) {
      stab = pa_processTable[n].stab;
    } else {
      stab = bdd_termTrue;
      for(i=0; i<pa_compositionTable[n].numProcesses; i++) {
        stab = Bdd_ITE(stab,
                       pa_processTable[pa_compositionTable[n].tableP[i]].stab,
                       bdd_termFalse);
      }
    }

    eps = Bdd_ITE(trcl,bdd_termTrue,stab);
    eps_rp = Bdd_RelOpSimple(eps,"S2P",TRUE);
    eps_qs = Bdd_RelOpSimple(eps,"R2Q",TRUE);
    Bdd_IncCounter();
    Bdd_Fresh(eps_rp);
    Bdd_Fresh(eps_qs);

    pom = Bdd_RelOpSimple(D,"R2P S2Q",TRUE);
    pom = Bdd_RelOp(pom,eps_rp,"#AND Ex xP",TRUE);  /* z leve mnozimo s tau prehodi */
    pom = Bdd_RelOp(pom,eps_qs,"#AND Ex xQ",TRUE);  /* z desne mnozimo s tau prehodi */
    Ptau = Bdd_ITE(tau,bdd_termFalse,pom);          /* brisemo tau prehode */
    Bdd_Fortify(Ptau);
    Bdd_IncCounter();
  }

  if (type == 1) {
    trcl = bdd_termFalse;
    Ptau = D;
  }

  /*
  printf("<Deterministic process>");
  */

  VersisBuildDet(orgname,name1,init,Ptau,trcl,s);
  det = Pa_FindProcess(name1);

  if (name1) free(name1);
  if (orgname) free(orgname);

  /* CHECK THE NUMBER OF STATES IN det - BEFORE MINIMIZATION */
  /*
  int i;
  i = Pa_DecodeProcessStates(&pa_processTable[det],pa_processTable[det].stateBDD,FALSE);
  printf("<%d states>",i);
  i = Pa_DecodeProcessTR(&pa_processTable[det],pa_processTable[det].d,FALSE);
  printf("<%d transitions>",i);
  */

  /* THIS METHOD FINDS A PROCESS WHICH IS NOT MINIMAL      */
  /* IT IS BISIMULATION EQUIVALENT TO THE MINIMAL PROCESS  */
  /*
  name1 = strdup(pa_processTable[det].name);
  Pa_CopyProcess(name1,name,NULL,"","");
  Pa_DeleteProcess(Pa_FindProcess(name1));
  free(name1);
  */

  /* THIS METHOD FINDS MINIMAL DETERMINISTIC PROCESS  */
  /* IT IS MUCH MORE COMPLEX THAN THE PREVIOUS METHOD */
  /**/
  VersisStrongEquivalence(&eqv,0,det,-1,-1);
  Minimization(name,eqv,0,det,3);
  /**/

  Pa_DeleteProcess(det);
  det = Pa_FindProcess(name);

  /* CHECK THE NUMBER OF STATES IN det - AFTER MINIMIZATION */
  /*
  printf(" (AFTER)");
  i = Pa_DecodeProcessStates(&pa_processTable[det],pa_processTable[det].stateBDD,FALSE);
  printf(" (%s: %d st, ",pa_processTable[det].name,i);
  i = Pa_DecodeProcessTR(&pa_processTable[det],pa_processTable[det].d,FALSE);
  printf("%d tr)...",i);
  */

  return det;
}


/**Function****************************************************************
  Synopsis    []
  Description [Remove duplicated paths from WCA]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
VersisWCAMinimization(Est_String name, int par, int n)
{
  int final;
  int i,m,finact;

  /* MINIMIZATION IS WORKING ON A COPY OF WCA */

  n = Pa_CopyProcess(pa_processTable[n].name, "_TMP", NULL, "", "");

  /* MARK FINAL STATES WITH ADDITIONAL TRANSITIONS */
  final = Pa_FOAStateProcess(&pa_processTable[n],"FINAL");
  finact = Pa_FOASortAction(&pa_sortTable[pa_processTable[n].sort],"FINAL");
  for(i=0; i<pa_processTable[n].numStates; i++) {
    if (pa_processTable[n].tableS[i].final) {
      Pa_FOATransition(&pa_processTable[n],i,finact,1,final);
    }
  }

  Pa_EncodeProcess("_TMP");

  /* PRODUCE WEAK EQUIVALENT AUTOMATON */
  /*
  m = VersisWeakMinimization(name,0,n);
  */

  /* PRODUCE TRACE EQUIVALENT AUTOMATON */
  /*
  m = VersisTraceMinimization(1,name,0,n);
  */

  /* PRODUCE STRONG EQUIVALENT AUTOMATON */
  /**/
  m = VersisStrongMinimization(name,0,n);
  /**/

  /* REMOVE ADDITIONAL TRANSITIONS */
  Versis_ChangeForbid(pa_processTable[m].name,"FINAL");

  /* REMOVE TMP COPY OF THE WCA */
  Pa_DeleteProcess(n);

  return Pa_FindProcess(name);
}

/*-----------------------------------------------------------------------*/
/* Definition of static functions                                        */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    [Minimization]
  Description [type: 0 - strong, 1 - weak , 3 - trace minimization]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Est_Boolean
Minimization(Est_String name, Bdd_Edge eqv, int par, int n, int type)
{
  Bdd_Edge D,init,sall;
  Est_String x;
  int s,min,t;
  Bdd_Edge sup,sup1,sup2,new,set;
  Bdd_Edge a;
  int i,j,k;
  Bdd_Edge final;

  if (par == 0) {
    s = pa_processTable[n].sort; /* sort */
    D = pa_processTable[n].d;
    init = pa_processTable[n].tableS[pa_processTable[n].initial].bddR;

    final = bdd_termFalse;
    for(i=0; i<pa_processTable[n].numStates; i++) {
      if (pa_processTable[n].tableS[i].final) {
        final = Bdd_ITE(final,bdd_termTrue,pa_processTable[n].tableS[i].bddR);
      }
    }
    Bdd_Fortify(final);

  } else {
    s = pa_compositionTable[n].sort; /* sort */
    D = pa_compositionTable[n].transitionBDD;
    init = pa_compositionTable[n].initialBDD;
    final = bdd_termFalse;
  }

  if (Bdd_isNull(D)) {
    return -1;
  }

  /* we will need the set of all states */
  sup = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
  sup1 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);
  sall = Bdd_ITE(sup,bdd_termTrue,sup1);
  Bdd_Fortify(sall);

  /* tvorimo ogrodje novega procesa */
  min = Pa_AddNewProcess(name);
  pa_processTable[min].sort = s;
  pa_processTable[min].numStates= 0;
  pa_processTable[min].initial = 0;

  /* tvorimo zacetno stanje */

  x = strdup("s");
  t = Pa_FOANextStateProcess(&pa_processTable[min],x);
  free(x);

  /* bddR in each state temporaly represents the set of original states */
  sup = Bdd_RelOpSimple(init,"R2P",TRUE);
  sup = Bdd_RelOp(eqv,sup,"#AND Ex xP",TRUE);
  Bdd_Fortify(sup);

  pa_processTable[min].tableS[t].bddR = sup;

  set = Bdd_ITE(sup,bdd_termFalse,sall);

  /*
  printf("\nIzracun stanj...\n");
  */

  /* v vsakem koraku poiscemo eno novo stanje minimalnega procesa */
  while (!Bdd_isEqv(set,bdd_termFalse)) {

    if (par == 0) {
      new = Pa_ExtractProcState(&pa_processTable[n],set);
    } else {
      new = Pa_ExtractCompState(&pa_compositionTable[n],set);
    }

    x = strdup("s");
    t = Pa_FOANextStateProcess(&pa_processTable[min],x);
    free(x);

    /* bddR in each state temporaly represents the set of original states */
    sup = Bdd_RelOpSimple(new,"R2P",TRUE);
    sup = Bdd_RelOp(eqv,sup,"#AND Ex xP",TRUE);
    Bdd_Fortify(sup);
    pa_processTable[min].tableS[t].bddR = sup;

    set = Bdd_ITE(sup,bdd_termFalse,set);

    /*
    printf("<%d>",t);
    */

  }

  /* dolocimo koncna stanja v minimalnem procesu */
  /* stanje je koncno, ce je VSAJ ENO izmed stanj v ekvivalencnem razredu koncno! */

  for (i=0; i<=t; i++) {
    sup = Bdd_ITE(pa_processTable[min].tableS[i].bddR,final,bdd_termFalse);
    if (!Bdd_isEqv(sup,bdd_termFalse)) {
      pa_processTable[min].tableS[i].final = TRUE;
    }
  }

  /* dolocimo prehode v minimalnem procesu */

  /*
  printf("Izracun prehodov...\n");
  */

  for (i=0; i<=t; i++) {
    sup = pa_processTable[min].tableS[i].bddR;

    for (j=0; j<pa_sortTable[s].numActions; j++) {
      a = pa_sortTable[s].table[j].p;

      /*
      pom = (Est_String) malloc(255);
      sprintf(pom," Stanje: %d, Akcija: %d\n",i,j);
      printf(pom);
      free(pom);
      */

      /* output action */

      sup1 = Bdd_ITE(pa_sortTable[s].a0,a,bdd_termFalse);
      sup1 = Bdd_ITE(sup,sup1,bdd_termFalse);
      sup1 = Bdd_ITE(D,sup1,bdd_termFalse);
      sup1 = Bdd_NewState(sup1);

      for (k=0; k<=t; k++) {
        sup2 = Bdd_ITE(pa_processTable[min].tableS[k].bddR,sup1,bdd_termFalse);
        if (!Bdd_isEqv(sup2,bdd_termFalse)) {
          Pa_FOATransition(&pa_processTable[min], i, j, 1, k);
        }
      }

      /* input action & action TAU */

      sup1 = Bdd_ITE(pa_sortTable[s].a0,bdd_termFalse,a);
      sup1 = Bdd_ITE(sup,sup1,bdd_termFalse);
      sup1 = Bdd_ITE(D,sup1,bdd_termFalse);
      sup1 = Bdd_NewState(sup1);

      for (k=0; k<=t; k++) {
        if ((type!=1) || (j!=0) || (i!=k)) {
          sup2 = Bdd_ITE(pa_processTable[min].tableS[k].bddR,sup1,bdd_termFalse);
          if (!Bdd_isEqv(sup2,bdd_termFalse)) {
            Pa_FOATransition(&pa_processTable[min], i, j, 0, k);
          }
	}
      }

    }
  }

  /* encode process */
  Pa_EncodeProcess(name);
  Bdd_IncCounter();

  return TRUE;
}
