The PLTL Front-end

The rule is of the form:
G |- PLTL Formula
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.

Determining the Temporal Scope of a Formula

The temporal scope can be either Now, which refers to the formula being true in a certain world, and Always, which refers to a formula being true in all following worlds.

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 Always, since it is a constant and does not change and therefore, we will obtain the following PLTL formula:
[]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 Always scope.

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

for programmers:
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