/* 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   */

#ifndef _PARAMETERS_
#define _PARAMETERS_

#define ALGORITHM 'A'
#define ERROR 'E'
#define HEURISTIC 'H'
#define WEIGHTH 'W'
#define WEIGHTG 'w'
#define DANGER 'D'
#define SNAPSHOT 'S'
#define REACH 'r'
#define PRINT_SOLUTION 'P'
#define DEPTH_BOUND 'd'
#define SELECTED_MAXH 'm'
#define SUPERTRACES 'R'
#define WRITE_TRAIL 'T'
#define HASH_SIZE 's'
#define BIT_ARRAY_SIZE 'b'
#define CACHE_SIZE 'c'
#define COMPRESSION 'K'
#define POC3 'C'
#define POH 'h'
#define FILTER_TRAIL 'F'
#define HISTORY 'l'
#define POPULATION_SIZE 'p'
#define CHROMOSOME_SIZE 'x'
#define MUTATION_PROBABILITY 'M'
#define ELITISM 'e'
#define CROSSOVER 'z'
#define SYM 'X'
#define RANDOMIZE 'a'
#define CONTINUE 'k'
#define FITNESS_FUNCTION 'f'
#define MUTATION_FUNCTION 'u'
#define SELECTION_FUNCTION  't'
#define ENCODING_METHOD 'N'
#define ITERATION_BOUND 'i'
                                                                                        
class Parameters{
 public:
  int process(int argc, char **argv);
  int process(char *argv);
  void usage(void);
  void values(char p);
  void set_defaults(void);
};

int Parameters::process(int argc, char **argv){
  int i,r;
  
  printf("HSF-SPIN 1.0\n");
  printf("A Simple Promela Verifier based on Heuristic Search Strategies.\n");
  printf("This tool is based on Spin 3.4.5  (by G.J. Holzmann) and\n");
  printf("                   on HsfLight 2.0 (by S. Edelkamp)\n");
  set_defaults();
  if(argc==1){ /* if only the program name is given */
    usage();
    return 0;
  }
  /* argc[0] is the program name */
  for(i=1; i<argc; i++){
    r=process(argv[i]);
    if(!r){
      return 0;
    }
  }
  return 1;
}

int Parameters::process(char *argv){
  if(argv[0]!='-'){
    printf("Error: arguments must be preceded by '-'!\n");
    usage();
    return 0;
  }
  if(argv[2]=='\0'){
    values(argv[1]);
    usage();
    return 0;
  }
  switch(argv[1]){
  case ALGORITHM:
    Selected_Algorithm=argv[2];
    break;
  case ERROR:
    Selected_Goal=argv[2];
    break;
  case HEURISTIC:
    Selected_Heuristic=argv[2];
    break;
  case WEIGHTH:
    Selected_WH=atoi(&argv[2]);
    break;
  case WEIGHTG:
    Selected_WG=atoi(&argv[2]);
    break;
  case DANGER:
    Selected_Danger=atoi(&argv[2]);
    break;
  case SNAPSHOT:
    Selected_Snapshot=atoi(&argv[2]);
    break;
  case REACH:
    Reach=atoi(&argv[2]);
    break;
  case PRINT_SOLUTION:
    Print_Solution=atoi(&argv[2]);
    break;
  case DEPTH_BOUND:
    Depth_Bound=atoi(&argv[2]);
    break;
  case SELECTED_MAXH:
    Selected_maxh=atoi(&argv[2]);
    break;
  case SUPERTRACES:
    Supertraces=atoi(&argv[2]);
    break;
  case WRITE_TRAIL:
    Write_Trail=atoi(&argv[2]);      
    break;
  case HASH_SIZE:
    Selected_Hash_Size=atoi(&argv[2]);
    break;
  case BIT_ARRAY_SIZE:
    Selected_Bit_Array_Size=atoi(&argv[2]);
    break;
  case CACHE_SIZE:
    Selected_Cache_Size=atoi(&argv[2]);
    break;
  case COMPRESSION:
    Selected_Compression=atoi(&argv[2]);
    break;
#ifndef NOREDUCE
  case POC3:
    Selected_C3=atoi(&argv[2]);
    break;
  case POH:
    Selected_Ample_Heuristic=atoi(&argv[2]);
    break;
  case FILTER_TRAIL:
    Filter_Trail=atoi(&argv[2]);
    break;
  case HISTORY:
    Selected_History_Length=atoi(&argv[2]);
    break;
#endif //
  case POPULATION_SIZE:
    population_size=atoi(&argv[2]);
    break;
  case CHROMOSOME_SIZE:
    chromosome_size=atoi(&argv[2]);
    break;
  case MUTATION_PROBABILITY:
    mutation_probability=(double)atof(&argv[2]);
    break;
  case ELITISM:
    elitism=atoi(&argv[2]);
    break;
#ifdef SYMMETRY
  case SYM:
    symmetry=atoi(&argv[2]);
    break;
#endif //
  case RANDOMIZE:
    randomize=atoi(&argv[2]);
    break;
  case CROSSOVER:
    crossover_operator=atoi(&argv[2]);
    break;
  case CONTINUE:
    Selected_Continue=atoi(&argv[2]);
    break;
  case FITNESS_FUNCTION:
    fitness_function = argv[2];
    break;
  case MUTATION_FUNCTION:
    mutation_function = argv[2];
    break;
  case SELECTION_FUNCTION:
    selection_function = argv[2];
    break; 
  case ENCODING_METHOD:
    encoding_method = argv[2];
    break;
  case ITERATION_BOUND:
    Iteration_Bound = atoi(&argv[2]);
    break;
  default:
    printf("Error: undefined argument!\n");
    usage();
    return 0;
  }
  return 1;
}

void Parameters::usage(void){
  printf("Parameters:\n");
  printf("\t-%cx: x=Search Algorithm\n",ALGORITHM);
  printf("\t-%cx: x=Error to be checked\n",ERROR);
  printf("\t-%cx: if x continue search in dfs.\n",CONTINUE);
  printf("\t-%cx: x=Heuristic Function\n",HEURISTIC);
  printf("\t-%cx: x=Weighting for h in A*\n",WEIGHTH);
  printf("\t-%cx: x=Weighting for g in A*\n",WEIGHTG);
  printf("\t-%cx: 2^x=Size of Hash table (number of entries)\n",HASH_SIZE);
  printf("\t-%cx: 2^x=Size of Cache for IDA* (number of states)\n",CACHE_SIZE);
  printf("\t-%cx: 2^x=Size of BitState Hash table (number of bits)\n",BIT_ARRAY_SIZE);
  printf("\t-%cx: x=Danger (for deadlock detection)\n",DANGER);
  printf("\t-%cx: show snapshot statistics each x stored states\n",SNAPSHOT);
  printf("\t-%cx: if x unreached states are printed\n",REACH);
  printf("\t-%cx: if x solution is printed\n",PRINT_SOLUTION);
  printf("\t-%cx: x=Depth bound\n",DEPTH_BOUND);
  printf("\t-%cx: x=Maximum value of heuristic estimate.\n",SELECTED_MAXH);
  printf("\t-%cx: x=Number of traces (for Supertrace)\n",SUPERTRACES);
  printf("\t-%cx: if x a trail file is created\n",WRITE_TRAIL);
  printf("\t-%cx: x=Compression Technique\n",COMPRESSION);
  printf("\t-%cx: if x random seed is randomized\n",RANDOMIZE);
#ifndef NOREDUCE
  printf("\t-%cx: x=C3 condition for partial order reduction\n",POC3);
  printf("\t-%cx: x=Heuristic for the selection of ample set\n",POH);
  printf("\t-%cx: if x filter is reordered for recovering quality lost by p.o.\n",FILTER_TRAIL);
#endif //
  printf("\t-%cx: x=length of history for thread interleaving heuristic.\n",HISTORY);
  printf("\t-%cx: x=size of population in genetic algorithm.\n",POPULATION_SIZE);
  printf("\t-%cx: x=size of chromosome (in bytes) in genetic algorithm.\n",CHROMOSOME_SIZE);
  printf("\t-%cx: x=mutation probability in genetic algorithm.\n",MUTATION_PROBABILITY);
  printf("\t-%cx: x=crossover operator in genetic algorithm.\n",CROSSOVER);
  printf("\t-%cx: if x elitism is applied in genetic algorithm.\n",ELITISM);
  printf("\t-%cx: x=fitness functions.\n", FITNESS_FUNCTION);
  printf("\t-%cx: x=mutation functions.\n", MUTATION_FUNCTION);
  printf("\t-%cx: x=selection functions.\n", SELECTION_FUNCTION);
  printf("\t-%cx: x=encoding methods.\n", ENCODING_METHOD);
  printf("\t-%cx: x=iteration bound.(DEFAULT: %d)\n", ITERATION_BOUND, DEFAULT_ITERATION_BOUND);
}

void Parameters::values(char p){
  switch(p){
  case ALGORITHM:
    print_algorithms();
    break;
  case ERROR:
    print_goals();
    break;
  case HEURISTIC:
    print_heuristics();
    break;
  case WEIGHTH:
    print_weighth();
    break;
  case WEIGHTG:
    print_weightg();
    break;
  case DANGER:
    print_dangers();
    break;
  case COMPRESSION:
    print_compressions();
  case SNAPSHOT:
    break;
  case REACH:
    break;
  case PRINT_SOLUTION:
    break;
  case DEPTH_BOUND:
    break;
  case SELECTED_MAXH:
    break;
  case SUPERTRACES:
    break;
  case WRITE_TRAIL:
    break;
  case HASH_SIZE:
    break;
  case CACHE_SIZE:
    break;
  case BIT_ARRAY_SIZE:
    break;
#ifndef NOREDUCE
  case POC3:
    print_C3_conditions();
    break;
  case POH:
    print_ampleh();
    break;
  case FILTER_TRAIL:
    break;
#endif //
  case POPULATION_SIZE:
    break;
  case CHROMOSOME_SIZE:
    break;
  case MUTATION_PROBABILITY:
    break;
  case CROSSOVER:
    print_crossover();
    break;
  case ELITISM:
    break;
  case SYM:
    break;
  case RANDOMIZE:
    break;
  case CONTINUE:
    break;
  case FITNESS_FUNCTION:
    print_fitness();
    break;
  case MUTATION_FUNCTION:
    print_mutation();
    break;
  case SELECTION_FUNCTION:
    print_selection();
    break;
  case ENCODING_METHOD:
    print_encoding();
    break;
  default:
    printf("Error: undefined argument!\n");
  }
}

void Parameters::set_defaults(void){
  Selected_Algorithm=DEFAULT_ALGORITHM;
  Selected_Heuristic=DEFAULT_HEURISTIC;
  Selected_Goal=DEFAULT_GOAL;
  Selected_WH=DEFAULT_WH;
  Selected_WG=DEFAULT_WG;
  Selected_Hash_Size=DEFAULT_HASH_SIZE;
  Selected_Cache_Size=DEFAULT_CACHE_SIZE;
  Selected_Bit_Array_Size=DEFAULT_BIT_ARRAY_SIZE;
  Selected_Danger=DEFAULT_DANGER;
  Selected_Snapshot=DEFAULT_SNAPSHOT;
  Selected_Compression=DEFAULT_COMPRESSION;
  Reach=DEFAULT_REACH;
  Print_Solution=DEFAULT_PRINT_SOLUTION;
  Depth_Bound=DEFAULT_DEPTH_BOUND;
  Selected_maxh=DEFAULT_MAXH;
  Supertraces=DEFAULT_SUPERTRACES;
  Write_Trail=DEFAULT_WRITE_TRAIL;
#ifndef NOREDUCE
  Selected_C3=DEFAULT_C3;
  Selected_Ample_Heuristic=DEFAULT_AMPLEH;
  Filter_Trail=DEFAULT_FILTER_TRAIL;
#endif //
  Selected_History_Length-DEFAULT_HISTORY_LENGTH;
  population_size=DEFAULT_POPULATION_SIZE;
  chromosome_size=DEFAULT_CHROMOSOME_SIZE;
  mutation_probability=DEFAULT_MUTATION_PROBABILITY;
  crossover_operator=DEFAULT_CROSSOVER;
  elitism=DEFAULT_ELITISM;
#ifdef SYMMETRY
  symmetry=DEFAULT_SYMMETRY;
#endif //
  randomize=DEFAULT_RANDOMIZE;
  Selected_Continue=DEFAULT_CONTINUE;
  fitness_function = FITNESS_ALBERTO;
  mutation_function = MUTATION_ALBERTO;
  selection_function = SELECTION_ALBERTO;
  encoding_method = ENCODING_ALBERTO;
  Iteration_Bound = DEFAULT_ITERATION_BOUND;
}

#endif //

