/*
        State Space Exploration Program Problem Defintion
        for the Pair Token Passing Problem

        Module problem.c, Revision 2.0, Date 1996-08-19
*/

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include "explore.h"
#include "problem.h"

/*  This section is intended to be read in conjunction with Section 3 */


/* The complete processor state: */
typedef struct {
    unsigned char phase;
    unsigned char inport;
    unsigned char mode;
} proc_state_t;

/* The system state is the state of the two processors a, b */
typedef struct {
    proc_state_t a;
    proc_state_t b;
} sys_state_t;

/* a bag of processor states */
#define MAX_PROBLEM_BAG_SIZE 3
typedef BAG_OF(proc_state_t, MAX_PROBLEM_BAG_SIZE);




/*  system state utility functions 

    Processor states are mapped 1-1 onto sequential state indexes in the
    range 0 ..  TOTAL_NUM_PROC_STATES - 1

    We need conversion functions between states and state indexes, and
    for printing states.
*/


/* convert processor state to processor index */
int proc_state_to_index( proc_state_t s ) {
    return ((s.phase * NUM_PROC_MODES) + s.inport ) * 
           NUM_PROC_MODES + s.mode;
}

/* convert processor index to processor state */
proc_state_t index_to_proc_state( int i ) {
    proc_state_t s;
    int t = i;
    s.mode = t % NUM_PROC_MODES;
    t = t / NUM_PROC_MODES;
    s.inport = t % NUM_PROC_MODES;
    t = t / NUM_PROC_MODES;
    s.phase = t % NUM_PROC_PHASES;
    return s;
}

/* convert system state to system index */
int sys_state_to_index( sys_state_t s ) {
    return proc_state_to_index(s.a) * TOTAL_NUM_PROC_STATES  +
        proc_state_to_index(s.b) ;
}

/* convert system index to system state */
sys_state_t index_to_sys_state( int i ) {
    sys_state_t s;
    int t = i;
    s.b = index_to_proc_state(t % TOTAL_NUM_PROC_STATES);
    t = t / TOTAL_NUM_PROC_STATES;
    s.a = index_to_proc_state(t % TOTAL_NUM_PROC_STATES);
    return s;
}


/* convert a system state s into to a string of the form

    <index>:(<astate>, <bstate>)<target_flag>

    where
        <index> is the state index of s
        <astate> is the state of processor a
        <bstate> is the state of processor b
        <target_flag> is T if s is a target state

    A processor state is  <phase><inport><mode>
    where
        <phase> is r or w
        <inport> is R, W, or P 
        <mode> is R, W, or P 

    HACK WARNING: no more than NUM_INTERNAL_BUFS instances of this 
    routine can be active, eg in an argument list, as an internal 
    buffer is required for each call.
*/

char* proc_state_phase_name[] = {"r", "w"};

char* proc_state_name[] = {"R", "W", "P"};

char* sys_state_to_str(sys_state_t s) {
    /* keep a buffer for each result */
    #define NUM_INTERNAL_BUFS 5
    static int cur_buf = NUM_INTERNAL_BUFS - 1;
    static char buf[NUM_INTERNAL_BUFS][256];
    int s_i;

    s_i = sys_state_to_index(s);
    cur_buf = ( cur_buf + 1 ) % NUM_INTERNAL_BUFS;
    sprintf(buf[cur_buf], "%d:(%s%s%s,%s%s%s)%s", 
                s_i,
                proc_state_phase_name[s.a.phase], 
                proc_state_name[s.a.inport],
                proc_state_name[s.a.mode],
                proc_state_phase_name[s.b.phase], 
                proc_state_name[s.b.inport],
                proc_state_name[s.b.mode],
                (target[s_i] ? "T" : "")
    );
    return buf[cur_buf];
}

/* convert state_index into string

   NOTE: the HACK WARNING for sys_state_to_str applies here also
*/
char* state_index_to_str(state_index_t s_i) {
    return sys_state_to_str(index_to_sys_state(s_i));
}


/*      
 *
 *              next_proc_state
 *
 *
 */

void next_proc_state(
    proc_state_t cur,     /* current state of processor */
    proc_state_t adj,     /* current state of adjacent processor */
    bag_of_proc_state_t* next_states /* result next possible states */
) {
/*  
    next state function for a processor
    
    As defined in Figure 1: Pair Token Passing Protocol 

    Pre: cur, adj are legitimate states
         next_states has enough capacity to hold result
    Post: none
    Side Effects: next_states will contain all of the possible next
        states that a processor in state cur with neighbour in state 
        adj can reach in one step.
*/

    proc_state_t next;

    next = cur;
    MAKE_BAG_EMPTY(*next_states);

    if ( cur.phase == P_READ ) {
        /* update input register from adjacent processor 
           Note: as part of its write phase, the adjacent processor does 
           a write to the output port register of its current mode.  Thus
           a read simply copies over the current mode of the adjacent 
           processor.
        */
        next.inport = adj.mode;
        next.phase = P_WRITE;
        ADD_TO_BAG( *next_states, next);
    } else if ( cur.phase == P_WRITE ) {
        next.phase = P_READ;

        /* change mode */
        if ( cur.mode == cur.inport ) {
            /* random choice of W, P, R */
            next.mode = M_READY;
            ADD_TO_BAG( *next_states, next);
            next.mode = M_PASSING;
            ADD_TO_BAG( *next_states, next);
            next.mode = M_WAITING;
            ADD_TO_BAG( *next_states, next);
        } else if ( cur.mode == M_WAITING && cur.inport == M_PASSING){
            next.mode = M_READY;
            ADD_TO_BAG( *next_states, next);
        } else if ( cur.mode == M_PASSING && cur.inport == M_READY ) {
            next.mode = M_WAITING;
            ADD_TO_BAG( *next_states, next);
        } else if ( cur.mode == M_READY && cur.inport == M_WAITING ) {
            next.mode = M_PASSING;
            ADD_TO_BAG( *next_states, next);
        } else {
            next.mode = cur.mode;
            ADD_TO_BAG( *next_states, next);
        }
    }
}

/*      
 *
 *              progress
 *
 *
 */
int progress(sys_state_t cur, sys_state_t next) {
/*
          Progess evaluation predicate

    Pre: system state next is a legitimate immediate successor 
        state to system state cur.

    Post: progress(cur, next) is
        1 if the activation that moves from cur -> next actually 
          results in progress.
        0 otherwise

    The scheduler is not permitted to schedule a processor activation 
    that does not result in progress.
*/
   

    proc_state_t activated;        /* the activated processor */
    proc_state_t adjacent;         /* the adjacent processor */
    proc_state_t next_activated;   /* next state of activated proc */
    proc_state_t next_adjacent;    /* next state of the adjacent proc */

    /* determine which processor was activated by seeing which one 
       changed phase */
    if ( cur.a.phase != next.a.phase && cur.b.phase == next.b.phase ) {
        /* processor A was activated */
        activated = cur.a;
        adjacent = cur.b;
        next_activated = next.a;         
        next_adjacent = next.b;
    } else if ( cur.a.phase == next.a.phase && 
            cur.b.phase != next.b.phase ) {
        /* processor B was activated */
        activated = cur.b;
        adjacent = cur.a;
        next_activated = next.b;
        next_adjacent = next.a;
    } else {
        assert(0);  /* ERROR: not exactly one processor was activated */  
    }
    
    /* adjacent processor should not change state */
    assert(adjacent.phase == next_adjacent.phase);
    assert(adjacent.inport == next_adjacent.inport);
    assert(adjacent.mode == next_adjacent.mode);


    /* from write to read phase is progress, i.e. do a write */
    if (activated.phase == P_WRITE && next_activated.phase == P_READ ) 
        return 1;
    
    /* if here, must be from read phase to write, i.e. do a read */
    
    /* from read phase to write phase is progress if:
    - a value different from the current inport value is read
    - the same value is read, but the mode of the processor would
      change anyway (with non-zero prob).  This prevents the scheduling 
      of infinite idle loops for a processor.
    */
    if ( activated.inport != next_activated.inport ) return 1;
    
    /* would it change mode anyway with non-zero probability ? */ 
    {
        bag_of_proc_state_t future_states;
        int item_num;
        next_proc_state(next_activated, adjacent, &future_states);
        for ( item_num = 0; 
              item_num < future_states.card; 
              item_num++ ) 
        {
            if (next_activated.mode != future_states.item[item_num].mode) 
                return 1;
        }
    }

    /* if got this far, the activation did not make progress */
    return 0;
}


/*      
 *
 *              sigma_fn
 *
 *
 */
/* 
        Compute sigma(cur)

    Pre: cur_i is the state index of system state cur,
         Note that cur_i is in the range 0 ... NUM_SYS_STATES-1
    Post: none
    Side Effects: successors will be sigma(cur), that is, it contains 
         an item for each progress-making processor activation for 
         state cur.

*/
void sigma_fn(
        state_index_t cur_i,
        bag_of_bag_of_state_index_t* successors
) {
    sys_state_t cur; 
    sys_state_t next; 
    bag_of_proc_state_t next_proc_states;
    bag_of_state_index_t next_sys_states;
    int item_num;
    int made_progress;

    cur = index_to_sys_state(cur_i);
    MAKE_BAG_EMPTY( *successors );

    /* activate A, 
       next_proc_states contains the possible next states for A */ 
    next_proc_state(cur.a, cur.b, &next_proc_states);

    /* 
        build the bag that contains the next possible SYSTEM states resulting
        from activating A.  Activating A is a valid scheduling choice if 
        at least one of the possible next states results in progress
    */
     
    MAKE_BAG_EMPTY( next_sys_states );
    made_progress = 0;      /* track whether progress was made */
    for (item_num =0; item_num < next_proc_states.card; item_num++ ) {
        /* 
            build a next system state by replacing the current state 
            of A by a possible successor state
        */
        next = cur;
        next.a = next_proc_states.item[item_num];
        ADD_TO_BAG( next_sys_states, sys_state_to_index(next));
        
        if ( progress(cur, next) ) made_progress = 1;
    }

    if ( made_progress ) {
        ADD_TO_BAG( *successors, next_sys_states);
    } else {
        /* display the activations rejected on the grounds of 
           no progress */
        int i;
        printf("A in state %s ->",
            sys_state_to_str(cur));
        for ( i=0; i < next_sys_states.card; i++ ) {
            printf(" %s", sys_state_to_str(index_to_sys_state(
              next_sys_states.item[i])));
        }
        printf("\n");
    }

    /* activate B - so the same as for A above */
    next_proc_state(cur.b, cur.a, &next_proc_states);

    MAKE_BAG_EMPTY( next_sys_states );
    made_progress = 0;
    for (item_num =0; item_num < next_proc_states.card; item_num++ ) {
        next = cur;
        next.b = next_proc_states.item[item_num];
        ADD_TO_BAG( next_sys_states, sys_state_to_index(next));
        
        if ( progress(cur, next) ) made_progress = 1;
    }

    if ( made_progress ) {
        ADD_TO_BAG( *successors, next_sys_states);
    } else {
        int i;
        printf("B in state %s ->",
            sys_state_to_str(cur));
        for ( i=0; i < next_sys_states.card; i++ ) {
            printf(" %s", sys_state_to_str(index_to_sys_state(
                next_sys_states.item[i])));
        }
        printf("\n");
    }
}

/*
        Compute the sigma table

    Pre: none
    Post: none
    Side Effects: 
        Computes sigma(q) for each q, and records this in sigma[q_i],
    also prints out the activations that were rejected on the grounds 
    that they do not make any progress.
*/
int compute_sigma(void) {
    int q_i;
    printf("Computing sigma(q).\n");
    printf("Activations rejected on the grounds of no progress:\n");
    for (q_i=0; q_i < NUM_SYS_STATES; q_i++ ) {
        sigma_fn(q_i, &sigma[q_i]);
    }
    printf("Finished computing sigma(q)\n");

    return 1;
}




/*      
 *
 *              compute_target
 *
 *
 */
/*  
        Compute the target set for the pair token passing problem.

    compute_target checks that the target set is a cycle (i.e. exactly 
    one scheduling decision at each point, and exactly one successor 
    state to each decision).  The user must confirm that it captures 
    the details of the token passing protocol, that is it goes through 
    the cycle of modes:

        WP, RP, RW, PW, PR, WR, WP, ...

    Pre: sigma table is well-defined
    Post: compute_and_print_target() is
        1 if target set is a cycle 
        0 otherwise
    Side Effects: 
        defines the target array,
        prints out the cycle and error messages if it is flawed.
*/

int compute_target(void) {
    sys_state_t init_state;
    sys_state_t cur_state;
    int init_state_i;
    int cur_state_i;
    int next_state_i;

    int q_i;
    int target_ok;  /* 1 if a cycle, 0 if flawed */
    int length;     /* the length of the path so far */
    int done;       /* 1 when path following finished */

    /* initial target state wRP rPR */
    init_state.a.phase = P_WRITE;
    init_state.b.phase = P_READ;

    init_state.a.mode = M_PASSING;
    init_state.b.mode = M_READY;

    init_state.a.inport = init_state.b.mode;
    init_state.b.inport = init_state.a.mode;

    /* initialize target array */
    for (q_i=0; q_i < NUM_SYS_STATES; q_i++ ) {
        target[q_i] = 0;
    }

    printf("Target cycle:\n");
    init_state_i = sys_state_to_index(init_state);
    target_ok = 0;

    /* 
        now simply walk down the path from the initial state until it is 
        reached again 
    */
    done = 0;
    cur_state_i = init_state_i;
    length = 0;

    while ( ! done ) {

        cur_state = index_to_sys_state(cur_state_i);
        target[cur_state_i] = 1;

        /* print our current position on the path */
        printf("%3d %s%s %s\n", length, 
                proc_state_name[cur_state.a.mode],
                proc_state_name[cur_state.b.mode],
                sys_state_to_str(cur_state)
        );

        if ( length > NUM_SYS_STATES ) {
            printf("Error, too great a cycle length, not a cycle\n");
            target_ok = 0;
            done = 1;
        }

 
        /* there must be only one possible scheduling decision */
        if ( sigma[cur_state_i].card != 1 ) {
            printf("Error, more than one possible scheduling decision.\n");
            target_ok = 0;
            done = 1;
        }

        /* at this point only one scheduling decision, item 0 */

        /* there must be only one possible successor state */ 
        if ( sigma[cur_state_i].item[0].card != 1 ) {
            printf("Error, more than one possible successor state.\n");
            target_ok = 0;
            done = 1;
        }

        /* get the next state */
        next_state_i = sigma[cur_state_i].item[0].item[0];
        length ++;       

        /* did we return to the initial state? */
        if ( init_state_i == next_state_i ) {
            printf("Return to initial state.\n");
            target_ok = 1;
            done = 1;        
        } else {
            cur_state_i = next_state_i; 
        }
    }

    if ( target_ok ) {
        printf("Target set is well defined.\n\n");
    } else {
        printf("Target set is not well defined.\n\n");
    }

    return target_ok;
}