<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.6//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_6.dtd'>
<nta>
	<declaration>/**
This case study has been published at "Correct System Design"
Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of
His 60th Birthday Oldenburg, Germany, September 8–9, 2015.

The paper "Safe and Optimal Adaptive Cruise Control" by 
Kim Guldstrand Larsen, Marius Mikucionis, Jakob Haahr Taankvist.

@incollection{cruise,
    year={2015},
    isbn={978-3-319-23505-9},
    booktitle={Correct System Design},
    volume={9360},
    series={Lecture Notes in Computer Science},
    editor={Meyer, Roland and Platzer, André and Wehrheim, Heike},
    doi={10.1007/978-3-319-23506-6_17},
    title={Safe and Optimal Adaptive Cruise Control},
    url={http://dx.doi.org/10.1007/978-3-319-23506-6_17},
    publisher={Springer International Publishing},
    author={Larsen, Kim Guldstrand and Miku\v{c}ionis, Marius and Taankvist, Jakob Haahr},
    pages={260-277},
    language={English}
}
*/

const int maxVelocity = 20;
const int minVelocity = -10;
const int radarRange = 100; /// maximum range radar can see

int distance = 10;           /// integer estimate of distance between cars

int velocityEgo;             /// integer estimate of Ego velocity
int[-2,2] accelerationEgo;   /// acceleration of Ego
broadcast chan chooseEgo;    /// signal to Ego to decide

int velocityFront;           /// integer estimate of Front velocity
int[-2,2] accelerationFront; /// acceleration of Front
broadcast chan chooseFront;  /// signal to Front to decide
broadcast chan update;       /// check if Front is still within radar range

/// Estimate velocities and distance using integers after 1s
void updateDiscrete() {
    int oldVel = velocityFront - velocityEgo;
    int newVel;
    velocityEgo = velocityEgo + accelerationEgo;
    velocityFront = velocityFront + accelerationFront;
    newVel = velocityFront - velocityEgo;
    if (distance &lt;= radarRange)
        distance += (oldVel + newVel)/2;
    else
        distance = radarRange + 1;
}

/// Continuous (realistic) state of the system:
hybrid clock rVelocityEgo;   /// velocity of Ego
hybrid clock rVelocityFront; /// velocity of Front
hybrid clock rDistance = 10; /// distance between cars
hybrid clock D; /// "cost" of distance used in strategy optimization

double relVelocity(double velFront, double velEgo, double dist) {
    if (dist &lt;= radarRange)
        return velFront - velEgo;
    else
        return 0.0;
}

/*
Hybrid clocks:
- Usually represent some continuous (dynamical) cost over the system state space.
- Can be used in rate (derivative) expressions.
- Cannot be used in constraints (guards and invariants).
- Are abstracted away and have no effect in symbolic analysis (Symbolic Simulator, queries like A[], E&lt;&gt;, TIGA safety synthesis), we can do this, because they do not influence the logic of the model.
- Are used in concrete simulations (Concrete Simulator, SMC queries like simulate, Pr, minE, maxE, E[...](max:)).
*/
</declaration>
	<template>
		<name>Ego</name>
		<location id="id0" x="102" y="-136">
			<name x="119" y="-161">Positive_acc</name>
			<label kind="comments" x="119" y="-136">Speeding up</label>
		</location>
		<location id="id1" x="102" y="68">
			<name x="60" y="85">Negative_acc</name>
			<label kind="comments" x="60" y="111">Breaking or 
driving backwards</label>
		</location>
		<location id="id2" x="-102" y="68">
			<name x="-153" y="85">No_acceleration</name>
			<label kind="comments" x="-153" y="111">Maintaining 
the same speed</label>
		</location>
		<location id="id3" x="0" y="-34">
			<name x="26" y="-59">Choose</name>
			<label kind="comments" x="26" y="-34">Make a decision</label>
			<committed/>
		</location>
		<init ref="id2"/>
		<transition id="id4">
			<source ref="id1"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="-25" y="68">chooseEgo?</label>
			<nail x="0" y="68"/>
		</transition>
		<transition id="id5">
			<source ref="id0"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="-17" y="-153">chooseEgo?</label>
			<nail x="0" y="-136"/>
		</transition>
		<transition id="id6">
			<source ref="id2"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="-93" y="17">chooseEgo?</label>
		</transition>
		<transition id="id7">
			<source ref="id3"/>
			<target ref="id1"/>
			<label kind="guard" x="26" y="9">velocityEgo &gt; minVelocity</label>
			<label kind="assignment" x="26" y="26">accelerationEgo = -2</label>
		</transition>
		<transition id="id8">
			<source ref="id3"/>
			<target ref="id0"/>
			<label kind="guard" x="26" y="-102">velocityEgo &lt; maxVelocity</label>
			<label kind="assignment" x="26" y="-85">accelerationEgo = 2</label>
		</transition>
		<transition id="id9">
			<source ref="id3"/>
			<target ref="id2"/>
			<label kind="assignment" x="-204" y="-8">accelerationEgo = 0</label>
			<nail x="-102" y="-8"/>
		</transition>
	</template>
	<template>
		<name>Front</name>
		<location id="id10" x="-340" y="-306">
			<name x="-382" y="-340">Faraway</name>
			<label kind="comments" x="-314" y="-340">Beyond radar range</label>
		</location>
		<location id="id11" x="102" y="-136">
			<name x="119" y="-153">Positive_acc</name>
		</location>
		<location id="id12" x="102" y="68">
			<name x="110" y="85">Negative_acc</name>
		</location>
		<location id="id13" x="-102" y="68">
			<name x="-153" y="85">No_acceleration</name>
		</location>
		<location id="id14" x="0" y="-34">
			<name x="17" y="-42">Choose</name>
			<committed/>
		</location>
		<location id="id15" x="-340" y="-238">
			<committed/>
		</location>
		<location id="id16" x="-340" y="-153">
			<committed/>
		</location>
		<branchpoint id="id17" x="-340" y="-195"/>
		<init ref="id13"/>
		<transition id="id18">
			<source ref="id17"/>
			<target ref="id10"/>
			<nail x="-374" y="-195"/>
			<nail x="-374" y="-289"/>
		</transition>
		<transition id="id19">
			<source ref="id17"/>
			<target ref="id16"/>
		</transition>
		<transition id="id20" controllable="false">
			<source ref="id15"/>
			<target ref="id17"/>
		</transition>
		<transition id="id21" controllable="false">
			<source ref="id12"/>
			<target ref="id10"/>
			<label kind="guard" x="-119" y="-340">distance &gt; radarRange</label>
			<label kind="synchronisation" x="-119" y="-323">update?</label>
			<label kind="assignment" x="-119" y="-306">distance = radarRange+1,
accelerationFront = 0</label>
			<nail x="264" y="68"/>
			<nail x="264" y="-306"/>
		</transition>
		<transition id="id22" controllable="false">
			<source ref="id11"/>
			<target ref="id10"/>
			<label kind="guard" x="-119" y="-255">distance &gt; radarRange</label>
			<label kind="synchronisation" x="-119" y="-238">update?</label>
			<label kind="assignment" x="-119" y="-221">distance = radarRange+1,
accelerationFront = 0</label>
			<nail x="102" y="-238"/>
			<nail x="-119" y="-238"/>
		</transition>
		<transition id="id23" controllable="false">
			<source ref="id13"/>
			<target ref="id10"/>
			<label kind="guard" x="-382" y="17">distance &gt; radarRange</label>
			<label kind="synchronisation" x="-382" y="34">update?</label>
			<label kind="assignment" x="-382" y="51">distance = radarRange+1,
accelerationFront = 0</label>
			<nail x="-391" y="68"/>
			<nail x="-391" y="-306"/>
		</transition>
		<transition id="id24" controllable="false">
			<source ref="id12"/>
			<target ref="id14"/>
			<label kind="synchronisation" x="-25" y="68">chooseFront?</label>
			<nail x="0" y="68"/>
		</transition>
		<transition id="id25" controllable="false">
			<source ref="id11"/>
			<target ref="id14"/>
			<label kind="synchronisation" x="-17" y="-153">chooseFront?</label>
			<nail x="0" y="-136"/>
		</transition>
		<transition id="id26" controllable="false">
			<source ref="id13"/>
			<target ref="id14"/>
			<label kind="synchronisation" x="-93" y="17">chooseFront?</label>
		</transition>
		<transition id="id27" controllable="false">
			<source ref="id14"/>
			<target ref="id12"/>
			<label kind="guard" x="26" y="9">velocityFront &gt; minVelocity</label>
			<label kind="assignment" x="26" y="26">accelerationFront = -2</label>
		</transition>
		<transition id="id28" controllable="false">
			<source ref="id14"/>
			<target ref="id11"/>
			<label kind="guard" x="26" y="-102">velocityFront &lt; maxVelocity</label>
			<label kind="assignment" x="26" y="-85">accelerationFront = 2</label>
		</transition>
		<transition id="id29" controllable="false">
			<source ref="id14"/>
			<target ref="id13"/>
			<label kind="assignment" x="-204" y="-8">accelerationFront = 0</label>
			<nail x="-102" y="-8"/>
		</transition>
		<transition id="id30" controllable="false">
			<source ref="id10"/>
			<target ref="id15"/>
			<label kind="synchronisation" x="-365" y="-280">chooseFront?</label>
		</transition>
		<transition id="id31" controllable="false">
			<source ref="id16"/>
			<target ref="id14"/>
			<label kind="select" x="-331" y="-127">i:int[minVelocity,maxVelocity]</label>
			<label kind="guard" x="-331" y="-110">i &lt;= velocityEgo</label>
			<label kind="assignment" x="-331" y="-93">velocityFront = i,
distance = radarRange,
rVelocityFront = i,
rDistance = radarRange</label>
			<label kind="comments" x="-314" y="-170">Back to radar range
with arbitrary velocity</label>
			<nail x="-340" y="-34"/>
		</transition>
	</template>
	<template>
		<name>Decisions</name>
		<declaration>clock timer;</declaration>
		<location id="id32" x="-68" y="-238">
			<name x="-85" y="-272">Done</name>
			<urgent/>
		</location>
		<location id="id33" x="-238" y="-238">
			<name x="-272" y="-272">FrontNext</name>
			<urgent/>
		</location>
		<location id="id34" x="-238" y="-187">
			<name x="-255" y="-170">Wait</name>
			<label kind="invariant" x="-272" y="-153">timer &lt;= 1</label>
		</location>
		<location id="id35" x="-408" y="-238">
			<name x="-433" y="-272">EgoNext</name>
			<label kind="comments" x="-476" y="-323">Every second Ego and Front may change their driving.
Ego updates first as they cannot instantly know Front's intentions.</label>
			<urgent/>
		</location>
		<init ref="id35"/>
		<transition id="id36" controllable="false">
			<source ref="id34"/>
			<target ref="id35"/>
			<label kind="guard" x="-408" y="-212">timer == 1</label>
			<label kind="assignment" x="-408" y="-195">updateDiscrete()</label>
		</transition>
		<transition id="id37" controllable="false">
			<source ref="id32"/>
			<target ref="id34"/>
			<label kind="synchronisation" x="-161" y="-195">update!</label>
			<label kind="assignment" x="-161" y="-212">timer = 0</label>
		</transition>
		<transition id="id38" controllable="false">
			<source ref="id33"/>
			<target ref="id32"/>
			<label kind="synchronisation" x="-204" y="-255">chooseFront!</label>
		</transition>
		<transition id="id39" controllable="false">
			<source ref="id35"/>
			<target ref="id33"/>
			<label kind="synchronisation" x="-365" y="-255">chooseEgo!</label>
		</transition>
	</template>
	<template>
		<name>Dynamics</name>
		<location id="id40" x="-153" y="-144">
			<label kind="invariant" x="-315" y="-127">rVelocityEgo' == accelerationEgo &amp;&amp;
rVelocityFront' == accelerationFront &amp;&amp;
rDistance' == relVelocity(rVelocityFront,rVelocityEgo,rDistance)
&amp;&amp; D' == rDistance</label>
			<label kind="comments" x="-314" y="-263">Continuous dynamics:
a'(t) == 0    // discrete changes
v'(t) == a(t) // velocity
d'(t) == v(t) // distance
D'(t) == d(t) // "cost" of distance</label>
		</location>
		<init ref="id40"/>
	</template>
	<system>clock time;
system Ego, Front, Decisions, Dynamics;
    </system>
	<simulator type="concrete">
		<plot-widget title="distance">
			<expression>distance</expression>
			<expression>rDistance</expression>
		</plot-widget>
	</simulator>
	<queries>
		<option key="--discretization" value="0.5"/>
		<query>
			<formula>// Validate the continuous dynamics with integer approximation:</formula>
			<comment/>
		</query>
		<query>
			<formula>simulate [&lt;=100] { rVelocityFront, velocityFront }</formula>
			<comment>Inspect that velocityFront approximates the dynamical state of rVelocityFront.
Click "Check", then right-click the property and inspect the plot.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100; 100] { rVelocityFront - velocityFront }</formula>
			<comment>Inspect the difference between dynamical and approximated velocity of Front.
Expect the difference to be in between -2 and 2.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100] { rVelocityEgo, velocityEgo }</formula>
			<comment>Inspect that velocityEgo approximates the dynamical state of rVelocityEgo.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100; 100] { rVelocityEgo - velocityEgo }</formula>
			<comment>Inspect the difference between dynamical and approximated velocity of Ego.
Expect the difference to be in between -2 and 2.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100] { rDistance, distance }</formula>
			<comment>Inspect that the distance approximates the dynamical state of rDistance.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=10000] { rDistance - distance }</formula>
			<comment>Inspect the difference between the real and approximated distance.
Expect some almost random fluctuations, but the long term trend should be around zero, i.e. the approximation does not diverge from the dynamical distance.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>// Safety issues with unconstrained behavior (both cars can do arbitrary decisions):</formula>
			<comment/>
		</query>
		<query>
			<formula>A[] distance &gt; 5                                              // false</formula>
			<comment>Is the distance between cars always greater than 5m? i.e. are there no colisions?
Expect false in seconds.</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100] (&lt;&gt; distance &lt;= 5)                                  // ~0.93</formula>
			<comment>What is the probability of cars crashing?
Expect 0.93 in 10s, i.e. the cars crash almost surely.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100; 100] { rDistance, distance, 5, 100 }</formula>
			<comment>Inspect 100 trajectories of distance variables over time.
Expect the values to vary widely between -2000 and +100.
Values lower than 5 correspond to crash. There are many crashes.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>// Compute and inspect the safe strategy (restricts behavior to safe states):</formula>
			<comment/>
		</query>
		<query>
			<formula>strategy Safe = control: A[] distance &gt; 5 </formula>
			<comment>Find a safe strategy where the distance is kept greater than 5m.
Expect success within 10s.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100] { accelerationFront - accelerationEgo, rVelocityFront-rVelocityEgo, rDistance} under Safe</formula>
			<comment>Validate the state dynamics of the safe strategy: the trajectories of relative acceleration, speed and distance between cars.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100] { rDistance, distance, 5, 100 } under Safe</formula>
			<comment>Inspect 100 trajectories of distance variables over time while using the safe strategy.
Expect trajectories to vary between 5 and 200, i.e. no crashes.</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100] (&lt;&gt; distance &lt;= 5) under Safe                       // &lt;0.01</formula>
			<comment>What is the probability of cars crashing while using safe strategy?
Expect &lt;0.01 in 15s (cannot find a single counter-exmple)</comment>
		</query>
		<query>
			<formula>A[] distance &gt; 5 under Safe                                   // true</formula>
			<comment>Is the safe strategy really safe?
Prove by exhaustive exploration.
Expect true (satisfied).</comment>
		</query>
		<query>
			<formula>inf: distance under Safe                                      // &gt;=6</formula>
			<comment>Find the smallest distance between cars by exhaustive search.
Expect the distance to be greater than 6, i.e. no crash.</comment>
		</query>
		<query>
			<formula>E[&lt;=100;100](min:rDistance) under Safe</formula>
			<comment>Estimate the mean of minimum distance between cars.
Expect about ~9m in between cars.
Conclusion: Ego can successfully outmaneuver Front with very safe distance ahead.</comment>
		</query>
		<query>
			<formula>E[&lt;=100;100](max:rDistance) under Safe</formula>
			<comment>Estimate the mean of maximum distance between cars.
Expect ~100m
Conclusion: Front may run away beyound the reach of the radar, i.e. the progress is not guaranteed with Safe strategy.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100; 100] { rVelocityFront-rVelocityEgo } under Safe</formula>
			<comment>Inspect the speed difference between cars of Safe strategy.
Negative speed means Ego car is approaching the front car (dangerous).
Observe that the speed does not go below -16 and stays mostly between -6 and 6.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>// Optimize (refine) the safe strategy into safeFast and inspect:</formula>
			<comment/>
		</query>
		<query>
			<formula>strategy Safe_Fast = minE(D) [&lt;=105] {}-&gt;{}: &lt;&gt; time &gt;= 100 under Safe
			</formula>
			<comment>Maximize the progress by minimizing the cumulative distance between cars while driving safely.
Takes up to 30s with the Discretization step size set to 0.5 (Options-&gt;Statistical parameters).</comment>
			<option key="--discretization" value="0.5"/>
		</query>
		<query>
			<formula>simulate [&lt;=100] { accelerationFront - accelerationEgo, rVelocityFront-rVelocityEgo, rDistance} under Safe_Fast</formula>
			<comment>Validate the state dynamics of the safeFast strategy: the trajectories of relative acceleration, speed and distance between cars.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=100; 100] { rDistance, distance, 5, 100 } under Safe_Fast</formula>
			<comment>Inspect the distances of the safeFast strategy:
the distance is always greater than 5 (safe),
and it does not allow the front car to go further than ~50m ahead 
(does not reach the limit 200), making the most possible progress.</comment>
		</query>
		<query>
			<formula>E[&lt;=100;100](min:rDistance) under Safe_Fast</formula>
			<comment>Estimate the mean of minimum distance between cars with Safe_Fast strategy.
Expect ~7.5m, the plot shows the least minimum is 6m.
Conclusion: Safe_Fast maintains shorter distance than Safe on average, but still within very safe distance.</comment>
		</query>
		<query>
			<formula>E[&lt;=100;100](max:rDistance) under Safe_Fast</formula>
			<comment>Estimate the mean of maximum distance.
Expect ~28m, the plot shows the greatest maximum is 42m.
Conclusion: Safe_Fast does not let Front car to run away from Ego's radar, i.e. it guarantees progress (as much as Front allows).</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>// Compute minimum safe distances for each relative speed value:</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo == -16}: distance under Safe  //  &gt;=MAXINT, no such states</formula>
			<comment>Find the minimum safe distance when the relative speed is -16 (Front is approaching Ego)</comment>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo == -14}: distance under Safe  // &gt;=55</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo == -12}: distance under Safe  // &gt;=42</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo == -10}: distance under Safe  // &gt;=31</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  -8}: distance under Safe  // &gt;=22</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  -6}: distance under Safe  // &gt;=15</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  -4}: distance under Safe  // &gt;=10</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  -2}: distance under Safe  // &gt;= 7</formula>
			<comment>Find the minimum safe distance when the relative speed is -2 (Front is approaching Ego)</comment>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==   0}: distance under Safe  // &gt;= 6</formula>
			<comment>Find the minimum safe distance when the relative speed is 0 (Front and Ego maintain the same speed)</comment>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==   2}: distance under Safe  // &gt;= 7
			</formula>
			<comment>Find the minimum safe distance when the relative speed is 2 (Front is speeding away from Ego)</comment>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==   4}: distance under Safe  // &gt;=10</formula>
			<comment>Find the minimum safe distance when the relative speed is 2 (Front is speeding away from Ego)</comment>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==   6}: distance under Safe  // &gt;=13</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==   8}: distance under Safe  // &gt;=18</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  10}: distance under Safe  // &gt;=23</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  12}: distance under Safe  // &gt;=28</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  14}: distance under Safe  // &gt;=35</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  16}: distance under Safe  // &gt;=42</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  18}: distance under Safe  // &gt;=51</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  20}: distance under Safe  // &gt;=60</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  22}: distance under Safe  // &gt;=73</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  24}: distance under Safe  // &gt;=86</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  26}: distance under Safe  // &gt;=101</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  28}: distance under Safe  // &gt;=101</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  30}: distance under Safe  // &gt;=101</formula>
			<comment/>
		</query>
		<query>
			<formula>inf{velocityFront - velocityEgo ==  32}: distance under Safe  // &gt;=MAXINT, no such states</formula>
			<comment/>
		</query>
	</queries>
</nta>
