# pluscal, tla+ and tekker algorithm

This is my first time using pluscal and tla+. So honestly, I have no clue how this works and what to do.

So, I got the dekker algorithm, which guarantees MutualExclusion and tests for deadlocks or starvations.

Here is the code:

EXTENDS Integers, Sequences

(*

--algorithm criticalsection5dekker
{
\* Global variables
variables turn = 1; wantp = FALSE; wantq = FALSE;

\* The non-critical section.
\* a process might stay in the non-critical section forever (however,
\* each process must leave the critical section).
\* This procedure covers both cases: finite and infinite execution
\* of the non-critical section.
procedure NCS()
variable isEndless;
{
\* Non-deterministically choose whether the procedure will
\* be endless or finite.
ncs0: with (x \in {0,1}) {
isEndless := x;
};
ncs1: if (isEndless = 1) {
ncs2: while (TRUE) {
ncs3: skip;
}
} else {
ncs4: return;
}
}

\* First process (name P, pid 1)
process(P = 1) {
p0: while (TRUE) {
p1: call NCS(); \* non-critical section
p2: wantp := TRUE;
p3: while (wantq = TRUE) {
p4: if (turn = 2) {
p5: wantp := FALSE;
p6: await turn = 1;
p7: wantp := TRUE;
};
};
p8: skip; \* critical section
p9: turn := 2;
p10: wantp := FALSE;
}
}

\* Second process (name Q, pid 2)
process(Q = 2) {
q0: while (TRUE) {
q1: call NCS(); \* non-critical section
q2: wantq := TRUE;
q3: while (wantp = TRUE) {
q4: if (turn = 1) {
q5: wantq := FALSE;
q6: await turn = 2;
q7: wantq := TRUE;
};
};
q8: skip; \* critical section
q9: turn := 1;
q10: wantq := FALSE;
}
}

}

*)

\*** Mutual exclusion
\* For mutual exclusion, process 1 and process 2 must never be in the
\* critical section at the same time.
MutualExclusion == [] ~ (pc = "p8" /\ pc = "q8")

\* If P and Q both want to enter the critical section, one of them will
\* eventually enter the critical section.
NoDeadlock == /\ pc = "p2"
/\ pc = "q2"
~>
\/ pc = "p8"
\/ pc = "q8"

\*** Starvation free
\* If P wants to enter the critical section, P will eventually enter
\* the critical section. The same must hold for Q.
NoStarvationP == (pc = "p2") ~> (pc = "p8")
NoStarvationQ == (pc = "q2") ~> (pc = "q8")
NoStarvation == /\ NoStarvationP
/\ NoStarvationQ

\* Assume weakly fair scheduling of all commands
(* PlusCal options (wf) *)

=============================================================================
I need to implement another feature of the algorithm, so if turn = 1, there will always be turn = 2. Thats what I wrote (not sure if it makes sense).

\***turn change
TurnChange == pc = "q4" ~> pc = "p9"

Now I use the commands to translate the code in the console:
java pcal.trans criticalsection5dekker.tla

and to run it:
java tlc2.TLC criticalsection5dekker.tla -config criticalsection5dekker.cfg -workers 1 -modelcheck -deadlock

And now, I have no clue at all what the console tells me. If what I wrote is correct or if I did another mistake.

http://imgur.com/a/RHuH8

Can anybody help me?