update to matlab 2021b docker on codeocean; updates to cav'21 segmentation package for codeocean execution (since segmentation now supported); other minor environment updates preparping for formats'22 ae packages

Author: ttj

Diff for: code/nnv/examples/Submission/CAV2021/M2NIST/compare_m2nist_nets_vs_num_attackedpixels.m

@@ -71,7 +71,8 @@
 VT = zeros(L, M); % verification time
 
 c = parcluster('local');
-numCores = c.NumWorkers;
+%numCores = c.NumWorkers;
+numCores = 1; % some error in codeocean latest release using auto-detect
 poolobj = gcp('nocreate');
 delete(poolobj); % reset parpool
 
@@ -180,7 +181,7 @@
 legend(labels{1:L}, 'interpreter', 'latex');
 hold off;
 
-saveas(fig, 'compare_m2nist_nets_vs_num_attackedpixels.pdf');
+saveas(fig, [path_results(), filesep,'compare_m2nist_nets_vs_num_attackedpixels.pdf']);
 %% plot reach time
 
 N1 = Nets(1);

Diff for: code/nnv/examples/Submission/CAV2021/M2NIST/compare_m2nist_nets_vs_relaxFactor.m

@@ -70,8 +70,7 @@
 
 c = parcluster('local');
 %numCores = c.NumWorkers;
-numCores = 1;
-
+numCores = 1; % some error in codeocean latest release using auto-detect
 
 
 % verify N1 networks in the Nets array using the relax-star approach
@@ -163,7 +162,7 @@
 
 %% Print latex table1
 
-fileID = fopen('N5_verifyTime_vs_relaxFactor.tex', 'w');
+fileID = fopen([path_results(), filesep, 'N5_verifyTime_vs_relaxFactor.tex'], 'w');
 
 N = size(N5_verifyTime, 1);
 for i=1:N

Diff for: code/nnv/examples/Submission/CAV2021/M2NIST/m2nist_net1_verifyTime_vs_relaxFactor.m

@@ -72,8 +72,7 @@
 
 c = parcluster('local');
 %numCores = c.NumWorkers;
-numCores = 1;
-
+numCores = 1; % some error in codeocean latest release using auto-detect
 
 
 % verify N1 networks in the Nets array using the relax-star approach
@@ -165,7 +164,7 @@
 
 %% Print latex table1
 
-fileID = fopen('N4_verifyTime_vs_relaxFactor.tex', 'w');
+fileID = fopen([path_results(), filesep, 'N4_verifyTime_vs_relaxFactor.tex'], 'w');
 
 N = size(N4_verifyTime, 1);
 for i=1:N

Diff for: code/nnv/examples/Submission/CAV2021/M2NIST/m2nist_net2_verifyTime_vs_relaxFactor.m

@@ -72,7 +72,7 @@
 
 c = parcluster('local');
 %numCores = c.NumWorkers;
-numCores = 1;
+numCores = 1; % some error in codeocean latest release using auto-detect
 
 
 
@@ -165,7 +165,7 @@
 
 %% Print latex table1
 
-fileID = fopen('N5_verifyTime_vs_relaxFactor.tex', 'w');
+fileID = fopen([path_results(), filesep, 'N5_verifyTime_vs_relaxFactor.tex'], 'w');
 
 N = size(N5_verifyTime, 1);
 for i=1:N

Diff for: code/nnv/examples/Submission/CAV2021/M2NIST/m2nist_net3_verifyTime_vs_relaxFactor.m

@@ -72,8 +72,7 @@
 
 c = parcluster('local');
 %numCores = c.NumWorkers;
-numCores = 1;
-
+numCores = 1; % some error in codeocean latest release using auto-detect
 
 
 % verify N1 networks in the Nets array using the relax-star approach
@@ -165,7 +164,7 @@
 
 %% Print latex table1
 
-fileID = fopen('N6_verifyTime_vs_relaxFactor.tex', 'w');
+fileID = fopen([path_results(), filesep, 'N6_verifyTime_vs_relaxFactor.tex'], 'w');
 
 N = size(N6_verifyTime, 1);
 for i=1:N

Diff for: code/nnv/examples/Submission/CAV2021/MNIST/compare_mnist_nets_vs_inputsize.m

@@ -71,7 +71,8 @@
 VT = zeros(L, M); % verification time
 
 c = parcluster('local');
-numCores = c.NumWorkers;
+%numCores = c.NumWorkers;
+numCores = 1; % some error in codeocean latest release using auto-detect
 
 % verify L networks in the Nets array
 t1 = tic;
@@ -178,7 +179,7 @@
 legend(labels{1:L}, 'interpreter', 'latex');
 hold off;
 
-saveas(fig, 'compare_mnist_nets_vs_inputsize.pdf');
+saveas(fig, [path_results(), filesep,'compare_mnist_nets_vs_inputsize.pdf']);
 
 fig2 = figure;
 for i=1:L
@@ -193,7 +194,7 @@
 hold off;
 ax = gca;
 ax.FontSize = 13;
-saveas(fig2, 'VT_mnist_nets_vs_inputsize.pdf');
+saveas(fig2, [path_results(), filesep, 'VT_mnist_nets_vs_inputsize.pdf']);
 
 %% plot verified output set
 

Diff for: code/nnv/examples/Submission/CAV2021/MNIST/compare_mnist_nets_vs_num_attackedpixels.m

@@ -70,8 +70,18 @@
 avg_numUnkPixels = zeros(L, M); % average number of unknown pixels
 VT = zeros(L, M); % verification time
 
+% see: https://www.mathworks.com/matlabcentral/answers/196549-failed-to-start-a-parallel-pool-in-matlab2015a
+distcomp.feature('LocalUseMpiexec', true); % false gave error
+
 c = parcluster('local');
-numCores = c.NumWorkers;
+% see: https://www.mathworks.com/help/matlab/ref/maxnumcompthreads.html
+% and: https://www.mathworks.com/matlabcentral/answers/463068-number-of-cores-by-default
+%numCores = maxNumCompThreads;
+%numCores = maxNumCompThreads('automatic');
+%numCores = c.NumWorkers; % causes error
+numCores = 1; % use if error from autodetect, for whatever reason this is showing up on latest codeocean versions
+
+numCores
 
 % verify L networks in the Nets array
 t1 = tic;
@@ -178,7 +188,7 @@
 legend(labels{1:L}, 'interpreter', 'latex');
 hold off;
 
-saveas(fig, 'compare_mnist_nets_vs_num_attackedpixels.pdf');
+saveas(fig, [path_results(), filesep,'compare_mnist_nets_vs_num_attackedpixels.pdf']);
 
 fig2 = figure;
 for i=1:L
@@ -193,6 +203,6 @@
 hold off;
 ax = gca;
 ax.FontSize = 13;
-saveas(fig2, 'VT_mnist_nets_vs_num_attackedpixels.pdf');
+saveas(fig2, [path_results(), filesep,'VT_mnist_nets_vs_num_attackedpixels.pdf']);
 %%
 

Diff for: code/nnv/examples/Submission/CAV2021/MNIST/mnist_net1_verifyTime_vs_relaxFactor.m

@@ -127,7 +127,7 @@
 N1_verifyTime
 
 fprintf("*** NOTE FOR EACH DELTA (de) ***\n");
-fprintf("The firt column is the verification time of the relax-star-random method \n")
+fprintf("The first column is the verification time of the relax-star-random method \n")
 fprintf("The second column is the verification time of the relax-star-area method \n");
 fprintf("The third column is the verification time of the relax-star-range method \n");
 fprintf("The last column is the verification time of the relax-star-bound method \n");
@@ -168,7 +168,7 @@
 
 %% Print latex table1
 
-fileID = fopen('N1_verifyTime_vs_relaxFactor.tex', 'w');
+fileID = fopen([path_results(), filesep, 'N1_verifyTime_vs_relaxFactor.tex'], 'w');
 
 N = size(N1_verifyTime, 1);
 for i=1:N

Diff for: code/nnv/examples/Submission/CAV2021/MNIST/mnist_net2_verifyTime_vs_relaxFactor.m

@@ -173,7 +173,7 @@
 
 %% Print latex table1
 
-fileID = fopen('N2_verifyTime_vs_relaxFactor.tex', 'w');
+fileID = fopen([path_results(), filesep, 'N2_verifyTime_vs_relaxFactor.tex'], 'w');
 
 N = size(N2_verifyTime, 1);
 for i=1:N

Diff for: code/nnv/examples/Submission/CAV2021/MNIST/mnist_net3_verifyTime_vs_relaxFactor.m

@@ -171,7 +171,7 @@
 
 %% Print latex table1
 
-fileID = fopen('N3_verifyTime_vs_relaxFactor.tex', 'w');
+fileID = fopen([path_results(), filesep, 'N3_verifyTime_vs_relaxFactor.tex'], 'w');
 
 N = size(N3_verifyTime, 1);
 for i=1:N

Diff for: code/nnv/examples/Submission/CAV2021/RelaxStarCompare/mnist01_conservativeness_vs_relaxFactor.m

@@ -3,7 +3,9 @@
 
 %% verify the image
 
-numCores = 8; 
+%numCores = 8; 
+numCores = 1; % some error in codeocean latest release using auto-detect
+
 N = 100; % number of Images tested maximum is 100
 %
 poolobj = gcp('nocreate');

Diff for: code/nnv/examples/Submission/CAV2021/RelaxStarCompare/mnist01_relax_star_area_vs_eran.m

@@ -3,7 +3,9 @@
 
 %% verify the image
 
-numCores = 8; 
+%numCores = 8; 
+numCores = 1; % some error in codeocean latest release using auto-detect
+
 N = 100; % number of Images tested maximum is 100
 %
 relaxFactor = [0 0.25 0.5 0.75 1]; % relax factor

Diff for: code/run_codeocean.m

@@ -8,6 +8,14 @@
     'ERROR: path likely not set, run install.m'
 end
 
+% default output path for path_results, ensure logs subdirectory there
+mkdir('/results/logs/')
+
+cd /code/nnv/examples/Submission/CAV2021/
+reproduce_CAV2021
+
+% arch-comp 2021 next
+return
 cd /code/nnv/examples/Submission/ARCH-COMP2021
 run_all
 

Diff for: environment/Dockerfile

@@ -1,5 +1,13 @@
-# hash:sha256:f622d7353e92f49ac2e11234b75ba3e52d96df0222aa7e2bf36ad6cd44b3be51
-FROM registry.codeocean.com/codeocean/matlab:2019a-ubuntu18.04
+# hash:sha256:5f616c6f66b2c7c0f5e3b8d5b21214210b9d8d1dbe6b703011b15b8d65208c91
+FROM registry.codeocean.com/codeocean/matlab:2021b-ubuntu20.04
+
+# old 2020b version
+# hash:sha256:eb133fa6ef390c8a024c045858d448a3c7a34f140ef89a10c693182c8e4e31c7
+#FROM registry.codeocean.com/codeocean/matlab:2020b-ubuntu20.04
+
+# old 2019a version
+## hash:sha256:f622d7353e92f49ac2e11234b75ba3e52d96df0222aa7e2bf36ad6cd44b3be51
+#FROM registry.codeocean.com/codeocean/matlab:2019a-ubuntu18.04
 
 # codeocean does not seem to support multi-stage builds, so python set up is below versus using this image
 # hash:sha256:1f62953520a0e0fb91a3b47349bfbecf2b530ada4a23f795534f50d6d9db554b
@@ -26,7 +34,6 @@ RUN apt-get update \
         python3 \
         python3-dev \
         wget \
-        python-pip \
         python3-pip \
         software-properties-common
 
@@ -38,7 +45,7 @@ RUN pip3 install numpy
 RUN pip install pybind11
 RUN pip3 install pybind11
 
-RUN pkg-config --cflags python
+#RUN pkg-config --cflags python
 
 # set up comparison scripts (for ReluVal, Reluplex, Marabou)
 

Diff for: metadata/metadata.yml

@@ -16,6 +16,7 @@ tags:
 - hybrid-systems
 - artificial-intelligence
 - machine-l
+- neural networks
 authors:
 - name: Taylor T Johnson
   affiliations: