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

*From*: ns <nedsri1988@xxxxxxxxx>*Date*: Wed, 18 Jan 2023 18:24:07 -0800 (PST)*References*: <6e887a4b-6db7-4a44-b099-fa37141adb82n@googlegroups.com> <69774156-c038-4c8e-87fb-49169b75530fn@googlegroups.com>

Yes sorry for some reason all the formatting was removed after I posted it. Here's the post again, this time with the specs in a different color

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

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

========================================================

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

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

===========================================================

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

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)

On Tuesday, January 17, 2023 at 7:09:07 AM UTC-8 andrew...@xxxxxxxxx wrote:

I found this confusing to follow, could you post the specific specs and model files that are giving you trouble?On Monday, January 16, 2023 at 4:42:25 PM UTC-5 ns wrote: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, h2and change the specinit_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)!HCBut 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?thanksP.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/3753e3e2-5272-43b5-9cac-cbc4e93c088dn%40googlegroups.com.

**References**:**[tlaplus] TLC error with INSTANCE mechanism***From:*ns

**[tlaplus] Re: TLC error with INSTANCE mechanism***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] How can I modelcheck an angle-bracket action formula?** - Next by Date:
**[tlaplus] Re: TLC error with INSTANCE mechanism** - Previous by thread:
**[tlaplus] Re: TLC error with INSTANCE mechanism** - Next by thread:
**[tlaplus] Re: TLC error with INSTANCE mechanism** - Index(es):