sort signal_colour = struct RD | GL | GR; %red, yellow, green train_general_position = struct before_track | on_track | after_track; point_position = struct left | right; driving_direction = struct L | R; %as the track can be viewed as an acyclic graph, it can be said to have a left side and right side route_status = struct requested | accepted | locked | ready | active | rejected; section_status = struct free | occupied | logically_occupied; %section status in view of the interlocking section_id = Nat; signal_id = Nat; train_id = Nat; point_id = Nat; section_info = struct section_info( status: section_status, on_border: Bool, %border/edge of the yard, connection to open track connections: List(section_connection) %connections to other sections ); signal_info = struct signal_info( colour: signal_colour, direction: driving_direction, virtual: Bool, %virtual signals can be used to set a route but are not a physical object section_before: section_id, section_after: section_id ); route_info = struct route_info( entry_signal: signal_id, exit_signal: signal_id, direction: driving_direction, sections_of_route: List(section_id), signals_of_route: List(signal_id), points_of_route: List(point_position_pair), protection: List(flank_protection), status: route_status ); flank_protection = struct flank_protection( for_section: section_id, flank_protection_points: List(point_position_pair), flank_protection_signals: List(signal_id) ); point_position_pair = struct point_position_pair( point: point_id, position: point_position ); point_info = struct point_info( in_section: section_id, position: point_position ); section_connection = struct section_connection( positions: List(point_position_pair), protection: flank_protection, left_section: section_id, right_section: section_id ); signal_pair = struct signal_pair( entry_signal: signal_id, exit_signal: signal_id ); signals = signal_id -> signal_info; sections = section_id -> section_info; points = point_id -> point_info; routing_table = List(signal_pair); %declarations and static positional calculations map efp: flank_protection; get_points_of_section: section_id#points -> List(point_id); get_points_of_section_iter: section_id#point_id#List(point_id)#points -> List(point_id); enumerate_point_position_pairs: List(point_id) -> List(List(point_position_pair)); enumerate_point_position_pairs_aux: List(point_id)#List(List(point_position_pair)) -> List(List(point_position_pair)); enumerate_point_position_pairs_aux_aux: point_id#List(List(point_position_pair))#List(List(point_position_pair)) -> List(List(point_position_pair)); legal_section: section_id -> Bool; legal_signal: signal_id -> Bool; legal_point: point_id -> Bool; in_front_of_signal: section_id#section_id#signals -> Bool; in_front_of_any_signal: section_id#section_id#signals -> Bool; get_signal_ahead: section_id#section_id#signals -> signal_id; get_signal_ahead_iter: section_id#section_id#signals#signal_id -> signal_id; expand_route: route_info#driving_direction#List(point_position_pair)#sections#signals#points -> List(route_info); expand_route_point_combinations: route_info#driving_direction#sections#signals#points -> List(route_info); expand_route_point_combinations_aux: route_info#driving_direction#sections#signals#points#List(List(point_position_pair))#List(route_info) -> List(route_info); find_route: signal_id#signal_id#sections#signals#points -> route_info; find_route_expand_options: signal_id#driving_direction#List(route_info)#List(route_info)#sections#signals#points -> route_info; find_route_check_done: signal_id#driving_direction#List(route_info)#List(route_info)#sections#signals#points -> route_info; get_right_section_connections: section_id#Set(point_position_pair)#Bool#List(section_connection) -> section_id; get_left_section_connections: section_id#Set(point_position_pair)#Bool#List(section_connection) -> section_id; check_equality_set: Set(point_position_pair)#Set(point_position_pair)#Bool -> Bool; get_next_section_static: section_id#section_id#driving_direction#List(point_position_pair)#Bool#sections -> section_id; get_flank_protection: section_id#section_id#List(point_position_pair)#sections -> flank_protection; get_flank_protection_aux: section_id#Set(point_position_pair)#List(section_connection) -> flank_protection; var se,se2,se3: section_id; si,si2: signal_id; p: point_id; pos: point_position; sc: section_connection; di: driving_direction; strict: Bool; sic: signals; sec: sections; poc: points; ro: route_info; flp: flank_protection; plist: List(point_id); ppp: point_position_pair; point_poss_todo: List(List(point_position_pair)); point_poss_done: List(List(point_position_pair)); point_poss: List(point_position_pair); point_poss_set, point_poss_set2: Set(point_position_pair); conns: List(section_connection); roo_todo: List(route_info); roo_done: List(route_info); eqn legal_point(p) = p >= first_point && p <= last_point; legal_section(se) = se >= first_section && se <= last_section; legal_signal(si) = si >= first_signal && si <= last_signal; efp = flank_protection(0,[],[]); get_points_of_section(se,poc) = if(last_point == 0, [],get_points_of_section_iter(se,first_point,[],poc)); %catch case without points get_points_of_section_iter(se,p,plist,poc) = %iterate over all points and add point to the list if it is in the given section if(p > last_point, plist, if(in_section(poc(p)) == se, get_points_of_section_iter(se,p+1,plist <| p,poc), get_points_of_section_iter(se,p+1,plist,poc))); %calculates all possible combinations of point positions pairs of a given list of points enumerate_point_position_pairs(plist) = enumerate_point_position_pairs_aux(plist,[]); enumerate_point_position_pairs_aux([],point_poss_done) = point_poss_done; enumerate_point_position_pairs_aux(p |> plist,point_poss_done) = enumerate_point_position_pairs_aux(plist, enumerate_point_position_pairs_aux_aux(p,point_poss_done,[])); enumerate_point_position_pairs_aux_aux(p,[], point_poss_done) = ((point_poss_done <| [point_position_pair(p,left)]) <| [point_position_pair(p,right)]) <| []; enumerate_point_position_pairs_aux_aux(p,point_poss |> point_poss_todo, point_poss_done) = enumerate_point_position_pairs_aux_aux(p,point_poss_todo, ((point_poss_done <| (point_poss <| point_position_pair(p,left))) <| (point_poss <| point_position_pair(p,right))) <| point_poss); in_front_of_signal(se,se2,sic) = %virtual signals excluded exists signal:signal_id. legal_signal(signal) && section_before(sic(signal)) == se && se2 == section_after(sic(signal)) && !virtual(sic(signal)); in_front_of_any_signal(se,se2,sic) = %virtual signals included exists signal:signal_id. legal_signal(signal) && section_before(sic(signal)) == se && se2 == section_after(sic(signal)); get_signal_ahead(se,se2,sic) = get_signal_ahead_iter(se,se2,sic,first_signal); get_signal_ahead_iter(se,se2,sic,si) = %iterate over the signals until the correct one is found if(si > last_signal, 0, if(legal_signal(si) && se == section_before(sic(si)) && se2 == section_after(sic(si)), si, get_signal_ahead_iter(se,se2,sic,si+1))); %finds a route between two signals. The functions ensure that from the starting signal the route options are expanded. %Expanding means that it 'drives' one section further down the route. When a point is encountered the search may continue along %two paths: a path with the point in the left position and a path with the point in the right position. %The search follows a breadth first strategy. After each expansion it is evaluated whether the destination is reached. find_route(si,si2,sec,sic,poc) = find_route_check_done(si2,direction(sic(si)), [route_info(si,si2,direction(sic(si)),[section_before(sic(si)), section_after(sic(si))],[si],[],[],requested)] ,[],sec,sic,poc); %expand route options find_route_expand_options(si,di,roo_todo,roo_done,sec,sic,poc) = if(#roo_todo == 0, find_route_check_done(si,di,roo_done,[],sec,sic,poc), find_route_expand_options(si,di,tail(roo_todo),roo_done ++ expand_route_point_combinations(head(roo_todo),di,sec,sic,poc),sec,sic,poc)); expand_route(ro,di,point_poss,sec,sic,poc) = %expands route given a specific point position if(!legal_section(next_section), [], %ditch route as we have come outside the track [route_info( entry_signal(ro), exit_signal(ro), direction(ro), sections_of_route(ro) <| next_section, if(in_front_of_signal(rhead(sections_of_route(ro)),next_section,sic), signals_of_route(ro) <| get_signal_ahead(rhead(sections_of_route(ro)),next_section,sic), signals_of_route(ro)), points_of_route(ro) ++ point_poss, protection(ro) ++ if(get_flank_protection(rhead(rtail(sections_of_route(ro))),rhead(sections_of_route(ro)),point_poss,sec) == efp , [], [get_flank_protection(rhead(rtail(sections_of_route(ro))),rhead(sections_of_route(ro)),point_poss,sec)]), status(ro) )]) whr next_section = get_next_section_static(rhead(rtail(sections_of_route(ro))),rhead(sections_of_route(ro)),di,point_poss,true,sec) end; %goes through every point combination of the current section and expands the route options expand_route_point_combinations(ro,di,sec,sic,poc) = expand_route_point_combinations_aux(ro,di,sec,sic,poc,enumerate_point_position_pairs(get_points_of_section(rhead(sections_of_route(ro)),poc)),[]); expand_route_point_combinations_aux(ro,di,sec,sic,poc,[],roo_done) = roo_done ++ expand_route(ro,di,[],sec,sic,poc); expand_route_point_combinations_aux(ro,di,sec,sic,poc,point_poss |> point_poss_todo,roo_done) = expand_route_point_combinations_aux(ro,di,sec,sic,poc,point_poss_todo,roo_done ++ expand_route(ro,di,point_poss,sec,sic,poc)); %check if destination is reached on one of the paths find_route_check_done(si,di,roo_todo,roo_done,sec,sic,poc) = if(#roo_todo == 0 && #roo_done == 0, %check if no more viable routes are available route_info(0,0,L,[],[],[],[],rejected), %if so, return rejected route_info if(#roo_todo == 0, %check if more to check find_route_expand_options(si,di,roo_done,[],sec,sic,poc), %all checked so continue expanding if(rhead(sections_of_route(head(roo_todo))) == section_before(sic(si)) && di == direction(sic(si)), %check if destination signal is reached route_free_first_section(head(roo_todo),sic,poc), %found route to destination so done, remove first section as entry section was initially included find_route_check_done(si,di,tail(roo_todo),roo_done <| head(roo_todo),sec,sic,poc)))); %check next %functions to determine the next section given the previous section and the point positions of the current section. %parameter strict makes a difference in the case that there are multiple points in a section. %If strict the given point positions need to exactly be the points needed to go from A to B %(no points included that are not on the route). %This is useful for the find_route function to not find routes with points that are not actually part of the route get_next_section_static(se,se2,R,point_poss,strict,sec) = get_right_section_connections(se,{ppp: point_position_pair | ppp in point_poss},strict,connections(sec(se2))); get_next_section_static(se,se2,L,point_poss,strict,sec) = get_left_section_connections(se,{ppp: point_position_pair | ppp in point_poss},strict,connections(sec(se2))); get_right_section_connections(se,point_poss_set,strict,[]) = 0; get_right_section_connections(se,point_poss_set,strict, sc |> conns) = if(left_section(sc) == se && check_equality_set({ppp: point_position_pair | ppp in positions(sc)}, point_poss_set,strict), right_section(sc), get_right_section_connections(se,point_poss_set,strict,conns)); get_left_section_connections(se,point_poss_set,strict,[]) = 0; get_left_section_connections(se,point_poss_set,strict,sc |> conns) = if(right_section(sc) == se && check_equality_set({ppp: point_position_pair | ppp in positions(sc)}, point_poss_set,strict), left_section(sc), get_left_section_connections(se,point_poss_set,strict,conns)); %based on point position pairs of a section and a neighbouring section, find the section connection and return the accompanying flank protection get_flank_protection(se,se2,point_poss,sec) = get_flank_protection_aux(se,{ppp: point_position_pair | ppp in point_poss},connections(sec(se2))); get_flank_protection_aux(se,point_poss_set,[]) = efp; get_flank_protection_aux(se,point_poss_set,sc |> conns) = if((left_section(sc) == se || right_section(sc) == se) && check_equality_set({ppp: point_position_pair | ppp in positions(sc)}, point_poss_set,true), protection(sc), get_flank_protection_aux(se,point_poss_set,conns)); check_equality_set(point_poss_set,point_poss_set2,true) = point_poss_set == point_poss_set2; check_equality_set(point_poss_set,point_poss_set2,false) = point_poss_set * point_poss_set2 == point_poss_set; %set1 is subset of set2 %get and set operations map section_get_occupance: section_id#sections -> Bool; section_get_status: section_id#sections -> section_status; section_update_status: section_id#section_status#sections -> sections; section_on_border: section_id#sections -> Bool; signal_get_colour: signal_id#signals -> signal_colour; signal_get_virtual: signal_id#signals -> Bool; signal_update_colour: signal_id#signal_colour#signals -> signals; route_update_status: route_info#route_status -> route_info; route_update_sections: route_info#List(section_id) -> route_info; route_update_signals: route_info#List(signal_id) -> route_info; route_update_points: route_info#List(point_position_pair) -> route_info; route_update_protection: route_info#List(flank_protection) -> route_info; route_remove_points_by_section: route_info#section_id#List(point_position_pair)#List(point_position_pair)#points -> route_info; route_remove_protection_by_section: route_info#section_id#List(flank_protection)#List(flank_protection) -> route_info; route_collection_update_route: route_info#route_info#List(route_info) -> List(route_info); route_collection_update_route_aux: route_info#route_info#List(route_info)#List(route_info) -> List(route_info); route_collection_discard_route: route_info#List(route_info) -> List(route_info); route_collection_discard_route_aux: route_info#List(route_info)#List(route_info) -> List(route_info); get_second_section_of_route: route_info -> section_id; route_free_first_signal: route_info -> route_info; route_free_first_section: route_info#signals#points -> route_info; section_before_signal: signal_id#signals -> section_id; section_after_signal: signal_id#signals -> section_id; point_update_position: point_id#point_position#points -> points; routes_handle_section_occupied: section_id#signals#List(route_info) -> List(route_info); routes_handle_section_occupied_aux: section_id#signals#List(route_info)#List(route_info)#List(route_info) -> List(route_info); routes_handle_section_free: section_id#signals#points#List(route_info) -> List(route_info); routes_handle_section_free_aux: section_id#signals#points#List(route_info)#List(route_info)#List(route_info) -> List(route_info); routes_handle_update_signal: signal_id#signal_colour#sections#signals#List(route_info) -> List(route_info); routes_handle_update_signal_aux: signal_id#signal_colour#sections#signals#List(route_info)#List(route_info) -> List(route_info); possibly_discard_route: route_info -> List(route_info); possibly_free_section: section_id#route_info#signals#points#List(route_info) -> route_info; possibly_activate_route: section_id#route_info#signals#List(route_info) -> route_info; possibly_free_signal:signal_id#signal_colour#sections#signals#route_info -> route_info; var se,se2: section_id; %se short for section si,si2: signal_id; %si short for signal po:point_id; pos: point_position; ss: section_status; co: signal_colour; %co short for colour sec: sections; %sec short for section collection sic: signals; %sic short for signal collection poc: points; ro,ro2,newro: route_info; %ro short for route roc,roc2,roc3: List(route_info); %roc short for route collection ppp: point_position_pair; ppp_list, ppp_list2: List(point_position_pair); flp: flank_protection; flp_list, flp_list2: List(flank_protection); ros: route_status; %ros short for route_status se_list: List(section_id); %se_list short for section list si_list: List(signal_id); %si_list short for signal list eqn section_get_occupance(se,sec) = !(status(sec(se)) == free); %true if occupied or logically occupied section_get_status(se,sec) = status(sec(se)); section_update_status(se,ss,sec) = sec[se -> section_info(ss,on_border(sec(se)),connections(sec(se)))]; section_on_border(se,sec) = on_border(sec(se)); signal_get_colour(si,sic) = colour(sic(si)); signal_get_virtual(si, sic) = virtual(sic(si)); signal_update_colour(si,co,sic) = sic[si -> signal_info(co,direction(sic(si)),virtual(sic(si)),section_before(sic(si)),section_after(sic(si)))]; route_update_status(ro,ros) = route_info(entry_signal(ro), exit_signal(ro), direction(ro), sections_of_route(ro), signals_of_route(ro),points_of_route(ro),protection(ro), ros); route_update_sections(ro,se_list) = route_info(entry_signal(ro), exit_signal(ro), direction(ro), se_list, signals_of_route(ro),points_of_route(ro),protection(ro), status(ro)); route_update_signals(ro,si_list) = route_info(entry_signal(ro), exit_signal(ro), direction(ro), sections_of_route(ro), si_list,points_of_route(ro),protection(ro), status(ro)); route_update_points(ro,ppp_list) = route_info(entry_signal(ro), exit_signal(ro), direction(ro), sections_of_route(ro), signals_of_route(ro),ppp_list,protection(ro), status(ro)); route_update_protection(ro,flp_list) = route_info(entry_signal(ro),exit_signal(ro), direction(ro),sections_of_route(ro), signals_of_route(ro),points_of_route(ro),flp_list,status(ro)); get_second_section_of_route(ro) = if(#sections_of_route(ro) < 2, 0,head(tail(sections_of_route(ro)))); route_free_first_signal(ro) = route_update_signals(ro, tail(signals_of_route(ro))); section_before_signal(si,sic) = section_before(sic(si)); section_after_signal(si,sic) = section_after(sic(si)); point_update_position(po,pos,poc) = poc[po -> point_info(in_section(poc(po)), pos)]; route_collection_update_route(newro,ro,roc) = route_collection_update_route_aux(newro,ro,roc,[]); route_collection_update_route_aux(newro,ro,[],roc2) = roc2; route_collection_update_route_aux(newro,ro,ro2 |> roc,roc2) = route_collection_update_route_aux(newro,ro,roc,roc2 <| if(ro==ro2, newro, ro2)); route_collection_discard_route(ro,roc) = route_collection_discard_route_aux(ro,roc,[]); route_collection_discard_route_aux(ro,[],roc2) = roc2; route_collection_discard_route_aux(ro,ro2 |> roc,roc2) = route_collection_discard_route_aux(ro,roc,roc2 ++ if(ro==ro2, [], [ro2])); %frees up the first section of the route and calls functions to also free any flank protection and points of the section route_free_first_section(ro,sic,poc) = route_remove_protection_by_section( route_remove_points_by_section( route_update_sections(ro, tail(sections_of_route(ro))) ,head(sections_of_route(ro)),points_of_route(ro),[],poc) ,head(sections_of_route(ro)),protection(ro),[]); %goes through the entire list of points of the route and removes the ones that are in the given section route_remove_points_by_section(ro,se,[],ppp_list2,poc) = route_update_points(ro,ppp_list2); route_remove_points_by_section(ro,se,ppp |> ppp_list,ppp_list2,poc) = if(se == in_section(poc(point(ppp))), route_remove_points_by_section(ro,se,ppp_list,ppp_list2,poc), route_remove_points_by_section(ro,se,ppp_list,ppp_list2 <| ppp,poc)); %goes through the entire list of flank protections of the route and removes the ones that are of the given section route_remove_protection_by_section(ro,se,[],flp_list2) = route_update_protection(ro,flp_list2); route_remove_protection_by_section(ro,se,flp |> flp_list,flp_list2) = if(se == for_section(flp), route_remove_protection_by_section(ro,se,flp_list,flp_list2), route_remove_protection_by_section(ro,se,flp_list,flp_list2 <| flp)); %update routes based on a section being marked as free routes_handle_section_free(se,sic,poc,roc) = routes_handle_section_free_aux(se,sic,poc,roc,roc,[]); routes_handle_section_free_aux(se,sic,poc,roc,[],roc3) = roc3; routes_handle_section_free_aux(se,sic,poc,roc,ro |> roc2,roc3) = routes_handle_section_free_aux(se,sic,poc,roc,roc2,roc3 ++ possibly_discard_route(possibly_free_section(se,ro,sic,poc,roc))); possibly_discard_route(ro) = if(#sections_of_route(ro) == 0, [], [ro]); possibly_free_section(se,ro,sic,poc,roc) = if(#sections_of_route(ro) != 0 && status(ro) == active && section_first_of_route(se,ro), route_free_first_section(ro,sic,poc), ro); %update routes based on a section being marked as occupied routes_handle_section_occupied(se,sic,roc) = routes_handle_section_occupied_aux(se,sic,roc,roc,[]); routes_handle_section_occupied_aux(se,sic,roc,[],roc3) = roc3; routes_handle_section_occupied_aux(se,sic,roc,ro |> roc2,roc3) = routes_handle_section_occupied_aux(se,sic,roc,roc2,roc3 <| possibly_activate_route(se,ro,sic,roc)); possibly_activate_route(se,ro,sic,roc) = if(status(ro) == ready && se == section_after(sic(entry_signal(ro))),route_update_status(ro,active),ro); %update routes based on a signal being set to a new colour (a signal might be removed from a route) routes_handle_update_signal(si,co,sec,sic,roc) = routes_handle_update_signal_aux(si,co,sec,sic,roc,[]); routes_handle_update_signal_aux(si,co,sec,sic,[],roc2) = roc2; routes_handle_update_signal_aux(si,co,sec,sic,ro |> roc,roc2) = routes_handle_update_signal_aux(si,co,sec,sic,roc,roc2 <| possibly_free_signal(si,co,sec,sic,ro)); possibly_free_signal(si,co,sec,sic,ro) = if(co == RD && signal_first_of_route(si,ro) && section_after_signal_occupied(si,sec,sic),route_free_first_signal(ro),ro); %dynamic calculations (dependent on current section occupations, point positions and routes) map all_points_locked: route_info#sections#points -> Bool; border_unclaimed: section_id#List(route_info) -> Bool; get_points_to_be_locked: route_info#sections#points -> Set(point_position_pair); route_conflict_free_points: route_info#sections#List(route_info)#points -> Bool; route_conflict_free_flank_signals: route_info#sections#List(route_info) -> Bool; route_conflict_free_head_on: route_info#List(route_info) -> Bool; compute_signal: signal_id#sections#signals#List(route_info)#points -> signal_colour; section_first_of_route: section_id#route_info -> Bool; section_part_of_route: section_id#List(route_info) -> Bool; section_first_of_active_route: section_id#List(route_info) -> Bool; section_last_of_active_route: section_id#List(route_info) -> Bool; second_section_of_route_occupied: section_id#sections#List(route_info) -> Bool; signal_part_of_ready_route: signal_id#List(route_info) -> Bool; signal_first_of_route: signal_id#route_info -> Bool; section_before_signal_part_of_active_route: signal_id#signals#List(route_info) -> Bool; section_before_signal_occupied: signal_id#sections#signals -> Bool; section_after_signal_occupied: signal_id#sections#signals -> Bool; signal_free: signal_id#List(route_info) -> Bool; sections_of_route_free: route_info#sections -> Bool; get_next_section: section_id#section_id#driving_direction#sections#points -> section_id; get_point_positions: List(point_id)#points#List(point_position_pair) -> List(point_position_pair); get_possible_routes: routing_table#sections#signals#points#Set(route_info) -> Set(route_info); var se,se2: section_id; si,si2: signal_id; max_sec_to_go: Nat; o: Bool; %o short for occupance p: point_id; co: signal_colour; sec: sections; %sec short for section collection sic: signals; %sic short for signal collection poc: points; %poc short for point collection pos: point_position; di: driving_direction; si_togo: Nat; ro,ro2: route_info; %ro short for route sp: signal_pair; plist: List(point_id); ppplist: List(point_position_pair); rot: routing_table; roc,roc2,roc3: List(route_info); %roc short for route collection rocset: Set(route_info); ros: route_status; se_list: List(section_id); si_list: List(signal_id); eqn %goes through all the allowed signal combinations for which a route can be requested and calculates the route between the signals using find_route %this function is used to precalculate all the routes during linearisation to improve efficiency get_possible_routes([],sec,sic,poc,rocset) = rocset; get_possible_routes(sp |> rot,sec,sic,poc,rocset) = get_possible_routes(rot,sec,sic,poc,rocset+{find_route(entry_signal(sp),exit_signal(sp),sec,sic,poc)}); %verify that no route is set to a given border section border_unclaimed(se,roc) = forall ro:route_info. (ro in roc) => (#sections_of_route(ro) == 0 || rhead(sections_of_route(ro)) != se); %functions to check/get the points of a given route that are not yet in the right position all_points_locked(ro,sec,poc) = get_points_to_be_locked(ro,sec,poc) == {}; get_points_to_be_locked(ro,sec,poc) = {ppp: point_position_pair| ppp in points_of_route(ro) && position(poc(point(ppp))) != position(ppp)} + {ppp: point_position_pair| exists fp:flank_protection. fp in protection(ro) && ppp in flank_protection_points(fp) && position(poc(point(ppp))) != position(ppp)}; %checks whether the points of a given route conflict with the points of a route that has already been accepted, %also takes into account flank protection points route_conflict_free_points(ro,sec,roc,poc) = forall p:point_id. (legal_point(p) && exists ppp:point_position_pair. ppp in get_points_to_be_locked(ro,sec,poc) && p == point(ppp)) => (forall other_route:route_info. (other_route in roc) => (forall other_route_p:point_id. (legal_point(other_route_p) && exists ppp2:point_position_pair. ppp2 in points_of_route(other_route) && other_route_p == point(ppp2)) => (p != other_route_p))); %checks whether the flank protection signals of a given route conflict with the signals of a route that has already been accepted route_conflict_free_flank_signals(ro,sec,roc) = forall si:signal_id. (legal_signal(si) && exists fp:flank_protection. fp in protection(ro) && si in flank_protection_signals(fp)) => (forall other_route:route_info. other_route in roc && other_route != ro => (forall si2:signal_id. (legal_signal(si2) && si2 in signals_of_route(other_route)) => (si != si2))); route_conflict_free_head_on(ro,roc) = forall other_route:route_info. (other_route in roc) => (direction(ro) == direction(other_route) || (forall se:section_id. (se in sections_of_route(ro)) => !(se in sections_of_route(other_route)))); %gets the next section based on the previous section and the current point positions get_next_section(se,se2,di,sec,poc) = get_next_section_static(se,se2,di,get_point_positions(get_points_of_section(se2,poc),poc,[]),false,sec); get_point_positions([],poc,ppplist) = ppplist; get_point_positions(p |> plist,poc,ppplist) = get_point_positions(plist,poc,ppplist <| point_position_pair(p, position(poc(p)))); %remaining equations are self explanatory section_before_signal_part_of_active_route(si,sic,roc) = legal_signal(si) && exists route:route_info. (route in roc && (status(route) == active || status(route) == ready)) && (exists route_section: section_id. legal_section(route_section) && (route_section in sections_of_route(route)) && (route_section == section_before_signal(si,sic))); signal_first_of_route(si,ro) = si == head(signals_of_route(ro)) && #signals_of_route(ro) > 0; section_first_of_route(se,ro) = se == head(sections_of_route(ro)) && #sections_of_route(ro) > 0; section_part_of_route(se,roc) = exists route:route_info. exists section:section_id . route in roc && section in sections_of_route(route); section_first_of_active_route(se,roc) = exists route:route_info. route in roc && status(route) == active && #sections_of_route(route) > 0 && se == head(sections_of_route(route)); section_last_of_active_route(se,roc) = exists route:route_info. route in roc && status(route) == active && #sections_of_route(route) == 1 && se == head(sections_of_route(route)); second_section_of_route_occupied(se,sec,roc) = exists route:route_info. route in roc && #sections_of_route(route) > 1 && se == head(sections_of_route(route)) && section_get_occupance(head(tail(sections_of_route(route))),sec); signal_part_of_ready_route(si,roc) = exists route:route_info. route in roc && status(route) == ready && si in signals_of_route(route); sections_of_route_free(ro,sec) = forall se:section_id. se in sections_of_route(ro) => !section_get_occupance(se,sec); section_before_signal_occupied(si,sec,sic) = section_get_occupance(section_before_signal(si,sic), sec); section_after_signal_occupied(si,sec,sic) = section_get_occupance(section_after_signal(si,sic),sec); signal_free(si,roc) = forall other_route:route_info. (other_route in roc) => (forall other_route_signal: signal_id. (other_route_signal in signals_of_route(other_route)) => other_route_signal != si); %contains the simple signal logic: default is red, if signal is the entry signal of a ready route and all sections of route are free: at least yellow. %if the exit signal is not red than this signal can be set to green. compute_signal(si,sec,sic,roc,poc) = if(!(exists ro:route_info. ro in roc && entry_signal(ro) == si && status(ro) == ready && sections_of_route_free(ro,sec)), RD, if(exists ro:route_info. ro in roc && entry_signal(ro) == si && status(ro) == ready && sections_of_route_free(ro,sec) && signal_get_colour(exit_signal(ro),sic) != RD && !signal_get_virtual(exit_signal(ro),sic), GR, GL)); %track layout configuration, several instances can be configured and the instance to be used can be specified below map instance: Nat; eqn instance = 1; sort constants_sort = struct c( last_section: section_id, last_signal: signal_id, last_point: point_id, last_train: Nat ); train_config = struct train_config( entry_section: section_id, direction: driving_direction, start_over: Bool ); trains = Nat -> train_config; map first_section, last_section: section_id; first_signal, last_signal: signal_id; first_point, last_point: point_id; last_train: Nat; constants: Nat -> constants_sort; sections_config : Nat -> sections; signals_config : Nat -> signals; points_config: Nat -> points; trains_config: Nat -> trains; routing_table_config: Nat -> routing_table; eqn constants(1) = constants(3); sections_config(1) = sections_config(3); signals_config(1) = signals_config(3); points_config(1) = points_config(3); trains_config(1)(1) = train_config(4,L,false); trains_config(1)(2) = train_config(4,L,false); routing_table_config(1) = [signal_pair(1,4), signal_pair(1,5), signal_pair(2,6),signal_pair(3,6)]; constants(2) = constants(3); sections_config(2) = sections_config(3); signals_config(2) = signals_config(3); points_config(2) = points_config(3); trains_config(2)(1) = train_config(4,L,false); trains_config(2)(2) = train_config(1,R,false); routing_table_config(2) = routing_table_config(1); constants(3) = c(4,6,1,2);%constants are the number of section,signals,points and trains sections_config(3)(1) = section_info(free, true, [section_connection([],efp,0,2)]); sections_config(3)(2) = section_info(free, false, [section_connection([point_position_pair(1,left)],flank_protection(2,[],[3]),1,3), section_connection([point_position_pair(1,right)],flank_protection(2,[],[2]),1,4)]); sections_config(3)(3) = section_info(free, true, [section_connection([],efp,2,0)]); sections_config(3)(4) = section_info(free, true, [section_connection([],efp,2,0)]); signals_config(3)(1) = signal_info(RD, R, false, 1,2); signals_config(3)(2) = signal_info(RD, L, false, 3,2); signals_config(3)(3) = signal_info(RD, L, false, 4,2); signals_config(3)(4) = signal_info(GR, R, true, 3,0); %virtual signal always green signals_config(3)(5) = signal_info(GR, R, true, 4,0); %virtual signal always green signals_config(3)(6) = signal_info(GR, L, true, 1,0); %virtual signal always green points_config(3)(1) = point_info(2, right); trains_config(3)(1) = train_config(4,L,false); trains_config(3)(2) = train_config(4,L,false); routing_table_config(3) = [signal_pair(3,6)]; constants(4) = c(4,6,1,0); sections_config(4) = sections_config(3); signals_config(4) = signals_config(3); points_config(4) = points_config(3); routing_table_config(4) = routing_table_config(1); %Zevenaar constants(5) = c(9,8,0,2); sections_config(5)(1) = section_info(free, true, [section_connection([],efp,0,2)]); sections_config(5)(2) = section_info(free, false, [section_connection([],efp,1,3)]); sections_config(5)(3) = section_info(free, false, [section_connection([],efp,2,4)]); sections_config(5)(4) = section_info(free, false, [section_connection([],efp,3,5)]); sections_config(5)(5) = section_info(free, false, [section_connection([],efp,4,6)]); sections_config(5)(6) = section_info(free, false, [section_connection([],efp,5,7)]); sections_config(5)(7) = section_info(free, false, [section_connection([],efp,6,8)]); sections_config(5)(8) = section_info(free, false, [section_connection([],efp,7,9)]); sections_config(5)(9) = section_info(free, true, [section_connection([],efp,8,0)]); signals_config(5)(1) = signal_info(RD, L, false, 9,8); signals_config(5)(2) = signal_info(RD, L, false, 6,5); signals_config(5)(3) = signal_info(RD, L, false, 3,2); signals_config(5)(4) = signal_info(GR, L, true, 1,0); %virtual signal always green signals_config(5)(5) = signal_info(RD, R, false, 1,2); signals_config(5)(6) = signal_info(RD, R, false, 3,4); signals_config(5)(7) = signal_info(RD, R, false, 6,7); signals_config(5)(8) = signal_info(GR, R, true, 9,0); %virtual signal always green trains_config(5)(1) = train_config(1,R,false); trains_config(5)(2) = train_config(9,L,false); routing_table_config(5) = [signal_pair(1,2), signal_pair(2,3), signal_pair(3,4),signal_pair(5,6), signal_pair(6,7),signal_pair(7,8)]; first_section = 1; last_section = last_section(constants(instance)); first_signal = 1; last_signal = last_signal(constants(instance)); first_point = 1; last_point = last_point(constants(instance)); last_train = last_train(constants(instance)); act getStatusSection, getStatusSectionSend, getStatusSectionRec: Nat # Bool; %parameters: section id, occupied seeSignal, seeSignalSend, seeSignalRec: Nat # signal_colour; %first parameter: signal id setStatusSection,setStatusSectionSection,setStatusSectionTrain: Nat # Bool; %parameters: section id, occupied permissionTrain, permissionInterlocking, permission: section_id # Bool; setSignalSend, setSignalRec, setSignal: Nat # signal_colour; %first parameter: signal id getPositionPoint, getPositionPointSend, getPositionPointRec: point_id#point_position; setPositionPoint, setPositionPointSend, setPositionPointRec, setPositionPointRecTrain: point_id#point_position#section_id; requestRoute: signal_id # signal_id; %parameters: entry signal, exit signal routeAccepted; routeRejected; activateRoute; readyRoute; notReadyRoute; freeUpSection: section_id; discardRoute; freeUpSignal: signal_id; mergeRoutes; skip; proc %sections act as a sort of variable that can be set by the train and read by the interlocking %Abbreviations: cs->current status Section(id: section_id, cs: Bool) = (sum b:Bool. setStatusSectionSection(id, b) . Section(cs = b)) + getStatusSectionSend(id, cs). Section(); %Signals can be set by the interlocking and read by a train %Abbreviations: cc->current colour, nc->new colour Signal(id: signal_id, cc: signal_colour) = (sum nc: signal_colour . setSignalRec(id, nc) . Signal(id, nc)) + seeSignalSend(id, cc). Signal(); %Points are set by the interlocking Point(id: point_id, pos: point_position, se:section_id) = (sum npos: point_position. setPositionPointRec(id, npos,se).Point(pos = npos)) + getPositionPointSend(id, pos). Point(); %Trains go through the lifecycle before_track->on_track->after_track. %To enter the track permission from the interlocking is neccesary. %A train can occuppy at most two sections. If it occupies only one, %the next section can become occupied. Before this, it needs to see that %the signal is yellow or green (if there is a signal) If it occupies two sections, %the section occupied by the back of the train can become unoccupied. %Once the train has reached the other side of the yard it can leave the yard. %If the boolean so is set to true, it can start over and simulate a new train. %Abbreviations: gp->general position, es->entry section, os->occupied sections, %so->start over, prevs->previous section, %sec->section collection, sic->signal collection, poc->point collection Train(gp: train_general_position, can_proceed: Bool, es: section_id, os: List(section_id), prevs:section_id, di: driving_direction, so: Bool, sec: sections, sic:signals, poc: points) = ((gp == before_track) -> %entering first section only if permission by interlocking permissionTrain(es, true).Train(gp = on_track, os = [es])) + ((gp == on_track) -> sum next_section:section_id. (next_section == get_next_section(prevs,head(os),di,sec,poc)) -> ( (#os == 2) -> setStatusSectionTrain(head(os),false).Train(prevs = head(os), os = tail(os)) +(#os == 1 && legal_section(next_section) && !can_proceed) -> ( (in_front_of_signal(rhead(os),next_section, sic)) -> (seeSignalRec(get_signal_ahead(rhead(os),next_section, sic),GR) + seeSignalRec(get_signal_ahead(rhead(os),next_section, sic),GL)) +(!in_front_of_signal(rhead(os),next_section, sic)) -> skip ).Train(can_proceed = true) +(#os == 1 && legal_section(next_section) && can_proceed) -> setStatusSectionTrain(next_section,true) .Train(os = os <| next_section, can_proceed = false) +(#os == 1 && !legal_section(next_section)) -> setStatusSectionTrain(head(os),false).Train(os = [], gp = after_track, prevs = 0) ) ) + ((gp == after_track && so) -> skip.Train(gp = before_track)) + (sum npos: point_position. sum p:point_id. sum se:section_id. (legal_section(se) && legal_point(p)) -> setPositionPointRecTrain(p, npos, se).Train(poc = point_update_position(p,npos,poc))); %Interlocking can non deterministically choose to do any action that is enabled %Abbreviations: sec->section collection, sic->signal collection, roc->route collection, poc->point collection, pro->precalculated routes, rro->requested routes Interlocking(sec: sections, sic: signals, roc:List(route_info), poc: points, pro:Set(route_info), rro: List(route_info)) = InterlockingUpdatingSignal() + InterlockingReadingSection() + InterlockingMovingPoint() + InterlockingReceivingRouteRequest() + InterlockingProcessingRoute() + InterlockingReadyRoute() + InterlockingNotReadyRoute() + InterlockingPermitTrainEntry(); %To enter the yard the interlocking needs to give permission. Permission is %given when the entry section is free, the signal on that section is showing %stop and the border is not claimed (a route set to the open track via that %section) InterlockingPermitTrainEntry(sec: sections, sic: signals, roc:List(route_info), poc: points, pro:Set(route_info), rro: List(route_info)) = sum se:section_id. sum next_section:section_id. ((next_section == get_next_section(0,se,L,sec,poc) || next_section == get_next_section(0,se,R,sec,poc)) && (legal_section(se) && !section_get_occupance(se,sec) && border_unclaimed(se,roc) && in_front_of_signal(se,next_section,sic) && signal_get_colour(get_signal_ahead(se,next_section,sic),sic) == RD)) -> permissionInterlocking(se,true).Interlocking(sec = section_update_status(se,occupied,sec)); %read the status of a section. Reading a section is occupied always results %in the interlocking seeing the section as occupied. When a section becomes %unoccupied the interlocking can see it as truely free or logically occupied. %It can become logically occupied when it is the first section of a route and %the next section has not (yet) become occupied (the train disappeared in view %of the interlocking). Once a section has become free or occupied the effect %on the routes is also calculated immediately. In this variant a timing issue %is excluded. The interlocking can only read that the border section has become %unoccupied when it has read that the section afterwards has become occupied. InterlockingReadingSection(sec: sections, sic: signals, roc:List(route_info), poc: points, pro:Set(route_info), rro: List(route_info)) = sum s: Bool. sum se: section_id.(legal_section(se) && section_get_occupance(se,sec)!=s) -> (!(section_on_border(se,sec) && !section_last_of_active_route(se,roc) && ((legal_section(get_next_section(0,se,L,sec,poc)) && !section_get_occupance(get_next_section(0,se,L,sec,poc),sec)) || (legal_section(get_next_section(0,se,R,sec,poc)) && !section_get_occupance(get_next_section(0,se,R,sec,poc),sec))) && !s)) ->getStatusSectionRec(se, s) .((!s && !section_on_border(se,sec) && !second_section_of_route_occupied(se,sec,roc) && section_first_of_active_route(se,roc)) -> Interlocking(sec = section_update_status(se,logically_occupied,sec)) + (!s && (section_on_border(se,sec) || second_section_of_route_occupied(se,sec,roc) || !section_first_of_active_route(se,roc))) -> Interlocking(sec = section_update_status(se,free,sec), roc = routes_handle_section_free(se,sic,poc,roc)) + (s) -> Interlocking(sec = section_update_status(se,occupied,sec), roc = routes_handle_section_occupied(se,sic,roc))); %receive a route request that is in the precalculated route_info set pro %If a previous route request has not been answered yet a new %route request is not possible. InterlockingReceivingRouteRequest(sec: sections, sic: signals, roc:List(route_info), poc: points, pro:Set(route_info), rro: List(route_info)) = sum ro: route_info. (ro in pro && #rro == 0) -> requestRoute(entry_signal(ro), exit_signal(ro)).Interlocking(rro = [ro]); %evaluate whether a requested route can be accepted or not %accepted when there is no conflict with another route already accepted InterlockingProcessingRoute(sec: sections, sic: signals, roc:List(route_info), poc: points, pro:Set(route_info), rro: List(route_info)) = (#rro > 0) -> ((signal_free(entry_signal(head(rro)),roc) && route_conflict_free_flank_signals(head(rro),sec,roc) && route_conflict_free_points(head(rro),sec,roc,poc)&& route_conflict_free_head_on(head(rro),roc)) -> routeAccepted.Interlocking(roc = roc <| if(all_points_locked(head(rro),sec,poc), route_update_status(head(rro),locked),route_update_status(head(rro),accepted)), rro = []) + (!(signal_free(entry_signal(head(rro)),roc) && route_conflict_free_flank_signals(head(rro),sec,roc) && route_conflict_free_points(head(rro),sec,roc,poc)&& route_conflict_free_head_on(head(rro),roc))) -> routeRejected.Interlocking(rro = [])); %if a route is accepted but not all points have been moved to the correct position yet, this process can move one of those points InterlockingMovingPoint(sec: sections, sic: signals, roc:List(route_info), poc: points, pro:Set(route_info), rro: List(route_info)) = sum ro:route_info. sum ppp:point_position_pair. (ppp in get_points_to_be_locked(ro,sec,poc) && ro in roc && status(ro) == accepted) -> (setPositionPointSend(point(ppp), position(ppp), in_section(poc(point(ppp)))) .Interlocking(poc = point_update_position(point(ppp),position(ppp),poc), roc = if(all_points_locked(ro,sec,point_update_position(point(ppp),position(ppp),poc)),route_collection_update_route(route_update_status(ro,locked),ro,roc),roc))); %if the compute signal function returns a different signal aspect than the current aspect, it is updated InterlockingUpdatingSignal(sec: sections, sic: signals, roc:List(route_info), poc: points, pro:Set(route_info), rro: List(route_info)) = sum result: signal_colour. sum si: signal_id. (legal_signal(si) && result == compute_signal(si,sec,sic,roc,poc) && !signal_get_virtual(si,sic)) -> ((!(result == signal_get_colour(si,sic))) -> setSignalSend(si, result).Interlocking(sic = signal_update_colour(si, result, sic), roc = routes_handle_update_signal(si,result,sec,sic,roc))); %a route that is locked and of which the section before the entry signal is occupied becomes ready (the signal can show proceed) InterlockingReadyRoute(sec: sections, sic: signals, roc:List(route_info), poc: points, pro:Set(route_info), rro: List(route_info)) = sum ro:route_info. (ro in roc && status(ro) == locked) -> (section_before_signal_occupied(entry_signal(ro),sec,sic) || section_before_signal_part_of_active_route(entry_signal(ro),sic,roc)) -> (legal_signal(entry_signal(ro)))-> (sections_of_route_free(ro,sec)) -> readyRoute.Interlocking(roc = route_collection_update_route(route_update_status(ro,ready),ro,roc)); %a route can go from ready backed to locked if the conditions for ready no longer apply InterlockingNotReadyRoute(sec: sections, sic: signals, roc:List(route_info), poc: points, pro:Set(route_info), rro: List(route_info)) = sum ro:route_info. (ro in roc && status(ro) == ready && !(section_before_signal_occupied(entry_signal(ro),sec,sic) || section_after_signal_occupied(entry_signal(ro),sec,sic) || section_before_signal_part_of_active_route(entry_signal(ro),sic,roc))) -> notReadyRoute.Interlocking(roc = route_collection_update_route(route_update_status(ro,locked),ro,roc)); % Initialization init %hide internal communication hide({skip}, %, seeSignal, getStatusSection,activateRoute,readyRoute,notReadyRoute,freeUpSection,discardRoute,freeUpSignal,setSignal allow( % Allow the following actions to happen {setSignal, getStatusSection, setStatusSection,seeSignal, setPositionPoint, requestRoute,routeAccepted,routeRejected,activateRoute,readyRoute,notReadyRoute, freeUpSection,discardRoute,freeUpSignal,skip}, comm( { seeSignalSend|seeSignalRec -> seeSignal, setSignalSend|setSignalRec -> setSignal, setStatusSectionSection|setStatusSectionTrain -> setStatusSection, getStatusSectionSend|getStatusSectionRec -> getStatusSection, setPositionPointSend|setPositionPointRec|setPositionPointRecTrain|setPositionPointRecTrain -> setPositionPoint },comm({permissionTrain|permissionInterlocking -> setStatusSectionTrain}, %Initial situation, based on the configuration the right number of processes is created. %Some processes are also passed parameters based on the configuration. ((1 <= last_section) -> Section(1, false)) || ((2 <= last_section) -> Section(2, false)) || ((3 <= last_section) -> Section(3, false)) || ((4 <= last_section) -> Section(4, false)) || ((5 <= last_section) -> Section(5, false)) || ((6 <= last_section) -> Section(6, false)) || ((7 <= last_section) -> Section(7, false)) || ((8 <= last_section) -> Section(8, false)) || ((9 <= last_section) -> Section(9, false)) || ((10 <= last_section) -> Section(10, false)) || ((11 <= last_section) -> Section(11, false)) || ((12 <= last_section) -> Section(12, false)) || ((13 <= last_section) -> Section(13, false)) || ((14 <= last_section) -> Section(14, false)) || ((15 <= last_section) -> Section(15, false)) || ((16 <= last_section) -> Section(16, false)) || ((17 <= last_section) -> Section(17, false)) || ((18 <= last_section) -> Section(18, false)) || ((19 <= last_section) -> Section(19, false)) || ((20 <= last_section) -> Section(20, false)) || ((21 <= last_section) -> Section(21, false)) || ((22 <= last_section) -> Section(22, false)) || ((23 <= last_section) -> Section(23, false)) || ((24 <= last_section) -> Section(24, false)) || ((25 <= last_section) -> Section(25, false)) || ((26 <= last_section) -> Section(26, false)) || ((27 <= last_section) -> Section(27, false)) || ((28 <= last_section) -> Section(28, false)) || ((29 <= last_section) -> Section(29, false)) || ((30 <= last_section) -> Section(30, false)) || ((31 <= last_section) -> Section(31, false)) || ((32 <= last_section) -> Section(32, false)) || ((33 <= last_section) -> Section(33, false)) || ((34 <= last_section) -> Section(34, false)) || ((35 <= last_section) -> Section(35, false)) || ((36 <= last_section) -> Section(36, false)) || ((1 <= last_signal && !virtual(signals_config(instance)(1))) -> Signal(1, RD)) || ((2 <= last_signal && !virtual(signals_config(instance)(2))) -> Signal(2, RD)) || ((3 <= last_signal && !virtual(signals_config(instance)(3))) -> Signal(3, RD)) || ((4 <= last_signal && !virtual(signals_config(instance)(4))) -> Signal(4, RD)) || ((5 <= last_signal && !virtual(signals_config(instance)(5))) -> Signal(5, RD)) || ((6 <= last_signal && !virtual(signals_config(instance)(6))) -> Signal(6, RD)) || ((7 <= last_signal && !virtual(signals_config(instance)(7))) -> Signal(7, RD)) || ((8 <= last_signal && !virtual(signals_config(instance)(8))) -> Signal(8, RD)) || ((9 <= last_signal && !virtual(signals_config(instance)(9))) -> Signal(9, RD)) || ((10 <= last_signal && !virtual(signals_config(instance)(10))) -> Signal(10, RD)) || ((11 <= last_signal && !virtual(signals_config(instance)(11))) -> Signal(11, RD)) || ((12 <= last_signal && !virtual(signals_config(instance)(12))) -> Signal(12, RD)) || ((13 <= last_signal && !virtual(signals_config(instance)(13))) -> Signal(13, RD)) || ((14 <= last_signal && !virtual(signals_config(instance)(14))) -> Signal(14, RD)) || ((15 <= last_signal && !virtual(signals_config(instance)(15))) -> Signal(15, RD)) || ((16 <= last_signal && !virtual(signals_config(instance)(16))) -> Signal(16, RD)) || ((17 <= last_signal && !virtual(signals_config(instance)(17))) -> Signal(17, RD)) || ((18 <= last_signal && !virtual(signals_config(instance)(18))) -> Signal(18, RD)) || ((1 <= last_point) -> Point(1, position(points_config(instance)(1)),in_section(points_config(instance)(1)))) || ((2 <= last_point) -> Point(2, position(points_config(instance)(2)),in_section(points_config(instance)(2)))) || ((3 <= last_point) -> Point(3, position(points_config(instance)(3)),in_section(points_config(instance)(3)))) || ((4 <= last_point) -> Point(4, position(points_config(instance)(4)),in_section(points_config(instance)(4)))) || ((5 <= last_point) -> Point(5, position(points_config(instance)(5)),in_section(points_config(instance)(5)))) || ((6 <= last_point) -> Point(6, position(points_config(instance)(6)),in_section(points_config(instance)(6)))) || Train(before_track, false, entry_section(trains_config(instance)(1)), [], 0, direction(trains_config(instance)(1)), start_over(trains_config(instance)(1)), sections_config(instance), signals_config(instance), points_config(instance)) || Train(before_track, false, entry_section(trains_config(instance)(2)), [], 0, direction(trains_config(instance)(2)), start_over(trains_config(instance)(2)), sections_config(instance), signals_config(instance), points_config(instance)) %|| Train(before_track, false, entry_section(trains_config(instance)(3)), [], 0, direction(trains_config(instance)(3)), start_over(trains_config(instance)(3)), % sections_config(instance), signals_config(instance), points_config(instance)) %|| Train(before_track, false, entry_section(trains_config(instance)(4)), [], 0, direction(trains_config(instance)(4)), start_over(trains_config(instance)(4)), % sections_config(instance), signals_config(instance), points_config(instance)) || Interlocking(sections_config(instance), signals_config(instance), [], points_config(instance), get_possible_routes(routing_table_config(instance),sections_config(instance),signals_config(instance),points_config(instance),{}),[]) ))));