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

  FileName    [versisTcl.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 [File versisTcl.c contains definitions of Tcl commands,
               which can be used for manipulating from Tcl interpreter
               (e.g. tclsh or wish).]
  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"
#include "versisDecls.h"

#include <tcl.h>

extern VersisStubs versisStubs;
extern CONST char *Gui_InitStubs (Tcl_Interp *interp, char *version, int exact);
extern CONST char *Bdd_InitStubs (Tcl_Interp *interp, char *version, int exact);
extern CONST char *Pa_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 VersisInitPkgCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

#ifdef __cplusplus
extern "C" {
#endif

int
Versis_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

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

  Tcl_CreateCommand(interp, "versis_initPkg", VersisInitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_exitPkg", VersisExitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_aboutPkg", VersisAboutPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_compose", VersisComposeCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_compose_step", VersisComposeStepCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_strong_equivalence",
                     VersisStrongEquivalenceCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_weak_equivalence",
                     VersisWeakEquivalenceCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_testing_equivalence",
                     VersisTestingEquivalenceCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_trace_equivalence",
                     VersisTraceEquivalenceCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_strong_minimization",
                     VersisStrongMinimizationCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_weak_minimization",
                     VersisWeakMinimizationCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_trace_minimization",
                     VersisTraceMinimizationCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_trace_strong_minimization",
                     VersisTraceStrongMinimizationCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_wca_minimization",
                     VersisWCAMinimizationCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_change_rename", VersisChangeRenameCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_change_hide", VersisChangeHideCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_change_forbid", VersisChangeForbidCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_check_deadlock", VersisCheckDeadlockCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "versis_check_divergence",
                    VersisCheckDivergenceCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  return Tcl_PkgProvideEx(interp, "est2ed-versis", "1.0", &versisStubs);
}

#ifdef __cplusplus
}
#endif

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

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

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

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

  printf("Initialization of Versis package... ");
  Versis_InitPkg();
  printf("OK");

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

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

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

  printf("Exit Versis package... ");
  Versis_ExitPkg();
  printf("OK");

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

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

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

  Versis_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 VersisComposeCmd.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
VersisComposeCmd(ClientData clientData, Tcl_Interp *interp,
                      int argc, USECONST char **argv)
{
  Est_String s1,s2,s3,s4,s5;
  int type;
  Est_Boolean onthefly;

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

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);
  s4 = strdup(argv[4]);

  if (argc == 5) {
    onthefly = FALSE;
  } else {
    s5 = strdup(argv[5]);
    onthefly = (atoi(s5) != 0);
    free(s5);
  }

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

  if (onthefly) {
    printf("On-the-fly parallel composition (%d):",type);
  } else {
    printf("Parallel composition (%d):",type);
  }
  printf(" %s...",s2);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Versis_Compose_Thr(s2,type,s3,s4,onthefly);
#else
  Versis_Compose(s2,type,s3,s4,onthefly);
#endif
  Tcl_Eval(interp,"enable_input");

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

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

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

static int
VersisComposeStepCmd(ClientData clientData, Tcl_Interp *interp,
                      int argc, USECONST char **argv)
{
  Est_String s1,s2;
  int n,N;
  int loop=0;

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

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

  n = Pa_FindComposition(s1);
  N = atoi(s2);

  Tcl_Eval(interp,"disable_input");

  if (N > 0) {

    printf("Calculating %d step",N);
    if (N == 1) printf(" "); else printf("s ");
    printf("of parallel composition: %s...",s1);

    loop = Versis_ComposeStep(n,N);

  } else {

    printf("Initialization of parallel composition: %s...",s1);
    Versis_ComposeInit(s1);

  }

  Tcl_Eval(interp,"enable_input");

  free(s1);
  free(s2);

  if (loop == N) {
    printf(" OK\n");
  } else {
    printf(" OK (terminated after %d steps)\n",loop);
  }

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

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

static int
VersisStrongEquivalenceCmd(ClientData clientData, Tcl_Interp *interp,
                      int argc, USECONST char **argv)
{
  Est_String s1,s2,s3,s4;
  int par1, par2;
  Est_Boolean r;

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

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);
  s4 = strdup(argv[4]);

  printf("Strong observational equivalence checking ");

  sscanf(s1,"%d",&par1);
  sscanf(s3,"%d",&par2);

  printf("between %s and %s... ",s2,s4);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  r = Versis_Equivalence_Thr(0,par1,s2,par2,s4);
#else
  r = Versis_Equivalence(0,par1,s2,par2,s4);
#endif
  Tcl_Eval(interp,"enable_input");

  if (r == TRUE) printf("OK");
  if (r == FALSE) printf("NOT EQUIVALENT");

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

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

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

static int
VersisWeakEquivalenceCmd(ClientData clientData, Tcl_Interp *interp,
                      int argc, USECONST char **argv)
{
  Est_String s1,s2,s3,s4;
  int par1, par2;
  Est_Boolean r;

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

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);
  s4 = strdup(argv[4]);

  printf("Weak observational equivalence checking ");

  sscanf(s1,"%d",&par1);
  sscanf(s3,"%d",&par2);

  printf("between %s and %s... ",s2,s4);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  r = Versis_Equivalence_Thr(1,par1,s2,par2,s4);
#else
  r = Versis_Equivalence(1,par1,s2,par2,s4);
#endif
  Tcl_Eval(interp,"enable_input");

  if (r == TRUE) printf("OK");
  if (r == FALSE) printf("NOT EQUIVALENT");

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

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

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

static int
VersisTestingEquivalenceCmd(ClientData clientData, Tcl_Interp *interp,
                      int argc, USECONST char **argv)
{
  Est_String s1,s2,s3,s4;
  int par1, par2;
  Est_Boolean r;

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

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);
  s4 = strdup(argv[4]);

  printf("Testing equivalence checking ");

  sscanf(s1,"%d",&par1);
  sscanf(s3,"%d",&par2);

  printf("between %s and %s... ",s2,s4);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  r = Versis_Equivalence_Thr(2,par1,s2,par2,s4);
#else
  r = Versis_Equivalence(2,par1,s2,par2,s4);
#endif
  Tcl_Eval(interp,"enable_input");

  if (r == TRUE) printf("OK");
  if (r == FALSE) printf("NOT EQUIVALENT");

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

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

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

static int
VersisTraceEquivalenceCmd(ClientData clientData, Tcl_Interp *interp,
                          int argc, USECONST char **argv)
{
  Est_String s1,s2,s3,s4;
  int par1, par2;
  Est_Boolean r;

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

  s1 = strdup(argv[1]);
  s2 = strdup(argv[2]);
  s3 = strdup(argv[3]);
  s4 = strdup(argv[4]);

  printf("Trace equivalence checking ");

  sscanf(s1,"%d",&par1);
  sscanf(s3,"%d",&par2);

  printf("between %s and %s... ",s2,s4);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  r = Versis_Equivalence_Thr(3,par1,s2,par2,s4);
#else
  r = Versis_Equivalence(3,par1,s2,par2,s4);
#endif
  Tcl_Eval(interp,"enable_input");

  if (r == TRUE) printf("OK");
  if (r == FALSE) printf("NOT EQUIVALENT");

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

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

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

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

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

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

  printf("Strong minimization of %s... ",s2);

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

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Versis_Minimization_Thr(0,par,s2);
#else
  Versis_Minimization(0,par,s2);
#endif
  Tcl_Eval(interp,"enable_input");

  printf("OK");

  free(s1);
  free(s2);

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

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

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

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

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

  printf("Weak minimization of %s... ",s2);

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

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Versis_Minimization_Thr(1,par,s2);
#else
  Versis_Minimization(1,par,s2);
#endif
  Tcl_Eval(interp,"enable_input");

  printf("OK");

  free(s1);
  free(s2);

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

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

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

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

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

  printf("Trace minimization of %s... ",s2);

  sscanf(argv[1],"%d",&par);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Versis_Minimization_Thr(3,par,s2);
#else
  Versis_Minimization(3,par,s2);
#endif
  Tcl_Eval(interp,"enable_input");

  printf("OK");

  free(s1);
  free(s2);

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

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

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

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

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

  printf("Strong trace minimization of %s... ",s2);

  sscanf(argv[1],"%d",&par);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Versis_Minimization_Thr(4,par,s2);
#else
  Versis_Minimization(4,par,s2);
#endif
  Tcl_Eval(interp,"enable_input");

  printf("OK");

  free(s1);
  free(s2);

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

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

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

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

  s1 = strdup(argv[2]);

  printf("WCA minimization of %s... ",s1);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Versis_Minimization_Thr(5,0,s1);
#else
  Versis_Minimization(5,0,s1);
#endif
  Tcl_Eval(interp,"enable_input");

  printf("OK");

  free(s1);

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

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

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

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

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

  printf("Rename actions in proces %s: ",s1);

  printf("%s --> ",s2);
  Versis_ChangeRename(s1,s2,s3);
  printf("%s\n",s3);

  free(s1);
  free(s2);
  free(s3);

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

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

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

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

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

  printf("Hide actions in proces %s: ",s1);

  printf("%s --> ",s2);
  Versis_ChangeHide(s1,s2);
  printf("TAU\n");

  free(s1);
  free(s2);

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

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

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

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

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

  printf("Forbid actiona in proces %s: ",s1);

  Versis_ChangeForbid(s1,s2);
  printf("%s\n",s2);

  free(s1);
  free(s2);

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

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

static int
VersisCheckDeadlockCmd(ClientData clientData, Tcl_Interp *interp,
                       int argc, USECONST char **argv)
{
  Est_String s1;
  Bdd_Edge sd;
  int n;

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

  s1 = strdup(argv[1]);
  n = Pa_FindProcess(s1);

  if (n != -1) {

    printf("Deadlock states in process %s:\n",s1);

    sd = bdd_termFalse;
    sd = Versis_CheckDeadlock(pa_processTable[n].d);
    Pa_DecodeProcessStates(&pa_processTable[n],sd,TRUE);

  }

  free(s1);

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

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

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

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

  s1 = strdup(argv[1]);

  n = Pa_FindProcess(s1);

  if (n != -1) {

    tau = pa_sortTable[pa_processTable[n].sort].table[0].p;

    printf("Divergent states in process %s:\n",s1);

    sd = bdd_termFalse;
    sd = Versis_CheckDivergence(pa_processTable[n].d,tau);
    Pa_DecodeProcessStates(&pa_processTable[n],sd,TRUE);

  }

  free(s1);

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