These are issues I am facing when I am trying to run this spec.
- Definition of sort is wrong; it can always return {} as pointed out by Stephan Merz.
- Definition of Min is wrong as this is conjunction of boolean _expression_ and integer
- In HasConflict(txRequest[tx],txRequest[tupleOwners[tuple]]) , tupleOwners[tuple] is set whereas txRequest is mapping from integer to RequestTypes
That
is how far I looked. I advise you to check the _expression_ you are
writing with TLA+ Evaluate _expression_ tool to check if this is what you
intend.