I fixed the original error by completing the IF statement. All 3 statements must be present IF/THEN/ELSE. However, that only introduced an new error as I don't know who to express what I'm trying to say properly in that statement still. The error is now with my my questions I asked about /\ jdState \in JD. That is the error thrown when running the checker.
In computing initial states, the right side of \IN is not enumerable.
line 35, col 9 to line 35, col 22 of module summons
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. SInit
1. Line 33, column 6 to line 38, column 16 in summons
2. Line 33, column 9 to line 33, column 44 in summons
3. Line 34, column 9 to line 34, column 43 in summons
4. Line 35, column 9 to line 35, column 22 in summons