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

13 lines
185 B
INI

SPECIFICATION Spec
INVARIANTS
Inv_AtMostOnce
Inv_LogImpliesDeduped
Inv_EmitsUseStableSession
CONSTANTS
Events = {"e"}
Routes = {"r1"}
MaxAttempts = 3
Route0Route = "r1"