From: Martin Quinson Date: Wed, 8 Nov 2023 09:24:14 +0000 (+0100) Subject: Fix SemWai::ReversibleRace() X-Git-Tag: v3.35~87^2 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/54a9845736995132258adc2e056946dfd2eeb57c Fix SemWai::ReversibleRace() --- diff --git a/examples/sthread/pthread-mc-producer-consumer.tesh b/examples/sthread/pthread-mc-producer-consumer.tesh index 508d8dac98..3c2eee5958 100644 --- a/examples/sthread/pthread-mc-producer-consumer.tesh +++ b/examples/sthread/pthread-mc-producer-consumer.tesh @@ -13,4 +13,4 @@ $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-chec $ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/reduction:odpor --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q -C 1 -P 1 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' > [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. -> [0.000000] [mc_dfs/INFO] DFS exploration ended. 39 unique states visited; 0 backtracks (0 transition replays, 39 states visited overall) +> [0.000000] [mc_dfs/INFO] DFS exploration ended. 617 unique states visited; 29 backtracks (524 transition replays, 1170 states visited overall) diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp index b20ebaa49e..d671e93703 100644 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp @@ -168,7 +168,7 @@ bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Ex // Reversible with everynbody but unlock which creates a free token const auto e1_transition = E.get_transition_for_handle(e1); if (e1_transition->type_ == Transition::Type::SEM_UNLOCK && - static_cast(e1_transition)->get_capacity() == 0) + static_cast(e1_transition)->get_capacity() <= 1) return false; return true; }