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?
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)