Invariant is not able to stop the reachable set!

[ArsalMu]

Hi,
I am doing some reachability analysis on a hybrid automaton of my system using CORA. But the thing is that I am not able to simulate just 4 states. It is because the invariant set does not limit the state variables from going out.
MATLAB version is latest so does with CORA
Here are some settings:
params.tFinal = 100;
params.R0 = zonotope(interval([0; 2; 0; 0],[0;2;0;0]));
params.startLoc = 3; % initial location

% Reachability Settings ---------------------------------------------------

% algorithm options
options.timeStep = 0.1;

options.zonotopeOrder = 20;
options.taylorTerms = 10;

options.intermediateOrder = 2;
options.errorOrder = 5;

options.tensorOrder = 2;
options.alg = 'lin';

% guard intersection method
options.guardOrder=4;
options.guardIntersect = 'conZonotope';
options.enclose = {'box'};

%invariants are like this------------------
inv = interval([0;2.55;-10;0],[40;3.5;50;0]);

[toladnertum]

Dear @ArsalMu,

Please provide a full example such that we can run the code to reproduce the bug.

Best,
Tobias

[toladnertum]

Unfortunately, there are some syntax issue in the code. For example, the second line in f2 is not valid matlab syntax

0.53.14r^3V(dd)^21.2251.49(-0.0029+0.0132x(2)r/V(dd)+0.00219x(1)-0.000979x(2)x(2)rr/V(dd)/V(dd)-0.0003232x(1)*x(2)r/V(dd)-0.000066x(1)*x(1))/j;

In particular, this 0.53.14r (two decimal points, multiplicatation without *) is not valid.

[ArsalMu]

I think there is some problem with pasting the code.
Let me upload the file

[ArsalMu]

myp2L3.txt

[ArsalMu]

It'll definitely work. And You may see the issues.

[ArsalMu]

Dear @toladnertum ,
Are you able to reproduce the issue?

[wetzlingerm]

Can you tell us exactly how the computed behavior (as plotted at the end of the script) differs from the behavior you expect? In particular, do you expect that the reachable set should not enter the region x_1 <= 0?

[ArsalMu]

Yes @wetzlingerm. In the state L3 the invariant for x(2) is 0.9148 to 2.58. So it should not exceed this limit. Along with that, there is a guard at 2.58 there, too. It must make a transition instead of staying in L3 and breaking the limits.

[wetzlingerm]

CORA implements transitions in hybrid systems reachability as follows:

1. The reachable set must entirely leave the invariant, which stops the reachability analysis in the current location.
2. All computed reachable sets are checked for intersection with the guard set (in fact, with all guard sets).
3. The intersections are mapped by the reset function associated with each guard set.
4. The mapped intersections constitute the initial sets for the reachability analysis in the next location.

In your case, the reachable set does not entirely leave the invariant of location 3, as the last time-point reachable set R.timePoint.set{end} has its minimum in the x_2 direction at 2.4734, which is still within the bounds of the invariant. Since the reachable intersects the unsafe set, the analysis aborts prematurely.

We are currently working on our v2025 version, which will be released in one or two weeks. We'll integrate a fix for this issue.

[ArsalMu]

Hi @wetzlingerm,
I don't know but I think the issue is till there in 2025 Version. Maybe I am wrong but for me the issue is still there. LEt me know if you can help.

Thanks in advance.

[wetzlingerm]

Your specific issue was addressed in @location/reach in the helper function aux_adaptSpecs, as tested by test_hybridAutomaton_reach_unsafeSet.

If you have further questions about your example, please let us know the exact error message and we'll be happy to help you out!

[ArsalMu]

The example I posted, still going to the unsafe set prematurely. It is still in the comments. You may check. It would be great if I might be able to know the issue.

[TUMcps]

Dear @ArsalMu,

Are you still having this issue? If so, please try again using the latest CORA version (v2025.1.0).