.. index:: single: ccsds_packet_services .. _ccsds_packet_services/0:

.. rst-class:: right

object

ccsds_packet_services

Helpers for CCSDS packet service packet-zone splitting and cross-frame TM/AOS packet reassembly.

| Availability: | logtalk_load(ccsds_packet_services(loader))

| Author: Paulo Moura | Version: 0:1:1 | Date: 2026-06-14

| Compilation flags: | static, context_switching_calls

| Uses: | :ref:`ccsds_packets(SecondaryHeaderLength) <ccsds_packets/1>` | :ref:`list <list/0>` | :ref:`type <type/0>`

| Remarks: | (none)

| Inherited public predicates: | (none)

.. contents:: :local: :backlinks: top

Public predicates

.. index:: valid_reassembly_state/1 .. _ccsds_packet_services/0::valid_reassembly_state/1:

valid_reassembly_state/1 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

True if the argument is a valid packet reassembly state term.

| Compilation flags: | static

| Template: | valid_reassembly_state(State) | Mode and number of proofs: | valid_reassembly_state(@compound) - zero_or_one

---

.. index:: initial_reassembly_state/1 .. _ccsds_packet_services/0::initial_reassembly_state/1:

initial_reassembly_state/1 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Returns the initial cross-frame packet reassembly state.

| Compilation flags: | static

| Template: | initial_reassembly_state(State) | Mode and number of proofs: | initial_reassembly_state(-compound) - one

---

.. index:: pending_data/2 .. _ccsds_packet_services/0::pending_data/2:

pending_data/2 ^^^^^^^^^^^^^^^^^^

Extracts the currently buffered trailing packet fragment bytes from a packet reassembly state.

| Compilation flags: | static

| Template: | pending_data(State,Bytes) | Mode and number of proofs: | pending_data(+compound,-list(byte)) - one

---

.. index:: valid_channel_reassembly_state/1 .. _ccsds_packet_services/0::valid_channel_reassembly_state/1:

valid_channel_reassembly_state/1 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

True if the argument is a valid frame-channel packet reassembly state term keyed by frame type, spacecraft identifier, and virtual channel identifier.

| Compilation flags: | static

| Template: | valid_channel_reassembly_state(State) | Mode and number of proofs: | valid_channel_reassembly_state(@compound) - zero_or_one

---

.. index:: initial_channel_reassembly_state/1 .. _ccsds_packet_services/0::initial_channel_reassembly_state/1:

initial_channel_reassembly_state/1 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Returns the initial frame-channel packet reassembly state.

| Compilation flags: | static

| Template: | initial_channel_reassembly_state(State) | Mode and number of proofs: | initial_channel_reassembly_state(-compound) - one

---

.. index:: pending_fragments/2 .. _ccsds_packet_services/0::pending_fragments/2:

pending_fragments/2 ^^^^^^^^^^^^^^^^^^^^^^^

Extracts the non-empty pending packet fragments buffered per frame type, spacecraft identifier, and virtual channel identifier.

| Compilation flags: | static

| Template: | pending_fragments(State,PendingFragments) | Mode and number of proofs: | pending_fragments(+compound,-list(compound)) - one

---

.. index:: valid_discontinuity_policy/1 .. _ccsds_packet_services/0::valid_discontinuity_policy/1:

valid_discontinuity_policy/1 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

True if the argument is a valid discontinuity recovery policy atom. Valid values are throw, drop, and resynchronize.

| Compilation flags: | static

| Template: | valid_discontinuity_policy(Policy) | Mode and number of proofs: | valid_discontinuity_policy(@atom) - zero_or_one

---

.. index:: valid/1 .. _ccsds_packet_services/0::valid/1:

valid/1 ^^^^^^^^^^^

True if the argument is a valid packet-zone term.

| Compilation flags: | static

| Template: | valid(PacketZone) | Mode and number of proofs: | valid(@compound) - zero_or_one

---

.. index:: prefix_data/2 .. _ccsds_packet_services/0::prefix_data/2:

prefix_data/2 ^^^^^^^^^^^^^^^^^

Extracts the bytes that precede the first complete packet in a packet zone.

| Compilation flags: | static

| Template: | prefix_data(PacketZone,PrefixData) | Mode and number of proofs: | prefix_data(+compound,-list(byte)) - one

---

.. index:: packets/2 .. _ccsds_packet_services/0::packets/2:

packets/2 ^^^^^^^^^^^^^

Extracts the list of complete packets in a packet zone.

| Compilation flags: | static

| Template: | packets(PacketZone,Packets) | Mode and number of proofs: | packets(+compound,-list(compound)) - one

---

.. index:: suffix_data/2 .. _ccsds_packet_services/0::suffix_data/2:

suffix_data/2 ^^^^^^^^^^^^^^^^^

Extracts the bytes that trail the last complete packet in a packet zone.

| Compilation flags: | static

| Template: | suffix_data(PacketZone,SuffixData) | Mode and number of proofs: | suffix_data(+compound,-list(byte)) - one

---

.. index:: split_packet_zone/4 .. _ccsds_packet_services/0::split_packet_zone/4:

split_packet_zone/4 ^^^^^^^^^^^^^^^^^^^^^^^

Splits a packet-zone byte sequence using the first header pointer and parses any complete packets starting at that offset. A pointer value of 2047 denotes that no packet starts in the zone.

| Compilation flags: | static

| Template: | split_packet_zone(Bytes,FirstHeaderPointer,SecondaryHeaderLength,PacketZone) | Mode and number of proofs: | split_packet_zone(+list(byte),+integer,+integer,-compound) - one_or_error

| Exceptions: | Bytes, FirstHeaderPointer, or SecondaryHeaderLength is a variable: | instantiation_error | Bytes is neither a variable nor a valid packet-zone byte sequence: | domain_error(ccsds_packet_zone_bytes,Bytes) | FirstHeaderPointer is neither a variable nor a valid first header pointer for Bytes: | domain_error(ccsds_first_header_pointer,FirstHeaderPointer) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength)

---

.. index:: join_packet_zone/4 .. _ccsds_packet_services/0::join_packet_zone/4:

join_packet_zone/4 ^^^^^^^^^^^^^^^^^^^^^^

Encodes a packet-zone term back into bytes and returns the corresponding first header pointer. When the packet list is empty, the pointer is set to 2047.

| Compilation flags: | static

| Template: | join_packet_zone(PacketZone,SecondaryHeaderLength,Bytes,FirstHeaderPointer) | Mode and number of proofs: | join_packet_zone(+compound,+integer,-list(byte),-integer) - one_or_error

| Exceptions: | PacketZone or SecondaryHeaderLength is a variable: | instantiation_error | PacketZone is neither a variable nor a valid packet-zone term: | domain_error(ccsds_packet_zone,PacketZone) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength)

---

.. index:: extract_tm_packets/3 .. _ccsds_packet_services/0::extract_tm_packets/3:

extract_tm_packets/3 ^^^^^^^^^^^^^^^^^^^^^^^^

Extracts a TM transfer frame packet zone as a packet-zone term using the frame first header pointer and the given packet secondary header length.

| Compilation flags: | static

| Template: | extract_tm_packets(Frame,SecondaryHeaderLength,PacketZone) | Mode and number of proofs: | extract_tm_packets(+compound,+integer,-compound) - one_or_error

| Exceptions: | Frame or SecondaryHeaderLength is a variable: | instantiation_error | Frame is neither a variable nor a valid TM transfer frame term: | domain_error(ccsds_tm_transfer_frame_term,Frame) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | The frame packet-zone bytes or first header pointer are invalid: | domain_error(ccsds_packet_zone_bytes,Bytes)

---

.. index:: insert_tm_packets/4 .. _ccsds_packet_services/0::insert_tm_packets/4:

insert_tm_packets/4 ^^^^^^^^^^^^^^^^^^^^^^^

Updates a TM transfer frame data field and first header pointer from a packet-zone term while preserving the remaining frame fields unchanged.

| Compilation flags: | static

| Template: | insert_tm_packets(PacketZone,SecondaryHeaderLength,Frame,UpdatedFrame) | Mode and number of proofs: | insert_tm_packets(+compound,+integer,+compound,-compound) - one_or_error

| Exceptions: | PacketZone, SecondaryHeaderLength, or Frame is a variable: | instantiation_error | PacketZone is neither a variable nor a valid packet-zone term: | domain_error(ccsds_packet_zone,PacketZone) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | Frame is neither a variable nor a valid TM transfer frame term: | domain_error(ccsds_tm_transfer_frame_term,Frame)

---

.. index:: split_aos_packet_zone/3 .. _ccsds_packet_services/0::split_aos_packet_zone/3:

split_aos_packet_zone/3 ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Splits an AOS M_PDU packet-service data field into a packet-zone term. The first two octets are interpreted as the M_PDU first header pointer field, where 2046 denotes idle data only and 2047 denotes that no packet starts in the packet zone.

| Compilation flags: | static

| Template: | split_aos_packet_zone(Bytes,SecondaryHeaderLength,PacketZone) | Mode and number of proofs: | split_aos_packet_zone(+list(byte),+integer,-compound) - one_or_error

| Exceptions: | Bytes or SecondaryHeaderLength is a variable: | instantiation_error | Bytes is neither a variable nor a valid AOS packet-zone byte sequence: | domain_error(ccsds_aos_packet_zone_bytes,Bytes) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength)

---

.. index:: join_aos_packet_zone/3 .. _ccsds_packet_services/0::join_aos_packet_zone/3:

join_aos_packet_zone/3 ^^^^^^^^^^^^^^^^^^^^^^^^^^

Encodes a packet-zone term as an AOS M_PDU packet-service data field, including the two-octet first header pointer field.

| Compilation flags: | static

| Template: | join_aos_packet_zone(PacketZone,SecondaryHeaderLength,Bytes) | Mode and number of proofs: | join_aos_packet_zone(+compound,+integer,-list(byte)) - one_or_error

| Exceptions: | PacketZone or SecondaryHeaderLength is a variable: | instantiation_error | PacketZone is neither a variable nor a valid packet-zone term: | domain_error(ccsds_packet_zone,PacketZone) | PacketZone has neither packets nor a pure prefix or suffix and therefore cannot be encoded as an empty AOS packet zone: | domain_error(ccsds_aos_packet_zone,PacketZone) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength)

---

.. index:: reassemble_packet_zone/5 .. _ccsds_packet_services/0::reassemble_packet_zone/5:

reassemble_packet_zone/5 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Reassembles complete packets from a packet-zone term and a prior packet reassembly state, returning any complete packets plus the updated trailing fragment state.

| Compilation flags: | static

| Template: | reassemble_packet_zone(PacketZone,SecondaryHeaderLength,State,Packets,UpdatedState) | Mode and number of proofs: | reassemble_packet_zone(+compound,+integer,+compound,-list(compound),-compound) - one_or_error

| Exceptions: | PacketZone, SecondaryHeaderLength, or State is a variable: | instantiation_error | PacketZone is neither a variable nor a valid packet-zone term: | domain_error(ccsds_packet_zone,PacketZone) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | State is neither a variable nor a valid packet reassembly state: | domain_error(ccsds_packet_reassembly_state,State) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: extract_aos_packets/3 .. _ccsds_packet_services/0::extract_aos_packets/3:

extract_aos_packets/3 ^^^^^^^^^^^^^^^^^^^^^^^^^

Extracts an AOS transfer frame packet zone as a packet-zone term using the two-octet M_PDU header at the beginning of the frame data field.

| Compilation flags: | static

| Template: | extract_aos_packets(Frame,SecondaryHeaderLength,PacketZone) | Mode and number of proofs: | extract_aos_packets(+compound,+integer,-compound) - one_or_error

| Exceptions: | Frame or SecondaryHeaderLength is a variable: | instantiation_error | Frame is neither a variable nor a valid AOS transfer frame term: | domain_error(ccsds_aos_transfer_frame_term,Frame) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | The frame data field is not a valid AOS packet-zone byte sequence: | domain_error(ccsds_aos_packet_zone_bytes,Bytes)

---

.. index:: insert_aos_packets/4 .. _ccsds_packet_services/0::insert_aos_packets/4:

insert_aos_packets/4 ^^^^^^^^^^^^^^^^^^^^^^^^

Updates an AOS transfer frame data field from a packet-zone term by regenerating the M_PDU first header pointer and packet-zone bytes while preserving the remaining frame fields unchanged.

| Compilation flags: | static

| Template: | insert_aos_packets(PacketZone,SecondaryHeaderLength,Frame,UpdatedFrame) | Mode and number of proofs: | insert_aos_packets(+compound,+integer,+compound,-compound) - one_or_error

| Exceptions: | PacketZone, SecondaryHeaderLength, or Frame is a variable: | instantiation_error | PacketZone is neither a variable nor a valid packet-zone term: | domain_error(ccsds_packet_zone,PacketZone) | PacketZone cannot be encoded as an AOS empty packet zone: | domain_error(ccsds_aos_packet_zone,PacketZone) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | Frame is neither a variable nor a valid AOS transfer frame term: | domain_error(ccsds_aos_transfer_frame_term,Frame)

---

.. index:: reassemble_tm_packets/5 .. _ccsds_packet_services/0::reassemble_tm_packets/5:

reassemble_tm_packets/5 ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Extracts the packet zone from a TM transfer frame, using the default throw discontinuity recovery policy, and returns the complete packets plus the updated channel reassembly state.

| Compilation flags: | static

| Template: | reassemble_tm_packets(Frame,SecondaryHeaderLength,State,Packets,UpdatedState) | Mode and number of proofs: | reassemble_tm_packets(+compound,+integer,+compound,-list(compound),-compound) - one_or_error

| Exceptions: | Frame, SecondaryHeaderLength, or State is a variable: | instantiation_error | Frame is neither a variable nor a valid TM transfer frame term: | domain_error(ccsds_tm_transfer_frame_term,Frame) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | The TM frame sequence is discontinuous: | domain_error(ccsds_tm_transfer_frame_sequence,tm_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current TM frame counter moduli differ: | domain_error(ccsds_tm_transfer_frame_counter_modulus,tm_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_tm_packets/6 .. _ccsds_packet_services/0::reassemble_tm_packets/6:

reassemble_tm_packets/6 ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Extracts the packet zone from a TM transfer frame, applies the selected discontinuity recovery policy when frame-count continuity is broken, and returns the complete packets plus the updated channel reassembly state.

| Compilation flags: | static

| Template: | reassemble_tm_packets(Frame,SecondaryHeaderLength,Policy,State,Packets,UpdatedState) | Mode and number of proofs: | reassemble_tm_packets(+compound,+integer,+atom,+compound,-list(compound),-compound) - one_or_error

| Exceptions: | Frame, SecondaryHeaderLength, Policy, or State is a variable: | instantiation_error | Frame is neither a variable nor a valid TM transfer frame term: | domain_error(ccsds_tm_transfer_frame_term,Frame) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | Policy is neither a variable nor a valid discontinuity recovery policy: | domain_error(ccsds_discontinuity_policy,Policy) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | The TM frame sequence is discontinuous under the throw recovery policy: | domain_error(ccsds_tm_transfer_frame_sequence,tm_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current TM frame counter moduli differ: | domain_error(ccsds_tm_transfer_frame_counter_modulus,tm_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_tm_packets/7 .. _ccsds_packet_services/0::reassemble_tm_packets/7:

reassemble_tm_packets/7 ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Extracts the packet zone from a TM transfer frame, applies the selected discontinuity recovery policy when frame-count continuity is broken, and returns the complete packets, updated channel reassembly state, and explicit recovery events.

| Compilation flags: | static

| Template: | reassemble_tm_packets(Frame,SecondaryHeaderLength,Policy,State,Packets,UpdatedState,Events) | Mode and number of proofs: | reassemble_tm_packets(+compound,+integer,+atom,+compound,-list(compound),-compound,-list(compound)) - one_or_error

| Exceptions: | Frame, SecondaryHeaderLength, Policy, or State is a variable: | instantiation_error | Frame is neither a variable nor a valid TM transfer frame term: | domain_error(ccsds_tm_transfer_frame_term,Frame) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | Policy is neither a variable nor a valid discontinuity recovery policy: | domain_error(ccsds_discontinuity_policy,Policy) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | The TM frame sequence is discontinuous under the throw recovery policy: | domain_error(ccsds_tm_transfer_frame_sequence,tm_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current TM frame counter moduli differ: | domain_error(ccsds_tm_transfer_frame_counter_modulus,tm_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_tm_frames/5 .. _ccsds_packet_services/0::reassemble_tm_frames/5:

reassemble_tm_frames/5 ^^^^^^^^^^^^^^^^^^^^^^^^^^

Reassembles complete packets across a sequence of TM transfer frames using the default throw discontinuity recovery policy.

| Compilation flags: | static

| Template: | reassemble_tm_frames(Frames,SecondaryHeaderLength,State,Packets,UpdatedState) | Mode and number of proofs: | reassemble_tm_frames(+list(compound),+integer,+compound,-list(compound),-compound) - one_or_error

| Exceptions: | Frames, SecondaryHeaderLength, or State is a variable: | instantiation_error | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | An element Frame of Frames is neither a variable nor a valid TM transfer frame term: | domain_error(ccsds_tm_transfer_frame_term,Frame) | The TM frame sequence is discontinuous: | domain_error(ccsds_tm_transfer_frame_sequence,tm_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current TM frame counter moduli differ: | domain_error(ccsds_tm_transfer_frame_counter_modulus,tm_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_tm_frames/6 .. _ccsds_packet_services/0::reassemble_tm_frames/6:

reassemble_tm_frames/6 ^^^^^^^^^^^^^^^^^^^^^^^^^^

Reassembles complete packets across a sequence of TM transfer frames using the selected discontinuity recovery policy.

| Compilation flags: | static

| Template: | reassemble_tm_frames(Frames,SecondaryHeaderLength,Policy,State,Packets,UpdatedState) | Mode and number of proofs: | reassemble_tm_frames(+list(compound),+integer,+atom,+compound,-list(compound),-compound) - one_or_error

| Exceptions: | Frames, SecondaryHeaderLength, Policy, or State is a variable: | instantiation_error | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | Policy is neither a variable nor a valid discontinuity recovery policy: | domain_error(ccsds_discontinuity_policy,Policy) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | An element Frame of Frames is neither a variable nor a valid TM transfer frame term: | domain_error(ccsds_tm_transfer_frame_term,Frame) | The TM frame sequence is discontinuous under the throw recovery policy: | domain_error(ccsds_tm_transfer_frame_sequence,tm_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current TM frame counter moduli differ: | domain_error(ccsds_tm_transfer_frame_counter_modulus,tm_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_tm_frames/7 .. _ccsds_packet_services/0::reassemble_tm_frames/7:

reassemble_tm_frames/7 ^^^^^^^^^^^^^^^^^^^^^^^^^^

Reassembles complete packets across a sequence of TM transfer frames using the selected discontinuity recovery policy and returns any recovery events in frame order.

| Compilation flags: | static

| Template: | reassemble_tm_frames(Frames,SecondaryHeaderLength,Policy,State,Packets,UpdatedState,Events) | Mode and number of proofs: | reassemble_tm_frames(+list(compound),+integer,+atom,+compound,-list(compound),-compound,-list(compound)) - one_or_error

| Exceptions: | Frames, SecondaryHeaderLength, Policy, or State is a variable: | instantiation_error | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | Policy is neither a variable nor a valid discontinuity recovery policy: | domain_error(ccsds_discontinuity_policy,Policy) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | An element Frame of Frames is neither a variable nor a valid TM transfer frame term: | domain_error(ccsds_tm_transfer_frame_term,Frame) | The TM frame sequence is discontinuous under the throw recovery policy: | domain_error(ccsds_tm_transfer_frame_sequence,tm_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current TM frame counter moduli differ: | domain_error(ccsds_tm_transfer_frame_counter_modulus,tm_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_aos_packets/5 .. _ccsds_packet_services/0::reassemble_aos_packets/5:

reassemble_aos_packets/5 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Extracts the packet zone from an AOS transfer frame, using the default throw discontinuity recovery policy, and returns the complete packets plus the updated channel reassembly state.

| Compilation flags: | static

| Template: | reassemble_aos_packets(Frame,SecondaryHeaderLength,State,Packets,UpdatedState) | Mode and number of proofs: | reassemble_aos_packets(+compound,+integer,+compound,-list(compound),-compound) - one_or_error

| Exceptions: | Frame, SecondaryHeaderLength, or State is a variable: | instantiation_error | Frame is neither a variable nor a valid AOS transfer frame term: | domain_error(ccsds_aos_transfer_frame_term,Frame) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | The AOS frame sequence is discontinuous: | domain_error(ccsds_aos_transfer_frame_sequence,aos_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current AOS frame counter moduli differ: | domain_error(ccsds_aos_transfer_frame_counter_modulus,aos_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_aos_packets/6 .. _ccsds_packet_services/0::reassemble_aos_packets/6:

reassemble_aos_packets/6 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Extracts the packet zone from an AOS transfer frame, applies the selected discontinuity recovery policy when frame-count continuity is broken, and returns the complete packets plus the updated channel reassembly state.

| Compilation flags: | static

| Template: | reassemble_aos_packets(Frame,SecondaryHeaderLength,Policy,State,Packets,UpdatedState) | Mode and number of proofs: | reassemble_aos_packets(+compound,+integer,+atom,+compound,-list(compound),-compound) - one_or_error

| Exceptions: | Frame, SecondaryHeaderLength, Policy, or State is a variable: | instantiation_error | Frame is neither a variable nor a valid AOS transfer frame term: | domain_error(ccsds_aos_transfer_frame_term,Frame) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | Policy is neither a variable nor a valid discontinuity recovery policy: | domain_error(ccsds_discontinuity_policy,Policy) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | The AOS frame sequence is discontinuous under the throw recovery policy: | domain_error(ccsds_aos_transfer_frame_sequence,aos_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current AOS frame counter moduli differ: | domain_error(ccsds_aos_transfer_frame_counter_modulus,aos_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_aos_packets/7 .. _ccsds_packet_services/0::reassemble_aos_packets/7:

reassemble_aos_packets/7 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Extracts the packet zone from an AOS transfer frame, applies the selected discontinuity recovery policy when frame-count continuity is broken, and returns the complete packets, updated channel reassembly state, and explicit recovery events.

| Compilation flags: | static

| Template: | reassemble_aos_packets(Frame,SecondaryHeaderLength,Policy,State,Packets,UpdatedState,Events) | Mode and number of proofs: | reassemble_aos_packets(+compound,+integer,+atom,+compound,-list(compound),-compound,-list(compound)) - one_or_error

| Exceptions: | Frame, SecondaryHeaderLength, Policy, or State is a variable: | instantiation_error | Frame is neither a variable nor a valid AOS transfer frame term: | domain_error(ccsds_aos_transfer_frame_term,Frame) | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | Policy is neither a variable nor a valid discontinuity recovery policy: | domain_error(ccsds_discontinuity_policy,Policy) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | The AOS frame sequence is discontinuous under the throw recovery policy: | domain_error(ccsds_aos_transfer_frame_sequence,aos_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current AOS frame counter moduli differ: | domain_error(ccsds_aos_transfer_frame_counter_modulus,aos_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_aos_frames/5 .. _ccsds_packet_services/0::reassemble_aos_frames/5:

reassemble_aos_frames/5 ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Reassembles complete packets across a sequence of AOS transfer frames using the default throw discontinuity recovery policy.

| Compilation flags: | static

| Template: | reassemble_aos_frames(Frames,SecondaryHeaderLength,State,Packets,UpdatedState) | Mode and number of proofs: | reassemble_aos_frames(+list(compound),+integer,+compound,-list(compound),-compound) - one_or_error

| Exceptions: | Frames, SecondaryHeaderLength, or State is a variable: | instantiation_error | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | An element Frame of Frames is neither a variable nor a valid AOS transfer frame term: | domain_error(ccsds_aos_transfer_frame_term,Frame) | The AOS frame sequence is discontinuous: | domain_error(ccsds_aos_transfer_frame_sequence,aos_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current AOS frame counter moduli differ: | domain_error(ccsds_aos_transfer_frame_counter_modulus,aos_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_aos_frames/6 .. _ccsds_packet_services/0::reassemble_aos_frames/6:

reassemble_aos_frames/6 ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Reassembles complete packets across a sequence of AOS transfer frames using the selected discontinuity recovery policy.

| Compilation flags: | static

| Template: | reassemble_aos_frames(Frames,SecondaryHeaderLength,Policy,State,Packets,UpdatedState) | Mode and number of proofs: | reassemble_aos_frames(+list(compound),+integer,+atom,+compound,-list(compound),-compound) - one_or_error

| Exceptions: | Frames, SecondaryHeaderLength, Policy, or State is a variable: | instantiation_error | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | Policy is neither a variable nor a valid discontinuity recovery policy: | domain_error(ccsds_discontinuity_policy,Policy) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | An element Frame of Frames is neither a variable nor a valid AOS transfer frame term: | domain_error(ccsds_aos_transfer_frame_term,Frame) | The AOS frame sequence is discontinuous under the throw recovery policy: | domain_error(ccsds_aos_transfer_frame_sequence,aos_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current AOS frame counter moduli differ: | domain_error(ccsds_aos_transfer_frame_counter_modulus,aos_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

.. index:: reassemble_aos_frames/7 .. _ccsds_packet_services/0::reassemble_aos_frames/7:

reassemble_aos_frames/7 ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Reassembles complete packets across a sequence of AOS transfer frames using the selected discontinuity recovery policy and returns any recovery events in frame order.

| Compilation flags: | static

| Template: | reassemble_aos_frames(Frames,SecondaryHeaderLength,Policy,State,Packets,UpdatedState,Events) | Mode and number of proofs: | reassemble_aos_frames(+list(compound),+integer,+atom,+compound,-list(compound),-compound,-list(compound)) - one_or_error

| Exceptions: | Frames, SecondaryHeaderLength, Policy, or State is a variable: | instantiation_error | SecondaryHeaderLength is neither a variable nor a valid CCSDS packet secondary header length: | domain_error(ccsds_secondary_header_length,SecondaryHeaderLength) | Policy is neither a variable nor a valid discontinuity recovery policy: | domain_error(ccsds_discontinuity_policy,Policy) | State is neither a variable nor a valid channel reassembly state term: | domain_error(ccsds_channel_reassembly_state,State) | An element Frame of Frames is neither a variable nor a valid AOS transfer frame term: | domain_error(ccsds_aos_transfer_frame_term,Frame) | The AOS frame sequence is discontinuous under the throw recovery policy: | domain_error(ccsds_aos_transfer_frame_sequence,aos_transfer_frame_sequence(SpacecraftId,VirtualChannelId,ExpectedFrameCount,VirtualChannelFrameCount)) | The stored and current AOS frame counter moduli differ: | domain_error(ccsds_aos_transfer_frame_counter_modulus,aos_transfer_frame_counter_modulus(SpacecraftId,VirtualChannelId,StoredCounterModulus,CounterModulus)) | A pending fragment cannot be continued by the packet zone prefix data: | domain_error(ccsds_packet_reassembly_continuation,packet_reassembly_state(PendingData)) | A continuation fragment is followed by a new packet before the previous packet is completed: | domain_error(ccsds_packet_reassembly_continuation,incomplete_continuation_before_new_packet)

---

Protected predicates

(no local declarations; see entity ancestors if any)

Private predicates

(no local declarations; see entity ancestors if any)

Operators

(none)