Network PlusCal's instantiation of the process and algorithm layers. Everything structural — ProcState, CodeTable, Algebra, the three fixed points — is GuardedPlusCal's and is used here unchanged; see Core/GuardedPlusCal/Semantics/Process.lean.

The only difference between the two languages at this level is what a process's threads contribute. A .code thread contributes its blocks' labels and their branches, exactly as in Guarded PlusCal. A .rx thread contributes no label — it contributes one label-free step, Thread.rxStep, collected into the code table's relay component and taken by the process step with no scheduled label consumed.

def NetworkPlusCal.Process.ownedLabels (p : ComputableNetworkPlusCal.Process) : Set String

Every label a process owns, across all of its threads. A .rx thread owns none.

Equations

• NetworkPlusCal.Process.ownedLabels p = {l : String | ∃ T ∈ p.threads, l ∈ T.labels}

def NetworkPlusCal.Process.entryLabels (p : ComputableNetworkPlusCal.Process) : Set String

The label each .code thread starts at — its first block's. A .rx thread owns no label and contributes nothing.

Equations

• NetworkPlusCal.Process.entryLabels p = {l : String | ∃ T ∈ p.threads, T.labels.head? = some l}

def NetworkPlusCal.Process.codeTable {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (p : ComputableNetworkPlusCal.Process) : GuardedPlusCal.CodeTable V

The paper's Ξₚ. reducing/aborting/blocking/owned match GuardedPlusCal.Process.codeTable over the .code threads; relay collects every .rx thread's receiving step and relayBlocking says every such thread's channel is empty.

Equations

• One or more equations did not get rendered due to their size.

theorem NetworkPlusCal.Process.ownedLabels_of_reducing {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {p : ComputableNetworkPlusCal.Process} {l : String} {x : GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V × GuardedPlusCal.LocalState V} (hx : x ∈ (codeTable Ξ Ω p).reducing l) : l ∈ ownedLabels p

A step at a label is a step of some thread's own block, so the label is one the process owns — codeTable's "absent label is unschedulable" convention, read the other way round. Used at the algorithm level to derive l ∈ ownedLabels p' straight from the step in hand, rather than carrying ownership as a separate hypothesis to case on.

theorem NetworkPlusCal.Process.ownedLabels_of_aborting {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {p : ComputableNetworkPlusCal.Process} {l : String} {x : GuardedPlusCal.LocalState V × GuardedPlusCal.Trace V} (hx : x ∈ (codeTable Ξ Ω p).aborting l) : l ∈ ownedLabels p

A step at a label is a step of some thread's own block, so the label is one the process owns — codeTable's "absent label is unschedulable" convention, read the other way round. Used at the algorithm level to derive l ∈ ownedLabels p' straight from the step in hand, rather than carrying ownership as a separate hypothesis to case on.

Instantiating the algorithm layer

ι = String × V: an instance is a declared process's name paired with the identity it runs under, so every lookup below resolves the name against algo.processes and reads this language's codeTable/ownedLabels/entryLabels off the process it finds.

def NetworkPlusCal.Algorithm.algebra {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (algo : ComputableNetworkPlusCal.Algorithm) : GuardedPlusCal.Algebra V

Assembles a whole Algorithm's Algebra.

Equations

• One or more equations did not get rendered due to their size.

def NetworkPlusCal.Process.identities {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (p : ComputableNetworkPlusCal.Process) : Set V

The instance identities a declared process contributes, read off its =/∈ form and its id expression.

Equations

• NetworkPlusCal.Process.identities Ξ Ω p = GuardedPlusCal.identitiesOf Ξ Ω p.«=|∈» p.id

theorem NetworkPlusCal.Process.identities_eq {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {p : ComputableNetworkPlusCal.Process} : identities Ξ Ω p = GuardedPlusCal.identitiesOf Ξ Ω p.«=|∈» p.id

Process.identities reads nothing but the two fields, which is what lets a pass preserving them preserve the instances by rewriting.

def NetworkPlusCal.Process.inits (p : ComputableNetworkPlusCal.Process) : List (String × ComputablePlusCal.Expression)

A declared process's local initializers, in the shape InitProc takes them.

Equations

• NetworkPlusCal.Process.inits p = GuardedPlusCal.initsOf p.localState.variables

theorem NetworkPlusCal.Process.inits_eq {p : ComputableNetworkPlusCal.Process} : inits p = GuardedPlusCal.initsOf p.localState.variables

Process.inits reads nothing but the declared locals, which is what lets a pass that only extends the locals say so.

def NetworkPlusCal.Algorithm.init {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (algo : ComputableNetworkPlusCal.Algorithm) : GuardedPlusCal.AlgState (String × V) V → Prop

A valid initial state: the instance map holds exactly one state per declared process and identity, each at that process's entry labels under its declared initializers, and every declared channel starts empty. A characterization of membership, not an existence claim.

Equations

• One or more equations did not get rendered due to their size.