Files
bot-formal-models/tla/models/dedupe_collision_fallback_ok.cfg

10 lines
151 B
INI

SPECIFICATION Spec
INVARIANT Inv_NoLossUnderFallback
CONSTANTS
Events = {"e1","e2"}
Keys = {"k"}
KeyE1 = "k"
KeyE2 = "k"
UseFallback = TRUE