model-checker : ddfs stateless and stateful fixed

[simgrid.git] / examples / msg / mc / automatonparse_promela.c

diff --git a/examples/msg/mc/automatonparse_promela.c b/examples/msg/mc/automatonparse_promela.c
index 00678ab..857ff0e 100644 (file)
--- a/examples/msg/mc/automatonparse_promela.c
+++ b/examples/msg/mc/automatonparse_promela.c
@@ -10,10 +10,16 @@ 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
+  int type = 0 ; // -1=état initial, 0=état intermédiaire, 1=état final, 2=état initial/final
 
   if(strcmp(first_part,"accept")==0){
-    type = 1;
+     char* second_part = strtok(NULL,"_");
+     if(strcmp(second_part,"init")==0){
+       type = 2;
+     }else{
+       type = 1;
+     }
+     
   }else{
     char* second_part = strtok(NULL,"_");
     if(strcmp(second_part,"init")==0){
@@ -27,7 +33,7 @@ void new_state(char* id, int src){
     state = xbt_automaton_new_state(automaton, type, id_state);
   }
 
-  if(type==-1)
+  if(type==-1 || type==2)
     automaton->current_state = state;
 
   if(src)