FOCUS

FOCUS

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

Input file

FOCUS