Add support for new property check for requirements called State-Recoverability

[Tob1as864]

Adding a new property check to UltimatePA after consultation with Vincent.

[bahnwaerter]

Thanks @Tob1as864 for your great work.

Although I'm not a requirement analysis expert, I reviewed your code. I marked problematic code locations with some short explanations for you. Hopefully they can help you to resolve the mentioned issues. If not, feel free to ask!

Note: if you use Eclipse, you can get rid of code formatting problems very quickly. Eclipse supports automatic code formatting. If you want to use it, we recommend to use this code formatter template to avoid reformatting all the code in a different style. For setting up the formatter, go to Window → Preferences → Java → Code Style → Formatter, click Import, and choose the file. You can then format the currently opened source file through Source → Format or by using the shortcut key Ctrl+Shift+F.

[Tob1as864]

Thanks @Tob1as864 for your great work.

Although I'm not a requirement analysis expert, I reviewed your code. I marked problematic code locations with some short explanations for you. Hopefully they can help you to resolve the mentioned issues. If not, feel free to ask!

Note: if you use Eclipse, you can get rid of code formatting problems very quickly. Eclipse supports automatic code formatting. If you want to use it, we recommend to use this code formatter template to avoid reformatting all the code in a different style. For setting up the formatter, go to Window → Preferences → Java → Code Style → Formatter, click Import, and choose the file. You can then format the currently opened source file through Source → Format or by using the shortcut key Ctrl+Shift+F.

Thanks for the hint with the template. I have imported and used it immediately. The problematic code locations should be resolved right now.

[bahnwaerter]

Now the code files look clean and are ready for a review by the requirement experts @danieldietsch, @Langenfeld, and @hauff. Let's see what they say about the implementation of checking the new property and the code structure.

[danieldietsch]

I did not review the algorithm, but before I continue you should fix
coding conventions (variable, class names, spacing, modifiers, license headers, comments for interfaces, author comments, etc.) and the comments I already added.

You should also add a description to the PR that states what this is all about, as it is a rather large change and hence, it might be somewhat confusing to review it without knowing what the purpose is.

[danieldietsch]

@Tob1as864 I need a little bit of context before I can review this PR. In particular, I need to know what kind of property you want to check.

[Tob1as864]

@Tob1as864 I need a little bit of context before I can review this PR. In particular, I need to know what kind of property you want to check.

State-Recoverability describes a property that applies if specific condition is recoverable for each interpretation of the requirements specification.
For example if we have requirements specification with one requirement (Just as a very simple example):

• Req1: After "sig_1", it is never the case that "sig_2" holds

and we ask if the condition sig_2 is true is recoverable for the specification, then the property shall that for this specification the property does not apply.

Another example is this parallel composition of a more complex set of requirements where as soon as a certain location is entered certain states are no longer possible (VEH_ELEC_SYS_SEPARATED == true).

[danieldietsch]

@Tob1as864 @Langenfeld is this PR still relevant?

[Langenfeld]

@danieldietsch the property in the wip/ad/stuck-at branch should be a generalisation of this branch. But as with so many hunches regarding requirements properties, I have to take a serious look if I did not overlook something.
Shall say: thanks for reminding me. As the mentioned branch should be pull requested soon, there should come clarity about this one. But most likely this one is dropped.

[danieldietsch]

@Langenfeld we can keep it around nearly indefinitely ;)