+/* 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 */
+struct ProcessState {
+ /** Exploration control information */
+ ProcessInterleaveState state = ProcessInterleaveState::no_interleave;
+ /** Number of times that the process was interleaved */
+ unsigned int interleave_count;
+
+ bool done() const
+ {
+ return this->state == ProcessInterleaveState::done;
+ }
+ bool interleave() const {
+ return this->state == ProcessInterleaveState::interleave
+ || this->state == ProcessInterleaveState::more_interleave;
+ }
+};
+