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