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

  FileName    [paTcl.c]
  Revision    [$Revision: 77 $]
  Date        [$Date: 2013-04-29 21:10:06 +0200 (pon, 29 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si)]
  Description [The file paTcl.c contains definitions of Tcl commands,
               which can be used for manipulating from Tcl interpreter
               (e.g. tclsh or wish).]
  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 "paInt.h"
#include "paDecls.h"

#include <tcl.h>

extern PaStubs paStubs;
extern CONST char *Gui_InitStubs (Tcl_Interp *interp, char *version, int exact);
extern CONST char *Bdd_InitStubs (Tcl_Interp *interp, char *version, int exact);

/* on tcl 8.3 use #define USECONST */
/* on tcl 8.4 use #define USECONST const*/
/* this is defined in Makefile */

/*-----------------------------------------------------------------------*/
/* Constant declarations                                                 */
/*-----------------------------------------------------------------------*/

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

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

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

static int PaInitPkgCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaExitPkgCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaAboutPkgCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaReadSortCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaReadProcessCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaCopyProcessCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaProcess2CompositionCmd(ClientData clientData,
                          Tcl_Interp *interp, int argc, USECONST char **argv);

static int PaComposition2ProcessCmd(ClientData clientData,
                          Tcl_Interp *interp, int argc, USECONST char **argv);

static int PaListSortsCmd(ClientData clientData,
                          Tcl_Interp *interp, int argc, USECONST char **argv);

static int PaListProcessesCmd(ClientData clientData,
                          Tcl_Interp *interp, int argc, USECONST char **argv);

static int PaListCompositionsCmd(ClientData clientData,
                          Tcl_Interp *interp, int argc, USECONST char **argv);

static int PaWriteSortCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaWriteProcessCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaWriteProcessCCSCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaWriteProcessFSPCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaEncodeSortCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaEncodeProcessCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaDecodeProcessCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaDecodeProcVisibleCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaDecodeCompositionCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaDecodeCompVisibleCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaDecodeInitialStateCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaDecodeComposedStateCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaStateNumberCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaTransitionNumberCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaTransitionVisibleCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaCompStateNumberCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaCompTransitionNumberCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

static int PaCompTransitionVisibleCmd(ClientData clientData,
                          Tcl_Interp *interp, int argc, USECONST char **argv);

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

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

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

#ifdef __cplusplus
extern "C" {
#endif

int
Pa_Init(Tcl_Interp *interp)
{

#ifdef USE_TCL_STUBS
  if (Tcl_InitStubs(interp, "8.1", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

#ifdef USE_GUI_STUBS
  if (Gui_InitStubs(interp, "1.0", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

#ifdef USE_BDD_STUBS
  if (Bdd_InitStubs(interp, "1.0", 0) == NULL) {
    return TCL_ERROR;
  }
#endif

  Tcl_CreateCommand(interp, "pa_initPkg", PaInitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_exitPkg", PaExitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_aboutPkg", PaAboutPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_read_sort", PaReadSortCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_read_process", PaReadProcessCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_copy_process", PaCopyProcessCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_process2composition", PaProcess2CompositionCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_composition2process", PaComposition2ProcessCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_list_sorts", PaListSortsCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_list_processes", PaListProcessesCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_list_compositions", PaListCompositionsCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_write_sort", PaWriteSortCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_write_process", PaWriteProcessCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_write_process_ccs", PaWriteProcessCCSCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_write_process_fsp", PaWriteProcessFSPCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_encode_sort", PaEncodeSortCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_encode_process", PaEncodeProcessCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_decode_process", PaDecodeProcessCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_decode_proc_visible", PaDecodeProcVisibleCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_decode_composition", PaDecodeCompositionCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_decode_comp_visible", PaDecodeCompVisibleCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_decode_initial_state", PaDecodeInitialStateCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_decode_composed_state", PaDecodeComposedStateCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_state_number", PaStateNumberCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_transition_number", PaTransitionNumberCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_transition_visible", PaTransitionVisibleCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_comp_state_number", PaCompStateNumberCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_comp_transition_number",
                     PaCompTransitionNumberCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "pa_comp_transition_visible",
                     PaCompTransitionVisibleCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  return Tcl_PkgProvideEx(interp, "est2ed-pa", "1.0", &paStubs);
}

#ifdef __cplusplus
}
#endif

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

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

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

static int
PaInitPkgCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                  USECONST char **argv)
{
  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  printf("Initialization of Process_Algebra package... ");
  Pa_InitPkg();
  printf("OK");

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaExitPkgCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                   USECONST char **argv)
{
  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  printf("Exit PA package... ");
  Pa_ExitPkg();
  printf("OK");

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaAboutPkgCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                   USECONST char **argv)
{
  if (argc != 1) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  Pa_AboutPkg();

  printf("DEBUG: FALSE = %x, TRUE = %x\n",FALSE,TRUE);
  printf("DEBUG: bdd_termTrue = (%p, %x)\n",bdd_termTrue.p,bdd_termTrue.mark);
  printf("DEBUG: bdd_termFalse = (%p, %x)\n",bdd_termFalse.p,bdd_termFalse.mark);
  printf("DEBUG: bdd_termNull = (%p, %x)\n",bdd_termNull,bdd_termNull.mark);
  printf("\n");

  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaReadSortCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                   USECONST char **argv)
{
  Est_String s1;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  printf("Warning: Command pa_read_sort is depreciated. Please, use pa_read_process!\n");

  printf("Reading file: %s",s1);
  Pa_ParseSortProcess(s1);

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaReadProcessCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String s1;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  printf("Reading file: %s",s1);
  Pa_ParseSortProcess(s1);

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaCopyProcessCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                      USECONST char **argv)
{
  Est_String s1,s2,s3,s4,s5;
  int ok;
  Est_String newsort;

  if ((argc != 3) && (argc != 6)) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);

  if (argc == 3) {
    s3 = strdup("NULL");
    s4 = strdup("");
    s5 = strdup("");
  } else {
    s3 = strdup(argv[3]);
    s4 = strdup(argv[4]);
    s5 = strdup(argv[5]);
  }

  if (!strcmp(s3,"NULL")) {
    newsort = NULL;
  } else {
    newsort = s3;
  }

  printf("Copying process:");
  printf("  %s --> %s... ",s1,s2);

  ok = Pa_CopyProcess(s1,s2,newsort,s4,s5);

  if (ok != -1) {
    printf("OK");
  }

  free(s1);
  free(s2);
  free(s3);
  free(s4);
  free(s5);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaProcess2CompositionCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                              USECONST char **argv)
{
  Est_String s1;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (Pa_FindProcess(s1) == -1) {
    printf("  Process %s does not exist. ",s1);
    Tcl_SetResult(interp, "", TCL_STATIC);
    return TCL_OK;
  }

  printf("Creating composition from process:");
  printf(" %s... ",s1);

  Pa_Process2Composition(s1);

  printf("OK");

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaComposition2ProcessCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                              USECONST char **argv)
{
  Est_String s1,s2;
  int full;

  if ((argc != 2) && (argc != 3)) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (Pa_FindComposition(s1) == -1) {
    printf("  Composition %s does not exist. ",s1);
    Tcl_SetResult(interp, "", TCL_STATIC);
    return TCL_OK;
  }

  if (argc == 2) {
    full = 1;                        /* default is full transformation */
  } else {
    s2 = strdup(argv[2]);
    sscanf(s2,"%d",&full);
    free(s2);
  }

  printf("Creating process from composition:");
  printf(" %s... ",s1);

  if (!full) {
    Pa_Composition2Process(s1,FALSE);
  } else {
    Pa_Composition2Process(s1,TRUE);
  }

  printf("OK");

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}


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

static int
PaListSortsCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  int i;
  Est_String list,newlist;

  if (pa_sorts == 0) {
    list = strdup("");
  } else {
    list = strdup("");

    for(i=0;i<pa_sorts;i++) {
      if (!pa_sortTable[i].deleted) {
        newlist = (Est_String) malloc(strlen(list)+strlen(pa_sortTable[i].name)+2);
        sprintf(newlist,"%s %s",list,pa_sortTable[i].name);
        free(list);
        list=newlist;
      }
    }

  }

  Tcl_SetResult(interp, list, TCL_VOLATILE);
  free(list);

  return TCL_OK;
}


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

static int
PaListProcessesCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  int i;
  Est_String list,newlist;

  if (pa_processes == 0) {
    list = strdup("");
  } else {
    list = strdup("");

    for(i=0;i<pa_processes;i++) {
      if (!pa_processTable[i].deleted) {
        newlist = (Est_String) malloc(strlen(list)+strlen(pa_processTable[i].name)+2);
        sprintf(newlist,"%s %s",list,pa_processTable[i].name);
        free(list);
        list=newlist;
      }
    }

  }

  Tcl_SetResult(interp, list, TCL_VOLATILE);
  free(list);

  return TCL_OK;
}


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

static int
PaListCompositionsCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  int i;
  Est_String list,newlist;

  if (pa_compositions == 0) {
    list = strdup("");
  } else {
    list = strdup("");

    for(i=0;i<pa_compositions;i++) {
      newlist = (Est_String) malloc(strlen(list)+strlen(pa_compositionTable[i].name)+2);
      sprintf(newlist,"%s %s",list,pa_compositionTable[i].name);
      free(list);
      list=newlist;
    }

  }

  Tcl_SetResult(interp, list, TCL_VOLATILE);
  free(list);

  return TCL_OK;
}

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

static int
PaWriteSortCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                    USECONST char **argv)
{
  Est_String s1;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (!strcmp(s1,"?")) {
    Pa_WriteKnownSorts();
  } else {
    Pa_WriteSort(s1);
  }

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaWriteProcessCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1,s2;
  char type;

  if ((argc != 2) && (argc != 3)) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (argc == 2) {
    type = 1;
  } else {
    s2 = strdup(argv[2]);
    type = atoi(s2);
    free(s2);
  }

  if (!strcmp(s1,"?")) {
    Pa_WriteKnownProcesses();
  } else {
    Pa_WriteProcess(s1,type);
  }

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}


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

static int
PaWriteProcessCCSCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1,s2;
  char type;

  if ((argc != 2) && (argc != 3)) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (argc == 2) {
    type = 1;
  } else {
    s2 = strdup(argv[2]);
    type = atoi(s2);
    free(s2);
  }

  if (!strcmp(s1,"?")) {
    Pa_WriteKnownProcesses();
  } else {
    Pa_WriteProcessCCS(s1,type);
  }

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaWriteProcessFSPCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1,s2;
  char type;

  if ((argc != 2) && (argc != 3)) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (argc == 2) {
    type = 1;
  } else {
    s2 = strdup(argv[2]);
    type = atoi(s2);
    free(s2);
  }

  if (!strcmp(s1,"?")) {
    Pa_WriteKnownProcesses();
  } else {
    Pa_WriteProcessFSP(s1,type);
  }

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaEncodeSortCmd(ClientData clientData, Tcl_Interp *interp,
                int argc, USECONST char **argv)
{
  Est_String s1;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  printf("Warning: Command pa_encode_sort is depreciated. Please, remove it!\n");

  if (!strcmp(s1,"?")) {
    Pa_WriteKnownSorts();
  } else {
    /*
    printf("Encoding sort:\n");
    printf("  %s... ",s1);
    */
    Pa_EncodeSort(s1);
    /*
    printf("OK");
    */
  }

  free(s1);

  /*
  printf("\n");
  */
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaEncodeProcessCmd(ClientData clientData, Tcl_Interp *interp,
                   int argc, USECONST char **argv)
{
  Est_String s1;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (!strcmp(s1,"?")) {
    Pa_WriteKnownProcesses();
  } else {

    /*
    printf("Encoding processes: ");
    printf("%s... ",s1);
    */

    Pa_EncodeMultiProcesses(s1);

    /*
    printf("OK");
    */
  }

  free(s1);

  /*
  printf("\n");
  */
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaDecodeProcessCmd(ClientData clientData, Tcl_Interp *interp,
                   int argc, USECONST char **argv)
{
  Est_String s1;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (!strcmp(s1,"?")) {
    Pa_WriteKnownProcesses();
  } else {
    printf("Decoding process:\n");
    Pa_DecodeProcess(s1, TRUE);
  }

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaDecodeProcVisibleCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1;
  int i;
  Bdd_Edge tau;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (!strcmp(s1,"?")) {
    Pa_WriteKnownProcesses();
  } else {
    i = Pa_FindProcess(s1);
    if (i != -1) {
      if (pa_processTable[i].encoded) {
        printf("Decoding visible part of process:\n");
        tau = pa_sortTable[pa_processTable[i].sort].table[0].p;
        Pa_DecodeProcessTR(
            &pa_processTable[i],
            Bdd_ITE(tau,bdd_termFalse,pa_processTable[i].d),
            TRUE);
      } else {
        printf("  Process is not encoded.");
      }
    } else {
      printf("  Process does not exist.");
    }
  }

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaDecodeCompositionCmd(ClientData clientData, Tcl_Interp *interp,
                   int argc, USECONST char **argv)
{
  Est_String s1;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (!strcmp(s1,"?")) {
    Pa_WriteKnownCompositions();
  } else {
    printf("Decoding composition:\n");
    Pa_DecodeComposition(s1, TRUE);
  }

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaDecodeCompVisibleCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1;
  int i;
  Bdd_Edge tau;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  if (!strcmp(s1,"?")) {
    Pa_WriteKnownCompositions();
  } else {
    i = Pa_FindComposition(s1);
    if (i != -1) {

      if (pa_compositionTable[i].onthefly) {

        printf("ERROR: Cannot decode on-the-fly composition\n");

      } else {

        printf("Decoding visible part of composition:\n");
        tau = pa_sortTable[pa_compositionTable[i].sort].table[0].p;
        Pa_DecodeCompTR(
            &pa_compositionTable[i],
            Bdd_ITE(tau,bdd_termFalse,pa_compositionTable[i].transitionBDD),
            TRUE);

      }
    } else {
      printf("  Composition does not exist.");
    }
  }

  free(s1);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaDecodeInitialStateCmd(ClientData clientData, Tcl_Interp *interp,
                         int argc, USECONST char **argv)
{
  Est_String s1,s2;
  int type,procnum,compnum;
  Pa_Process *p;
  Pa_Composition *c;
  Bdd_Edge F;

  if (argc != 3) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);

  sscanf(s1,"%d",&type);

  /* PROCESS */

  if (type == 0) {

    procnum = Pa_FindProcess(s2);

    if (procnum == -1) {
      printf("  Process %s does not exist. ",s2);
    } else {

      p = &pa_processTable[procnum];
      printf("Initial state: %s\n",p->tableS[p->initial].name);

      if (p->compname) {
        printf("Composed of: ");
        compnum = Pa_FindComposition(p->compname);
        if (compnum != -1) {
          c = &pa_compositionTable[compnum];
          F = p->tableS[p->initial].bddComp;
          Pa_DecodeCompStates(c,F,TRUE);
        } else {
          printf("/\n");
	}
      }
    }
  }

  if (type == 1) {

    compnum = Pa_FindComposition(s2);

    if (compnum == -1) {
      printf("  Composition %s does not exist. ",s2);
    } else {

      c = &pa_compositionTable[compnum];

      if (c->onthefly) {

        printf("ERROR: Cannot decode on-the-fly composition\n");

      } else {

        printf("Initial state: ");
        Pa_DecodeCompStates(c,c->initialBDD,TRUE);

      }
    }
  }

  free(s1);
  free(s2);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaDecodeComposedStateCmd(ClientData clientData, Tcl_Interp *interp,
                         int argc, USECONST char **argv)
{
  Est_String s1,s2;
  int procnum,compnum,state;
  Pa_Process *p;
  Pa_Composition *c;
  Bdd_Edge F;
  Est_String statename;

  if (argc != 3) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);

  procnum = Pa_FindProcess(s1);

  if (procnum == -1) {
    printf("  Process %s does not exist. ",s1);
  } else {

    p = &pa_processTable[procnum];

    if (!p->compname) {
      printf("  Process %s does not have composed states. ",s1);
    } else {

      compnum = Pa_FindComposition(p->compname);

      if (compnum == -1) {
        printf("  Composition %s does not exist. ",s1);
      } else {

        c = &pa_compositionTable[compnum];
        statename = NULL;

        if (c->onthefly) {

          /* Cannot decode on-the-fly composition */

        } else {

          if (strchr(s2,'<')) {
            statename = strdup(s2);
          } else {
            statename = (Est_String) malloc(127);
            sprintf(statename,"%s<%s>",s2,s1);
          }

          state = Pa_FindStateProcess(p,statename);

          if (state == -1) {
            printf("  State %s does not exist in process %s. ",statename,s1);
          } else {

            F = p->tableS[state].bddComp;

            if (Bdd_isNull(F)) {
              printf("ERROR: Decoding not possible. ");
            } else {
              Pa_DecodeCompStates(c,F,TRUE);
	    }
	  }
	}

        if (statename) free(statename);
      }
    }
  }

  free(s1);
  free(s2);

  printf("\n");
  Tcl_SetResult(interp, "", TCL_STATIC);
  return TCL_OK;
}

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

static int
PaStateNumberCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1;
  int i;
  int j=-1;
  Est_String sup;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  i = Pa_FindProcess(s1);
  if (i != -1) {
    j = Pa_NumberStateProcess(&pa_processTable[i]);
  } else {
    /* process does not exist */
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%d",j);

  free(s1);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
PaTransitionNumberCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1,s2;
  int i;
  int j=-1;
  int actnum;
  Est_String sup;
  Bdd_Edge D,act;

  if ((argc != 2) && (argc != 3)) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  i = Pa_FindProcess(s1);
  if (i != -1) {
    if (pa_processTable[i].encoded) {
      D = pa_processTable[i].d;
      if (argc == 3) {
        s2 = strdup(argv[2]);
        actnum = Pa_FindSortAction(&pa_sortTable[pa_processTable[i].sort],s2);
        free(s2);
        if (actnum != -1) {
          act = pa_sortTable[pa_processTable[i].sort].table[actnum].p;
          D = Bdd_ITE(D,act,bdd_termFalse);
	} else {
          printf("  Action ignored because it does not exist. ");
	}
      }
      j = Pa_DecodeProcessTR(&pa_processTable[i],D,FALSE);
    } else {
      /* process is not encoded */
    }
  } else {
    /* process does not exist */
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%d",j);

  free(s1);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
PaTransitionVisibleCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1;
  int i;
  int j=-1;
  Est_String sup;
  Bdd_Edge tau;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  i = Pa_FindProcess(s1);
  if (i != -1) {
    if (pa_processTable[i].encoded) {
      tau = pa_sortTable[pa_processTable[i].sort].table[0].p;
      j = Pa_DecodeProcessTR(
            &pa_processTable[i],
            Bdd_ITE(tau,bdd_termFalse,pa_processTable[i].d),
            FALSE);
    } else {
      /* process is not encoded */
    }
  } else {
    /* process does not exist */
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%d",j);

  free(s1);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
PaCompStateNumberCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1;
  int i;
  int j=-1;
  Est_String sup;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  i = Pa_FindComposition(s1);
  if (i != -1) {
    j = Pa_DecodeCompStates(
          &pa_compositionTable[i],
          pa_compositionTable[i].stateBDD,
          FALSE);
  } else {
    /* composition does not exist */
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%d",j);

  free(s1);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
PaCompTransitionNumberCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1,s2;
  int i;
  int j=-1;
  int actnum;
  Est_String sup;
  Bdd_Edge D,act;

  if ((argc != 2) && (argc != 3)) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  i = Pa_FindComposition(s1);
  if (i != -1) {
    D = pa_compositionTable[i].transitionBDD;
    if (argc == 3) {
      s2 = strdup(argv[2]);
      actnum = Pa_FindSortAction(&pa_sortTable[pa_compositionTable[i].sort],s2);
      free(s2);
      if (actnum != -1) {
        act = pa_sortTable[pa_compositionTable[i].sort].table[actnum].p;
        D = Bdd_ITE(D,act,bdd_termFalse);
      } else {
        printf("  Action ignored because it does not exist. ");
      }
    }
    j = Pa_DecodeCompTR(&pa_compositionTable[i],D,FALSE);
  } else {
    /* composition does not exist */
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%d",j);

  free(s1);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}

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

static int
PaCompTransitionVisibleCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1;
  int i;
  int j=-1;
  Est_String sup;
  Bdd_Edge tau;

  if (argc != 2) {
    interp->result = "wrong # args";
    return TCL_ERROR;
  }

  s1 = strdup(argv[1]);

  i = Pa_FindComposition(s1);
  if (i != -1) {
    tau = pa_sortTable[pa_compositionTable[i].sort].table[0].p;
    j = Pa_DecodeCompTR(
          &pa_compositionTable[i],
          Bdd_ITE(tau,bdd_termFalse,pa_compositionTable[i].transitionBDD),
          FALSE);
  } else {
    /* composition does not exist */
  }

  sup = (Est_String) malloc(15);
  sprintf(sup,"%d",j);

  free(s1);

  Tcl_SetResult(interp, sup, TCL_VOLATILE);
  free(sup);

  return TCL_OK;
}
