From beec1389e9398a7d088835d1a841b89a1e54c925 Mon Sep 17 00:00:00 2001
From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Tue, 25 Oct 2011 13:21:28 +0200
Subject: [PATCH] model-checker : function to compare propositional symbol
 values

---
 src/mc/mc_liveness.c | 9 ++++-----
 src/xbt/automaton.c  | 7 ++++++-
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 480358ff7d..f04cb31b8d 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -76,17 +76,16 @@ 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;
-      int res = (*f)();
+      const int res = (*f)();
       xbt_dynar_push(pair->prop_ato, &res);
     }
     
     cursor = 0;
     mc_pair_reached_t pair_test;
-    int (*compare_dynar)(const void*; const void*) = propositional_symbols_compare;
-    
+    //int (*compare_dynar)(const void*, const void*) = &propositional_symbols_compare_value;
     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
       if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
-	if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, compare_dynar) == 0){
+	if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, propositional_symbols_compare_value) == 0){
 	  if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){
 	    MC_UNSET_RAW_MEM;
 	    return 1;
@@ -110,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;
-    pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+    pair->prop_ato = xbt_dynar_new(sizeof(const int), NULL);
     pair->system_state = s;
     
     /* Get values of propositional symbols */
diff --git a/src/xbt/automaton.c b/src/xbt/automaton.c
index e9f4f02787..85ba9896a9 100644
--- a/src/xbt/automaton.c
+++ b/src/xbt/automaton.c
@@ -343,6 +343,11 @@ 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){
 
-  return (!(s1 == s2));
+  const int *ps1 = s1;
+  const int *ps2 = s2;
+  printf("ps 1 = %d, ps2 = %d", *ps1, *ps2);
+
+  //return (!(*ps1 == *ps2));
+  return 0;
 
 }
-- 
2.20.1