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

*From*: Earnshaw <dongluming77@xxxxxxxxx>*Date*: Fri, 5 May 2023 20:05:50 -0700 (PDT)*References*: <92ac2873-a0a6-415a-9c6f-fd6a8afa028cn@googlegroups.com> <68599e0d-f105-4103-97ad-3e98644274ean@googlegroups.com> <E22933E0-B6A3-4530-9D60-152A789D76F8@gmail.com> <6ffc80d4-e218-40cc-8f53-bca2c868dbb6n@googlegroups.com> <ac28683b-f55a-4916-978a-b7a5b1f5f18en@googlegroups.com> <4AB111BC-F840-4085-9A25-9B39EB368CB4@gmail.com>

Hi ns, this is my spec to solve the problem, hope it can help:

-------------------------------- MODULE Time --------------------------------

(*turn lights on and off, but at least every K seconds*)

EXTENDS Naturals

CONSTANTS

MAX_TIME, K

Time == 0 .. MAX_TIME

VARIABLE lights,clock, lightsTrigT

vars == <<lights, clock, lightsTrigT>>

isTyped == lights \in BOOLEAN /\ clock \in Time /\ lightsTrigT \in Time

Init == lights=TRUE /\ clock=0 /\ lightsTrigT=0

\*Init == lights=FALSE /\ clock=10 /\ lightsTrigT=10

TBound(actionTriggerT, maxWait) == clock < actionTriggerT + maxWait

clockNext == /\ TBound(lightsTrigT, K)

/\ IF TBound(lightsTrigT, K-1)

THEN

/\ clock' = clock+1

/\ UNCHANGED <<lights,lightsTrigT>>

ELSE \*clock = (lightsTrigT + K -1)

/\ (IF lights THEN lights'=FALSE ELSE lights'=TRUE)

/\ clock' = clock+1

/\ lightsTrigT' = clock'

Next == clockNext

Spec == Init /\ [][Next]_vars

TimingOK == clock <= lightsTrigT + K

Test == clock # 10

THEOREM Spec => [] TimingOK

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

(*turn lights on and off, but at least every K seconds*)

EXTENDS Naturals

CONSTANTS

MAX_TIME, K

Time == 0 .. MAX_TIME

VARIABLE lights,clock, lightsTrigT

vars == <<lights, clock, lightsTrigT>>

isTyped == lights \in BOOLEAN /\ clock \in Time /\ lightsTrigT \in Time

Init == lights=TRUE /\ clock=0 /\ lightsTrigT=0

\*Init == lights=FALSE /\ clock=10 /\ lightsTrigT=10

TBound(actionTriggerT, maxWait) == clock < actionTriggerT + maxWait

clockNext == /\ TBound(lightsTrigT, K)

/\ IF TBound(lightsTrigT, K-1)

THEN

/\ clock' = clock+1

/\ UNCHANGED <<lights,lightsTrigT>>

ELSE \*clock = (lightsTrigT + K -1)

/\ (IF lights THEN lights'=FALSE ELSE lights'=TRUE)

/\ clock' = clock+1

/\ lightsTrigT' = clock'

Next == clockNext

Spec == Init /\ [][Next]_vars

TimingOK == clock <= lightsTrigT + K

Test == clock # 10

THEOREM Spec => [] TimingOK

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

在2021年10月16日星期六 UTC+8 19:50:41<Stephan Merz> 写道：

First, you can of course ignore the deadlock by disabling deadlock checking if you are not interested in it.Second, a state is deadlocked if `ENABLED Next' is false at that state, but the actual transition relation is [Next]_vars, so a finite behavior ending in a deadlocked state can always be extended to an infinite behavior.StephanOn 16 Oct 2021, at 06:23, ns <nedsr...@xxxxxxxxx> wrote:But perhaps one answer here is that while the spec doesn't admit any traces in which the invariant is violated, it does admit finite traces (ie those that deadlock) and that is what TLC is catching. However, given TLA semantics, only infinite traces can be traces of the model so finite traces don't or shouldn't enter the picture.On Friday, October 15, 2021 at 8:53:55 PM UTC-7 ns wrote:hi Stephan, thanks as always for your insightful answer. My thinking was that since the spec doesn't admit any traces in which the lights don't change at least once every K s (based on my understanding of TLA semantics) I was hoping that the model checker would agree and say that the invariant was indeed satisfied. But instead it reported deadlock. I did see where the deadlock is coming from, and I suppose its a way of rejecting those bad traces, but was somewhat surprising. I like your solution to the problem using a kind of "lookahead" to prevent DoNothing when a bound is about to expire, but it appears to me a way of getting TLC to do the right thing. Please let me know if I'm still missing something key.On Sunday, October 10, 2021 at 2:19:32 AM UTC-7 Stephan Merz wrote:Not sure I understand your question: TLC *does* model check your spec, it just (correctly) signals a deadlock, since the non-clock variables may stutter according to DoNothing until the clock exceeds its bound, at which point no action is enabled anymore. If you intend to avoid this, DoNothing needs a stronger time bound, see attached module for a possible definition.Since the modified spec generates an unbounded state space, you'll need to add a state constraint to your model, such asclock <= MAX_TIMEHope this helps,Stephan--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ac28683b-f55a-4916-978a-b7a5b1f5f18en%40googlegroups.com.

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/1ea351c1-618c-46d4-a6d9-038ac968710dn%40googlegroups.com.

**References**:**[tlaplus] How to model check this "real-time" spec?***From:*ns

**[tlaplus] Re: How to model check this "real-time" spec?***From:*ns

**Re: [tlaplus] How to model check this "real-time" spec?***From:*Stephan Merz

**Re: [tlaplus] How to model check this "real-time" spec?***From:*ns

**Re: [tlaplus] How to model check this "real-time" spec?***From:*ns

**Re: [tlaplus] How to model check this "real-time" spec?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Contributing TLA+ specification to GitHub** - Next by Date:
**Re: [tlaplus] Parser Error** - Previous by thread:
**Re: [tlaplus] How to model check this "real-time" spec?** - Next by thread:
**[tlaplus] Understanding PlusCal 'either' translation to TLA** - Index(es):