Skip to content

Commit

Permalink
Fix benchmark naming, counterexample reshape if needed
Browse files Browse the repository at this point in the history
  • Loading branch information
mldiego committed Jul 8, 2024
1 parent 9bc450c commit a1dc065
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 8 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,11 @@
'traffic_signs_recognition'; 'vggnet'; 'vit';
}; % we don't really care much about this one

% for i=3:length(benchmarks)
for i=3 % only do acasxu
for i=3:length(benchmarks)
% for i=3 % only do acasxu

name_noyear = split(benchmarks(i).name, "_");
name_noyear = name_noyear{1};
name_noyear = strjoin(name_noyear(1:end-1), '_');

if contains(name_noyear, regularTrack) % evaluate only regular track

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -290,11 +290,12 @@
if contains(category, 'collins_rul')
net = importNetworkFromONNX(onnx);
nnvnet = matlab2nnv(net);
if contains(onnx, 'full_window_40')
needReshape = 2;
else
needReshape = 1;
end
% if contains(onnx, 'full_window_40')
% needReshape = 2;
% else
% needReshape = 1;
% end
needReshape = 2;

elseif contains(category, "nn4sys")
% nn4sys: onnx to matlab:
Expand Down Expand Up @@ -507,6 +508,12 @@ function write_counterexample(outputfile, counterEx)
% disp([x;yPred']);
for h=1:length(Hs)
if Hs(h).contains(double(yPred)) % property violated
% check if the counter example needs to be reshaped
n = numel(x);
if needReshape == 2
% x = reshape(x, [n 1]);
x = permute(x, [2 1 3]);
end
counterEx = {x; yPred}; % save input/output of countex-example
break;
end
Expand Down

0 comments on commit a1dc065

Please sign in to comment.