bot-formal-models/tla/models/precedence_negative_bad_allow_overrides.cfg

SPECIFICATION Spec
INVARIANT Inv_DenyWins

CONSTANTS
  Tools = {read, write, exec, memory_get}
  N = 4

  Allow1 = {read, write, exec, memory_get}
  Allow2 = {read, write, exec, memory_get}
  \* layer 3 explicitly allows memory_get again
  Allow3 = {memory_get}
  Allow4 = {read, write, exec, memory_get}

  Deny1 = {}
  Deny2 = {memory_get}
  Deny3 = {}
  Deny4 = {}

  \* Unused layers
  Allow5 = {read, write, exec, memory_get}
  Allow6 = {read, write, exec, memory_get}
  Allow7 = {read, write, exec, memory_get}
  Allow8 = {read, write, exec, memory_get}
  Deny5 = {}
  Deny6 = {}
  Deny7 = {}
  Deny8 = {}