TLC error with INSTANCE mechanism

[ns]

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)

[Andrew Helwer]

I found this confusing to follow, could you post the specific specs and model files that are giving you trouble?

[ns]

es sorry for some reason all the formatting was removed after I posted it. And the displayed post seems to ignore all color formatting. Here's the post again, this time with the specs in a different font

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 Specifying Systems book, there is an hour clock that uses bit vectors instead of ints. This spec BinHourClock is treated as an interface refinement of HourClock. (valueOf converts a bit vector into its corresponding integer value)

--------------------------------------- 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))

BHC == \EE h: IR(h, h_bv) /\ H(h)!HC
========================================================

But now suppose I want to treat the  BinHourClock   as an implementation of  HourClock   rather than an interface refinement, I need to expose h (and possibly hide h_bv). I tried the following (changes to BinHourClock shown in red)

--------------------------------------- MODULE BinHourClockImpl -------------------------------

(*represents the time as a bit vector*)
EXTENDS Naturals

VARIABLE h_bv, h2

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))

init_h_bv == h_bv = [i \in (0 .. 3) |-> IF i=0 THEN 1 ELSE 0]

BHCImpl   == init_h_bv /\ IR(h2, h_bv) /\ H(h2)!HC
===========================================================

(I added a new variable h2 representing integer time, an initializer for h_bv so TLC doesn't complain, and changed the spec so it no longer hides the integer time)

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)



Reply all

Reply to author

Forward

[ns]

In case anyone is interested, I figured out where I was going wrong with what I had. The problem was that I forgot that TLC needs specs to be in a "normal" form of Init /\ [Next]_vars /\ <fairness conds> and what I have above doesn't fit that. Although I would like to have written something similar to what is in the Specifying Systems book:

    init_hr_bv == hr_bv = [i \in (0 .. 3) |-> IF i=0 THEN 1 ELSE 0]

    IR(h,b) == [] (h = hourVal(b))

          SpecNoTLC == init_hr_bv /\ IR(hr, hr_bv) /\ HC(hr)!Spec

It gets rejected by TLC. The following does pass TLC. 

    Init == init_hr_bv /\ HC(hr)!CInit
    \*this is the key for TLC to be able to check. Constrain hr' to be the HourVal of hr_bv
    Next == HC(hr)!CNext /\ hr_bv' \in [(0 .. 3) -> {0,1}] /\ hr' = hourVal(hr_bv')
    Spec == Init /\ [][Next]_<<hr_bv,hr>> 

The hr_bv' \in [(0 .. 3) -> {0,1}] is necessary so TLC has a finite set of values to try in turn for the next conjunct