src/xbt/automaton/automaton.c

   1 /* automaton - representation of büchi automaton */
   2
   3 /* Copyright (c) 2011. The SimGrid Team.
   4  * All rights reserved.                                                     */
   5
   6 /* This program is free software; you can redistribute it and/or modify it
   7  * under the terms of the license (GNU LGPL) which comes with this package. */
   8
   9 #include "xbt/automaton.h"
  10
  11 xbt_automaton_t xbt_automaton_new(){
  12   xbt_automaton_t automaton = NULL;
  13   automaton = xbt_new0(struct xbt_automaton, 1);
  14   automaton->states = xbt_dynar_new(sizeof(xbt_state_t), xbt_state_free_voidp);
  15   automaton->transitions = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp);
  16   automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_propositional_symbol_t), xbt_propositional_symbol_free_voidp);
  17   return automaton;
  18 }
  19
  20 xbt_state_t xbt_automaton_new_state(xbt_automaton_t a, int type, char* id){
  21   xbt_state_t state = NULL;
  22   state = xbt_new0(struct xbt_state, 1);
  23   state->type = type;
  24   state->id = strdup(id);
  25   state->in = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp);
  26   state->out = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp);
  27   xbt_dynar_push(a->states, &state);
  28   return state;
  29 }
  30
  31 xbt_transition_t xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst, xbt_exp_label_t label){
  32   xbt_transition_t transition = NULL;
  33   transition = xbt_new0(struct xbt_transition, 1);
  34   if(src != NULL){
  35     xbt_dynar_push(src->out, &transition);
  36     transition->src = src;
  37   }
  38   if(dst != NULL){
  39     xbt_dynar_push(dst->in, &transition);
  40     transition->dst = dst;
  41   }
  42   transition->label = label;
  43   xbt_dynar_push(a->transitions, &transition);
  44   return transition;
  45 }
  46
  47 xbt_exp_label_t xbt_automaton_new_label(int type, ...){
  48   xbt_exp_label_t label = NULL;
  49   label = xbt_new0(struct xbt_exp_label, 1);
  50   label->type = type;
  51
  52   va_list ap;
  53   va_start(ap, type);
  54   switch(type){
  55   case 0 : {
  56     xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
  57     xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
  58     label->u.or_and.left_exp = left;
  59     label->u.or_and.right_exp = right;
  60     break;
  61   }
  62   case 1 : {
  63     xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
  64     xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
  65     label->u.or_and.left_exp = left;
  66     label->u.or_and.right_exp = right;
  67     break;
  68   }
  69   case 2 : {
  70     xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t);
  71     label->u.exp_not = exp_not;
  72     break;
  73   }
  74   case 3 :{
  75     char* p = va_arg(ap, char*);
  76     label->u.predicat = strdup(p);
  77     break;
  78   }
  79   }
  80   va_end(ap);
  81   return label;
  82 }
  83
  84
  85 xbt_dynar_t xbt_automaton_get_states(xbt_automaton_t a){
  86   return a->states;
  87 }
  88
  89 xbt_dynar_t xbt_automaton_get_transitions(xbt_automaton_t a){
  90   return a->transitions;
  91 }
  92
  93 xbt_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst){
  94   xbt_transition_t transition;
  95   unsigned int cursor;
  96   xbt_dynar_foreach(src->out, cursor, transition){
  97     if((transition->src == src) && (transition->dst == dst))
  98       return transition;
  99   }
 100   return NULL;
 101 }
 102
 103 xbt_state_t xbt_automaton_transition_get_source(xbt_transition_t t){
 104   return t->src;
 105 }
 106
 107 xbt_state_t xbt_automaton_transition_get_destination(xbt_transition_t t){
 108   return t->dst;
 109 }
 110
 111 void xbt_automaton_transition_set_source(xbt_transition_t t, xbt_state_t src){
 112   t->src = src;
 113   xbt_dynar_push(src->out,&t);
 114 }
 115
 116 void xbt_automaton_transition_set_destination(xbt_transition_t t, xbt_state_t dst){
 117   t->dst = dst;
 118   xbt_dynar_push(dst->in,&t);
 119 }
 120
 121 xbt_dynar_t xbt_automaton_state_get_out_transitions(xbt_state_t s){
 122   return s->out;
 123 }
 124
 125 xbt_dynar_t xbt_automaton_state_get_in_transitions(xbt_state_t s){
 126   return s->in;
 127 }
 128
 129 xbt_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){
 130   xbt_state_t state = NULL;
 131   unsigned int cursor = 0;
 132   xbt_dynar_foreach(a->states, cursor, state){
 133    if(strcmp(state->id, id)==0)
 134      return state;
 135   }
 136   return NULL;
 137 }
 138
 139 void  xbt_automaton_display(xbt_automaton_t a){
 140   unsigned int cursor = 0;
 141   xbt_state_t state = NULL;
 142
 143   printf("\n\nEtat courant : %s\n", a->current_state->id);
 144
 145   printf("\nListe des états : %lu\n\n", xbt_dynar_length(a->states));
 146
 147
 148   xbt_dynar_foreach(a->states, cursor, state){
 149     printf("ID : %s, type : %d\n", state->id, state->type);
 150   }
 151
 152   cursor=0;
 153   xbt_transition_t transition = NULL;
 154   printf("\nListe des transitions : %lu\n\n", xbt_dynar_length(a->transitions));
 155
 156   xbt_dynar_foreach(a->transitions, cursor, transition){
 157     printf("label :");
 158     xbt_automaton_display_exp(transition->label);
 159     printf(", %s -> %s\n", transition->src->id, transition->dst->id);
 160   }
 161 }
 162
 163 void xbt_automaton_display_exp(xbt_exp_label_t label){
 164
 165   switch(label->type){
 166   case 0 :
 167     printf("(");
 168     xbt_automaton_display_exp(label->u.or_and.left_exp);
 169     printf(" || ");
 170     xbt_automaton_display_exp(label->u.or_and.right_exp);
 171     printf(")");
 172     break;
 173   case 1 :
 174     printf("(");
 175     xbt_automaton_display_exp(label->u.or_and.left_exp);
 176     printf(" && ");
 177     xbt_automaton_display_exp(label->u.or_and.right_exp);
 178     printf(")");
 179     break;
 180   case 2 :
 181     printf("(!");
 182     xbt_automaton_display_exp(label->u.exp_not);
 183     printf(")");
 184     break;
 185   case 3 :
 186     printf("(%s)",label->u.predicat);
 187     break;
 188   case 4 :
 189     printf("(1)");
 190     break;
 191   }
 192
 193 }
 194
 195 xbt_state_t xbt_automaton_get_current_state(xbt_automaton_t a){
 196   return a->current_state;
 197 }
 198
 199 xbt_propositional_symbol_t xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct){
 200   xbt_propositional_symbol_t prop_symb = NULL;
 201   prop_symb = xbt_new0(struct xbt_propositional_symbol, 1);
 202   prop_symb->pred = strdup(id);
 203   prop_symb->function = fct;
 204   xbt_dynar_push(a->propositional_symbols, &prop_symb);
 205   return prop_symb;
 206 }
 207
 208 int automaton_state_compare(xbt_state_t s1, xbt_state_t s2){
 209
 210   /* single id for each state, id and type sufficient for comparison*/
 211
 212   if(strcmp(s1->id, s2->id))
 213     return 1;
 214
 215   if(s1->type != s2->type)
 216     return 1;
 217
 218   return 0;
 219
 220 }
 221
 222 int automaton_transition_compare(const void *t1, const void *t2){
 223
 224   if(automaton_state_compare(((xbt_transition_t)t1)->src, ((xbt_transition_t)t2)->src))
 225     return 1;
 226
 227   if(automaton_state_compare(((xbt_transition_t)t1)->dst, ((xbt_transition_t)t2)->dst))
 228     return 1;
 229
 230   if(automaton_label_transition_compare(((xbt_transition_t)t1)->label,((xbt_transition_t)t2)->label))
 231     return 1;
 232
 233   return 0;
 234
 235 }
 236
 237 int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
 238
 239   if(l1->type != l2->type)
 240     return 1;
 241
 242   switch(l1->type){
 243
 244   case 0 : // OR
 245   case 1 : // AND
 246     if(automaton_label_transition_compare(l1->u.or_and.left_exp, l2->u.or_and.left_exp))
 247       return 1;
 248     else
 249       return automaton_label_transition_compare(l1->u.or_and.right_exp, l2->u.or_and.right_exp);
 250     break;
 251
 252   case 2 : // NOT
 253     return automaton_label_transition_compare(l1->u.exp_not, l2->u.exp_not);
 254     break;
 255
 256   case 3 : // predicat
 257     return (strcmp(l1->u.predicat, l2->u.predicat));
 258     break;
 259
 260   case 4 : // 1
 261     return 0;
 262     break;
 263
 264   default :
 265     return -1;
 266     break;
 267
 268   }
 269
 270 }
 271
 272
 273 int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){
 274
 275   int *iptr1, *iptr2;
 276   unsigned int cursor;
 277   unsigned int nb_elem = xbt_dynar_length(s1);
 278
 279   for(cursor=0;cursor<nb_elem;cursor++){
 280     iptr1 = xbt_dynar_get_ptr(s1, cursor);
 281     iptr2 = xbt_dynar_get_ptr(s2, cursor);
 282     if(*iptr1 != *iptr2)
 283       return 1;
 284   }
 285
 286   return 0;
 287 }
 288
 289 /************ Free functions ****************/
 290
 291 static void xbt_transition_free(xbt_transition_t t);
 292 static void xbt_exp_label_free(xbt_exp_label_t e);
 293 static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps);
 294
 295 void xbt_state_free(xbt_state_t s){
 296   if(s){
 297     xbt_free(s->id);
 298     xbt_dynar_free(&(s->in));
 299     xbt_dynar_free(&(s->out));
 300     xbt_free(s);
 301     s = NULL;
 302   }
 303 }
 304
 305 void xbt_state_free_voidp(void *s){
 306   xbt_state_free((xbt_state_t) * (void **) s);
 307 }
 308
 309 static void xbt_transition_free(xbt_transition_t t){
 310   if(t){
 311     xbt_exp_label_free(t->label);
 312     xbt_free(t);
 313     t = NULL;
 314   }
 315 }
 316
 317 void xbt_transition_free_voidp(void *t){
 318   xbt_transition_free((xbt_transition_t) * (void **) t);
 319 }
 320
 321 static void xbt_exp_label_free(xbt_exp_label_t e){
 322   if(e){
 323     switch(e->type){
 324     case 0:
 325     case 1:
 326       xbt_exp_label_free(e->u.or_and.left_exp);
 327       xbt_exp_label_free(e->u.or_and.right_exp);
 328       break;
 329     case 2:
 330       xbt_exp_label_free(e->u.exp_not);
 331       break;
 332     case 3:
 333       xbt_free(e->u.predicat);
 334       break;
 335     default:
 336       break;
 337     }
 338     xbt_free(e);
 339     e = NULL;
 340   }
 341 }
 342
 343 void xbt_exp_label_free_voidp(void *e){
 344   xbt_exp_label_free((xbt_exp_label_t) * (void **) e);
 345 }
 346
 347 static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps){
 348   if(ps){
 349     xbt_free(ps->pred);
 350     xbt_free(ps);
 351     ps = NULL;
 352   }
 353 }
 354
 355 void xbt_propositional_symbol_free_voidp(void *ps){
 356   xbt_propositional_symbol_free((xbt_propositional_symbol_t) * (void **) ps);
 357 }
 358
 359 void xbt_automaton_free(xbt_automaton_t a){
 360   if(a){
 361     xbt_dynar_free(&(a->propositional_symbols));
 362     xbt_dynar_free(&(a->transitions));
 363     xbt_dynar_free(&(a->states));
 364     xbt_state_free(a->current_state);
 365     xbt_free(a);
 366     a = NULL;
 367   }
 368 }