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

[Egor Suvorov <egor.suvorov@xxxxxxxxx>]

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.