bot-formal-models/tla/models/precedence_min.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}
  Allow3 = {read, write, exec, 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 = {}