Re: [tlaplus] How is this successful?

Spec == Init /\ [][Next]_<<http, status>> /\ WF_<<http, status>>(Done)

However, running the model now throws an exception and I'm not sure why. The position does point to the WF clause that was introduced but I can't tell why it's incorrect. The full error given is:

TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a java.lang.RuntimeException

The error occurred when TLC was evaluating the nested

expressions at the following positions:

0. Line 41, column 66 to line 41, column 69 in Service

1. Line 38, column 5 to line 39, column 36 in Service

2. Line 39, column 8 to line 39, column 36 in Service

3. Line 39, column 8 to line 39, column 17 in Service

4. Line 39, column 22 to line 39, column 36 in Service

5. Line 41, column 49 to line 41, column 64 in Service

6. Line 41, column 51 to line 41, column 54 in Service

On Tuesday, 5 October 2021 at 17:16:06 UTC-7 Matt McCormick wrote:

Thank you Markus! I knew I was missing something simple.

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.