On Tuesday, 5 October 2021 at 16:48:02 UTC-7 Markus Alexander Kuppe wrote:
On 10/5/21 4:30 PM, Matt McCormick wrote:
> Hi there,
>
> I have a beginner question that I'm sure has an obvious answer but I've
> been looking things over for quite a while and can't figure it out. I
> have the following .tla file and when I run it with the following .cfg
> file, the model checker succeeds.
>
> However, I'm pretty sure it should fail because when BadRequest is acted
> upon, http will become 400 and status will become a value other than
> "null". This should fail since `Done` will not eventually be reached.
> What am I missing?
>
> # Service.cfg
> SPECIFICATION Spec
> CHECK_DEADLOCK FALSE
>
> # Service.tla
> ---- MODULE Service ----
> EXTENDS TLC
>
> VARIABLES http, status
>
> Init ==
> http = 0 /\ status = "null"
>
> Success ==
> /\ http = 0
> /\ http' = 200
> /\ status = "null"
> /\ status' = "successful"
>
> BadRequest ==
> /\ http = 0
> /\ http' = 400
> /\ status = "null"
> /\ status' = "SpecificError"
>
> InternalError ==
> /\ http = 0
> /\ http' = 500
> /\ UNCHANGED <<status>>
>
> Next ==
> \/ Success
> \/ BadRequest
> \/ InternalError
>
> Spec == Init /\ [][Next]_<<http, status>>
> Done ==
> \/ http = 200 /\ status # "null"
> \/ http # 200 /\ status = "null"
> ----
> THEOREM Spec => <>[]Done
> ====
TLC *ignores* THEOREM and instead requires you to add a corresponding
"PROPERTY" in Service.cfg.
Service.tla:
...
Prop == <>[]Done
Service.cfg:
...
PROPERTY Prop
M.