extern XBT_PRIVATE char* _sg_mc_dot_output_file;
extern XBT_PUBLIC(int) _sg_mc_comms_determinism;
extern XBT_PUBLIC(int) _sg_mc_send_determinism;
-extern XBT_PRIVATE int _sg_mc_safety;
extern XBT_PRIVATE int _sg_mc_liveness;
extern XBT_PRIVATE int _sg_mc_snapshot_fds;
extern XBT_PRIVATE int _sg_mc_termination;
return SIMGRID_MC_EXIT_NON_TERMINATION;
}
- if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) {
+ if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
for (auto& p : mc_model_checker->process().simix_processes())
else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
reductionMode_ = simgrid::mc::ReductionMode::dpor;
- _sg_mc_safety = 1;
-
if (_sg_mc_termination)
XBT_INFO("Check non progressive cycles");
else
xbt_fifo_unshift(mc_stack, initial_state);
}
+static inline
+bool all_communications_are_finished()
+{
+ for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
+ xbt_dynar_t pattern = xbt_dynar_get_as(
+ incomplete_communications_pattern, current_process, xbt_dynar_t);
+ if (!xbt_dynar_is_empty(pattern)) {
+ XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
+ return false;
+ }
+ }
+ return true;
+}
+
static int MC_modelcheck_comm_determinism_main(void)
{
/* Create the new expanded state */
next_state = MC_state_new();
- if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) {
+ /* If comm determinism verification, we cannot stop the exploration if
+ some communications are not finished (at least, data are transfered).
+ These communications are incomplete and they cannot be analyzed and
+ compared with the initial pattern. */
+ bool compare_snapshots = all_communications_are_finished()
+ && initial_global_state->initial_communications_pattern_done;
+
+ if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, compare_snapshots)) == nullptr) {
/* Get enabled processes and insert them in the interleave set of the next state */
for (auto& p : mc_model_checker->process().simix_processes())
char *_sg_mc_dot_output_file = nullptr;
int _sg_mc_comms_determinism = 0;
int _sg_mc_send_determinism = 0;
-int _sg_mc_safety = 0;
int _sg_mc_liveness = 0;
int _sg_mc_snapshot_fds = 0;
int _sg_mc_termination = 0;
};
extern XBT_PRIVATE std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
-XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state);
+XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state, bool compare_snpashots);
XBT_PRIVATE int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2);
}
MC_state_delete(this->graph_state, 1);
}
-}
-}
-
-static
-bool some_communications_are_not_finished()
-{
- for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
- xbt_dynar_t pattern = xbt_dynar_get_as(
- incomplete_communications_pattern, current_process, xbt_dynar_t);
- if (!xbt_dynar_is_empty(pattern)) {
- XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
- return true;
- }
- }
- return false;
-}
-
-namespace simgrid {
-namespace mc {
-
static void prune_visited_states()
{
while (visited_states.size() > (std::size_t) _sg_mc_visited) {
/**
* \brief Checks whether a given state has already been visited by the algorithm.
*/
-std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state)
+std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state, bool compare_snpashots)
{
- if (_sg_mc_visited == 0)
- return nullptr;
- /* If comm determinism verification, we cannot stop the exploration if some
- communications are not finished (at least, data are transfered). These communications
- are incomplete and they cannot be analyzed and compared with the initial pattern. */
- int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
- some_communications_are_not_finished();
std::unique_ptr<simgrid::mc::VisitedState> new_state =
std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState());
auto range = std::equal_range(visited_states.begin(), visited_states.end(),
new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
- if (_sg_mc_safety || (!partial_comm
- && initial_global_state->initial_communications_pattern_done)) {
+ if (compare_snpashots) {
for (auto i = range.first; i != range.second; ++i) {
auto& visited_state = *i;