CodePlexProject Hosting for Open Source Software

G' |- TLA Formula

This is done by both a kind of simple Coalescing and by determining the temporal scope of assumed formulas.

The Coalescing done is trivial. Given a formula \forall x: P(x), we replace it by the proposition C_{\forall x: P(x)}. The same is done for any other first-order formula.

This information is used by the PLTL front-end in order to affect the context of the rule. For example, if we want to apply the PLTL rule to the TLA sequent:

CONSTANT x, x = 1 |- [](x = 1)

then, we will first determine that the temporal scope of x = 1 is

[]C_{x = 1} |- []C_{x = 1}

which is a valid PLTL formula.

In general, the front-end always place a box on all assumptions which are in the

The higher-level process of determining the temporal scope of a formula is the following:

- For any formula occurring in the ASSUME section of an ASSUME/PROVE construct, we determine if it
Is Boxed. If it is, it is marked as an
**Always**formula. Otherwise, it is marked as a**Now**formula. - Each proof step in a proof has a certain temporal scope. This scope is determined as follows:
- The scope of all steps on the first level of a proof of an ASSUME/PROVE sequent are getting either the scope of the ASSUME/PROVE, or if it is
**Always**and there is a**Now**formula in the ASSUME section, then it gets a**Now**scope. - The temporal scope of a THEOREM is
**Always**.

- The scope of all steps on the first level of a proof of an ASSUME/PROVE sequent are getting either the scope of the ASSUME/PROVE, or if it is
- All asserted formulas and sequents get the temporal scope of the step they occur in. This is because they are assumed to be provable using all assumptions and once we have a
**Now**assumption, then the asserted formula is determined to be**Now**as well. On the otherhand, even if the asserted formula is not is Box but is within an**Always**scope, we know we can prove it using only**Always**assumptions and therefore it is also an**Always**formula.

The lower-level process of determining the temporal scope of a formula is the following:

- Each parsed fact get the NotSet temporal scope.
- Each parsed definition in a proof gets the
**Always**temporal scope (TODO: check for let definitions within proofs). - The anonymization process for expression (expr/e_anon) replaces the NotSet flags in Facts to be according to the Is Boxed value (TODO: check for NotSet definitions, see previous bullet).
- In p_gen and p_simplify, when we process the proofs for either simplifying the commands (p_simplify) or generating the obligations (p_gen), we carry a flag when going into deeper levels in a proof which denotes the scope of all steps on this level.
- The recursive calls for these methods from inside THEOREM get the
**Always**scope. - In the simplification process, all added assumptions (such as using HAVE or CASE) get the scope of the step.
- In the generation process we distinguish:
- Assumptions added by a USE statement (or BY which are eliminated by the simplify process). If the used formula is a definition, we use the definition temporal scope. Otherwise, we use the step temporal scope.
- Assumptions added by asserting a formula, which get the current scope. Note that the assumptions are added to the context of the next step in a normal assertion and to the nested proof in a SUFFICES assertion.
- When proving the asserted sequent (I.e. in the nested proof for normal assertions and the next step in a {{SUFFICES} assertion), we add all the assumptions of the sequent as assumptions and the scope of the nested proof is
**Always**iff it was**Always**in the sequent and there is no**Now**assumption in the sequent. - Another place where we propagate a scope is in the mutate process (in p_gen). Right now we just use the current temporal scopes for all facts added (TODO: check this).

Last edited Dec 5, 2013 at 2:20 PM by libal, version 8