rework OCRA refinement
At present the verification using OCRA contracts works as follows:
- For the atomic components the property is tested against the behaviour
- for the composite components the property is tested for the refinement. The user in this case has to provide the list of refining contracts and the tool tries to prove the property using these contracts
This causes usability issues as the suer needs to define a lot of contracts, and also the contracts at lower levels mimic the behaviour.
For the tutorial and in the future we want to give an option to the user such that contracts at composite components can also be verified against the behaviour.
My approach to this issue is: if no refining contract is specified then verify the specification against the behaviour otherwise use the refinement.
(from redmine: issue id 3509, created on 2018-09-10)