|
Hi. How to specify that a variable can non deterministicly change to one value in a set? Assume that I have a tempetarue sensor that detects the temperature, that value should be any value in the set {-273..-264} in each state. I tried many combinations such like next_temp == temp \in {-273..-264} next_temp
== temp' \in {-273..-264} But the result is either that the variable is undefined or I am comparing an integer with a set (I specified the initial value of it).
Thank you very much! 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/06fca6632f504b478c31b1f6be21c04b%40kth.se. |