Model checking clean components of a not-clean model
Many subcomponents could be modelchecked even if the model uses unclean features.
#2 Updated by Anonymous over 2 years ago
- Assignee changed from Anonymous to Anonymous
I think the wording "clean" just means "containing features which are not formal verification compatible".
This was probably resulting of the situation back then: people were trying to model check some components and were often getting "the model uses a non-compatible fragment".
If it is still the case today that the verification fails because of this, I'd say the issue is still relevant.
Otherwise we can reject.