Running TLC on the generated 2PC spec leads to deadlock after only the initial state. I have tried specifying the TLC config in two ways, and both leads to the same issue:
Expressing tla_c as a variable and constraining it's values
Expressing tic_c as a literal.
Run 2PC in TLC
With 1 participant and 1 coordinator, takes 7min, which is like forever.
Only 2 distinct states generated. Why? Is this thing live? Check that decision is eventually reached
Change decision algorithm to always commit in the generated TLA.
Yep, safety is not violated. This thing is not live
Actually yes something is wrong. In the trace returned after deadlock, there is only the initial state.
Running TLC on the generated 2PC spec leads to deadlock after only the initial state. I have tried specifying the TLC config in two ways, and both leads to the same issue:
tla_cas a variable and constraining it's valuestic_cas a literal.