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
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.