/* Copyright (c) 2001 by the Institute for Computer Science,               */
/* Alberts-Ludwigs-University of Freiburg, Germany.                        */
/* All Rights Reserved.  This software is for educational purposes only.   */
/* Permission is given to distribute this code provided that this intro-   */
/* ductory message is not removed and no monies are exchanged.             */
/* No guarantee is expressed or implied by the distribution of this code.  */
/* Software written by Alberto Lluch Lafuente and Stefan Edelkamp.         */
/* References:                                                             */
/* - Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue,              */
/*   Directed Explicit Model Checking with HSF-SPIN, to appear in:         */
/*   Proc. 8th International SPIN Workshop on Model Checking Software,     */
/*   Springer LNCS 2057, Toronto, May 2001                                 */
/* - Stefan Edelkamp, Alberto Lluch Lafuente and Stefan Leue,              */
/*   Protocol Verification with Heuristic Search,                          */
/*   Proc. AAAI Spring Symposium on Model-Based Validation of Inteligence, */
/*   AAAI, Stanford, April 2001.                                           */
/* Send bug-reports or questions to: lafuente@informatik.uni-freiburg.de   */

/* Parameters */
char Selected_Algorithm;           /* Search algorithm to be used. */
#define DEFAULT_ALGORITHM 'd'
int Depth_Bound;                   /* Maximum reachable depth. */
#define DEFAULT_DEPTH_BOUND 10000
int Selected_maxh;                 /* Maximum heuristic estimate. */
#define DEFAULT_MAXH 1000
unsigned char Selected_WH;         /* Weight of h value to be used. */
#define DEFAULT_WH 1
unsigned char Selected_WG;         /* Weight of g value to be used. */
#define DEFAULT_WG 1
int Selected_Hash_Size;            /* Size of hash table (number of entries. */
#define DEFAULT_HASH_SIZE 18
int Selected_Cache_Size;           /* Size of cache for IDA*. */
#define DEFAULT_CACHE_SIZE 22
int Selected_Bit_Array_Size;       /* Size of bitstate table. */
#define DEFAULT_BIT_ARRAY_SIZE 30
unsigned char Reach;               /* Print or not unreached states. */
#define DEFAULT_REACH 0;
unsigned char Print_Solution;      /* Print or not print solution. */
#define DEFAULT_PRINT_SOLUTION 0
unsigned char Write_Trail;         /* Write trail or not. */
#define DEFAULT_WRITE_TRAIL 1
int Supertraces;                   /* Number of runs of supertrace. */
#define DEFAULT_SUPERTRACES 1
int randomize;
#define DEFAULT_RANDOMIZE 0
int Selected_Continue;
#define DEFAULT_CONTINUE 0

int Iteration_Bound;
#define DEFAULT_ITERATION_BOUND 1000

void print_algorithms(void);
void print_weights(void);
void interrupt(int i);

/* End Parameters */

/****** Available Search Algorithms ******/
#define DFS 'd'
#define DFS2 'x'
#define ADFS 'D'
#define ADFS2 'X'
#define ASTAR 'A'
#define IDASTAR 'i'
#define HYBRID_IDASTAR 'h'
#define NDFS 'n'
#define INDFS 'N'
#define RESPONSE 'r'
#define IMPROVE_CYCLE 'c'
#define IMPROVE_CYCLE2 'C'
#define GENETIC 'g'
#define GENETIC2 'G'

int old_brk; /* Old break value for estimating memory consumption. */

/* Includes */
#include <stdlib.h>
#include <stdio.h>
#include <unistd.h>
#include <signal.h>
#include <time.h>
#include <debug.h>
#include <global.h>            /* State definitions */
#include <symmetry.h>          /* Symmetry Reduction for the philosophers */
#include <partial_order.h>     /* Partial Order Reduction things. */
#include <protocol.h>          /* Expansion function,... */
#include <search.h>            /* Generic search class */
#include <astar.h>             /* A* search class */
#include <dfs.h>               /* Depth-first search class */
#include <dfs2.h>              /* Depth-first search class (expands only next successor) */
#include <idastar.h>           /* IDA* search class */
#include <ndfs.h>              /* Nested Depth-first search class (normal and improved). */ 
#include <response.h>          /* A*+NDFS */
#include <genetic.h>           /* Genetic Algorithm */
#include <partial_order.h>     /* Partial Order Reduction things. */

#include <search.c>

void print_algorithms(void){
  printf("Available Algorithms are:\n");
  printf("\t%c: Depth-First Search (Enforced DFS if heuristic defined)\n",DFS);
  printf("\t%c: Admissible Depth-First Search\n",ADFS);
  printf("\t%c: AStar (Bread-First if no heuristic or wh=0. BestFirst if wg=0)\n",ASTAR);
  printf("\t%c: IDAStar\n",IDASTAR);
  printf("\t%c: Nested depth-first search\n",NDFS);
  printf("\t%c: A*+Nested depth-first search\n",RESPONSE);
  printf("\t%c: Improved Nested depth-first search\n",INDFS);
  printf("\t%c: Improve liveness trail with A*\n",IMPROVE_CYCLE);
  printf("\t%c: Improve liveness trail with A* (equivalent seeds)\n",IMPROVE_CYCLE2);
  printf("\t%c: Genetic Algorithm\n",GENETIC);
  printf("\tDefault value is %c\n",DEFAULT_ALGORITHM);
}

void print_weighth(void){
  printf("Weighting of the heuristic Function\n");
  printf("\t 0: uninformed search\n");
  printf("\t 1: optimal informed search\n");
  printf("\t>1: suboptimal informed search\n");
}

void print_weightg(void){
  printf("Weighting of g\n");
  printf("\t 0: best-first\n");
  printf("\t 1: A*\n");
}

Search *Algo;
Search *AuxAlgo; /* Used for reproducing the given error. */

#include <partial_order.c>

void interrupt(int i){
  printf("Search Interrumpted!\n");
  if(Algo){
    Algo->statistics();
    exit(0);
  } else if(AuxAlgo) AuxAlgo->statistics();
  exit(0);
}

Protocol *proto;
#include <symmetry.c>          /* Symmetry Reduction for the philosophers */

void check(void) {
  unsigned int maxf=(Selected_WG*Depth_Bound+Selected_WH*Selected_maxh); /* Maximum total F value. */ 
  int r;
  int auxh;
  Protocol *auxproto,*my_proto;

  the_hash_function=new Hash_Function(HOLZMANN_ORIGINAL,32); /* create hash function. */
  the_hash_function->rand(); /* randomize hash function. */

  my_proto = new Protocol(Selected_maxh); proto=my_proto;
  printf("Verifying %s...\n",Source);

  if(Selected_Algorithm==IMPROVE_CYCLE || Selected_Algorithm==IMPROVE_CYCLE2 || Selected_Heuristic==HAMMING_DISTANCE || Selected_Heuristic==STATE_BASED || Selected_Goal==GIVEN_STATE || Selected_Heuristic==SYMMETRY_FSM1 || Selected_Heuristic==SYMMETRY_FSM2 || Selected_Goal==ORBIT
#ifdef ARROWPROTOCOL
     ||  Selected_Heuristic==LINKINVERSIONS || Selected_Heuristic==HAMMINGGRAPH || Selected_Heuristic==DEGREES
#endif
){
    auxh=Selected_Heuristic;
    Selected_Heuristic=TRAIL_FILE;
    auxproto = new Protocol(Selected_maxh);
    //AuxAlgo = new AStar(Selected_Hash_Size,Depth_Bound+Selected_maxh,1,1);
    AuxAlgo = new Dfs(Selected_Hash_Size,Depth_Bound+Selected_maxh,0,0);
    AuxAlgo->init(auxproto);
    printf("Trying to reproduce trail...\n");
    if(AuxAlgo->search(Depth_Bound)==-1){
      printf("Error! Unable to reproduce error from trail.\n");
      printf("Please make sure that the trail was generated by using the same Promela source file. ");
      possible_bug();
      exit(0);
    }
    printf("Trail reproduced.\n");
#ifdef SYMMETRY
    if(symmetry){
      canonicalize_state(AuxAlgo->sol_ind[0]);
      construct_error_orbit(AuxAlgo->sol_ind[0]);
    }
#endif //
    proto=my_proto;
    proto->My_Heuristic->set_goal_state(AuxAlgo->sol_ind[0]);
    proto->My_Goal->set_goal(AuxAlgo->sol_ind[0]);
#ifdef ARROWPROTOCOL
    /* The problem is that after reaching the goal state the never claims continues to move to reach its endstate thus forcing further transitions in the system. */
    proto->My_Heuristic->set_goal_state(AuxAlgo->sol_ind[4]);
    proto->My_Goal->set_goal(AuxAlgo->sol_ind[4]);
#endif
    //delete AuxAlgo;
    Selected_Heuristic=auxh;
  }

#ifdef BITSTATE
  Selected_Hash_Size=Selected_Bit_Array_Size;
  Selected_Cache_Size=Selected_Bit_Array_Size;
#endif //
  
  switch(Selected_Algorithm){
  case GENETIC:
    Algo = new Genetic(Selected_Hash_Size,maxf,0);
    break;
  case GENETIC2:
    Algo = new Genetic(Selected_Hash_Size,maxf,1);
    break;
  case DFS:
    Algo = new Dfs(Selected_Hash_Size,maxf,0,Selected_Continue);
    break;
  case DFS2:
    Algo = new Dfs2(Selected_Hash_Size,maxf,0);
    break;
  case ADFS:
    Algo = new Dfs(Selected_Hash_Size,maxf,1,1);
    break;
  case ADFS2:
    Algo = new Dfs2(Selected_Hash_Size,maxf,1);
    break;
  case ASTAR:
    Algo = new AStar(Selected_Hash_Size,maxf,Selected_WG,Selected_WH);
    break;
  case IDASTAR:
    Algo = new IDAStar(Selected_Cache_Size,Selected_Hash_Size,maxf,Selected_WG,Selected_WH);
    break;
  case NDFS:
    Algo = new Ndfs(Selected_Hash_Size,maxf,0);
    break;
  case INDFS:
    Algo = new Ndfs(Selected_Hash_Size,maxf,1);
    break;
  case RESPONSE:
    Algo = new Response(Selected_Hash_Size,maxf,Selected_WG,Selected_WH);
    break;
  case IMPROVE_CYCLE2:
    Selected_Goal=EQUIVALENT_SEED;
  case IMPROVE_CYCLE:
    Algo = new AStar(Selected_Hash_Size,maxf,Selected_WG,Selected_WH);
    Algo->init(proto); /* Init the algorithm */
    if(Selected_Goal=EQUIVALENT_SEED)
      printf("Shortening path to equivalent seed with ");
    else
      printf("Shortening path to seed with ");
    Algo->print_name(); printf("...\n");
    r=Algo->search(Depth_Bound); /* Start search */
    if(r!=-1 && Write_Trail){
      printf("Writing Trail\n");
      Algo->print_trail(); printf("\tLength of trail is %d\n",depth);
    } else if(r==-1) { printf("\tseed not found!\n"); bug(); }
    //proto->My_Heuristic->set_goal_state(Algo->sol_ind[0]);
    //proto->My_Goal->set_goal(Algo->sol_ind[0]);
    if(Print_Solution && r){
      printf("Printing Solution...\n");
      Algo->print_solution();
    }
    printf("Printing Statistics...\n");
    Algo->statistics();

    Selected_Goal=GIVEN_STATE;
    //Algo = new AStar(Selected_Hash_Size,maxf,Selected_WG,Selected_WH);
    //Algo->init(proto);
    //Algo->proto=proto;
    Algo->S=*proto->My_Goal->given_state;
    //Algo->S.ps=new PackedState;
    //memcpy(Algo->S.ps,proto->My_Goal->given_state->ps,proto->My_Goal->given_state->ps->_vsz);
    Algo->S.pred=(State *)0; Algo->S.move.o_t=(Trans *)0;
    Algo->S.g = 0; Algo->S.h = proto->Heuristic(&Algo->S); /* Set h value. */
    printf("Shortening cycle with "); Algo->print_name(); printf("...\n");
    r=Algo->search(Depth_Bound); /* Start search */
    if(r==-1) { printf("\tseed not found!\n"); bug(); }
    if(Print_Solution && r){
      printf("Printing Solution...\n");
      Algo->print_solution();
    }
    printf("Printing Statistics...\n");
    Algo->statistics();
    //exit(0);
    if(Reach) do_reach();
    if(r!=-1 && Write_Trail){
      printf("Writing Trail\n");
      Algo->print_trail(); printf("\tLength of trail is %d\n",depth);
    } else if(r==-1 && (Selected_Heuristic==HAMMING_DISTANCE || Selected_Heuristic==STATE_BASED)) {
      printf("Error! Error found while reproducing trail, but not while checking.\n");
      bug();
      exit(0);
    }
    exit(0);
  default:
    printf("Error! Undefined algorithm.\n"); print_algorithms(); exit(0);
  }

  Algo->init(proto); /* Init the algorithm */
  printf("Checking for "); print_goal();
  printf(" with "); Algo->print_name(); printf("...\n");
  r=Algo->search(Depth_Bound); /* Start search */
  if(r==-1) printf("\tno errors found!\n");
  if(Print_Solution && r){
    printf("Printing Solution...\n");
    Algo->print_solution();
  }
  printf("Printing Statistics...\n");
  Algo->statistics();
  if(Reach) do_reach();
#ifndef NOREDUCE
  if(r!=-1 && Filter_Trail) Algo->filter_trail();
#endif //
  if(r!=-1 && Write_Trail){
    printf("Writing Trail\n");
    Algo->print_trail(); printf("\tLength of trail is %d\n",depth);
    if(Print_Solution && r){
      printf("Printing Reduced Solution...\n");
      Algo->print_solution();
    }
  } else if(r==-1 && (Selected_Heuristic==HAMMING_DISTANCE || Selected_Heuristic==STATE_BASED)) {
    printf("Error! Error found while reproducing trail, but not while checking.\n");
    bug();
    exit(0);
  }
}

#include <parameters.h>
#include <time.h>
int main(int argc, char *argv[]) {
  Parameters Param;
  //State *state; int i;
  //printf("Begin %d\n", clock());
        
  /* Get old brk value */
  old_brk=(int) sbrk(0) - 1448*1240; /* How can i get the initial heap address?  */
  /*scanf("\n");*/

  // added by Liu
  int begin = clock();
  
  if(!Param.process(argc, argv)) exit(0);
  if(randomize){ srandom((unsigned int)time((time_t*)0));}
  signal(SIGINT, interrupt);
  check();
  printf("\n***************Duration %dms\n", (clock() - begin) * 1000/ (CLOCKS_PER_SEC));
}
