Skip to content

Commit dfcf67b

Browse files
committed
Add comment about widening delay transfer functions
1 parent debfc28 commit dfcf67b

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/lifters/wideningDelay.ml

+4
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,9 @@ struct
4747
end
4848

4949

50+
(** Lift {!S} to use widening delay for local states.
51+
52+
All transfer functions reset the counter to 0, so counting only happens between old and new values at a local unknown. *)
5053
module DLifter (S: Spec): Spec =
5154
struct
5255
module D =
@@ -114,6 +117,7 @@ struct
114117
lift_fun ctx lift S.event ((|>) (conv octx) % (|>) e)
115118
end
116119

120+
(** Lift {!S} to use widening delay for global unknowns. *)
117121
module GLifter (S: Spec): Spec =
118122
struct
119123
module D = S.D

0 commit comments

Comments
 (0)