Use default when checking for invariants on cycle heads

[maul-esel]

The linter complains about cycleheads that do not have an invariant attribute. This warning occurs for us in many of Ultimate's termination witnesses.

This change relaxes that check to take into account the default value of the invariant key, i.e., if such a default is specified, no warning is issued.

[danieldietsch]

@MartinSpiessl can you have a quick look? Ultimate Automizer looses around 50 termination tasks because of this.

[MartinSpiessl]

Thanks, the code looks nice!

Just one thing, this is also a problem in the https://github.com/sosy-lab/sv-witnesses/blob/master/termination/README.md, isn't it?

The following sentence:

Thus, a node for which the cyclehead key is set, must also contain an invariant description.

Should probably be clarified by:

Thus, a node for which the cyclehead key is set to true, must also contain an invariant description.

Otherwise if I take the current form literally one could argue the linter is right, but this doesn't make sense of course, right? Could you also make that change to the termination format README.md (without the bold face, that was just for highlighting what I changed)? Then this will be merged and I will create a new archive MR for the linter against https://gitlab.com/sosy-lab/sv-comp/archives-2021.

[MartinSpiessl]

Oh, I see, the problem is actually the default value for the invariant key, not the default value for the cyclehead.

So my change request is actually a separate concern:
Even if I have a cyclehead set to false there needs to be an invariant? Sounds to me like we should actually make it clear that this is only the case if the cyclehead key is set to true.

@Eiram @danieldietsch @TBunk can you shed some light on this? I am not a termination expert so I really don't know what the right semantics should be here.

We can also just merge this right away and discuss that change in a separate issue/PR given the closeness to the deadline.
This PR even in the current form improves the linter, so I will merge it if you tell me to.

[danieldietsch]

Ultimate does not require cycleHead or invariant for termination witnesses. This was just an additional element CPAChecker introduced.

I just looked into the README and found this sentence from https://github.com/sosy-lab/sv-witnesses/blob/master/README.md#witnessing-program-termination

The extensions specified in the termination witness format required by CPAchecker will not lead to rejections, but are currently not used. Currently, Ultimate Automizer supports only violation witnesses.

Perhaps the linter should not validate cycleHead or invariant at all?

[danieldietsch]

I also think you should merge this PR and we can discuss the rulings separately.

[MartinSpiessl]

Perhaps the linter should not validate cycleHead or invariant at all?

Yeah, there is definitely more clarification needed. I would propose disabling the check via this PR now and creating a separate issue to discuss this further (after SV-COMP). Much like Michael Tautschnig did with the other PR: #29
@maul-esel can you comment out the cycleHead check similar to what @tautschnig did in his PR and reference issue #32 there?

Regarding the quote in #31 (comment), that is actually too short, the full paragraph reads:

Ultimate Automizer supports termination witnesses as specified by this document. No additional information is necessary. The extensions specified in the termination witness format required by CPAchecker will not lead to rejections, but are currently not used

So it is just about Ultimate's capabilities, and the claim is only that these keys will not lead to any rejection by Ultimate.

[maul-esel]

Done. I left the collection of default values and the invariant_present method unchanged, seeing as we will probably enable some form of the check in the future again.

[MartinSpiessl]

Done. I left the collection of default values and the invariant_present method unchanged, seeing as we will probably enable some form of the check in the future again.

Sounds very good! I will merge this now and create a new MR to the SV-COMP 2021 archives repository