[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 

<HourClock.tla>

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)

<BinHourClock.tla>

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

<BinHourClockImpl.tla>

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

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