Re: [tlaplus] On the axiomatization of state in Isabelle

Also, as far as I know these Isabelle theories have not been used for any serious verification attempt. In particular, the part about quantification over state variables that you refer to is really experimental, and I expect changes to be necessary.

On 9 Mar 2022, at 19:42, Abhishek Singh <abhishek1729@xxxxxxxxx> wrote:

Hi.

I have a few questions about the Isabelle AFP on TLA (https://www.isa-afp.org/entries/TLA.html). If this is not the right forum to ask questions about this, please redirect me to the correct forum.

1. The history axiom in State.thy says:

history: "⊢ (I ∧ □[A]_v) = (∃∃ h. ($h = ha) ∧ I ∧ □[A ∧ h$=hb]_(h,v))"

but this does not allow me to replace sub-actions that are more nested, as described in Th. 1 (http://lamport.azurewebsites.net/tla/auxiliary/auxiliary.html). Is it advisable to add more history axioms? e.g.

history2: "⊢ (I ∧ □[A ∨ (∃i. P i)]_v) = (∃∃ h. ($h = ha) ∧ I ∧ □[A ∨ (∃i. P i ∧ h$=hc i)]_(h,v))"

I would expect that you'd rather like to have

⊢ (I ∧ □[A ∨ (∃i. P i)]_v) = (∃∃ h. ($h = ha) ∧ I ∧ □[(A /\ h$ = $h) ∨ (∃i. P i ∧ h$=hc i)]_(h,v))

so that h is not left unconstrained for A action. Can't you get this from the above by instantiating hb by something along the lines of

if A then $h else (CHOOSE i : P i /\ hc i)

2. Unlike history variables one-prediction prophecy variables seem to require appending either PredA(p)∧(p′ ∈Π) or (p′=p) to all sub-actions (from equations 4.4 and 4.5 in http://lamport.azurewebsites.net/tla/auxiliary/auxiliary.html) but this requirement is harder to state as an axiom. Is it possible to support prophecy variables axiomatically in the AFP? (My requirement is most likely satisfied by prophecy data structure variables.)

Not having had any significant experience with prophecy variables, I didn't dare write an axiom for them in Isabelle. You'll want to experiment to see what works for you.

3. The eexE axiom says:

eexE: "⟦s ⊨ (∃∃ x. F x) ; basevars vs; (⋀ x. ⟦ basevars (x,vs); s ⊨ F x ⟧ ⟹ s ⊨ G)⟧ ⟹ (s ⊨ G)"
but basevars and vs do not seem to interact with formulas F and G; would the following simpler axiom be unsound?

eexE: "⟦s ⊨ (∃∃ x. F x); (⋀ x. s ⊨ F x ⟹ s ⊨ G)⟧ ⟹ (s ⊨ G)"

This is sound but weaker. The "basevars" predicate is a hack in order to distinguish state variables from other state functions. The predicate is used for reasoning about ENABLED, and the above axiom allows you to treat the bound variable x as any other state variable in that context.

Further information: The reason for my interest in the Isabelle AFP is that I need to prove a property of the form
"s ⊨ ∀∀ x. P x ⟶ □Q x ⟹ s ⊨ ∀∀ y. R y ⟶ □S y"
i.e. the system R is safe (S) if the system P is safe (Q) where the rigid variables in P and R satisfy some relationship. Equivalently, I need to show
"s ⊨ ∃∃y. R y ∧ ◇¬S y ⟹ s ⊨ ∃∃ x. P x ∧ ◇¬Q x"
but this is not a standard TLA+ specification, and I felt that the Isabelle AFP might be a better system to try to formalize the proof of the above property than say TLAPS.

Indeed, if you need history or prophecy variables in these reductions, TLAPS won't be able to help you at this point. If the relationship between the variables can be expressed as a refinement mapping, you can instantiate the specification of R in the module that defines system P.

Regards,

Stephan

Any help is appreciated.

-Abhishek

--
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/614e6577-d96d-4db5-b950-47d651f53331n%40googlegroups.com.