4253#line 2521 "Elevator.c"
4254 retValue_acc = isFloorCalling(executiveFloor);
4255 }
4256#line 2523
4257 return (retValue_acc);
4258#line 2530
4259 return (retValue_acc);
4260}
4261}
4262#line 429 "Elevator.c"
4263int isExecutiveFloor(int floorID )
4264{ int retValue_acc ;
4265
4266 {
4267#line 2552 "Elevator.c"
4268 retValue_acc = executiveFloor == floorID;
4269#line 2554
4270 return (retValue_acc);
4271#line 2561
4272 return (retValue_acc);
4273}
4274}
4275#line 1 "wsllib_check.o"
4276#pragma merger(0,"wsllib_check.i","")
4277#line 3 "wsllib_check.c"
4278void __automaton_fail(void)
4279{
4280
4281 {
4282 goto ERROR;
4283 ERROR: ;
4284#line 53 "wsllib_check.c"
4285 return;
4286}
4287}
4288#line 1 "UnitTests.o"
4289#pragma merger(0,"UnitTests.i","")
4290#line 24 "UnitTests.c"
4291void spec1(void)
4292{ int tmp ;
4293 int tmp___0 ;