How to obtain the value in a function

33 views
Skip to first unread message

Naomi Cherono

unread,
Jul 26, 2021, 6:35:33 AMJul 26
to tlaplus
Statement1==/\effect'="allow"
            /\action'="close"
            /\resource'="db1"
      
Statement2==/\effect'="deny"
            /\action'="close"
            /\resource'="db1"


Hello:

In the above statements, i need to compare the values of effect in statement1 and effect in statement2. I am learning TLA+ and would like to know the equivalent of Statement1[effect] in TLA+ (I need to return the value allow so that i can compare with  effect in Statement2)

Andrew Helwer

unread,
Jul 26, 2021, 8:29:21 AMJul 26
to tlaplus
Since this sort of value comparison across possible steps isn't something you can really do in TLA+ (other than trivially - you've hardcoded the values of these steps so you can also hardcode the comparison of "deny" = "allow", which would of course be false) the issue is with how you've chosen to model your desired behavior. What are you trying to do?

Andrew

Naomi Cherono

unread,
Jul 26, 2021, 10:28:50 AMJul 26
to tla...@googlegroups.com
I am checking a policy such as:

image.png

and i have a TLA+ representation as:

image.png
I need  a property conflict to check  where in the same statement, there is deny and allow for the same set of op and obj

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ecb11934-6cd0-4360-bd6e-a1c7acbaf2e6n%40googlegroups.com.

Andrew Helwer

unread,
Jul 26, 2021, 11:35:20 AMJul 26
to tlaplus
If you're mechanically translating policy lists to TLA+ to check them, it might not be the most ideal tool for the job - but anyway here's how you might do something like this:

--------------------------- MODULE AccessControl ---------------------------
EXTENDS Naturals, Sequences

Policy == [
    perm    : STRING,
    op      : STRING,
    obj     : STRING
]

ACL == <<
    [
        perm    |-> "allow",
        op      |-> "db1",
        obj     |-> "all"
    ],
    [
        perm    |-> "deny",
        op      |-> "db1",
        obj     |-> "all"
    ]
>>

TypeOK == ACL \in Seq(Policy)

ConflictsWith(p1, p2) ==
    /\ ACL[p1].op = ACL[p2].op
    /\ ACL[p1].obj = ACL[p2].obj
    /\ ACL[p1].perm /= ACL[p2].perm

Conflicts == {
    <<p1, p2>> \in (DOMAIN ACL) \X (DOMAIN ACL) :
        /\ p1 < p2
        /\ ConflictsWith(p1, p2)
}

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


Then you create a model with no behavior spec, got to the Model Checking Results tab, and enter the expression "Conflicts" into the "Evaluate Constant Expression" box. It will return a set of pairs of indices in the sequence that conflict with one another.

Andrew
Reply all
Reply to author
Forward
0 new messages