From 9e890be0084b31677be60ce7e379294971782bb2 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 21 Apr 2011 10:10:51 +0200 Subject: [PATCH] new struct automaton --- include/xbt/automaton.h | 103 ++++++++++ include/xbt/automatonparse_promela.h | 24 +++ src/xbt/automaton.c | 278 +++++++++++++++++++++++++++ src/xbt/automatonparse_promela.c | 92 +++++++++ 4 files changed, 497 insertions(+) create mode 100644 include/xbt/automaton.h create mode 100644 include/xbt/automatonparse_promela.h create mode 100644 src/xbt/automaton.c create mode 100644 src/xbt/automatonparse_promela.c diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h new file mode 100644 index 0000000000..a91f8ab16e --- /dev/null +++ b/include/xbt/automaton.h @@ -0,0 +1,103 @@ +#ifndef _XBT_AUTOMATON_H +#define _XBT_AUTOMATON_H + +#include +#include +#include "xbt/dynar.h" +#include "xbt/sysdep.h" + +SG_BEGIN_DECL() + +typedef struct xbt_state { + char* id; + int type; /* -1 = init, 0 = inter, 1 = final */ + xbt_dynar_t in; + xbt_dynar_t out; + int visited; +} s_xbt_state; + +typedef struct xbt_state* xbt_state_t; + +typedef struct xbt_automaton { + xbt_dynar_t propositional_symbols; + xbt_dynar_t transitions; + xbt_dynar_t states; + xbt_state_t current_state; +} s_xbt_automaton; + +typedef struct xbt_automaton* xbt_automaton_t; + +typedef struct xbt_exp_label{ + enum{or=0, and=1, not=2, predicat=3, one=4} type; + union{ + struct{ + struct xbt_exp_label* left_exp; + struct xbt_exp_label* right_exp; + }or_and; + struct xbt_exp_label* exp_not; + char* predicat; + }u; +} s_xbt_exp_label; + +typedef struct xbt_exp_label* xbt_exp_label_t; + +typedef struct xbt_transition { + xbt_state_t src; + xbt_state_t dst; + xbt_exp_label_t label; +} s_xbt_transition; + + +typedef struct xbt_transition* xbt_transition_t; + +typedef struct xbt_propositional_symbol{ + char* pred; + void* function; +} s_xbt_propositional_symbol; + +typedef struct xbt_propositional_symbol* xbt_propositional_symbol_t; + + +XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new_automaton(); + +XBT_PUBLIC(xbt_state_t) xbt_automaton_new_state(xbt_automaton_t a, int type, char* id); + +XBT_PUBLIC(xbt_transition_t) xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst, xbt_exp_label_t label); + +XBT_PUBLIC(xbt_exp_label_t) xbt_automaton_new_label(int type, ...); + +XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_states(xbt_automaton_t a); + +XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_transitions(xbt_automaton_t a); + +XBT_PUBLIC(xbt_transition_t) xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst); + +XBT_PUBLIC(void) xbt_automaton_free_automaton(xbt_automaton_t a, void_f_pvoid_t transition_free_function); + +XBT_PUBLIC(void) xbt_automaton_free_state(xbt_automaton_t a, xbt_state_t s, void_f_pvoid_t transition_free_function); + +XBT_PUBLIC(void) xbt_automaton_free_transition(xbt_automaton_t a, xbt_transition_t t, void_f_pvoid_t transition_free_function); + +XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_source(xbt_transition_t t); + +XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_destination(xbt_transition_t t); + +XBT_PUBLIC(void) xbt_automaton_transition_set_source(xbt_transition_t t, xbt_state_t src); + +XBT_PUBLIC(void) xbt_automaton_transition_set_destination(xbt_transition_t t, xbt_state_t dst); + +XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_out_transitions(xbt_state_t s); + +XBT_PUBLIC(xbt_dynar_t) xbt_automaton_state_get_in_transitions(xbt_state_t s); + +XBT_PUBLIC(xbt_state_t) xbt_automaton_state_exists(xbt_automaton_t a, char *id); + +XBT_PUBLIC(void) xbt_automaton_display(xbt_automaton_t a); + +XBT_PUBLIC(void) xbt_automaton_display_exp(xbt_exp_label_t l); + +XBT_PUBLIC(xbt_propositional_symbol_t) xbt_new_propositional_symbol(xbt_automaton_t a, char* id, void* fct); + +SG_END_DECL() + +#endif diff --git a/include/xbt/automatonparse_promela.h b/include/xbt/automatonparse_promela.h new file mode 100644 index 0000000000..edcad66760 --- /dev/null +++ b/include/xbt/automatonparse_promela.h @@ -0,0 +1,24 @@ +#ifndef _XBT_AUTOMATONPARSE_PROMELA_H +#define _XBT_AUTOMATONPARSE_PROMELA_H + +#include +#include +#include "xbt/automaton.h" + +xbt_automaton_t automaton; + +SG_BEGIN_DECL() + +XBT_PUBLIC(void) init(); + +XBT_PUBLIC(void) new_state(char* id, int src); + +XBT_PUBLIC(void) new_transition(char* id, xbt_exp_label_t label); + +XBT_PUBLIC(xbt_exp_label_t) new_label(int type, ...); + +XBT_PUBLIC(xbt_automaton_t) get_automaton(); + +SG_END_DECL() + +#endif diff --git a/src/xbt/automaton.c b/src/xbt/automaton.c new file mode 100644 index 0000000000..436e293d29 --- /dev/null +++ b/src/xbt/automaton.c @@ -0,0 +1,278 @@ +#include "xbt/automaton.h" + +xbt_automaton_t xbt_automaton_new_automaton(){ + xbt_automaton_t automaton = NULL; + automaton = xbt_new0(struct xbt_automaton, 1); + automaton->states = xbt_dynar_new(sizeof(xbt_state_t), NULL); + automaton->transitions = xbt_dynar_new(sizeof(xbt_transition_t), NULL); + automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_propositional_symbol_t), NULL); + return automaton; +} + +xbt_state_t xbt_automaton_new_state(xbt_automaton_t a, int type, char* id){ + xbt_state_t state = NULL; + state = xbt_new0(struct xbt_state, 1); + state->visited = 0; + state->type = type; + state->id = strdup(id); + state->in = xbt_dynar_new(sizeof(xbt_transition_t), NULL); + state->out = xbt_dynar_new(sizeof(xbt_transition_t), NULL); + xbt_dynar_push(a->states, &state); + return state; +} + +xbt_transition_t xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst, xbt_exp_label_t label){ + xbt_transition_t transition = NULL; + transition = xbt_new0(struct xbt_transition, 1); + if(src != NULL){ + xbt_dynar_push(src->out, &transition); + transition->src = src; + } + if(dst != NULL){ + xbt_dynar_push(dst->in, &transition); + transition->dst = dst; + } + transition->label = label; + xbt_dynar_push(a->transitions, &transition); + return transition; +} + +xbt_exp_label_t xbt_automaton_new_label(int type, ...){ + xbt_exp_label_t label = NULL; + label = xbt_new0(struct xbt_exp_label, 1); + label->type = type; + + va_list ap; + va_start(ap, type); + switch(type){ + case 0 : { + xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t); + xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t); + label->u.or_and.left_exp = left; + label->u.or_and.right_exp = right; + break; + } + case 1 : { + xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t); + xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t); + label->u.or_and.left_exp = left; + label->u.or_and.right_exp = right; + break; + } + case 2 : { + xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t); + label->u.exp_not = exp_not; + break; + } + case 3 :{ + char* p = va_arg(ap, char*); + label->u.predicat = strdup(p); + break; + } + } + va_end(ap); + return label; +} + + +xbt_dynar_t xbt_automaton_get_states(xbt_automaton_t a){ + return a->states; +} + +xbt_dynar_t xbt_automaton_get_transitions(xbt_automaton_t a){ + return a->transitions; +} + +xbt_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst){ + xbt_transition_t transition; + unsigned int cursor; + xbt_dynar_foreach(src->out, cursor, transition){ + if((transition->src == src) && (transition->dst == dst)) + return transition; + } + return NULL; +} + +void xbt_automaton_free_automaton(xbt_automaton_t a, void_f_pvoid_t transition_free_function){ + unsigned int cursor = 0; + xbt_state_t state = NULL; + xbt_transition_t transition = NULL; + + xbt_dynar_foreach(a->states, cursor, state){ + xbt_dynar_free(&(state->out)); + xbt_dynar_free(&(state->in)); + } + + xbt_dynar_foreach(a->transitions, cursor, transition){ + if(transition_free_function) + (*transition_free_function) (transition->label); + } + + xbt_dynar_foreach(a->states, cursor, state) + free(state); + xbt_dynar_free(&(a->states)); + + xbt_dynar_foreach(a->transitions, cursor, state) + free(transition); + xbt_dynar_free(&(a->transitions)); + + free(a); + + return; +} + +void xbt_automaton_free_state(xbt_automaton_t a, xbt_state_t s, void_f_pvoid_t transition_free_function){ + unsigned long nbr; + unsigned long i; + unsigned int cursor = 0; + xbt_state_t state = NULL; + xbt_transition_t transition = NULL; + + nbr = xbt_dynar_length(a->transitions); + for(i = 0; i transitions, cursor, &transition); + if((transition->src == s) || (transition->dst == s)){ + xbt_automaton_free_transition(a, transition, transition_free_function); + }else{ + cursor++; + } + } + + cursor = 0; + xbt_dynar_foreach(a->states, cursor, state) + if(state == s) + xbt_dynar_cursor_rm(a->states, &cursor); + + xbt_dynar_free(&(s->in)); + xbt_dynar_free(&(s->out)); + + free(s); + + return; +} + +void xbt_automaton_free_transition(xbt_automaton_t a, xbt_transition_t t, void_f_pvoid_t transition_free_function){ + int index; + unsigned int cursor = 0; + xbt_transition_t transition = NULL; + + if((transition_free_function) && (t->label)) + (*transition_free_function) (t->label); + + xbt_dynar_foreach(a->transitions, cursor, transition) { + if(transition == t){ + index = __xbt_find_in_dynar(transition->dst->in, transition); + xbt_dynar_remove_at(transition->dst->in, index, NULL); + index = __xbt_find_in_dynar(transition->src->out, transition); + xbt_dynar_remove_at(transition->src->out, index, NULL); + xbt_dynar_cursor_rm(a->transitions, & cursor); + free(transition); + break; + } + } +} + +xbt_state_t xbt_automaton_transition_get_source(xbt_transition_t t){ + return t->src; +} + +xbt_state_t xbt_automaton_transition_get_destination(xbt_transition_t t){ + return t->dst; +} + +void xbt_automaton_transition_set_source(xbt_transition_t t, xbt_state_t src){ + t->src = src; + xbt_dynar_push(src->out,&t); +} + +void xbt_automaton_transition_set_destination(xbt_transition_t t, xbt_state_t dst){ + t->dst = dst; + xbt_dynar_push(dst->in,&t); +} + +xbt_dynar_t xbt_automaton_state_get_out_transitions(xbt_state_t s){ + return s->out; +} + +xbt_dynar_t xbt_automaton_state_get_in_transitions(xbt_state_t s){ + return s->in; +} + +xbt_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){ + xbt_state_t state = NULL; + unsigned int cursor = 0; + xbt_dynar_foreach(a->states, cursor, state){ + if(strcmp(state->id, id)==0) + return state; + } + return NULL; +} + +void xbt_automaton_display(xbt_automaton_t a){ + unsigned int cursor = 0; + xbt_state_t state = NULL; + + printf("\n\nEtat courant : %s\n", a->current_state->id); + + printf("\nListe des états : %lu\n\n", xbt_dynar_length(a->states)); + + + xbt_dynar_foreach(a->states, cursor, state){ + printf("ID : %s, type : %d\n", state->id, state->type); + } + + cursor=0; + xbt_transition_t transition = NULL; + printf("\nListe des transitions : %lu\n\n", xbt_dynar_length(a->transitions)); + + xbt_dynar_foreach(a->transitions, cursor, transition){ + printf("label :"); + xbt_automaton_display_exp(transition->label); + printf(", %s -> %s\n", transition->src->id, transition->dst->id); + } +} + +void xbt_automaton_display_exp(xbt_exp_label_t label){ + + switch(label->type){ + case 0 : + printf("("); + xbt_automaton_display_exp(label->u.or_and.left_exp); + printf(" || "); + xbt_automaton_display_exp(label->u.or_and.right_exp); + printf(")"); + break; + case 1 : + printf("("); + xbt_automaton_display_exp(label->u.or_and.left_exp); + printf(" && "); + xbt_automaton_display_exp(label->u.or_and.right_exp); + printf(")"); + break; + case 2 : + printf("(!"); + xbt_automaton_display_exp(label->u.exp_not); + printf(")"); + break; + case 3 : + printf("(%s)",label->u.predicat); + break; + case 4 : + printf("(1)"); + break; + } + +} + +xbt_state_t xbt_automaton_get_current_state(xbt_automaton_t a){ + return a->current_state; +} + +xbt_propositional_symbol_t xbt_new_propositional_symbol(xbt_automaton_t a, char* id, void* fct){ + xbt_propositional_symbol_t prop_symb = NULL; + prop_symb = xbt_new0(struct xbt_propositional_symbol, 1); + prop_symb->pred = strdup(id); + prop_symb->function = fct; + xbt_dynar_push(a->propositional_symbols, &prop_symb); + return prop_symb; +} diff --git a/src/xbt/automatonparse_promela.c b/src/xbt/automatonparse_promela.c new file mode 100644 index 0000000000..6159835829 --- /dev/null +++ b/src/xbt/automatonparse_promela.c @@ -0,0 +1,92 @@ +#include "xbt/automatonparse_promela.h" + +char* state_id_src; + +void init(){ + automaton = xbt_automaton_new_automaton(); +} + +void new_state(char* id, int src){ + + char* id_state = strdup(id); + char* first_part = strtok(id,"_"); + int type = 0 ; // -1=état initial, 0=état intermédiaire, 1=état final + + if(strcmp(first_part,"accept")==0){ + type = 1; + }else{ + char* second_part = strtok(NULL,"_"); + if(strcmp(second_part,"init")==0){ + type = -1; + } + } + + xbt_state_t state = NULL; + state = xbt_automaton_state_exists(automaton, id_state); + if(state == NULL){ + state = xbt_automaton_new_state(automaton, type, id_state); + } + + if(type==-1) + automaton->current_state = state; + + if(src) + state_id_src = strdup(id_state); + +} + +void new_transition(char* id, xbt_exp_label_t label){ + + char* id_state = strdup(id); + xbt_state_t state_dst = NULL; + new_state(id, 0); + state_dst = xbt_automaton_state_exists(automaton, id_state); + xbt_state_t state_src = xbt_automaton_state_exists(automaton, state_id_src); + + xbt_transition_t trans = NULL; + trans = xbt_automaton_new_transition(automaton, state_src, state_dst, label); + +} + +xbt_exp_label_t new_label(int type, ...){ + xbt_exp_label_t label = NULL; + va_list ap; + va_start(ap,type); + switch(type){ + case 0 : { + xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t); + xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t); + label = xbt_automaton_new_label(type, left, right); + break; + } + case 1 : { + xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t); + xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t); + label = xbt_automaton_new_label(type, left, right); + break; + } + case 2 : { + xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t); + label = xbt_automaton_new_label(type, exp_not); + break; + } + case 3 : { + char* p = va_arg(ap, char*); + label = xbt_automaton_new_label(type, p); + break; + } + case 4 : { + label = xbt_automaton_new_label(type); + break; + } + } + va_end(ap); + return label; +} + +xbt_automaton_t get_automaton(){ + return automaton; +} + + + -- 2.20.1