Toolbox for Reachability Analysis
License: GNU General Public License v3.0
Prof. Dr.-Ing. Matthias Althoff
https://www.ce.cit.tum.de/cps/
See also: https://www.ce.cit.tum.de/cps/software/
% Cora release 2020. Matlab 2019b. Windows 10.
zono1 = zonotope([0.7,1, -0.2, 0.5;1,1, 0.4, 0.2]);
zono2 = zonotope([1.5,0.7,0.1,0.9,0.2;1.0,-0.1,-0.1,-0.9,-0.1]);
isIntersecting(zono1, zono2)
% ans = logical 0. But It is wrong.
% In fact, two zonotopes does intersect. Plot them to check
Propagating Polynomial Zonotopes through a ReLU neural network fails, for polynomial relaxations of order > 2.
Using the mnist-net_256x4.onnx (available here), the code
evParams = struct;
evParams.num_generators = 10000;
evParams.reuse_bounds = true;
nn = neuralNetwork.readONNXNetwork("../mnist-net_256x4.onnx", false, 'SSC');
lbs = zeros(784,1);
ubs = zeros(784,1);
lbs(390:394) = 0;
ubs(390:394) = 1;
X = polyZonotope(X0);
Y = nn.evaluate(X, evParams);
nn.refine(3, 'layer', 'both', X.randPoint(1), true);
Y = nn.evaluate(X, evParams);
nn.refine(3, 'layer', 'both', X.randPoint(1), true);
Y = nn.evaluate(X, evParams);fails with error message
Error using +
Arrays have incompatible sizes for this operation.
Error in nnActivationLayer/evaluatePolyZonotope>aux_preOrderReduction (line 161)
id = [id; id_ + (1:q)'];
Error in nnActivationLayer/evaluatePolyZonotope (line 57)
[c, G, GI, E, id, id_, ind, ind_] = aux_preOrderReduction(obj, c, G, GI, E, id, id_, ind, ind_, evParams);
Error in neuralNetwork/evaluate>aux_evaluatePolyZonotope (line 178)
layer_i.evaluatePolyZonotope(c, G, GI, E, id, id_, ind, ind_, evParams);
Error in neuralNetwork/evaluate (line 92)
r = aux_evaluatePolyZonotope(obj, input, evParams, idxLayer);
Error in mwe_refine_error (line 17)
Y = nn.evaluate(X, evParams);
Related documentation
% Cora release 2020 installed. Matlab 2019b. Windows 10.
% the following section works. although zono1&zono2 = empty
zono1=zonotope(0,[1,2]);
zono2=zonotope(5,1);
zono1&zono2
zono1=zonotope(-0.7965,[0.1067 -0.2881 0.1512 0.0534 -0.2368 -0.1073 0.0449 -0.1008 -0.1057 0.0270 0.0227 -0.0342 0.0024 0.0442 -0.0091 -0.0030 0.0246 0.0039 0.0479 -0.1852 0.5000 0]);
zono2=zonotope(2.3811,-0.1000);
% empty intersection
% next command will raise error: Error using interval. Lower limit larger than upper limit.
zono1 & zono2
When running the example in @interval/gridPoints.m, I get the follow error
>> I = interval([1 2; -1 1]);
>> coordinates = gridPoints(I,10);
Unable to perform assignment because the size of the left side is 2-by-1 and the size of the right side is 2-by-2.
Error in interval/gridPoints (line 50)
coordinateMat(:,i) = startingPoint+(comb(i,:)'-1).*segLengthVec;
When you download the cora repository, its size is around 30MB. This big size is mostly from the manuals. As every update increases the size of the repository heavily (pdf = binary file), I would recommend splitting the repo into two:
I would be happy to hear your thoughts.
I've met this issue several times in CORA 2020. symVariable.m doesn't add 'real' assumption when declaring a matlab 'sym' variable. So when running derivatives.m to get high order derivatives, the matlab symbolic toolbox will automatically generate stuff like 'conj', which is super unfriendly to your interval class, when you try to use interval arithmetic to bound high order error. I wonder since the states in your applications mostly are real numbers, maybe you can add this 'real' assumption in the symVariable.m, so that I don't have to manually remove 'conj' every time.
Undefined function 'select' for input arguments of type 'nonlinDASys'.
instantiate any zontope Z. Then use polygon(Z).
you should see that the two middle points are always the same. This results in unnecessary warnings, such as by using polyshape(polygon(Z)')
In zonotope/polygon.m, change line 71-72 to:
p = [p(1,:),p(1,end)+p(1,1)-p(1,2:end);...
p(2,:),p(2,end)+p(2,1)-p(2,2:end)];
Hi,
My name is Daniel, and I am taking my first steps heading for using the reachInner algorithm from your package. Trying to run the example from Sec. 4.1.2 from the CORA Manual, I got stuck with an issue. After debugging the code a little bit, I noticed that the problem is in the call to the mptPolytope constructor (in this line).
Here is the stack trace:
>> C = [1 0 -1 0 1; 0 1 0 -1 1]';
>> d = [3; 2; 3; 2; 1];
>> poly = mptPolytope(C,d);
Undefined function 'polytope' for input arguments of type 'double'.
Error in mptPolytope (line 73)
obj.P=polytope(varargin{1},varargin{2});Am I doing something wrong?
Thanks in advance, and congratulations on your code!
The following code in CORA 2020 is returning false instead of true:
Z = zonotope([zeros(2,1),rand(2,5)])
in(Z,zeros(2,1))
However, this works correctly:
in(Z,zonotope(zeros(2,1)))
Recently I need to solve the reachable set of a one dimensional linear dynamical system, but when I set the matrix to one dimensional, the generated set is of zonotope type and one dimensional sets cannot be represented using zonotope type. I don't know how to solve the reachable set of a one dimensional linear dynamical system, can you give some suggestions.
Wrong value for the first input argument.
The right value: zonotope
Type 'help zonotope\plot' for more information.
error zonotope/plot>aux_parseInput
inputArgsCheck({{Z,'att','zonotope'};
error zonotope/plot
[Z,dims,NVpairs] = aux_parseInput(Z,varargin{:});
error test
plot(a,b);
Hi,
I am trying to extract the YData from the reachSet after using reach. I specifically want to do this to add a constant offset to each y-value of the reach set and then plot Y vs time. Is there a method to extract that information from the zonotope object?
This is my code:
R = reach(reactor_ss, params, options);
The output is R which is a 1x1 reachSet consisting of timePoint, timeInterval, parent. and loc. The 'timePoint' is a structure which contains the set, time, and error. 'set' is a cell array containing zonotopes for each time point of the reachset. Is there a away to extract the 'set' information to manipulate and plot it.
Hi,
Im using CORA v2024.2.1 on a nonlinear system. I receive this error:
Array indices must be positive integers or logical values.
Error in nonlinearSys/linReach_adaptive (line 303)
if varphi < options.zetaphi(options.minorder+1)
Error in nonlinearSys/reach_adaptive (line 83)
[Rnext.ti,Rnext.tp,options] = linReach_adaptive(obj,options,options.R);
Error in contDynamics/reach (line 68)
[timeInt,timePoint,res,~,options] = reach_adaptive(obj,params,options);
Error in verification_reach_turbine (line 36)
R = reach(turbine, params, options);
I have tried other nonlinear systems and they are working fine, but this .m file seems to have issues.
When trying to use the nonlinParamSys class with multiple time varying inputs, I get the error:
Incorrect number or types of inputs or outputs for function 'dim'.
Error in equalDimCheck (line 50)
ind_dim = dim(obj)==dim(S);
Error in * (line 115)
equalDimCheck(Z,M);
Error in inputSolution (line 66)
inputSetTrans = intM*zonotope(vTrans);
I've cut out the stack traces above the multiplication which causes the error.
I've attached a file which causes the error. (rename to .m to get around GitHub upload limitations) Note that a different error is caused if only one parameter is used instead of two. This error also stops occurring if there is only one RHS equation or input, or if the number of RHS equations and input are equal. I'm running CORA 2022 stable with MATLAB 2022b on MacOS.
Hello,
I am getting a dimension error while using the reach function for a linear system, without having any error in previous function for the system definition. Here is the error and my code (I tried different examples that works perfectly) :
_Error using *
Incorrect dimensions for matrix multiplication. Check that the number of columns in the first matrix
matches the number of rows in the second matrix. To perform elementwise multiplication, use '.*'.
Error in zonotope/intervalMultiplication (line 47)
Z.Z = [0center(Z),diag(SZabssum)];
Error in * (line 42)
res = intervalMultiplication(factor2,factor1);
Error in reach_adaptive>initTimeStep (line 443)
Etu = obj.taylor.error * options.timeStep * options.U;
Error in reach_adaptive (line 97)
options = initTimeStep(obj,options);
Error in linearSys/reach (line 62)
[Rout,Rout_tp,res,deltaT] = reach_adaptive(obj, options);
Error in Example_Full_Algo (line 34)
Rf = reach(sysf,params,options);_
The code :
`% system definition
A = [zeros(6,6) eye(6,6); zeros(1,4) 2 zeros(1,7); zeros(1,3) -5 zeros(1,8); zeros(4,12);]; % size 12x12
B = [zeros(8,4); diag([1/0.063 1/0.582857e-4 1/0.716914e-4 1/1e-4])]; % size 12x4
% zonotopes definition
x = [1 1 1, 0.01 0.02 0.5, 0.02 0.03 -0.05, 0.02 0.03 -0.05]'; %size 1x12
genx = 0.1*eye(12,12); %size 12x12
u = [1;0;0;0]; %size 1x4
genu = diag([1 0.1 0.1 0.1]); %size 4x4
Zx = conZonotope(x,genx,[],[]);
Zu = zonotope(u,genu);
sysf = linearSys(A, B);
% Parameters and options
clear params options
options.linAlg = 'adaptive';
options.error = 0.1;
options.verbose = true;
params.tFinal = 1;
params.R0 = Zx;
params.U = Zu;
Rf = reach(sysf,params,options);`
The linearization error computation of the nonlinearSys should always terminate, as the error is increased step by step. However, the current implementation does not always increase it and therefore, can get stuck in an infinite loop.
In contDynamics/@nonlinearSys/private/linReach.m: The error variable saves the true error of the last iteration, which is increased for the next iteration. For a model with dimension > 1, I experienced the following:
Unfortunately, I cannot extract a minimum working example (can someone come up with one?). Therefore, the numbers from above are not the real ones, but have the same characteristics as the experienced ones. This is possibly a corner case, but there should be a workaround.
The following code throws an error for me:
Z = zonotope(zeros(2, 1), randn(2, 5));
V = Z.polytope()
It seems that after going to the line 193 here https://github.com/TUMcps/CORA/blob/master/contSet/%40zonotope/polytope.m, the execution halts at the line 73 here https://github.com/TUMcps/CORA/blob/master/contSet/%40mptPolytope/mptPolytope.m, trying to call the same polytope.m one more time, but now with incorrect parameters. Trying to force it to call this guy https://github.com/TUMcps/CORA/blob/master/contSet/%40mptPolytope/polytope.m does not fix the issue.
error message:
Check for missing argument or incorrect argument data type in call to function 'mptPolytope_polytope'.
Error in mptPolytope (line 82)
obj.P=mptPolytope_polytope(varargin{1},varargin{2});
Error in zonotope/polytope (line 193)
P = mptPolytope(C,d);
Error in try1 (line 21)
V = Z.polytope()
Hello,
When removing indepent generators to depedent ones for the minkswoksi difference of constrained polynomial zonotopes, the constrained matrix A is keep the same size while transferring independant generators as dependant one. A size should be updated to the new dependant generators size :
(Auxilary function removeIndepGens(cPZ) in minkdiff for class conPolyZono, line 122-124)
from:
cPZ = conPolyZono(cPZ.c,[cPZ.G,cPZ.Grest], ...
blkdiag(cPZ.expMat,E), cPZ.A, cPZ.b, ...
blkdiag(cPZ.expMat_,E),[],id);
to:
cPZ = conPolyZono(cPZ.c,[cPZ.G,cPZ.Grest], ...
blkdiag(cPZ.expMat,E), [cPZ.A zeros(size(cPZ.Grest))], cPZ.b, ...
blkdiag(cPZ.expMat_,E),[],id);
Run the following code:
int1 = interval([-1.4897; -0.3403], [ -0.6545; 0.3403]);
int2 = interval([-1.5; -0.1], [-0.5; 0.1]);
isIntersecting(int1, int2)
I get:
isIntersecting(int1, int2)
ans =
0
However, as we know, the two intervals are intersected. Plot them we will see.
plot(int1); hold on; plot(int2, [1,2], 'r');
PS. Thinkpad E480, Windows 10, Matlab R2020b, Cora2020.
The following nonlinear reachability computation creates an empty interval (which then triggers bug #6 ):
>> Nonlinear_tank
Left limit larger than right limit
Error using +
Matrix dimensions must agree.
Error in + (line 56)
res.inf = res.inf + summand.inf;
Error in tie (line 63)
obj.taylor.F=Asum+obj.taylor.error;
Error in linearSys/initReach (line 41)
obj = tie(obj,options);
Error in linReach (line 58)
R = initReach(linSys,Rdelta,linOptions);
Error in nonlinearSys/initReach (line 58)
[Rti,Rtp,nr,perfInd] = linReach(obj,options,Rinit{iIteration},recur);
Error in nonlinearSys/post (line 36)
[Rnext,options] = initReach(obj,R.tp,options);
Error in contDynamics/reach (line 127)
[Rnext,options]=post(obj,Rnext,options);
Error in Nonlinear_tank (line 47)
Rcont = reach(tank, options);
Hi,
I used the previous version (2022) on MATLAB and lately switched to the latest version that was updated this year. And I noticed some functions, e.g., /contSet/@zonotope/sampleBox.m, are removed in the new packages. My previous development was based on some of the removed functions. I would much appreciate it if you could point me to the alternative functions or possibly consider adding the deleted functions back.
Thanks,
Hi,
I have noticed that the reachable sets for outputs, which was present in the reach( ) for continuous Dynamics in CORA18 are absent in the CORA20 version. I found the use of outputSet( ) in only the Linear discrete system reach( )
Has there been a change in way the reach( ) handles outputs between CORA'18 to CORA'20?
Could you maybe provide a minimal example of how to invoke output reachable sets in cont. dynamics using a linearsys obj?
I have attached a couple screenshots for your reference on this issue.
Kind regards,
Anurag Mohapatra
Getting an error while calling functions from configfiles.
Error: Check for incorrect argument data type or missing argument in call to function 'config_linearSys_reach'.
I am calling config_linearSys_reach(sys, params, options) and getting the above error.
Here, sys is 'linearSys' object, params is 'struct' and options is also 'struct'.
Hello,
The manual says params.R0 can be any set representation in section 'Basic Set Representations', but I'm having trouble on computing the reachable sets of discrete-time nonlinear system with initial set as constrained zonotope or zonotope bundle. Could you please provide a simple example script on how this can be done with CORA? Thanks!
CORA/contSet/@zonotope/volume.m
Line 83 in f4e6749
index slice is [end-n-r+1, end], but r is binary here. Is r supposed to be the rank of the generators?
Hi,
I have a nonlinear ODE system with 8 states. When i try running CORA I receive this error:
Warning: Check computation for order of abstraction error
Warning: The analysis is aborted because the time step size converges to 0.
The reachable sets until t = 1.4257e-17 are returned.
Are there ways to fix this while keeping the ODEs nonlinear? Or is this a limitation of MATLAB itself?
There is a typo in line 60 of reachset/find.m, it should be:
val = interval(val);
instead of
val = interal(time);
While trying to run my model, which is related to the non-linear uncertain parameter , using the example from nonlinParamSys. I run into an error which shows - "@parametricDynamicFIile*" not present. For the examples present these "parametricDynamicFile" are present in the auxiliary folder while for my test models these file are not created.
the output equation of a linearSysDT is y[i] = Cx[i] + Du[i], i.e., the indices of x and u are the same
The current implementation of @linearSysDT/reach.m in line 66, however, results in y[i-1] = Cx[i] + Du[i-1], i.e., the indices of x and u are different.
Hi,
I'm trying to calculate the inner approximation of the solution of a linParamSys problem (an interval matrix). Unfortunately, if I'm right, the reachInner operation is not supported for this system.
I wanted to ask you if there is any suggestion for working out such an issue.
Many thanks for considering my request,
Daniel
In my model I am using "nonlinParamSys" to compute the reachability of my uncertain parameter system.
My model with uncertain parameter is:
dx(1,1)= u(1)*p(3) + (x(2) - x(1)).*p(1).*p(3) ;
dx(2,1)= (28 - x(2))*p(2).*p(4) - (x(2) - x(1))*p(1).*p(4) ;
The error is I am getting is shown in the attached figure:
I think the error might be due to inaccurate computation of Jacobians, as the Jocabians files created have all 0 elements.
How can I fix it?
Im trying to run reach on a nonlinear hybrid automaton, but i receive a matrix dimension error in the abstractionError_adaptive function.
My code:
% Dynamics
pke = nonlinearSys(@pke,4,0);
% Invariant set
inv = polytope([-1,0,0,0; 0,-1,0,0; 0,0,-1,0; 0,0,0,-1],[0;0;0;-1]); % n>=0, C1>=0, Trx>=0, rhoc>=-1
%%
% Locations/ nodes
guard1 = conHyperplane([0,0,-1,0],675); % transition to 2 when Trx >= 675
reset1.f = @(x,u)([x(1); x(2); x(3); 0.66 + 1.2*(675-x(3))]);
trans1 = transition(guard1,reset1,2); % --> next loc: 2
loc(1) = location('startup',inv,trans1,pke); % startup
guard2 = conHyperplane([0,0,-1,0],810); % transition to 3 when Trx >= 1.2*675
reset2.f = @(x,u)([x(1); x(2); x(3); -1]);
trans2 = transition(guard2,reset2,3); % --> next loc: 3
loc(2) = location('steadystate',inv,trans2,pke); % steady state
guard3 = conHyperplane([0,0,1,0],650); % transition to 1 when Trx <= 650
reset3.f = @(x,u)([x(1); x(2); x(3); 0.7]);
trans3 = transition(guard3,reset3,1); % --> next loc: 1
loc(3) = location('scram',inv,trans3,pke); % SCRAM
HA = hybridAutomaton(loc);
%% Reachability
clc
% Parameters --------------------------------------------------------------
params.tFinal = 400;
params.R0 = zonotope([[0; 0.0012; 650; 0.7], diag([0,0,0,0])]);
params.startLoc = 1;
parama.U = zonotope(0,0);
% Reachability Settings ---------------------------------------------------
options.timeStep = 1;
options.taylorTerms = 10;
options.zonotopeOrder = 50;
options.alg = 'lin-adaptive';
options.tensorOrder = 2;
options.lagrangeRem.simplify = 'simplify';
% settings for hybrid systems
options.guardIntersect = ['polytope'];
options.enclose = {'box'};
% Reachability Analysis ---------------------------------------------------
tic
R = reach(HA, params, options);
tComp = toc;
disp(['computation time of reachable set: ',num2str(tComp)]);
The error:
Error using *
Incorrect dimensions for matrix multiplication. Check that the number of columns in the first matrix matches the number of rows in the second matrix. To perform elementwise
multiplication, use '.*'.
Error in abstractionError_adaptive (line 101)
err(i,1) = 0.5 * dz' * options.hessianConst{i} * dz;
Error in nonlinearSys/linReach_adaptive>aux_initStepTensorOrder (line 419)
[~,~,L0_2,options] = abstractionError_adaptive(obj,options,Rdelta);
Error in nonlinearSys/linReach_adaptive (line 98)
options = aux_initStepTensorOrder(obj,options,Rstart);
Error in nonlinearSys/reach_adaptive (line 85)
[Rnext.ti,Rnext.tp,options] = linReach_adaptive(obj,options,options.R);
Error in contDynamics/reach (line 68)
[timeInt,timePoint,res,~,options] = reach_adaptive(obj,params,options);
Error in location/reach (line 56)
R = reach(loc.contDynamics,params,options_,spec);
Error in hybridAutomaton/reach (line 136)
[Rtemp,Rjump,res] = reach(HA.location(locID),R0,tStart,options);
Error in reactor_HA (line 53)
R = reach(HA, params, options);
Related documentation
The returned variable "res" in mergeTransitionSets is not initialized outside the for-loop in line 48 which is based on the length of the transition sets. If, at one point within execution, all components reach states which have no transitions, "res" is never initialized which leads to a run-time error.
Concrete evaluation of neuralNetworkOld and overapproximate evaluation with zonotopes gives wrong results.
The execution of the following code:
net = neuralnetwork2cora('./networks/CAS/ACASXU_experimental_v2a_1_8.nnet');
[in_spec, out_spec] = vnnlib2cora('./vnncomp2022_benchmarks/benchmarks/acasxu/vnnlib/prop_3.vnnlib');
z = zonotope(in_spec{1});
interval(net.evaluate(z))produced the output
ans =
[0.0000, 0.0000]
[0.0000, 0.0000]
[0.0000, 0.0000]
[0.0000, 0.0000]
[0.0000, 0.0000]The concrete evaluation also results in
>> net.evaluate(in_spec{1}.inf)
ans =
0
0
0
0
0However, evaluating the same .nnet network in a different program or loading the corresponding .onnx network in CORA results in the output of
>> acas = neuralNetwork.readONNXNetwork('./vnncomp2022_benchmarks/benchmarks/acasxu/onnx/ACASXU_run2a_1_8_batch_2000.onnx', true, 'BSSC', 'BC');
>> acas.evaluate(in_spec{1}.inf)
ans =
5×1 single column vector
-0.0203
-0.0191
-0.0191
-0.0180
-0.0180The .nnet networks are available in this repo, while the .onnx networks and .vnnlib specifications are available in this repo.
Below is the error, it is calling the wrong split. A workaround is to remove CORA from path and start the profile viewer and then add CORA back to path 😞 . And I am using 2018, Cheers!
Error in split (line 30)
inf = input.inf;
Error in matlab.internal.cef.webwindowmanager/buildDefaultStartupOptions (line 129)
versionInfo = split(info.Version);
Error in matlab.internal.cef.webwindow (line 306)
windowMgr.buildDefaultStartupOptions(obj.BrowserMode)
Error in matlab.internal.webwindow/createImplementation (line 295)
implObj = matlab.internal.cef.webwindow(varargin{:});
Error in matlab.internal.webwindow (line 147)
obj.impl = obj.createImplementation(varargin{:});
Error in matlab.internal.profileviewer.BrowserService/getProfileViewerWindow
Error in matlab.internal.profileviewer.ProfileViewerService/showProfileViewerWindow
Error in matlab.internal.profileviewer.ProfileViewerService/startService
Error in matlab.internal.profileviewer.invokeProfiler
Error in profile (line 200)
matlab.internal.profileviewer.invokeProfiler;
Undefined function 'polytope' for input arguments of type 'double'.
Error in mptPolytope (line 61)
obj.P=polytope(varargin{1},varargin{2});
Error in zonotope/polytope (line 101)
P=mptPolytope([C;-C],[dPos;dNeg]);
Error in zonotopeBundle/polytope (line 34)
Ptmp{i}=polytope(Zbundle.Z{i},varargin{2:end});
Error in deleteRedundantSets (line 54)
R.P{i}=polytope(R.tp{i}.set,options);
Error in nonlinearSys/post (line 47)
Rnext = deleteRedundantSets(Rnext,R,options);
Error in contDynamics/reach (line 127)
[Rnext,options]=post(obj,Rnext,options);
Error in example_nonlinear_reach_03_vanDerPol (line 80)
Rcont = reach(vanderPol, options);
I was facing the following error from reach() while trying to check a safeSet specification that I made using interval objects.
Check for missing argument or incorrect argument data
type in call to function 'polytope'.Error in mptPolytope (line 73)
obj.P=polytope(varargin{1},varargin{2});Error in interval/mptPolytope (line 41)
poly = mptPolytope(C,d);Error in interval/in (line 53)
res = in(mptPolytope(obj1),obj2);Error in specification/check>checkSafeSet (line 88)
res = in(set,S);Error in specification/check (line 43)
res = checkSafeSet(obj(i,1).set,S);Error in linearSysDT/reach (line 87)
if ~check(spec,Rout{i})Error in reachabilityAnalysis (line 81)
[R,res] = reach(sys,params,options,spec);
Am I missing something here?
If not entirely wrong, I am guessing this happens because the mptPolytope function under interval set representation takes only an interval object as input. But the polytope function under interval on the other hand converts the input interval objects into a generic polytope-like representation and then calls mptPolytope function internally with this object (which does not take polytope type input but interval type objects as input), which might cause this error.
The following sample code from CORA 2020 manual also throws a similar error.
% set S (intersection)
S1 = mptPolytope(...
[-1 -1;0 -1;0 1;1 1], ...
[-0.5; 0; 2; 2.5]);
S2 = mptPolytope(...
[-1 -1;0 -1;0 1;1 1], ...
[2.5; 2; 0; -0.5]);
S = S1 & S2;
% check if set is empty
res = isempty(S)
Check for missing argument or incorrect argument data
type in call to function 'polytope'.Error in mptPolytope (line 73)
obj.P=polytope(varargin{1},varargin{2});
Please guide. Thank you.
I received an error stating 'Tuning error...report to devs' when i ran my code.
% Parameters --------------------------------------------------------------
params.tFinal = 400;
params.R0 = zonotope([[0; 0.0124; 650], diag([0.001,0.001,1])]);
params.U = zonotope([0.66]);
% Reachability Settings ---------------------------------------------------
options.timeStep = 1;
options.taylorTerms = 4;
options.zonotopeOrder = 50;
options.alg = 'lin-adaptive';
options.tensorOrder = 2;
options.lagrangeRem.simplify = 'simplify';
% System Dynamics ---------------------------------------------------------
reactor = nonlinearSys(@pke);
% Reachability Analysis ---------------------------------------------------
tic
R = reach(reactor, params, options);
tComp = toc;
disp(['computation time of reachable set: ',num2str(tComp)]);
% Simulation --------------------------------------------------------------
tic
simOpt.points = 10;
simRes = simulateRandom(reactor, params, simOpt);
tComp = toc;
disp(['computation time of simulation: ',num2str(tComp)]);
%% Visualization -----------------------------------------------------------
tic
figure(1)
hold on; box on;
% plot reachable sets
useCORAcolors("CORA:contDynamics")
plotOverTime(R,1,'DisplayName','Reachable set');
% plot initial set
plotOverTime(R.R0,1, 'DisplayName','Initial set');
% plot simulation results
plotOverTime(simRes,1,'DisplayName','Simulations');
sgtitle('n vs time')
toc
Error message:
Error using nonlinearSys/linReach_adaptive (line 76)
Tuning error.. report to devs
Error in nonlinearSys/reach_adaptive (line 85)
[Rnext.ti,Rnext.tp,options] = linReach_adaptive(obj,options,options.R);
Error in contDynamics/reach (line 68)
[timeInt,timePoint,res,~,options] = reach_adaptive(obj,params,options);
Error in reactor_nl (line 31)
R = reach(reactor, params, options);
I created a linear hybrid automaton for my system. But when I try to run reach i receive this error
Array indices must be positive integers or logical values.
Error in reach_adaptive>aux_ebar (line 1430)
ebarredt_max = ebar.red_e(t_idx-1) + ...
Error in reach_adaptive (line 149)
ebar = aux_ebar(t,k,e,ebar,timeStep,options.tFinal);
Error in linearSys/reach (line 83)
[timeInt,timePoint,res] = reach_adaptive(obj, options);
Error in location/reach (line 56)
R = reach(loc.contDynamics,params,options_,spec);
Error in hybridAutomaton/reach (line 136)
[Rtemp,Rjump,res] = reach(HA.location(locID),R0,tStart,options);
Error in reactor_linear_hybrid_automaton (line 202)
R = reach(HA, params, options);
I have attached my .m file here. This error has not happened in the past when i created other automatons.
reduce method in polyZonotope
line 37: N = size(pZ.G,1);
Is N here the dimension of the polynomial zonotope? I found some cases in my program that pZ.G might be empty and N becomes 0 incorrectly. Maybe using the center of the polynomial zonotope (N = length(pZ.c);) might be more reasonable and robust?
The "deleteAligned" function sometimes causes under-approximation like this in a 4-dimensional zonotope.
This figure is an example of two states in a four-dimensional system. The blue is the original zonotope and the red is the zonotope after the "deleteAligned" function works.
Could this function not work well in higher-order systems? Or is there something I overlooked??
Hi,
I tried overapproximating an ONNX network using polynomial zonotopes.
Execution of the following code:
>> acas = neuralNetwork.readONNXNetwork('./vnncomp2022_benchmarks/benchmarks/acasxu/onnx/ACASXU_run2a_1_1_batch_2000.onnx', true, 'BSSC', 'BC');
>> [in_spec, out_spec] = vnnlib2cora('./vnncomp2022_benchmarks/benchmarks/acasxu/vnnlib/prop_3.vnnlib');
>> pz = polyZonotope(in_spec{1})
>> acas.evaluate(pz)resulted in the error shown below:
Error using inputArgsCheck
Wrong value for the first input argument.
The right value: double (finite)
Type 'help polyZonotope' for more information.
Error in polyZonotope>aux_checkInputArgs (line 142)
inputArgsCheck({ ...
Error in polyZonotope (line 79)
aux_checkInputArgs(c,G,Grest,expMat,id,nargin);
Error in nnHelper.compBoundsPolyZono (line 37)
pZ = polyZonotope(c, G, Grest, E);
Error in nnLeakyReLULayer/evaluatePolyZonotopeNeuronLin (line 114)
[l, u] = nnHelper.compBoundsPolyZono(c, G, Grest, E, ind, ind_, approx);
Error in nnActivationLayer/evaluatePolyZonotopeLin (line 39)
obj.evaluatePolyZonotopeNeuronLin(c(j), G(j, :), Grest(j, :), expMat, ind, ind_, evParams.bound_approx);
Error in nnActivationLayer/evaluatePolyZonotope (line 29)
[c, G, Grest, expMat, id, id_, ind, ind_] = evaluatePolyZonotopeLin(obj, c, G, Grest, expMat, id, id_, ind, ind_, evParams);
Error in neuralNetwork/evaluate (line 97)
layer_i.evaluatePolyZonotope(c, G, Grest, expMat, id, id_, ind, ind_, evParams);
The onnx network and vnnlib specification are available at this repo.
When performing the operation Z-E with the zonotopes Z and E (see attachment), CORA returns an empty set in version 2020 and the correct/expected set in version 2018.
When calling 'split' for char arrays in MATLAB, '/global/functions/globOptimization/split.m' is invoked instead. Please avoid same function names
In the "linearize.m" file, you wrote in a comment: "% linearize - linearizes the nonlinear system; linearization error is not included yet".
But at the end of the file, you reference the linearization error using " [dA,dB] = lin_error2dAB(options.Ronestep,options.U,obj.hessian,p)"
I am a bit lost, is it possible to access all the linearization errors for a Ronestep?
Thank you in advance.
Calling vnnlib2cora('./vnncomp2022_benchmarks/benchmarks/rl_benchmarks/vnnlib/dubinsrejoin_case_unsafe_11.vnnlib') fails with the following error message:
Output argument "len" (and possibly others) not assigned a value in the execution with "vnnlib2cora>parseAssert" function.
Error in vnnlib2cora>parseAssert (line 109)
[len_,data_] = parseAssert(text,data_);
Error in vnnlib2cora (line 54)
[len,data] = parseAssert(text,data);The reason seems to be that while loop in line 102 is also executed for empty text (since it doesn't start with ')').
The .vnnlib specifications are available in this repo.
I am trying to plot the flowpipe over time for a discrete linear system. But it seems the plotOverTime and plotAllOverTime, both are using timeInterval field in a reachset object nad because the reachSet objects for a linearSysDT type objects do not contain timeInterval field. So I am facing error whenever trying to plot the reachsets over time. Am I missing something here? Or there is some issue regarding this? Please help.
plotOverTime(R,[1 2],'FaceColor',[.8 .8 .8],'EdgeColor','b');
Dot indexing is not supported for variables of
this type.Error in reachSet/plotOverTime (line 83)
for j =
1:length(R(i,1).timeInterval.set)
Does CORA allow us to write if-then statements as guard conditions? For example, for a control system the guard condition might be "if a control signal is sent to deactivate the system, then reset and update the system parameters to shut it down".
I'm not sure if the above statement can be written in CORA using set representations.
The handling of empty intervals does not work for nonscalar values.
>> interval([1 2], [3 4]) + interval([4 3], [2 1])
Left limit larger than right limit
Error using +
Matrix dimensions must agree.
Error in + (line 56)
res.inf = res.inf + summand.inf;
(I guess that the interval constructor should error if left limit > right limit.)
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.