.

Sem.tla

@@ -13,15 +13,23 @@ Procs == 0..N
    fair process (P \in Procs) {
      ncs:- while (TRUE) {
              skip ;
-     enter:+ await sem = 1 ;
-             sem := 0 ;
+\*     enter:+ await sem = 1 ;
+\*             sem := 0 ;
+        enter:+ if (sem = 1) {
+                  sem := 0 ;
+                  goto cs 
+                } 
+                else {
+                  goto enter
+                } ;
+
          cs: skip ;
        exit: sem := 1 ;
            }
    }
 }
 *******)
-\* BEGIN TRANSLATION (chksum(pcal) = "63149355" /\ chksum(tla) = "b638a8a")
+\* BEGIN TRANSLATION (chksum(pcal) = "d43d362d" /\ chksum(tla) = "8dfff25d")
 VARIABLES sem, pc
 
 vars == << sem, pc >>
@@ -38,9 +46,11 @@ ncs(self) == /\ pc[self] = "ncs"
              /\ sem' = sem
 
 enter(self) == /\ pc[self] = "enter"
-               /\ sem = 1
-               /\ sem' = 0
-               /\ pc' = [pc EXCEPT ![self] = "cs"]
+               /\ IF sem = 1
+                     THEN /\ sem' = 0
+                          /\ pc' = [pc EXCEPT ![self] = "cs"]
+                     ELSE /\ pc' = [pc EXCEPT ![self] = "enter"]
+                          /\ sem' = sem
 
 cs(self) == /\ pc[self] = "cs"
             /\ TRUE

Sem.toolbox/Sem___Model_1.launch

@@ -5,7 +5,7 @@
     <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
     <intAttribute key="distributedNodesCount" value="1"/>
     <stringAttribute key="distributedTLC" value="off"/>
-    <intAttribute key="fpIndex" value="24"/>
+    <intAttribute key="fpIndex" value="10"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>