-
Notifications
You must be signed in to change notification settings - Fork 1
/
traffic_mdp.rddl
executable file
·147 lines (126 loc) · 7.08 KB
/
traffic_mdp.rddl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
////////////////////////////////////////////////////////////////////
// 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];
// };
}