3.11.1 Abstract Data Model

All necessary state information is specified in section 3.1.1.