Re: [tlaplus] How is this successful?

On Saturday, 9 October 2021 at 08:56:04 UTC-7 Stephan Merz wrote:

Fairness should be asserted for actions, not for state predicates. I believe you want to write

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

That fairness condition asserts that as long as some (non-stuttering) action may occur, some such action will occur.

Stephan

On 9 Oct 2021, at 02:02, Matt McCormick <matt...@xxxxxxxxx> wrote:

I have a followup question.

I've tried to simplify the spec since I'm running into an error trying to avoid the model checker failing due to "Temporal properties were violated." With the following spec, the error trace shows stuttering after the Initial predicate where status = 0

vars == <<status>>
Success == status = 0 /\ status' = 200
Error == status = 0 /\ status' = 500
Init == status = 0 \* 0 represents an incomplete response
Next == Success \/ Error
Done == status = 200 \/ status = 500
Spec == Init /\ [][Next]_vars
----
Prop == <>[]Done

In order to avoid stuttering I thought I should be able to make the following modification

Spec == Init /\ [][Next]_vars /\ WF_vars(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

The Error Trace shows that the Success step was taken and status = 200.
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.

--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6f5e5d5e-c7cb-4b88-9086-6d5134c2914dn%40googlegroups.com.