]> AND Public Git Repository - simgrid.git/blobdiff - src/mc/mc_safety.cpp
Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] Remove the --cfg=model-check:1 flag
[simgrid.git] / src / mc / mc_safety.cpp
index 2ca64ec1aec6ecddc115bf20b341bc118486846d..7336489ef41ed6cb4cf2f498866b02ef1cfd4c7e 100644 (file)
@@ -199,6 +199,9 @@ void MC_modelcheck_safety(void)
       while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           req = MC_state_get_internal_request(state);
+          if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
+            xbt_die("Mutex is currently not supported with DPOR, "
+              "use --cfg=model-check/reduction:dpor");
           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {