[Analysis] use counter-example to refine black box components guarantees
- Open the attached project
- Open the component architecture
- Open the component named “Component”
- In the navigation tree, open “A/G, Contracts, Patterns”
- In the editor which just opened, click “Check selected”
- Observe that the specification is “FAIL”
- Observe that the Counterexample view opened on the right
- Observe that this counterexample involves the output of the subcomponent C (which should probably be equal to –1 in the counterexample)
Note: C is considered as a black box for verification in the model (which can be seen by clicking on it and observing the Properties section)
Now imagine the following situation: C should actually never output
–1.
Since it is unimplemented, AF3 cannot know it, but the user (we) know
it.
Now we would like to inform AF3 about this fact.
To do so, this issue is about adding the following:
- when the counterexample involves a blackbox component (in the example above: C) some GUI element (button, list, whatever — to be discussed) should give the user the option to refine this blackbox component in order to avoid these cases
- when selected by the user, the corresponding specification should be added as a contract to the component (in the example above: Output != –1)
Any improvements to the counterexample GUI are welcomed…
(from redmine: issue id 2165, created on 2014-11-25, closed on 2019-05-29)
- Relations:
- relates #2141 (closed)
- relates #2128
- Uploads: