%%% TRAFFIC %%% :- sorts integer; node; segment; car. :- variables Nd :: node; Sg :: segment; C,C1 :: car; Ds,Ds1 :: integer; Sp,Sp1 :: integer. :- objects 0..maxInt :: integer. :- constants % If a car is pointing toward the end node of the segment on % which it currently is, its positiveOrientation is true positiveOrientation(car) :: inertialFluent; % Each car has a position at each point in time. The position is % indicated as a pair consisting of the segment where the car % is located, and the distance travelled along the segment % (lmw) segment(car) :: inertialFluent(segment); distance(car) :: simpleFluent(integer). :- macros position(#1,#2,#3) -> (segment(#1)=(#2) & distance(#1)=(#3)). :- constants % Each segment has exactly one start node and exactly one end % node (lmw) startNode(segment) :: node; endNode(segment) :: node; % Each segment has a length, which is a real number (or rational % number, if preferred). (lmw) We assume it to be an integer length(segment) :: integer; % Each road segment has a speed limit (lmw) speedLimit(segment) :: integer; % Each car has a top speed (lmw) topSpeed(car) :: integer; % Actual speed of a car during the next time interval speed(car) :: sdFluent(integer); % The new segment a car will continue on nextSegment(car) :: inertialFluent(segment+none); % A car will leave the segment on which it is currently % travelling willLeave(car) :: simpleFluent; % The node at which a car is node(car) :: sdFluent(node+none). exogenous willLeave(C). % The position of a car determines whether it is at a node or % not and, if it is, which node it is at. caused node(C)=Nd if positiveOrientation(C) & position(C,Sg,0) & startNode(Sg)=Nd. caused node(C)=Nd if -positiveOrientation(C) & position(C,Sg,0) & endNode(Sg)=Nd. caused node(C)=Nd if positiveOrientation(C) & position(C,Sg,length(Sg)) & endNode(Sg)=Nd. caused node(C)=Nd if -positiveOrientation(C) & position(C,Sg,length(Sg)) & startNode(Sg)=Nd. default node(C)=none. % A car will have a positive orientation after leaving the % start node of the segment it is entering caused positiveOrientation(C) after willLeave(C) & nextSegment(C)=Sg & node(C)=startNode(Sg). % A car will have a negative orientation after leaving the end % node of the segment it is entering caused -positiveOrientation(C) after willLeave(C) & nextSegment(C)=Sg & node(C)=endNode(Sg). % Proceed to the next segment if the car was about to leave caused segment(C)=Sg after willLeave(C) & nextSegment(C)=Sg. % The distance covered by a car which remained on the same % segment caused distance(C)=Ds+Sp after -willLeave(C) & distance(C)=Ds & speed(C)=Sp where Ds+Sp=> Ds=> positiveOrientation(C)\=positiveOrientation(C1) where C@> Ds1==modifiedDistance(C) where C\=C1. default -ahead(C1,C). % No overtaking constraint -ahead(C,C1) after ahead(C1,C). :- constants % The first car is ahead of the second car and not farther % than varsigma from it varsigmaAhead(car,car) :: sdFluent. caused varsigmaAhead(C1,C) if ahead(C1,C) & distance(C1)=Ds1 & modifiedDistance(C)=Ds where Ds1-Ds=> willLeave(C1)]. % If a car is in the middle of a segment and there is a car % varsigma ahead of it which will not leave, then its speed % will be the smaller of its maximum speed and the speed of % the car in front caused speed(C)=min(Sp,Sp1) if nextSegment(C)=none & maxSpeed(C)=Sp & varsigmaAhead(C1,C) & -willLeave(C1) & speed(C1)=Sp1. % If a car is at the end of a segment and will not leave then % it will stay where it is caused speed(C)=0 if nextSegment(C)\=none & -willLeave(C). % If a car is at the end of a segment and will enter a new seg- % ment where there is no car within varsigma, then it will % travel at its maximum speed caused speed(C)=Sp if willLeave(C) & maxSpeed(C)=Sp & [/\C1 | -varsigmaAhead(C1,C)]. % If a car is at the end of a segment and will enter a new seg- % ment where there is a car within varsigma, its speed will be % the smaller of its maximum speed and the speed of the car in % front caused speed(C)=min(Sp,Sp1) if willLeave(C) & varsigmaAhead(C1,C) & maxSpeed(C)=Sp & speed(C1)=Sp1. :- constants % Choose a new segment for a car to proceed chooseSegment(car,segment) :: exogenousAction. % Direct effect of choosing a new segment chooseSegment(C,Sg) causes nextSegment(C)=Sg. % Cannot choose the segment that is already chosen nonexecutable chooseSegment(C,Sg) if nextSegment(C)=Sg. % When a car arrives at a node ("intersection") then it may % continue on any segment that connects to that node... (lmw) constraint node(C)=startNode(Sg) ++ node(C)=endNode(Sg) after chooseSegment(C,Sg). % ...except the one it is arriving at (lmw) constraint nextSegment(C)\=Sg after segment(C)=Sg. % A car cannot arrive at a node without choosing a new segment % on which to proceed constraint -[\/Nd | node(C)=Nd] after [/\Sg | -chooseSegment(C,Sg)] & node(C)=none. % A car can't have a next segment unless it has travelled to the % end of its current segment caused nextSegment(C)=none if node(C)=none. caused nextSegment(C)=none if node(C)=startNode(segment(C)) & positiveOrientation(C). caused nextSegment(C)=none if node(C)=endNode(segment(C)) & -positiveOrientation(C). % Only cars which have selected a new segment can leave constraint willLeave(C) ->> nextSegment(C)\=none. % At most one car will leave a node and enter a new segment at % each time constraint willLeave(C) & willLeave(C1) & node(C)=node(C1) ->> nextSegment(C)\=nextSegment(C1) where C@> [\/C1 | node(C1)=node(C) & nextSegment(C1)=Sg & willLeave(C1)].