Wei-jupiter-tla: +JupiterH for introducing history variable; +AbsJupi…

…terH for test (not passed); see Issue #37

tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.tla

@@ -1,14 +1,11 @@
 ---------------------------- MODULE AbsJupiterH ----------------------------
-(*
-AbsJupiter with a history of all list states across the system.
-*)
-EXTENDS AbsJupiter 
+EXTENDS AbsJupiter
 -------------------------------------------------------------
 VARIABLE list
 varsH == <<vars, list>>
-
-TypeOKH == TypeOK /\ (list \subseteq List)
 -------------------------------------------------------------
+TypeOKH == TypeOK /\ (list \subseteq List)
+
 InitH == Init /\ list = {InitState}
 
 DoH(c) == Do(c) /\ list' = list \cup {state'[c]}
@@ -36,5 +33,5 @@ WLSpec == \* The weak list specification
 THEOREM SpecH => WLSpec
 =============================================================================
 \* Modification History
-\* Last modified Mon Dec 31 20:38:09 CST 2018 by hengxin
-\* Created Sat Dec 15 09:00:46 CST 2018 by hengxin
+\* Last modified Tue Jan 01 10:22:57 CST 2019 by hengxin
+\* Created Sat Dec 15 09:00:46 CST 2018 by hengxin

tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/AbsJupiterH.toolbox/.project

@@ -40,6 +40,11 @@
 			<type>1</type>
 			<locationURI>PARENT-1-PROJECT_LOC/JupiterCtx.tla</locationURI>
 		</link>
+		<link>
+			<name>JupiterH.tla</name>
+			<type>1</type>
+			<location>/home/hengxin/Git-Projects/github-projects/tlaplus-lamport-projects/tlaplus-projects/Hengfeng-Wei/Wei-jupiter-tla/JupiterH.tla</location>
+		</link>
 		<link>
 			<name>JupiterInterface.tla</name>
 			<type>1</type>