[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Confusion in TLA+ model for access control

The specification you have written seems to be assuming that UserId is
a set of strings, apparently containing the elements "u1" and "u2" and
perhaps other elements.  My guess is that you are telling TLC to set
UserId to a set whose elements are not strings.  Since you don't
report an error message, I presume that set is a set of model values.
It is helpful to readers of a spec to say what the "types" of the
spec's constants are.  The best way to do that is with an assumption
such as
   ASSUME UserId \subseteq STRING
TLC checks that assumptions are satisfied by a model.  If you had
done that, I expect that TLC would have reported an error
that would have told you exactly what your problem was.
Leslie Lamport

On Saturday, January 11, 2014 1:23:17 PM UTC-8, Reena Singh wrote:

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 ------------------
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"]]
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