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

Check all three properties by default #675

Merged
merged 5 commits into from
May 15, 2024
Merged

Conversation

hernanponcedeleon
Copy link
Owner

No description provided.

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Copy link
Collaborator

@ThomasHaas ThomasHaas left a comment

Choose a reason for hiding this comment

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

LGTM

EDIT: As you probably noticed, some unit tests used the default properties and now they fail. This also shows a problem in regards to litmus code assertions: it is not guaranteed that you can even check all three properties at the same time!
Only for C-code you know that all properties are of the same type.

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
@hernanponcedeleon
Copy link
Owner Author

This also shows a problem in regards to litmus code assertions: it is not guaranteed that you can even check all three properties at the same time! Only for C-code you know that all properties are of the same type.

You are right, but we don't have any real user checking litmus tests. I still think we should use all 3 properties as default and maybe just improve the error msg (i.e., tell the user what to do) when mixed type properties are used

The set of properties [Program specification, Liveness, CAT specification] are of mixed type (safety and reachability properties). Cannot encode mixed properties into a single SMT-query.

->

The set of properties [Program specification, Liveness, CAT specification] are of mixed type (safety and reachability properties). Cannot encode mixed properties into a single SMT-query. Please select a different set of properties.

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
@ThomasHaas
Copy link
Collaborator

Fine with me

@hernanponcedeleon hernanponcedeleon merged commit 356c711 into development May 15, 2024
1 check passed
@hernanponcedeleon hernanponcedeleon deleted the property branch May 15, 2024 09:15
tonghaining pushed a commit to tonghaining/Dat3M that referenced this pull request May 24, 2024
…ernanponcedeleon#675)

* Check all three properties by default

* Force thread creation to succeed by default

* Improve error msg for mixed type properties

---------

Signed-off-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Co-authored-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants