X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/517f86be9ef7be0099cc50dfd103786fc80552d1..2b32f4ae7739666694f8f27ff5122c829daa94dc:/src/mc/LivenessChecker.cpp

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index fcf0ed3b1e..cc3ae5dc8d 100644
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -33,8 +33,6 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
 
-/********* Global variables *********/
-
 /********* Static functions *********/
 
 namespace simgrid {
@@ -59,7 +57,6 @@ VisitedPair::VisitedPair(
   this->automaton_state = automaton_state;
   this->num = pair_num;
   this->other_num = -1;
-  this->acceptance_pair = 0;
   this->atomic_propositions = atomic_propositions;
 }
 
@@ -73,26 +70,26 @@ static int MC_automaton_evaluate_label(
 {
 
   switch (l->type) {
-  case 0:{
+  case xbt_automaton_exp_label::AUT_OR:{
       int left_res = MC_automaton_evaluate_label(
         l->u.or_and.left_exp, atomic_propositions_values);
       int right_res = MC_automaton_evaluate_label(
         l->u.or_and.right_exp, atomic_propositions_values);
       return (left_res || right_res);
     }
-  case 1:{
+  case xbt_automaton_exp_label::AUT_AND:{
       int left_res = MC_automaton_evaluate_label(
         l->u.or_and.left_exp, atomic_propositions_values);
       int right_res = MC_automaton_evaluate_label(
         l->u.or_and.right_exp, atomic_propositions_values);
       return (left_res && right_res);
     }
-  case 2:{
+  case xbt_automaton_exp_label::AUT_NOT:{
       int res = MC_automaton_evaluate_label(
         l->u.exp_not, atomic_propositions_values);
       return (!res);
     }
-  case 3:{
+  case xbt_automaton_exp_label::AUT_PREDICAT:{
       unsigned int cursor = 0;
       xbt_automaton_propositional_symbol_t p = nullptr;
       xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
@@ -101,7 +98,7 @@ static int MC_automaton_evaluate_label(
       }
       return -1;
     }
-  case 4:
+  case xbt_automaton_exp_label::AUT_ONE:
     return 2;
   default:
     return -1;
@@ -137,12 +134,11 @@ std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::
   std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(
     pair->num, pair->automaton_state, pair->atomic_propositions,
     pair->graph_state);
-  new_pair->acceptance_pair = 1;
 
   auto res = std::equal_range(acceptancePairs_.begin(), acceptancePairs_.end(),
     new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 
-  if (pair->search_cycle == 1)
+  if (pair->search_cycle)
     for (auto i = res.first; i != res.second; ++i) {
       std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
       if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) {
@@ -197,7 +193,7 @@ void LivenessChecker::prepare(void)
           MC_state_interleave_process(initial_pair->graph_state.get(), &p.copy);
 
       initial_pair->requests = MC_state_interleave_size(initial_pair->graph_state.get());
-      initial_pair->search_cycle = 0;
+      initial_pair->search_cycle = false;
 
       livenessStack_.push_back(initial_pair);
     }
@@ -400,7 +396,7 @@ int LivenessChecker::main(void)
 
     if (current_pair->requests > 0) {
 
-      if (current_pair->automaton_state->type == 1 && current_pair->exploration_started == 0) {
+      if (current_pair->automaton_state->type == 1 && !current_pair->exploration_started) {
         /* If new acceptance pair, return new pair */
         if ((reached_pair = this->insertAcceptancePair(current_pair)) == nullptr) {
           this->showAcceptanceCycle(current_pair->depth);
@@ -409,7 +405,7 @@ int LivenessChecker::main(void)
       }
 
       /* Pair already visited ? stop the exploration on the current path */
-      if ((current_pair->exploration_started == 0)
+      if ((!current_pair->exploration_started)
         && (visited_num = this->insertVisitedPair(
           reached_pair, current_pair)) != -1) {
 
@@ -447,7 +443,7 @@ int LivenessChecker::main(void)
 
          /* Update mc_stats */
          mc_stats->executed_transitions++;
-         if(current_pair->exploration_started == 0)
+         if (!current_pair->exploration_started)
            mc_stats->visited_pairs++;
 
          /* Answer the request */
@@ -457,7 +453,7 @@ int LivenessChecker::main(void)
          mc_model_checker->wait_for_requests();
 
          current_pair->requests--;
-         current_pair->exploration_started = 1;
+         current_pair->exploration_started = true;
 
          /* Get values of atomic propositions (variables used in the property formula) */
          std::vector<int> prop_values = this->getPropositionValues();
@@ -482,7 +478,7 @@ int LivenessChecker::main(void)
 
               /* FIXME : get search_cycle value for each acceptant state */
               if (next_pair->automaton_state->type == 1 || current_pair->search_cycle)
-                next_pair->search_cycle = 1;
+                next_pair->search_cycle = true;
 
               /* Add new pair to the exploration stack */
               livenessStack_.push_back(next_pair);
@@ -536,7 +532,6 @@ int LivenessChecker::run()
   mc_model_checker->wait_for_requests();
 
   XBT_DEBUG("Starting the liveness algorithm");
-  _sg_mc_liveness = 1;
 
   /* Create the initial state */
   simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());