Benefits of temporal logic for KOHCTPRYKTOP / KNOH about knoh HOT 4 OPEN

Part 1 - Getting excited

Now, in order to get across what that means specifically - I have to strike out a bit:

As you know, the circuit specification (ie what the player is to implement) need only be little above trivial - and the fixed plus rather limited test protocol as it appears in the original game cannot anymore check all possible input combinations. Even more so if we think about not only combinations of logic levels at the input pins but also of combinations of transitions of these levels. Then you have 4^n instead of 2^n with n input pins, hence a factor of 2^n or 2 in the exponent.
Oh, and it does make a difference to look at combinations of logic level transitions vs combinations of logic levels alone. This is due to the rules of the game, particularly the delay from junctions (those rules are set and they're fine, IMHO. They're what makes the game so interesting.)

You can watch people exploiting this lack of verifaction in a quest for minimal "Design score (lower is better)" over at kongregate; see also #5. The best (lowest) scores are achieved by exploiting the limitedness of the test protocol, by simply not implementing what is not tested.

To be clear: there's nothing wrong with competition to reach an optimum, rather on the contrary. My problem in this case is that the optimum is awfully ill-defined as it stands (ie defined by the original game).

So then, how to specify the optimum, really? And how to verify and score an actual proposed solution against it?
Btw, scoring is of course much harder than just "yes" vs "no", but we'll come to this later on.
For now let's compare these:

• Naive approach: check all the 4^n possible combinations of logic-level transitions in the test protocol explicitly. Well, you know why this is not being done in the original game.
• Enter CTL: Instead of laying out explicitly all of that state space and the transitions between those states (now: not between logic levels at a single pin) - we will keep it implicit in some way. What this abstracted representation actually is will be seen later. But on it we can do reasoning out of which will get either
  • YES, complies with specification under all circumstances
  • or NO plus a counter-example under which circumstances it doesn't

So it's that last point which should get you excited!

To be clear: the counter-example will consist of an ordered series of (sets of simultaneous) logic level transitions at the input pins (alongside with level transitions at the outputs) which, at the end, has a state that's outside the specification.
Note that both, the specification and the counter-example include timely order. You could also call it order of states wrt time. That's what I meant by saying (sets of) logic level transitions rather than just (sets of) logic levels. This, however, is not entirely precise. In fact, what defines a state really only is the logic levels, but:

The difference that the inclusion of timely order makes - and that really makes pretty much all the difference - is this:

• "is state X" - defined as one combination of input and output levels - a valid state of the specification at all?
• or - in addition to the above - has it also been reached in a way compliant to the spec?

As said, CTL will allow for not only having the first but both of these points. It will also allow for some rewind / fast-forward action to inspect the counter-example at particular instances of time.
The trick that makes this feasible for considerably larger models is to keep states and and transitions between them implicit (ie with a compact representation) as much as possible. This is called symbolic modelchecking, "symbolic" standing for having things implicit.

In the next part there'll be an example of a transition system, illustrating said difference.

from knoh.

Let me put in a small repost from #1, as it just seems to fit well in here:

[...] It's doable in principle, my endeavour here is to find out if it's practically applicable in a game like that (and see what size is manageable). [...]

In fact such or similar techniques have been employed in the hardware industry for a long time (> a decade for sure, maybe two). However, there's always the problem of state-space explosion. And putting timing into the equation makes it considerably worse. I know of some attempts of formalizing timing (ie not just "a before b", but rather "a before b in such and such a margin of some atomic time") but to my knowledge that's nothing like mainstream, yet...

from knoh.

Ah, forgot to put this in somehwere:

It's moving from incomplete simulation towards complete verification!

And, as said, not only this. Also providing kind of constructive criticism in case of not, or not quite (!), meeting the spec.

from knoh.

Hey, just to mention: looking forward to your thoughts!

Of course I understand that digesting my rather long ramblings... well, as said: just wanted to have it mentioned.
In fact I cannot devote myself as much time to this as I'd like.

from knoh.