/* *****************************************************************

Parameters:
-l or -logic
-m or -model

Default is model checking only.
-p or -path = linear witness/counterexample
-a or -automaton = witness/counterexample automaton
-e or -explain = explain linear w/c and w/c automaton

****************************************************************** */

#include <bdd.h>
#include <pa.h>
#include <versis.h>
#include <mc.h>
#include <strucval.h>
#include <ccs.h>

#define PROGNAME "wca"

void hello() {
  printf("=======================================================================\n");
  printf("   W i t n e s s   a n d   C o u n t e r e x a m p l e   S e r v e r   \n");
  printf("        Witness and Counterexample Automata Generator for ACTL         \n");
  printf("                      (from EST project)\n");
  printf("     try 'wca -help' to get some help on the usage and parameteres     \n");
  printf("=======================================================================\n");
  printf("   Minimization ()\n");
}

int main(int argc, char **argv)
{
  int i;
  int mctype;
  Est_Boolean help,path,automaton,explain;
  Est_String ccsname,actlname,sysname;
  int p;

  mctype = MC_SIMPLE;
  ccsname = NULL;
  actlname = NULL;
  sysname = strdup("S");

  if (argc == 0) {
    help = TRUE;
  } else {
    help = FALSE;
  }

  path = FALSE;
  automaton = FALSE;
  explain = FALSE;

  i = 1;
  while (i<argc) {

    if (!strcmp(argv[i],"-help")) {
      help = TRUE;
    }

    if (!strcmp(argv[i],"-model") || !strcmp(argv[i],"-m")) {
      ccsname = strdup(argv[++i]);
    }

    if (!strcmp(argv[i],"-logic") || !strcmp(argv[i],"-l")) {
      actlname = strdup(argv[++i]);
    }

    if (!strcmp(argv[i],"-path") || !strcmp(argv[i],"-p")) {
      path = TRUE;
      mctype =  mctype | MC_DIAGNOSTIC | MC_TRACEPATH;
    }

    if (!strcmp(argv[i],"-automaton") || !strcmp(argv[i],"-a")) {
      automaton = TRUE;
      mctype =  mctype | MC_AUTOMATON | MC_MINIMIZE;
    }

    if (!strcmp(argv[i],"-explain") || !strcmp(argv[i],"-e")) {
      explain = TRUE;
      mctype =  mctype | MC_EXPLAIN;
    }

    if (!strcmp(argv[i],"-system") || !strcmp(argv[i],"-s")) {
      free(sysname);
      sysname = strdup(argv[++i]);
    }

    i++;
  }

  hello();

  if (help) {
    printf("Usage:\n");
    printf("wca [-path] [-automaton] [-explain] -model ccsname -logic actlname\n");
    printf("    [-system systemname]\n");
    printf("Parameters:\n");
    printf("  -path               generate a linear witness / linear counterexample\n");
    printf("  -automaton          generate a witness / counterexample automaton\n");
    printf("  -explain            trace the algorithm\n");
    printf("  -model ccsname      the file with CCS model description\n");
    printf("  -logic actlname     the file with actl formulae\n");
    printf("  -system systemname  the name of the system (default: S)\n");
    return 1;
  }

  if (!ccsname) {
    printf("\nERROR: The file with CCS model description must be specified.\n");
    printf("HELP: Use: -model ccsname -logic actlname \n\n");
    return 1;
  }

  if (!actlname) {
    printf("\nERROR: The file with actl formulae must be specified.\n");
    printf("HELP: Use: -model ccsname -logic actlname \n\n");
    return 1;
  }

  /* *********************************************************************** */
  /* *********************************************************************** */

  Bdd_InitPkg();
  Pa_InitPkg();
  Versis_InitPkg();
  Mc_InitPkg();
  Strucval_InitPkg();
  Ccs_InitPkg();
 
  /* *********************************************************************** */
  /* *********************************************************************** */

  printf("\nLoading...");
  Ccs_ParseCCS(ccsname,FALSE); /* FALSE means not silent */

  p = Pa_FindProcess(sysname);
  if (p == -1) {
    printf("\nProcess %s does not exist.\n",sysname);
  } else {

    printf("\n");
    printf("-----------------------------------------------------------------------\n");
    printf("Report on model %s\n",sysname);
    printf("-----------------------------------------------------------------------\n\n");

    if (explain) {
      Pa_WriteProcessCCS(sysname,1);
    } else {
      Pa_WriteProcess(sysname,0);
    }

    /* *********************************************************************** */
    printf("-----------------------------------------------------------------------\n");
    printf("ACTL model checking on model %s\n",sysname);
    printf("-----------------------------------------------------------------------\n\n");
    /* *********************************************************************** */

    Mc_CheckACTLFile(0,sysname,actlname,mctype);
  }

  free(sysname);
  if (actlname) free(actlname);
  if (ccsname) free(ccsname);

  /* *********************************************************************** */
  /* *********************************************************************** */

  Ccs_ExitPkg();
  Strucval_ExitPkg();
  Mc_ExitPkg();
  Versis_ExitPkg();
  Pa_ExitPkg();
  Bdd_ExitPkg();

  return(0);
}
