How to obtain the value in a function

[Naomi Cherono]

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]

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]

I am checking a policy such as:

and i have a TLA+ representation as:

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]

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