Is this TLA+ specification correct?

Question

So far, i have done a little bit of code for my project, but don't know whether its true or false. Can u guys see my code?? First at all, i should post the requirement for better understanding..

In computer science, mutual exclusion refers to the requirement of ensuring that no two processes or threads are in their critical section at the same time. A critical section refers to a period of time when the process accesses a shared resource, such as shared memory. The problem of mutual exclusion was first identified and solved by Edsger W. Dijkstra in 1965 in his paper titled: Solution of a problem in concurrent programming control.

For visual description of a problem see Figure. In the linked list the removal of a node is done by changing the “next” pointer of the preceding node to point to the subsequent node (e.g., if node i is being removed then the “next” pointer of node i-1 will be changed to point to node i+1). In an execution where such a linked list is being shared between multiple processes, two processes may attempt to remove two different nodes simultaneously resulting in the following problem: let nodes i and i+1 be the nodes to be removed; furthermore, let neither of them be the head nor the tail; the next pointer of node i-1 will be changed to point to node i+1 and the next pointer of node i will be changed to point to node i+2. Although both removal operations complete successfully, node i+1 remains in the list since i-1 was made to point to i+1 skipping node i (which was the node that reflected the removal of i+1 by having it's next pointer set to i+2). This problem can be avoided using mutual exclusion to ensure that simultaneous updates to the same part of the list cannot occur.

This is my code :

EXTENDS Naturals
CONSTANT Unlocked, Locked
VARIABLE P1,P2

TypeInvariant == /\ P1 \in {Unlocked,Locked}
             /\ P2 \in {Unlocked,Locked}


Init == /\ TypeInvariant
        /\ P1 = Unlocked


Remove1 == P2' = Locked
Remove2 == P1' = Locked

Next == Remove1 \/ Remove2

Spec == Init /\ [][Next]_<<P1,P2>>
THEOREM Spec => []TypeInvariant 

Answer 1

First, what are you trying to model? It seems the only thing you are interested in proving as a theorem is the type invariant. I would have thought you want to prove something about mutual exclusion and not just the possible values of P1 and P2. For example, do you want to prove that P1 and P2 are never both locked at the same time?

MutualExclusion == ~(P1 = Locked /\ P2 = Locked)
THEOREM MutualExclusionTheorem == Spec => []MutualExclusion

Also, I wouldn't put TypeInvariant in the definition of Init. Your Init should contain the starting value(s) of your variables P1 and P2. Then you have a theorem,

THEOREM InitTypeInvariant == Init => TypeInvariant

and prove it. This theorem will be used in the proof of the theorem Spec.