let reachable_on_trace_from_init s unsafe trace = let all_procs = procs_on_trace trace in let proc_sets = (* all_partitions *) [all_procs] in let inits = mkinits_up_to proc_sets s in match possible_trace ~starts:inits ~finish:unsafe ~procs:all_procs ~trace with | Spurious _ | Unreach -> Unreach | Reach _ as r -> r