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

  FileName    [versisMain.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si),
               Mirjam Sepesy Maucec (mirjam.sepesy@uni-mb.si),
               Tatjana Kapus (kapus@uni-mb.si)]
  Description [File versisMain.c contains main functions.]
  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"

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

int versis_status = 0;                     /* initialization status */

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

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

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

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

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

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

#ifndef TCLOUT
   void Versis_Init(void) {}
#endif

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

void
Versis_InitPkg()
{
  if (versis_status == 1) {
    printf("\nVersis package is already initialized. ");
    return;
  } else {
    versis_status = 1;
  }

  return;
}

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

void
Versis_ExitPkg()
{
  if (versis_status == 0) {
    printf("\nVersis package is not initialized. ");
    return;
  } else {
    versis_status = 0;
  }

}

/**Function****************************************************************
  Synopsis    [Function Versis_AboutPkg]
  Description [Versis_AboutPkg reports release of Versis package.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Versis_AboutPkg()
{
  printf("EST ");
  printf(EDITION);
  printf(", version ");
  printf(VERSION);
  printf(", ");
  printf("Versis package");
  printf("\n");
}

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

void
Versis_ChangeRename(Est_String process, Est_String name1, Est_String name2)
{
  int procnum;
  int act1,act2;
  Bdd_Edge subst,sup1,sup2,newtr;
  Pa_Process *p;
  int i;
  Est_String tmpname,tmpsort;

  procnum = Pa_FindProcess(process);
  if (procnum == -1) {
    printf("Process does not exists.\n");
    return;
  }

  p = &pa_processTable[procnum];

  act1 =Pa_FindSortAction(&pa_sortTable[p->sort],name1);

  if (act1 == -1) {
    printf("Action %s does not exists in the sort.\n",name1);
    return;
  }

  if (act1 == 0) {
    printf("Cannot rename action TAU.\n");
    return;
  }

  act2 =Pa_FindSortAction(&pa_sortTable[p->sort],name2);
  if (act2 == -1) {
    if (p->encoded) {
      tmpname = strdup(process);
      concat(&tmpname,"_CR");
      tmpsort = strdup(pa_sortTable[p->sort].name);
      concat(&tmpsort,"_CR");
      Pa_AddNewSort(tmpsort);
      Pa_CopyProcess(process,tmpname,tmpsort,name1,name2);
      Pa_RenameProcess(tmpname,process);
      Pa_EncodeProcess(process);
      free(tmpname);
      free(tmpsort);
      return;
    } else {
      act2 = Pa_FOASortAction(&pa_sortTable[p->sort],name2);
    }
  }

  if (p->tableS) {
    for (i=0; i<p->numTransitions; i++) {
      if (p->tableT[i].action == act1) {
        p->tableT[i].action = act2;
        if (act2 == 0) {
          p->tableT[i].type = 0;
	}
      }
    }
  }

  if (p->encoded) {

    newtr = Bdd_ITE(pa_sortTable[p->sort].table[act1].p,bdd_termFalse,p->d);

    sup1 = Bdd_ITE(pa_sortTable[p->sort].a0,
                     pa_sortTable[p->sort].table[act1].p,bdd_termFalse);
    sup2 = Bdd_ITE(pa_sortTable[p->sort].a0,
                     pa_sortTable[p->sort].table[act2].p,bdd_termFalse);
    subst = Bdd_RelOp(p->d,sup1,"#AND Ex xA",TRUE);
    sup2  = Bdd_ITE(subst,sup2,bdd_termFalse);
    newtr = Bdd_ITE(newtr,bdd_termTrue,sup2);

    sup1 = Bdd_ITE(pa_sortTable[p->sort].a0,bdd_termFalse,
                     pa_sortTable[p->sort].table[act1].p);
    sup2 = Bdd_ITE(pa_sortTable[p->sort].a0,bdd_termFalse,
                     pa_sortTable[p->sort].table[act2].p);
    subst = Bdd_RelOp(p->d,sup1,"#AND Ex xA",TRUE);
    sup2  = Bdd_ITE(subst,sup2,bdd_termFalse);
    newtr = Bdd_ITE(newtr,bdd_termTrue,sup2);

    p->d = newtr;

    /* ****************** */
    /* ALTERNATIVE METHOD */
    /* ********************************************************************

    Bdd_Edge substBA;
    substBA = bdd_termFalse;
    for (i=0; i<pa_sortTable[p->sort].numActions; i++) {

      if (i>0) {
        sup1 = Bdd_ITE(pa_sortTable[p->sort].a0,
                       pa_sortTable[p->sort].table[i].p,bdd_termFalse);
        sup2 = sup1;
        sup1 = Bdd_RelOpSimple(sup1,"A2B",TRUE);

        if (i == act1) {
          sup2 = Bdd_ITE(pa_sortTable[p->sort].a0,
                         pa_sortTable[p->sort].table[act2].p,bdd_termFalse);
        }
        sup2 = Bdd_ITE(sup1,sup2,bdd_termFalse);
        substBA = Bdd_ITE(substBA,bdd_termTrue,sup2);
        Bdd_IncCounter();
        Bdd_Fresh(substBA);
      }

      sup1 = Bdd_ITE(pa_sortTable[p->sort].a0,bdd_termFalse,
                     pa_sortTable[p->sort].table[i].p);
      sup2 = sup1;
      sup1 = Bdd_RelOpSimple(sup1,"A2B",TRUE);

      if (i == act1) {
        sup2 = Bdd_ITE(pa_sortTable[p->sort].a0,bdd_termFalse,
                       pa_sortTable[p->sort].table[act2].p);
      }
      sup2 = Bdd_ITE(sup1,sup2,bdd_termFalse);
      substBA = Bdd_ITE(substBA,bdd_termTrue,sup2);
      Bdd_IncCounter();
      Bdd_Fresh(substBA);
    }

    newtr = Bdd_RelOpSimple(p->d,"A2B",TRUE);
    p->d = Bdd_RelOp(newtr,substBA,"#AND Ex xB",TRUE);

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

  }
}

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

void
Versis_ChangeHide(Est_String process, Est_String name1)
{
  int procnum;
  int act1;
  Pa_Process *p;
  int i;

  procnum = Pa_FindProcess(process);
  if (procnum == -1) {
    printf("Process does not exists.\n");
    return;
  }

  p = &pa_processTable[procnum];

  act1 =Pa_FindSortAction(&pa_sortTable[p->sort],name1);

  if (act1 == -1) {
    printf("Action does not exists.\n");
    return;
  }

  if (act1 == 0) {
    printf("Cannot hide action TAU.\n");
    return;
  }

  if (p->tableS) {
    for (i=0; i<p->numTransitions; i++) {
      if (p->tableT[i].action == act1) {
        p->tableT[i].action = 0;
        p->tableT[i].type = 0; /* THIS IS TYPE OF ACTION TAU */
      }
    }
  }

  if (p->encoded) {
    p->encoded = 0;
    Pa_EncodeProcess(process);
  }
}

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

void
Versis_ChangeForbid(Est_String process, Est_String name1)
{
  int procnum;
  int act1;
  Pa_Process *p;
  Pa_Transition *table;
  int *states;
  int i,num;
  int encoded;

  procnum = Pa_FindProcess(process);
  if (procnum == -1) {
    printf("Process does not exists.\n");
    return;
  }

  p = &pa_processTable[procnum];

  act1 =Pa_FindSortAction(&pa_sortTable[p->sort],name1);

  if (act1 == -1) {
    printf("Action does not exists.\n");
    return;
  }

  if (p->compname) free(p->compname);
  p->compname = NULL;
  p->numVar = 0;
  p->d = bdd_termNull;
  p->stab = bdd_termNull;

  encoded = p->encoded;
  p->encoded = 0;

  num = p->numTransitions;
  p->numTransitions = 0;

  table = p->tableT;
  p->tableT = NULL;

  states = (int *) malloc(p->numStates * sizeof(int));
  for(i=0; i<p->numStates; i++) {
    states[i]=0;
  }
  states[p->initial]=1;

  if (table) {
    for (i=0; i<num; i++) {
      if (table[i].action != act1) {
        Pa_FOATransition(p,table[i].source,table[i].action,table[i].type,table[i].dest);
        states[table[i].source] = 1;
        states[table[i].dest] = 1;
      }
    }
  }

  for(i=0; i<p->numStates; i++) {
    if (!states[i]) Pa_DeleteStateProcess(p,i);
  }

  for(i=0; i<p->numStates; i++) {
    if (p->tableS[i].ccs) {
      free(p->tableS[i].ccs);
      p->tableS[i].ccs = NULL;
    }
  }

  free(table);
  free(states);

  if (encoded) {
    Pa_EncodeProcess(process);
  }
}

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

Bdd_Edge
Versis_CheckDeadlock(Bdd_Edge D)
{
  Bdd_Edge sup1,sup2,sd;

  if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termFalse;

  sup1 = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);

  sd = Bdd_ITE(sup1,bdd_termFalse,sup2);     /* the set of all deadlocked states */

  return sd;
}

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

Bdd_Edge
Versis_CheckDivergence(Bdd_Edge D, Bdd_Edge tau)
{
  Bdd_Edge Div,last,new,sup;

  last = bdd_termFalse;
  Div = bdd_termTrue;

  while (!Bdd_isEqv(Div,last)) {
    last = Div;
    new = Bdd_ITE(D,Div,bdd_termFalse);
    sup = Bdd_RelOpSimple(Div,"R2S",TRUE);
    new = Bdd_RelOp(new,sup,"#AND Ex xS",TRUE);
    new = Bdd_RelOp(new,tau,"#AND Ex xA",TRUE);
    Div = new;
  }

  return Div;
}

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

/**Function****************************************************************
  Synopsis    [VersisTrCl]
  Description [Transitive closure on state variables RS. Not reflexive!]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
VersisTrCl(Bdd_Edge f)
{
  Bdd_Edge f1,last,new,trcl;

  f1 = Bdd_RelOpSimple(f,"R2P",TRUE);
  last = bdd_termTrue;
  trcl = f;

  while (!Bdd_isEqv(trcl,last)) {

    Bdd_IncCounter();
    Bdd_Fresh(f1);
    Bdd_Fresh(trcl);

    last = trcl;
    new = Bdd_RelOpSimple(trcl,"S2P",TRUE);
    new = Bdd_RelOp(new,f1,"#AND Ex xP",TRUE);
    new = Bdd_ITE(new,bdd_termTrue,trcl);
    trcl = new;
  }

  return(trcl);
}

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

Bdd_Edge
VersisComposeActions(Pa_Composition *c)
{
  Pa_Sort *s;
  Bdd_Edge sup1,sup2;
  int i;

  s = &pa_sortTable[c->sort];
  sup1 = bdd_termFalse;

  for (i=0; i<c->numActions; i++) {
    sup2 = Bdd_ITE(s->a0,s->table[c->tableA[i]].p,bdd_termFalse);
    sup1 = Bdd_ITE(sup1,bdd_termTrue,sup2);
    sup2 = Bdd_ITE(s->a0,bdd_termFalse,s->table[c->tableA[i]].p);
    sup1 = Bdd_ITE(sup1,bdd_termTrue,sup2);
  }

  return sup1;
}

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

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

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