- * @invariant: When a new event is created by UDPOR, it is inserted into
- * this set. All new events that are created by UDPOR have causes that
- * also exist in U and are valid for the duration of the search.
+ * @param C the current configuration from which UDPOR will be used
+ * to explore expansions of the concurrent system being modeled
+ * @param D the set of events that should not be considered by UDPOR
+ * while performing its searches, in order to avoid sleep-set blocked
+ * executions. See [1] for more details
+ * @param A the set of events to "guide" UDPOR in the correct direction
+ * when it returns back to a node in the unfolding and must decide among
+ * events to select from `ex(C)`. See [1] for more details