model-checker : add or remove debug information

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

diff --git a/examples/msg/mc/example2_liveness_without_cycle.c b/examples/msg/mc/example2_liveness_without_cycle.c
index 14c54b0..a53a5f7 100644 (file)
--- a/examples/msg/mc/example2_liveness_without_cycle.c
+++ b/examples/msg/mc/example2_liveness_without_cycle.c
@@ -20,7 +20,7 @@ XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "Example liveness with
 extern xbt_automaton_t automaton;
 
 
 extern xbt_automaton_t automaton;
 
 

-int p=1;
+int p=0;

 int q=0;
 
 
 int q=0;
 
 


@@ -51,7 +51,7 @@ int server(int argc, char *argv[])
   val1 = (long) MSG_task_get_data(task1);
   XBT_INFO("Received %lu", val1);
 
   val1 = (long) MSG_task_get_data(task1);
   XBT_INFO("Received %lu", val1);
 

-  //MC_assert_pair_stateless(val1 == 2);
+  MC_assert_pair_stateless(val1 == 2);

 
   /*if(val1 == 2)
     q = 1;
 
   /*if(val1 == 2)
     q = 1;


@@ -90,8 +90,8 @@ int main(int argc, char *argv[])
   init();
   yyparse();
   automaton = get_automaton();
   init();
   yyparse();
   automaton = get_automaton();

-  xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP); 
-  ps = xbt_new_propositional_symbol(automaton,"q", &predQ); 
+  xbt_new_propositional_symbol(automaton,"p", &predP); 
+  xbt_new_propositional_symbol(automaton,"q", &predQ); 

       
   //display_automaton();
 
       
   //display_automaton();