Implemented feedback

dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java

@@ -118,8 +118,6 @@ public static void main(String[] args) throws Exception {
                 .orElseThrow(() -> new IllegalArgumentException("CAT model not given or format not recognized")));
         logger.info("CAT file path: " + fileModel);
 
-        logger.info("Progress model: " + o.getProgressModel());
-
         Wmm mcm = new ParserCat().parse(fileModel);
         Program p = new ProgramParser().parse(fileProgram);
         EnumSet<Property> properties = o.getProperty();

dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java

@@ -8,14 +8,14 @@ public class OptionNames {
     public static final String TARGET = "target";
     public static final String METHOD = "method";
     public static final String SOLVER = "solver";
-    public static final String PROGRESSMODEL = "progressModel";
     public static final String TIMEOUT = "timeout";
     public static final String VALIDATE = "validate";
     public static final String COVERAGE = "coverage";
     public static final String WITNESS = "witness";
     public static final String SMTLIB2 = "smtlib2";
 
     // Modeling Options
+    public static final String PROGRESSMODEL = "modeling.progress";
     public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds";
     public static final String RECURSION_BOUND = "modeling.recursionBound";
     public static final String MEMORY_IS_ZEROED = "modeling.memoryIsZeroed";

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java

@@ -133,10 +133,8 @@ private BooleanFormula threadHasStarted(Thread thread) {
     private BooleanFormula threadHasTerminated(Thread thread) {
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
         return bmgr.and(
-                context.execution(thread.getExit()),
+                context.execution(thread.getExit()), // Also guarantees that we are not stuck in a barrier
                 bmgr.not(threadIsStuckInLoop(thread))
-                // The following is not needed since the first condition already implies this
-                // bmgr.not(threadIsStuckInBarrier(thread))
         );
     }
 
@@ -445,8 +443,7 @@ private BooleanFormula encodeFairForwardProgress(Thread thread) {
 
             // For every event in the cf a successor will be in the cf (unless a barrier is blocking).
             for (Event cur : thread.getEvents()) {
-                if (cur.getSuccessor() == null) {
-                    assert cur == thread.getExit();
+                if (cur == thread.getExit()) {
                     break;
                 }
                 final List<Event> succs = new ArrayList<>();

dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java

@@ -16,71 +16,95 @@
 public abstract class BaseOptions {
 
     @Option(
-        name=PROPERTY,
-        description="The property to check for: reachability (default), liveness, races.",
-        toUppercase=true)
+            name = PROPERTY,
+            description = "A combination of properties to check for: program_spec, liveness, cat_spec (defaults to all).",
+            toUppercase = true)
     private EnumSet<Property> property = Property.getDefault();
 
-    public EnumSet<Property> getProperty() { return property; }
+    public EnumSet<Property> getProperty() {
+        return property;
+    }
 
     @Option(
-            name=PROGRESSMODEL,
-            description="The progress model to assume: fair (default), HSA, OBE, unfair",
-            toUppercase=true)
+            name = PROGRESSMODEL,
+            description = "The progress model to assume: fair (default), hsa, obe, unfair",
+            toUppercase = true)
     private ProgressModel progressModel = ProgressModel.getDefault();
 
-    public ProgressModel getProgressModel() { return progressModel; }
+    public ProgressModel getProgressModel() {
+        return progressModel;
+    }
 
     @Option(
-        name=VALIDATE,
-        description="Performs violation witness validation. Argument is the path to the witness file.")
+            name = VALIDATE,
+            description = "Performs violation witness validation. Argument is the path to the witness file.")
     private String witnessPath;
 
-    public boolean runValidator() { return witnessPath != null; }
-    public String getWitnessPath() { return witnessPath; }
+    public boolean runValidator() {
+        return witnessPath != null;
+    }
+
+    public String getWitnessPath() {
+        return witnessPath;
+    }
 
     @Option(
-        name=METHOD,
-        description="Solver method to be used.",
-        toUppercase=true)
-    private Method method=Method.getDefault();
+            name = METHOD,
+            description = "Solver method to be used.",
+            toUppercase = true)
+    private Method method = Method.getDefault();
 
-    public Method getMethod() { return method; }
+    public Method getMethod() {
+        return method;
+    }
 
     @Option(
-        name=SOLVER,
-        description="Uses the specified SMT solver as a backend.",
-        toUppercase=true)
-    private Solvers solver=Solvers.Z3;
+            name = SOLVER,
+            description = "Uses the specified SMT solver as a backend.",
+            toUppercase = true)
+    private Solvers solver = Solvers.Z3;
 
-    public Solvers getSolver() { return solver; }
+    public Solvers getSolver() {
+        return solver;
+    }
 
     @Option(
-        name=TIMEOUT,
-        description="Timeout (in secs) before interrupting the SMT solver.")
-    private int timeout=0;
+            name = TIMEOUT,
+            description = "Timeout (in secs) before interrupting the SMT solver.")
+    private int timeout = 0;
+
+    public boolean hasTimeout() {
+        return timeout > 0;
+    }
 
-    public boolean hasTimeout() { return timeout > 0; }
-    public int getTimeout() { return timeout; }
+    public int getTimeout() {
+        return timeout;
+    }
 
     @Option(
-        name=PHANTOM_REFERENCES,
-        description="Decrease references on Z3 formula objects once they are no longer referenced.")
-    private boolean phantomReferences=true;
+            name = PHANTOM_REFERENCES,
+            description = "Decrease references on Z3 formula objects once they are no longer referenced.")
+    private boolean phantomReferences = true;
 
-    public boolean usePhantomReferences() { return phantomReferences; }
+    public boolean usePhantomReferences() {
+        return phantomReferences;
+    }
 
     @Option(
-        name=WITNESS,
-        description="Type of the violation graph to generate in the output directory.")
-    private WitnessType witnessType=WitnessType.getDefault();
+            name = WITNESS,
+            description = "Type of the violation graph to generate in the output directory.")
+    private WitnessType witnessType = WitnessType.getDefault();
 
-    public WitnessType getWitnessType() { return witnessType; }
+    public WitnessType getWitnessType() {
+        return witnessType;
+    }
 
     @Option(
-        name=SMTLIB2,
-        description="Dump encoding to an SMTLIB2 file.")
-    private boolean smtlib=false;
+            name = SMTLIB2,
+            description = "Dump encoding to an SMTLIB2 file.")
+    private boolean smtlib = false;
 
-    public boolean getDumpSmtLib() { return smtlib; }
+    public boolean getDumpSmtLib() {
+        return smtlib;
+    }
 }

dartagnan/src/main/java/com/dat3m/dartagnan/verification/VerificationTask.java

@@ -34,7 +34,7 @@ protected VerificationTask(Program program, Wmm memoryModel, ProgressModel progr
     throws InvalidConfigurationException {
         this.program = checkNotNull(program);
         this.memoryModel = checkNotNull(memoryModel);
-        this.progressModel = progressModel;
+        this.progressModel = checkNotNull(progressModel);
         this.property = checkNotNull(property);
         this.witness = checkNotNull(witness);
         this.config = checkNotNull(config);