Feature #6702
open
Generate restricted environment model
Added by Ilja Zakharov over 8 years ago.
Updated about 8 years ago.
Category:
Environment models
Description
To simplify an environment model code for huge drivers it is possible to generate environment model with restricted number of processes. Such model can be simpler but less correct and complete.
Related issues
1 (1 open — 0 closed)
- Tracker changed from Bug to Feature
- Priority changed from Normal to High
- Priority changed from High to Low
Currently we can try for huge modules environment model with label-based automata with nested registration. This reduces completeness of an environment model but does not influence correctness which is much better than reducing them both. Referred type of an environment model is implemented and is available from master.
I didn't catch whether the problem exists still. Is the suggested approach really work or it is just your assumptions? If it can help, why it isn't enabled by default and this issue isn't closed? Besides, please, describe how the given feature and things made around it is connected with #7110.
Restricted model is not implemented as it is described in the ticket but there is another implemented feature which should help. I described it in my comment above. By the way this option just may help to check huge drivers reducing completeness of an environment model, so there is no reason to turn it on by default. And I have not performed many experiments to prove results and close the issue or increase its priority.
The feature is not connected with #7110.
- Related to Feature #6703: Generate several environment models per abstract verification task added
Also available in: Atom
PDF