/* 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 _GOALS_
#define _GOALS_

/* Type of errors */
#define NO_GOAL 'n'
#define DEADLOCK 'd' /* Warning: for endstates (states without successors) */
#define ASSERTION_VIOLATION 'a'
#define SIMPLESAFETY 's' /* assertion violation or deadlock */
#define VALID_ENDSTATE 'v'
#define GIVEN_STATE 'g' /* Set state with method set_goal() (see later) */
#define ORBIT 'o' /* orbit of given state */
#define LTL 'l' /* Warning: only endstates in claim will be checked. Cycles must be detected by the search algorithm */
#define EQUIVALENT_SEED 'e'
#define LIVENESS  'L'
/* End Type of errors */

char Selected_Goal;
/* Type of error to be detected. Set as argument in command line
   and used as global variable in many places (search algorithm, goal functions, etc. */
int given_state_available;


/* Settings for Parameters.h */
#define DEFAULT_GOAL NO_GOAL
void print_goals(void) /* Procedure that visualizes the available kind of errors */
{
  printf("Possible Goals are:\n");
  printf("\t%c: no goal\n",NO_GOAL);
  printf("\t%c: deadlocks\n",DEADLOCK);
  printf("\t%c: assertion violations\n",ASSERTION_VIOLATION);
  printf("\t%c: simple safety properties (deadlocks and assertion violations)\n",SIMPLESAFETY);
  printf("\t%c: valid endstates\n",VALID_ENDSTATE);
  printf("\t%c: violation of LTL properties\n",LTL);
  printf("\t%c: liveness\n", LIVENESS);
  printf("\tGoals for a given error trail\n");
  printf("\t%c: given state\n",GIVEN_STATE);
#ifdef SYMMETRY
  printf("\t%c: orbit of given state (when symmetry reduction is applied)\n",ORBIT);
#endif // SYMMETRY
  printf("\tDefault value is %c\n",DEFAULT_GOAL);
}
/* End Settings for Parameters.h */

void print_goal(void) /* Auxiliary function used in the main programm */
{
  switch(Selected_Goal){
  case NO_GOAL: printf("nothing"); break;
  case DEADLOCK: printf("deadlocks"); break;
  case ASSERTION_VIOLATION: printf("assertion violations"); break;
  case SIMPLESAFETY: printf("safety errors"); break;
  case VALID_ENDSTATE: printf("valid endstates"); break;
  case GIVEN_STATE: printf("a given state"); break;
  case ORBIT: printf("orbit of a given state"); break;
  case LTL: printf("violation of an LTL formula"); break;
  case EQUIVALENT_SEED: printf("equivalent seed"); break;
  case LIVENESS: printf("liveness");break;
  default: printf("Error! Undefined goal.\n"); exit(0);
  }
}

/* Class Protocol_Goal */
class Protocol_Goal{
 public:
  State *given_state;

  Protocol_Goal(){};
  int is_in_orbit;

  int Is_Goal(State *S, int p){
    switch(Selected_Goal){
      case NO_GOAL:
        return 0;
        break;
      case DEADLOCK: /* Given that S has no successors. */
        return deadlock_goal(S,p);
        break;
      case VALID_ENDSTATE: /* Given that S has no successors. */
        return valid_endstate_goal(S,p);
        break;
      case ASSERTION_VIOLATION:
        return assertion_violation_goal(S,p); break;
      case SIMPLESAFETY:
        return assertion_violation_goal(S,p) || deadlock_goal(S,p); break;
      case GIVEN_STATE: /* Given state must be set before this is used. */
        if(!given_state_available)
          return 0; /* No state available yet. */
        if(PackedState::equal(*(given_state->ps),*(S->ps))){
          if(p)
            printf("\tgiven state (at depth %d)\n",S->g);

          return 1;
        }else
          return 0;
      case EQUIVALENT_SEED:
        return equivalent_seed(S,p);
      case ORBIT: /* Given state must be set before this is used. */
        if(!given_state_available)
          return 0; /* No state available yet. */

#ifdef SYMMETRY
        if(ErrorOrbit->search(S)){
          printf("\torbit of given state (at depth %d)\n",S->g);
          return 1;
        }else
          return 0;

      /* Atencion, no siempre S esta canicalizado! */

#ifndef SYMMOD
#ifndef CANONICAL
        is_in_orbit=PackedState::equal(*(given_state->ps),*(S->ps));
        full2_zeta(S->ps);
        if(p && is_in_orbit)
          printf("\torbit of given state (at depth %d)\n",S->g);

        return is_in_orbit;
#endif //
#endif //

        PackedState *rep_aux;
        PackedState rep_s,rep_g;
        vsize=S->ps->_vsz;
#ifdef SYMMETRY
#ifndef SYMMOD
        rep_aux=zeta(S->ps);
        memcpy(&rep_s,rep_aux,vsize);
        rep_aux=zeta(given_state->ps);
        memcpy(&rep_g,rep_aux,vsize);
#else
        canonicalize_state(S);
        canonicalize_state(given_state);
        memcpy(&rep_s,S->ps,vsize);
        memcpy(&rep_g,given_state->ps,vsize);
#endif //
#endif //
        if(PackedState::equal(rep_s,rep_g)){
          //canonicalize_state(S);
          //canonicalize_state(given_state);
          /* The next is OK iif rep is canonical and both given_state are S are reps.*/
          //if(PackedState::equal(*(given_state->ps),*(S->ps))){
          if(p)
            printf("\torbit of given state (at depth %d)\n",S->g);

          return 1;
        }else{
          /*if(assertion_violation_goal(S,p) && S->g==33){
      	  printf("Symmetric????\n");
      	  for(int j=0; j<rep_s._vsz; j++) printf("%d ",((unsigned char *)&rep_s)[j]); printf("\n");
      	  for(int j=0; j<rep_g._vsz; j++) printf("%d ",((unsigned char *)&rep_g)[j]); printf("\n");
	        }*/
          return 0;
        }
#endif //
    case LTL: /* Check claim endstates only. */
      return claim_matched(S,p);
        break;
    case LIVENESS:
      //return claim_matched(S, p);
      break;
    default:
      printf("Error! Undefined goal %d\n",Selected_Goal); exit(0);
    }
  }
    
  void set_goal(State *S){
    /* This procedure sets the goal state vector */
    given_state=new State;
    // *given_state=*S;
    given_state->ps=new PackedState;
    memcpy(given_state->ps,S->ps,S->ps->_vsz);
    given_state_available=1;
  }

 private:

  int assertion_violation_goal(State *S, int p){
    /* This function checks if an assertion has been violated
       by re-executing the transition and testing the value
       of flag assertion_violated. */
    Trans *t;

    t=S->move.o_t;

    if((!t) || !(t->lextok_tree) || (t->lextok_tree->ntyp!=ASSERT))
      /* If no transition lead to S (it is the root state) or
	 there is no lextok_tree or transition is not an assertion then
	 no assertion has been violated */
       return 0;

    now=S->ps; /* Set now and this_p for eventual use in val(). */
    this_p=pptr(S->move.pr);
    assertion_violated=!(t->lextok_tree->lft->val());
    if(assertion_violated && p)
      printf("\tassertion violated (%s) (at depth %d)\n",t->tp,S->g);
    return assertion_violated;
  }
  
  int valid_endstate_goal(State *S, int p){
    /* Warning: It is supposed that S has no successors.
       It should be used after expanding S and checking that S has no successors. */
    int v;

    now=S->ps; /* now must point to state vector for endstate () */
    if(now->boq!=-1){
      /* If it it is not a real state, but a rendezvous try, return 0 */
      return 0;
    }
    v=endstate();
    if(v && p) printf("\tvalid endstate (at depth %d)\n",S->g);
    return v;
  }

  int deadlock_goal(State *S, int p){
    /* Warning: It is supposed that S has no successors.
       It should be used after expanding S and checking that S has no successors. */
    int v;

    now=S->ps; /* now must point to state vector for endstate () */
    if(now->boq!=-1){
      /* If it it is not a real state, but a rendezvous try, return 0 */
      return 0;
    }
    v=!endstate();
    if(v && p) printf("\tinvalid endstate (at depth %d)\n",S->g);
    return v;
  }

  int claim_matched(State *S, int p){
    /* Note that cycles are detected in the search algorithm not here.
       This function checks only if the never claim is an endstate */
#ifdef VERI
    if(((P0 *)hsf_pptr(S->ps,0))->_p == endclaim ){ /* never claim in endstate */
      if(p) printf("\tclaim violated! (at depth %d)\n",S->g);
      return 1;
    }
    if(stopstate[VERI][((P0 *)hsf_pptr(S->ps,0))->_p]){ /* never claim in stopstate */
      if(p) printf("\tendstate in claim reached\n");
      return 1;
    }
#endif //
    return 0;
  }

  int equivalent_seed(State *S, int p){
    unsigned u,v;

#if 0 /* philo */

    for(int i=0; i<S->ps->_nr_pr; i++){
      u=(int)((P0 *)hsf_pptr(S->ps,i))->_p;
      v=((P0 *)hsf_pptr(given_state->ps,i))->_p;
      if(u!=v) return 0;
    }

#elif 0 /* giop */

    /* never claim */
    u=(int)((P0 *)hsf_pptr(S->ps,VERI))->_p;
    v=((P0 *)hsf_pptr(given_state->ps,VERI))->_p;
    if(u!=v) return 0;
    /* user[3] */
    u=(int)((P0 *)hsf_pptr(S->ps,3))->_p;
    v=((P0 *)hsf_pptr(given_state->ps,3))->_p;
    if(u!=v) return 0;

#elif 0 /* elevator */

    /* never claim */
    u=(int)((P0 *)hsf_pptr(S->ps,VERI))->_p;
    v=((P0 *)hsf_pptr(given_state->ps,VERI))->_p;
    if(u!=v) return 0;
    /* init */
    u=(int)((P0 *)hsf_pptr(S->ps,1))->_p;
    v=((P0 *)hsf_pptr(given_state->ps,1))->_p;
    if(u!=v) return 0;
    /* level[4] */
    u=(int)((P0 *)hsf_pptr(S->ps,4))->_p;
    v=((P0 *)hsf_pptr(given_state->ps,4))->_p;
    if(u!=v) return 0;
    /* elevator[5] */
    u=(int)((P0 *)hsf_pptr(S->ps,5))->_p;
    v=((P0 *)hsf_pptr(given_state->ps,5))->_p;
    if(u!=v) return 0;
    /* controller[6] */
    u=(int)((P0 *)hsf_pptr(S->ps,6))->_p;
    v=((P0 *)hsf_pptr(given_state->ps,6))->_p;
    if(u!=v) return 0;
    if(given_state->ps->elevator_pos!=S->ps->elevator_pos) return 0;
    if(given_state->ps->elevator_opened!=S->ps->elevator_opened) return 0;
    if(given_state->ps->elevator_tick!=S->ps->elevator_tick) return 0;
    if(given_state->ps->controller_tick!=S->ps->controller_tick) return 0;
    if(given_state->ps->level_requested[2]!=S->ps->level_requested[2]) return 0;

#endif //    

    if(p) printf("\tequivalent seed (at depth %d)\n",S->g);
    return 1;
  }
};

#endif // _GOALS_
