Feature #6570
closedIterate over dictionaries deterministically in EMG
0%
Description
All loops over dictionaries should be rewritten to guarantee deterministical generation of an environment model code, since default Python "for" loops do that differently from time to time.
Updated by Evgeny Novikov over 8 years ago
Consider using standard collections.OrderedDict for this.
Updated by Evgeny Novikov about 8 years ago
BTW this nondeterminism leads to we can't use our simple error trace comparison algorithms since function names vary from time to time.
Updated by Evgeny Novikov about 8 years ago
- Priority changed from High to Normal
#6814 suggests the much more universal approach than deterministic names of functions from environment models.
Updated by Vadim Mutilin about 8 years ago
- Priority changed from Normal to High
nondetermism in generated EMG models leads to nondeterministics of results produced by verification tools, thus this bug is still important to fix
Updated by Evgeny Novikov about 8 years ago
- Priority changed from High to Urgent
For at least 3 modules from the validation set CPAchecker can consume several times more resources and even fails with time outs instead of finding target bugs likely due to non-determinism in generated environment models. Without deterministic behaviour even at that level we can not perform reliable experiments.
Updated by Ilja Zakharov about 8 years ago
- Status changed from New to Resolved
- Priority changed from Urgent to High
The problem is solved and corresponding code merged to master.
Aspect files generated by EMG and corresponding cil files should be equivalent now. If you encounter any problems with non-determinism caused by EMG it is preferable to open a new issue with details about your task provided.
Updated by Evgeny Novikov about 8 years ago
- Status changed from Resolved to Closed