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

*From*: Saswata Paul <paulsaswata1@xxxxxxxxx>*Date*: Fri, 18 Oct 2019 13:29:42 -0400*References*: <21faa3af-ecde-490a-b824-246ceea7bc07@googlegroups.com> <00FFDC65-91F4-4E66-A0F6-F2F7D50997F5@gmail.com>

Hi,

Thank you for your reply.

In a system where two actions are permitted - SomeAction1() and
SomeAction2(), I was trying to directly prove that if
SomeAction1() happens, then var would change and that would cause SomeAction2() to begin.

I think I have to revisit and better formalize the property I want to prove.

And that \A was a typing error in G. It should have been \E.

Thank you

On Fri, Oct 18, 2019 at 12:48 PM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

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,StephanOn 18 Oct 2019, at 18:30, Saswata Paul <paulsaswata1@xxxxxxxxx> wrote:HI,I was wondering if there is a smart way to use the primed variables in the proofs in order to use them for implication chaining.For example:Let us assume we have a variable var.var = {} initiallyIf we have two rules F == \E x \in SomeSet : (var' = var \cup {x})and G == \A x \in SomeSet : x \in var => SomeAction(x)What should be the approach to prove SomeAction(x) using these two rules?...<n>1. \E x \in SomeSet : (var' = var \cup {x})PROOF<n>2. \A x \in SomeSet : x \in var => SomeAction(x)PROOF<n>3. \E x \in SomeSet : x \in var** Is there any inherent property of the primed variables that can be used to prove this from step <n>1? **<n>4. \E x \in SomeSet : SomeAction(x)BY <n>2, <n>3...Basically, the essence of my question is - since var' represents the new state of var, can we use this new state to prove something that depends on the current state? Doesn't the new state implicitly become the current state once it is updated?Thank you--

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/21faa3af-ecde-490a-b824-246ceea7bc07%40googlegroups.com.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.

To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/J18UWKvR24c/unsubscribe.

To unsubscribe from this group and all its topics, 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.

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/CAHeFUE-JqzB5rS_qxW6zJWx6eG_XBhySZs-YgW7oZN5UATXa-g%40mail.gmail.com.

**References**:**[tlaplus] Using the primed variables in proofs***From:*Saswata Paul

**Re: [tlaplus] Using the primed variables in proofs***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Using the primed variables in proofs** - Next by Date:
**Re: [tlaplus] TLA+ Conference talks?** - Previous by thread:
**Re: [tlaplus] Using the primed variables in proofs** - Next by thread:
**[tlaplus] [TLAPS] Is there a way to see the steps taken by the automated prover to prove a goal ?** - Index(es):