Skip to content
Merged
Show file tree
Hide file tree
Changes from 4 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ code/nnv/UUV/
code/nnv/tbxmanager/
code/nnv/tests/io/models/*.caffemodel
.venv
*.asv


data/vgg16_cache.mat
Expand Down
59 changes: 54 additions & 5 deletions code/nnv/engine/nn/NN.m
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@
input_sets = {}; % input set values for each layer (cell array of cells of layer input sets)
dis_opt = []; % display option = 'display' or []
lp_solver = 'linprog'; % choose linprog as default LP solver for constructing reachable set user can choose 'glpk' or 'linprog' as an LP solver
matlabnet = []; % the matlab network this NN was created from

% To facilitate graph computation flow
name2indx = []; % Match name to index in nnvLayers list
Expand Down Expand Up @@ -440,21 +441,57 @@
methods % secondary methods (verification, safety, robustness...)

% Verify a VNN-LIB specification
function result = verify_vnnlib(obj, propertyFile, reachOptions)
function [result, X] = verify_vnnlib(obj, propertyFile, reachOptions, needReshape)

arguments
obj
propertyFile
reachOptions
needReshape = 0;
end

% Load specification to verify
property = load_vnnlib(propertyFile);
lb = property.lb;
ub = property.ub;


if isfield(reachOptions, 'single_average_input') && reachOptions.single_average_input
if ~isa(lb, 'cell')
lb = (lb + ub)/2;
ub = lb;
else
lb = (lb{1} + ub{1})/2;
ub = lb;
end
end

if needReshape > 0.1
Copy link

Copilot AI Dec 1, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[nitpick] Unclear conditional check: Using needReshape > 0.1 is an unusual way to check if reshaping is needed. Since needReshape has a default value of 0 and can be 1 or 2, it would be clearer to use needReshape > 0 or needReshape ~= 0 instead of > 0.1. The current threshold of 0.1 seems arbitrary and could be confusing.

Suggested change
if needReshape > 0.1
if needReshape > 0

Copilot uses AI. Check for mistakes.
% Format bounds into correct dimensions
% (using code from run_vnncomp2024_instance.m)

first_layer = obj.Layers(1, 1);
inputSize = first_layer{1}.InputSize;
if needReshape == 1
lb = permute(lb, [2 1 3]);
ub = permute(ub, [2 1 3]);
elseif needReshape == 2
newSize = [inputSize(2) inputSize(1) inputSize(3:end)];
lb = reshape(lb, newSize);
lb = permute(lb, [2 1 3 4]);
ub = reshape(ub, newSize);
ub = permute(ub, [2 1 3 4]);
else
error("Unsupported value for needReshape")
end
end

% Create reachability parameters and options
if contains(reachOptions.reachMethod, "zono")
X = ImageZono(lb, ub);
else
X = ImageStar(lb,ub);
X = ImageStar(lb, ub);
end

% Compute reachability

Y = obj.reach(X, reachOptions); % Seems to be working
result = verify_specification(Y, property.prop);

Expand Down Expand Up @@ -1468,6 +1505,18 @@ function start_pool(obj)
end
end

% return the indices of layers of the specified types
function layers = get_layer_indices(obj, layer_types)
layers = [];
for l = 1:length(obj.Layers)
for n = 1:length(layer_types)
if isa(obj.Layers{l}, layer_types(n))
layers = [layers l];
end
end
end
end

end % end helper functions


Expand Down
Loading