PM-PTN-0020
If Partitions exist, state selection is per Partition
Should Partitions be adopted, every State MUST belong to exactly one Partition, and the selection rule that resolves PM-STR-0030 MUST be applied within a Partition rather than across a Thing's States as a whole. PO-0002 and PO-0003 MUST then be discharged per Partition.
Non-normative: this is stated now, conditionally, because it changes what the proof obligations mean. Across a whole Thing, "at most one State is selected" is false for any object with two lifecycles, and would look like a defect in the model rather than a defect in the obligation.
PO-0002andPO-0003are already written per "state dimension" for this reason; this assertion is what that phrase refers to.
DESIGN MUST · draft · area PTN · since 0.1.1
Source
No source citation — trust token DESIGN; see the reasoning above.