I am writing a model to check access of users on documents. If the user satisfies certain conditions document should be accessible. For example, say we have users with UserId u1, u2 and documents with DocId d1, d2. I initialize them with default values (in Init). Then I call a function, say Assign with UserId which assigns different values for the different fields depending on the value of UserId i.e. u1 or u2. Similarly, we assign values to Document d1, d2. Then we will specify other actions where states of u1, u2, d1, d2 will be changed.
Here is what I have written.
---------------MODULE acm0 ------------------
EXTENDS Naturals, TLC
CONSTANTS UserId, DocId
VARIABLES user, doc
------------------------------
User == [st:{"idle", "requesting", "accessing", "ended"}, role:{"na","pm", "operator"}, op: {"na","sp", "agg", "r", "w", "a"}]
Doc == [st:{"idle", "active", "ended"}, access: {"na","pm"}, op : {"na", "sp", "agg"}]
------------------------------
TypeOK == /\ user \in [UserId -> User]
/\ doc \in [DocId -> Doc]
Init ==
/\ user = [u \in UserId |-> [st |-> "idle", role |-> "na", op |-> "na"]]
/\ doc = [D \in DocId |-> [st |-> "idle", access |-> "na", op |-> "na"]]
Assign(uid) ==
/\ PrintT(uid)
/\ IF (uid = "u1")
THEN ( PrintT(uid) \/ user' = [uid |-> [st |-> "idle", role |-> "pm", op |-> "sp"]])
ELSE IF (uid = "u2")
THEN (PrintT(uid) /\ user' = [uid |-> [st |-> "idle", role |-> "pm", op |-> "agg"]] )
ELSE (PrintT("Nothing")/\ UNCHANGED <<user>>)
/\ PrintT(user')
## Comment-- The comparison in the If condition in above function fails always as I am comparing value to string.
AssignD(oid) ==
IF (oid = "D1")
THEN doc = [oid |-> [st |-> "idle", access |-> "pm", op |-> "sp"]]
ELSE IF (oid = "D2")
THEN doc = [oid |-> [st |-> "idle", access |-> "pm", op |-> "agg"]]
ELSE UNCHANGED <<doc>>
------------------------------
Tryaccess(uid, oid) ==
IF (user[uid].st = "idle" /\ doc[oid].st = "idle")
THEN (user' = [user EXCEPT ![uid].st = "requesting"]
/\ doc' = [doc EXCEPT ![oid].st = "active"])
ELSE UNCHANGED <<user, doc>>
Allowaccess(uid, oid) ==
IF (user[uid].st = "requesting" /\ doc[oid].st = "active" /\ user[uid].role = doc[oid].access /\ user[uid].op = doc[oid].op)
THEN (/\ user' = [user EXCEPT ![uid].st = "accessing"]
/\ doc' = [doc EXCEPT ![oid].st = "accessing"])
ELSE UNCHANGED <<user, doc>>
Next ==
\E uid \in UserId, oid \in DocId :
/\ Assign(uid)
/\ AssignD(oid)
/\ \/ Tryaccess(uid, oid)
\/ Allowaccess(uid,oid)
------------------------------
Spec == Init /\ [][Next]_<<user,doc>>
THEOREM Spec => []TypeOK
==============================
Only Init action happens. In Assign(), the If condition always evaluates to false. What is the alternative way to do this?
Thank you so much in advance