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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Mon, 26 Jul 2021 05:29:21 -0700 (PDT)*References*: <ae636808-dcf5-447b-a50a-7b86d09d4c9cn@googlegroups.com>

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 ofeffectinstatement1andeffectinstatement2. I am learning TLA+ and would like to know the equivalent ofStatement1[effect]in TLA+ (I need to return the value allow so that i can compare witheffectinStatement2)

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/ecb11934-6cd0-4360-bd6e-a1c7acbaf2e6n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Re: How to obtain the value in a function***From:*Naomi Cherono

**References**:**[tlaplus] How to obtain the value in a function***From:*Naomi Cherono

- Prev by Date:
**[tlaplus] How to obtain the value in a function** - Next by Date:
**Re: [tlaplus] Re: How to obtain the value in a function** - Previous by thread:
**[tlaplus] How to obtain the value in a function** - Next by thread:
**Re: [tlaplus] Re: How to obtain the value in a function** - Index(es):