---------------------------- MODULE RoostRelations ----------------------------
EXTENDS Naturals, FiniteSets

CONSTANTS r1, c1, u1, l1, Star, NoRecord, NoRead, NoList

Records == {r1, c1}
Users == {u1}
Links == {l1}
Subjects == Users \cup Links \cup {Star}
Relations == {"owner", "guest"}
Roles == {"member", "none"}

Parent(r) == IF r = c1 THEN r1 ELSE NoRecord

VARIABLES exists, tuples, linkSt, open, role, lastRead, lastList

vars == <<exists, tuples, linkSt, open, role, lastRead, lastList>>

TypeOK ==
  /\ exists \subseteq Records
  /\ tuples \subseteq (Records \X Relations \X Subjects)
  /\ linkSt \in [Links -> {"active", "revoked"}]
  /\ open \in [Records -> BOOLEAN]
  /\ role \in [Users -> Roles]
  /\ lastRead \in ({NoRead} \cup [s: Subjects, r: Records])
  /\ lastList \in ({NoList} \cup [s: Subjects, set: SUBSET Records])

Alive(s) == s \in Links => linkSt[s] = "active"

Holds(s, r) ==
  \/ s \in Users /\ role[s] = "member"
  \/ <<r, "owner", s>> \in tuples
  \/ open[r] /\ (<<r, "guest", s>> \in tuples \/ <<r, "guest", Star>> \in tuples)

Check(s, r) ==
  /\ Alive(s)
  /\ \/ Holds(s, r)
     \/ Parent(r) # NoRecord /\ Parent(r) \in exists /\ Holds(s, Parent(r))

Permitted(s) == {r \in exists : Check(s, r)}

Init ==
  /\ exists = {r1}
  /\ tuples = {}
  /\ linkSt = [l \in Links |-> "active"]
  /\ open = [r \in Records |-> FALSE]
  /\ role = [u \in Users |-> "none"]
  /\ lastRead = NoRead
  /\ lastList = NoList

Clear == lastRead' = NoRead /\ lastList' = NoList

CanHold(rel, s) == rel = "guest" \/ s \in Links

Share(r, rel, s) ==
  /\ r \in exists /\ CanHold(rel, s) /\ Alive(s)
  /\ tuples' = tuples \cup {<<r, rel, s>>}
  /\ UNCHANGED <<exists, linkSt, open, role>> /\ Clear

Unshare(r, rel, s) ==
  /\ <<r, rel, s>> \in tuples
  /\ tuples' = tuples \ {<<r, rel, s>>}
  /\ UNCHANGED <<exists, linkSt, open, role>> /\ Clear

Toggle(r) ==
  /\ open' = [open EXCEPT ![r] = ~open[r]]
  /\ UNCHANGED <<exists, tuples, linkSt, role>> /\ Clear

SetRole(u, x) ==
  /\ role' = [role EXCEPT ![u] = x]
  /\ UNCHANGED <<exists, tuples, linkSt, open>> /\ Clear

CreateByLink(r, l) ==
  /\ r \notin exists /\ linkSt[l] = "active"
  /\ exists' = exists \cup {r}
  /\ tuples' = tuples \cup {<<r, "owner", l>>}
  /\ UNCHANGED <<linkSt, open, role>> /\ Clear

Delete(r) ==
  /\ r \in exists
  /\ exists' = exists \ {r}
  /\ tuples' = {t \in tuples : t[1] # r}
  /\ UNCHANGED <<linkSt, open, role>> /\ Clear

Revoke(l) ==
  /\ linkSt[l] = "active"
  /\ linkSt' = [linkSt EXCEPT ![l] = "revoked"]
  /\ tuples' = {t \in tuples : t[3] # l}
  /\ UNCHANGED <<exists, open, role>> /\ Clear

Read(s, r) ==
  /\ r \in exists /\ Check(s, r)
  /\ lastRead' = [s |-> s, r |-> r]
  /\ lastList' = NoList
  /\ UNCHANGED <<exists, tuples, linkSt, open, role>>

List(s) ==
  /\ lastList' = [s |-> s, set |-> Permitted(s)]
  /\ lastRead' = NoRead
  /\ UNCHANGED <<exists, tuples, linkSt, open, role>>

Next ==
  \/ \E r \in Records, rel \in Relations, s \in Subjects : Share(r, rel, s) \/ Unshare(r, rel, s)
  \/ \E r \in Records : Toggle(r) \/ Delete(r)
  \/ \E u \in Users, x \in Roles : SetRole(u, x)
  \/ \E r \in Records, l \in Links : CreateByLink(r, l)
  \/ \E l \in Links : Revoke(l)
  \/ \E s \in Subjects, r \in Records : Read(s, r)
  \/ \E s \in Subjects : List(s)

Spec == Init /\ [][Next]_vars

DecisionFromCurrentState ==
  lastRead # NoRead => lastRead.r \in exists /\ Check(lastRead.s, lastRead.r)

ListIsCheck ==
  lastList # NoList => lastList.set = Permitted(lastList.s)

RevokedLinkNeverServes ==
  /\ (lastRead # NoRead /\ lastRead.s \in Links) => linkSt[lastRead.s] = "active"
  /\ (lastList # NoList /\ lastList.s \in Links /\ linkSt[lastList.s] = "revoked") => lastList.set = {}

NoOrphanTuples ==
  \A t \in tuples : t[1] \in exists /\ (t[3] \in Links => linkSt[t[3]] = "active")

VisitorOnlyThroughStar ==
  (lastRead # NoRead /\ lastRead.s = Star) =>
    \E r \in {lastRead.r} \cup ({Parent(lastRead.r)} \ {NoRecord}) : open[r] /\ <<r, "guest", Star>> \in tuples

================================================================================