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

Another advice: in the initial condition, instead of

    /\ txRequest = [tx \in txs |-> RandomElement(RequestType)] 

write

    /\ txRequest \in [txs -> RequestType] 

This will cause the model checker to consider all possible combinations of requests instead of just one randomly chosen one.

On Apr 20, 2024, at 08:31, idivyans...@xxxxxxxxx <idivyanshu.ranjan@xxxxxxxxx> wrote:

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.

--
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/D03E3621-C252-4052-B37A-C04BBCBCE0B4%40gmail.com.