module checkInconcOrFailSetverdictPrecededByLog { testcase t_sendMsg() runs on myComponent { p1.send(msg_a); // this is as expected alt { [] p2.receive(msg_b) { someOtherfunction(); log("*** t_sendMsg: INFO: Wrong message has been received ***") setverdict(fail); someOtherfunction(); } [] p2.receive(msg_c) { setverdict(pass); } [] p2.receive { log("*** t_sendMsg: INFO: Unexpected message, possibly malicious ***"); setverdict(inconc); } } // here, the log statements are missing alt { [] p2.receive(msg_b) { setverdict(fail); } [] p2.receive(msg_c) { setverdict(pass); } [] p2.receive { setverdict(inconc); } } } }