search

hernanponcedeleon / Dat3M

A verification tool for many memory models
MIT License
77 stars 30 forks source link

Illegal default configuration #717

Closed natgavrilenko closed 3 months ago

natgavrilenko commented 3 months ago

Dartagnan configuration has been changed to verify all three properties by default. This brings two problems:

  1. Depending on the type of assertion (in a litmus test), the default configuration (with all three properties) can be illegal.
  2. Such tests cannot be executed in the UI, because there is no input to select a verification property.

Possible solutions for conflicting properties:

Also, an input for verification property (and possibly other configuration) should be added to the UI.

The issue has been introduced by: https://github.com/hernanponcedeleon/Dat3M/commit/356c71140881c5912c5baa4d0264fe5b79587657

ThomasHaas commented 3 months ago

Are you running an outdated UI? I added quite a few extra options a while ago (#684), including the possiblity to select the verification property (but no combinations thereof).

natgavrilenko commented 3 months ago

Yes, it was an old branch. UI works fine in the latest version, sorry. Default verification property for litmus tests is still a problem.

hernanponcedeleon commented 3 months ago

Fixed by 48d880d4a8c524f1275c003a4e2a305f1d0dcbc7