src/xbt/automaton/automaton.c

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