/**CFile*******************************************************************
  PackageName [mc]
  Synopsis    [Package 'mc' provides a symbolic ACTLW model checker]

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

#include <tcl.h>

extern McStubs mcStubs;
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);
extern CONST char *Versis_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 McInitPkgCmd(ClientData clientData, Tcl_Interp *interp,
                        int argc, USECONST char **argv);

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

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

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

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

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

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

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

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

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

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


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

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

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

#ifdef __cplusplus
extern "C" {
#endif

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

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

  Tcl_LinkVar(interp, "mc_simple", (char *) &MC_SIMPLE,
                     TCL_LINK_INT || TCL_LINK_READ_ONLY);

  Tcl_LinkVar(interp, "mc_trace", (char *) &MC_TRACE,
                     TCL_LINK_INT || TCL_LINK_READ_ONLY);

  Tcl_LinkVar(interp, "mc_xtrace", (char *) &MC_XTRACE,
                     TCL_LINK_INT || TCL_LINK_READ_ONLY);

  Tcl_LinkVar(interp, "mc_explain", (char *) &MC_EXPLAIN,
                     TCL_LINK_INT || TCL_LINK_READ_ONLY);

  Tcl_LinkVar(interp, "mc_tracepath", (char *) &MC_TRACEPATH,
                     TCL_LINK_INT || TCL_LINK_READ_ONLY);

  Tcl_LinkVar(interp, "mc_diagnostic", (char *) &MC_DIAGNOSTIC,
                     TCL_LINK_INT || TCL_LINK_READ_ONLY);

  Tcl_LinkVar(interp, "mc_automaton", (char *) &MC_AUTOMATON,
                     TCL_LINK_INT || TCL_LINK_READ_ONLY);

  Tcl_LinkVar(interp, "mc_minimize", (char *) &MC_MINIMIZE,
                     TCL_LINK_INT || TCL_LINK_READ_ONLY);

  Tcl_LinkVar(interp, "mc_tree", (char *) &MC_TREE,
                     TCL_LINK_INT || TCL_LINK_READ_ONLY);

  Tcl_LinkVar(interp, "mc_progress", (char *) &MC_PROGRESS,
                     TCL_LINK_INT || TCL_LINK_READ_ONLY);

  Tcl_CreateCommand(interp, "mc_initPkg", McInitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "mc_exitPkg", McExitPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "mc_aboutPkg", McAboutPkgCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "mc_list_formulae", McListFormulaeCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "mc_write_actl", McWriteACTLCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "mc_check_actl", McCheckACTLCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "mc_check_actl_string", McCheckACTLStringCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "mc_check_actl_file", McCheckACTLFileCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "mc_generate_wca", McGenerateWCACmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "mc_read_actl", McReadACTLCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  Tcl_CreateCommand(interp, "mc_read_actl_file", McReadACTLFileCmd,
                     (ClientData) NULL, (Tcl_CmdDeleteProc *) NULL);

  return Tcl_PkgProvideEx(interp, "est2ed-mc", "1.0", &mcStubs);
}

#ifdef __cplusplus
}
#endif

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

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

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

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

  printf("Initialization of Model checking package... ");
  Mc_InitPkg();
  printf("OK");

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

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

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

  printf("Exit Model checking package... ");
  Mc_ExitPkg();
  printf("OK");

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

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

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

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

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

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

    for(i=0;i<mc_formulae;i++) {
      word = (Est_String) malloc(255);
      sprintf(word,"{%s == %s} ",mc_formulaTable[i].name,mc_formulaTable[i].formula);
      list = (Est_String) realloc(list,strlen(list)+strlen(word)+1);
      strcat(list,word);
      free(word);
    }
  }

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

  return TCL_OK;
}

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

static int
McWriteACTLCmd(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,"?")) {
    Mc_WriteKnownFormulae();
  } else {
    Mc_WriteFormula(s1,type);
  }

  free(s1);

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

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

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

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

  s1 = strdup(argv[1]);
  sscanf(s1,"%d",&par);
  free(s1);

  if ((par != 0) && (par != 1)) {
    interp->result = "first arg is wrong";
    return TCL_ERROR;
  }

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

  if (argc == 5) {
    s4 = strdup(argv[4]);
    if (!strcmp(s4,"simple")) parserSettings = MC_SIMPLE;
    else if (!strcmp(s4,"diagnostic")) parserSettings = MC_DIAGNOSTIC;
    else if (!strcmp(s4,"automaton")) parserSettings = MC_AUTOMATON | MC_MINIMIZE;
    else parserSettings = atoi(s4);
    free(s4);
  } else {
    parserSettings = 0;
  }

  printf("ACTL/ACTLW model checking ");
  if (par == 0) printf("on process ");
  if (par == 1) printf("on composition ");
  printf(s2);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Mc_CheckACTL_Thr(par,s2,s3,parserSettings);
#else
  Mc_CheckACTL(par,s2,s3,parserSettings);
#endif
  Tcl_Eval(interp,"enable_input");

  free(s2);
  free(s3);

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

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

static int
McCheckACTLStringCmd(ClientData clientData, Tcl_Interp *interp, int argc,
                     USECONST char **argv)
{
  Est_String s1,s2,s3,s4;
  Est_String tmp;
  int par;
  int parserSettings;
  int i,len;

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

  s1 = strdup(argv[1]);
  sscanf(s1,"%d",&par);
  free(s1);

  if ((par != 0) && (par != 1)) {
    interp->result = "first arg is wrong";
    return TCL_ERROR;
  }

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

  len = strlen(s3);
  while (s3[len-1] == ' ') len--;
  if (s3[len-1] != ';') {
    tmp = s3;
    s3 = (Est_String) malloc(len+1);
    for (i=0; i<len; i++) s3[i]=tmp[i];
    s3[len] = ';';
    s3[len+1] = 0;
    free(tmp);
  }

  if (argc == 5) {
    s4 = strdup(argv[4]);
    if (!strcmp(s4,"simple")) parserSettings = MC_SIMPLE;
    else if (!strcmp(s4,"diagnostic")) parserSettings = MC_DIAGNOSTIC;
    else if (!strcmp(s4,"automaton")) parserSettings = MC_AUTOMATON | MC_MINIMIZE;
    else parserSettings = atoi(s4);
    free(s4);
  } else {
    parserSettings = 0;
  }

  printf("ACTL/ACTLW model checking ");
  if (par == 0) printf("on process ");
  if (par == 1) printf("on composition ");
  printf(s2);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Mc_CheckACTLString_Thr(par,s2,s3,parserSettings);
#else
  Mc_CheckACTLString(par,s2,s3,parserSettings);
#endif
  Tcl_Eval(interp,"enable_input");

  free(s2);
  free(s3);

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

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

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

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

  s1 = strdup(argv[1]);
  sscanf(s1,"%d",&par);
  free(s1);

  if ((par != 0) && (par != 1)) {
    interp->result = "first arg is wrong";
    return TCL_ERROR;
  }

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

  if (argc == 5) {
    s4 = strdup(argv[4]);
    if (!strcmp(s4,"simple")) parserSettings = MC_SIMPLE;
    else if (!strcmp(s4,"diagnostic")) parserSettings = MC_DIAGNOSTIC;
    else if (!strcmp(s4,"automaton")) parserSettings = MC_AUTOMATON | MC_MINIMIZE;
    else parserSettings = atoi(s4);
    free(s4);
  } else {
    parserSettings = 0;
  }

  printf("ACTL/ACTLW model checking ");
  if (par == 0) printf("on process ");
  if (par == 1) printf("on composition ");
  printf(s2);
  printf(" using file ");
  printf(s3);
  printf("\n");

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Mc_CheckACTLFile_Thr(par,s2,s3,parserSettings);
#else
  Mc_CheckACTLFile(par,s2,s3,parserSettings);
#endif
  Tcl_Eval(interp,"enable_input");

  free(s2);
  free(s3);

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

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

static int
McGenerateWCACmd(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("Generating WCA %s for formula %s on process %s\n\n",s3,s2,s1);

  Tcl_Eval(interp,"disable_input");
#ifdef USETHREADS
  Mc_GenerateWCA(s1,s2,s3);
#else
  Mc_GenerateWCA(s1,s2,s3);
#endif
  Tcl_Eval(interp,"enable_input");

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

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

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

static int
McReadACTLCmd(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]);

  Mc_ReadACTL(s1,s2);

  free(s1);
  free(s2);

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

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

static int
McReadACTLFileCmd(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]);

  Mc_ReadACTLFile(s1);

  free(s1);

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