[tlaplus] How is this successful?

[Matt McCormick <mattmccor@xxxxxxxxx>]

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

==== 

-- 
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/af66454a-0473-4d7a-bdb1-1c5a05b1c23fn%40googlegroups.com.