Feature #6702
openGenerate restricted environment model
0%
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.
Updated by Ilja Zakharov about 8 years ago
- 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.
Updated by Evgeny Novikov about 8 years ago
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.
Updated by Ilja Zakharov about 8 years ago
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.
Updated by Evgeny Novikov over 4 years ago
- Related to Feature #6703: Generate several environment models per abstract verification task added