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

*From*: Abhishek Singh <abhishek1729@xxxxxxxxx>*Date*: Wed, 9 Mar 2022 10:42:32 -0800 (PST)

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))"

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.)

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)"

"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.

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.

**Follow-Ups**:**Re: [tlaplus] On the axiomatization of state in Isabelle***From:*Stephan Merz

- Prev by Date:
**[tlaplus] TLA+ Community Survey - https://forms.gle/uLea7TR9a7uxS9tU6** - Next by Date:
**[tlaplus] Re: TLA+ Community Survey - https://forms.gle/uLea7TR9a7uxS9tU6** - Previous by thread:
**Re: [tlaplus] TLA+ Community Survey - https://forms.gle/uLea7TR9a7uxS9tU6** - Next by thread:
**Re: [tlaplus] On the axiomatization of state in Isabelle** - Index(es):