/* Update statistics */
mc_model_checker->visited_states++;
- if (stack_.size() <= (std::size_t)_sg_mc_max_depth && (req = MC_state_get_request(state)) != nullptr &&
- (visited_state == nullptr)) {
+ if (stack_.size() <= (std::size_t)_sg_mc_max_depth)
+ req = MC_state_get_request(state);
+ else
+ req = nullptr;
+
+ if (req != nullptr && visited_state == nullptr) {
int req_num = state->transition.argument;
* with the initial pattern. */
bool compare_snapshots = all_communications_are_finished() && this->initial_communications_pattern_done;
- if (_sg_mc_max_visited_states == 0 ||
- (visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots)) ==
- nullptr) {
+ if (_sg_mc_max_visited_states != 0)
+ visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots);
+ else
+ visited_state = nullptr;
+
+ if (visited_state == nullptr) {
/* Get enabled actors and insert them in the interleave set of the next state */
for (auto& actor : mc_model_checker->process().actors())
}
std::shared_ptr<VisitedPair> reached_pair;
- if (current_pair->automaton_state->type == 1 && not current_pair->exploration_started &&
- (reached_pair = this->insertAcceptancePair(current_pair.get())) == nullptr) {
- this->showAcceptanceCycle(current_pair->depth);
- throw simgrid::mc::LivenessError();
+ if (current_pair->automaton_state->type == 1 && not current_pair->exploration_started) {
+ reached_pair = this->insertAcceptancePair(current_pair.get());
+ if (reached_pair == nullptr) {
+ this->showAcceptanceCycle(current_pair->depth);
+ throw simgrid::mc::LivenessError();
+ }
}
/* Pair already visited ? stop the exploration on the current path */
int visited_num = -1;
- if ((not current_pair->exploration_started) &&
- (visited_num = this->insertVisitedPair(reached_pair, current_pair.get())) != -1) {
- if (dot_output != nullptr){
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
- this->previousPair_, visited_num,
- this->previousRequest_.c_str());
- fflush(dot_output);
+ if (not current_pair->exploration_started) {
+ visited_num = this->insertVisitedPair(reached_pair, current_pair.get());
+ if (visited_num != -1) {
+ if (dot_output != nullptr) {
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", this->previousPair_, visited_num,
+ this->previousRequest_.c_str());
+ fflush(dot_output);
+ }
+ XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
+ current_pair->requests = 0;
+ this->backtrack();
+ continue;
}
- XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
- current_pair->requests = 0;
- this->backtrack();
- continue;
}
smx_simcall_t req = MC_state_get_request(current_pair->graph_state.get());
/* xbt_os_file.c -- portable interface to file-related functions */
-/* Copyright (c) 2007-2010, 2012-2015. The SimGrid Team.
+/* Copyright (c) 2007-2010, 2012-2017. The SimGrid Team.
* All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
}
(*buf)[i] = ch;
i++;
- } while (ch != '\n' && (ch = getc(stream)) != EOF);
+ if (ch == '\n')
+ break;
+ } while ((ch = getc(stream)) != EOF);
if (i == *n) {
*n += 1;