A linear, three-dimensional model of a mutant of V. fischeri [1].

Let x1, x2 and x3 respectively represent the protein LuxI, the autoinducer Ai and the complex Co described in the original paper. The model has two modes with dynamics in the form x'=Ax+bi, i=1,2, where x=(x1,x2,x3)T and

A=[ -1/3600 0 0; 7.5e-5 -(1/36000+7.5e-9) 1.5e-9; 0 0.005 -1/3600-0.01]

and b1=(0.00375,0,0)T and b2=(3.75375,0,0)T.

We set the state space to be [0,30000]×[0,60000]×[0,30000] and the switches occur when the plane x3=1000 is reachable and x2 in [1000,45000]. We want to verify that x1 >= 27500\/x2 >= 50000\/x3 >= 25000 cannot be reachable when starting from [17500,20000]×[40000,45000]×[5000, 7500] in mode 1.

Input file