Using the primed variables in proofs

19 views
Skip to first unread message

Saswata Paul

unread,
Oct 18, 2019, 12:30:54 PM10/18/19
to tlaplus
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 = {} initially
   
   If 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

Stephan Merz

unread,
Oct 18, 2019, 12:48:51 PM10/18/19
to tla...@googlegroups.com
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/21faa3af-ecde-490a-b824-246ceea7bc07%40googlegroups.com.

Saswata Paul

unread,
Oct 18, 2019, 1:29:55 PM10/18/19
to tla...@googlegroups.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


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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/00FFDC65-91F4-4E66-A0F6-F2F7D50997F5%40gmail.com.
Reply all
Reply to author
Forward
0 new messages