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

12 lines
264 B
INI

SPECIFICATION Spec
INVARIANTS Inv_ThreadBindingWins
\* Negative: show bug where thread loses to parent
CONSTANTS
Agents = {"a","b","default"}
DefaultAgent = "default"
HasThreadBinding = TRUE
HasParentBinding = TRUE
ThreadAgent = "a"
ParentAgent = "b"