locus: Blueprint

6.5. Runs🔗

Theorem6.5.1
uses 1used by 0✓L∃∀N

A run steps from an agent under a strategy, which picks one of the matcher's steps or declines, until a goal holds or the fuel f runs out. Every run from a good agent is a chain of certified reactions: if it visits a_0, a_1, \dots, a_n then, at a common outer face,

\llbracket a_i \rrbracket \longrightarrow_{\mathcal{R}} \llbracket a_{i+1} \rrbracket \qquad (0 \le i < n) .

Rests on NEW: Occ, Run.Chain, Run.Good; not audited: Run.Strategy, Run.Trace, Run.run.

Lean code for Theorem6.5.1●3 declarations
  • theoremdefined in BigraphSim/Run.lean
    complete
    theorem run_sound {Ctrl : Type} [DecidableEq Ctrl] {S : Sig Ctrl}
  {rules : List (RuleD Ctrl)} (strat : Run.Strategy Ctrl)
  (goal : BD Ctrl → Bool) (f : Nat) (a : BD Ctrl) :
  Run.Good S a →
    Run.Chain (Run.Certified S rules)
      (Run.run S rules strat goal f a).states
    theorem run_sound {Ctrl : Type} [DecidableEq Ctrl]
  {S : Sig Ctrl}
  {rules : List (RuleD Ctrl)}
  (strat : Run.Strategy Ctrl)
  (goal : BD Ctrl → Bool) (f : Nat)
  (a : BD Ctrl) :
  Run.Good S a →
    Run.Chain (Run.Certified S rules)
      (Run.run S rules strat goal f
          a).states
    **(S5) Every run is a chain of certified reactions.**
  • defdefined in BigraphSim/Run.lean
    complete
    def run {Ctrl : Type} [DecidableEq Ctrl] (S : Sig Ctrl)
  (rules : List (RuleD Ctrl)) (strat : Run.Strategy Ctrl)
  (goal : BD Ctrl → Bool) : Nat → BD Ctrl → Run.Trace Ctrl
    def run {Ctrl : Type} [DecidableEq Ctrl]
  (S : Sig Ctrl)
  (rules : List (RuleD Ctrl))
  (strat : Run.Strategy Ctrl)
  (goal : BD Ctrl → Bool) :
  Nat → BD Ctrl → Run.Trace Ctrl
    **Run** under a strategy until the goal holds, within `f` steps.
  • defdefined in BigraphSim/Run.lean
    complete
    def Certified {Ctrl : Type} [DecidableEq Ctrl] (S : Sig Ctrl)
  (rules : List (RuleD Ctrl)) (a b : BD Ctrl) : Prop
    def Certified {Ctrl : Type} [DecidableEq Ctrl]
  (S : Sig Ctrl)
  (rules : List (RuleD Ctrl))
  (a b : BD Ctrl) : Prop
    **`a` reacts to `b`** in the library's BRS of the rule list, at a common
outer face.