[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] TLC Error that had me puzzled for a while
- From: ns <nedsri1988@xxxxxxxxx>
- Date: Sat, 1 May 2021 11:04:25 -0700 (PDT)
- Ironport-hdrordr: A9a23:e3a0MKBzI5+x9E/lHegisceALOonbusQ8zAX/mp2TgFYddHdqtC2kJ0gpGXJoRsyeFVlo9CPP6GcXWjRnKQejLU5EL++UGDdyQ+VBa5464+K+UyGJwTa9vRBkY96eal/F9GYNykPse/e4BOkV/ctxcDvytHcuc76z21xCSFGApsQnjtRLwaADwlOQhNabKBJZqa0w8pcun6dfm4KZd6wHXkPU4H41qr2vbbHRTJDOBI98gmJilqTmcXHOjyR3hIfVD0KxLc57AH+4nLEz4GuqeuyxBOZ92K71eUupPLZ0ddICMGBjcIYQw+c9TqAX4hqV72csD1dmojGgydJrPD2rw4kL4BP7RrqDx2IiCHg3ATty18VhEPK80OSgnfovKXCNUoHIvdG7LgpFCfx2g4KsN167aNGxG7xjes1MTrw2Ar4o/zFTQtjmEbxm2crjOJ7tRJieLpbRrlWo4kSuG52MLNFJiL174g7DPJjZfux2N9mNX2daX7dsi1A29qxRzASE369Mzs/k/3Q/T5RknV0i3Ed2dVapHEd75gwIqMk2830doJylL9PSccSKZhwA+oMWqKMexHwaCOJC26ZLVT5GKxvARK9zqLf0fEO/emvPLYIwJExlJmEcFQdm3U1Z1uGM7z/4KF2
I just wanted to share something that had me puzzled for a while which I have distilled down to its essence in case its useful to anyone. Suppose I have a simple spec as follows,
Init == x=1 /\ y=1
A == y'=2 /\ UNCHANGED x
B == x < y'
Next == A /\ B
Spec == Init /\ [Next]_<<x,y>>
TLC is fine with this spec. However, if I change the Next definition to
Next == A /\ ENABLED(B)
Then TLC throws a runtime error with a strange message saying that it has no idea what y is. I subsequently discovered that this means that it doesn't have a value for y'. The reason is that in the first spec TLC is evaluating the step predicate B and as long as A comes before B, it has a value for y'. However in the second spec, ENABLED is a state predicate, and unfortunately TLC doesn't have a value for y' in the current state.
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/e8418ec5-830c-4fb3-a968-28295857c59dn%40googlegroups.com.