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;