Very simple question by TLA newcomer

[Petar Vukmirovic]

Dear all TLA lovers,

I am very new to TLA, but I read the Amazon article and I was very much intrigued by this tool so I wanted to learn more.

In one of my masters courses we learning about modelling specifications and trying to generate test cases from them or proof some of our assumptions about specifications.

I talked to my professor about TLA+ and she liked it as well, so she told me to prepare a short introduction to it on Special Topics class. My task is to create a simple model of a sempaphore in TLA+.

To this end, I created the following TLA+ specification:

----------------------------- MODULE semaphore -----------------------------
VARIABLES CarsGo, PedestriansGo


\* Initial state
Init == \/ /\ CarsGo = TRUE
/\ PedestriansGo = FALSE
\/ /\ CarsGo = FALSE
/\ PedestriansGo = TRUE

\* Next step
Next == /\ CarsGo' = ~CarsGo
/\ PedestriansGo' = ~PedestriansGo

Spec == Init /\ [][Next]_<<CarsGo, PedestriansGo>>

Invariant == CarsGo # PedestriansGo

----------------------------------------------------------------------------
THEOREM Spec => []Invariant
BY DEF Spec, Invariant
============================================================================

However, when I try to prove the theorem, I get the message:
(* SMT failed with status = sat
*).

Can someone explain me what I am doing wrong?

Kindest regards,
Thanks in advance,

Petar Vukmirovic.

[Stephan Merz]

Dear Petar,

welcome to this group.

In order to answer your question: the SMT backend of the proof system is not able to prove temporal logic formulas. You should decompose your proof as follows:

THEOREM Spec => []Invariant

<1>1. Init => Invariant

<1>2. Invariant /\ [Next]_<<CarsGo, PedestriansGo>> => Invariant'

<1>. QED

   BY <1>1, <1>2, PTL DEF Spec

The non-temporal steps <1>1 and <1>2 should be provable using SMT, but the PTL backend has to be used for the final step. You may also want to read the tutorial on the TLAPS Web site.

----

However, I am not sure if it is a good idea to introduce the proof system for your presentation. I would imagine that you are better off showing the model checker, all the more for a finite-state specification such as yours.

Best regards,

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

[Leslie Lamport]

Hi Petar,

Stephan is probably right about showing the model checker rather than
the proof system.  However, it's impossible to give you good advice
without knowing more about your presentation--in particular, who it's
for, what its purpose is, and how much time you have.  You might want
to look at one or more of the presentations I've given that have been
recorded and put on the Web.  The one that I expect is most relevant
is at

   http://www.heidelberg-laureate-forum.org/blog/video/lecture-monday-august-24-2015-leslie-lamport/

You might also suggest that your professor watch it. 

Good luck,

Leslie

[Petar Vukmirovic]

Dear Mr Lamport and Mr Merz,

I am really sorry I did not respond earlier, but somehow I did not get any notifications for this post.

Anyway, thank you very much for your help and answers, I will take a look at the presentation you proposed.

The presentation is half an hour presentation on a special topic in software testing (such as TLA+)
aimed towards first year Master CS students.

Kindest regards,
Petar Vukmirovic.