235void bigMacCall(void) ;
236#line 3
237void angelinaCall(void) ;
238#line 4
239void cleanup(void) ;
240#line 1 "scenario.c"
241void test(void)
242{
243
244 {
245 {
246#line 2
247 bigMacCall();
248#line 3
249 angelinaCall();
250#line 4
251 cleanup();
252 }
253#line 55 "scenario.c"
254 return;
255}
256}
257#line 1 "wsllib_check.o"
258#pragma merger(0,"wsllib_check.i","")
259#line 3 "wsllib_check.c"
260void __automaton_fail(void)
261{
262
263 {
264 goto ERROR;
265 ERROR: ;
266#line 53 "wsllib_check.c"
267 return;
268}
269}
270#line 1 "Elevator.o"
271#pragma merger(0,"Elevator.i","")
272#line 359 "/usr/include/stdio.h"
273extern int printf(char const * __restrict __format , ...) ;
274#line 16 "Person.h"
275void enterElevator(int p ) ;