The DisCo Home Page

Formalization of TLA in PVS

discoev: THEORY
  BEGIN
  
  state: TYPE
  
  behavior: TYPE = [nat -> state]
  
  temporal_formula: TYPE = [behavior -> bool]
  
  state_predicate: TYPE = [state -> bool]
  
  action: TYPE = [state, state -> bool]

  stutter(A : action) : action =
    LAMBDA (unprimed, primed : state) : 
      A(unprimed, primed) or primed = unprimed
  
  []((F: temporal_formula), (b: behavior)):
      bool = FORALL (n: nat): F(suffix(b, n))
  
  statepred2temporal((P: state_predicate)):
      temporal_formula = LAMBDA (b: behavior): P(b(0))
  
  CONVERSION statepred2temporal
  
  action2temporal((A: action)): temporal_formula =
    LAMBDA (b: behavior): A(b(0), b(1))
  
  CONVERSION action2temporal
  
  invariant((P: state_predicate), (assumptions: bool),
            (I: state_predicate), (A: action)):
      bool = FORALL (b: behavior):
                assumptions AND I(b(0)) AND [](stutter(A),b) => [](P,b)
  
  preserves((single_action: action), (P: state_predicate),
            (assumptions: bool), (I: state_predicate), (A: action)):
      bool =
    FORALL (b: behavior):
      assumptions AND I(b(0)) AND [](stutter(A),b)
          => FORALL (n: nat):
          P(b(n)) AND single_action(b(n), b(n + 1)) => P(b(n + 1))
  
  invariant_rule: THEOREM
        FORALL (P: state_predicate, assumptions: bool,
                I: state_predicate, A: action):
          (FORALL (b: behavior):
             NOT (I(b(0)) AND [](stutter(A),b))
                 OR
               ((assumptions AND I(b(0)) => P(b(0)))
                    AND FORALL (n: nat):
                    assumptions AND P(b(n)) AND A(b(n), b(n + 1))
                        => P(b(n + 1))))
              => invariant(P, assumptions, I, A)
  
  invariant_intro_rule: THEOREM
        FORALL (assumptions: bool, P: state_predicate,
                I: state_predicate, A: action):
          invariant(P, assumptions, I, A)
              => FORALL (b: behavior):
              assumptions AND I(b(0))
              AND [](stutter(A),b) => FORALL (n: nat): P(b(n))
  
  invariant_implication_rule: THEOREM
        FORALL (assumptions: bool, Pstrong: state_predicate,
                Pweak: state_predicate, I: state_predicate, A: action):
          invariant(Pstrong, assumptions, I, A)
              AND (FORALL (b: behavior, n: nat):
                      assumptions and Pstrong(b(n)) => Pweak(b(n)))
              => invariant(Pweak, assumptions, I, A)
  
  objid: TYPE

  null : objid
  
  END discoev