Merge pull request #212 from mldiego/master

Misc. error fixes
verivital · Mar 20, 2024 · 0687ce4 · 0687ce4
2 parents dbe8633 + 2521f2a
commit 0687ce4
Show file tree

Hide file tree

Showing 67 changed files with 94,498 additions and 1,420 deletions.
diff --git a/code/nnv/engine/nn/NN.m b/code/nnv/engine/nn/NN.m
@@ -952,7 +952,7 @@
         function inputSet = consistentPrecision(obj, inputSet)
             % (assume parameters have same precision across layers)
             % approach: change input precision based on network parameters
-            inputPrecision = class(inputSet.V);
+            inputPrecision = class(inputSet(1).V);
             netPrecision = 'double'; % default
             for i=1:length(obj.Layers)
                 if isa(obj.Layers{i}, "FullyConnectedLayer") || isa(obj.Layers{i}, "Conv2DLayer")
@@ -963,7 +963,9 @@
             if ~strcmp(inputPrecision, netPrecision)
                 % input and parameter precision does not match
                 warning("Changing input set precision to "+string(netPrecision));
-                inputSet = inputSet.changeVarsPrecision(netPrecision);
+                for i = 1:length(inputSet)
+                    inputSet(i) = inputSet(i).changeVarsPrecision(netPrecision);
+                end
             end
         end
 

diff --git a/code/nnv/engine/set/Star.m b/code/nnv/engine/set/Star.m
@@ -813,7 +813,7 @@
                 if ismember(exitflag, ["l1","g5"])
                     xmax = -fval + obj.V(index, 1);
                 else
-                    error('Cannot find an optimal solution, exitflag = %d', exitflag);
+                    error('Cannot find an optimal solution, exitflag = %s', exitflag);
                 end      
             end
 
@@ -1166,9 +1166,21 @@
             if obj.dim ~= S.dim
                 error('Two sets have different dimension');
             end
+
+            if isa(obj.V, 'single') || isa(obj.C,'single') || isa(obj.d, 'single')
+                S1 = obj.changeVarsPrecision('double');
+            else
+                S1 = obj;
+            end
+
+            if isa(S.V, 'single') || isa(S.C,'single') || isa(S.d, 'single')
+                S2 = S.changeVarsPrecision('double');
+            else
+                S2 = S;
+            end
 
-            P1 = obj.toPolyhedron();
-            P2 = S.toPolyhedron();
+            P1 = S1.toPolyhedron();
+            P2 = S2.toPolyhedron();
 
             bool = (P1 <= P2);
 

diff --git a/code/nnv/engine/utils/matlab2nnv.m b/code/nnv/engine/utils/matlab2nnv.m
@@ -44,7 +44,7 @@
     % Layers with no effect on the reachability analysis
     if isa(L, 'nnet.cnn.layer.DropoutLayer') || isa(L, 'nnet.cnn.layer.SoftmaxLayer') || isa(L, 'nnet.cnn.layer.ClassificationOutputLayer') ...
             || isa(L,"nnet.onnx.layer.VerifyBatchSizeLayer") || isa(L, "nnet.cnn.layer.RegressionOutputLayer") ...
-            || customLayer_no_NLP == 1 || isa(L, "nnet.onnx.layer.CustomOutputLayer")
+            || customLayer_no_NLP == 1 || isa(L, "nnet.onnx.layer.CustomOutputLayer") || contains(class(L), "LogSoftmax")
         Li = PlaceholderLayer.parse(L);
 
     elseif customLayer_no_NLP

diff --git a/code/nnv/examples/NN/medmnist/debugInconsistenciesNodulemnist.m b/code/nnv/examples/NN/medmnist/debugInconsistenciesNodulemnist.m
diff --git a/code/nnv/examples/NN/medmnist/generate_vnnlib_files.m b/code/nnv/examples/NN/medmnist/generate_vnnlib_files.m
@@ -3,8 +3,9 @@
 %% All 2D datasets
 
 datapath = "data/mat_files/";
-datafiles = ["bloodmnist"; "breastmnist.mat"; "dermamnist.mat"; "octmnist.mat"; "organamnist.mat"; ...
-    "organcmnist.mat"; "organsmnist.mat"; "pathmnist.mat"; "pneumoniamnist"; "retinamnist.mat"; "tissuemnist.mat"];
+% datafiles = ["bloodmnist"; "breastmnist.mat"; "dermamnist.mat"; "octmnist.mat"; "organamnist.mat"; ...
+%     "organcmnist.mat"; "organsmnist.mat"; "pathmnist.mat"; "pneumoniamnist.mat"; "retinamnist.mat"; "tissuemnist.mat"];
+datafiles = "pneumoniamnist.mat";
 
 N = 10; % number of vnnlib files to create
 epsilon = [1,2,3]; % {epsilon} pixel color values for every channel