specification EXPERIMENT_01 [OPEN, CLOSE] : noexit behaviour hide PRED1, SUCC1, PRED2, SUCC2, PRED3, SUCC3 in library NETWORK_WITHOUT_CRASHES endlib where library DATA, LINK_1, BASIC_STATION endlib endspec