module checkNoLabelsOrGotoStatements {
	testcase tc1() runs on mtcType system systemType {
		label TC_START;
		
		alt{
			[] p1.receive {
				label P1_RECEIVE;
				p1.send(integer:1);
				goto TC_END;
			}
			[] p2.receive {
				p1.send(integer:2);
				goto TC_START;
			}
		}
		
		label TC_END;
	}
}