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

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 as

clock <= MAX_TIME

Hope 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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/E22933E0-B6A3-4530-9D60-152A789D76F8%40gmail.com.

Attachment: Time.tla
Description: Binary data

On 8 Oct 2021, at 03:45, ns <nedsri1988@xxxxxxxxx> wrote:

Sorry a correction: the TBound is clock < actionTriggerT + maxWait. The problem is deadlock not invariant not being satisfied.

On Thursday, October 7, 2021 at 6:26:10 PM UTC-7 ns wrote:
hello I've been reading the chapter on Real-time in the Specifying Systems book and am trying to experiment with a small spec that uses an integer clock (thereby bypassing the need to worry about real valued time, which wouldn't work with TLC anyway). This specific example is to turn the lights on and off, but in any case no less than every K seconds. However, it does not model check (invariant TimingOK violated) although it *seems* correct to me. The problem is that there is no way of forcing the LNext action to take place so the invariant is violated. (for the example I used K=2 and MAX_TIME 4). Is there a way to fix this so TLC will model check it?

thanks!

(*turn lights on and off, but at least every K seconds*)
EXTENDS Naturals
CONSTANTS
MAX_TIME, K

Time == 0 .. (MAX_TIME+1)

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

LNext == (IF lights THEN lights'=FALSE ELSE lights'=TRUE) /\ lightsTrigT' = clock
DoNothing == UNCHANGED <<lights,lightsTrigT>>

clockNext == clock' = clock+1

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

Next == (LNext \/ DoNothing) /\ clockNext /\ TBound(lightsTrigT, K)

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

TimingOK == (clock <= lightsTrigT + K)

THEOREM Spec => [] TimingOK

--
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/68599e0d-f105-4103-97ad-3e98644274ean%40googlegroups.com.