Project

General

Profile

Revision ffe46d5f

View differences:

tests/cocospec/regulator_12B_Spec.lus
61 61

  
62 62

  
63 63

  
64
contract RegulatorSpec()
64
(*@ contract RegulatorSpec(pom:bool)
65 65
returns (lcvdt_cmd_fcs_dps2 : real;
66 66
	mcvdt_cmd_fcs_dps2 : real;
67 67
	ncvdt_cmd_fcs_dps2 : real;
......
117 117
	guarantee "REG003" S( ((count_yaw_output_exceeding_50 <= 100) and FTP), (count_yaw_output_exceeding_50 <= 100) );
118 118

  
119 119
tel
120
*)

Also available in: Unified diff