domain traffic_mdp {
requirements = {
reward-deterministic,
concurrent,
constrained-state
};
types {
intersection : object;
cell : object;
};
pvariables {
FLOWS-INTO-CELL(cell, cell) : {non-fluent, bool, default = false};
PERIMETER-INPUT-RATE(cell) : {non-fluent, real, default = 1.0};
occupied(cell) : {state-fluent, bool, default = false};
PERIMETER-EXIT-CELL(cell) : {non-fluent, bool, default = false};
light-signal1(intersection) : {state-fluent, bool, default = false};
light-signal2(intersection) : {state-fluent, bool, default = false};
PERIMETER-INPUT-CELL(cell) : {non-fluent, bool, default = false};
FLOWS-INTO-INTERSECTION-NS(cell, intersection) : {non-fluent, bool, default = false};
advance(intersection) : {action-fluent, bool, default = false};
FLOWS-INTO-INTERSECTION-EW(cell, intersection) : {non-fluent, bool, default = false};
};
cpfs {
(occupied’ ?c) = (if (PERIMETER-INPUT-CELL ?c) then (if (~ (occupied ?c)) then (Bernoulli (PERIMETER-INPUT-RATE ?c)) else (if (exists ( (?c2 : cell) ) (^ (FLOWS-INTO-CELL ?c ?c2) (~ (occupied ?c2)) )) then (KronDelta false) else (KronDelta true))) else (if (| (exists ( (?i : intersection) (?c2 : cell) ) (^ (FLOWS-INTO-INTERSECTION-NS ?c ?i) (FLOWS-INTO-CELL ?c ?c2) (light-signal2 ?i) (~ (light-signal1 ?i)) (~ (occupied ?c2)) )) (exists ( (?i : intersection) (?c2 : cell) ) (^ (FLOWS-INTO-INTERSECTION-EW ?c ?i) (FLOWS-INTO-CELL ?c ?c2) (light-signal1 ?i) (~ (light-signal2 ?i)) (~ (occupied ?c2)) )) ) then (if (~ (occupied ?c)) then (KronDelta (exists ( (?c2 : cell) ) (^ (FLOWS-INTO-CELL ?c2 ?c) (occupied ?c2) ))) else (KronDelta false)) else (if (exists ( (?i : intersection) ) (| (^ (FLOWS-INTO-INTERSECTION-NS ?c ?i) (occupied ?c) ) (^ (FLOWS-INTO-INTERSECTION-EW ?c ?i) (occupied ?c) ) )) then (KronDelta true) else (if (exists ( (?i : intersection) (?c2 : cell) ) (^ (| (FLOWS-INTO-INTERSECTION-NS ?c2 ?i) (FLOWS-INTO-INTERSECTION-EW ?c2 ?i) ) (FLOWS-INTO-CELL ?c2 ?c) )) then (if (occupied ?c) then (KronDelta (~ (exists ( (?c2 : cell) ) (^ (FLOWS-INTO-CELL ?c ?c2) (~ (occupied ?c2)) )))) else (KronDelta (| (exists ( (?i : intersection) (?c2 : cell) ) (^ (FLOWS-INTO-INTERSECTION-NS ?c2 ?i) (FLOWS-INTO-CELL ?c2 ?c) (light-signal2 ?i) (~ (light-signal1 ?i)) (occupied ?c2) )) (exists ( (?i : intersection) (?c2 : cell) ) (^ (FLOWS-INTO-INTERSECTION-EW ?c2 ?i) (FLOWS-INTO-CELL ?c2 ?c) (light-signal1 ?i) (~ (light-signal2 ?i)) (occupied ?c2) )) ))) else (if (occupied ?c) then (KronDelta (^ (~ (PERIMETER-EXIT-CELL ?c)) (~ (exists ( (?c2 : cell) ) (^ (FLOWS-INTO-CELL ?c ?c2) (~ (occupied ?c2)) ))) )) else (KronDelta (exists ( (?c2 : cell) ) (^ (FLOWS-INTO-CELL ?c2 ?c) (occupied ?c2) ))))))));
(light-signal1′ ?i) = (if (| (advance ?i) (^ (light-signal1 ?i) (light-signal2 ?i) ) (^ (~ (light-signal1 ?i)) (~ (light-signal2 ?i)) ) ) then (KronDelta (light-signal2 ?i)) else (KronDelta (light-signal1 ?i)));
(light-signal2′ ?i) = (if (| (advance ?i) (^ (light-signal1 ?i) (light-signal2 ?i) ) (^ (~ (light-signal1 ?i)) (~ (light-signal2 ?i)) ) ) then (KronDelta (~ (light-signal1 ?i))) else (KronDelta (light-signal2 ?i)));
};
reward = (sum ( (?c : cell) ) (- 0 (^ (occupied ?c) (exists ( (?c2 : cell) ) (^ (FLOWS-INTO-CELL ?c2 ?c) (occupied ?c2) )) )));
state-action-constraints {
};
}