Currently, we do not try to detect if the processes of session equivalences are determinate.
If they are determinate then run the determinate algorithm since it is equivalent to trace equivalence.
Maybe display a message indicating that the two equivalences would coincide ?
Even if they are not determinate, we should implement the management of improper block (one unique Exist for one Forall + unique label in permutation). That would speedup the procedure quite a lot for processes that are "almost" determinate.
Currently, we do not try to detect if the processes of session equivalences are determinate.