diff --git a/lib/STM_internal.ml b/lib/STM_internal.ml index cd2e7cb74..d25d1ef36 100644 --- a/lib/STM_internal.ml +++ b/lib/STM_internal.ml @@ -156,8 +156,8 @@ module Make(Spec : STM_spec.Spec) = struct (fun (seq,p1,p2) -> all_interleavings_ok seq p1 p2 Spec.init_state) (fun ((seq,p1,p2) as triple) -> (* Shrinking heuristic: - First reduce the cmd list sizes as much as possible, since the interleaving - is most costly over long cmd lists. *) + First reduce the cmd list sizes as much as possible, since the interleaving + is most costly over long cmd lists. *) (map (fun seq' -> (seq',p1,p2)) (Shrink.list_spine seq)) <+> (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2)) diff --git a/lib/STM_spec.mli b/lib/STM_spec.mli index cb9a189c5..2dd83b0f1 100644 --- a/lib/STM_spec.mli +++ b/lib/STM_spec.mli @@ -97,8 +97,8 @@ sig val next_state : cmd -> state -> state (** [next_state c s] expresses how interpreting the command [c] moves the - model's internal state machine from the state [s] to the next state. - Ideally a [next_state] function is pure. *) + model's internal state machine from the state [s] to the next state. + Ideally a [next_state] function is pure. *) val init_sut : unit -> sut (** Initialize the system under test. *)