---- MODULE OutputFolder ----EXTENDS Naturals Runs == {1, 2}NoRun == 0NoFolder == [exists |-> FALSE, by |-> NoRun, read |-> {}, notes |-> FALSE] VARIABLES pc, inputOk, snap, read, out, aside, spec, noted, wrote, broke, exitCode vars == <<pc, inputOk, snap, read, out, aside, spec, noted, wrote, broke, exitCode>> Init ==  /\ pc = [r \in Runs |-> "idle"]  /\ inputOk = [r \in Runs |-> TRUE]  /\ snap = [r \in Runs |-> 0]  /\ read = [r \in Runs |-> {}]  /\ out = NoFolder  /\ aside = [r \in Runs |-> NoFolder]  /\ spec = 1  /\ noted = FALSE  /\ wrote = [r \in Runs |-> FALSE]  /\ broke = [r \in Runs |-> FALSE]  /\ exitCode = [r \in Runs |-> "none"] Set(f, r, v) == [f EXCEPT ![r] = v]Going(r) == pc[r] \notin {"idle", "exited", "stopped", "orphanTlc"}Go(r, to) == pc' = Set(pc, r, to)Exit(r, code) == pc' = Set(pc, r, "exited") /\ exitCode' = Set(exitCode, r, code) Start(r) ==  /\ pc[r] = "idle"  /\ r = 2 => pc[1] # "idle"  /\ \E ok \in BOOLEAN : inputOk' = Set(inputOk, r, ok)  /\ snap' = Set(snap, r, spec)  /\ Go(r, "check")  /\ UNCHANGED <<read, out, aside, spec, noted, wrote, broke, exitCode>> Refuse(r) ==  /\ pc[r] = "check"  /\ ~inputOk[r] \/ out.notes  /\ Exit(r, "2")  /\ UNCHANGED <<inputOk, snap, read, out, aside, spec, noted, wrote, broke>> Tlc(r) ==  /\ \/ pc[r] = "check" /\ inputOk[r] /\ ~out.notes     \/ pc[r] = "tlc"  /\ read' = Set(read, r, read[r] \cup {spec})  /\ Go(r, IF pc[r] = "check" THEN "tlc" ELSE "draw")  /\ UNCHANGED <<inputOk, snap, out, aside, spec, noted, wrote, broke, exitCode>> Draw(r) ==  /\ pc[r] = "draw"  /\ Go(r, "publish")  /\ UNCHANGED <<inputOk, snap, read, out, aside, spec, noted, wrote, broke, exitCode>> Stale(r) ==  /\ pc[r] = "publish" /\ spec # snap[r]  /\ Exit(r, "2")  /\ UNCHANGED <<inputOk, snap, read, out, aside, spec, noted, wrote, broke>> Foreign(r) ==  /\ pc[r] = "publish" /\ spec = snap[r] /\ out.notes  /\ Exit(r, "2")  /\ UNCHANGED <<inputOk, snap, read, out, aside, spec, noted, wrote, broke>> Swap(r) ==  /\ pc[r] = "publish" /\ spec = snap[r] /\ ~out.notes  /\ Go(r, "swap")  /\ UNCHANGED <<inputOk, snap, read, out, aside, spec, noted, wrote, broke, exitCode>> MoveIn(r) ==  /\ pc[r] = "swap" /\ ~out.exists  /\ out' = [exists |-> TRUE, by |-> r, read |-> read[r], notes |-> FALSE]  /\ wrote' = Set(wrote, r, TRUE)  /\ Go(r, "clean")  /\ UNCHANGED <<inputOk, snap, read, aside, spec, noted, broke, exitCode>> MoveAside(r) ==  /\ pc[r] = "swap" /\ out.exists /\ ~aside[r].exists  /\ aside' = Set(aside, r, out)  /\ out' = NoFolder  /\ Go(r, "aside")  /\ UNCHANGED <<inputOk, snap, read, spec, noted, wrote, broke, exitCode>> Checked(r) ==  /\ pc[r] = "aside" /\ ~aside[r].notes  /\ Go(r, "swap")  /\ UNCHANGED <<inputOk, snap, read, out, aside, spec, noted, wrote, broke, exitCode>> Supersede(r) ==  /\ pc[r] = "swap" /\ out.exists /\ aside[r].exists /\ ~out.notes  /\ aside' = Set(aside, r, NoFolder)  /\ UNCHANGED <<pc, inputOk, snap, read, out, spec, noted, wrote, broke, exitCode>> Restore(r) ==  /\ pc[r] = "aside" /\ aside[r].notes /\ ~out.exists  /\ out' = aside[r]  /\ aside' = Set(aside, r, NoFolder)  /\ Exit(r, "2")  /\ UNCHANGED <<inputOk, snap, read, spec, noted, wrote, broke>> KeepAside(r) ==  /\ \/ pc[r] = "aside" /\ aside[r].notes /\ out.exists     \/ pc[r] = "swap" /\ aside[r].exists /\ out.notes  /\ Exit(r, "2")  /\ UNCHANGED <<inputOk, snap, read, out, aside, spec, noted, wrote, broke>> RenameFails(r) ==  /\ pc[r] \in {"swap", "aside"}  /\ \/ /\ aside[r].exists /\ ~out.exists        /\ out' = aside[r]        /\ aside' = Set(aside, r, NoFolder)     \/ UNCHANGED <<out, aside>>  /\ broke' = Set(broke, r, TRUE)  /\ Exit(r, "2")  /\ UNCHANGED <<inputOk, snap, read, spec, noted, wrote>> Clean(r) ==  /\ pc[r] = "clean"  /\ aside' = Set(aside, r, NoFolder)  /\ Exit(r, "0")  /\ UNCHANGED <<inputOk, snap, read, out, spec, noted, wrote, broke>> Stop(r) ==  /\ Going(r)  /\ Go(r, "stopped")  /\ UNCHANGED <<inputOk, snap, read, out, aside, spec, noted, wrote, broke, exitCode>> KillNode(r) ==  /\ pc[r] = "tlc"  /\ Go(r, "orphanTlc")  /\ UNCHANGED <<inputOk, snap, read, out, aside, spec, noted, wrote, broke, exitCode>> OrphanEnd(r) ==  /\ pc[r] = "orphanTlc"  /\ Go(r, "stopped")  /\ UNCHANGED <<inputOk, snap, read, out, aside, spec, noted, wrote, broke, exitCode>> Edit ==  /\ spec = 1  /\ spec' = 2  /\ UNCHANGED <<pc, inputOk, snap, read, out, aside, noted, wrote, broke, exitCode>> Note ==  /\ ~noted  /\ noted' = TRUE  /\ out' = [out EXCEPT !.exists = TRUE, !.notes = TRUE]  /\ UNCHANGED <<pc, inputOk, snap, read, aside, spec, wrote, broke, exitCode>> Next ==  \/ Edit \/ Note  \/ \E r \in Runs :       Start(r) \/ Refuse(r) \/ Tlc(r) \/ Draw(r) \/ Stale(r) \/ Foreign(r) \/ Swap(r)         \/ MoveIn(r) \/ MoveAside(r) \/ Checked(r) \/ Supersede(r) \/ Restore(r)         \/ KeepAside(r) \/ RenameFails(r) \/ Clean(r) \/ Stop(r) \/ KillNode(r) \/ OrphanEnd(r) Spec == Init /\ [][Next]_vars \* The folder never holds a chart drawn from two versions of the spec.ChartsOneSpec == out.read \in {{}, {1}, {2}} \* A file that you put in the folder is never deleted.KeepsYourFiles == noted => out.notes \/ \E r \in Runs : aside[r].notes \* Once a run writes a chart, the folder or a folder that a run moved aside always holds one.NeverLosesChart ==  (\E r \in Runs : wrote[r]) => out.by # NoRun \/ \E r \in Runs : aside[r].by # NoRun \* A run that exits 2 did not write the folder.ExitTwoLeavesFolder == \A r \in Runs : exitCode[r] = "2" => ~wrote[r] \* A run exits 2 only for a wrong input, an edited spec, a file that it did not write, or a failed\* rename, never because another run overlaps it.OverlapNeverRefuses ==  \A r \in Runs : exitCode[r] = "2" => ~inputOk[r] \/ spec # snap[r] \/ noted \/ broke[r]====