non deterministic bug with distribution

DeepSec-prover / deepsec

DEciding Equivalence Properties in SECurity protocols

GNU General Public License v3.0

17 stars 2 forks source link

non deterministic bug with distribution #81

Open irakoton opened 4 years ago

irakoton commented 4 years ago

The following file contains non-equivalent processes. Sometimes the analysis is conclusive, sometimes it is interrupted by the internal error before starting the analysis:

Internal Error: [distributed_equibalence.ml >> convert_trace_to_original_symbols] The recipe should be ground.

The bug is not always easy to reproduce (and minimising the bugged example is hard as well) as the bug sometimes randomly disappears for a few minuts.

bug.txt

irakoton commented 3 years ago

NB. I confirm that the bug seems to be caused by parallelisation (does not appear with option -d false)