////////////////////////////////////////////////////////////////////
// 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} [light-signal2(?i) ^ ~light-signal1(?i) ^ FLOWS-INTO-INTERSECTION-NS(?c,?i) ^ exists_{?c2 : cell} [FLOWS-INTO-CELL(?c, ?c2) ^ ~occupied(?c2)]]]
  		   						 | [exists_{?i : intersection} [light-signal1(?i) ^ ~light-signal2(?i) ^ FLOWS-INTO-INTERSECTION-EW(?c,?i) ^ exists_{?c2 : cell} [FLOWS-INTO-CELL(?c, ?c2) ^ ~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) | 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} [light-signal2(?i) ^ ~light-signal1(?i) ^ exists_{?c2 : cell} [FLOWS-INTO-INTERSECTION-NS(?c2,?i) ^ FLOWS-INTO-CELL(?c2, ?c) ^ occupied(?c2)]]]
  		   						 | [exists_{?i : intersection} [light-signal1(?i) ^ ~light-signal2(?i) ^ exists_{?c2 : cell} [FLOWS-INTO-INTERSECTION-EW(?c2,?i) ^ FLOWS-INTO-CELL(?c2, ?c) ^ 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];
//	};
}
