Modify copy mechanism of unused properties in configuration builder

[MartinSpiessl]

Currently, when we have something like the following:

Configuration newConfig = configBuilder.copyFrom(oldConfig).build();

the newConfig and the oldConfig share the same set of unusedProperties.

This has the downside that newConfig might add options that are not in the oldConfig. These are then nowhere marked as unused, despite the fact that this information is relevant for users.

This PR will address this by keeping the sets of unusedProperties separate and updating the set in oldConfig when the option is used in the newConfig.
The unusedProperties of newConfig are set to only contain properties that are only present in newConfig, not oldConfig. This has the advantage that unused properties are not reported redundantly.

I introduced a reference to the parent configuration inside the new configuration, this effectively leads to a tree-like structure where unused property tracking will work correctly across all levels.

The motivation behind this PR is to allow to check for unused options in subconfigs (c.f. CPAchecker issue #545). It should be backwards compatible as far as the effect on oldConfig is concerned.

I have not yet added unit tests that test the new functionality, I will add them if there are no objections against this PR in general.

[PhilippWendler]

In general, we do want this, of course. Feel free to add more unit tests for the whole functionality of detecting unused options, there is currently only one.

Currently this code does not work transitively for chains of >= 3 configuration instances, correct?

If a field Configuration parent is added, it should be final. However, I am not sure whether we should have such a field. Would the code be more complicated if only a reference to the parent's set is kept? Would proper transitive handling of unused options still be possible?

It is probably nice for code understandability if Configuration instances can stand alone. Furthermore, just today I had the idea of #26, which would also introduce a reference to some kind of "parent config", but with different semantics. But if a parent field is necessary, it is not unacceptable.

[MartinSpiessl]

Thanks for the input!

Currently this code does not work transitively for chains of >= 3 configuration instances, correct?

I thought it would, but I can just write a test to see who is right.

However, I am not sure whether we should have such a field

Me neither.

Would the code be more complicated if only a reference to the parent's set is kept?

Not at all, I thought it was nicer to have the relation via a parent object instead of just the sets.
In the end, what difference does it really make?

Would proper transitive handling of unused options still be possible?

Sure, currently, the only thing I need the reference to the parent for is for getting the set of unused properties. And of course once in the constructor, I need the actual set of properties. But after construction, there is no need to keep that.
I will rewrite it that way, then we will see how it turns out

It is probably nice for code understandability if Configuration instances can stand alone

Do you mean that we should try to avoid accessing the parents set of unused properties? This would lead to options marked as unused in the parent config that are used in the child config, I do not see a way to make both work at the same time.

Furthermore, just today I had the idea of #26, which would also introduce a reference to some kind of "parent config", but with different semantics.

I looked into it and posted some questions I had. It is kind of hard to wrap my head around all the implications and possibilities of the configuration system.

[PhilippWendler]

It is probably nice for code understandability if Configuration instances can stand alone

Do you mean that we should try to avoid accessing the parents set of unused properties?

No, that's fine. My slight tendency against a parent field comes from the fact that if there is such a field, you need to look at the whole class to see in which circumstances it is used. If there is only a specific reference to a set with unused properties and no general parent reference, it is clear that the parent has no effect on anything else than unused properties.

[PhilippWendler]

Will this be continued or shall we close it?

[PhilippWendler]

@MartinSpiessl ping?