/**CFile*******************************************************************
  PackageName [strucval]
  Synopsis    [Structure-driven validation of hardware and software systems]

  FileName    [strucvalMain.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si)]
  Description [File strucvalMain.c contains main functions.]
  SeeAlso     [strucval.h, strucvalInt.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 "strucvalInt.h"

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

int strucval_status = 0;                        /* initialization status */

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

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

static int wordNumber(Est_String s);

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

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

/**Function****************************************************************
  Synopsis    [Function Strucval_Init.]
  Description [Creates tcl commands.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

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

/**Function****************************************************************
  Synopsis    [Function Strucval_InitPkg.]
  Description [Initializes the package.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Strucval_InitPkg()
{
  if (strucval_status == 1) {
    printf("\nStrucval package is already initialized. ");
    return;
  } else {
    strucval_status = 1;
  }

}

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

void
Strucval_ExitPkg()
{
  if (strucval_status == 0) {
    printf("\nStrucval package is not initialized. ");
    return;
  } else {
    strucval_status = 0;
  }

}

/**Function****************************************************************
  Synopsis    [Function Strucval_AboutPkg]
  Description [Strucval_AboutPkg reports release of Strucval package.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

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

/**Function****************************************************************
  Synopsis    [Strucval_SyncProduct]
  Description [Strucval_SyncProduct("PRODUCT","LTS","WCA","x").
               The result is a process.
               Partialy implemented by Marina Bagic (marina.bagic@fer.hr)]
  SideEffects ["x" is a set of restricted actions]
  SeeAlso     []
  ************************************************************************/

void
Strucval_SyncProduct(Est_String name, Est_String lts, Est_String wca,
                     Est_String actions)
{
  int i,k,finalWCA;
  int numP,numA,numcomp,token;
  int sync;
  Est_String sup,sup_next,token1;
  Pa_Composition *c;
  Pa_Sort *s;
  Pa_Process *p;

  Bdd_Edge actionsBDD;
  Bdd_Edge s_new,s_acc;
  Bdd_Edge sup1,sup2;
  Bdd_Edge new1,new2,s1,s2,s3,s1_next,s2_next,s3_next;
  Bdd_Edge tr1,tr2,tau;
  Bdd_Edge finalBddWCA;

  /* THIS PART IS FOR DEBUGGING */
  /*
  static int iteration=0;
  printf("Synchronous product between LTS %s and WCA %s\n",lts,wca);
  printf("Creating automaton %s... ",name);
  */

  numP = 2;
  numA = wordNumber(actions);

  /* CREATE EMPTY COMPOSITION c WITH NUMBER numcomp */
  /* TYPE OF COMPOSITION IS -1 */

  i = pa_compositions;
  numcomp = Pa_AddNewComposition(name,-1,2,numA);
  if (pa_compositions == i) {
    printf("(composition overwritten) ");
  }
  c = &pa_compositionTable[numcomp];

  /* ADD INFORMATION ABOUT PROCESSES INTO c */

  i = Pa_FindProcess(lts);

  if (i == -1) {
    Pa_RemoveComposition(numcomp);
    printf("\nLTS %s does not exist.\n",lts);
    return;
  }
  if (!pa_processTable[i].encoded) {
    Pa_EncodeProcess(pa_processTable[i].name);
  }
  c->tableP[0] = i;                     /* number of first process */
  c->sort = pa_processTable[i].sort;

  i = Pa_FindProcess(wca);

  if (i == -1) {
    Pa_RemoveComposition(numcomp);
    printf("\nWCA %s does not exist.\n",wca);
    return;
  }
  if (!pa_processTable[i].encoded) {
    Pa_EncodeProcess(pa_processTable[i].name);
  }
  c->tableP[1] = i;
  if (c->sort != pa_processTable[i].sort) {
    Pa_RemoveComposition(numcomp);
    printf("\nLTS and WCA have different sorts!\n");
    return;
  }

  /* ADD INFORMATION ABOUT ACTIONS INTO COMPOSITION c */

  sup = (Est_String) strdup(actions);

  token = strcspn(sup," ");
  token1 = (Est_String) malloc(token+1);
  strncpy(token1,sup,token);            /* name of first action */
  token1[token] = '\0';

  i = Pa_FindSortAction(&pa_sortTable[c->sort],token1);
  free(token1);

  if (i == -1) {
    Pa_RemoveComposition(numcomp);
    printf(" Action %%%d does not exist.\n",1);
    return;
  }
  c->tableA[0] = i;  /* number of first action */

  k = 1;
  while (k < numA) {
    while (sup[token] == ' ') token = token + 1;
    sup_next = (Est_String) strdup(&sup[token]);
    free(sup);
    sup = sup_next;

    token = strcspn(sup," ");
    token1 = (Est_String) malloc(token+1);
    strncpy(token1,sup,token);           /* name of next action */
    token1[token] = '\0';

    i = Pa_FindSortAction(&pa_sortTable[c->sort],token1);
    free(token1);

    if (i == -1) {
      Pa_RemoveComposition(numcomp);
      printf(" Action %%%d does not exist.\n",k+1);
      return;
    }
    c->tableA[k++] = i;      /* sequence number of first action */
  }
  free(sup);

  /* CALCULATE actionsBDD */

  s = &pa_sortTable[c->sort];
  tau = s->table[0].p;

  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);
  }
  actionsBDD = sup1;
  Bdd_Fortify(actionsBDD);
  Bdd_IncCounter();

  /* THIS PART IS FOR DEBUGGING */
  /*
  printf("\nActions in actionsBDD:\n");
  Pa_DecodeSortActions(&pa_sortTable[c->sort],actionsBDD,TRUE);
  printf("\n");
  */

  /* CALCULATE INITIAL STATE OF THE COMPOSITION */

  sup1 = bdd_termTrue;
  for(i=0; i<numP; i++) {
    p = &pa_processTable[c->tableP[i]];

    /*
    printf("\nBDD for initial state of process number %d:\n",i);
    Bdd_WriteFunction(p->tableS[p->initial].bddR);
    */

    sup1 = Bdd_ITE(sup1,p->tableS[p->initial].bddR,bdd_termFalse);
  }
  c->initialBDD = sup1;

  /* THIS PART IS FOR DEBUGGING */
  /*
  printf("\nInitial state of the composition:\n");
  Pa_DecodeCompStates(c,c->initialBDD,TRUE);
  printf("\n");
  */

  /* s_new (RRR) CONTAINS NEW STATES FOUND IN PREVIOUSLY STEP OF CALCULATION */
  /*             BEFORE LOOP, s_new = INITIAL STATE OF THE COMPOSITION       */
  /*                                                                         */
  /* s_acc (RRR) WILL CONTAIN ALL REACHED STATES                             */

  s_new = c->initialBDD;
  s_acc = s_new;
  s1 = bdd_termFalse;

  /* SET OF WCA'S FINAL STATES*/

  finalWCA=0;
  finalBddWCA = bdd_termFalse;

  for(i=0; i < pa_processTable[c->tableP[1]].numStates; i++){
	if (pa_processTable[c->tableP[1]].tableS[i].final){
		finalWCA++;
		finalBddWCA = Bdd_ITE(finalBddWCA,bdd_termTrue,pa_processTable[c->tableP[1]].tableS[i].bddR);
	}
  }

  /* THIS PART IS FOR DEBUGGING */
  /*
  printf("\nSet of final states in WCA:\n");
  Pa_DecodeProcessStates(&pa_processTable[c->tableP[1]],finalBddWCA,TRUE);
  printf("\n");
  */

  /* LOOP UNTIL NO NEW STATE IS REACHED */

  tr1 = bdd_termFalse;
  tr2 = bdd_termFalse;
  do {

    /* THIS PART IS FOR DEBUGGING */
    /*
    printf("\n*****************************\n");
    printf("STARTING ITERATION %d",++iteration);
    printf("\n*****************************\n");
    */

    /* PART ONE */
    /* CALCULATE NEW STATES, WHICH ARE REACHED WITHOUT COMMUNICATION */
    /* BETWEEN PROCESSES AND STORE THEM IN new1 (RRR) */
    /* TRANSITIONS GO TO tr1 (RRRASSS) */

    new1 = bdd_termFalse;

    /* COMPUTE ALL TRANSITIONS IN PROCESSES lts AND wca WHICH ARE ALLOWED */
    /* WITHOUT COMMUNICATION AND STORE THEM IN s1 (RAS) */

    s1 = Bdd_ITE(actionsBDD,bdd_termFalse,pa_processTable[c->tableP[0]].d);
    s2 = Bdd_ITE(actionsBDD,bdd_termFalse,pa_processTable[c->tableP[1]].d);

    /* UPDATE s1 AND s2 */
    /* THEY SHOULD CONTAIN ONLY TRANSITIONS STARTING FROM s_new (RRR) */
    /* s1 AND s2 BECAME (RRRAS) */

    s1 = Bdd_ITE(s1,s_new,bdd_termFalse);
    s2 = Bdd_ITE(s2,s_new,bdd_termFalse);

    /* s1 SHOULD CONTAIN ONLY TRANSITIONS NOT STARTING IN A FINAL STATE */
    s1 = Bdd_ITE(s1,Bdd_NOT(finalBddWCA),bdd_termFalse);

    /* COMPUTE TRANSITIONS (RRRASSS) */
    tr1 = Bdd_ITE(tr1,bdd_termTrue,Bdd_ITE(s1,pa_processTable[c->tableP[1]].stab,bdd_termFalse));
    tr1 = Bdd_ITE(tr1,bdd_termTrue,Bdd_ITE(s2,pa_processTable[c->tableP[0]].stab,bdd_termFalse));

    /* COMPUTE STATES IN c REACHED WITH TRANSITIONS FROM */
    /* s1 AND s2, RESPECTIVELY, AND STORE THEM IN s1_next (RRR) AND s2_next (RRR)*/
    /* s1_next AND s2_next ARE COMPLETE, THUS ADDING stab IS NOT NEEDED */

    s1_next = Bdd_NewState1(s1,pa_processTable[c->tableP[0]].name);
    s2_next = Bdd_NewState1(s2,pa_processTable[c->tableP[1]].name);

    /* ADD STATES FROM s1_next AND s2_next TO new1 (RRR) */

    new1 = Bdd_ITE(new1,bdd_termTrue,s1_next);
    new1 = Bdd_ITE(new1,bdd_termTrue,s2_next);

    /* THIS PART IS FOR DEBUGGING */
    /*
    printf("\nBDD for new1:\n");
    Bdd_WriteFunction(new1);
    Pa_DecodeCompStates(c,new1,TRUE);
    printf("\n");
    */

    /* PART TWO */
    /* CALCULATE NEW STATES, WHICH ARE REACHED WITH COMMUNICATION */
    /* BETWEEN PROCESSES AND STORE THEM IN new2 (RRR) */
    /* TRANSITIONS GO TO tr2 (RRRASSS) */

    new2 = bdd_termFalse;

    /* COMPUTE TRANSITIONS WITHOUT a0 */
    /* s1 (RAS) = IN PROCESS lts WITH OUTPUT ACTIONS */
    /* s2 (RAS) = IN PROCESS wca WITH INPUT ACTIONS */

    s1 = Bdd_Restrict(pa_processTable[c->tableP[0]].d,
                      Bdd_GetVariable(pa_sortTable[c->sort].a0), TRUE);

    s2 = Bdd_Restrict(pa_processTable[c->tableP[1]].d,
                      Bdd_GetVariable(pa_sortTable[c->sort].a0), FALSE);

    /* COMPOSE s1 (RAS) AND s2 (RAS) TOGETHER AND CREATE s3 (RRRSSS) */

    s3 = Bdd_RelOp(s1,s2,"#AND Ex xA",TRUE);

    /* COMPUTE TRANSITIONS WITHOUT a0 */
    /* s1 (RAS) = IN PROCESS lts WITH INPUT ACTIONS  */
    /* s2 (RAS) = IN PROCESS wca WITH OUTPUT ACTIONS */

    s1 = Bdd_Restrict(pa_processTable[c->tableP[0]].d,
                      Bdd_GetVariable(pa_sortTable[c->sort].a0), FALSE);

    s2 = Bdd_Restrict(pa_processTable[c->tableP[1]].d,
                      Bdd_GetVariable(pa_sortTable[c->sort].a0), TRUE);

    /* COMPOSE s1 (RAS) AND s2 (RAS) TOGETHER AND ADD TO s3 (RRRSSS) */

    s3 =  Bdd_ITE(s3,bdd_termTrue,Bdd_RelOp(s1,s2,"#AND Ex xA",TRUE));

    /* UPDATE s3 */
    /* IT SHOULD CONTAIN ONLY TRANSITIONS STARTING FROM s_new (RRR) */

    s3 = Bdd_ITE(s3,s_new,bdd_termFalse);

    /* ADD TRANSITIONS TO tr2 */

    tr2 = Bdd_ITE(tr2,bdd_termTrue,s3);

    /* COMPUTE STATES IN c REACHED WITH TRANSITIONS FROM */
    /* s3 AND STORE THEM IN s3_next (RRR) */
    /* s3_next IS COMPLETE, THUS ADDING stab IS NOT NEEDED */

    s3_next = Bdd_NewState2(s3,
                            pa_processTable[c->tableP[0]].name,
                            pa_processTable[c->tableP[1]].name);

    /* ADD STATES FROM s3_next TO new2 (RRR) */

    new2 = Bdd_ITE(new2,bdd_termTrue,s3_next);

    /* THIS PART IS FOR DEBUGGING */
    /*
    printf("\nBDD for new2:\n");
    Pa_DecodeCompStates(c,new2,TRUE);
    Bdd_WriteFunction(new2);
    printf("\n");
    */

    /* UPDATE s_new (RRR) */
    s_new = Bdd_ITE(new1,bdd_termTrue,new2);
    s_new = Bdd_ITE(s_acc,bdd_termFalse,s_new);

    /* UPDATE s_acc (RRR) */
    s_acc = Bdd_ITE(s_acc,bdd_termTrue,s_new);

  } while(!(Bdd_isEqv(s_new,bdd_termFalse)));

  /* s_acc ARE ALL STATES IN COMPOSITION c */
  c->stateBDD = s_acc;

  /* CREATE COMPLETE TRANSITION RELATION FOR c */

  tr2 = Bdd_ITE(tau,tr2,bdd_termFalse); /* tr2 = 'tau' * tr2 */
  c->transitionBDD = Bdd_ITE(tr1,bdd_termTrue,tr2);

  /* THIS PART IS FOR DEBUGGING */
  /*
  printf("\nCREATED COMPOSITION\n");
  Pa_DecodeComposition(name,TRUE);
  printf("\n");
  */

  /* MINIMIZATION */

  StrucvalReduceStates(c,finalBddWCA);
  sync = Pa_Composition2Process(name,TRUE);

  /* THE RESULT IS A PROCESS, BUT COMPOSITION IS NOT REMOVED */

  /* MARK FINAL STATES */

  for(i=0; i < pa_processTable[sync].numStates; i++){
    sup1 = Bdd_ITE(pa_processTable[sync].tableS[i].bddComp,finalBddWCA,bdd_termFalse);
    if (!Bdd_isEqv(sup1,bdd_termFalse)) {
      pa_processTable[sync].tableS[i].final = TRUE;
    }
  }

  /*
  printf("OK\n\n");
  Pa_WriteProcessCCS(name,0);
  */
}

/**Function****************************************************************
  Synopsis    [StrucvalReduceStates]
  Description [Reduces states of the composition starting from
	       bottom to to top]
  SideEffects [tableP[0]=LTS, tableP[1]=WCA]
  SeeAlso     []
  ************************************************************************/

void
StrucvalReduceStates(Pa_Composition *c, Bdd_Edge finalBddWCA)
{
  Bdd_Edge reduceSynPStates;
  Bdd_Edge delta_acc,new;

  reduceSynPStates = bdd_termFalse;

  /* REDUCE STATES OF THE SYNCHRONOUS PRODUCT (RRR): all states of SynProd x final WCA states */
  new = Bdd_ITE(finalBddWCA,c->stateBDD,bdd_termFalse);

  while (!Bdd_isEqv(new,bdd_termFalse))  {

    /* ACCUMULATE REDUCE STATES */
    reduceSynPStates = Bdd_ITE(reduceSynPStates,bdd_termTrue,new);

    /* RENAME REDUCE STATES FROM (RRR) TO (SSS) */
    new = Bdd_RelOpSimple(new,"R2S",TRUE);

    /* CALCULATE TRANSITIONS WHICH LEAD TO REDUCE STATES */
    delta_acc = Bdd_ITE(new,c->transitionBDD,bdd_termFalse);

    /* REMOVE (AAA) AND (SSS) FROM TRANSITION RELATION x NOT reduceSynPStates (EXCLUDE REPEATED STATES) */
    new = Bdd_ITE(Bdd_RelOpSimple(delta_acc,"Ex xA xS",TRUE),
                  Bdd_NOT(reduceSynPStates),
                  bdd_termFalse);

  }

  c->stateBDD = reduceSynPStates;
  c->transitionBDD = Bdd_ITE(c->transitionBDD,reduceSynPStates,bdd_termFalse);
  c->transitionBDD = Bdd_ITE(c->transitionBDD,Bdd_RelOpSimple(reduceSynPStates,"R2S",TRUE),bdd_termFalse);

  Bdd_Fortify(c->stateBDD);
  Bdd_Fortify(c->transitionBDD);
}

/**Function****************************************************************
  Synopsis    [static int wordNumber(Est_String s)]
  Description [translates string s to number]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
wordNumber(Est_String s)
{
  int num;
  int token;
  Est_String sup,sup_next;

  num = 0;
  sup = strdup(s);

  token = strspn(sup," ");
  while (strspn(sup," ") < strlen(sup)) {
    sup_next = (Est_String) strdup(&sup[token]);
    free(sup);
    sup = sup_next;

    num++;
    token = strcspn(sup," ");
    sup_next = (Est_String) strdup(&sup[token]);
    free(sup);
    sup = sup_next;

    token = strspn(sup," ");
  }

  free(sup);
  return num;
}

