diff --git a/src/tracedAtomic.ml b/src/tracedAtomic.ml index b8d0712..b75f749 100644 --- a/src/tracedAtomic.ml +++ b/src/tracedAtomic.ml @@ -290,8 +290,7 @@ let _set_to_str s = IntSet.to_seq s |> List.of_seq |> List.map Int.to_string |> String.concat ", " let rec explore_source depth func state sleep_sets = - let _sleep = last_element sleep_sets in - let sleep = ref IntSet.empty in + let sleep = last_element sleep_sets in let s = last_element state in (* Printf.printf "[depth=%d] explore (backtrack=[%s], sleep=[%s], enabled=[%s])\n%!" depth (set_to_str s.backtrack) (set_to_str !sleep) (set_to_str s.enabled); *) @@ -443,17 +442,17 @@ let rec explore_source depth func state sleep_sets = (List.length prefix - 1) prefix_top.run_proc (atomic_op_str prefix_top.run_op); *) - let _prefix_top_sleep = + let prefix_top_sleep = !(List.nth sleep_sets (List.length prefix - 1)) in if IntSet.( cardinal - (inter prefix_top.backtrack ( initials ))) + (inter prefix_top.backtrack (diff initials prefix_top_sleep))) = 0 then ( let _initial = - match IntSet.(min_elt_opt ( initials )) with + match IntSet.(min_elt_opt (diff initials prefix_top_sleep)) with | Some initial -> initial | None -> IntSet.min_elt initials in