CORA v2025.2.0

- ci: better handling of failed jobs and retries, now warns if the duration of a test changed drastically
- conZonotope/representsa: check for 'emptySet' makes use of polytope/representsa now
- converter/cora2spaceex: bug fix, reset assignments
- examples/ARCH'25 revisions
- global/CORAROOT: major speedup
- global/CORAerror: made help text clickable for convenience
- global/CORAlinprog: improved stability
- global/CORAtable: added 'rownr' and 'time' format, added 'csv' design
- global/checkValueAttributes: bug fix, gpuArrays
- global/codingConvention: enforced timerVal in tic-toc
- global/printCell: bug fixes
- global/printMatrix: bug fixes
- global/updateCORApath: should be faster now; no longer includes the repeatability template
- global/verbose: sets, systems, matrices, tables, etc. can now be printed directly into a file
- linearSys/Krylov: refactor, speed up, and improved testing
- linearSys/sparse|full: added
- matZonotope/contains: added
- matZonotope/randPoint: bug fix
- models: moved distributed model files into ./model folder
- neuralNetwork/calcSensitivity: fixed bug with incorrect size
- neuralNetwork/computeReducedNetwork: added, computes a reduced network with nice verification guarantees
- neuralNetwork/explain: added, computes provably sufficient explanations
- nn: added ability to verify graph neural networks
- nnActivationLayer: bug fix, large domains
- polygon/minkDiff: bug fix, reset vertices property
- polytope/project: bug fix, empty polytope did not return the correct polytope
- polytope/representa: emptySet, bug fix
- polytope/zonotope: added method 'inner'
- reachSet/hasTimeInterval: added
- reachSet/plot: bug fix, no time interval
- repeatability package: updates for clarity
- simResult/add: bug fix
- simResult/isemptyobject: bug fix
- specification/check: improved check of reachSet/simResult for timed specifications
- zonoBundle/generateRandom: bug fix
- zonotope/compact: bug fix, outputs are now consistent for 'all'
- zonotope/contains: speed up, if the zonotope represents an interval; bug fix, tolerances
- zonotope/reduce: added two methods based scaling
- zonotope/sparse|full: added
- zonotope/zonotopeNorm: bug fix, minimizer was not returned properly

Author: toladnertum

.github/ISSUE_TEMPLATE/issue-template.md

@@ -0,0 +1,40 @@
+---
+name: Issue Template
+about: General questions, bug reports, and feature requests
+title: ''
+labels: ''
+assignees: TUMcps
+
+---
+
+## Description 
+
+*Briefly describe the issue*
+
+## Steps to Reproduce the Issue
+
+*Ideally provide code of a minimal example. E.g.*
+```
+% 1. init two zonotopes
+Z1 = zonotope([1;2], [1 0 1; 0 1 1]);
+Z2 = zonotope([5;4], [1 0 -1; 0 1 1]);
+
+% 2. plot the zonotopes
+figure;
+plot(Z1);
+plot(Z2);
+```
+
+### Expected Behavior
+
+*both zonotopes are visible in the figure*
+
+### Current Behavior
+
+*only the last zonotope is visible*
+
+## Versions
+
+- CORA version: *v2025.0.0* (type `CORAVERSION` in command window)
+- Matlab version: *R2024b* (type `version` in command window)
+- OS: *Linux/Windows/Mac*

.github/README.md

@@ -0,0 +1,7 @@
+# GitHub
+
+This folder contains all files related to our GitHub repository: https://github.com/TUMcps/CORA
+
+<hr style="height: 1px;">
+
+<img src="../app/images/coraLogo_readme.svg"/>

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

@@ -0,0 +1,27 @@
+name: Create Release on Tag Push
+
+on:
+  push:
+    tags:
+      - '*'
+
+jobs:
+  create_release:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v3
+
+      - name: Get Commit Message
+        id: get_commit_message
+        run: |
+          COMMIT_MESSAGE=$(git log -1 --pretty=format:%s ${{ github.ref }})
+          echo "commit_message=$COMMIT_MESSAGE" >> $GITHUB_ENV
+
+      - name: Create GitHub Release
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          gh release create "${{ github.ref_name }}" \
+            --title "${{ github.ref_name }}" \
+            --notes "${{ env.commit_message }}"

README.md

@@ -10,14 +10,14 @@ A Tool for COntinuous Reachability Analysis.
 
 <hr style="height: 1px;">
 
-The COntinuous Reachability Analyzer (CORA) is a collection of MATLAB classes for the formal verification of cyber-physical systems using reachability analysis. 
-CORA integrates various vector and matrix set representations and operations on them as well as reachability algorithms of various dynamic system classes. 
-The software is designed such that set representations can be exchanged without having to modify the code for reachability analysis. 
-CORA is designed using the object oriented paradigm, such that users can safely use methods without concerning themselves with detailed information hidden inside the object.
- Since the toolbox is written in MATLAB, the installation and use is platform independent. 
-From Release 2018 on, the direct import of SpaceEx models into CORA is also supported. 
-The following points summarize the main features of the CORA toolbox:
-
+The Continuous Reachability Analyzer (CORA) is a MATLAB-based toolbox designed for the formal verification of cyber-physical systems through reachability analysis. 
+It offers a comprehensive suite of tools for modeling and analyzing various system dynamics, including linear, nonlinear, and hybrid systems. 
+CORA supports both continuous and discrete-time systems, accommodating uncertainties in system inputs and parameters. 
+These uncertainties are captured by a diverse range of set representations such as intervals, zonotopes, Taylor models, and polytopes. 
+Additionally, CORA provides functionalities for the formal verification of neural networks as well as data-driven system identification with reachset conformance. 
+Various converters are implemented to easily model a system in CORA such as the well-established SpaceEx format for dynamic systems and ONNX format for neural networks. 
+CORA ensures the seamless integration of different reachability algorithms without code modifications and aims for a user-friendly experience through automatic parameter tuning, 
+making it a versatile tool for researchers and engineers in the field of cyber-physical systems.
 
 ### Reachability Analysis for Continuous Systems
 
@@ -50,8 +50,19 @@ Additionally, one can train verifiably robust neural networks in CORA.
 
 Please check Section 1.3 in the <a target='_blank' href="https://cora.in.tum.de/manual">CORA manual</a>.
 
-Furthermore, if you clone CORA using git, please also i) install <a href="https://git-lfs.com/" target="_blank">git lfs</a> (large file storage) and ii) run the command `git lfs pull` to ensure all data files are downloaded correctly.
+The installation of all required toolboxes can be checked individually by running `test_requiredToolboxes` in MATLAB. 
+To check whether the core functionality of CORA has been set up correctly, 
+run the standard test suite `runTestSuite` which should take about 10 minutes.
+
+Furthermore, if you clone CORA using git, please also 
+i) install <a href="https://git-lfs.com/" target="_blank">git lfs</a> (large file storage) 
+sand ii) run the `git lfs pull` in the command line to ensure all data files are downloaded correctly.
+Then, iii) you can check the correct download of the data files in MATLAB using `test_gitlfs`.
 
+**Repeatability package:**
+We also provide a template for a repeatability package to run CORA within Docker in one click.
+This can also be used to use CORA without installing Matlab directly on your device.
+Please visit `./unitTests/ci/repeatability-template` for details.
 
 ### Folder Structure
 

app/examples/linear_reach.mat

@@ -1,19 +1,23 @@
-function printSystem(sys,varargin)
+function res = printSystem(varargin)
 % printSystem - prints a contDynamic object such that if one executes this command
 %    in the workspace, this contDynamic object would be created
 %
 % Syntax:
 %    printSystem(sys)
-%    printSystem(sys,'high')
+%    printSystem(sys,accuracy,doCompact,clearLine)
+%    printSystem(fid,sys,varargin)
+%    printSystem(filename,sys,varargin)
 %
 % Inputs:
-%    sys - contDynamic
-%    accuracy - (optional) floating-point precision
-%    doCompact - (optional) whether to compactly print the set
-%    clearLine - (optional) whether to finish with '\n'
+%    sys - contDynamics
+%    accuracy - floating-point precision
+%    doCompact - whether to compactly print the set
+%    clearLine - whether to finish with '\n'
+%    filename - char, filename to print given obj to
+%    fid - char, fid to print given obj to
 %
 % Outputs:
-%    -
+%    res - logical
 %
 % Other m-files required: none
 % Subfunctions: none
@@ -23,78 +27,74 @@ function printSystem(sys,varargin)
 
 % Authors:       Tobias Ladner
 % Written:       10-October-2024
-% Last update:   ---
+% Last update:   20-May-2025 (TL, added option for fid)
 % Last revision: ---
 
 % ------------------------------ BEGIN CODE -------------------------------
 
-narginchk(0,4);
-[accuracy,doCompact,clearLine] = setDefaultValues({'%4.3f',false,true},varargin);
-if ischar(accuracy) && strcmp(accuracy,'high')
-    accuracy = '%16.16f';
-end
-inputArgsCheck({ ...
-    {sys,'att',{'contDynamics'}}, ...
-    {accuracy,'att', {'char','string'}}, ...
-    {doCompact,'att','logical'}, ...
-    {clearLine,'att','logical'}
-})
+% parse input
+[fid,closefid,sys,accuracy,doCompact,clearLine] = initPrint(varargin{:});
 
 % get print info
 [propertyOrder] = getPrintSystemInfo(sys);
 
 if doCompact
     % print in one line
-    fprintf('%s(',class(sys))
+    fprintf(fid,'%s(',class(sys));
     for p = 1:numel(propertyOrder)
         pname = propertyOrder{p};
-        aux_printProperty(sys.(pname),accuracy);
+        aux_printProperty(fid,sys.(pname),accuracy);
         if p < numel(propertyOrder)
-            fprintf(', ')
+            fprintf(fid,', ');
         end
     end
-    fprintf(')')
+    fprintf(fid,')');
 
 else
     % print each property as variable
     for p = 1:numel(propertyOrder)
         pname = propertyOrder{p};
-        fprintf('%s = ',pname);
-        aux_printProperty(sys.(pname),accuracy);
-        fprintf(';\n');
+        fprintf(fid,'%s = ',pname);
+        aux_printProperty(fid,sys.(pname),accuracy);
+        fprintf(fid,';\n');
     end
     % init set
-    fprintf('sys = %s(%s);',class(sys),strjoin(propertyOrder,','));
+    fprintf(fid,'sys = %s(%s);',class(sys),strjoin(propertyOrder,','));
 end
 
 if clearLine
-    fprintf('\n');
+    fprintf(fid,'\n');
 end
 
+% finalize
+res = closePrint(fid,closefid);
+
 end
 
 
 % Auxiliary functions -----------------------------------------------------
 
-function aux_printProperty(property,accuracy)
+function aux_printProperty(fid,property,accuracy)
+    % Matlab objects ---
     if ischar(property) || isstring(property)
-        fprintf("'%s'",property);
+        fprintf(fid,"'%s'",property);
     elseif isnumeric(property)
-        printMatrix(property,accuracy,true,false);
+        printMatrix(fid,property,accuracy,true,false);
     elseif iscell(property)
-        printCell(property,accuracy,true,false);
+        printCell(fid,property,accuracy,true,false);
     elseif isstruct(property)
-        printStruct(property,accuracy,true,false);
-    elseif isa(property,'contSet') || isa(property,'matrixSet')
-        printSet(property,accuracy,true,false)
-    elseif isa(property,'contDynamics')
-        printSystem(property,accuracy,true,false)
+        printStruct(fid,property,accuracy,true,false);
     elseif isa(property,'function_handle')
         funcstr = func2str(property);
         if ~startsWith(funcstr,'@')
             funcstr = sprintf('@%s',funcstr);
         end
-        fprintf(funcstr)
+        fprintf(fid,funcstr);
+        % CORA objects ---
+    elseif isa(property,'contSet') || isa(property,'matrixSet')
+        printSet(fid,property,accuracy,true,false);
+    elseif isa(property,'contDynamics')
+        printSystem(fid,property,accuracy,true,false);
     else
         throw(CORAerror("CORA:noops",property))
     end

app/examples/nonlinear_reach.mat

@@ -89,9 +89,14 @@
             H_ = max(infimum(H_),supremum(H_));
             errorLagr(i) = 0.5 * dz' * H_ * dz;
         end
+
+        % check if Lagrange remainder is too large
+        if any(isnan(errorLagr)) || any(isinf(errorLagr))
+            throw(CORAerror('CORA:reachSetExplosion','Lagrange remainder exploded.'))
+        end
 
         trueError = errorLagr;
-        VerrorDyn = zonotope(0*trueError,diag(trueError));
+        VerrorDyn = zonotope(zeros(size(trueError)),diag(trueError));
 
     else
         % no interval arithmetic (?)

contDynamics/@contDynamics/printSystem.m

@@ -84,9 +84,9 @@
     if options.approx.verbose
         fprintf('Output dimension %d. \n', i_y)
     end
-    tic
+    timerVal = tic;
     gp = rungp(@(x) config_gp(x, params, options, 'blackGP'));
-    T = toc;
+    T = toc(timerVal);
     if options.approx.save_res
         save(file_approx_iy,"gp", "T");
     end
@@ -106,7 +106,7 @@
 options.approx.yval = yval;
 options.approx.ytrain = ytrain;
 options.approx.pop_pre = true;
-tic
+timerVal = tic;
 % create initial propulation with normal genetic programming
 del_res = false;
 if ~isfield(options.approx, 'cgp_file_pop_pre') && ...
@@ -125,7 +125,7 @@
 
 params.testSuite = params.testSuite_val;
 gp = rungp(@(x)config_gp(x, params, options, 'blackCGP'));
-T = toc;
+T = toc(timerVal);
 if options.approx.save_res
     save(options.approx.filename,"gp", "T");
 end

contDynamics/@contDynamics/private/priv_abstrerr_lin.m

@@ -0,0 +1,49 @@
+function linsys_full = full(linsys)
+% full - Converts system matrices/vectors to full representation
+%
+% Syntax:
+% linsys_full = full(linsys)
+%
+% Inputs:
+%    linsys - linearSys object
+%
+% Outputs:
+%    linsys_full - linearSys object with full system matrices/vectors
+%
+% Example:
+%    A = rand(10,10);
+%    A(A < 0.8) = 0;
+%    B = rand(10,10);
+%    B(B < 0.8) = 0;
+%    sys = linearSys(sparse(A),sparse(B));
+%    sys_full = full(sys);
+%    disp(sys);
+%    disp(sys_full);
+%
+% Other m-files required: none
+% Subfunctions: none
+% MAT-files required: none
+%
+% See also: none
+
+% Authors:       Maximilian Perschl
+% Written:       02-June-2025
+% Last update:   ---
+% Last revision: ---
+
+% ------------------------------ BEGIN CODE -------------------------------
+
+A = full(linsys.A);
+B = full(linsys.B);
+c = full(linsys.c);
+C = full(linsys.C);
+D = full(linsys.D);
+k = full(linsys.k);
+E = full(linsys.E);
+F = full(linsys.F);
+
+linsys_full = linearSys(linsys.name,A,B,c,C,D,k,E,F);
+
+end
+
+% ------------------------------ END OF CODE ------------------------------