/* **************************************************************
   File    : fsm.h
   Author  : Himanshu A. Sanghavi
   Advisor : Dr. Vijay K. Garg
   Date    : August 1, 1991

   This is the header file for the finite state machine library.
   This file must be included in any file containing a program
   that uses and of the functions of the library.
  
   ************************************************************** */


#include <stdio.h>
#include <string.h>
#include <stdlib.h> /*added for malloc*/
 
/* Define constants TRUE and FALSE to aid readability */
#define FALSE 0
#define TRUE 1

/* Define type BOOLEAN which is used for variables which are 
   either TRUE or FALSE */
#define BOOLEAN char

/* Define the maximum length of any string that can occur in the 
   program.  This parameter should be changed if strings of larger
   or smaller lengths are required */
#define MAX_LENGTH 500


/* **************************************************************
   Enumerated variables defined to aid readability

   The "type" of any transition is either "controllable" or
   "uncontrollable".

   A state is either "marked" or "unmarked" depending upon 
   whether it is a final state or not. 
   *************************************************************** */

enum TYPE {UNCONT, CONT};
enum MRKD {UNMKD, MKD};

/*shouldn't have to do this!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!1*/
struct _masklist {
	char			original[MAX_LENGTH];
	char			masked[MAX_LENGTH];
	struct _masklist 	*next;
};

typedef struct _masklist MASK_LIST;


/*list of mask lists*/
struct mult_masklists{
	MASK_LIST *masklist;
	struct mult_masklists *next;
};

typedef struct mult_masklists MULT_MASKL;

struct _contlist {
	char	event[MAX_LENGTH];
	enum TYPE type;
	struct _contlist	*next;
};

typedef struct _contlist CONT_LIST;


/*list of controllability lists*/
struct mult_contlists{
	CONT_LIST *contlist;
	struct mult_contlists *next;
};

typedef struct mult_contlists MULT_CONTL;


/* *****************************************************************
   The next structure stores information about a transition 
   Its elements store the following information

   input - name of the event triggering the transition
   
   next_state - a pointer to the resultant state
   next - a pointer to the next transition of the current state
   ***************************************************************** */

struct _trlist {
	char		input[MAX_LENGTH];   
	struct _stlist  *next_state; 
	struct _trlist  *next;  
};

typedef struct _trlist TR_LIST;


/* ***************************************************************
   The next structure stores information about a state
   Its elements store the following information

   name - name of the state
   marked - variable to decide whether the state is
            marked or unmarked
   trans - pointer to a linked list of transitions allowed in
           the state 
   next - pointer to the next state of the state machine
   **************************************************************** */

struct _stlist {
	char		name[MAX_LENGTH];
	enum MRKD	marked;
	TR_LIST		*trans;
	struct _stlist  *next;
};

typedef struct _stlist ST_LIST;


/* ***************************************************************
   The next structure stores information about a state machine
   Its elements store the following information

   states - a linked list of states of the state machine
   *************************************************************** */

struct _fsm {
	ST_LIST		*states;
};

typedef struct _fsm FSM;


/* ****************************************************************
   The next structure is used to create a linked list of character
   strings.  This could be names of states or names of transitions.
   Its elements store the following information.

   name - name of the state 
   next - pointer to the next element of the list
   **************************************************************** */
   
struct _namelist {
	char 		   name[MAX_LENGTH];
	struct _namelist   *next;
};

typedef struct _namelist NAME_LIST;

/* Short forms for malloc statements which are frequently used */
#define alloc_state (ST_LIST *) malloc(sizeof(ST_LIST));
#define alloc_trans (TR_LIST *) malloc(sizeof(TR_LIST));

/* Definition of all functions visible to the user of this library */

/* If you compiler accepts function prototypes, use the declerations
   that follow and comment out the declerations at the end of the
   file.  If your compiler does not accept function prototyping, 
   comment out these  declerations and use the declerations without 
   prototypes given at the end of the file */

/* Functions in file "fsm_general.c" */
void fsm_read(FILE*, FSM*);
void fsm_print(FILE*, FSM*);
void fsm_copy(FSM*, FSM*);
void fsm_delete(FSM*);
void fsm_trim(FSM*);
void fsm_rename(FSM*);
void fsm_mask(FILE*, FSM*, FSM*);
void fsm_unmask(FILE*, FSM*, FSM*);


/*VC input alphabet of a FSM		*/
void list_print(FILE*, FSM*);
void exclusive_events(FSM*, FSM*, FILE*);
void complete_fsm_sync_comp(FSM*, FSM*, FSM*);
void multiplefile_complete_fsm_sync_comp(FILE*, FSM*);
void control_AugmentFsm(FILE*, FSM*);
void fsm_trim_sup_cont_sublang(FSM*, FSM*, FSM*, FILE*);



/* Functions in file "fsm_operators.c" */
int fsm_reachability(FSM*, char*, char*, NAME_LIST**);
int fsm_minimize(FSM*);
void fsm_remove_epsilon(FSM*, FSM*);
void fsm_deterministic(FSM*, FSM*);
void fsm_complement(FSM*);
void fsm_sync_comp(FSM*, FSM*, FSM*);
void fsm_union(FSM*, FSM*, FSM*);
void fsm_concatenate(FSM*, FSM*, FSM*);
void fsm_shuffle(FSM*, FSM*, FSM*);
void fsm_quotient(FSM*, FSM*, FSM*);
void fsm_sup_cont_sublang(FSM*, FSM*, FSM*, FILE*);
void fsm_sup_norm_sublang(FILE*, FSM*, FSM*, FSM*);
void fsm_sup_cont_norm_sublang(FILE*, FILE*, FSM*, FSM*, FSM*);



/* Functions in file "fsm_lower.c" */
int get_NTrans(ST_LIST*);
TR_LIST* find_trans(ST_LIST*, char*, char*);
TR_LIST* insert_trans(FSM*, ST_LIST*, char*, char*);
void delete_trans(ST_LIST*, TR_LIST*);
int get_NStates(FSM*);
int get_NBadStates(FSM*);
ST_LIST* find_state(FSM*, char*);
ST_LIST* insert_state(FSM*, char*);
void delete_state(FSM*, ST_LIST*);
int find_name(NAME_LIST*, char*);
void delete_name(NAME_LIST**);
void prog_abort(char*);
void list_print(FILE*, FSM*);



/* All the functions written by Sudhir Nelvagal, to augment the FSM
Library routines */

void CompleteGraph(FILE*, FSM*, FSM*);
void AugmentFsm(FILE*, FSM*);
int SafetyCheck(FSM *);
int SafetyTest(FSM *, FSM *, FILE *, FILE *, FSM *);
void LabelEvents(FSM *, FILE *);
void RelabelEvents(FSM *, FSM *, FSM *);
int ProgressCheck(FSM *, FSM *);
int ProgressTest(FSM *, FSM *, FILE *, FILE *, FSM *, FILE *);
void MarkBadStates(FSM *, ST_LIST *, TR_LIST *);
int Containment(char *[], char *[]);
int FindLabel(char *[], char *);
int ControlCheck(FSM *, FILE *);
int ControlTest(FILE *, FILE *, FILE *);
int BadStates();
int NormalityCheck(FILE *, FILE *, FSM*, FSM*);

MASK_LIST *po_readmask(FILE *);
void po_graph(FSM *, FSM *, FSM *, MULT_MASKL *);
void po_masked_sync_comp(FSM *, FSM *, FSM *, MASK_LIST *);
int po_observability(FSM *, MULT_MASKL *);
MULT_MASKL *po_read_maskl(FILE *);
void po_extract_events(FILE *);
void po_read_cont_file(FILE *, char *[MAX_LENGTH]);
void po_read_cont_file2(FILE *, char *[MAX_LENGTH]);
void po_del_uncontlist(char *[MAX_LENGTH]);
void po_remove_event_temp_files(void);
int po_normality(FSM *, MULT_MASKL *);
void po_delete_mask(MASK_LIST *);
void po_diag_create_pertinent_fsm(FSM *, FSM *);
void po_diag_remove_deadlock(FSM *);
void TEST(FSM *);
void TEST2(FILE *);
int po_diagnosability(FSM *);

