CORA v2026.0.0

- Automatic system identification: It is now possible to automatically identify a suitable dynamic model from data and establish reachset conformance via the identify and conform operators. We also overhauled how trajectories are handled in CORA to improve efficiency. For details, please visit Sec. 4.1.9, Sec. 4.1.11, and Sec. 7.2.
- Neural network verification: We significantly improved the verification of neural networks in CORA, added the ability to verify graph neural networks, generate sufficient explanations for neural network predictions, and overhauled the training of verifiably robust neural networks. Details can be found in Sec. 6.
- Set containment certificate: While contains has always returned true if CORA was able to determine containment, a returned false might also indicate that containment holds, but CORA is not able to determine it. To eliminate this ambiguity, contains now also returns a certificate on the result. Details are described in Sec. 2.1.2.1.
- Visualizations: We revised the plotting capabilities of CORA and introduced a new default schema to plot sets to improve visibility on small monitors and beamers. It is also possible to create animated videos directly from CORA. Additionally, users might want to check CORAtables for better display of tabular data. For details, please visit Sec. 2.1.4.10.
- Repeatability package: If you want to use CORA as part of a repeatability package, we got you covered and provide a Docker file with all dependencies installed. Instructions on how to set it up can be found in Appendix F.
- Miscellaneous: Minor improvements have been made in various parts of the code: Some basic functionality runs more efficiently, several bug fixes result in an improved user experience, and more unit tests ensure greater reliability. Please also have a look at Appendix A.12 for deprecated functionality and their replacements.

Author: maxPerschl

.gitattributes

@@ -13,3 +13,4 @@
 *.mexa32 filter=lfs diff=lfs merge=lfs -text
 *.mexa64 filter=lfs diff=lfs merge=lfs -text
 *.ins filter=lfs diff=lfs merge=lfs -text
+

.github/ISSUE_TEMPLATE/issue-template.md

@@ -35,6 +35,6 @@ plot(Z2);
 
 ## Versions
 
-- CORA version: *v2025.0.0* (type `CORAVERSION` in command window)
-- Matlab version: *R2024b* (type `version` in command window)
+- CORA version: *v202x.x.x* (type `CORAVERSION` in command window)
+- Matlab version: *R202xx* (type `version` in command window)
 - OS: *Linux/Windows/Mac*

.github/README.md

@@ -15,7 +15,7 @@ jobs:
       - name: Get Commit Message
         id: get_commit_message
         run: |
-          COMMIT_MESSAGE=$(git log -1 --pretty=format:%s ${{ github.ref }})
+          COMMIT_MESSAGE=$(git log -1 --pretty=format:%B ${{ github.ref }})
           echo "commit_message=$COMMIT_MESSAGE" >> $GITHUB_ENV
 
       - name: Create GitHub Release

.github/workflows/release-on-tag.yml

@@ -37,11 +37,17 @@ manual/*.pdf
 **/*.toc
 **/*.synctex.gz
 **/*-eps-converted-to.pdf
+**/*.synctex(busy)
 
-manual/figures/externalize
+manual/figures/externalize/**/*.dpth
+manual/figures/externalize/**/*.log
+manual/figures/externalize/**/*.md5
 
 */.idea
 manual/manual.iml
 
 # for MAC users
-**/.DS_Store
+**/.DS_Store
+
+# exclude folders in workspace
+workspace/*

.gitignore

@@ -84,4 +84,4 @@ Please visit `./unitTests/ci/repeatability-template` for details.
 
 <hr style="height: 1px;">
 
-<img src="./app/images/coraLogo_readme.svg"/>
+<img src="./app/images/coraLogo_readme.svg"/>

README.md

@@ -522,10 +522,10 @@
     % for Hybrid system the location was also inserted
     if ~strcmp(currentOption, 'Hybrid System')
         fprintf(id, '\n[t,x] = simulate(%s, paramsSim);\n', Sys);
-        fprintf(id, 'simRes = simResult({x},{t});\n\n');
+        fprintf(id, 'traj = trajectory([],x,[],t);\n\n');
     else
         fprintf(id, '\n[t,x,loc] = simulate(%s, paramsSim);\n', Sys);
-        fprintf(id, 'simRes = simResult(x,t,loc);\n\n');
+        fprintf(id, 'traj = trajectory([],x,[],t,[],loc);\n\n');
     end
 
 elseif Random_Simulation
@@ -540,7 +540,7 @@
     fprintf(id, 'simOpt.fracInpVert = %s;\n', simOpt_fracInpVert_random);
     fprintf(id, 'simOpt.nrConstInp = %s;\n', simOpt_nrConstInp_random);
 
-    fprintf(id, '\nsimRes = simulateRandom(%s, params, simOpt);\n\n', Sys);
+    fprintf(id, '\ntraj = simulateRandom(%s, params, simOpt);\n\n', Sys);
 
 elseif Simulate_RRT
 
@@ -558,7 +558,7 @@
     end
 
     fprintf(id, 'simOpt.stretchFac = %s;\n', simOpt_stretchFac_RRT);
-    fprintf(id, '\nsimRes = simulateRandom(%s, reachSet, params, simOpt, ''rrt'');\n\n', Sys);
+    fprintf(id, '\ntraj = simulateRandom(%s, reachSet, params, simOpt, ''rrt'');\n\n', Sys);
 end
 
 % ... write the fifth section which is the plotting settings
@@ -649,13 +649,13 @@
     fprintf(id, '\n    %% plot simulation results');
     fprintf(id, '\n    if length(projDims) == 1\n');
     if strcmp(color_simulation, 'gray')
-        fprintf(id, '        plotOverTime(simRes, projDims, ''%s'', ''color'', %s);\n',line_simulation, gray_color); 
+        fprintf(id, '        plotOverTime(traj, projDims, ''%s'', ''color'', %s);\n',line_simulation, gray_color); 
         fprintf(id, '    else\n');
-        fprintf(id, '        plot(simRes, projDims, ''%s'', ''color'', %s);\n',line_simulation, gray_color); 
+        fprintf(id, '        plot(traj, projDims, ''%s'', ''color'', %s);\n',line_simulation, gray_color); 
     else
-        fprintf(id, '        plotOverTime(simRes, projDims, ''%s'', ''color'', ''%s'');\n',line_simulation, color_simulation); 
+        fprintf(id, '        plotOverTime(traj, projDims, ''%s'', ''color'', ''%s'');\n',line_simulation, color_simulation); 
         fprintf(id, '    else\n');
-        fprintf(id, '        plot(simRes,projDims, ''%s'', ''color'', ''%s'');\n',line_simulation, color_simulation);  
+        fprintf(id, '        plot(traj,projDims, ''%s'', ''color'', ''%s'');\n',line_simulation, color_simulation);  
     end
     fprintf(id, '    end\n');
 end

app/generate_file.m

@@ -1,10 +1,10 @@
-function [params, results] = conform(sys,params,options,varargin)
+function [params,results] = conform(sys,params,options,varargin)
 % conform - performs reachset conformance by computing the reachable 
 %         of a system and checking whether all measurements are included
 %
 % Syntax:
-%    [params, results] = conform(sys,params,options)
-%    [params, results] = conform(sys,params,options,type)
+%    [params,results] = conform(sys,params,options)
+%    [params,results] = conform(sys,params,options,type)
 %
 % Inputs:
 %    sys - contDynamics object
@@ -17,9 +17,9 @@
 %    params - struct with conformant parameters
 %    results - struct with the optimization results (dependent on type)
 %       .R - reachSet object (only time steps for which measurments exist)
-%       .simRes - states of the rapidly exploring random tree
-%       .unifiedOutputs - unified test cases (only deviation to nominal 
-%           solution)
+%       .traj - states of the rapidly exploring random tree
+%       .unifiedOutputs - n_m x 1 cell array with dim_y x n_k x n_s 
+%           arrays describing the deviation to the nominal solution
 %       .sys - updated system
 %       .p - estimated parameters
 %       .fval - final optimization cost
@@ -41,6 +41,7 @@
 % Authors:       Matthias Althoff, Laura Luetzow
 % Written:       15-June-2023
 % Last update:   21-March-2024 (LL, change name from confSynth to conform)
+%                08-September-2025 (LL, change structure of unified outputs)
 % Last revision: ---
 
 % ------------------------------ BEGIN CODE -------------------------------
@@ -52,47 +53,56 @@
 switch type
     case "RRT"
         % synthesize conformance using RRTs, see [1]    
-        [params, R, simRes] = priv_conform_RRT(sys, params, options);
+        [params,R,traj] = priv_conform_RRT(sys,params,options);
         results.R = R;
-        results.simRes = simRes;
+        results.traj = traj;
 
     otherwise
 
-        if contains(type,"black") % blackGP, blackCGP
+        if type == "black" 
             % approximate the system dynamics
-            sys = priv_conform_black(params, options, type);
+            traj = options.id.testSuite_id;
+            options_ = options;
+            options_.id = rmfield(options_.id, 'testSuite_id');
+            if isa(sys, 'nonlinearARX') && contains(options.idAlg, 'gp')
+                % requires system parameters and conformance testSuite for 
+                % identification
+                options_.params = params;
+            end
+            sys = sys.identify(traj,options_);
+            if options.id.save_res
+                save(options.id.filename + "_sys", 'sys');
+            end
+            options = rmiffield(options,'id');
             results.sys = sys;
-            options = rmfield(options, 'approx');
-            params = rmfield(params, ["testSuite_train","testSuite_val"]);
         end
-    
+
         % conformance synthesis for dedicated system dynamics
         [params,options] = validateOptions(sys,params,options);
         [sys_upd,params,options] = aux_updateSys(sys,params,options);
 
         % Identify conformant parameters
-        if type == "white" || contains(type,"black")
-            [params, fval, p_opt,  union_y_a] = priv_conform_white(sys_upd, params, options);
+        if type == "white" || type == "black"
+            [params,fval,p_opt,union_y_a] = priv_conform_white(sys_upd,params,options);
             results.sys = sys;
             results.unifiedOutputs = union_y_a;
-    
-        elseif contains(type,"gray") % "graySim", "graySeq", "grayLS"
-            [params, fval, p_opt, sys_opt] = priv_conform_gray(sys_upd, params, options, type);
+
+        elseif contains(type,"gray") % "graySim","graySeq","grayLS"
+            [params,fval,p_opt,sys_opt] = priv_conform_gray(sys_upd,params,options,type);
             results.sys = sys_opt;
         end
-    
+
         params = aux_updateUWV(params);
         results.fval = fval;
         results.p = p_opt;
-
 end
 
 end
 
 
 % Auxiliary functions -----------------------------------------------------
 
-function [sys, params, options] = aux_updateSys(sys, params, options)
+function [sys,params,options] = aux_updateSys(sys,params,options)
 % preprocess sys, parameters and options
 
 % augment input set with the additive uncertainty sets W and V if given
@@ -107,19 +117,9 @@
     sys = augment_u_with_v(sys);
 end
 
-% add the dimensions of the optimization variables to options
-options.cs.n_a = size(params.U.generators,2) + size(params.R0.generators,2);
-if isa(sys, 'linearSysDT') || isa(sys, 'linearARX')
-    % c can be computed with linear programming
-    options.cs.n_c = size(params.U.generators,1) + size(params.R0.generators,1);
-else
-    % c is not estimated in the linear program
-    options.cs.n_c = 0;
-end
-
 % adapt testSuite to the system dynamics (augment nominal input, update
 % initial state)
-params.testSuite = aux_preprocessTestSuite(sys, params.testSuite);
+params.testSuite = aux_preprocessTestSuite(sys,params.testSuite,options.cs.recMethod);
 
 end
 
@@ -141,45 +141,34 @@
 
 end
 
-function testSuite = aux_preprocessTestSuite(sys, testSuite)
+function testSuite = aux_preprocessTestSuite(sys,testSuite,recMethod)
 % preprocessTestSuite - preprocess testSuite, i.e., 
 %   - augment nominal inputs with zeros to match input dimension of sys
 %   - unify test cases for linear systems, 
 %   - adapt the initial state to the given system dynamics
 
 % Augment nominal input with zeros
 for m = 1:length(testSuite)
-    diff_u = sys.nrOfInputs - size(testSuite{m}.u,2);
+    diff_u = sys.nrOfInputs - size(testSuite(m).u,1);
     if diff_u > 0
-        u_in = cat(2, testSuite{m}.u, zeros(size(testSuite{m}.u,1), diff_u, size(testSuite{m}.u,3)));
-        testSuite{m} = testCase(testSuite{m}.y, u_in, testSuite{m}.initialState, sys.dt, class(sys));
-    end
-end
-
-% Combine test cases for linear systems
-if (isa(sys, 'linearARX') || isa(sys, 'linearSysDT')) ...
-        && length(testSuite) > 1
-    testSuite_m = combineTestCases(testSuite{1},testSuite{2});
-    for m=3:length(testSuite)
-        testSuite_m = combineTestCases(testSuite_m,testSuite{m});
+        u_in = [testSuite(m).u; zeros(diff_u, testSuite(m).n_k)];
+        testSuite(m) = trajectory(u_in, testSuite(m).x, testSuite(m).y, [], sys.dt, [], [], testSuite(m).name);
     end
-    testSuite = {};
-    testSuite{1} = testSuite_m;
 end
 
 % Adaption initial state to state-space models
 if ~isa(sys, 'linearARX') && ~isa(sys, 'nonlinearARX') 
-    if sys.nrOfDims == size(testSuite{1}.initialState,1)
+    if sys.nrOfDims == size(testSuite(1).x,1)
         % all good
         return
     end
-    throw(CORAerror('CORA:notSupported',['Transformation of test cases created by input-output-models ' ...
+    throw(CORAerror('CORA:notSupported',['Transformation of trajectories created by input-output-models ' ...
         'to state-space models is not implemented, yet.']))
 end
 
 % Adaption initial state to input-output models
-if contains(testSuite{1}.name, ["ARX", "ARX"]) && ...
-        sys.n_p*sys.nrOfOutputs == size(testSuite{1}.initialState,1)
+if contains(testSuite(1).name, ["ARX", "ARX"]) && ...
+        sys.n_p*sys.nrOfOutputs == size(testSuite(1).x,1)
     % testSuite was generated by an input-output model with the same
     % model dimension
     % -> initial state should be set correctly
@@ -191,7 +180,7 @@
 n_m = length(testSuite);
 testSuite_new = {};
 for m=1:n_m
-    testSuite_new = [testSuite_new; setInitialStateToMeas(testSuite{m},sys.nrOfDims)];
+    testSuite_new = [testSuite_new; setInitialStateToMeas(testSuite(m),sys.nrOfDims)];
 end
 testSuite = testSuite_new;