Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 24 commits into
base: dev
Choose a base branch
from

Conversation

Tob1as864
Copy link

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

Copy link
Member

@bahnwaerter bahnwaerter left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 WindowPreferencesJavaCode StyleFormatter, click Import, and choose the file. You can then format the currently opened source file through SourceFormat or by using the shortcut key Ctrl+Shift+F.

@bahnwaerter bahnwaerter requested a review from hauff August 15, 2023 17:42
Tob1as864 and others added 11 commits August 15, 2023 20:21
…tik/ultimate/core/model/preferences/UltimatePreferenceItem.java

Co-authored-by: Manuel Bentele <[email protected]>
…te/pea2boogie/generator/RtInconcistencyConditionGenerator.java

Co-authored-by: Manuel Bentele <[email protected]>
…te/pea2boogie/preferences/Pea2BoogiePreferences.java

Co-authored-by: Manuel Bentele <[email protected]>
…te/pea2boogie/req2pea/ReqCheckAnnotator.java

Co-authored-by: Manuel Bentele <[email protected]>
…te/pea2boogie/req2pea/ReqCheckAnnotator.java

Co-authored-by: Manuel Bentele <[email protected]>
…te/pea2boogie/staterecoverability/AuxStatement.java

Co-authored-by: Manuel Bentele <[email protected]>
…te/pea2boogie/translator/Req2BoogieTranslator.java

Co-authored-by: Manuel Bentele <[email protected]>
…te/pea2boogie/translator/Req2BoogieTranslator.java

Co-authored-by: Manuel Bentele <[email protected]>
@Tob1as864
Copy link
Author

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 WindowPreferencesJavaCode StyleFormatter, click Import, and choose the file. You can then format the currently opened source file through SourceFormat 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.

Copy link
Member

@bahnwaerter bahnwaerter left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

@danieldietsch danieldietsch left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Member

@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
Copy link
Author

@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).
grafik

@danieldietsch
Copy link
Member

@Tob1as864 @Langenfeld is this PR still relevant?

@Langenfeld
Copy link
Member

Langenfeld commented Aug 22, 2024

@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
Copy link
Member

@Langenfeld we can keep it around nearly indefinitely ;)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants