From 99cbb45d8f0ab2de02d0ef46a75e17f7cf57c466 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 4 Jun 2014 17:15:21 +0200 Subject: [PATCH] model-checker : use new variable _sg_mc_liveness instead of _sg_mc_property_file --- src/mc/mc_compare.c | 9 ++------- src/mc/mc_global.c | 3 +-- 2 files changed, 3 insertions(+), 9 deletions(-) diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 7042a5854b..69176ea285 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -414,17 +414,12 @@ int snapshot_compare(void *state1, void *state2) mc_snapshot_t s1, s2; int num1, num2; - if (_sg_mc_property_file && _sg_mc_property_file[0] != '\0') { /* Liveness MC */ + if (_sg_mc_liveness) { /* Liveness MC */ s1 = ((mc_visited_pair_t) state1)->graph_state->system_state; s2 = ((mc_visited_pair_t) state2)->graph_state->system_state; num1 = ((mc_visited_pair_t) state1)->num; num2 = ((mc_visited_pair_t) state2)->num; - /* Firstly compare automaton state */ - /*if(xbt_automaton_state_compare(((mc_pair_t)state1)->automaton_state, ((mc_pair_t)state2)->automaton_state) != 0) - return 1; - if(xbt_automaton_propositional_symbols_compare_value(((mc_pair_t)state1)->atomic_propositions, ((mc_pair_t)state2)->atomic_propositions) != 0) - return 1; */ - } else { /* Safety MC */ + } else { /* Safety or comm determinism MC */ s1 = ((mc_visited_state_t) state1)->system_state; s2 = ((mc_visited_state_t) state2)->system_state; num1 = ((mc_visited_state_t) state1)->num; diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 809f87797a..a3de319ea1 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -249,8 +249,7 @@ void MC_init() MC_SET_STD_HEAP; - if (_sg_mc_visited > 0 - || (_sg_mc_property_file && _sg_mc_property_file[0] != '\0')) { + if (_sg_mc_visited > 0 || _sg_mc_liveness) { /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ MC_ignore_local_variable("e", "*"); MC_ignore_local_variable("__ex_cleanup", "*"); -- 2.20.1