S-FOCUSTopNAVIGATIONREAL-EIGEN

REAL-EIGEN

A linear, three-dimensional example.


Flow: (x1',x2',x3')=(0.80x2+0.6x3-1.8,0.8x1+0.7x3-15.2,0.6x1+0.7x2-1.8)
Empty jump relation
Init: 19 <= x1 <= 20/\19 <= x2 <= 20 /\19 <= x3 <= 20
Unsafe: x1 <= 21/\x2 <= 20/\x3 >= 22.5
The state space: [15,24]×[15,24] ×[15,24]

Input file


S-FOCUSTopNAVIGATIONREAL-EIGEN