S-FOCUS

S-FOCUS

FLOW: (x_1',x_2')=(-x_1-x_2,x_1-x_2)
Empty jump relation
Init: 2.5 <= x₁ <= 3/\x₂=0
Unsafe: x₁>3 \/x₂>3
The state space: [0,4]×[0,4]

Input file

S-FOCUS