%% Redlog file for LCR relational abstraction. %% 2-d system with dynamics: %% switch open mode: %% d Vc/dt = 5-Vc-Vl, d Vl/dt = -5 + Vc - Vl %% Switch closed mode: %% d Vc/dt = 5 - 3 Vc - Vl; d Vl/dt = -5 + 3 Vc - Vl %% Can we synthesize a relational invariant for this. %% Template: %% Vcinit+a*Vlinit >= b => b <= Vc + a*Vl <= Vcinit + a*Vlinit %% Vcinit+a*Vlinit <= b => b >= Vc + a*Vl >= Vcinit + a*Vlinit %% Vcinit+a*Vlinit >= 0 => Vc + a*Vl >= Vcinit + a*Vlinit %% Vcinit+a*Vlinit <= 0 => Vc + a*Vl <= Vcinit + a*Vlinit on echo; load_package redlog; rlset r; load_package qepcad; on rlqefbqepcad; rlqepcadn(100*10^6); rlqepcadl(200*10^3); on rlverbose; on time; %off rlqefb; %% Vcinit+a*Vlinit >= b => b <= Vc + a*Vl <= Vcinit + a*Vlinit phi1 := ( Vcinit + a*Vlinit >= b and b = Vc + a*Vl impl (5-Vc-Vl) + a*(-5+Vc-Vl) >= 0 ); phi2 := ( Vcinit + a*Vlinit >= b and Vc + a*Vl = Vcinit + a*Vlinit impl (5-Vc-Vl) + a*(-5+Vc-Vl) <= 0 ); % Result: THere is no invariant of this form. Because there is no negative real eigenvalue. %% Vcinit+a*Vlinit >= 0 => Vc + a*Vl >= Vcinit + a*Vlinit phi1 := ( Vcinit + a*Vlinit >= b and Vc + a*Vl = Vcinit + a*Vlinit impl (5-Vc-Vl) + a*(-5+Vc-Vl) >= 0 ); % Result: Also false. No invariant of this form either. % Same result also when >= b is replaced by <= b. %% a*(Vc-Vcinit) + b*(Vl-Vlinit) >= c and d*(Vc-Vcinit) + e*(Vl-Vlinit) >= f phi1 := ( a*(Vc-Vcinit) + b*(Vl-Vlinit) >= c and d*(Vc-Vcinit) + e*(Vl-Vlinit) = f impl d*(5-Vc-Vl) + e*(-5+Vc-Vl) >= 0 ); phi2 := ( a*(Vc-Vcinit) + b*(Vl-Vlinit) = c and d*(Vc-Vcinit) + e*(Vl-Vlinit) >= f impl a*(5-Vc-Vl) + b*(-5+Vc-Vl) >= 0 ); % b = -1, e = 1, a = -d, e c > b f...i.e. c + f > 0 % c = 1, f = 1, a = % No interesting solution here too.... phi1 := ( (Vc-5)^2 + a*Vl^2 = (Vcinit-5)^2 + a*Vlinit^2 impl (Vc-5)*(5-Vc-Vl) + a*Vl*(-5+Vc-Vl) <= 0 ); % Result: a = 1 or any a between 3-2\sqrt{2} and 3+2\sqrt{2} % Template: Vc remains inside (Vcinit+-d) if Vlinit < e phi1 := ( -e <= Vl and Vl <= e and Vc-5 = d impl (5-Vc-Vl) <= 0 ); phi2 := ( -e <= Vl and Vl <= e and Vc-5 = -d impl (5-Vc-Vl) >= 0 ); phi3 := ( -e = Vl and -d <= Vc-5 and Vc-5 <= d impl (-5+Vc-Vl) >= 0 ); phi4 := ( e = Vl and -d <= Vc-5 and Vc-5 <= d impl (-5+Vc-Vl) <= 0 ); % Answer: d = e. % Therefore, invariant is % |Vl|, |Vc-5| <= MAX( |Vlinit|, |Vcinit-5| ) phi := phi1 and phi2 and phi3 and phi4; phi := all({Vc,Vl,Vcinit,Vlinit}, phi); psi := rlqe(phi); rlqepcad( rlex(psi), "lcr.qepcad"); end;