% Adaptive flight control system: Example from my AIAA paper. % template: -we^2 - b*intwe^2 -c*(L-optL)^2 is a Lyapunov fn. % We fail on this; see adaptive-simpl for what we can do. on echo; load_package redlog; rlset r; load_package qepcad; on rlqefbqepcad; % use QEPCAD as the fallback QE rlqepcadn(100*10^6); % The number of cells used by QEPCAD. The % default is (only) 1 * 10^6. rlqepcadl(200*10^3); % The size of the prime list used by QEPCAD. The % default is (only) 2 * 10^3. on rlverbose; on time; off rlqefb; % No fallback QE phi := ( e > 0 AND d > 0 AND a > 0 AND ((intwe*intwe <= e AND optL*optL*beta*beta - 2*optL*L*beta*beta + L*L*beta*beta <= d AND we*we >= a) impl ( -2*intwe*we*b + 20*intwe*we - 2000*intwe*optL*beta*c + 2000*intwe*L*beta*c + 10*we*we - 4400*we*optL*beta*c + 2*we*optL*beta + 4400*we*L*beta*c - 2*we*L*beta > 0))); psi := rlgqe( all({intwe, we, L, optL, beta}, phi ) ); psi1 := second psi; psi2 := rlqepcad( rlex(psi1), "adaptive.qepcad" ); %psi2 := rlqepcad( psi ); off nat; % Output same syntax as input (for reduce) out "adaptive.out"; psi; psi2; shut "adaptive.out"; end; % suppose a = 1, e = 1, d = 1; % suppose b = 10 % redlog takes a long time on this one; % but qepcad immmediately gives % [ [ 800 c + 1 > 0 /\ 4400 c - 7 <= 0 ] \/ [ 1600 c - 3 < 0 /\ 4400 c - 7 >= 0 ] ]