DeepSec-prover / deepsec

DEciding Equivalence Properties in SECurity protocols
GNU General Public License v3.0
17 stars 2 forks source link

Check QBC examples #57

Closed VincentCheval closed 4 years ago

VincentCheval commented 4 years ago

Between 1.02 and v2.0.0-beta, there is an important difference between computation time of QBC examples for session equivalence.

We need to check whether it was a bug in 1.02 that would make it faster or if it is a bug in v2.0.0-beta that makes it slower. Mostly, QBC files are currently the only examples that are really slower on v2.0.0-beta compare to 1.02

VincentCheval commented 4 years ago

A bug was found in v2.0.0-beta that would slow down the computation. A bug was also found in v1.02 which would speed up incorrectly the computation. The latter bug did not impact v2.0.0-beta.

The bug in v2.0.0-beta was fix in bd8f43b