diff --git a/specs/GraphProcessing.tla b/specs/GraphProcessing.tla index 6dddaab..206c551 100644 --- a/specs/GraphProcessing.tla +++ b/specs/GraphProcessing.tla @@ -260,6 +260,15 @@ FinalizeTasks(T) == IF t \in T THEN TASK_FINALIZED ELSE taskState[t]] /\ UNCHANGED << agentTaskAlloc, deps, objectState, objectTargets >> +(** + * TERMINAL STATE + * Action representing the terminal state of the system, reached once all + * targeted objects have been finalized. + *) +Terminating == + /\ OP!Terminating + /\ UNCHANGED << agentTaskAlloc, deps, taskState >> + ------------------------------------------------------------------------------- (*****************************************************************************) @@ -283,6 +292,7 @@ Next == \/ ReleaseTasks(a, T) \/ ProcessTasks(a, T) \/ FinalizeTasks(T) + \/ Terminating (** * Returns TRUE iff task 't' is upstream on an open (i.e., fully unexecuted) diff --git a/specs/GraphProcessing_mc.cfg b/specs/GraphProcessing_mc.cfg index ee5122e..ce63345 100644 --- a/specs/GraphProcessing_mc.cfg +++ b/specs/GraphProcessing_mc.cfg @@ -6,13 +6,13 @@ CONSTANTS ObjectId = {o, p, q} \* Task identifiers (model values) - TaskId = {t, u, v} + TaskId = {t, u} \* Override the Graphs operator with ACGraphs operator Graphs <- MCGraphs SPECIFICATION - MCSpec + Spec INVARIANTS TypeInv diff --git a/specs/GraphProcessing_mc.tla b/specs/GraphProcessing_mc.tla index 018ae7d..89d9a05 100644 --- a/specs/GraphProcessing_mc.tla +++ b/specs/GraphProcessing_mc.tla @@ -47,33 +47,6 @@ MCGraphs(Nodes) == -------------------------------------------------------------------------------- -(** - * Dummy action representing the terminal state of the system, reached once all - * targeted objects have been finalized. - *) -Terminating == - /\ objectTargets \subseteq FinalizedObject - /\ UNCHANGED vars - -(** - * Modified next-state action. Extends the original system behavior with the - * Terminating action to avoid artificial deadlocks due to the bounded task - * and object sets. - *) -MCNext == - \/ Next - \/ Terminating - -(** - * Modified full system specification. - *) -MCSpec == - /\ Init - /\ [][MCNext]_vars - /\ Fairness - --------------------------------------------------------------------------------- - (** * Symmetry relation between task, object and agent identifiers. *) diff --git a/specs/ObjectProcessing_mc.cfg b/specs/ObjectProcessing.cfg similarity index 95% rename from specs/ObjectProcessing_mc.cfg rename to specs/ObjectProcessing.cfg index 636832e..7e351d7 100644 --- a/specs/ObjectProcessing_mc.cfg +++ b/specs/ObjectProcessing.cfg @@ -3,7 +3,7 @@ CONSTANTS ObjectId = {o, p, q} SPECIFICATION - MCSpec + Spec INVARIANTS TypeInv diff --git a/specs/ObjectProcessing.tla b/specs/ObjectProcessing.tla index 385d3e1..3b37f24 100644 --- a/specs/ObjectProcessing.tla +++ b/specs/ObjectProcessing.tla @@ -94,6 +94,15 @@ FinalizeObjects(O) == [o \in ObjectId |-> IF o \in O THEN OBJECT_FINALIZED ELSE objectState[o]] /\ UNCHANGED objectTargets +(** + * TERMINAL STATE + * Action representing the terminal state of the system, reached once all + * targeted objects have been finalized. + *) +Terminating == + /\ objectTargets \subseteq FinalizedObject + /\ UNCHANGED vars + ------------------------------------------------------------------------------- (*****************************************************************************) @@ -105,11 +114,12 @@ FinalizeObjects(O) == * Defines all possible atomic transitions of the system. *) Next == - \E O \in SUBSET ObjectId: + \/ \E O \in SUBSET ObjectId: \/ RegisterObjects(O) \/ TargetObjects(O) \/ UntargetObjects(O) \/ FinalizeObjects(O) + \/ Terminating (** * FAIRNESS CONDITIONS diff --git a/specs/ObjectProcessing_mc.tla b/specs/ObjectProcessing_mc.tla deleted file mode 100644 index 7d16269..0000000 --- a/specs/ObjectProcessing_mc.tla +++ /dev/null @@ -1,46 +0,0 @@ --------------------------- MODULE ObjectProcessing_mc -------------------------- -(******************************************************************************) -(* Bounded model-checking extension of ObjectProcessing. *) -(* *) -(* For model checking, the set of object identifiers must be finite and *) -(* explicitly materialized. Since the number of objects is finite, the system *) -(* eventually reaches a state where no new objects can be registered which, *) -(* leads to an artificial deadlock. *) -(* *) -(* To avoid this spurious deadlock, the next-state action is overridden to *) -(* include a dummy terminal state, allowing the model checker to terminate *) -(* exploration gracefully. *) -(******************************************************************************) - -EXTENDS FiniteSets, ObjectProcessing - -ASSUME IsFiniteSet(ObjectId) - --------------------------------------------------------------------------------- - -(** - * Dummy action representing the terminal state of the system, reached once all - * targeted objects have been finalized. - *) -Terminating == - /\ objectTargets \subseteq FinalizedObject - /\ UNCHANGED vars - -(** - * Modified next-state action. Extends the original system behavior with the - * Terminating action to avoid artificial deadlocks due to the bounded object - * set. - *) -MCNext == - \/ Next - \/ Terminating - -(** - * Modified full system specification. - *) -MCSpec == - /\ Init - /\ [][MCNext]_vars - /\ Fairness - -================================================================================ \ No newline at end of file diff --git a/specs/TaskProcessing_mc.cfg b/specs/TaskProcessing.cfg similarity index 96% rename from specs/TaskProcessing_mc.cfg rename to specs/TaskProcessing.cfg index 270bebe..3abe4c4 100644 --- a/specs/TaskProcessing_mc.cfg +++ b/specs/TaskProcessing.cfg @@ -6,7 +6,7 @@ CONSTANTS TaskId = {t, u, v} SPECIFICATION - MCSpec + Spec INVARIANTS TypeInv diff --git a/specs/TaskProcessing.tla b/specs/TaskProcessing.tla index cdc8078..3611a76 100644 --- a/specs/TaskProcessing.tla +++ b/specs/TaskProcessing.tla @@ -112,6 +112,16 @@ FinalizeTasks(T) == [t \in TaskId |-> IF t \in T THEN TASK_FINALIZED ELSE taskState[t]] /\ UNCHANGED agentTaskAlloc +(** + * TERMINAL STATE + * Action representing the terminal state of the system, reached when + * there are no more tasks being processed (i.e., assigned to an agent or not + * yet finalized). + *) +Terminating == + /\ TaskId = UnknownTask \union StagedTask \union FinalizedTask + /\ UNCHANGED vars + ------------------------------------------------------------------------------- (*****************************************************************************) @@ -123,13 +133,14 @@ FinalizeTasks(T) == * Defines all possible atomic transitions of the system. *) Next == - \E T \in SUBSET TaskId: + \/ \E T \in SUBSET TaskId: \/ StageTasks(T) \/ \E a \in AgentId: \/ AssignTasks(a, T) \/ ReleaseTasks(a, T) \/ ProcessTasks(a, T) \/ FinalizeTasks(T) + \/ Terminating (** * FAIRNESS CONDITIONS diff --git a/specs/TaskProcessing_mc.tla b/specs/TaskProcessing_mc.tla deleted file mode 100644 index c04caaf..0000000 --- a/specs/TaskProcessing_mc.tla +++ /dev/null @@ -1,47 +0,0 @@ ---------------------------- MODULE TaskProcessing_mc --------------------------- -(*****************************************************************************) -(* Bounded model-checking extension of TaskProcessing. *) -(* *) -(* For model checking, both the sets of task identifiers and agent *) -(* identifiers must be finite and explicitly materialized. Since the *) -(* number of tasks is finite, the system may eventually reaches a state *) -(* where no new tasks can be staged, which leads to an artificial deadlock. *) -(* *) -(* To avoid this spurious deadlock, the next-state action is overridden to *) -(* include a dummy terminal state, allowing the model checker to complete *) -(* exploration gracefully. *) -(*****************************************************************************) - -EXTENDS FiniteSets, TaskProcessing - -ASSUME IsFiniteSet(TaskId) -ASSUME IsFiniteSet(AgentId) - --------------------------------------------------------------------------------- - -(** - * Dummy action representing the terminal state of the system, reached when - * there are no more tasks being processed (i.e., assigned to an agent or not - * yet finalized). - *) -Terminating == - /\ TaskId = UnknownTask \union StagedTask \union FinalizedTask - /\ UNCHANGED vars - -(** - * Modified next-state action. Extends the original system behavior with the - * Terminating action to avoid artificial deadlocks due to the bounded task set. - *) -MCNext == - \/ Next - \/ Terminating - -(** - * Modified full system specification. - *) -MCSpec == - /\ Init - /\ [][MCNext]_vars - /\ Fairness - -================================================================================ \ No newline at end of file