I'm experimenting with implementation vs interface refinement using the HourClock spec as an example. Here's the HourClock spec
------- MODULE HourClock -------------
EXTENDS Naturals
VARIABLE h
CInit == h = 1 \* was \in (1..12)
CNext == h' = (h % 12) + 1
HC == CInit /\ [][CNext]_h
===
In the book, an hour clock that uses bit vectors instead of ints, BinHourClock is treated as an interface refinement of HourClock.
------------ MODULE BinHourClock -------------------------------
(*represents the time as a bit vector*)
EXTENDS Naturals
VARIABLE h_bv
valueOf(b) ==
LET n == CHOOSE i \in 0 .. 3 : DOMAIN b = 0 .. i
val[i \in 0 .. n] == IF i=0 THEN b[0]*(2^0)
ELSE (b[i]* (2^i)) + val[i - 1]
IN val[n]
hourVal(b) == IF b \in [(0 .. 3) -> {0,1}] THEN valueOf(b) ELSE 99
H(h) == INSTANCE HourClock \*substs param h for HourClock's var h
IR(h,b) == [] (h = hourVal(b))
BH2 == \EE h: IR(h, h_bv) /\ H(h)!HC
=============================================================
But now suppose I want to treat the BHC as an implementation of HC rather than an interface refinement, which means exposing h (and possibly hiding h_bv). I tried the following:
Add a new variable h2:
VARIABLE h_bv, h2
and change the spec
init_h_bv == h_bv = [i \in (0 .. 3) |-> IF i=0 THEN 1 ELSE 0]
Spec == init_h_bv /\ IR(h2, h_bv) /\ H(h2)!HC
But TLC produces the following error:
current state is not a legal state
While working on the initial state:
/\ h2 = null
/\ h_bv = (0 :> 1 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
If my understanding of INSTANCE is correct, h2 should be initialized to 1. Could someone tell me what I'm missing?
thanks
P.S. I changed HourClock to start at 1, not just to make TLC's life easier but also because TLC didn't like the initializer that implicitly initialized h_bv saying h2=hourVal(h_bv)