Some minor modifications to reachOptions

mldiego · Jul 13, 2024 · 95fea61 · 95fea61
1 parent 58a0d35
commit 95fea61
Showing 1 changed file with 19 additions and 9 deletions.
diff --git a/code/nnv/examples/Submission/VNN_COMP2024/run_vnncomp2024_instance.m b/code/nnv/examples/Submission/VNN_COMP2024/run_vnncomp2024_instance.m
@@ -58,7 +58,7 @@
     warning("Working on adding support to other vnnlib properties");
 end
 
-cEX_time = toc(t)
+cEX_time = toc(t);
 
 %% 3) UNSAT?
 
@@ -470,7 +470,7 @@
         needReshape = 1;
         reachOptions = struct;
         reachOptions.reachMethod = 'relax-star-area';
-        reachOptions.relaxFactor = 0.9;
+        reachOptions.relaxFactor = 1;
         reachOptionsList{1} = reachOptions;
         reachOptions.reachMethod = 'relax-star-area';
         reachOptions.relaxFactor = 0.5;
@@ -513,13 +513,23 @@
         % cora benchmark: onnx 2 nnv
         net = importNetworkFromONNX(onnx, "InputDataFormats","BC", "OutputDataFormats","BC");
         nnvnet = matlab2nnv(net);
-        reachOptions = struct;
-        reachOptions.reachMethod = 'relax-star-area';
-        reachOptions.relaxFactor = 0.5;
-        reachOptionsList{1} = reachOptions;
-        reachOptions = struct;
-        reachOptions.reachMethod = 'approx-star'; % default parameters
-        reachOptionsList{2} = reachOptions;
+        if contains(onnx, '-set')
+            reachOptions = struct;
+            reachOptions.reachMethod = 'relax-star-area';
+            reachOptions.relaxFactor = 0.5;
+            reachOptionsList{1} = reachOptions;
+            reachOptions = struct;
+            reachOptions.reachMethod = 'approx-star'; % default parameters
+            reachOptionsList{2} = reachOptions;
+        else
+            reachOptions = struct;
+            reachOptions.reachMethod = 'relax-star-area';
+            reachOptions.relaxFactor = 0.9;
+            reachOptionsList{1} = reachOptions;
+            reachOptions.reachMethod = 'relax-star-area';
+            reachOptions.relaxFactor = 0.7;
+            reachOptionsList{1} = reachOptions;
+        end
 
     elseif contains(category, "lsnc")
         % lyapunov benchmark: onnx to nnv (barely, some IR and opset version differences)