initial_communications_pattern.resize(maxpid);
incomplete_communications_pattern.resize(maxpid);
- auto initial_state = std::make_unique<State>(++expanded_states_count_);
+ ++expanded_states_count_;
+ auto initial_state = std::make_unique<State>(expanded_states_count_);
XBT_DEBUG("********* Start communication determinism verification *********");
mc_model_checker->wait_for_requests();
/* Create the new expanded state */
- auto next_state = std::make_unique<State>(++expanded_states_count_);
+ ++expanded_states_count_;
+ auto next_state = std::make_unique<State>(expanded_states_count_);
/* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at
* least, data are transferred). These communications are incomplete and they cannot be analyzed and compared
std::shared_ptr<Pair> LivenessChecker::create_pair(const Pair* current_pair, xbt_automaton_state_t state,
std::shared_ptr<const std::vector<int>> propositions)
{
- expanded_pairs_count_++;
+ ++expanded_pairs_count_;
+ ++expanded_states_count_;
auto next_pair = std::make_shared<Pair>(expanded_pairs_count_);
next_pair->automaton_state = state;
- next_pair->graph_state = std::make_shared<State>(++expanded_states_count_);
+ next_pair->graph_state = std::make_shared<State>(expanded_states_count_);
next_pair->atomic_propositions = std::move(propositions);
if (current_pair)
next_pair->depth = current_pair->depth + 1;
this->get_session().execute(state->transition_);
/* Create the new expanded state (copy the state of MCed into our MCer data) */
- auto next_state = std::make_unique<State>(++expanded_states_count_);
+ ++expanded_states_count_;
+ auto next_state = std::make_unique<State>(expanded_states_count_);
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
XBT_DEBUG("Starting the safety algorithm");
- auto initial_state = std::make_unique<State>(++expanded_states_count_);
+ ++expanded_states_count_;
+ auto initial_state = std::make_unique<State>(expanded_states_count_);
XBT_DEBUG("**************************************************");
XBT_DEBUG("Initial state");