diff --git a/specs/ObjectProcessing.cfg b/specs/ObjectProcessing.cfg index 7e351d7..5d9fa14 100644 --- a/specs/ObjectProcessing.cfg +++ b/specs/ObjectProcessing.cfg @@ -7,8 +7,10 @@ SPECIFICATION INVARIANTS TypeInv - TargetStateConsistent + DistinctObjectStates + TargetValidity PROPERTIES - EventualTargetFinalization PermanentFinalization + EventualTargetFinalization + EventualTargetResolution diff --git a/specs/ObjectProcessing.tla b/specs/ObjectProcessing.tla index 7552127..f0cbc48 100644 --- a/specs/ObjectProcessing.tla +++ b/specs/ObjectProcessing.tla @@ -128,7 +128,9 @@ Next == * eventually finalized. *) Fairness == - /\ \A o \in ObjectId: WF_vars(o \in objectTargets /\ FinalizeObjects({o})) + \A o \in ObjectId: + EventuallyFinalized(o) :: + WF_vars(o \in objectTargets /\ FinalizeObjects({o})) (** * Full system specification. @@ -148,35 +150,32 @@ Spec == * SAFETY * An object can only be targeted if it is known to the system. *) -TargetStateConsistent == +TargetValidity == objectTargets \intersect UnknownObject = {} +(** + * SAFETY + * Once an object reaches the FINALIZED state, it remains there permanently. + *) +PermanentFinalization == + \A o \in ObjectId: + [](o \in FinalizedObject => [](o \in FinalizedObject)) + (** * LIVENESS * Every targeted object is eventually either finalized or untargeted. *) EventualTargetFinalization == \A o \in ObjectId: - o \in objectTargets ~> (o \in FinalizedObject \/ o \notin objectTargets) + <>[](o \in objectTargets) => <>(o \in FinalizedObject) (** * LIVENESS - * Once an object reaches the FINALIZED state, it remains there permanently. + * Any object added to the target set must eventually be resolved, + * meaning it is either finalized or removed from the target set. *) -PermanentFinalization == - \A o \in ObjectId: - [](o \in FinalizedObject => [](o \in FinalizedObject)) - -------------------------------------------------------------------------------- - -(*****************************************************************************) -(* THEOREMS *) -(*****************************************************************************) - -THEOREM Spec => []TypeInv -THEOREM Spec => []DistinctObjectStates -THEOREM Spec => []TargetStateConsistent -THEOREM Spec => EventualTargetFinalization -THEOREM Spec => PermanentFinalization +EventualTargetResolution == + \A o \in ObjectId : + o \in objectTargets ~> (o \in FinalizedObject \/ o \notin objectTargets) =============================================================================== \ No newline at end of file diff --git a/specs/ObjectProcessing_proof.tla b/specs/ObjectProcessing_proof.tla new file mode 100644 index 0000000..bd83ac1 --- /dev/null +++ b/specs/ObjectProcessing_proof.tla @@ -0,0 +1,108 @@ +------------------------ MODULE ObjectProcessing_proof ------------------------ +EXTENDS ObjectProcessing, TLAPS + +THEOREM TypeCorrect == Spec => []TypeInv +<1>. USE DEF OBJECT_UNKNOWN, OBJECT_REGISTERED, OBJECT_FINALIZED, UnknownObject, + RegisteredObject, FinalizedObject +<1>1. Init => TypeInv + BY DEF Init, TypeInv +<1>2. TypeInv /\ [Next]_vars => TypeInv' + BY DEF TypeInv, Next, vars, RegisterObjects, TargetObjects, + UntargetObjects, FinalizeObjects, Terminating +<1>. QED + BY <1>1, <1>2, PTL DEF Spec + +THEOREM DistinctObjectStatesCorrect == Spec => []DistinctObjectStates +<1>. USE DEF IsPairwiseDisjoint, OBJECT_UNKNOWN, OBJECT_REGISTERED, + OBJECT_FINALIZED, OBJECT_COMPLETED, OBJECT_ABORTED, OBJECT_DELETED, + UnknownObject, RegisteredObject, FinalizedObject, CompletedObject, + AbortedObject, DeletedObject +<1>1. Init => DistinctObjectStates + BY DEF Init, DistinctObjectStates +<1>2. TypeInv /\ DistinctObjectStates /\ [Next]_vars => DistinctObjectStates' + BY DEF TypeInv, DistinctObjectStates, Next, vars, RegisterObjects, + TargetObjects, UntargetObjects, FinalizeObjects, Terminating +<1>. QED + BY <1>1, <1>2, TypeCorrect, PTL DEF Spec + +THEOREM TargetValidityCorrect == Spec => []TargetValidity +<1>. USE DEF OBJECT_UNKNOWN, OBJECT_REGISTERED, OBJECT_FINALIZED, UnknownObject, + RegisteredObject, FinalizedObject +<1>1. Init => TargetValidity + BY DEF Init, TargetValidity +<1>2. TypeInv /\ TargetValidity /\ [Next]_vars => TargetValidity' + BY DEF TargetValidity, TypeInv, Next, vars, RegisterObjects, + TargetObjects, UntargetObjects, FinalizeObjects, Terminating +<1>. QED + BY <1>1, <1>2, TypeCorrect, PTL DEF Spec + +ObjectSafetyInv == + /\ TypeInv + /\ DistinctObjectStates + /\ TargetValidity + +THEOREM ObjectSafetyInvCorrect == Spec => []ObjectSafetyInv +BY TypeCorrect, DistinctObjectStatesCorrect, TargetValidityCorrect, PTL + DEF ObjectSafetyInv + +THEOREM PermanentFinalizationCorrect == Spec => PermanentFinalization +<1>. SUFFICES ASSUME NEW o \in ObjectId + PROVE Spec => [](o \in FinalizedObject => [](o \in FinalizedObject)) + BY DEF PermanentFinalization +<1>. USE DEF OBJECT_UNKNOWN, OBJECT_REGISTERED, OBJECT_FINALIZED, UnknownObject, + RegisteredObject, FinalizedObject +<1>1. TypeInv /\ o \in FinalizedObject /\ [Next]_vars + => (o \in FinalizedObject)' + BY DEF TypeInv, Next, vars, RegisterObjects, TargetObjects, + UntargetObjects, FinalizeObjects, Terminating +<1>. QED + BY <1>1, TypeCorrect, PTL DEF Spec + +LEMMA TargetsAreKnown == ASSUME NEW o \in objectTargets + PROVE ObjectSafetyInv => \/ o \in RegisteredObject + \/ o \in FinalizedObject +BY DEF ObjectSafetyInv, TypeInv, DistinctObjectStates, TargetValidity, + OBJECT_UNKNOWN, OBJECT_REGISTERED, OBJECT_FINALIZED, UnknownObject, + RegisteredObject, FinalizedObject + +THEOREM EventualTargetFinalizationCorrect == Spec => EventualTargetFinalization +<1>. SUFFICES ASSUME NEW o \in ObjectId + PROVE Spec => (<>[](o \in objectTargets) => <>(o \in FinalizedObject)) + BY DEF EventualTargetFinalization +<1>1. Fairness => Fairness!EventuallyFinalized(o) + BY DEF Fairness +<1>2. []ObjectSafetyInv /\ [][Next]_vars /\ Fairness!EventuallyFinalize(o) /\ [](o \in objectTargets) + => <>(o \in FinalizedObject) + <2>. USE DEF OBJECT_FINALIZED, FinalizedObject + <2>1. ObjectSafetyInv /\ (o \in objectTargets) /\ ~(o \in FinalizedObject) + => ENABLED <>_vars + BY ExpandENABLED, TargetsAreKnown DEF FinalizeObjects, vars + <2>2. <>_vars => (o \in FinalizedObject)' + BY DEF FinalizeObjects, vars + <2>3. QED + BY <2>1, <2>2, PTL +<1> QED + BY <1>1, <1>2, PTL, ObjectSafetyInvCorrect DEF Spec + +THEOREM EventualTargetResolutionCorrect == Spec => EventualTargetResolution +<1>. SUFFICES ASSUME NEW o \in ObjectId + PROVE Spec => (o \in objectTargets ~> (o \in FinalizedObject \/ o \notin objectTargets)) + BY DEF EventualTargetResolution +<1>1. o \in objectTargets /\ [Next]_vars => \/ (o \in objectTargets)' + \/ (o \in FinalizedObject)' + \/ (o \notin objectTargets)' + BY DEF Next, vars, RegisterObjects, TargetObjects, UntargetObjects, + FinalizeObjects, Terminating +<1>2. <>_vars + => (o \in FinalizedObject)' + BY DEF FinalizeObjects, OBJECT_REGISTERED, OBJECT_FINALIZED, + RegisteredObject, FinalizedObject +<1>3. ObjectSafetyInv /\ o \in objectTargets => ENABLED <>_vars \/ o \in FinalizedObject + BY ExpandENABLED, TargetsAreKnown DEF FinalizeObjects, vars, + OBJECT_REGISTERED, OBJECT_FINALIZED, RegisteredObject, FinalizedObject +<1>4. Fairness => Fairness!EventuallyFinalize(o) + BY DEF Fairness +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, ObjectSafetyInvCorrect, PTL DEF Spec, ObjectSafetyInv + +=============================================================================== \ No newline at end of file diff --git a/specs/ObjectStates.tla b/specs/ObjectStates.tla index e5afffe..95e592c 100644 --- a/specs/ObjectStates.tla +++ b/specs/ObjectStates.tla @@ -8,9 +8,9 @@ (* allowing other specifications to reason about groups of objects sharing *) (* the same lifecycle phase. *) (*****************************************************************************) +EXTENDS Utils LOCAL INSTANCE FiniteSets -LOCAL INSTANCE Utils (** * Abstract operator returning the set of objects in a given state. diff --git a/specs/TaskProcessing.cfg b/specs/TaskProcessing.cfg index e74e4b6..7d92682 100644 --- a/specs/TaskProcessing.cfg +++ b/specs/TaskProcessing.cfg @@ -10,10 +10,14 @@ SPECIFICATION INVARIANTS TypeInv - AllocConsistent + DistinctTaskStates AllocStateConsistent ExclusiveAssignment PROPERTY PermanentFinalization + EventualStaging + EventualDeallocation + EventualProcessing + EventualFinalization EventualQuiescence diff --git a/specs/TaskProcessing.tla b/specs/TaskProcessing.tla index d394370..fc4f3b9 100644 --- a/specs/TaskProcessing.tla +++ b/specs/TaskProcessing.tla @@ -8,6 +8,8 @@ (* properties of the system. *) (*****************************************************************************) +EXTENDS Utils + CONSTANTS AgentId, \* Set of agent identifiers (theoretically infinite) TaskId \* Set of task identifiers (theoretically infinite) @@ -165,9 +167,9 @@ Next == *) Fairness == \A t \in TaskId: - /\ WF_vars(StageTasks({t})) - /\ SF_vars(\E a \in AgentId : ProcessTasks(a, {t})) - /\ WF_vars(FinalizeTasks({t})) + /\ EventuallyStaged(t) :: WF_vars(StageTasks({t})) + /\ EventuallyProcessed(t) :: SF_vars(\E a \in AgentId : ProcessTasks(a, {t})) + /\ EventuallyFinalized(t) :: WF_vars(FinalizeTasks({t})) (** * Full system specification. @@ -183,18 +185,11 @@ Spec == (* SAFETY AND LIVENESS PROPERTIES *) (*****************************************************************************) -(** - * SAFETY - * The set of all allocated tasks always belongs to the universe of tasks. - *) -AllocConsistent == - UNION {agentTaskAlloc[a] : a \in AgentId} \subseteq TaskId - (** * SAFETY * A task is assigned to an agent if and only if it is in the ASISGNED state. *) -AllocStateConsistent == +AssignedStateIntegrity == \A t \in TaskId: t \in AssignedTask <=> \E a \in AgentId: t \in agentTaskAlloc[a] @@ -213,6 +208,40 @@ ExclusiveAssignment == PermanentFinalization == \A t \in TaskId: [](t \in FinalizedTask => [](t \in FinalizedTask)) +(** + * LIVENESS + * Every registered task is eventually staged for processing. + *) +EventualStaging == + \A t \in TaskId : + t \in RegisteredTask ~> t \in StagedTask + +(** + * LIVENESS + * Any task assigned to an agent will eventually be either released back + * to the staged pool or successfully processed. + *) +EventualDeallocation == + \A t \in TaskId : + t \in AssignedTask ~> t \in StagedTask \/ t \in ProcessedTask + +(** + * LIVENESS + * If a task is repeatedly assigned to agents, it must eventually reach + * the processed state. + *) +EventualProcessing == + \A t \in TaskId : + []<>(t \in AssignedTask) => <>(t \in ProcessedTask) + +(** + * LIVENESS + * Every processed task will eventually reach the finalized state. + *) +EventualFinalization == + \A t \in TaskId : + t \in ProcessedTask ~> t \in FinalizedTask + (** * LIVENESS * Any staged task ultimately remains in the STAGED or FINALIZED state. @@ -223,17 +252,4 @@ EventualQuiescence == \/ [](t \in StagedTask) \/ [](t \in FinalizedTask) -------------------------------------------------------------------------------- - -(*****************************************************************************) -(* THEOREMS *) -(*****************************************************************************) - -THEOREM Spec => []TypeInv -THEOREM Spec => []AllocConsistent -THEOREM Spec => []AllocStateConsistent -THEOREM Spec => []ExclusiveAssignment -THEOREM Spec => PermanentFinalization -THEOREM Spec => EventualQuiescence - -============================================================================= \ No newline at end of file +=============================================================================== \ No newline at end of file diff --git a/specs/TaskProcessing_proof.tla b/specs/TaskProcessing_proof.tla new file mode 100644 index 0000000..445202e --- /dev/null +++ b/specs/TaskProcessing_proof.tla @@ -0,0 +1,216 @@ +------------------------- MODULE TaskProcessing_proof ------------------------- +EXTENDS TaskProcessing, TLAPS + +THEOREM TypeCorrect == Spec => []TypeInv +<1>. USE DEF TASK_UNKNOWN, TASK_REGISTERED, TASK_STAGED, TASK_ASSIGNED, TASK_PROCESSED, + TASK_FINALIZED, UnknownTask, RegisteredTask, StagedTask, AssignedTask, + ProcessedTask, FinalizedTask +<1>1. Init => TypeInv + BY DEF Init, TypeInv +<1>2. TypeInv /\ [Next]_vars => TypeInv' + BY DEF TypeInv, Next, vars, RegisterTasks, StageTasks, AssignTasks, ReleaseTasks, ProcessTasks, FinalizeTasks, Terminating +<1>. QED + BY <1>1, <1>2, PTL DEF Spec + +THEOREM DistinctTaskStatesCorrect == Spec => []DistinctTaskStates +<1>. USE DEF IsPairwiseDisjoint, TASK_UNKNOWN, TASK_REGISTERED, TASK_STAGED, + TASK_ASSIGNED, TASK_PROCESSED, TASK_FINALIZED, UnknownTask, + RegisteredTask, StagedTask, AssignedTask, ProcessedTask, FinalizedTask +<1>1. Init => DistinctTaskStates + BY DEF Init, DistinctTaskStates +<1>2. TypeInv /\ DistinctTaskStates /\ [Next]_vars => DistinctTaskStates' + BY DEF TypeInv, DistinctTaskStates, Next, vars, RegisterTasks, StageTasks, + AssignTasks, ReleaseTasks, ProcessTasks, FinalizeTasks, Terminating +<1>. QED + BY <1>1, <1>2, TypeCorrect, PTL DEF Spec + +TaskSafetyInv == + /\ TypeInv + /\ DistinctTaskStates + /\ AssignedStateIntegrity + /\ ExclusiveAssignment + +THEOREM TaskSafetyInvCorrect == Spec => []TaskSafetyInv +<1>1. TypeInv /\ Init => AssignedStateIntegrity /\ ExclusiveAssignment + BY DEF Init, TypeInv, AssignedStateIntegrity, ExclusiveAssignment, AssignedTask, + TASK_UNKNOWN, TASK_ASSIGNED +<1>2. TypeInv /\ AssignedStateIntegrity /\ ExclusiveAssignment /\ [Next]_vars + => AssignedStateIntegrity' /\ ExclusiveAssignment' + <2>. SUFFICES ASSUME TypeInv, AssignedStateIntegrity, ExclusiveAssignment, [Next]_vars + PROVE AssignedStateIntegrity' /\ ExclusiveAssignment' + OBVIOUS + <2>. USE DEF TypeInv, AssignedStateIntegrity, ExclusiveAssignment, AssignedTask + <2>1. ASSUME NEW T \in SUBSET TaskId, RegisterTasks(T) + PROVE AssignedStateIntegrity' /\ ExclusiveAssignment' + BY <2>1 DEF RegisterTasks, UnknownTask, TASK_UNKNOWN, TASK_REGISTERED, TASK_ASSIGNED + <2>2. ASSUME NEW T \in SUBSET TaskId, StageTasks(T) + PROVE AssignedStateIntegrity' /\ ExclusiveAssignment' + BY <2>2 DEF StageTasks, RegisteredTask, TASK_REGISTERED, TASK_STAGED, TASK_ASSIGNED + <2>3. ASSUME NEW T \in SUBSET TaskId, NEW a \in AgentId, AssignTasks(a, T) + PROVE AssignedStateIntegrity' /\ ExclusiveAssignment' + BY <2>3 DEF AssignTasks, StagedTask, TASK_STAGED, TASK_ASSIGNED + <2>4. ASSUME NEW T \in SUBSET TaskId, NEW a \in AgentId, ReleaseTasks(a, T) + PROVE AssignedStateIntegrity' /\ ExclusiveAssignment' + BY <2>4 DEF ReleaseTasks, TASK_STAGED, TASK_ASSIGNED + <2>5. ASSUME NEW T \in SUBSET TaskId, NEW a \in AgentId, ProcessTasks(a, T) + PROVE AssignedStateIntegrity' /\ ExclusiveAssignment' + BY <2>5 DEF ProcessTasks, TASK_ASSIGNED, TASK_PROCESSED + <2>6. ASSUME NEW T \in SUBSET TaskId, FinalizeTasks(T) + PROVE AssignedStateIntegrity' /\ ExclusiveAssignment' + BY <2>6 DEF FinalizeTasks, ProcessedTask, TASK_PROCESSED, TASK_FINALIZED, TASK_ASSIGNED + <2>7. CASE Terminating + BY <2>7 DEF Terminating, vars + <2>8. CASE UNCHANGED vars + BY <2>8 DEF vars + <2>. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8 DEF Next +<1>. QED + BY <1>1, <1>2, TypeCorrect, DistinctTaskStatesCorrect, PTL DEF Spec, TaskSafetyInv + +THEOREM AssignedStateIntegrityCorrect == Spec => []AssignedStateIntegrity +BY TaskSafetyInvCorrect, PTL DEF TaskSafetyInv + +THEOREM ExclusiveAssignmentCorrect == Spec => []ExclusiveAssignment +BY TaskSafetyInvCorrect, PTL DEF TaskSafetyInv + +THEOREM PermanentFinalizationCorrect == Spec => PermanentFinalization +<1>. SUFFICES ASSUME NEW t \in TaskId + PROVE Spec => [](t \in FinalizedTask => [](t \in FinalizedTask)) + BY DEF PermanentFinalization +<1>. USE DEF TASK_UNKNOWN, TASK_REGISTERED, TASK_STAGED, TASK_ASSIGNED, TASK_PROCESSED, + TASK_FINALIZED, UnknownTask, RegisteredTask, StagedTask, AssignedTask, + ProcessedTask, FinalizedTask +<1>1. TaskSafetyInv /\ t \in FinalizedTask /\ [Next]_vars + => (t \in FinalizedTask)' + BY DEF TaskSafetyInv, TypeInv, AssignedStateIntegrity, ExclusiveAssignment, + Next, vars, RegisterTasks, StageTasks, AssignTasks, ReleaseTasks, + ProcessTasks, FinalizeTasks, Terminating +<1>2. QED + BY <1>1, TaskSafetyInvCorrect, PTL DEF Spec + +THEOREM EventualStagingCorrect == Spec => EventualStaging +<1>. SUFFICES ASSUME NEW t \in TaskId + PROVE Spec => t \in RegisteredTask ~> t \in StagedTask + BY DEF EventualStaging +<1>1. Fairness => Fairness!EventuallyStaged(t) + BY DEF Fairness +<1>. USE DEF TASK_UNKNOWN, TASK_REGISTERED, TASK_STAGED, TASK_ASSIGNED, TASK_PROCESSED, + TASK_FINALIZED, UnknownTask, RegisteredTask, StagedTask, AssignedTask, + ProcessedTask, FinalizedTask +<1>2. TaskSafetyInv /\ t \in RegisteredTask /\ [Next]_vars => (t \in RegisteredTask)' \/ (t \in StagedTask)' + BY DEF TaskSafetyInv, TypeInv, AssignedStateIntegrity, Next, vars, RegisterTasks, + StageTasks, AssignTasks, ReleaseTasks, ProcessTasks, FinalizeTasks, + Terminating +<1>3. t \in RegisteredTask /\ <>_vars => (t \in StagedTask)' + BY DEF StageTasks +<1>4. t \in RegisteredTask => ENABLED <>_vars + BY ExpandENABLED DEF StageTasks, vars +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, TaskSafetyInvCorrect, PTL DEF Spec + +LEMMA AssignmentEnablesProcessing == ASSUME NEW t \in TaskId +PROVE TaskSafetyInv /\ t \in AssignedTask + => ENABLED <<\E a \in AgentId: ProcessTasks(a, {t})>>_vars +<1>. SUFFICES ASSUME TaskSafetyInv + PROVE t \in AssignedTask => ENABLED <<\E a \in AgentId: ProcessTasks(a, {t})>>_vars + OBVIOUS +<1>1. <<\E a \in AgentId: ProcessTasks(a, {t})>>_vars <=> \E a \in AgentId: ProcessTasks(a, {t}) + BY DEF TaskSafetyInv, TypeInv, vars, ProcessTasks +<1>2. (ENABLED <<\E a \in AgentId: ProcessTasks(a, {t})>>_vars) <=> ENABLED (\E a \in AgentId: ProcessTasks(a, {t})) + BY <1>1, ENABLEDaxioms +<1>3. t \in AssignedTask => ENABLED (\E a \in AgentId: ProcessTasks(a, {t})) + BY ExpandENABLED DEF TaskSafetyInv, TypeInv, AssignedStateIntegrity, ProcessTasks +<1>. QED + BY <1>2, <1>3 + +THEOREM EventualDeallocationCorrect == Spec => EventualDeallocation +<1>. SUFFICES ASSUME NEW t \in TaskId + PROVE Spec => t \in AssignedTask ~> t \in StagedTask \/ t \in ProcessedTask + BY DEF EventualDeallocation +<1>1. t \in AssignedTask /\ [Next]_vars => \/ (t \in AssignedTask)' + \/ (t \in StagedTask)' + \/ (t \in ProcessedTask)' + <2>. SUFFICES ASSUME NEW T \in SUBSET TaskId, t \in AssignedTask + PROVE [\/ RegisterTasks(T) + \/ StageTasks(T) + \/ \E a \in AgentId: + \/ AssignTasks(a, T) + \/ ReleaseTasks(a, T) + \/ ProcessTasks(a, T) + \/ FinalizeTasks(T) + \/ Terminating]_vars => \/ (t \in AssignedTask)' + \/ (t \in StagedTask)' + \/ (t \in ProcessedTask)' + BY DEF Next + <2>. QED + BY DEF RegisterTasks, StageTasks, AssignTasks, ReleaseTasks, ProcessTasks, + FinalizeTasks, Terminating, vars, UnknownTask, RegisteredTask, StagedTask, + AssignedTask, ProcessedTask, FinalizedTask, TASK_UNKNOWN, + TASK_REGISTERED, TASK_STAGED, TASK_ASSIGNED, TASK_PROCESSED, TASK_FINALIZED +<1>2. TaskSafetyInv /\ t \in AssignedTask /\ <<\E a \in AgentId : ProcessTasks(a, {t})>>_vars => (t \in ProcessedTask)' + BY DEF TaskSafetyInv, TypeInv, ProcessTasks, AssignedTask, ProcessedTask +<1>3. TaskSafetyInv /\ t \in AssignedTask => ENABLED <<\E a \in AgentId : ProcessTasks(a, {t})>>_vars + BY AssignmentEnablesProcessing +<1>4. Fairness => SF_vars(\E a \in AgentId : ProcessTasks(a, {t})) + BY DEF Fairness +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, TaskSafetyInvCorrect, PTL DEF Spec + +THEOREM EventualProcessingCorrect == Spec => EventualProcessing +<1>. SUFFICES ASSUME NEW t \in TaskId + PROVE Spec => ([]<>(t \in AssignedTask) => <>(t \in ProcessedTask)) + BY DEF EventualProcessing +<1>1. TaskSafetyInv /\ t \in AssignedTask => ENABLED <<\E a \in AgentId: ProcessTasks(a, {t})>>_vars + BY AssignmentEnablesProcessing +<1>2. <<\E a \in AgentId: ProcessTasks(a, {t})>>_vars => (t \in ProcessedTask)' + BY DEF ProcessTasks, ProcessedTask +<1>3. Fairness => Fairness!EventuallyProcessed(t) + BY DEF Fairness +<1>. QED + BY <1>1, <1>2, <1>3, TaskSafetyInvCorrect, PTL DEF Spec + +THEOREM EventualFinalizationCorrect == Spec => EventualFinalization +<1>. SUFFICES ASSUME NEW t \in TaskId + PROVE Spec => t \in ProcessedTask ~> t \in FinalizedTask + BY DEF EventualFinalization +<1>1. Fairness => Fairness!EventuallyFinalized(t) + BY DEF Fairness +<1>. USE DEF TASK_UNKNOWN, TASK_REGISTERED, TASK_STAGED, TASK_ASSIGNED, TASK_PROCESSED, + TASK_FINALIZED, UnknownTask, RegisteredTask, StagedTask, AssignedTask, + ProcessedTask, FinalizedTask +<1>2. TaskSafetyInv /\ t \in ProcessedTask /\ [Next]_vars => (t \in ProcessedTask)' \/ (t \in FinalizedTask)' + BY DEF TaskSafetyInv, TypeInv, AssignedStateIntegrity, Next, vars, RegisterTasks, + StageTasks, AssignTasks, ReleaseTasks, ProcessTasks, FinalizeTasks, + Terminating +<1>3. t \in ProcessedTask /\ <>_vars => (t \in FinalizedTask)' + BY DEF FinalizeTasks +<1>4. t \in ProcessedTask => ENABLED <>_vars + BY ExpandENABLED DEF FinalizeTasks, vars +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, TaskSafetyInvCorrect, PTL DEF Spec + +THEOREM EventualQuiescenceCorrect == Spec => EventualQuiescence +<1>. SUFFICES ASSUME NEW t \in TaskId + PROVE Spec => (t \in RegisteredTask ~> \/ [](t \in StagedTask) + \/ [](t \in FinalizedTask)) + BY DEF EventualQuiescence +<1>1. Spec => (t \in RegisteredTask ~> t \in StagedTask) + BY EventualStagingCorrect DEF EventualStaging +<1>2. TaskSafetyInv /\ t \in StagedTask /\ [Next]_vars => (t \in StagedTask)' \/ (t \in AssignedTask)' + BY DEF TaskSafetyInv, TypeInv, AssignedStateIntegrity, Next, vars, RegisterTasks, + StageTasks, AssignTasks, ReleaseTasks, ProcessTasks, FinalizeTasks, + Terminating, TASK_UNKNOWN, TASK_REGISTERED, TASK_STAGED, TASK_ASSIGNED, + TASK_PROCESSED, TASK_FINALIZED, UnknownTask, RegisteredTask, StagedTask, + AssignedTask, ProcessedTask, FinalizedTask +<1>3. Spec => (t \in AssignedTask ~> t \in StagedTask \/ t \in ProcessedTask) + BY EventualDeallocationCorrect DEF EventualDeallocation +<1>4. Spec => ([]<>(t \in AssignedTask) => <>(t \in ProcessedTask)) + BY EventualProcessingCorrect DEF EventualProcessing +<1>5. Spec => (t \in ProcessedTask ~> t \in FinalizedTask) + BY EventualFinalizationCorrect DEF EventualFinalization +<1>6. Spec => [](t \in FinalizedTask => [](t \in FinalizedTask)) + BY PermanentFinalizationCorrect DEF PermanentFinalization +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, TaskSafetyInvCorrect, PTL DEF Spec + +=============================================================================== \ No newline at end of file diff --git a/specs/TaskStates.tla b/specs/TaskStates.tla index 549e6f3..fd77073 100644 --- a/specs/TaskStates.tla +++ b/specs/TaskStates.tla @@ -8,6 +8,7 @@ (* other specifications to reason about groups of tasks sharing the same *) (* lifecycle phase. *) (*****************************************************************************) +EXTENDS Utils LOCAL INSTANCE FiniteSets @@ -58,4 +59,25 @@ AssignedTask == SetOfTasksIn(TASK_ASSIGNED) ProcessedTask == SetOfTasksIn(TASK_PROCESSED) FinalizedTask == SetOfTasksIn(TASK_FINALIZED) + +(** + * SAFETY PROPERTY + * Asserts that the sets representing different task lifecycle stages are + * mutually disjoint. This ensures that every task exists in exactly one + * primary state at any given time, preventing logical overlaps (e.g., an + * object being both 'Completed' and 'Deleted'). + * + * Any specification instantiating the current module must have this property + * as an invariant. + *) +DistinctTaskStates == + IsPairwiseDisjoint({ + UnknownTask, + RegisteredTask, + StagedTask, + AssignedTask, + ProcessedTask, + FinalizedTask + }) + =============================================================================== \ No newline at end of file