| Hello, I don't understand your question. What is the overall assertion that you would like to prove? It sounds like you want to chain two actions together in a single line of reasoning. But what would this be good for: you don't control how actions are scheduled. In a behavior of your specification, after a first occurrence of the F action there might be another occurrence of the same action? And anyway a proof is purely declarative, there is no notion of dynamic system behavior or "implicit update" of state. You may want to prove an invariant of your system, and then you need to prove that both F and G maintain the invariant from any state that satisfies it, independently if they directly follow each other or not. Also note that your definition of action G looks suspicious: if SomeSet \cap var contains, say, two elements d and e, then you'd have to satisfy both SomeAction(d) and SomeAction(e), which is unlikely to work. To answer your precise question, you cannot use <n>1 to prove your step <n>3 but you can (of course) use it to prove <n>3a. \E x \in SomeSet : x \in var' \* equivalent to "SomeSet \cap var' # {}" although this is not likely to be very useful. Regards, Stephan
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/00FFDC65-91F4-4E66-A0F6-F2F7D50997F5%40gmail.com. |