Valued signals are mis-interpreted

Consider the attached MWE (valsig.sctx). Contrary to my possible bogus intuition, we can't make it to state B. I'm assuming here that `b` refers to the tick and `val(b)` to the most recent value of `b`, similar to `current b` in some lustre dialects.

That this might not just a problem in the simulation IDE can be seen by exporting to Promela. I've verified that `s` is never true, implying that the challenge is infeasable, by adding

ltl doh { []!s }

to the .pml and running spin. The same problem manifests itself when trying to emit a valued signal as in MWE (valsig2.sctx) as being "not asc-schedulable".