[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TLC Error with Implementation Refinement of HourClock

Yes sorry for some reason all the formatting was removed after I posted it and despite multiple attempts I simply cannot get them to display in the final posted version so I am enclosing the files instead

I'm experimenting with implementation vs interface refinement using the HourClock spec as an example. Here's the HourClock spec 


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)


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


(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?

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)

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7575a5a2-66ea-44a7-9177-28f63f919a42n%40googlegroups.com.

Attachment: HourClock.tla
Description: Binary data

Attachment: BinHourClock.tla
Description: Binary data

Attachment: BinHourClockImpl.tla
Description: Binary data