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