Project

General

Profile

Feature #1762

Model checking clean components of a not-clean model

Added by Anonymous about 7 years ago. Updated over 1 year ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
09/29/2013
Due date:
% Done:

0%

Estimated time:

Description

Many subcomponents could be modelchecked even if the model uses unclean features.

History

#1 Updated by Anonymous over 2 years ago

  • Assignee set to Anonymous

I would say this should be rejected as we do not have the notion of clean/unclean now.

What is your opinion?

#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.

#3 Updated by Anonymous over 2 years ago

  • Target version set to AF3 2.14 RC1 (Feature Freeze)

#4 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.14 RC1 (Feature Freeze) to Backlog

Also available in: Atom PDF