Very simple question by TLA newcomer

[Petar Vukmirovic <petar.vu...@xxxxxxxxx>]

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.