On Monday, 5 November 2018 12:18:38 UTC, Catalin Marinas wrote:
Without the 'cmd' debug variable (or cmd only set to inst[1] in the spec below, which is part of the symmetry optimisation):
Small correction here: The inst[1] strings are not part of the symmetry optimisations (that was a different spec I had with ldr/str etc. as model constants). However, the rest is valid, if I change the last CPUNext line to cmd' = inst[1], I get only 244 distinct states, as expected. For some reason, it doesn't like the << inst[1], inst[2], inst[3] >> tuple in a variable that's not part of the VIEW (or I got the this part of TLC wrong).
Catalin