Alternating bit protocol

InductiveAlternating-bit channel names#✓fully proved

The channel names of the alternating-bit protocol are \(\mathit{acc}\) (accept a message from the user), \(\mathit{del}\) (deliver a message to the user), and, for each bit \(b\), the internal names \(\mathit{send}_b\) (sender to data channel), \(\mathit{recv}_b\) (data channel to receiver), \(\mathit{reply}_b\) (receiver to acknowledgement channel) and \(\mathit{ack}_b\) (acknowledgement channel to sender).

inductive Name
  /-- Accept a message from the user. -/
  | acc
  /-- Deliver a message to the user. -/
  | del
  /-- Sender to data channel. -/
  | send (b : Bool)
  /-- Data channel to receiver. -/
  | recv (b : Bool)
  /-- Receiver to acknowledgement channel. -/
  | reply (b : Bool)
  /-- Acknowledgement channel to sender. -/
  | ack (b : Bool)
  deriving DecidableEq

Used by 15

Used byThe data-free alternating-bit protocol · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Transitions of the acknowledgement channel in the data-free alternating-bit protocol · The data-free one-place buffer · The data-free one-place buffer in a given state · Transitions of the data-free one-place buffer · Alternating-bit configuration transitions · Alternating-bit data channel transitions · Internal channels of the alternating-bit protocol · Alternating-bit transition system · Alternating-bit receiver transitions · Alternating-bit sender transitions · Recursive specification of the data-free alternating-bit protocol · The alternating-bit protocol in a configuration

InductiveSender states of the data-free alternating-bit protocol#✓fully proved

For each bit \(b\), the sender has three states: \(\mathrm{accept}(b)\), ready to accept a message to be sent with bit \(b\); \(\mathrm{transmit}(b)\), about to transmit a frame tagged with bit \(b\); and \(\mathrm{await}(b)\), waiting for the acknowledgement of bit \(b\). These six states are all the sender states.

inductive Sender
  /-- Ready to accept a message, to be sent with this bit. -/
  | accept (b : Bool)
  /-- About to transmit a frame with this bit. -/
  | transmit (b : Bool)
  /-- Waiting for the acknowledgement of this bit. -/
  | await (b : Bool)
  deriving DecidableEq

Used by 10

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Process constants of the data-free alternating-bit protocol · Weak-bisimulation certificate for the data-free alternating-bit protocol · Alternating-bit configuration · Alternating-bit configuration transitions · Initial alternating-bit configuration · Alternating-bit sender transitions · Recursive specification of the data-free alternating-bit protocol · The alternating-bit protocol in a configuration

InductiveStates of a one-place channel#✓fully proved

A one-place channel is either empty or full, holding a single bit.

inductive Channel
  | empty
  | full (b : Bool)
  deriving DecidableEq

Used by 11

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Transitions of the acknowledgement channel in the data-free alternating-bit protocol · Process constants of the data-free alternating-bit protocol · Weak-bisimulation certificate for the data-free alternating-bit protocol · Alternating-bit configuration · Alternating-bit configuration transitions · Alternating-bit data channel transitions · Initial alternating-bit configuration · Recursive specification of the data-free alternating-bit protocol · The alternating-bit protocol in a configuration

InductiveAlternating-bit receiver states#✓fully proved

A state of the alternating-bit receiver is, for a bit \(b\), either expecting a frame with bit \(b\), about to deliver the message of a frame with bit \(b\), or about to acknowledge bit \(b\).

inductive Receiver
  /-- Expecting a frame with this bit. -/
  | expect (b : Bool)
  /-- About to deliver the message of a frame with this bit. -/
  | deliver (b : Bool)
  /-- About to acknowledge this bit. -/
  | reply (b : Bool)
  deriving DecidableEq

Used by 10

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Process constants of the data-free alternating-bit protocol · Weak-bisimulation certificate for the data-free alternating-bit protocol · Alternating-bit configuration · Alternating-bit configuration transitions · Initial alternating-bit configuration · Alternating-bit receiver transitions · Recursive specification of the data-free alternating-bit protocol · The alternating-bit protocol in a configuration

DefinitionAlternating-bit sender transitions#✓fully proved

The sender of the alternating-bit protocol has the following transitions. Ready to accept with bit \(b\), it can input on \(\mathit{acc}\) and become about to transmit \(b\). About to transmit \(b\), it can output on \(\mathit{send}_b\) and then await the acknowledgement of \(b\). Awaiting the acknowledgement of \(b\), it can input on \(\mathit{ack}_b\) and become ready to accept with bit \(\lnot b\), input on \(\mathit{ack}_{\lnot b}\) and keep waiting, or time out by a silent step and become about to transmit \(b\) again.

def senderSteps : Sender → List (Label Name × Sender)
  | .accept b => [(.input .acc, .transmit b)]
  | .transmit b => [(.output (.send b), .await b)]
  | .await b =>
      [(.input (.ack b), .accept (!b)), (.input (.ack (!b)), .await b), (.tau, .transmit b)]

Uses 3 · Used by 4

Statement usesAlternating-bit channel names · Sender states of the data-free alternating-bit protocol · CCS labels

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Alternating-bit configuration transitions · Recursive specification of the data-free alternating-bit protocol

DefinitionAlternating-bit data channel transitions#✓fully proved

The one-place data channel of the alternating-bit protocol has the following transitions. When empty, it can input on \(\mathit{send}_b\) and become full with bit \(b\), for each bit \(b\). When full with bit \(b\), it can output on \(\mathit{recv}_b\) and become empty, or lose the bit by a silent step and become empty.

def dataSteps : Channel → List (Label Name × Channel)
  | .empty => [(.input (.send false), .full false), (.input (.send true), .full true)]
  | .full b => [(.output (.recv b), .empty), (.tau, .empty)]

Uses 3 · Used by 4

Statement usesStates of a one-place channel · Alternating-bit channel names · CCS labels

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Alternating-bit configuration transitions · Recursive specification of the data-free alternating-bit protocol

DefinitionAlternating-bit receiver transitions#✓fully proved

The receiver of the alternating-bit protocol has the following transitions. Expecting bit \(b\), it can input on \(\mathit{recv}_b\) and become ready to deliver \(b\), or input on \(\mathit{recv}_{\lnot b}\) and become ready to acknowledge \(\lnot b\). Ready to deliver \(b\), it can output on \(\mathit{del}\) and become ready to acknowledge \(b\). Ready to acknowledge \(b\), it can output on \(\mathit{reply}_b\) and then expect \(\lnot b\).

def receiverSteps : Receiver → List (Label Name × Receiver)
  | .expect b => [(.input (.recv b), .deliver b), (.input (.recv (!b)), .reply (!b))]
  | .deliver b => [(.output .del, .reply b)]
  | .reply b => [(.output (.reply b), .expect (!b))]

Uses 3 · Used by 4

Statement usesAlternating-bit channel names · Alternating-bit receiver states · CCS labels

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Alternating-bit configuration transitions · Recursive specification of the data-free alternating-bit protocol

DefinitionTransitions of the acknowledgement channel in the data-free alternating-bit protocol#✓fully proved

When empty, the lossy one-place acknowledgement channel can, for either bit \(b\), input on \(\mathit{reply}_b\) and become full with bit \(b\). When full with bit \(b\), it can output on \(\mathit{ack}_b\) or make a silent \(\tau\) step (losing the bit), in both cases becoming empty. These are all its transitions.

def ackSteps : Channel → List (Label Name × Channel)
  | .empty => [(.input (.reply false), .full false), (.input (.reply true), .full true)]
  | .full b => [(.output (.ack b), .empty), (.tau, .empty)]

Uses 3 · Used by 4

Statement usesStates of a one-place channel · Alternating-bit channel names · CCS labels

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Alternating-bit configuration transitions · Recursive specification of the data-free alternating-bit protocol

DefinitionTransitions of the data-free one-place buffer#✓fully proved

The one-place buffer has two states, empty (false) and full (true). When empty, its only transition is an input on \(\mathit{acc}\) to the full state; when full, its only transition is an output on \(\mathit{del}\) to the empty state.

def bufferSteps : Bool → List (Label Name × Bool)
  | false => [(.input .acc, true)]
  | true => [(.output .del, false)]

Uses 2 · Used by 3

Statement usesAlternating-bit channel names · CCS labels

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Recursive specification of the data-free alternating-bit protocol

InductiveProcess constants of the data-free alternating-bit protocol#✓fully proved

There is one process constant for each sender state, each state of the data channel, each receiver state, each state of the acknowledgement channel, and each state of the one-place buffer (empty or full).

inductive Agent
  | sender (s : Sender)
  | data (c : Channel)
  | receiver (r : Receiver)
  | ack (c : Channel)
  | buffer (full : Bool)

Uses 3 · Used by 8

Statement usesStates of a one-place channel · Alternating-bit receiver states · Sender states of the data-free alternating-bit protocol

Used byThe data-free alternating-bit protocol · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · The data-free one-place buffer · The data-free one-place buffer in a given state · Alternating-bit transition system · Recursive specification of the data-free alternating-bit protocol · The alternating-bit protocol in a configuration

DefinitionRecursive specification of the data-free alternating-bit protocol#✓fully proved

The process constants are the states of the five agents: the sender, the data channel, the receiver, the acknowledgement channel and the one-place buffer. For a state \(x\) of one of these agents, let \((a_1, x_1), \dots, (a_n, x_n)\) be the transitions of \(x\) as listed by the transition function of its agent, let \(X_i\) be the constant of the same agent at state \(x_i\), and let \(\mathbf{0}\) be the inactive process. The specification defines the constant of \(x\) as the choice of prefixes \(a_1.X_1 + (a_2.X_2 + \cdots + (a_n.X_n + \mathbf{0}))\).

def spec : Specification Name Agent
  | .sender s => sumOf ((senderSteps s).map fun y => (y.1, .constant (.sender y.2)))
  | .data c => sumOf ((dataSteps c).map fun y => (y.1, .constant (.data y.2)))
  | .receiver r => sumOf ((receiverSteps r).map fun y => (y.1, .constant (.receiver y.2)))
  | .ack c => sumOf ((ackSteps c).map fun y => (y.1, .constant (.ack y.2)))
  | .buffer b => sumOf ((bufferSteps b).map fun y => (y.1, .constant (.buffer y.2)))

Uses 14 · Used by 3

Statement usesProcess constants of the data-free alternating-bit protocol · States of a one-place channel · Alternating-bit channel names · Alternating-bit receiver states · Sender states of the data-free alternating-bit protocol · Transitions of the acknowledgement channel in the data-free alternating-bit protocol · Transitions of the data-free one-place buffer · Alternating-bit data channel transitions · Alternating-bit receiver transitions · Alternating-bit sender transitions · Sum of prefixes · CCS labels · Recursive CCS processes · Recursive CCS specification

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Alternating-bit transition system

AbbreviationAlternating-bit transition system#✓fully proved

The labelled transition system whose states are the CCS processes over the alternating-bit channel names and process constants, whose labels are the CCS labels over those names, and whose transitions are the steps of the CCS operational semantics for the recursive specification that defines each process constant (one per state of the sender, the data channel, the receiver, the acknowledgement channel and the one-place buffer) as the choice of its listed transitions.

abbrev lts : LTS (Process Name Agent) (Label Name) := Process.lts spec

Uses 6 · Used by 2

Statement usesProcess constants of the data-free alternating-bit protocol · Alternating-bit channel names · Recursive specification of the data-free alternating-bit protocol · CCS labels · Recursive CCS processes · Labelled transition system of a recursive specification

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer

DefinitionInternal channels of the alternating-bit protocol#✓fully proved

The internal channel names, all of which the protocol restricts, are \(\mathit{send}_b\), \(\mathit{recv}_b\), \(\mathit{reply}_b\) and \(\mathit{ack}_b\) for both bits \(b\), that is, every channel name except \(\mathit{acc}\) and \(\mathit{del}\).

def internal : List Name :=
  [.send false, .send true, .recv false, .recv true, .reply false, .reply true,
    .ack false, .ack true]

Uses 1 · Used by 4

Statement usesAlternating-bit channel names

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Alternating-bit configuration transitions · The alternating-bit protocol in a configuration

AbbreviationAlternating-bit configuration#✓fully proved

A configuration of the alternating-bit protocol consists of a sender state, a state of the data channel, a receiver state and a state of the acknowledgement channel.

abbrev Config := ((Sender × Channel) × Receiver) × Channel

Uses 3 · Used by 6

Statement usesStates of a one-place channel · Alternating-bit receiver states · Sender states of the data-free alternating-bit protocol

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Weak-bisimulation certificate for the data-free alternating-bit protocol · Alternating-bit configuration transitions · Initial alternating-bit configuration · The alternating-bit protocol in a configuration

DefinitionThe alternating-bit protocol in a configuration#✓fully proved

Consider a configuration with sender state \(s\), data channel state \(d\), receiver state \(r\) and acknowledgement channel state \(k\). Write \(\mathrm{Sender}(s)\), \(\mathrm{Data}(d)\), \(\mathrm{Receiver}(r)\) and \(\mathrm{Ack}(k)\) for the constants of the four agents at these states, and let \(L\) be the set of internal channels \(\mathrm{send}(b)\), \(\mathrm{recv}(b)\), \(\mathrm{reply}(b)\) and \(\mathrm{ack}(b)\) for both bits \(b\). The protocol process is the parallel composition of these constants with every internal channel restricted, \((((\mathrm{Sender}(s) \mid \mathrm{Data}(d)) \mid \mathrm{Receiver}(r)) \mid \mathrm{Ack}(k)) \setminus L\).

def system (c : Config) : Process Name Agent :=
  .restriction internal
    (.parallel (.parallel (.parallel (.constant (.sender c.1.1.1)) (.constant (.data c.1.1.2)))
      (.constant (.receiver c.1.2))) (.constant (.ack c.2)))

Uses 8 · Used by 3

Statement usesProcess constants of the data-free alternating-bit protocol · States of a one-place channel · Alternating-bit configuration · Alternating-bit channel names · Alternating-bit receiver states · Sender states of the data-free alternating-bit protocol · Internal channels of the alternating-bit protocol · Recursive CCS processes

Used byThe data-free alternating-bit protocol · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer

DefinitionAlternating-bit configuration transitions#✓fully proved

The transitions of a configuration of the alternating-bit protocol, listed as pairs of a label and a successor configuration, are obtained by composing the transitions of the sender, the data channel, the receiver and the acknowledgement channel in parallel, in that order (at each stage either side moves alone, or the two sides synchronize on an input and the complementary output on the same channel name, giving a silent step), and then keeping only the silent steps and the steps whose channel name is not one of the internal channel names.

def configSteps : Config → List (Label Name × Config) :=
  restrictSteps internal (parSteps (parSteps (parSteps senderSteps dataSteps) receiverSteps)
    ackSteps)

Uses 13 · Used by 2

Statement usesStates of a one-place channel · Alternating-bit configuration · Alternating-bit channel names · Alternating-bit receiver states · Sender states of the data-free alternating-bit protocol · Transitions of the acknowledgement channel in the data-free alternating-bit protocol · Alternating-bit data channel transitions · Internal channels of the alternating-bit protocol · Alternating-bit receiver transitions · Alternating-bit sender transitions · Code-level parallel composition · Code-level restriction · CCS labels

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer

DefinitionThe data-free one-place buffer in a given state#✓fully proved

For a Boolean \(f\), \(\mathit{buffer}(f)\) is the process constant for the one-place buffer that is full if \(f\) is true and empty if \(f\) is false.

def buffer (full : Bool) : Process Name Agent := .constant (.buffer full)

Uses 3 · Used by 3

Statement usesProcess constants of the data-free alternating-bit protocol · Alternating-bit channel names · Recursive CCS processes

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · The data-free one-place buffer

DefinitionInitial alternating-bit configuration#✓fully proved

The initial configuration of the alternating-bit protocol has the sender ready to accept a message with bit \(\mathrm{false}\), both channels empty, and the receiver expecting bit \(\mathrm{false}\).

def initial : Config := (((.accept false, .empty), .expect false), .empty)

Uses 4 · Used by 3

Statement usesStates of a one-place channel · Alternating-bit configuration · Alternating-bit receiver states · Sender states of the data-free alternating-bit protocol

Used byThe data-free alternating-bit protocol · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer

DefinitionThe data-free alternating-bit protocol#✓fully proved

The process \(\mathit{abp}\) is the protocol in its initial configuration: the parallel composition of the sender, the lossy one-place data channel, the receiver and the lossy one-place acknowledgement channel, with all eight internal channels \(\mathit{send}_b\), \(\mathit{recv}_b\), \(\mathit{reply}_b\) and \(\mathit{ack}_b\) (for both bits \(b\)) restricted, where the sender is ready to accept a message to be sent with bit \(0\), both channels are empty, and the receiver expects bit \(0\).

def abp : Process Name Agent := system initial

Uses 5 · Used by 2

Statement usesProcess constants of the data-free alternating-bit protocol · Alternating-bit channel names · Initial alternating-bit configuration · The alternating-bit protocol in a configuration · Recursive CCS processes

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer

DefinitionThe data-free one-place buffer#✓fully proved

The process \(\mathit{buf}\) is the one-place buffer in its empty state. By the specification it accepts on \(\mathit{acc}\) and becomes full, and the full buffer delivers on \(\mathit{del}\) and becomes empty again, so \(\mathit{buf} = \mathit{acc}.\overline{\mathit{del}}.\mathit{buf}\).

def buf : Process Name Agent := buffer false

Uses 4 · Used by 2

Statement usesProcess constants of the data-free alternating-bit protocol · Alternating-bit channel names · The data-free one-place buffer in a given state · Recursive CCS processes

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer

DefinitionWeak-bisimulation certificate for the data-free alternating-bit protocol#✓fully proved

The list of every reachable protocol configuration, paired with the buffer state it simulates (full from the accept of a message until its delivery), sorted by silent distance to the next visible action.

Cslib.Algorithms.CCS.AlternatingBit.certificate · 109 lines

def certificate : List (Config × Bool) := [
  (((((.accept false), (.full true)), (.expect false)), (.full true)), false),
  (((((.accept false), (.full true)), (.expect false)), .empty), false),
  (((((.accept false), (.full true)), (.reply true)), .empty), false),
  (((((.accept false), .empty), (.expect false)), (.full true)), false),
  (((((.accept false), .empty), (.expect false)), .empty), false),
  (((((.accept false), .empty), (.reply true)), (.full true)), false),
  (((((.accept false), .empty), (.reply true)), .empty), false),
  (((((.accept true), (.full false)), (.expect true)), (.full false)), false),
  (((((.accept true), (.full false)), (.expect true)), .empty), false),
  (((((.accept true), (.full false)), (.reply false)), .empty), false),
  (((((.accept true), .empty), (.expect true)), (.full false)), false),
  (((((.accept true), .empty), (.expect true)), .empty), false),
  (((((.accept true), .empty), (.reply false)), (.full false)), false),
  (((((.accept true), .empty), (.reply false)), .empty), false),
  (((((.await false), (.full false)), (.expect true)), (.full false)), false),
  (((((.await false), (.full false)), (.reply false)), (.full false)), false),
  (((((.await false), .empty), (.expect true)), (.full false)), false),
  (((((.await false), .empty), (.reply false)), (.full false)), false),
  (((((.await true), (.full true)), (.expect false)), (.full true)), false),
  (((((.await true), (.full true)), (.reply true)), (.full true)), false),
  (((((.await true), .empty), (.expect false)), (.full true)), false),
  (((((.await true), .empty), (.reply true)), (.full true)), false),
  (((((.await false), (.full false)), (.reply false)), .empty), false),
  (((((.await false), .empty), (.reply false)), .empty), false),
  (((((.await true), (.full true)), (.reply true)), .empty), false),
  (((((.await true), .empty), (.reply true)), .empty), false),
  (((((.transmit false), .empty), (.expect true)), (.full false)), false),
  (((((.transmit false), .empty), (.reply false)), (.full false)), false),
  (((((.transmit true), .empty), (.expect false)), (.full true)), false),
  (((((.transmit true), .empty), (.reply true)), (.full true)), false),
  (((((.await false), (.full false)), (.expect true)), .empty), false),
  (((((.await false), (.full false)), (.reply false)), (.full true)), false),
  (((((.await false), .empty), (.reply false)), (.full true)), false),
  (((((.await true), (.full true)), (.expect false)), .empty), false),
  (((((.await true), (.full true)), (.reply true)), (.full false)), false),
  (((((.await true), .empty), (.reply true)), (.full false)), false),
  (((((.transmit false), (.full false)), (.expect true)), (.full false)), false),
  (((((.transmit false), (.full false)), (.reply false)), (.full false)), false),
  (((((.transmit false), .empty), (.reply false)), .empty), false),
  (((((.transmit true), (.full true)), (.expect false)), (.full true)), false),
  (((((.transmit true), (.full true)), (.reply true)), (.full true)), false),
  (((((.transmit true), .empty), (.reply true)), .empty), false),
  (((((.transmit false), (.full false)), (.expect true)), .empty), false),
  (((((.transmit false), (.full false)), (.reply false)), .empty), false),
  (((((.transmit false), .empty), (.expect true)), .empty), false),
  (((((.transmit false), .empty), (.reply false)), (.full true)), false),
  (((((.transmit true), (.full true)), (.expect false)), .empty), false),
  (((((.transmit true), (.full true)), (.reply true)), .empty), false),
  (((((.transmit true), .empty), (.expect false)), .empty), false),
  (((((.transmit true), .empty), (.reply true)), (.full false)), false),
  (((((.await false), .empty), (.expect true)), .empty), false),
  (((((.await true), .empty), (.expect false)), .empty), false),
  (((((.transmit false), (.full false)), (.reply false)), (.full true)), false),
  (((((.transmit true), (.full true)), (.reply true)), (.full false)), false),
  (((((.await false), (.full false)), (.deliver false)), (.full true)), true),
  (((((.await false), (.full false)), (.deliver false)), .empty), true),
  (((((.await false), .empty), (.deliver false)), (.full true)), true),
  (((((.await false), .empty), (.deliver false)), .empty), true),
  (((((.await true), (.full true)), (.deliver true)), (.full false)), true),
  (((((.await true), (.full true)), (.deliver true)), .empty), true),
  (((((.await true), .empty), (.deliver true)), (.full false)), true),
  (((((.await true), .empty), (.deliver true)), .empty), true),
  (((((.transmit false), (.full false)), (.deliver false)), (.full true)), true),
  (((((.transmit false), (.full false)), (.deliver false)), .empty), true),
  (((((.transmit false), .empty), (.deliver false)), (.full true)), true),
  (((((.transmit false), .empty), (.deliver false)), .empty), true),
  (((((.transmit true), (.full true)), (.deliver true)), (.full false)), true),
  (((((.transmit true), (.full true)), (.deliver true)), .empty), true),
  (((((.transmit true), .empty), (.deliver true)), (.full false)), true),
  (((((.transmit true), .empty), (.deliver true)), .empty), true),
  (((((.await false), (.full false)), (.expect false)), (.full true)), true),
  (((((.await false), (.full false)), (.expect false)), .empty), true),
  (((((.await true), (.full true)), (.expect true)), (.full false)), true),
  (((((.await true), (.full true)), (.expect true)), .empty), true),
  (((((.transmit false), (.full false)), (.expect false)), (.full true)), true),
  (((((.transmit false), (.full false)), (.expect false)), .empty), true),
  (((((.transmit true), (.full true)), (.expect true)), (.full false)), true),
  (((((.transmit true), (.full true)), (.expect true)), .empty), true),
  (((((.await false), (.full false)), (.reply true)), .empty), true),
  (((((.await true), (.full true)), (.reply false)), .empty), true),
  (((((.transmit false), (.full false)), (.reply true)), .empty), true),
  (((((.transmit false), .empty), (.expect false)), (.full true)), true),
  (((((.transmit false), .empty), (.expect false)), .empty), true),
  (((((.transmit true), (.full true)), (.reply false)), .empty), true),
  (((((.transmit true), .empty), (.expect true)), (.full false)), true),
  (((((.transmit true), .empty), (.expect true)), .empty), true),
  (((((.await false), (.full false)), (.reply true)), (.full true)), true),
  (((((.await false), .empty), (.expect false)), (.full true)), true),
  (((((.await false), .empty), (.expect false)), .empty), true),
  (((((.await true), (.full true)), (.reply false)), (.full false)), true),
  (((((.await true), .empty), (.expect true)), (.full false)), true),
  (((((.await true), .empty), (.expect true)), .empty), true),
  (((((.transmit false), (.full false)), (.reply true)), (.full true)), true),
  (((((.transmit false), (.full true)), (.expect false)), (.full true)), true),
  (((((.transmit false), .empty), (.reply true)), .empty), true),
  (((((.transmit true), (.full false)), (.expect true)), (.full false)), true),
  (((((.transmit true), (.full false)), (.expect true)), .empty), true),
  (((((.transmit true), (.full true)), (.reply false)), (.full false)), true),
  (((((.transmit true), .empty), (.reply false)), .empty), true),
  (((((.await false), .empty), (.reply true)), .empty), true),
  (((((.await true), .empty), (.reply false)), .empty), true),
  (((((.transmit false), (.full true)), (.expect false)), .empty), true),
  (((((.transmit false), (.full true)), (.reply true)), .empty), true),
  (((((.transmit false), .empty), (.reply true)), (.full true)), true),
  (((((.transmit true), (.full false)), (.reply false)), .empty), true),
  (((((.transmit true), .empty), (.reply false)), (.full false)), true),
  (((((.await false), .empty), (.reply true)), (.full true)), true),
  (((((.await true), .empty), (.reply false)), (.full false)), true)]

Uses 4 · Used by 2

Statement usesStates of a one-place channel · Alternating-bit configuration · Alternating-bit receiver states · Sender states of the data-free alternating-bit protocol

Used byThe alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer

TheoremThe alternating-bit protocol implements a one-place buffer#✓fully proved

In the labelled transition system of the protocol's recursive CCS specification, the data-free alternating-bit protocol over lossy one-place channels is weakly bisimilar to the one-place buffer \(\mathit{buf} = \mathit{acc}.\overline{\mathit{del}}.\mathit{buf}\).

theorem abp_weaklyBisimilar_buffer : lts.HomWeakBisimilarity abp buf

Uses 30

Statement usesProcess constants of the data-free alternating-bit protocol · Alternating-bit channel names · The data-free alternating-bit protocol · The data-free one-place buffer · Alternating-bit transition system · CCS labels · Recursive CCS processes

Proof usesStates of a one-place channel · Alternating-bit configuration · Alternating-bit receiver states · Sender states of the data-free alternating-bit protocol · Transitions of the acknowledgement channel in the data-free alternating-bit protocol · The data-free one-place buffer in a given state · Transitions of the data-free one-place buffer · Weak-bisimulation certificate for the data-free alternating-bit protocol · Alternating-bit configuration transitions · Alternating-bit data channel transitions · Initial alternating-bit configuration · Internal channels of the alternating-bit protocol · Alternating-bit receiver transitions · Alternating-bit sender transitions · Recursive specification of the data-free alternating-bit protocol · The alternating-bit protocol in a configuration · Realization of a code-level transition system · Constants listing their transitions realize them · Parallel composition preserves realization · Restriction preserves realization · Weak-bisimulation certificate check · Code-level parallel composition · Certificate checks give weak bisimilarity

TheoremThe alternating-bit protocol is observation congruent to a one-place buffer#✓fully proved

In the labelled transition system of the protocol's recursive CCS specification, the data-free alternating-bit protocol over lossy one-place channels is rooted weakly bisimilar (observation congruent) to the one-place buffer \(\mathit{buf} = \mathit{acc}.\overline{\mathit{del}}.\mathit{buf}\).

This is stronger than weak bisimilarity; it holds because initially neither process can move silently.

theorem abp_observationCongruent_buffer : lts.RootedWeaklyBisimilar abp buf

Uses 32

Statement usesProcess constants of the data-free alternating-bit protocol · Alternating-bit channel names · The data-free alternating-bit protocol · The data-free one-place buffer · Alternating-bit transition system · CCS labels · Recursive CCS processes · Rooted observation congruence

Proof usesStates of a one-place channel · Alternating-bit configuration · Alternating-bit receiver states · Sender states of the data-free alternating-bit protocol · Transitions of the acknowledgement channel in the data-free alternating-bit protocol · The data-free one-place buffer in a given state · Transitions of the data-free one-place buffer · Weak-bisimulation certificate for the data-free alternating-bit protocol · Alternating-bit configuration transitions · Alternating-bit data channel transitions · Initial alternating-bit configuration · Internal channels of the alternating-bit protocol · Alternating-bit receiver transitions · Alternating-bit sender transitions · Recursive specification of the data-free alternating-bit protocol · The alternating-bit protocol in a configuration · Realization of a code-level transition system · Constants listing their transitions realize them · Parallel composition preserves realization · Restriction preserves realization · Weak-bisimulation certificate check · Code-level parallel composition · Direct check of the root condition · Certificate checks give rooted observation congruence

InductiveChannel names of the alternating-bit protocol with data#✓fully proved

For bits \(b\) and \(d\), where \(b\) is a sequence bit and \(d\) a data bit, the channel names are \(\mathsf{acc}(d)\) (accept the data bit \(d\) from the user), \(\mathsf{del}(d)\) (deliver the data bit \(d\) to the user), \(\mathsf{send}(b, d)\) (sender to data channel), \(\mathsf{recv}(b, d)\) (data channel to receiver), \(\mathsf{reply}(b)\) (receiver to acknowledgement channel) and \(\mathsf{ack}(b)\) (acknowledgement channel to sender).

inductive Name
  /-- Accept a data bit from the user. -/
  | acc (d : Bool)
  /-- Deliver a data bit to the user. -/
  | del (d : Bool)
  /-- Sender to data channel. -/
  | send (b d : Bool)
  /-- Data channel to receiver. -/
  | recv (b d : Bool)
  /-- Receiver to acknowledgement channel. -/
  | reply (b : Bool)
  /-- Acknowledgement channel to sender. -/
  | ack (b : Bool)
  deriving DecidableEq

Used by 15

Used byThe alternating-bit protocol with data · The alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Acknowledgement channel of the alternating-bit protocol with data · The empty one-place buffer of bits · The one-place buffer of bits with given content · Transitions of the one-place buffer of bits · Transitions of the alternating-bit protocol with data · Data-channel transitions of the alternating-bit protocol with data · Internal channels of the alternating-bit protocol with data · Transition system of the alternating-bit protocol with data · Receiver transitions of the alternating-bit protocol with data · Sender transitions of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data · The alternating-bit protocol with data in a configuration

InductiveSender states of the alternating-bit protocol with data#✓fully proved

For bits \(b\) and \(d\), a sender state is \(\mathsf{accept}(b)\), ready to accept a message to be sent with sequence bit \(b\); \(\mathsf{transmit}(b, d)\), about to transmit the data bit \(d\) with sequence bit \(b\); or \(\mathsf{await}(b, d)\), waiting for the acknowledgement of \(b\) while holding \(d\) for retransmission.

inductive Sender
  /-- Ready to accept a message, to be sent with sequence bit `b`. -/
  | accept (b : Bool)
  /-- About to transmit data `d` with sequence bit `b`. -/
  | transmit (b d : Bool)
  /-- Waiting for the acknowledgement of `b`, holding `d` for retransmission. -/
  | await (b d : Bool)
  deriving DecidableEq

Used by 10

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Process constants of the alternating-bit protocol with data · Weak-bisimulation certificate for the alternating-bit protocol with data · Configurations of the alternating-bit protocol with data · Transitions of the alternating-bit protocol with data · Initial configuration of the alternating-bit protocol with data · Sender transitions of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data · The alternating-bit protocol with data in a configuration

InductiveReceiver states of the alternating-bit protocol with data#✓fully proved

For bits \(b\) and \(d\), a receiver state is \(\mathsf{expect}(b)\), expecting a frame with sequence bit \(b\); \(\mathsf{deliver}(b, d)\), about to deliver the data bit \(d\) of a frame with sequence bit \(b\); or \(\mathsf{reply}(b)\), about to acknowledge \(b\).

inductive Receiver
  /-- Expecting a frame with sequence bit `b`. -/
  | expect (b : Bool)
  /-- About to deliver data `d` of a frame with sequence bit `b`. -/
  | deliver (b d : Bool)
  /-- About to acknowledge `b`. -/
  | reply (b : Bool)
  deriving DecidableEq

Used by 10

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Process constants of the alternating-bit protocol with data · Weak-bisimulation certificate for the alternating-bit protocol with data · Configurations of the alternating-bit protocol with data · Transitions of the alternating-bit protocol with data · Initial configuration of the alternating-bit protocol with data · Receiver transitions of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data · The alternating-bit protocol with data in a configuration

DefinitionSender transitions of the alternating-bit protocol with data#✓fully proved

The transitions of each sender state, as a list of pairs of a label and a successor state, for bits \(b\) and \(d\): \(\mathsf{accept}(b)\) inputs on \(\mathsf{acc}(d)\) and moves to \(\mathsf{transmit}(b, d)\), for \(d = \mathrm{false}\) and then \(d = \mathrm{true}\); \(\mathsf{transmit}(b, d)\) outputs on \(\mathsf{send}(b, d)\) and moves to \(\mathsf{await}(b, d)\); and \(\mathsf{await}(b, d)\) inputs on \(\mathsf{ack}(b)\) and moves to \(\mathsf{accept}(\lnot b)\), inputs on \(\mathsf{ack}(\lnot b)\) and stays in \(\mathsf{await}(b, d)\), or times out by a silent step \(\tau\) back to \(\mathsf{transmit}(b, d)\), in this order.

def senderSteps : Sender → List (Label Name × Sender)
  | .accept b => [(.input (.acc false), .transmit b false), (.input (.acc true), .transmit b true)]
  | .transmit b d => [(.output (.send b d), .await b d)]
  | .await b d =>
      [(.input (.ack b), .accept (!b)), (.input (.ack (!b)), .await b d), (.tau, .transmit b d)]

Uses 3 · Used by 4

Statement usesChannel names of the alternating-bit protocol with data · Sender states of the alternating-bit protocol with data · CCS labels

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Transitions of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data

DefinitionData-channel transitions of the alternating-bit protocol with data#✓fully proved

The data channel is a lossy one-place channel whose content is either empty or a pair \((b, d)\) of a sequence bit \(b\) and a data bit \(d\). Its transitions, as a list of pairs of a label and a successor content: the empty channel inputs on \(\mathsf{send}(b, d)\) and then holds \((b, d)\), for the four pairs \((b, d)\) in the order \((\mathrm{false}, \mathrm{false})\), \((\mathrm{false}, \mathrm{true})\), \((\mathrm{true}, \mathrm{false})\), \((\mathrm{true}, \mathrm{true})\); a channel holding \((b, d)\) either outputs on \(\mathsf{recv}(b, d)\) and becomes empty, or loses the frame by a silent step \(\tau\) and becomes empty.

def dataSteps : Option (Bool × Bool) → List (Label Name × Option (Bool × Bool))
  | none => [false, true].flatMap fun b => [false, true].map fun d =>
      (.input (.send b d), some (b, d))
  | some (b, d) => [(.output (.recv b d), none), (.tau, none)]

Uses 2 · Used by 4

Statement usesChannel names of the alternating-bit protocol with data · CCS labels

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Transitions of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data

DefinitionReceiver transitions of the alternating-bit protocol with data#✓fully proved

The transitions of each receiver state, as a list of pairs of a label and a successor state, for bits \(b\) and \(d\): \(\mathsf{expect}(b)\) inputs on \(\mathsf{recv}(b, d)\) and moves to \(\mathsf{deliver}(b, d)\), or inputs a duplicate on \(\mathsf{recv}(\lnot b, d)\) and moves to the state \(\mathsf{reply}(\lnot b)\), these two for \(d = \mathrm{false}\) and then for \(d = \mathrm{true}\); \(\mathsf{deliver}(b, d)\) outputs on \(\mathsf{del}(d)\) and moves to the state \(\mathsf{reply}(b)\); and the state \(\mathsf{reply}(b)\) outputs on the channel \(\mathsf{reply}(b)\) and moves to \(\mathsf{expect}(\lnot b)\). So the receiver delivers the data of an expected frame and acknowledges a duplicate again.

def receiverSteps : Receiver → List (Label Name × Receiver)
  | .expect b => [false, true].flatMap fun d =>
      [(.input (.recv b d), .deliver b d), (.input (.recv (!b) d), .reply (!b))]
  | .deliver b d => [(.output (.del d), .reply b)]
  | .reply b => [(.output (.reply b), .expect (!b))]

Uses 3 · Used by 4

Statement usesChannel names of the alternating-bit protocol with data · Receiver states of the alternating-bit protocol with data · CCS labels

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Transitions of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data

DefinitionAcknowledgement channel of the alternating-bit protocol with data#✓fully proved

The transitions of the lossy one-place acknowledgement channel: when empty, it can take an input on \(\mathrm{reply}_b\) for either bit \(b\) and then holds \(b\); when holding \(b\), it can either output on \(\mathrm{ack}_b\) or lose \(b\) by a silent step, and in both cases it becomes empty.

def ackSteps : Option Bool → List (Label Name × Option Bool)
  | none => [(.input (.reply false), some false), (.input (.reply true), some true)]
  | some b => [(.output (.ack b), none), (.tau, none)]

Uses 2 · Used by 4

Statement usesChannel names of the alternating-bit protocol with data · CCS labels

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Transitions of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data

DefinitionTransitions of the one-place buffer of bits#✓fully proved

When empty, the buffer can take an input on \(\mathrm{acc}_d\) for either bit \(d\) and then holds \(d\); when holding \(d\), its only transition is an output on \(\mathrm{del}_d\), after which it is empty.

def bufferSteps : Option Bool → List (Label Name × Option Bool)
  | none => [(.input (.acc false), some false), (.input (.acc true), some true)]
  | some d => [(.output (.del d), none)]

Uses 2 · Used by 3

Statement usesChannel names of the alternating-bit protocol with data · CCS labels

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Recursive specification of the alternating-bit protocol with data

InductiveProcess constants of the alternating-bit protocol with data#✓fully proved

There is one process constant for each sender state, each content of the data channel (empty, or a sequence bit with a data bit), each receiver state, each content of the acknowledgement channel (empty, or a bit), and each content of the one-place buffer of bits (empty, or a bit).

inductive Agent
  | sender (s : Sender)
  | data (c : Option (Bool × Bool))
  | receiver (r : Receiver)
  | ack (c : Option Bool)
  | buffer (content : Option Bool)

Uses 2 · Used by 8

Statement usesReceiver states of the alternating-bit protocol with data · Sender states of the alternating-bit protocol with data

Used byThe alternating-bit protocol with data · The alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · The empty one-place buffer of bits · The one-place buffer of bits with given content · Transition system of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data · The alternating-bit protocol with data in a configuration

DefinitionRecursive specification of the alternating-bit protocol with data#✓fully proved

There is a separate process constant \(X_s\) for each state \(s\) of each of five components: the sender, the lossy data channel, the receiver, the lossy acknowledgement channel and the one-place buffer of bits. If \((a_1, s_1), \dots, (a_n, s_n)\) are the listed transitions of \(s\) in its component, then the body of \(X_s\) is the choice of prefixes \(a_1.X_{s_1} + (a_2.X_{s_2} + \dots + (a_n.X_{s_n} + 0))\), where each \(X_{s_i}\) is the constant of the same component and \(0\) is the inactive process; the body is \(0\) when \(s\) has no listed transitions.

def spec : Specification Name Agent
  | .sender s => sumOf ((senderSteps s).map fun y => (y.1, .constant (.sender y.2)))
  | .data c => sumOf ((dataSteps c).map fun y => (y.1, .constant (.data y.2)))
  | .receiver r => sumOf ((receiverSteps r).map fun y => (y.1, .constant (.receiver y.2)))
  | .ack c => sumOf ((ackSteps c).map fun y => (y.1, .constant (.ack y.2)))
  | .buffer q => sumOf ((bufferSteps q).map fun y => (y.1, .constant (.buffer y.2)))

Uses 13 · Used by 3

Statement usesProcess constants of the alternating-bit protocol with data · Channel names of the alternating-bit protocol with data · Receiver states of the alternating-bit protocol with data · Sender states of the alternating-bit protocol with data · Acknowledgement channel of the alternating-bit protocol with data · Transitions of the one-place buffer of bits · Data-channel transitions of the alternating-bit protocol with data · Receiver transitions of the alternating-bit protocol with data · Sender transitions of the alternating-bit protocol with data · Sum of prefixes · CCS labels · Recursive CCS processes · Recursive CCS specification

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Transition system of the alternating-bit protocol with data

AbbreviationTransition system of the alternating-bit protocol with data#✓fully proved

The labelled transition system whose states are the CCS processes over the protocol's channel names and process constants, whose labels are the CCS labels over its channel names, and whose transitions are generated by the protocol's recursive specification.

abbrev lts : LTS (Process Name Agent) (Label Name) := Process.lts spec

Uses 6 · Used by 2

Statement usesProcess constants of the alternating-bit protocol with data · Channel names of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data · CCS labels · Recursive CCS processes · Labelled transition system of a recursive specification

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly

DefinitionInternal channels of the alternating-bit protocol with data#✓fully proved

The list of the channel names that the protocol restricts: \(\mathsf{send}(b, d)\) followed by \(\mathsf{recv}(b, d)\) for the pairs \((b, d)\) in the order \((\mathrm{false}, \mathrm{false})\), \((\mathrm{false}, \mathrm{true})\), \((\mathrm{true}, \mathrm{false})\), \((\mathrm{true}, \mathrm{true})\), then \(\mathsf{reply}(\mathrm{false})\), \(\mathsf{reply}(\mathrm{true})\), \(\mathsf{ack}(\mathrm{false})\) and \(\mathsf{ack}(\mathrm{true})\).

def internal : List Name :=
  ([false, true].flatMap fun b => [false, true].flatMap fun d => [.send b d, .recv b d]) ++
    [.reply false, .reply true, .ack false, .ack true]

Uses 1 · Used by 4

Statement usesChannel names of the alternating-bit protocol with data

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Transitions of the alternating-bit protocol with data · The alternating-bit protocol with data in a configuration

AbbreviationConfigurations of the alternating-bit protocol with data#✓fully proved

A configuration consists of a sender state, the content of the data channel (empty, or a pair of a sequence bit and a data bit), a receiver state, and the content of the acknowledgement channel (empty, or a bit).

abbrev Config := ((Sender × Option (Bool × Bool)) × Receiver) × Option Bool

Uses 2 · Used by 6

Statement usesReceiver states of the alternating-bit protocol with data · Sender states of the alternating-bit protocol with data

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · Weak-bisimulation certificate for the alternating-bit protocol with data · Transitions of the alternating-bit protocol with data · Initial configuration of the alternating-bit protocol with data · The alternating-bit protocol with data in a configuration

DefinitionThe alternating-bit protocol with data in a configuration#✓fully proved

For a configuration \(c\) made of a sender state \(s\), a data-channel content \(d\), a receiver state \(r\) and an acknowledgement-channel content \(k\), the protocol process at \(c\) is \(((X_s \mid X_d) \mid X_r) \mid X_k\) with every internal channel restricted, where \(X_s\), \(X_d\), \(X_r\) and \(X_k\) are the process constants of these states. The internal channels are all channel names other than accepting and delivering a data bit.

def system (c : Config) : Process Name Agent :=
  .restriction internal
    (.parallel
      (.parallel (.parallel (.constant (.sender c.1.1.1)) (.constant (.data c.1.1.2)))
        (.constant (.receiver c.1.2)))
      (.constant (.ack c.2)))

Uses 7 · Used by 3

Statement usesProcess constants of the alternating-bit protocol with data · Configurations of the alternating-bit protocol with data · Channel names of the alternating-bit protocol with data · Receiver states of the alternating-bit protocol with data · Sender states of the alternating-bit protocol with data · Internal channels of the alternating-bit protocol with data · Recursive CCS processes

Used byThe alternating-bit protocol with data · The alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly

DefinitionTransitions of the alternating-bit protocol with data#✓fully proved

For a configuration, made of a sender state, a data-channel content, a receiver state and an acknowledgement-channel content, the transitions are those of the parallel composition of the sender, the data channel, the receiver and the acknowledgement channel, where one component moves alone or two components synchronize on complementary labels in a silent step. Of these, only the silent steps and the actions on names that are not internal channels are kept; the internal channels are the sending, receiving, reply and acknowledgement channels.

def configSteps : Config → List (Label Name × Config) :=
  restrictSteps internal
    (parSteps (parSteps (parSteps senderSteps dataSteps) receiverSteps) ackSteps)

Uses 12 · Used by 2

Statement usesConfigurations of the alternating-bit protocol with data · Channel names of the alternating-bit protocol with data · Receiver states of the alternating-bit protocol with data · Sender states of the alternating-bit protocol with data · Acknowledgement channel of the alternating-bit protocol with data · Data-channel transitions of the alternating-bit protocol with data · Internal channels of the alternating-bit protocol with data · Receiver transitions of the alternating-bit protocol with data · Sender transitions of the alternating-bit protocol with data · Code-level parallel composition · Code-level restriction · CCS labels

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly

DefinitionThe one-place buffer of bits with given content#✓fully proved

For a content \(q\), which is either empty or a bit, the process constant of the one-place buffer of bits holding \(q\).

def buffer (q : Option Bool) : Process Name Agent := .constant (.buffer q)

Uses 3 · Used by 3

Statement usesProcess constants of the alternating-bit protocol with data · Channel names of the alternating-bit protocol with data · Recursive CCS processes

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · The empty one-place buffer of bits

DefinitionInitial configuration of the alternating-bit protocol with data#✓fully proved

The configuration in which the sender is in state \(\mathsf{accept}(\mathrm{false})\), ready to accept a message to be sent with sequence bit false, the data channel and the acknowledgement channel are empty, and the receiver is in state \(\mathsf{expect}(\mathrm{false})\), expecting a frame with sequence bit false.

def initial : Config := (((.accept false, none), .expect false), none)

Uses 3 · Used by 3

Statement usesConfigurations of the alternating-bit protocol with data · Receiver states of the alternating-bit protocol with data · Sender states of the alternating-bit protocol with data

Used byThe alternating-bit protocol with data · The alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly

DefinitionThe alternating-bit protocol with data#✓fully proved

The protocol process in its initial configuration: the sender is ready to accept a data bit, to be sent with sequence bit false, the data channel and the acknowledgement channel are empty, and the receiver expects a frame with sequence bit false. The four agents run in parallel, with all internal channels restricted.

def abpData : Process Name Agent := system initial

Uses 5 · Used by 2

Statement usesProcess constants of the alternating-bit protocol with data · Channel names of the alternating-bit protocol with data · Initial configuration of the alternating-bit protocol with data · The alternating-bit protocol with data in a configuration · Recursive CCS processes

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly

DefinitionThe empty one-place buffer of bits#✓fully proved

The process constant of the one-place buffer of bits with empty content.

def buf : Process Name Agent := buffer none

Uses 4 · Used by 2

Statement usesProcess constants of the alternating-bit protocol with data · Channel names of the alternating-bit protocol with data · The one-place buffer of bits with given content · Recursive CCS processes

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly

DefinitionWeak-bisimulation certificate for the alternating-bit protocol with data#✓fully proved

A list of 220 pairs, each a protocol configuration together with the buffer content it simulates: every reachable configuration with the buffer content it simulates, listed so that every pair reaches the visible actions of its buffer state through pairs listed earlier.

Cslib.Algorithms.CCS.AlternatingBitData.certificate · 221 lines

def certificate : List (Config × Option Bool) := [
  ((((.accept true, none), .expect true), some false), none),
  ((((.transmit false true, none), .deliver false true), none), some true),
  ((((.transmit false true, none), .deliver false true), some true), some true),
  ((((.accept true, none), .reply false), some false), none),
  ((((.await false true, some (false, true)), .deliver false true), none), some true),
  ((((.await false true, some (false, true)), .deliver false true), some true), some true),
  ((((.transmit true false, some (true, false)), .deliver true false), none), some false),
  ((((.accept true, some (false, false)), .reply false), none), none),
  ((((.await true false, none), .deliver true false), some false), some false),
  ((((.accept true, none), .expect true), none), none),
  ((((.accept false, some (true, true)), .expect false), none), none),
  ((((.transmit false true, some (false, true)), .expect false), some true), some true),
  ((((.accept false, none), .reply true), some true), none),
  ((((.transmit false true, some (false, true)), .expect false), none), some true),
  ((((.transmit true false, none), .deliver true false), none), some false),
  ((((.accept false, some (true, false)), .reply true), none), none),
  ((((.transmit false true, some (false, true)), .reply true), none), some true),
  ((((.accept false, some (true, true)), .expect false), some true), none),
  ((((.transmit false false, some (false, false)), .deliver false false), some true), some false),
  ((((.accept true, some (false, false)), .expect true), some false), none),
  ((((.accept false, some (true, false)), .expect false), none), none),
  ((((.accept true, some (false, false)), .expect true), none), none),
  ((((.transmit true true, some (true, true)), .deliver true true), none), some true),
  ((((.await false true, none), .deliver false true), none), some true),
  ((((.transmit true false, some (true, false)), .expect true), none), some false),
  ((((.await false false, none), .expect true), some false), none),
  ((((.await true false, none), .deliver true false), none), some false),
  ((((.transmit false true, some (false, true)), .deliver false true), some true), some true),
  ((((.await true false, some (true, false)), .expect false), some true), none),
  ((((.await false false, none), .deliver false false), none), some false),
  ((((.accept true, some (false, true)), .expect true), none), none),
  ((((.accept false, some (true, false)), .expect false), some true), none),
  ((((.await false false, none), .deliver false false), some true), some false),
  ((((.await false true, none), .deliver false true), some true), some true),
  ((((.await true false, some (true, false)), .deliver true false), some false), some false),
  ((((.accept false, none), .reply true), none), none),
  ((((.transmit true false, some (true, false)), .expect true), some false), some false),
  ((((.transmit false false, none), .deliver false false), none), some false),
  ((((.accept true, some (false, true)), .reply false), none), none),
  ((((.transmit false true, some (false, true)), .deliver false true), none), some true),
  ((((.await false true, none), .expect true), some false), none),
  ((((.await false false, some (false, false)), .deliver false false), some true), some false),
  ((((.accept false, none), .expect false), none), none),
  ((((.await false true, some (false, true)), .expect false), none), some true),
  ((((.await true true, none), .reply true), some true), none),
  ((((.accept true, some (false, true)), .expect true), some false), none),
  ((((.transmit true false, none), .expect false), some true), none),
  ((((.transmit true false, none), .deliver true false), some false), some false),
  ((((.transmit false false, some (false, false)), .deliver false false), none), some false),
  ((((.accept false, none), .expect false), some true), none),
  ((((.await false true, some (false, true)), .expect false), some true), some true),
  ((((.await false false, some (false, false)), .reply false), some false), none),
  ((((.transmit false false, none), .deliver false false), some true), some false),
  ((((.transmit true false, some (true, false)), .expect false), some true), none),
  ((((.transmit true true, some (true, true)), .deliver true true), some false), some true),
  ((((.await true false, some (true, false)), .deliver true false), none), some false),
  ((((.await true false, some (true, false)), .reply true), some true), none),
  ((((.transmit true true, none), .deliver true true), some false), some true),
  ((((.transmit true true, none), .deliver true true), none), some true),
  ((((.transmit false true, none), .expect false), none), some true),
  ((((.await false false, some (false, false)), .deliver false false), none), some false),
  ((((.transmit false true, some (false, true)), .reply true), some true), some true),
  ((((.await true true, some (true, true)), .deliver true true), some false), some true),
  ((((.await false true, some (false, true)), .expect true), some false), none),
  ((((.accept false, some (true, true)), .reply true), none), none),
  ((((.transmit false true, none), .expect false), some true), some true),
  ((((.await false true, some (false, true)), .reply false), none), none),
  ((((.await true false, none), .reply true), some true), none),
  ((((.await false true, some (false, true)), .reply false), some false), none),
  ((((.await true true, some (true, true)), .deliver true true), none), some true),
  ((((.await false false, some (false, false)), .expect true), some false), none),
  ((((.await true true, none), .deliver true true), some false), some true),
  ((((.transmit true false, some (true, false)), .deliver true false), some false), some false),
  ((((.await true true, none), .deliver true true), none), some true),
  ((((.transmit true true, some (true, true)), .expect true), some false), some true),
  ((((.accept true, none), .reply false), none), none),
  ((((.await false false, some (false, false)), .expect false), none), some false),
  ((((.await true true, some (true, true)), .expect true), some false), some true),
  ((((.transmit false false, some (false, false)), .expect false), none), some false),
  ((((.transmit true true, some (true, true)), .expect true), none), some true),
  ((((.transmit false true, none), .reply true), none), some true),
  ((((.await true true, some (true, true)), .expect false), some true), none),
  ((((.transmit true true, some (true, true)), .reply false), none), some true),
  ((((.await true true, none), .expect false), some true), none),
  ((((.await false true, none), .reply true), none), some true),
  ((((.await false true, none), .reply false), some false), none),
  ((((.await true false, some (true, false)), .expect true), some false), some false),
  ((((.transmit false false, none), .reply false), some false), none),
  ((((.transmit true true, none), .expect true), some false), some true),
  ((((.await false false, none), .reply false), none), none),
  ((((.await true false, some (true, false)), .reply true), none), none),
  ((((.transmit true false, none), .reply true), none), none),
  ((((.await false false, some (false, false)), .expect false), some true), some false),
  ((((.await true true, some (true, true)), .expect true), none), some true),
  ((((.await false true, some (false, true)), .reply true), none), some true),
  ((((.transmit false false, some (false, false)), .expect false), some true), some false),
  ((((.transmit true false, none), .reply true), some true), none),
  ((((.transmit true true, none), .reply false), none), some true),
  ((((.await false true, some (false, true)), .reply true), some true), some true),
  ((((.await true false, none), .expect false), some true), none),
  ((((.await true false, some (true, false)), .expect true), none), some false),
  ((((.await true true, none), .expect true), some false), some true),
  ((((.await false true, none), .expect false), some true), some true),
  ((((.transmit true true, some (false, true)), .expect true), none), some true),
  ((((.transmit true false, none), .expect true), none), some false),
  ((((.await true true, none), .reply true), none), none),
  ((((.transmit false true, some (true, true)), .expect false), none), some true),
  ((((.transmit true false, none), .expect true), some false), some false),
  ((((.await false true, none), .reply false), none), none),
  ((((.transmit false true, some (true, false)), .expect false), none), some true),
  ((((.await false true, none), .reply false), some true), none),
  ((((.transmit false true, some (true, true)), .expect false), some true), some true),
  ((((.transmit false true, some (true, false)), .expect false), some true), some true),
  ((((.await false true, some (false, true)), .reply false), some true), none),
  ((((.await true true, some (true, true)), .reply true), none), none),
  ((((.transmit true false, some (true, false)), .reply true), none), none),
  ((((.await false true, none), .expect false), none), some true),
  ((((.transmit true false, some (false, true)), .expect true), none), some false),
  ((((.await true true, some (true, true)), .reply true), some true), none),
  ((((.transmit false true, none), .reply true), some true), some true),
  ((((.transmit false false, some (false, false)), .reply false), some false), none),
  ((((.await true false, none), .expect true), some false), some false),
  ((((.await false false, none), .reply false), some false), none),
  ((((.transmit true false, some (true, false)), .reply false), none), some false),
  ((((.transmit false true, none), .reply false), some false), none),
  ((((.transmit true false, some (true, false)), .reply true), some true), none),
  ((((.transmit false true, some (true, true)), .reply true), none), some true),
  ((((.transmit false true, none), .reply false), none), none),
  ((((.transmit true true, some (false, false)), .expect true), some false), some true),
  ((((.await false false, some (false, false)), .reply true), none), some false),
  ((((.transmit false true, some (false, true)), .reply false), none), none),
  ((((.transmit false true, some (false, true)), .expect true), some false), none),
  ((((.await false false, some (false, false)), .reply true), some true), some false),
  ((((.transmit true true, some (false, false)), .expect true), none), some true),
  ((((.transmit false true, none), .reply false), some true), none),
  ((((.transmit false false, none), .expect true), some false), none),
  ((((.transmit false false, none), .reply true), none), some false),
  ((((.transmit true true, none), .reply true), some true), none),
  ((((.transmit false true, none), .expect true), some false), none),
  ((((.transmit false false, none), .expect false), none), some false),
  ((((.await false false, some (false, false)), .reply false), none), none),
  ((((.await true false, none), .expect true), none), some false),
  ((((.transmit false false, some (false, false)), .reply true), none), some false),
  ((((.transmit false true, some (false, true)), .expect true), none), none),
  ((((.transmit true false, some (true, false)), .expect false), none), none),
  ((((.await false false, some (false, false)), .reply false), some true), none),
  ((((.transmit false false, some (true, false)), .reply true), none), some false),
  ((((.await false false, none), .reply false), some true), none),
  ((((.transmit true true, some (true, true)), .reply false), some false), some true),
  ((((.transmit true true, some (false, true)), .reply false), none), some true),
  ((((.await true false, none), .reply true), none), none),
  ((((.await false false, none), .expect false), none), some false),
  ((((.transmit false false, none), .expect false), some true), some false),
  ((((.await false true, none), .reply true), some true), some true),
  ((((.transmit false false, some (false, false)), .expect true), some false), none),
  ((((.await false true, some (false, true)), .expect true), none), none),
  ((((.await true false, none), .reply false), none), some false),
  ((((.await true true, some (true, true)), .reply false), none), some true),
  ((((.transmit false true, some (true, false)), .reply true), none), some true),
  ((((.await false false, some (false, false)), .expect true), none), none),
  ((((.await true false, some (true, false)), .reply true), some false), none),
  ((((.transmit true true, none), .expect false), some true), none),
  ((((.transmit false false, some (true, true)), .expect false), some true), some false),
  ((((.transmit false false, some (true, false)), .expect false), some true), some false),
  ((((.transmit true false, none), .reply false), none), some false),
  ((((.transmit true true, some (false, true)), .expect true), some false), some true),
  ((((.transmit true false, some (false, true)), .reply false), none), some false),
  ((((.transmit true false, some (false, false)), .expect true), some false), some false),
  ((((.await true false, some (true, false)), .reply false), none), some false),
  ((((.transmit true false, none), .reply true), some false), none),
  ((((.transmit true true, none), .expect true), none), some true),
  ((((.await true true, some (true, true)), .expect false), none), none),
  ((((.await true true, none), .reply false), none), some true),
  ((((.await true true, some (true, true)), .reply false), some false), some true),
  ((((.await true false, some (true, false)), .reply false), some false), some false),
  ((((.transmit true false, none), .reply false), some false), some false),
  ((((.await false false, none), .reply true), none), some false),
  ((((.transmit true false, some (false, false)), .expect true), none), some false),
  ((((.transmit true false, some (false, true)), .expect true), some false), some false),
  ((((.transmit true true, none), .reply false), some false), some true),
  ((((.transmit true true, some (false, false)), .reply false), none), some true),
  ((((.await true true, none), .reply true), some false), none),
  ((((.transmit false false, some (true, true)), .reply true), none), some false),
  ((((.await true true, none), .expect true), none), some true),
  ((((.transmit true false, some (true, false)), .reply false), some false), some false),
  ((((.transmit true true, none), .reply true), none), none),
  ((((.await true false, some (true, false)), .expect false), none), none),
  ((((.await false false, none), .expect false), some true), some false),
  ((((.transmit false false, none), .reply true), some true), some false),
  ((((.await true true, some (true, true)), .reply true), some false), none),
  ((((.await false false, none), .reply true), some true), some false),
  ((((.transmit false false, none), .reply false), some true), none),
  ((((.transmit false true, some (false, true)), .reply false), some false), none),
  ((((.transmit true false, some (true, false)), .reply true), some false), none),
  ((((.transmit false true, some (false, true)), .reply false), some true), none),
  ((((.transmit true true, some (true, true)), .reply true), none), none),
  ((((.transmit false false, some (false, false)), .reply false), none), none),
  ((((.transmit false false, none), .reply false), none), none),
  ((((.transmit false false, some (true, false)), .expect false), none), some false),
  ((((.transmit false false, some (false, false)), .reply false), some true), none),
  ((((.transmit false false, some (false, false)), .reply true), some true), some false),
  ((((.transmit true true, some (true, true)), .expect false), some true), none),
  ((((.transmit true true, some (true, true)), .reply true), some true), none),
  ((((.transmit false false, some (true, true)), .expect false), none), some false),
  ((((.transmit false true, none), .expect true), none), none),
  ((((.await true false, none), .reply false), some false), some false),
  ((((.transmit true false, none), .expect false), none), none),
  ((((.await true false, none), .reply true), some false), none),
  ((((.transmit true true, none), .expect false), none), none),
  ((((.transmit false false, none), .expect true), none), none),
  ((((.transmit false false, some (false, false)), .expect true), none), none),
  ((((.transmit true false, some (false, false)), .reply false), none), some false),
  ((((.transmit true true, some (true, true)), .expect false), none), none),
  ((((.await true true, none), .expect false), none), none),
  ((((.await true true, none), .reply false), some false), some true),
  ((((.await true false, none), .expect false), none), none),
  ((((.transmit true true, none), .reply true), some false), none),
  ((((.transmit true true, some (true, true)), .reply true), some false), none),
  ((((.await false false, none), .expect true), none), none),
  ((((.await false true, none), .expect true), none), none)]

Uses 3 · Used by 2

Statement usesConfigurations of the alternating-bit protocol with data · Receiver states of the alternating-bit protocol with data · Sender states of the alternating-bit protocol with data

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly

TheoremThe alternating-bit protocol transmits data correctly#✓fully proved

It is weakly bisimilar to the empty one-place buffer of bits.

theorem abpData_weaklyBisimilar_buffer : lts.HomWeakBisimilarity abpData buf

Uses 29

Statement usesProcess constants of the alternating-bit protocol with data · Channel names of the alternating-bit protocol with data · The alternating-bit protocol with data · The empty one-place buffer of bits · Transition system of the alternating-bit protocol with data · CCS labels · Recursive CCS processes

Proof usesConfigurations of the alternating-bit protocol with data · Receiver states of the alternating-bit protocol with data · Sender states of the alternating-bit protocol with data · Acknowledgement channel of the alternating-bit protocol with data · The one-place buffer of bits with given content · Transitions of the one-place buffer of bits · Weak-bisimulation certificate for the alternating-bit protocol with data · Transitions of the alternating-bit protocol with data · Data-channel transitions of the alternating-bit protocol with data · Initial configuration of the alternating-bit protocol with data · Internal channels of the alternating-bit protocol with data · Receiver transitions of the alternating-bit protocol with data · Sender transitions of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data · The alternating-bit protocol with data in a configuration · Realization of a code-level transition system · Constants listing their transitions realize them · Parallel composition preserves realization · Restriction preserves realization · Weak-bisimulation certificate check · Code-level parallel composition · Certificate checks give weak bisimilarity

TheoremThe alternating-bit protocol with data is observation congruent to the buffer#✓fully proved

In the labelled transition system of the protocol's recursive specification, the alternating-bit protocol with data is observation congruent (rooted weakly bisimilar) to the empty one-place buffer of bits: every transition of either process with some label is matched by the other process through silent steps, then one actual step with the same label, then silent steps, and the two resulting processes are weakly bisimilar.

theorem abpData_observationCongruent_buffer :
    lts.RootedWeaklyBisimilar abpData buf

Uses 31

Statement usesProcess constants of the alternating-bit protocol with data · Channel names of the alternating-bit protocol with data · The alternating-bit protocol with data · The empty one-place buffer of bits · Transition system of the alternating-bit protocol with data · CCS labels · Recursive CCS processes · Rooted observation congruence

Proof usesConfigurations of the alternating-bit protocol with data · Receiver states of the alternating-bit protocol with data · Sender states of the alternating-bit protocol with data · Acknowledgement channel of the alternating-bit protocol with data · The one-place buffer of bits with given content · Transitions of the one-place buffer of bits · Weak-bisimulation certificate for the alternating-bit protocol with data · Transitions of the alternating-bit protocol with data · Data-channel transitions of the alternating-bit protocol with data · Initial configuration of the alternating-bit protocol with data · Internal channels of the alternating-bit protocol with data · Receiver transitions of the alternating-bit protocol with data · Sender transitions of the alternating-bit protocol with data · Recursive specification of the alternating-bit protocol with data · The alternating-bit protocol with data in a configuration · Realization of a code-level transition system · Constants listing their transitions realize them · Parallel composition preserves realization · Restriction preserves realization · Weak-bisimulation certificate check · Code-level parallel composition · Direct check of the root condition · Certificate checks give rooted observation congruence

45 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.