-/* Possible exploration status of a process in a state */
-enum class ProcessInterleaveState {
- no_interleave=0, /* Do not interleave (do not execute) */
- interleave, /* Interleave the process (one or more request) */
- more_interleave, /* Interleave twice the process (for mc_random simcall) */
- done /* Already interleaved */
-};
+/* On every state, each process has an entry of the following type.
+ * This represents both the process and its transition because
+ * a process cannot have more than one enabled transition at a given time.
+ */
+class ProcessState {
+ /* Possible exploration status of a process transition in a state.
+ * Either the checker did not consider the transition, or it was considered and to do, or considered and done.
+ */
+ enum class InterleavingType {
+ /** This process transition is not considered by the checker (yet?) */
+ disabled = 0,
+ /** The checker algorithm decided that this process transitions should be done at some point */
+ todo,
+ /** The checker algorithm decided that this should be done, but it was done in the meanwhile */
+ done,
+ };