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

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

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:


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.