[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Deadlock reach without invocation of main actions.

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.

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/921bb42d-d870-4ba1-b2a0-efc322e80f4an%40googlegroups.com.