/**CFile*******************************************************************
  PackageName [pa]
  Synopsis    [Package 'pa' is a framework for implementation of
               process algebrae similar to Milner's CCS and Hoare's CSP.]

  FileName    [paOutput.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 paOutput.c provides basic reporting about LTSs.]
  SeeAlso     [pa.h, paInt.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 <unistd.h>
#include "paInt.h"

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

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

static void IZPIS_AKCIJ_SORTA(Pa_Sort *s);

static void IZPIS_SORTA_PROCESA(Pa_Process *p, char type);

static void IZPIS_STANJ_PROCESA(Pa_Process *p, char type);

static void IZPIS_PREHODOV_PROCESA(Pa_Process *p, char type);

static Est_String shortname(Est_String name);

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

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

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

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

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

void
Pa_WriteKnownSorts()
{
  int i;
  Est_String pom;

  printf("The list of sorts:\n");
  for(i=0; i<pa_sorts; i++) {
    pom = (Est_String) malloc(255);
    sprintf(pom,"%4d. sort  %s ",i+1,pa_sortTable[i].name);
    printf("%s",pom);
    if (pa_sortTable[i].encoded)
      printf("(encoded)\n");
    else
      printf("(not encoded)\n");
    free(pom);
  }
  printf("\n");
}

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

void
Pa_WriteSort(Est_String ime)
{
  Est_String pom;
  int s;

  pom = (Est_String) malloc(255);
  sprintf(pom,"Sort: %s\n",ime);
  printf("%s",pom);
  free(pom);

  s = Pa_FindSort(ime);
  if (s != -1) {
    IZPIS_AKCIJ_SORTA(&pa_sortTable[s]);
  } else {
    printf("Sort does not exist!\n");
  }
  printf("\n");
}

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

void
Pa_WriteKnownProcesses()
{
  int i;
  Est_String pom;

  printf("The list of processes:\n");
  for(i=0;i<pa_processes;i++) {
    pom = (Est_String) malloc(255);
    sprintf(pom,"%4d. proces  %s ",i+1,pa_processTable[i].name);
    printf("%s",pom);
    if (pa_processTable[i].encoded)
      printf("(encoded)\n");
    else
      printf("(not encoded)\n");
    free(pom);
  }
  printf("\n");
}

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

void
Pa_WriteProcess(Est_String ime, char type)
{
  Est_String pom;
  int p;

  pom = (Est_String) malloc(255);
  sprintf(pom,"PROCESS %s\n",ime);
  printf("%s",pom);
  free(pom);

  p = Pa_FindProcess(ime);
  if (p != -1) {
    IZPIS_SORTA_PROCESA(&pa_processTable[p],type);
    IZPIS_STANJ_PROCESA(&pa_processTable[p],type);
    IZPIS_PREHODOV_PROCESA(&pa_processTable[p],type);
  } else {
    printf("Process does not exist!\n");
  }
}

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

void
Pa_WriteKnownCompositions()
{
  int i;
  Est_String pom;

  printf("The list of compositions:\n");
  for(i=0;i<pa_compositions;i++) {
    pom = (Est_String) malloc(255);
    sprintf(pom,"%4d. composition  %s\n",i+1,pa_compositionTable[i].name);
    printf("%s",pom);
    free(pom);
  }
  printf("\n");
}

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

void
Pa_WriteProcessCCS(Est_String name, char type)
{
  int i,procnum;
  Pa_Process *p;
  Est_String s;
  int final;

  printf("PROCESS %s\n",name);

  procnum = Pa_FindProcess(name);
  if (procnum != -1) {

    p = &pa_processTable[procnum];

    /* report sort */

    /*
    if (type>0) {
      printf("SORT %s\n",pa_sortTable[p->sort].name);
    }
    */

    /* report initial state */

    if (type>0) {
      printf("INITIAL STATE ");
      if (p->initial == -1) {
        s = strdup("");
      } else {
        s = shortname(p->tableS[p->initial].name);
      }
      printf("%s\n",s);
      free(s);
    }

    /* REPORT NUMBER OF STATES */

    if (type!=1) {
      printf("Number of states: %d\n",Pa_NumberStateProcess(p));
    }

    /* REPORT FINAL STATES */
    final = 0;
    for(i=0; i<p->numStates; i++) {
      if (p->tableS[i].final) final++;
    }

    if (final>0) {

      if (type!=1) {
       printf("Number of final states: %d\n",final);
      }

      if ((type>0) && !(p->numTransitions > 1000)) {
        printf("FINAL STATES ");
        for(i=0; i<p->numStates; i++) {
          if (p->tableS[i].final) {
            printf(" ");
            s = shortname(p->tableS[i].name);
            printf("%s",s);
            free(s);
          }
        }
        printf("\n");
      }
    }

    /* REPORT NUMBER OF TRANSITIONS */

    if (type!=1) {
      printf("Number of transitions: %d\n",p->numTransitions);
    }

    /* REPORT TRANSITIONS */
    if (type == 0) {
      return;
    }

    /**/
    if ((type>1) && (p->numTransitions > 1000)) {
      printf("Transitions will not be printed (limit = 1000 transitions)!\n");
      return;
    }
    /**/

    /*
    if (type>0) {
      printf("TRANSITIONS\n");
    }
    */

    for(i=0; i<p->numTransitions; i++) {

      if (!p->tableS[p->tableT[i].source].ccs) {
        s = shortname(p->tableS[p->tableT[i].source].name);
        p->tableS[p->tableT[i].source].ccs = strdup(s);
        free(s);
        concat(&p->tableS[p->tableT[i].source].ccs," = ");
      } else {
        concat(&p->tableS[p->tableT[i].source].ccs," + ");
      }

      concat(&p->tableS[p->tableT[i].source].ccs,pa_sortTable[p->sort].table[p->tableT[i].action].name);
      if (p->tableT[i].action != 0) {
        if ((p->tableT[i].type) == 0) {
          concat(&p->tableS[p->tableT[i].source].ccs,"?");
        } else {
          concat(&p->tableS[p->tableT[i].source].ccs,"!");
        }
      }
      concat(&p->tableS[p->tableT[i].source].ccs," . ");
      s = shortname(p->tableS[p->tableT[i].dest].name);
      concat(&p->tableS[p->tableT[i].source].ccs,s);
    }

    for(i=0; i<p->numStates; i++) {
      if (p->tableS[i].ccs) {
        printf("%s\n",p->tableS[i].ccs);
        free(p->tableS[i].ccs);
        p->tableS[i].ccs = NULL;
      }
    }

  } else {
    printf("Process does not exist!\n");
  }
}


/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [Parameter "char type" is not used.]
  SeeAlso     []
  ************************************************************************/

void
Pa_WriteProcessFSP(Est_String name, char type)
{
  int i,procnum;
  Pa_Process *p;
  Est_String s,sn;
  Est_Boolean thefirst;

  procnum = Pa_FindProcess(name);
  if (procnum != -1) {

    sn = shortname(name);
    p = &pa_processTable[procnum];

    for(i=0; i<p->numTransitions; i++) {

      if (!p->tableS[p->tableT[i].source].ccs) {
        p->tableS[p->tableT[i].source].ccs = strdup("");
        if (p->tableT[i].source == p->initial) {
          concat(&p->tableS[p->tableT[i].source].ccs,sn);
        }
        s = shortname(p->tableS[p->tableT[i].source].name);
        s[0] = toupper(s[0]);
        concat(&p->tableS[p->tableT[i].source].ccs,s);
        free(s);
        concat(&p->tableS[p->tableT[i].source].ccs," = (");
      } else {
        concat(&p->tableS[p->tableT[i].source].ccs," | ");
      }

      if (p->tableT[i].action != 0) {

        /* INPUT AND OUTPUT ACTIONS */
        concatLower(&p->tableS[p->tableT[i].source].ccs,
                    pa_sortTable[p->sort].table[p->tableT[i].action].name);

        /* ADD MARK */
        /*
        if ((p->tableT[i].type) == 0) {
          concat(&p->tableS[p->tableT[i].source].ccs,"IN");
        } else {
          concat(&p->tableS[p->tableT[i].source].ccs,"OUT");
        }
        */

      } else {

        /* ACTION TAU */
        concat(&p->tableS[p->tableT[i].source].ccs,"tAU");

      }

      concat(&p->tableS[p->tableT[i].source].ccs," -> ");
      if (p->tableT[i].dest == p->initial) {
        concat(&p->tableS[p->tableT[i].source].ccs,sn);
      }
      s = shortname(p->tableS[p->tableT[i].dest].name);
      s[0] = toupper(s[0]);
      concat(&p->tableS[p->tableT[i].source].ccs,s);
      free(s);
    }

    thefirst = TRUE;
    for(i=0; i<p->numStates; i++) {
      if (p->tableS[i].ccs) {
        if (!thefirst) printf("),\n");
        printf("%s",p->tableS[i].ccs);
        free(p->tableS[i].ccs);
        p->tableS[i].ccs = NULL;
        thefirst = FALSE;
      }
    }
    if (!thefirst) {
      printf(").\n");
      s = shortname(p->tableS[p->initial].name);
      s[0] = toupper(s[0]);
      printf("||%s = %s%s\\{tAU}.\n",sn,sn,s);
      free(s);
    }

    free(sn);

  } else {
    printf("Process does not exist!\n");
  }
}

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

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

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

static void
IZPIS_AKCIJ_SORTA(Pa_Sort *s)
{
  Est_String pom;
  int i;

  pom = (Est_String) malloc(255);
  sprintf(pom,"Number of actions: %d\n",s->numActions);
  printf("%s",pom);
  free(pom);

  for(i=0; i<s->numActions; i++) {
    pom = (Est_String) malloc(255);
    sprintf(pom,"%4d. action  %s\n",i+1,s->table[i].name);

    /**/
    fprintf(stderr,"%s",pom);
    /**/

    printf("%s",pom);
    free(pom);
  }
  printf("\n");
}

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

static void
IZPIS_SORTA_PROCESA(Pa_Process *p, char type)
{

  if (type>0) {
    printf("SORT %s\n",pa_sortTable[p->sort].name);
  }
}

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

static void
IZPIS_STANJ_PROCESA(Pa_Process *p, char type)
{
  int comp;
  Pa_Composition *c = NULL;
  int i,j;
  int number;
  int final;
  int deleted;
  Est_String s;

  if (!p->tableS) {
    printf("WARNING: State table is empty.\n");
    return;
  }

  comp = -1;
  if (p->compname) {
    comp = Pa_FindComposition(p->compname);
  }

  number = 0;
  deleted = 0;
  j = 0;
  for(i=0; i<p->numStates; i++) {

    if (strcmp(p->tableS[i].name,"")) {

      if (!Pa_IsGate(p->tableS[i].name)) {
        number++;
      }

      if (type == 3) {
        printf("%4d. ",++j);
        if (Pa_IsGate(p->tableS[i].name)) {
          printf("gate: ");
      	} else {
          printf("state: ");
	      }
        printf("%s",p->tableS[i].name);
        printf("\n");

	      /*
        if (!Bdd_isNull(p->tableS[i].acc)) {
          printf("acc:\n");
          Bdd_WriteFunction1(stdout,p->tableS[i].acc);
        }
	      */

	      /*
        if (!Bdd_isNull(p->tableS[i].minacc)) {
          printf("minacc:\n");
          Bdd_WriteFunction1(stdout,p->tableS[i].minacc);
        }
	      */

        if (comp != -1) {
          if (!Bdd_isNull(p->tableS[i].bddComp)) {
            c = &pa_compositionTable[comp];
            printf("   ");
            Pa_DecodeCompStates(c, p->tableS[i].bddComp , TRUE);
            printf("\n");
          }
        }
      }

    } else {
      deleted++;
    }
  }

  /* REPORT INITIAL STATE */

  if (type>0) {
    printf("INITIAL STATE ");
    s = shortname(p->tableS[p->initial].name);
    printf("%s\n",s);
    free(s);
  }

  /* REPORT NUMBER OF STATES */

  if (type!=1) {
    printf("Number of states: %d\n",number);
  }

  /* REPORT FINAL STATES */
  final = 0;
  for(i=0; i<p->numStates; i++) {
    if (p->tableS[i].final) final++;
  }

  if (final>0) {

    if (type!=1) {
      printf("Number of final states: %d\n",final);
    }

    if ((type>0) && !(p->numTransitions > 1000)) {
      printf("FINAL STATES ");
      for(i=0; i<p->numStates; i++) {
        if (p->tableS[i].final) {
          printf(" ");
          s = shortname(p->tableS[i].name);
          printf("%s",s);
          free(s);
        }
      }
      printf("\n");
    }
  }

  if (type == 3) {
    if (deleted) {
      printf("WARNING: There are %d deleted states.\n",deleted);
    }
  }

  if (type == 3) {
    if (comp != -1) {
      printf("WARNING: The states are composed as in composition %s.\n",p->compname);
    }
  }

}

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

static void
IZPIS_PREHODOV_PROCESA(Pa_Process *p, char type)
{
  int i,N;
  Est_String s;

  if (type != 1) {
    printf("Number of transitions: %d\n",p->numTransitions);
  }

  /* FOR DEBUGGING: COMMENT THIS OUT */
  /**/
  if (type == 0) {
    return;
  }
  /**/

  if (!p->tableT) return;

  if (p->numTransitions > 1000) {
    printf("To many transitions (only 1000 transitions will be printed)!\n");
    N = 1000;
  } else {
    N = p->numTransitions;
  }

  printf("TRANSITIONS\n");

  for(i=0; i<N; i++) {

    /*
    if (p->tableT[i].source == -1) {
      fprintf(stderr,"<<%d>>",p->tableT[i].source);
    } else {
      fprintf(stderr,"%s",p->tableS[p->tableT[i].source].name);
    }
    if (p->tableT[i].action == -1) {
      fprintf(stderr," = <<%d>>",p->tableT[i].action);
    } else {
      fprintf(stderr," = %s",
                pa_sortTable[p->sort].table[p->tableT[i].action].name);
      if (p->tableT[i].action != 0) {
        if ((p->tableT[i].type) == 0) fprintf(stderr,"?"); else fprintf(stderr,"!");
      }
    }
    fprintf(stderr," . ");
    if (p->tableT[i].dest == -1) {
      fprintf(stderr,"<<%d>>",p->tableT[i].dest);
    } else {
      fprintf(stderr,"%s",p->tableS[p->tableT[i].dest].name);
    }
    fprintf(stderr,"\n");
    */

    if (type == 3) {
      /* LONG VERSION */
      printf("%s",p->tableS[p->tableT[i].source].name);
    } else if (type != 0) {
      /* SHORT VERSION */
      s = shortname(p->tableS[p->tableT[i].source].name);
      printf("%s",s);
      free(s);
    }

    if (type != 0) {
      printf(" = %s",
                pa_sortTable[p->sort].table[p->tableT[i].action].name);

      if (p->tableT[i].action != 0) {
        if ((p->tableT[i].type) == 0) printf("?"); else printf("!");
      }
    }

    if (type != 0) {
      printf(" . ");
    }

    if (type == 3) {
      /* LONG VERSION */
      printf("%s",p->tableS[p->tableT[i].dest].name);
    } else if (type != 0) {
      /* SHORT VERSION */
      s = shortname(p->tableS[p->tableT[i].dest].name);
      printf("%s",s);
      free(s);
    }

    if (type != 0) {
      printf("\n");
    }
  }

}

/**Function****************************************************************
  Synopsis    [Function shortname]
  Description []
  SideEffects [This may be different than in other files.]
  SeeAlso     []
  ************************************************************************/

static Est_String
shortname(Est_String name) {
  int i;
  Est_String shortname;

  i = strcspn(name,"<#");
  shortname = (char *) malloc(i+1);
  memcpy(shortname,name,i);
  shortname[i]=0;
  return(shortname);
}

/**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);
}

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

static void
concatLower(char **s1, const char *s2)
{
  int i,n1,n2;

  n1 = strlen(*s1);
  n2 = strlen(s2);
  *s1 = (char*) realloc(*s1,n1+n2+1);
  for (i=0; i<n2; i++) {
    (*s1)[n1+i]=tolower(s2[i]);
  }
  (*s1)[n1+i] = 0;
}
