////////////////////////////////////////////////////////////////////
// A simple binary version of the cell transition model (CTM) for
// modeling traffic. Based on the original CTM Tech Report and its
// specification as a factored MDP in the following papers:
//
// The Cell Transition Model: Network Traffic. Daganzo;
// Tech Report Berkeley Institute of Transport Studies, 1994.
//
// Efficient Solutions to Factored MDPs with Imprecise Transition
// Probabilities. Delgado, Sanner, de Barros, Cozman; ICAPS, 2009.
//
// Because of the binary variable and no intermediate variable
// restrictions for the IPPC 2011, this model is quite simplified
// and ignores traffic aspects such as turns and turn probabilities.
//
// Note that this model uses concurrent actions, but that the number
// of total actions will only ever be 2^(# intersections). Refer to
// the IPPC email list if you are unsure how to handle concurrent
// actions.
//
// Author: Scott Sanner (ssanner [at] gmail.com)
////////////////////////////////////////////////////////////////////
domain traffic_mdp {
requirements = {
reward-deterministic, // this domain does not use a stochastic reward
constrained-state, // this domain uses state constraints
concurrent // this domain permits multiple non-default actions
};
types {
cell : object;
intersection : object;
};
pvariables {
// Specify which cells are perimeter input cells and their input rates
PERIMETER-INPUT-CELL(cell) : { non-fluent, bool, default = false };
PERIMETER-INPUT-RATE(cell) : { non-fluent, real, default = 1.0 };
// Specify which cells are exit cells
PERIMETER-EXIT-CELL(cell) : { non-fluent, bool, default = false };
// Specify which cells flow into other cells
FLOWS-INTO-CELL(cell, cell) : { non-fluent, bool, default = false };
// Specify which cells can pass into intersection on a signal phase
FLOWS-INTO-INTERSECTION-NS(cell, intersection) : { non-fluent, bool, default = false };
FLOWS-INTO-INTERSECTION-EW(cell, intersection) : { non-fluent, bool, default = false };
// This is a simple boolean encoding of signal state for an intersection
//
// light-signal 1 2 -> effective light state
// =========================================
// 0 0 -> all red
// 0 1 -> green for north-south traffic flow
// 1 1 -> all red
// 1 0 -> green for east-west traffic flow
light-signal1(intersection) : { state-fluent, bool, default = false };
light-signal2(intersection) : { state-fluent, bool, default = false };
// Binary cell transition model (CTM): cell is either occupied or not
occupied(cell) : { state-fluent, bool, default = false };
// Do we advance this signal for an intersection to its next sequence?
advance(intersection) : { action-fluent, bool, default = false };
};
cpfs {
// Just use a finite state machine for the light-signals
// Note: a light signal that is red *must* advance to the next state…
// there would be no reason to hold a red signal indefinitely.
light-signal1′(?i) =
if (advance(?i) | (light-signal1(?i) ^ light-signal2(?i)) | (~light-signal1(?i) ^ ~light-signal2(?i)))
then // Advance to next state (see table above)
KronDelta( light-signal2(?i) )
else // No change
KronDelta( light-signal1(?i) );
light-signal2′(?i) =
if (advance(?i) | (light-signal1(?i) ^ light-signal2(?i)) | (~light-signal1(?i) ^ ~light-signal2(?i)))
then // Advance to next state (see table above)
KronDelta( ~light-signal1(?i) )
else // No change
KronDelta( light-signal2(?i) );
// Update a cell’s occupation status according to CTM rules
occupied'(?c) = // Check for perimeter cell
if (PERIMETER-INPUT-CELL(?c))
then [if (~occupied(?c))
then Bernoulli( PERIMETER-INPUT-RATE(?c) ) // Empty
else if (exists_{?c2 : cell} [FLOWS-INTO-CELL(?c, ?c2) ^ ~occupied(?c2)])
then KronDelta( false ) // Vacated
else KronDelta( true )] // Stopped
// Check for cell entering intersection on green light
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 )] // Vacated since cell enters intersection
// Check for occupied cell entering intersection (if get here, must be red)
else if (exists_{?i : intersection} [(FLOWS-INTO-INTERSECTION-NS(?c,?i) ^ occupied(?c)) | (FLOWS-INTO-INTERSECTION-EW(?c,?i) ^ occupied(?c)) ])
then KronDelta( true ) // car stuck at red light
// Check cells ?c that take traffic exiting an intersection
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))
// Can car go forward?
then KronDelta( ~exists_{?c2 : cell} FLOWS-INTO-CELL(?c, ?c2) ^ ~occupied(?c2) )
// Did a car enter from intersection?
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)]]
)]
// Must be a normal cell – normal transition rules apply
else if (occupied(?c)) // Does it empty?
then KronDelta ( ~PERIMETER-EXIT-CELL(?c) ^ ~exists_{?c2 : cell} [FLOWS-INTO-CELL(?c, ?c2) ^ ~occupied(?c2)])
else // Does it fill?
KronDelta ( exists_{?c2 : cell} [FLOWS-INTO-CELL(?c2, ?c) ^ occupied(?c2)] );
};
// Minimize congestion: this reward penalizes congested traffic defined as pairs
// of *consecutive* occupied cells
reward = sum_{?c : cell} -[occupied(?c) ^ exists_{?c2 : cell} (FLOWS-INTO-CELL(?c2, ?c) ^ occupied(?c2))];
// state-action-constraints {
// // Make sure probabilities are in correct range
// forall_{?c : cell} (PERIMETER-INPUT-RATE(?c) >= 0.0);
// forall_{?c : cell} (PERIMETER-INPUT-RATE(?c) <= 1.0);
//
// // Make sure all non-entry cells have a unique cell feeding into them
// forall_{?c : cell} [~PERIMETER-INPUT-CELL(?c) => ((sum_{?c2 : cell} FLOWS-INTO-CELL(?c2, ?c)) == 1)];
//
// // Make sure all non-exit cells feed into a unique cell
// forall_{?c : cell} [~PERIMETER-EXIT-CELL(?c) => ((sum_{?c2 : cell} FLOWS-INTO-CELL(?c, ?c2)) == 1)];
//
// // Each intersection must have at least one cell flow into it
// forall_{?i : intersection} [(sum_{?c : cell}
// (FLOWS-INTO-INTERSECTION-NS(?c, ?i) | FLOWS-INTO-INTERSECTION-EW(?c, ?i))) >= 1];
// };
}