spectacle icon indicating copy to clipboard operation
spectacle copied to clipboard
verified publisher icon will62794

Bogus results for trace expressions

Open lemmy opened this issue 1 year ago • 1 comments

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.

Screenshot 2024-05-05 at 10 00 16 AM

lemmy avatar May 05 '24 17:05 lemmy

I expect this is due to them including primed expressions, which likely won't be handled properly right now.

will62794 avatar May 07 '24 04:05 will62794