Documentation

EqCheckingAbstractInterpretation.Trace.RunningExample

Running Example: Abstract Trace Differences #

This file formalizes the running example for abstract trace differences. We instantiate the abstract difference computation AbstractDiff for the example with processes:

PA = a.PA + a.b.0 (the P_A of the note) PB = a.(PB + b.0) (the P_B of the note) PBb0 = PB + b.0 (the reachable intermediate state) b0 = b.0 (the stopping process)

Key results:

  1. abstractDiff_PBb0_b0 : marker present for (PBb0, {b0}) → not-preordered
  2. not_abstractDiff_b0_PBb0 : marker absent for (b0, {PBb0}) → b0 ≤ PBb0
  3. not_abstractDiff_PA_PB : marker absent for (PA, {PB}) → PA ≡ PB
source
inductive EqCheckingAbstractInterpretation.Trace.RunningExample.RunAct :
Type

Actions: a and b.

Instances For
    source
    @[implicit_reducible]
    instance EqCheckingAbstractInterpretation.Trace.RunningExample.instDecidableEqRunAct :
    DecidableEq RunAct
    Equations
    source
    inductive EqCheckingAbstractInterpretation.Trace.RunningExample.RunName :
    Type

    Process names: PA and PB.

    Instances For
      source
      @[implicit_reducible]
      instance EqCheckingAbstractInterpretation.Trace.RunningExample.instDecidableEqRunName :
      DecidableEq RunName
      Equations
      source
      @[reducible, inline]
      abbrev EqCheckingAbstractInterpretation.Trace.RunningExample.RunProc :
      Type
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def EqCheckingAbstractInterpretation.Trace.RunningExample.runEnv :
        CCS.Env RunAct RunName

        Environment: PA ↦ a.PA + a.b.0 PB ↦ a.(PB + b.0)

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def EqCheckingAbstractInterpretation.Trace.RunningExample.PA :
          RunProc
          Equations
          Instances For
            source
            def EqCheckingAbstractInterpretation.Trace.RunningExample.PB :
            RunProc
            Equations
            Instances For
              source
              def EqCheckingAbstractInterpretation.Trace.RunningExample.b0 :
              RunProc
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def EqCheckingAbstractInterpretation.Trace.RunningExample.PBb0 :
                RunProc
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem EqCheckingAbstractInterpretation.Trace.RunningExample.b0_no_a_deriv (p : RunProc) :
                  ¬CCS.Deriv runEnv b0 RunAct.a p

                  b.0 has no a-derivative.

                  source
                  theorem EqCheckingAbstractInterpretation.Trace.RunningExample.derivSetOf_b0_a_empty :
                  CCS.DerivSetOf runEnv {b0} RunAct.a = fun (x : CCS.CCS RunAct RunName) => False

                  The a-shifted set of {b.0} is empty: b.0 has no a-derivative.

                  source
                  theorem EqCheckingAbstractInterpretation.Trace.RunningExample.abstractDiff_PBb0_b0 :
                  AbstractDiff runEnv PBb0 {b0}

                  Abstract trace difference is present for (PBb0, {b0}).

                  Derivation (two-step lfp construction):

                  • step: PBb0 --a--> PBb0, shifted set Der({b.0}, a) = ∅
                  • base: the empty competitor set triggers the base case of DTrSharp.
                  source
                  theorem EqCheckingAbstractInterpretation.Trace.RunningExample.b0_le_PBb0 :
                  TracePreorder runEnv b0 PBb0

                  Every trace of b0 is also a trace of PBb0: b0 = b.0 can only do b to 0, and PBb0 = PB + b.0 can also do b to 0.

                  source
                  theorem EqCheckingAbstractInterpretation.Trace.RunningExample.not_abstractDiff_b0_PBb0 :
                  ¬AbstractDiff runEnv b0 {PBb0}

                  Abstract trace difference is absent for (b0, {PBb0}).

                  b0 is concrete-trace preordered below PBb0 (every trace of b0 is a trace of PBb0), so the marker can never appear.

                  source
                  theorem EqCheckingAbstractInterpretation.Trace.RunningExample.PA_le_PB :
                  TracePreorder runEnv PA PB

                  Every trace of PA is also a trace of PB.

                  Proved by simultaneous induction on TraceSem: for every reachable successor state p of PA (i.e. p ∈ {PA, b0, zero}), every trace of p is also a trace of the corresponding PB-side state.

                  source
                  theorem EqCheckingAbstractInterpretation.Trace.RunningExample.not_abstractDiff_PA_PB :
                  ¬AbstractDiff runEnv PA {PB}

                  Abstract trace difference is absent for (PA, {PB}).

                  PA and PB have identical trace languages ({a^n | n ≥ 0} ∪ {a^n b | n ≥ 1}), so PA ≤_Tr PB and no abstract difference marker can be derived.