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

[tlaplus] The TLA+ Video Course, module AB2H: is there a mistype in SpecH?

Hello everyone,

I'm watching this video: http://lamport.azurewebsites.net/video/video10b.html and around 5:41 it prompts to download AB2H.tla from https://lamport.azurewebsites.net/video/AB2H.tla . Here is an excerpt:

SpecH == /\ AB2!Spec
         /\ [] /\ AtoB  \in Seq(Data \X {0,1})
               /\ BtoA \in Seq({0,1})

It looks nothing like the previously demonstrated render (at 5:30).

My understanding is that this is a simple mistype: SpecH was probably mixed with TypeOKH from the second half of the file. So it's actually just an AB2!Spec with `Bad` messages prohibited.

Moreover, this error is not caught by model checking because TLC cannot check neither `SpecH => AB!Spec` nor `SpecH => SpecHH` implication as SpecH has a non-standard form. TLC can check the `SpecHH => SpecH` implication, but it is true: requirements for AtoB and BtoA in `SpecH` are more relaxed than necessary.

Is this understanding fully correct?

Best regards,
Egor Suvorov

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/33a5ce5c-919c-4061-84ba-ee6e9cecbac2n%40googlegroups.com.