Merge pull request #209 from mldiego/master

Segmentation for medical image
verivital · Feb 6, 2024 · ed13108 · ed13108
2 parents 3c18a62 + 3c5f509
commit ed13108
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 17 deletions.
diff --git a/code/nnv/engine/nn/funcs/TanSig.m b/code/nnv/engine/nn/funcs/TanSig.m
@@ -1210,17 +1210,15 @@
 
         end
 
-
-
         function S = reach_absdom_approx(varargin)
-        % @I: star input set
-        % @Z: Star output set
-
-        % author: Dung Tran
-        % date: 3/27/2020
-
-        % reference: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages,
-        % Gagandeep Singh, POPL, 2019
+            % @I: star input set
+            % @Z: Star output set
+    
+            % author: Dung Tran
+            % date: 3/27/2020
+    
+            % reference: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages,
+            % Gagandeep Singh, POPL, 2019
 
             switch nargin
                 case 1
@@ -1261,7 +1259,7 @@
                 S = TanSig.stepTanSig_absdom(S, i, l(i), u(i), y_l(i), y_u(i), dy_l(i), dy_u(i)); 
             end
 
-            end
+        end
 
         % dealing with multiple inputs in parallel
         function S = reach_absdom_approx_multipleInputs(varargin)
@@ -1299,7 +1297,6 @@
 
         end
 
-
     end
 
 methods(Static) % over-approximate reachability analysis using abstract-domain (absdom) based on eran
@@ -1475,6 +1472,7 @@
             end
         end
     end
+
 end
 
 
@@ -1697,9 +1695,11 @@
             end
         end
     end
+
 end
 
 methods(Static) % over-approximate reachability analysis using RStar0
+
     % step over-approximate reachability analysis using relaxed star with
     % zero constraints (RStar0)
     function R = stepTanSig_rstar_zero_constraints(I, index, l, u, y_l, y_u, dy_l, dy_u)
@@ -1819,6 +1819,7 @@
             end
         end
     end
+
 end
 
 
@@ -1909,6 +1910,10 @@
 
             R = TanSig.reach_relaxed_star_zero_constraints_approx(I);
 
+        elseif contains(method, 'relax-star')
+
+            R = I; % just return input (for specific example that I DM is working on this works. Please, fix after that!!
+
         else
             error('Unknown or unsupported reachability method for layer with TanSig activation function');
         end

diff --git a/code/nnv/engine/set/ImageStar.m b/code/nnv/engine/set/ImageStar.m
@@ -441,7 +441,11 @@
             end
 
             if ~isempty(scale) && (isvector(scale) || isscalar(scale))
-                new_V = scale.*obj.V;
+                try
+                    new_V = scale.*obj.V;
+                catch
+                    new_V = pagemtimes(scale,obj.V);
+                end
             elseif ~isempty(scale) && ismatrix(scale)
                 new_V = pagemtimes(scale,obj.V);
             else
@@ -490,8 +494,8 @@
             reshapedImage = ImageStar(V1,in_star.C, in_star.d, in_star.predicate_lb, in_star.predicate_ub);
         end
 
-        % reshape an Imagestar with the target dimesion
-        function upsamplededImage = upsample(obj, scaleDim)
+        % upsample imagestar for specific dimension
+        function reshapedImage = upsample(obj, scaleDim)
             if length(scaleDim) == 4
                 scaleDim = [scaleDim(4), scaleDim(3), 1];
             elseif length(scaleDim) == 3

diff --git a/code/nnv/engine/utils/export2vnnlib.m b/code/nnv/engine/utils/export2vnnlib.m
@@ -72,7 +72,7 @@ function export2vnnlib(lb, ub, outsize, property, name)
     nO = length(property.g); % number of output constraints
     for i=1:nO
         constraint = halfspaceConstraint2inequality_1(property.G(i,:), property.g(i));
-        fprintf(fID,"(assert "+constraint);
+        fprintf(fID,"(assert "+constraint+" \n");
     end
 end
 
@@ -116,7 +116,11 @@ function export2vnnlib(lb, ub, outsize, property, name)
             str = "(>= Y_"+string(locs(1)-1) + " " + "Y_"+string(locs(2)-1) + "))";
         end
     else % compare index to value
-        str = "(>= Y_"+string(locs(1)-1) + " " + num2str(hVal, '%.16f') + "))";
+        if hRow(locs) > 0
+            str = "(<= Y_"+string(locs(1)-1) + " " + num2str(hVal, '%.16f') + "))";
+        else
+            str = "(>= Y_"+string(locs(1)-1) + " " + num2str(hVal, '%.16f') + "))";
+        end
     end
 
 end