From 54a9845736995132258adc2e056946dfd2eeb57c Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Wed, 8 Nov 2023 10:24:14 +0100 Subject: [PATCH] Fix SemWai::ReversibleRace() --- examples/sthread/pthread-mc-producer-consumer.tesh | 2 +- src/mc/explo/odpor/ReversibleRaceCalculator.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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; } -- 2.20.1