Re: [tlaplus] How is this successful?

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.

--
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/671a75d2-94d6-b560-9b5e-108e23efbca5%40lemmster.de.