- // TODO: Get the semantics correct here
- // Certainement qu'il suffit de considérer les SemUnlock. ⋀ a priori,
- // il doit même suffir de considérer le cas où leur capacity après execution est <=1
- // ces cas disent qu'avant éxecution la capacity était de 0. Donc aucune chance de pouvoir
- // wait avant le unlock.
- return false;
+ // Reversible with everynbody but unlock which creates a free token
+ const auto e1_transition = E.get_transition_for_handle(e1);
+ if (e1_transition->type_ == Transition::Type::SEM_UNLOCK &&
+ static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() <= 1)
+ return false;
+ return true;