Intruiging performances of equivalence by session

[irakoton]

Here is a file where equivalence by session is significantly faster than the analogue verification query for determinate processes. The file models a sequence

P; P; ...; P

where the sequence is modelled by a form of token passing without private channels, but with a private function symbol (more detailed explanations in the file).

session_faster.txt

[VincentCheval]

I don't explain yet the difference of time but there is a bug for sure (caught when doing a make debug)

Internal Error: [data_structure.ml >> IK.transfer_incremented_knowledge_into_knowledge] Incorrect index counter

[VincentCheval]

I solved the bug from "make debug" but I still don't understand the difference of speed. The partition tree in determinate is somehow 10 times bigger than in session equivalence (1M nodes vs 130K nodes).

I leave the issue open but I'm changing the tag.