Project

General

Profile

Revision 6ccfcb12 tests/cocospec/integrator_12BWithoutModesAndInitialization.lus

View differences:

tests/cocospec/integrator_12BWithoutModesAndInitialization.lus
77 77
guarantee "TUI-001" S((( BL <= ic and ic <= TL ) and reset) => (yout = ic) , (((( BL <= ic and ic <= TL ) and reset) => (yout = ic)) and FTP));
78 78

  
79 79
guarantee "TUI-003-V2" normal and ((normal_yout <= TL and normal_yout >= BL)) => yout = normal_yout;
80
--guarantee "TUI-003" true -> (H(((( not normal) and (pre ( normal ))) and ( not FTP)) => (pre (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) ))))) and ((S( (( not (( not normal) and (pre ( normal )))) and (normal and (FTP or (pre (  not normal ))))), ( not (( not normal) and (pre ( normal )))) )) => (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) )));
80
guarantee "TUI-003" true -> (H(((( not normal) and (pre ( normal ))) and ( not FTP)) => (pre (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) ))))) and ((S( (( not (( not normal) and (pre ( normal )))) and (normal and (FTP or (pre (  not normal ))))), ( not (( not normal) and (pre ( normal )))) )) => (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) )));
81 81

  
82 82

  
83 83
tel

Also available in: Unified diff