Schedulers + Property: P_UNRC + State: (Cor.location = loc_1, unrc = False, sad = False) Choice: safe + Property: P_Sad + State: (Cor.location = loc_1, unrc = False, sad = False) Choice: risk + State: (Cor.location = loc_5, unrc = False, sad = False) Choice: τ + Property: R_MinCostToUNRC + State: (Cor.location = loc_1, unrc = False, sad = False) Choice: safe