<?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>// Place global declarations here.
clock t_sim = 0; //

const double T = 1; // 
const double T_cacc = 1;

const int N_CARS = 4;

const double alfa1 = 0.5;
const double alfa2 = 0.5;
const double alfa3 = -0.3;
const double alfa4 = -0.1;
const double alfa5 = -0.04;

const double d = 15;
broadcast chan cacc;

const double t_attack = 30;
const double A_lf = 0.08;
</declaration>
	<template>
		<name>Simulation</name>
		<declaration>clock t = 0;</declaration>
		<location id="id0" x="-42" y="-8">
			<name x="-44" y="9">STEP</name>
			<label kind="invariant" x="-52" y="35">t &lt;= T</label>
		</location>
		<init ref="id0"/>
		<transition id="id1">
			<source ref="id0"/>
			<target ref="id0"/>
			<label kind="guard" x="-178" y="-127">t &gt;= T</label>
			<label kind="synchronisation" x="-212" y="-59">cacc!</label>
			<label kind="assignment" x="-178" y="-102">t := 0</label>
			<nail x="-136" y="17"/>
			<nail x="-153" y="-51"/>
			<nail x="-110" y="-93"/>
			<nail x="-25" y="-110"/>
			<nail x="-17" y="-68"/>
		</transition>
	</template>
	<template>
		<name x="5" y="5">CarDynamic</name>
		<parameter>double start_time, double&amp; a_ref, clock&amp; a, clock&amp; v, clock&amp; x</parameter>
		<declaration>// Place local declarations here.
clock t;
clock o = 0;

//const double m = 2000.0
const double k = 25.0;
</declaration>
		<location id="id2" x="-399" y="-110">
			<name x="-416" y="-144">WAIT</name>
			<label kind="invariant" x="-476" y="-85">t_sim &lt;= start_time	 &amp;&amp;
a' == 0			 &amp;&amp;
v' == 0			 &amp;&amp;
x' == 0			 &amp;&amp;
o' == 0</label>
		</location>
		<location id="id3" x="0" y="-110">
			<name x="-10" y="-144">DYNAMICS</name>
			<label kind="invariant" x="-59" y="-68">o' == (a_ref - o)/0.2 &amp;&amp;
a' == k*o + (a_ref - o)/0.2 - k*a &amp;&amp;
v' == a &amp;&amp;
x' == v</label>
		</location>
		<init ref="id2"/>
		<transition id="id4">
			<source ref="id2"/>
			<target ref="id3"/>
			<label kind="guard" x="-306" y="-144">t_sim &gt;= start_time</label>
		</transition>
	</template>
	<template>
		<name>CarDynamicAttack</name>
		<parameter>double start_time, double&amp; a_ref, clock&amp; a, clock&amp; v, clock&amp; x, double attack_time, clock&amp; a_t, clock&amp; v_t, clock&amp; x_t</parameter>
		<declaration>// Place local declarations here.
clock t;
clock o = 0;

//const double m = 2000.0
const double k = 25.0;
</declaration>
		<location id="id5" x="-280" y="-25">
			<name x="-297" y="-59">WAIT</name>
			<label kind="invariant" x="-357" y="0">t_sim &lt;= start_time	 &amp;&amp;
o' == 0			 &amp;&amp;
a' == 0			 &amp;&amp;
v' == 0			 &amp;&amp;
x' == 0			 &amp;&amp;
a_t' == 0		 &amp;&amp;
v_t' == 0		 &amp;&amp;
x_t' == 0</label>
		</location>
		<location id="id6" x="119" y="-25">
			<name x="76" y="-59">DYNAMICS</name>
			<label kind="invariant" x="60" y="17">t_sim &lt;= attack_time &amp;&amp;
o'   == (a_ref - o)/0.2 &amp;&amp;
a'   == k*o + (a_ref - o)/0.2 - k*a &amp;&amp;
v'   == a &amp;&amp;
x'   == v &amp;&amp;
a_t' == k*o + (a_ref - o)/0.2 - k*a &amp;&amp;
v_t' == a &amp;&amp;
x_t' == v</label>
		</location>
		<location id="id7" x="748" y="-25">
			<name x="688" y="-59">DYNAMICS_ATTACK</name>
			<label kind="invariant" x="569" y="8">o'   == (a_ref - o)/0.2 &amp;&amp;
a'   == k*o + (a_ref - o)/0.2 - k*a + 0.2*M_PI*A_lf*cos(0.2*M_PI*t_sim)&amp;&amp;
v'   == a &amp;&amp;
x'   == v + 5*M_1_PI*A_lf &amp;&amp;
a_t' == k*o + (a_ref - o)/0.2 - k*a &amp;&amp;
v_t' == a &amp;&amp;
x_t' == v</label>
		</location>
		<init ref="id5"/>
		<transition id="id8">
			<source ref="id6"/>
			<target ref="id7"/>
			<label kind="guard" x="297" y="-119">t_sim &gt;= attack_time</label>
			<label kind="assignment" x="297" y="-93">v := v + 5*M_1_PI*A_lf,
x := x + 5*M_1_PI*A_lf*t_sim</label>
		</transition>
		<transition id="id9">
			<source ref="id5"/>
			<target ref="id6"/>
			<label kind="guard" x="-187" y="-59">t_sim &gt;= start_time</label>
		</transition>
	</template>
	<template>
		<name>LeaderDriver</name>
		<parameter>double &amp;a_ref</parameter>
		<declaration>clock t;
clock t1;

const double A = 0.8;
double f = 0.5;//*1e-3;
const double phase = 0;
const double offset = -0.01;
double acceleration_value = 2.0;//*1e-6;
double deceleration_value = -1.5;
const double slope = 0.5;
int mode;

const double sprint_p = 5;
const double T_sprint = sprint_p + 30;</declaration>
		<location id="id10" x="-204" y="-221">
			<name x="-221" y="-288">CONST_A</name>
			<label kind="invariant" x="-247" y="-271">t_sim &lt;= 10</label>
		</location>
		<location id="id11" x="212" y="-221">
			<name x="169" y="-254">REGIME</name>
			<label kind="invariant" x="229" y="-254">t &lt;= T</label>
		</location>
		<location id="id12" x="-901" y="-399">
			<name x="-911" y="-433">INIT</name>
			<urgent/>
		</location>
		<location id="id13" x="-204" y="59">
			<name x="-229" y="-34">SLOPE</name>
			<label kind="invariant" x="-238" y="0">t_sim &lt;= 8 &amp;&amp; t &lt;= T</label>
		</location>
		<location id="id14" x="-202" y="340">
			<name x="-212" y="272">ACCEL</name>
			<label kind="invariant" x="-246" y="289">t1 &lt;= sprint_p</label>
		</location>
		<location id="id15" x="136" y="340">
			<name x="102" y="255">FINAL_STEPS</name>
			<label kind="invariant" x="102" y="272">t1 &lt;= 30 &amp;&amp;
t &lt;= T</label>
		</location>
		<location id="id16" x="510" y="340">
			<name x="484" y="272">DECEL</name>
			<label kind="invariant" x="433" y="297">t1&lt;= T_sprint</label>
		</location>
		<branchpoint id="id17" x="-612" y="-221"/>
		<init ref="id12"/>
		<transition id="id18">
			<source ref="id15"/>
			<target ref="id15"/>
			<label kind="guard" x="42" y="399">t1 &lt;= 30 &amp;&amp;
t &gt;= T</label>
			<label kind="assignment" x="17" y="450">a_ref := 0.03*sin(1.5 * t_sim) + 0.005,
t := 0</label>
			<nail x="272" y="416"/>
			<nail x="238" y="442"/>
			<nail x="17" y="442"/>
			<nail x="0" y="408"/>
		</transition>
		<transition id="id19">
			<source ref="id15"/>
			<target ref="id16"/>
			<label kind="guard" x="238" y="340">t1 &gt;= 30</label>
			<label kind="assignment" x="238" y="357">a_ref = deceleration_value</label>
		</transition>
		<transition id="id20">
			<source ref="id14"/>
			<target ref="id15"/>
			<label kind="guard" x="-153" y="340">t1 &gt;= sprint_p</label>
			<label kind="assignment" x="-127" y="357">t := 0</label>
		</transition>
		<transition id="id21">
			<source ref="id16"/>
			<target ref="id14"/>
			<label kind="guard" x="493" y="212">t1 &gt;= T_sprint</label>
			<label kind="assignment" x="221" y="187">a_ref := acceleration_value,
t1 := 0</label>
			<nail x="680" y="340"/>
			<nail x="680" y="238"/>
			<nail x="-272" y="238"/>
			<nail x="-272" y="289"/>
		</transition>
		<transition id="id22">
			<source ref="id17"/>
			<target ref="id14"/>
			<label kind="assignment" x="-595" y="59">a_ref := acceleration_value,
mode := 2,
t1 := 0</label>
			<label kind="probability" x="-595" y="119">1</label>
			<nail x="-612" y="340"/>
		</transition>
		<transition id="id23">
			<source ref="id13"/>
			<target ref="id11"/>
			<label kind="guard" x="-34" y="-34">t_sim &gt;= 8</label>
			<label kind="assignment" x="-34" y="-8">a_ref := A*sin(f*t_sim + phase) + offset,
t := 0</label>
			<nail x="-42" y="59"/>
			<nail x="-42" y="-144"/>
		</transition>
		<transition id="id24">
			<source ref="id13"/>
			<target ref="id13"/>
			<label kind="guard" x="-272" y="161">t_sim &lt;= 8 &amp;&amp; t &gt;= T</label>
			<label kind="assignment" x="-272" y="187">a_ref := slope*t_sim,
t := 0</label>
			<nail x="-111" y="127"/>
			<nail x="-136" y="161"/>
			<nail x="-272" y="161"/>
			<nail x="-297" y="119"/>
		</transition>
		<transition id="id25">
			<source ref="id17"/>
			<target ref="id13"/>
			<label kind="assignment" x="-408" y="-136">a_ref := 0,
mode := 1</label>
			<label kind="probability" x="-527" y="-187">1</label>
		</transition>
		<transition id="id26">
			<source ref="id17"/>
			<target ref="id10"/>
			<label kind="assignment" x="-527" y="-289">a_ref := acceleration_value,
mode := 0</label>
			<label kind="probability" x="-552" y="-255">1</label>
		</transition>
		<transition id="id27" controllable="false">
			<source ref="id12"/>
			<target ref="id17"/>
			<label kind="select" x="-935" y="-331">avi: int[17, 20],
dvi: int[-17, -15],
fi: int[500, 630]</label>
			<label kind="assignment" x="-935" y="-263">f := fi / 1000.0,
acceleration_value = avi / 10.0,
deceleration_value = dvi / 10.0</label>
		</transition>
		<transition id="id28">
			<source ref="id11"/>
			<target ref="id11"/>
			<label kind="guard" x="212" y="-144">t &gt;= T</label>
			<label kind="assignment" x="118" y="-127">a_ref := A*sin(f*t_sim + phase) + offset,
t := 0</label>
			<nail x="169" y="-170"/>
			<nail x="178" y="-144"/>
			<nail x="314" y="-144"/>
			<nail x="305" y="-187"/>
		</transition>
		<transition id="id29">
			<source ref="id10"/>
			<target ref="id11"/>
			<label kind="guard" x="-60" y="-339">t_sim &gt;= 10</label>
			<label kind="assignment" x="-136" y="-297">a_ref := A*sin(f*t_sim + phase) + offset,
t := 0</label>
		</transition>
	</template>
	<template>
		<name>CACC</name>
		<parameter>double&amp; a_ref, clock&amp; a_leader, clock&amp; v_leader, clock&amp; x_leader, clock&amp; a_front, clock&amp; v_front, clock&amp; x_front, clock&amp; a_ego, clock&amp; v_ego, clock&amp; x_ego</parameter>
		<declaration>clock t = 0;</declaration>
		<location id="id30" x="-42" y="8">
			<name x="-68" y="34">STEP</name>
			<label kind="invariant" x="-85" y="59">t &lt;= T</label>
		</location>
		<init ref="id30"/>
		<transition id="id31">
			<source ref="id30"/>
			<target ref="id30"/>
			<label kind="guard" x="-296" y="-26">t &gt;= T</label>
			<label kind="synchronisation" x="-296" y="-9">cacc!</label>
			<label kind="assignment" x="-297" y="-170">t := 0,
a_ref := 	
	 alfa1*a_front + alfa2*a_leader +
	 alfa3*(v_ego - v_front) + alfa4*(v_ego-v_leader)
	 + alfa5*(x_ego - x_front + d)</label>
			<nail x="-314" y="8"/>
			<nail x="-365" y="-93"/>
			<nail x="-306" y="-178"/>
			<nail x="119" y="-178"/>
			<nail x="187" y="-102"/>
			<nail x="85" y="8"/>
		</transition>
	</template>
	<template>
		<name>Attack_1</name>
		<parameter>clock&amp; a_in, clock&amp; v_in, clock&amp; x_in, clock&amp; a_out, clock&amp; v_out, clock&amp; x_out</parameter>
		<declaration>clock t;</declaration>
		<location id="id32" x="0" y="0">
			<label kind="invariant" x="-10" y="17">t &lt;= T</label>
		</location>
		<init ref="id32"/>
		<transition id="id33">
			<source ref="id32"/>
			<target ref="id32"/>
			<label kind="guard" x="-425" y="-229">t &gt;= T</label>
			<label kind="synchronisation" x="-424" y="-17">cacc?</label>
			<label kind="assignment" x="-416" y="-187">t := 0,
a_out := a_in + A_lf*sin(2*M_PI*t_sim/10.0),
v_out := v_in - 5*M_1_PI*A_lf*cos(2*M_PI*t_sim/10.0) + 5*M_1_PI*A_lf,
x_out := x_in - 25*M_1_PI*M_1_PI*A_lf*sin(2*M_PI*t_sim/10) + 5*M_1_PI*A_lf*t_sim</label>
			<nail x="-442" y="0"/>
			<nail x="-467" y="-85"/>
			<nail x="-433" y="-195"/>
			<nail x="391" y="-195"/>
			<nail x="433" y="-102"/>
			<nail x="391" y="0"/>
		</transition>
	</template>
	<system>double a_ref[N_CARS] = {0, 0, 0, 0};

clock a[N_CARS] = {0, 0, 0, 0};
clock v[N_CARS] = {0, 0, 0, 0};
clock x[N_CARS] = {0, 0, 0, 0};

clock a_r = 0;
clock v_r = 0;
clock x_r = 0;


// Place template instantiations here.
//attack = Attack_1(a_r, v_r, x_r, a[1], v[1], x[1]);

driver = LeaderDriver(a_ref[0]);
leader = CarDynamic(0, a_ref[0], a[0], v[0], x[0]);

car1 = CarDynamicAttack(4, a_ref[1], a[1], v[1], x[1], 30, a_r, v_r, x_r);
//car1 = CarDynamic(4, a_ref[1], a[1], v[1], x[1]);
car2 = CarDynamic(8, a_ref[2], a[2], v[2], x[2]);
car3 = CarDynamic(12, a_ref[3], a[3], v[3], x[3]);

cacc1 = CACC(a_ref[1], a[0], v[0], x[0], a[0], v[0], x[0], a[1], v[1], x[1]);
cacc2 = CACC(a_ref[2], a[0], v[0], x[0], a[1], v[1], x[1], a[2], v[2], x[2]);
cacc3 = CACC(a_ref[3], a[0], v[0], x[0], a[2], v[2], x[2], a[3], v[3], x[3]);

sim = Simulation();


// List one or more processes to be composed into a system.
//system sim, driver, leader, cacc1, car1, cacc2, car2, cacc3, car3;
system sim, driver, leader, cacc1, car1, cacc2, car2, cacc3, car3;
</system>
	<simulator type="concrete">
		<plot-widget title="a">
			<expression>a_r</expression>
			<expression>a[2]</expression>
			<expression>a[3]</expression>
			<expression>a[0]</expression>
			<expression>a[1]</expression>
		</plot-widget>
		<plot-widget title="v">
			<expression>v[0]</expression>
			<expression>v[2]</expression>
			<expression>v[1]</expression>
			<expression>v[3]</expression>
		</plot-widget>
		<plot-widget title="a">
			<expression>a[2]</expression>
			<expression>a[3]</expression>
			<expression>a[0]</expression>
			<expression>a[1]</expression>
		</plot-widget>
	</simulator>
	<queries>
		<option key="--hashtable-size" value="31"/>
		<option key="--search-order" value="2"/>
		<option key="--truncation-error" value="1.0E-4"/>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>Pr[&lt;=200] ([] t_sim &gt; 5 imply x[0] &gt; x[1])</formula>
			<comment>No crash between leader and 1</comment>
			<result outcome="maybe_true" type="interval" value="≥ 0.950056 (95% CI)" timestamp="2025-04-08 14:55:02 +0200">
				<option key="--hashtable-size" value="31"/>
				<option key="--search-order" value="2"/>
				<option key="--truncation-error" value="1.0E-4"/>
				<details>≥ 0.950056 (95% CI)</details>
			</result>
		</query>
		<query>
			<formula>Pr[&lt;=200] ([] t_sim &gt; 5 imply x[0] &gt; x_r)</formula>
			<comment/>
			<result outcome="maybe_true" type="interval" value="≥ 0.950056 (95% CI)" timestamp="2025-04-08 14:55:08 +0200">
				<option key="--hashtable-size" value="31"/>
				<option key="--search-order" value="2"/>
				<option key="--truncation-error" value="1.0E-4"/>
				<details>≥ 0.950056 (95% CI)</details>
			</result>
		</query>
		<query>
			<formula>Pr[&lt;=200] ([] t_sim &gt; 9 imply x[1] &gt; x[2])</formula>
			<comment>no crash between 1 and 2</comment>
			<result outcome="maybe_true" type="interval" value="≥ 0.950056 (95% CI)" timestamp="2025-04-08 14:55:13 +0200">
				<option key="--hashtable-size" value="31"/>
				<option key="--search-order" value="2"/>
				<option key="--truncation-error" value="1.0E-4"/>
				<details>≥ 0.950056 (95% CI)</details>
			</result>
		</query>
		<query>
			<formula>Pr[&lt;=200] ([] t_sim &gt; 9 imply x_r &gt; x[2])</formula>
			<comment/>
			<result outcome="maybe_true" type="interval" value="≤ 0.0499441 (95% CI)" timestamp="2025-04-08 14:55:16 +0200">
				<option key="--hashtable-size" value="31"/>
				<option key="--search-order" value="2"/>
				<option key="--truncation-error" value="1.0E-4"/>
				<details>≤ 0.0499441 (95% CI)</details>
			</result>
		</query>
		<query>
			<formula>Pr[&lt;=200] ([] t_sim &gt; 13 imply x[2] &gt; x[3])</formula>
			<comment/>
			<option key="--hashtable-size" value="31"/>
			<option key="--search-order" value="2"/>
			<option key="--truncation-error" value="1.0E-4"/>
			<result outcome="maybe_true" type="interval" value="≥ 0.950056 (95% CI)" timestamp="2025-04-08 14:55:23 +0200">
				<option key="--hashtable-size" value="31"/>
				<option key="--search-order" value="2"/>
				<option key="--truncation-error" value="1.0E-4"/>
				<details>≥ 0.950056 (95% CI)</details>
			</result>
		</query>
	</queries>
</nta>
