Hi,
I am new to TLA+ trying to get my head around temporal properties and safety proofs. I want to learn how to assert that the final state of my finite system is reachable. I am not sure if temporal properties are adequate for enforcing this assertion, but I decided to give them a try.
A bit of context: the specification I am writing is for the 'finish' construct in the X10 language, which implements a termination detection protocol. As an example, the following 'finish' block sends an asynchronous task to each place (i.e. process) to print "Hello from: place x". Behind the scenes, finish waits for a termination message from each place. When all messages are received, finish terminates.
---- finish example start ---
finish {
for ( p in places) at (p) async {
print("Hello from: " + p); //hello messages appear in arbitrary order
}
}
print ("bye"); // bye is printed after all hello messages
--- finish example end ---
I wrote a specification that allows 3 states for finish, init, working, and terminated:
init: initializes my variables then switches to the working state.
working: the state when it is allowed for messages to be sent and received.
terminated: the final state that a correct finish must eventually reach.
I have an action called F_Term that makes the final transition from working to terminated.
F_Term ==
/\ state = 'working' /\ pending = 1 /\ ...
/\ state' = 'terminated' /\ pending' = 0 /\ ...
I am trying to define a liveness property that asserts that finish must terminate (i.e. F_Term is always reachable). I tried the following:
Liveness == WF_<<Vars>>(F_Term)
Spec == Init /\ [][Next]_Vars /\ Liveness
and in 'Model Overview', I added Liveness as a property.
My problem is that TLC always shows 'No errors' even if I intentionally alter F_Term to make it unreachable. I do so by changing the enabling condition (state = 'working') to ( state = 'xyz') while I never set state to 'xyz'. The statistics indeed show that F_Term lines were executed 0 times, but TLC doesn't report that the liveness property was violated.
Is it wrong to use temporal formulas to assert that the final state is reachable? If not, then what is wrong with my Liveness action?
Your help is highly appreciated.
Best Regards,
Sara
Sara Hamouda
PhD Student
The Australian National University