Re: [tlaplus] Re: How to obtain the value in a function

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

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

On Monday, July 26, 2021 at 10:28:50 AM UTC-4 chero...@xxxxxxxxx wrote:

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

On Mon, Jul 26, 2021 at 1:29 PM Andrew Helwer <andrew...@xxxxxxxxx> wrote:

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

On Monday, July 26, 2021 at 6:35:33 AM UTC-4 chero...@xxxxxxxxx wrote:

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)

--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ecb11934-6cd0-4360-bd6e-a1c7acbaf2e6n%40googlegroups.com.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a5da6e1c-4035-4a25-bfb3-84f45c0c2755n%40googlegroups.com.