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

        Problem-specific hooks expected by explore.c

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

/*
        PROBLEM SPECIFIC DEFINITIONS
*/

/* Description of the state of a single processor.

   Each processor is in a phase of its basic execution cycle:
        P_READ  - ready to read the input register
        P_WRITE - ready to make a state transition and write
                  the output register
*/

#define NUM_PROC_PHASES 2
#define P_READ 0
#define P_WRITE 1

/* Each processor has a current mode:
        M_READY   - received token and ready to pass it back
        M_WAITING - waiting to receive the token
        M_PASSING - passing the token

   Each processor has an input port register which contains the mode
   of read from the adjacent processor's output port register.
   
*/
#define NUM_PROC_MODES 3
#define M_READY 0
#define M_WAITING 1
#define M_PASSING 2

#define TOTAL_NUM_PROC_STATES \
        (NUM_PROC_PHASES * NUM_PROC_MODES * NUM_PROC_MODES)

/*  
        PROBLEM SPECIFIC HOOKS

    explore.c expects the following to be defined: 
*/

#define NUM_SYS_STATES (TOTAL_NUM_PROC_STATES * TOTAL_NUM_PROC_STATES)

bag_of_bag_of_state_index_t sigma[NUM_SYS_STATES];

int target[NUM_SYS_STATES];

char* state_index_to_str(state_index_t s_i);
int  compute_sigma(void);
int  compute_target(void);