Sem: SF for enter

.gitignore

@@ -11,3 +11,9 @@
 *.toolbox/*/*.dot
 *.toolbox/*/*.pdf
 *.toolbox/*/*.out
+
+*.toolbox/*/*/*.st
+*.toolbox/*/*/*.fp
+*.toolbox/*/*/nodes_*
+*.toolbox/*/*/ptrs_*
+

Sem.tla

+-------------------------------- MODULE Sem --------------------------------
+EXTENDS Integers
+
+CONSTANT N
+ASSUME N \in Nat
+
+Procs == 0..N
+
+
+(*******
+--algorithm SemMutex {
+   variable sem = 1 ;
+   fair process (P \in Procs) {
+     ncs:- while (TRUE) {
+             skip ;
+     enter:+ await sem = 1 ;
+             sem := 0 ;
+         cs: skip ;
+       exit: sem := 1 ;
+           }
+   }
+}
+*******)
+\* BEGIN TRANSLATION (chksum(pcal) = "63149355" /\ chksum(tla) = "b638a8a")
+VARIABLES sem, pc
+
+vars == << sem, pc >>
+
+ProcSet == (Procs)
+
+Init == (* Global variables *)
+        /\ sem = 1
+        /\ pc = [self \in ProcSet |-> "ncs"]
+
+ncs(self) == /\ pc[self] = "ncs"
+             /\ TRUE
+             /\ pc' = [pc EXCEPT ![self] = "enter"]
+             /\ sem' = sem
+
+enter(self) == /\ pc[self] = "enter"
+               /\ sem = 1
+               /\ sem' = 0
+               /\ pc' = [pc EXCEPT ![self] = "cs"]
+
+cs(self) == /\ pc[self] = "cs"
+            /\ TRUE
+            /\ pc' = [pc EXCEPT ![self] = "exit"]
+            /\ sem' = sem
+
+exit(self) == /\ pc[self] = "exit"
+              /\ sem' = 1
+              /\ pc' = [pc EXCEPT ![self] = "ncs"]
+
+P(self) == ncs(self) \/ enter(self) \/ cs(self) \/ exit(self)
+
+Next == (\E self \in Procs: P(self))
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ \A self \in Procs : WF_vars((pc[self] # "ncs") /\ P(self)) /\ SF_vars(enter(self))
+
+\* END TRANSLATION 
+
+--------
+
+ME == INSTANCE MutualExclusionSpec WITH
+                pc <- [proc \in Procs  |->  CASE pc[proc] = "cs"            ->  "cs"
+                                              [] pc[proc] \in {"enter"}     ->  "csentry"
+                                              [] OTHER                      ->  "non-cs"]
+
+THEOREM Spec => ME!Spec
+THEOREM Spec => []ME!MutualExclusion
+THEOREM Spec => ME!Liveness
+
+=============================================================================

Sem.toolbox/.project

+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>Sem</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>toolbox.builder.TLAParserBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>toolbox.natures.TLANature</nature>
+	</natures>
+	<linkedResources>
+		<link>
+			<name>MutualExclusionSpec.tla</name>
+			<type>1</type>
+			<location>/home/kirr/study/tla+/pluscal/ME/MutualExclusionSpec.tla</location>
+		</link>
+		<link>
+			<name>Sem.tla</name>
+			<type>1</type>
+			<locationURI>PARENT-1-PROJECT_LOC/Sem.tla</locationURI>
+		</link>
+	</linkedResources>
+</projectDescription>

Sem.toolbox/.settings/org.lamport.tla.toolbox.prefs

+ProjectRootFile=PARENT-1-PROJECT_LOC/Sem.tla
+eclipse.preferences.version=1

Sem.toolbox/Sem___Model_1.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="configurationName" value="Model_1"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <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="maxHeapSize" value="25"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="sem, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <stringAttribute key="specName" value="Sem"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+</launchConfiguration>