Re: [tlaplus] asserting that the final state is reachable

Hi Stephan,

Thanks very much for the clear explanation and for providing the solution. Asking TLC to check the property <>(state = "terminated" /\ pending = 0) instead of Liveness solved my problem.

Best Regards,

Sara

On Thursday, September 7, 2017 at 9:44:55 PM UTC+10, Stephan Merz wrote:

Hi Sara,

if I understand correctly, you have your "liveness" formula as a conjunct of the specification and also as the property you make TLC verify, so you really have TLC check if the implication

Init /\ [][Next]_vars /\ Liveness => Liveness

holds. This must obviously be true. What you probably meant was including the fairness condition that you have in the spec, and checking a liveness property such as

<>(state = "terminated" /\ pending = 0)

or perhaps (assuming you have several "places")

<>(\A p \in Places : state[p] = "terminated")

or similar. This will probably lead you to include fairness on more actions than just the final one in your specification.

Hope this helps,
Stephan

On 7 Sep 2017, at 11:09, Sara Hamouda <sar...@xxxxxxxxx> wrote:

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

--
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 post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.