Bogus results for trace expressions
Opened this issue · 1 comments
lemmy commented
The trace expressions RoTxRequestAction and RwTxRequestAction for https://github.com/lemmy/CCF/blob/mku-ConsistencyMonolith/tla/consistency/Consistency.tla are certainly not true in the shown trace.
will62794 commented
I expect this is due to them including primed expressions, which likely won't be handled properly right now.