finish ACC case study

code/nnv/engine/set/Star.m

@@ -609,7 +609,8 @@ function plot(obj)
 
             if isempty(obj.C) || isempty(obj.d) % star set is just a vector (one point)
                 lb = obj.V(:, 1);
-                ub = obj.V(:, 1);
+                ub = obj.V(:, 1);               
+                B = Box(lb, ub);
 
             else % star set is a set
 

code/nnv/examples/Submission/HSCC2020/ACC/How to run ACC case study.txt

@@ -0,0 +1,32 @@
+
+NOTE***: To run ACC case study, we need to have CORA installed. 
+
+1) Install NNV: 
+
+        a) git clone --recursive https://github.com/verivital/nnv.git
+
+        b) go to ..code/nnv/ folder to run install.m
+
+2) Run ACC case study: 
+
+        a) Run ACC with discrete linear plant model: 
+
+           a1) using exact analysis: run  verify_discrete_ACC_exact_star.m
+
+               total runtime is about 5.5 hours
+
+           a2) using approximate analysis: run verify_discrete_ACC_approx_star.m
+
+               total runtime is about 4 minutes
+
+        b) Run ACC with nonlinear plant model using approx-star method
+
+           run verify_nonlinear_ACC.m 
+
+           total runtime is about 30 minutes
+
+NOTE***: 
+
+We use 4 cores for computation. If your computer does not have >= 4 cores
+
+Set numCores (or n_cores) parameter (default = 4) in the script to a suitable number 

code/nnv/examples/Submission/HSCC2020/ACC/car_dynamics.m

@@ -0,0 +1,21 @@
+function [dx]=car_dynamics(t,x,a_ego)
+
+mu=0.0001; % friction parameter
+
+% x1 = lead_car position
+% x2 = lead_car velocity
+% x3 = lead_car internal state
+
+% x4 = ego_car position
+% x5 = ego_car velocity
+% x6 = ego_car internal state
+
+% lead car dynamics
+a_lead = -5; 
+dx(1,1)=x(2);
+dx(2,1) = x(3);
+dx(3,1) = -2 * x(3) + 2 * a_lead - mu*x(2)^2;
+% ego car dyanmics
+dx(4,1)= x(5); 
+dx(5,1) = x(6);
+dx(6,1) = -2 * x(6) + 2 * a_ego - mu*x(5)^2;

code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_approx_star.txt

@@ -0,0 +1,14 @@
+
+======================================================
+VERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL
+======================================================
+v_lead(0)                 approx-star    
+                       safety  |  VT   
+[29 30]                SAFE  |  15.764   
+[28 29]                SAFE  |  14.479   
+[27 28]                SAFE  |  17.387   
+[26 27]                UNSAFE  |  31.844   
+[25 26]                UNSAFE  |  41.238   
+[24 25]                UNSAFE  |  43.326   
+-------------------------------------------------------
+Total verification time:      164.038

code/nnv/examples/Submission/HSCC2020/ACC/discrete_ACC_verification_results.txt

@@ -0,0 +1,16 @@
+
+======================================================
+VERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL
+======================================================
+x_lead(0)        exact-star          approx-star    
+               safety  |  VT        safety  |  VT   
+[29 30]         |  0.000          |  0.000   
+[28 29]          |  0.000          |  0.000   
+[27 28]          |  0.000          |  0.000   
+[26 27]          |  0.000          |  0.000   
+[25 26]          |  0.000          |  0.000   
+[24 25]          |  0.000        UNSAFE  |  49.589   
+[23 24]          |  0.000          |  0.000   
+[22 23]          |  0.000          |  0.000   
+[21 22]          |  0.000          |  0.000   
+[20 21]          |  0.000          |  0.000   

code/nnv/examples/Submission/HSCC2020/ACC/nonlinear_ACC.txt

@@ -0,0 +1,14 @@
+
+=======================================================
+VERIFICATION RESULTS FOR ACC WITH NONLINEAR PLANT MODEL
+=======================================================
+v_lead(0)                 approx-star    
+                       safety  |  VT   
+[29 30]              UNSAFE  |  265.006   
+[28 29]              UNSAFE  |  283.954   
+[27 28]              UNSAFE  |  292.673   
+[26 27]              UNSAFE  |  294.249   
+[25 26]              UNSAFE  |  300.120   
+[24 25]              UNSAFE  |  276.630   
+-------------------------------------------------------
+Total verification time:      1712.633

code/nnv/examples/Submission/HSCC2020/ACC/plot_discrete_ACC_reachSets.m

@@ -0,0 +1,49 @@
+% Plot reachable sets for Discrete Linear ACC model
+% Dung Tran: 10/22/2019
+
+
+
+%% Plot output reach sets: actual distance vs. safe distance
+
+% plot reachable set of the distance between two cars d = x1 - x4 vs. ego
+% car's velocity
+
+figure;
+h1 = subplot(2,1,1);
+load dis_ACC_ncs_1.mat;
+map_mat = [1 0 0 -1 0 0 0];
+map_vec = [];
+ncs.plotOutputReachSets('blue', map_mat, map_vec);
+hold on;
+% plot safe distance between two cars: d_safe = D_default + t_gap * v_ego;
+% D_default = 10; t_gap = 1.4 
+% d_safe = 10 + 1.4 * x5; 
+
+map_mat = [0 0 0 0 1.4 0 0];
+map_vec = [10];
+ncs.plotOutputReachSets('red', map_mat, map_vec);
+title(h1,'Actual Distance (blue) vs. Safe Distance (red)');
+xlabel(h1, 'Control Time Steps');
+ylabel(h1, 'Distance');
+xticks(h1, [0:5:50])
+
+h2 = subplot(2,1,2);
+load dis_ACC_ncs_6.mat;
+map_mat = [1 0 0 -1 0 0 0];
+map_vec = [];
+ncs.plotOutputReachSets('blue', map_mat, map_vec);
+hold on;
+% plot safe distance between two cars: d_safe = D_default + t_gap * v_ego;
+% D_default = 10; t_gap = 1.4 
+% d_safe = 10 + 1.4 * x5; 
+
+map_mat = [0 0 0 0 1.4 0 0];
+map_vec = [10];
+ncs.plotOutputReachSets('red', map_mat, map_vec);
+title(h2,'Actual Distance (blue) vs. Safe Distance (red)');
+xlabel(h2, 'Control Time Steps');
+ylabel(h2, 'Distance');
+xticks(h2, [0:5:50])
+
+
+%% END OF SCRIPT

code/nnv/examples/Submission/HSCC2020/ACC/plot_nonlinear_ACC_counterExamples.m

@@ -0,0 +1,17 @@
+cI = counterExamples{1};
+cI = cell2mat(cI);
+d_rel = [1 0 0 -1 0 0]*cI;
+d_safe = [0 0 0 1.4 0 0]*cI + 10;
+
+figure; 
+T = 0:1:50;
+plot(T, d_rel, 'blue');
+hold on;
+plot(T, d_safe, 'red');
+
+xlabel('Control Time Steps', 'FontSize', 13);
+ylabel('Distance', 'FontSize', 13);
+xticks([0:5:50]);
+a = get(gca,'XTickLabel');
+set(gca,'XTickLabel',a,'FontName','Times','fontsize',13)
+title('Actual Distance (blue) vs. Safe Distance (red)');

code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/verify_discrete_ACC.m → code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC.m

@@ -72,7 +72,7 @@
 % initial condition of the plant
 
 % initial position of lead car x_lead
-x_lead = [90 100];
+x_lead = [90 92];
 % initial condition of v_lead
 v_lead = cell(10, 1);
 v_lead{1, 1} = [29 30];
@@ -99,7 +99,7 @@
 % initial condition for new introduced variable 
 x7_0 = [2*a_lead 2*a_lead]; % x7 = -2*x(3) + 2 * a_lead -> x7(0) = -2*x(3)(0) + 2*alead = -2*0 + 2*-2 = -4
 
-N = length(x1);
+N = length(v_lead);
 for i=1:N
     lb = [x_lead(1); v_lead{i}(1); internal_acc_lead(1); x_ego(1); v_ego(1); internal_acc_ego(1); x7_0(1)];
     ub = [x_lead(2); v_lead{i}(2); internal_acc_lead(2); x_ego(2); v_ego(2); internal_acc_ego(2); x7_0(2)];
@@ -118,17 +118,17 @@
 unsafe_mat = [1 0 0 -1 -alpha*1.4 0 0];
 unsafe_vec = alpha*10; 
 
-N = 1; % just for testing
-
+% N = 1; % just for testing
 safe_exact = cell(1,N);
 VT_exact = zeros(1, N);
 counterExamples_exact = cell(1, N);
 dis_ACC_exact = cell(1,N);
 
-% for i=1:N
-%     [safe_exact{i}, counterExamples_exact{i}, VT_exact(i)] = ncs.verify(init_set(i), ref_input, numSteps, 'exact-star', numCores, unsafe_mat, unsafe_vec); 
-%     dis_ACC_exact{i} = ncs; %store for plotting reachable sets
-% end
+for i=1:N
+    [safe_exact{i}, counterExamples_exact{i}, VT_exact(i)] = ncs.verify(init_set(i), ref_input, numSteps, 'exact-star', numCores, unsafe_mat, unsafe_vec); 
+    dis_ACC_exact{i} = ncs; %store for plotting reachable sets
+end
+
 
 safe_approx = cell(1, N);
 VT_approx = zeros(1, N);

code/nnv/examples/Submission/HSCC2020/ACC/Discrete Linear Plant/verify_discrete_ACC.asv → code/nnv/examples/Submission/HSCC2020/ACC/verify_discrete_ACC_approx_star.m

@@ -72,20 +72,16 @@
 % initial condition of the plant
 
 % initial position of lead car x_lead
-x_lead = [90 100];
-v_lead = cell(10, 1);
+x_lead = [90 92];
+% initial condition of v_lead
+v_lead = cell(6, 1);
 v_lead{1, 1} = [29 30];
 v_lead{2, 1} = [28 29];
 v_lead{3, 1} = [27 28];
 v_lead{4, 1} = [26 27];
 v_lead{5, 1} = [25 26];
 v_lead{6, 1} = [24 25];
-v_lead{7, 1} = [23 24];
-v_lead{8, 1} = [22 23];
-v_lead{9, 1} = [21 22];
-v_lead{10, 1} = [ 21];
-% initial condition of v_lead
-v_lead = [23 24];
+
 % initial condition of x_internal_lead
 internal_acc_lead = [0 0];
 % initial condition of x_ego
@@ -99,11 +95,10 @@
 % initial condition for new introduced variable 
 x7_0 = [2*a_lead 2*a_lead]; % x7 = -2*x(3) + 2 * a_lead -> x7(0) = -2*x(3)(0) + 2*alead = -2*0 + 2*-2 = -4
 
-x1 = x_lead;
-N = length(x1);
+N = length(v_lead);
 for i=1:N
-    lb = [x1{i}(1); v_lead(1); internal_acc_lead(1); x_ego(1); v_ego(1); internal_acc_ego(1); x7_0(1)];
-    ub = [x1{i}(2); v_lead(2); internal_acc_lead(2); x_ego(2); v_ego(2); internal_acc_ego(2); x7_0(2)];
+    lb = [x_lead(1); v_lead{i}(1); internal_acc_lead(1); x_ego(1); v_ego(1); internal_acc_ego(1); x7_0(1)];
+    ub = [x_lead(2); v_lead{i}(2); internal_acc_lead(2); x_ego(2); v_ego(2); internal_acc_ego(2); x7_0(2)];
     init_set(i) = Star(lb, ub);
 end
 
@@ -119,17 +114,7 @@
 unsafe_mat = [1 0 0 -1 -alpha*1.4 0 0];
 unsafe_vec = alpha*10; 
 
-N = 1; % just for testing
-
-safe_exact = cell(1,N);
-VT_exact = zeros(1, N);
-counterExamples_exact = cell(1, N);
-dis_ACC_exact = cell(1,N);
-
-% for i=1:N
-%     [safe_exact{i}, counterExamples_exact{i}, VT_exact(i)] = ncs.verify(init_set(i), ref_input, numSteps, 'exact-star', numCores, unsafe_mat, unsafe_vec); 
-%     dis_ACC_exact{i} = ncs; %store for plotting reachable sets
-% end
+% N = 1; % just for testing
 
 safe_approx = cell(1, N);
 VT_approx = zeros(1, N);
@@ -138,37 +123,39 @@
 
 for i=1:N
     [safe_approx{i}, counterExamples_approx{i}, VT_approx(i)] = ncs.verify(init_set(i), ref_input, numSteps, 'approx-star', numCores, unsafe_mat, unsafe_vec);
-    dis_ACC_approx{i} = ncs; % store for plotting reachable sets
 end
 
 
 %% Safe verification results
 
-save discrete_ACC_verification_results.mat safe_exact VT_exact counterExamples_exact safe_approx VT_approx counterExamples_approx dis_ACC_exact dis_ACC_approx;
+save discrete_ACC_approx_star.mat safe_approx VT_approx counterExamples_approx;
 
 %% Print verification results to screen
 fprintf('\n======================================================');
 fprintf('\nVERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL');
 fprintf('\n======================================================');
-fprintf('\nx_lead(0)        exact-star          approx-star    ');
-fprintf('\n               safety  |  VT        safety  |  VT   ');
-fprintf('\n[%d %d]       %s  |  %3.3f        %s  |  %3.3f   ', x_lead{1}(1), x_lead{1}(2), safe_exact{1}, VT_exact(1), safe_approx{1}, VT_approx(1));
-for i=2:N
-fprintf('\n[%d %d]        %s  |  %3.3f        %s  |  %3.3f   ', x_lead{i}(1), x_lead{i}(2), safe_exact{i}, VT_exact(i), safe_approx{i}, VT_approx(i));
+fprintf('\nv_lead(0)                 approx-star    ');
+fprintf('\n                       safety  |  VT   ');
+for i=1:N
+fprintf('\n[%d %d]                %s    %3.3f   ', v_lead{i}(1), v_lead{i}(2), safe_approx{i}, VT_approx(i));
 end
+fprintf('\n-------------------------------------------------------');
+fprintf('\nTotal verification time:      %3.3f', sum(VT_approx));
 
 %% Print verification results to a file
 
-fid = fopen('discrete_ACC_verification_results.txt', 'wt');
+fid = fopen('discrete_ACC_approx_star.txt', 'wt');
+
 fprintf(fid,'\n======================================================');
 fprintf(fid,'\nVERIFICATION RESULTS FOR ACC WITH DISCRETE PLANT MODEL');
 fprintf(fid,'\n======================================================');
-fprintf(fid,'\nx_lead(0)        exact-star          approx-star    ');
-fprintf(fid,'\n               safety  |  VT        safety  |  VT   ');
-fprintf(fid,'\n[%d %d]       %s  |  %3.3f        %s  |  %3.3f   ', x_lead{1}(1), x_lead{1}(2), safe_exact{1}, VT_exact(1), safe_approx{1}, VT_approx(1));
-for i=2:N
-fprintf(fid,'\n[%d %d]        %s  |  %3.3f        %s  |  %3.3f   ', x_lead{i}(1), x_lead{i}(2), safe_exact{i}, VT_exact(i), safe_approx{i}, VT_approx(i));
+fprintf(fid,'\nv_lead(0)                 approx-star    ');
+fprintf(fid,'\n                       safety  |  VT   ');
+for i=1:N
+fprintf(fid,'\n[%d %d]                %s  |  %3.3f   ', v_lead{i}(1), v_lead{i}(2), safe_approx{i}, VT_approx(i));
 end
+fprintf(fid,'\n-------------------------------------------------------');
+fprintf(fid,'\nTotal verification time:      %3.3f', sum(VT_approx));
 fclose(fid);
 
 %% END