model-checker : remove unused variables

diff --git a/examples/msg/mc/automaton.c b/examples/msg/mc/automaton.c
index 46d06fa..b2e3ae3 100644 (file)
--- a/examples/msg/mc/automaton.c
+++ b/examples/msg/mc/automaton.c
@@ -343,6 +343,10 @@ int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
 
 int propositional_symbols_compare_value(const void *s1, const void *s2){
 
 
 int propositional_symbols_compare_value(const void *s1, const void *s2){
 

-  return (!((int)s1 == (int)s2));
+  const int *ps1 = s1;
+  const int *ps2 = s2;
+  printf("ps 1 = %d, ps2 = %d", *ps1, *ps2);
+
+  return (!(*ps1 == *ps2));

 
 }
 
 }

diff --git a/examples/msg/mc/automatonparse_promela.c b/examples/msg/mc/automatonparse_promela.c
index 6159835..88c2caf 100644 (file)
--- a/examples/msg/mc/automatonparse_promela.c
+++ b/examples/msg/mc/automatonparse_promela.c
@@ -43,8 +43,8 @@ void new_transition(char* id, xbt_exp_label_t label){
   state_dst = xbt_automaton_state_exists(automaton, id_state);
   xbt_state_t state_src = xbt_automaton_state_exists(automaton, state_id_src); 
   
   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_transition_t trans = NULL;
+  xbt_automaton_new_transition(automaton, state_src, state_dst, label);

 
 }
 
 
 }
 

diff --git a/examples/msg/mc/example2_liveness_without_cycle.c b/examples/msg/mc/example2_liveness_without_cycle.c
index 519933c..a53a5f7 100644 (file)
--- a/examples/msg/mc/example2_liveness_without_cycle.c
+++ b/examples/msg/mc/example2_liveness_without_cycle.c
@@ -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();
 

diff --git a/examples/msg/mc/example_liveness_with_cycle.c b/examples/msg/mc/example_liveness_with_cycle.c
index 09deb12..17982c0 100644 (file)
--- a/examples/msg/mc/example_liveness_with_cycle.c
+++ b/examples/msg/mc/example_liveness_with_cycle.c
@@ -127,8 +127,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); 

   
   MSG_global_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   
   MSG_global_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");

diff --git a/examples/msg/mc/example_liveness_without_cycle.c b/examples/msg/mc/example_liveness_without_cycle.c
index a43f7c8..11983b9 100644 (file)
--- a/examples/msg/mc/example_liveness_without_cycle.c
+++ b/examples/msg/mc/example_liveness_without_cycle.c
@@ -74,9 +74,9 @@ 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,"r", &predR); 
-  ps = xbt_new_propositional_symbol(automaton,"e", &predE);
-  ps = xbt_new_propositional_symbol(automaton,"d", &predD);
+  xbt_new_propositional_symbol(automaton,"r", &predR); 
+  xbt_new_propositional_symbol(automaton,"e", &predE);
+  xbt_new_propositional_symbol(automaton,"d", &predD);

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

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index f04cb31..14b385e 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -76,7 +76,7 @@ int reached(xbt_automaton_t a, mc_snapshot_t s){
     xbt_propositional_symbol_t ps = NULL;
     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
       int (*f)() = ps->function;
     xbt_propositional_symbol_t ps = NULL;
     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
       int (*f)() = ps->function;

-      const int res = (*f)();
+      int res = (*f)();

       xbt_dynar_push(pair->prop_ato, &res);
     }
     
       xbt_dynar_push(pair->prop_ato, &res);
     }
     


@@ -109,7 +109,7 @@ int set_pair_reached(xbt_automaton_t a, mc_snapshot_t s){
     mc_pair_reached_t pair = NULL;
     pair = xbt_new0(s_mc_pair_reached_t, 1);
     pair->automaton_state = a->current_state;
     mc_pair_reached_t pair = NULL;
     pair = xbt_new0(s_mc_pair_reached_t, 1);
     pair->automaton_state = a->current_state;

-    pair->prop_ato = xbt_dynar_new(sizeof(const int), NULL);
+    pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);

     pair->system_state = s;
     
     /* Get values of propositional symbols */
     pair->system_state = s;
     
     /* Get values of propositional symbols */

diff --git a/src/xbt/automaton.c b/src/xbt/automaton.c
index 85ba989..b2e3ae3 100644 (file)
--- a/src/xbt/automaton.c
+++ b/src/xbt/automaton.c
@@ -347,7 +347,6 @@ int propositional_symbols_compare_value(const void *s1, const void *s2){
   const int *ps2 = s2;
   printf("ps 1 = %d, ps2 = %d", *ps1, *ps2);
 
   const int *ps2 = s2;
   printf("ps 1 = %d, ps2 = %d", *ps1, *ps2);
 

-  //return (!(*ps1 == *ps2));
-  return 0;
+  return (!(*ps1 == *ps2));

 
 }
 
 }

diff --git a/src/xbt/automatonparse_promela.c b/src/xbt/automatonparse_promela.c
index 6159835..88c2caf 100644 (file)
--- a/src/xbt/automatonparse_promela.c
+++ b/src/xbt/automatonparse_promela.c
@@ -43,8 +43,8 @@ void new_transition(char* id, xbt_exp_label_t label){
   state_dst = xbt_automaton_state_exists(automaton, id_state);
   xbt_state_t state_src = xbt_automaton_state_exists(automaton, state_id_src); 
   
   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_transition_t trans = NULL;
+  xbt_automaton_new_transition(automaton, state_src, state_dst, label);

 
 }
 
 
 }