How is this successful?

[Matt McCormick]

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

==== 

[Markus Kuppe]

TLC *ignores* THEOREM and instead requires you to add a corresponding
"PROPERTY" in Service.cfg.

Service.tla:

...
Prop == <>[]Done


Service.cfg:

...
PROPERTY Prop

M.

[Matt McCormick]

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

[Matt McCormick]

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.

[Stephan Merz]

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

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

[Matt McCormick]

Thank you Stephan.  This makes sense now that you point it out.  I thought I had tried this before and ran into an error.  I guess it must have been something unrelated because your suggestion does work as expected.

Matt