<?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>/**
I am now certain that this model is associated with the unpublished paper 

Proving and Improving Model Predictive Control of DC-DC Boost Converters
Tomislav Dragičević1 , Peter G. Jensen , Kim G. Larsen , Adrien Le Coënt , Mateja Novak , and Ulrik Nyman

See also source number 7 in that paper:
7. Karamanakos, P., Geyer, T., Manias, S.: Direct voltage control of dc–dc boost converters using enumeration-based model predictive control. IEEE Transactions on Power Electronics 29(2), 968–978 (2014)
*/


// Place global declarations here.
broadcast chan tick, tock;
broadcast chan on, off;
urgent broadcast chan urg;
int x_R = 30; // system load
clock x1 = 0.5; // Current
clock x2 = 15.0; // Voltage
clock time;

int switches;
int number_deaths; 

const double x_L = 450e-6;  // capacitor
const double x_RL = 0.3;   
const double x_Co = 220e-6; 
const double x_vs = 10.0;  // input voltage

const double x1ref = 0.35;    // Target values
const double x2ref = 15.0;    // Optimize to stay as close as possible

const double scale = 1.0/0.00005;

</declaration>
	<template>
		<name x="5" y="5">Converter</name>
		<location id="id0" x="0" y="0">
			<name x="-51" y="-17">d1u1</name>
			<label kind="invariant" x="-93" y="-102">x1'==(((-x_RL/x_L)*x1)+(x_vs/x_L))/scale &amp;&amp;
x2'==(-(1.0/(x_Co*x_R))*x2)/scale</label>
			<label kind="exponentialrate" x="-17" y="8">1</label>
			<label kind="comments" x="-93" y="-144">X'=A2*x+B,
d_aux = 1</label>
		</location>
		<location id="id1" x="229" y="0">
			<name x="212" y="-34">d1u0</name>
			<label kind="invariant" x="280" y="-102">x1'==((-x_RL/x_L)*x1+(-1.0/x_L)*x2+(x_vs/x_L))/scale &amp;&amp;
x2'==((1.0/x_Co)*x1+(-1.0/(x_Co*x_R))*x2)/scale</label>
			<label kind="exponentialrate" x="212" y="17">1</label>
			<label kind="comments" x="280" y="-144">X'=A1*x+B,
d_aux = 1</label>
		</location>
		<location id="id2" x="229" y="153">
			<name x="212" y="161">d0u0</name>
			<label kind="invariant" x="255" y="136">x1'==0 &amp;&amp;
x2'==((-1.0/(x_Co*x_R))*x2)/scale</label>
			<label kind="exponentialrate" x="221" y="204">1</label>
			<label kind="comments" x="255" y="204">X'=A2*x+B,
d_aux = 0</label>
		</location>
		<location id="id3" x="119" y="0">
			<name x="102" y="17">pd1u1</name>
			<urgent/>
		</location>
		<location id="id4" x="348" y="0">
			<name x="365" y="-8">pd1u0</name>
			<urgent/>
		</location>
		<location id="id5" x="0" y="153">
			<name x="-68" y="144">pu0d0</name>
			<urgent/>
		</location>
		<init ref="id3"/>
		<transition id="id6" controllable="false">
			<source ref="id1"/>
			<target ref="id4"/>
			<label kind="synchronisation" x="272" y="-17">tock?</label>
		</transition>
		<transition id="id7" controllable="false">
			<source ref="id4"/>
			<target ref="id1"/>
			<label kind="synchronisation" x="272" y="17">off?</label>
			<nail x="289" y="17"/>
		</transition>
		<transition id="id8" controllable="false">
			<source ref="id5"/>
			<target ref="id2"/>
			<label kind="synchronisation" x="102" y="178">off?</label>
			<nail x="119" y="178"/>
		</transition>
		<transition id="id9" controllable="false">
			<source ref="id2"/>
			<target ref="id5"/>
			<label kind="synchronisation" x="93" y="136">tock?</label>
		</transition>
		<transition id="id10" controllable="false">
			<source ref="id3"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="42" y="25">on?</label>
			<nail x="59" y="17"/>
		</transition>
		<transition id="id11" controllable="false">
			<source ref="id0"/>
			<target ref="id3"/>
			<label kind="synchronisation" x="42" y="-17">tock?</label>
		</transition>
		<transition id="id12" controllable="false">
			<source ref="id4"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="127" y="-59">on?</label>
			<label kind="assignment" x="102" y="-42">switches++</label>
			<nail x="348" y="-42"/>
			<nail x="0" y="-42"/>
		</transition>
		<transition id="id13" controllable="false">
			<source ref="id5"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="0" y="59">on?</label>
			<label kind="assignment" x="0" y="76">switches++</label>
		</transition>
		<transition id="id14" controllable="false">
			<source ref="id1"/>
			<target ref="id2"/>
			<label kind="guard" x="238" y="59">x1&lt;=0</label>
			<label kind="synchronisation" x="238" y="76">urg!</label>
		</transition>
		<transition id="id15" controllable="false">
			<source ref="id3"/>
			<target ref="id1"/>
			<label kind="synchronisation" x="153" y="-17">off?</label>
			<label kind="assignment" x="136" y="0">switches++</label>
		</transition>
	</template>
	<template>
		<name>Controller</name>
		<location id="id16" x="-221" y="-85">
			<committed/>
		</location>
		<location id="id17" x="-221" y="-8">
		</location>
		<init ref="id16"/>
		<transition id="id18">
			<source ref="id16"/>
			<target ref="id17"/>
			<label kind="synchronisation" x="-161" y="-25">off!</label>
			<nail x="-161" y="-8"/>
		</transition>
		<transition id="id19">
			<source ref="id16"/>
			<target ref="id17"/>
			<label kind="synchronisation" x="-306" y="-25">on!</label>
			<nail x="-280" y="-8"/>
		</transition>
		<transition id="id20" controllable="false">
			<source ref="id17"/>
			<target ref="id16"/>
			<label kind="synchronisation" x="-238" y="-42">tock?</label>
		</transition>
	</template>
	<template>
		<name>Monitor</name>
		<declaration>clock dist;</declaration>
		<location id="id21" x="-459" y="-34">
			<label kind="invariant" x="-544" y="-25">dist'==fabs(x2-x2ref)</label>
		</location>
		<init ref="id21"/>
	</template>
	<template>
		<name>Timer</name>
		<declaration>clock x;</declaration>
		<location id="id22" x="0" y="0">
			<label kind="invariant" x="-10" y="17">x&lt;=1</label>
		</location>
		<location id="id23" x="-76" y="-85">
			<urgent/>
		</location>
		<init ref="id22"/>
		<transition id="id24" controllable="false">
			<source ref="id23"/>
			<target ref="id22"/>
			<label kind="synchronisation" x="-76" y="-42">tock!</label>
		</transition>
		<transition id="id25" controllable="false">
			<source ref="id22"/>
			<target ref="id23"/>
			<label kind="guard" x="-33" y="-119">x&gt;=1</label>
			<label kind="synchronisation" x="-33" y="-102">tick!</label>
			<label kind="assignment" x="-33" y="-85">x=0</label>
			<nail x="25" y="-85"/>
		</transition>
	</template>
	<template>
		<name>Load</name>
		<location id="id26" x="0" y="0">
		</location>
		<location id="id27" x="119" y="-17">
			<committed/>
		</location>
		<init ref="id26"/>
		<transition id="id28" controllable="false">
			<source ref="id27"/>
			<target ref="id26"/>
			<label kind="select" x="76" y="17">i:int[-30,30]</label>
			<label kind="guard" x="76" y="51">x_R + i &gt;= 30 &amp;&amp; x_R + i &lt;= 200</label>
			<label kind="assignment" x="76" y="34">x_R= x_R + i</label>
			<nail x="127" y="17"/>
		</transition>
		<transition id="id29" controllable="false">
			<source ref="id26"/>
			<target ref="id27"/>
			<label kind="synchronisation" x="42" y="-34">tick?</label>
		</transition>
	</template>
	<template>
		<name>SimpleLoad</name>
		<location id="id30" x="0" y="0">
		</location>
		<location id="id31" x="119" y="-17">
			<committed/>
		</location>
		<init ref="id30"/>
		<transition id="id32" controllable="false">
			<source ref="id31"/>
			<target ref="id30"/>
			<label kind="select" x="76" y="17">i:int[-1,1]</label>
			<label kind="guard" x="76" y="51">x_R + i*30 &gt;= 30 &amp;&amp; x_R + i*30 &lt;= 200 &amp;&amp; i != 0</label>
			<label kind="assignment" x="76" y="34">x_R= x_R + i*30</label>
			<nail x="127" y="17"/>
		</transition>
		<transition id="id33" controllable="false">
			<source ref="id30"/>
			<target ref="id31"/>
			<label kind="synchronisation" x="42" y="-34">tick?</label>
		</transition>
	</template>
	<system>system Converter, Controller,Load, Timer, Monitor;
</system>
	<queries>
		<option key="--alpha" value="0.01"/>
		<option key="--beta" value="0.01"/>
		<option key="--repeat-samples" value="20"/>
		<option key="--epsilon" value="0.01"/>
		<option key="--out-of-bounds" value="2"/>
		<query>
			<formula>Pr[&lt;=50;10000] ([] x1 &lt; 4 &amp;&amp; x2 &gt; 14.5 &amp;&amp; x2 &lt; 15.5 )</formula>
			<comment>Expect: &lt;=0.005 | 10 seconds

Compute the probability that the system is safe with no strategy (random actions).</comment>
		</query>
		<query>
			<formula>strategy safe = acontrol: A[] true { x_R[30, 201], x1[0, 4]:40, x2[14.5, 15.5]:20 }</formula>
			<comment>Expect: "Strategy found" | 1500 seconds

Approximate safe strategy for staying within given bounds. 
Notice the setting in "Options &gt; Approximate-control parameters... &gt; How to handle leaving bounds" is set to "Enforce staying within bounds".</comment>
		</query>
		<query>
			<formula>saveStrategy("converter-safe.strategy.json", safe)</formula>
			<comment>Expect: 1 second

Save the strategy to disc. The file will appear in the documents folder or home folder, depending on the system.
The query also supports file-paths for saving to other folders.</comment>
		</query>
		<query>
			<formula>strategy safe = loadStrategy("converter-safe.strategy.json")</formula>
			<comment>Expect: 1 second

Load a strategy that has been previously saved.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>Pr[&lt;=50;10000] ([] x1 &lt; 4 &amp;&amp; x2 &gt; 14.5 &amp;&amp; x2 &lt; 15.5 ) under safe</formula>
			<comment>Expect: &gt;= 0.9995 | 10 seconds

Compute the probability that the strategy "safe" keeps the current and voltage within specified bounds.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>strategy S = minE(Monitor.dist + switches) [&lt;=1000] {Converter.location} -&gt; {x1, x2}: &lt;&gt; time &gt;= 1000 under safe</formula>
			<comment>Expect: "strategy found" | 200 seconds
Lean a strategy "S" under the strategy "safe" to minimize the expression `Monitor.dist + switches`. I.e. keep close to the reference value while limiting number of switches.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=120;20] {x1,x2, 7 + Converter.d1u1, 9 + Converter.d1u0, 11 + Converter.d0u0, fabs(x2-x2ref), 14.8,  15.2 , 4} under S</formula>
			<comment>Expect: 1 second

Simulation showing the behaviour of the strategy "S". It shows respectively
 - The current, x1
 - The voltage, x2
 - A plot indicating when the circuit is in state d1u1
 - A plot indicating when the circuit is in state d1u0
 - A plot indicating when the circuit is in state d0u0
 - The distance to the reference voltage
 - min voltage
 - max voltage
 - max current</comment>
		</query>
		<query>
			<formula>simulate [&lt;=120;2] {x_R}</formula>
			<comment>Expect: 1 second

Simulation showing the varying resistance of the consumer. The consumer is part of the environment.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=120;10] {x1, x2, 14.5,  15.5 , 4}</formula>
			<comment>Expect: 1 second

Simulation showing the behaviour under no strategy (random actions). It shows respectively
 - The current, x1
 - The voltage, x2
 - min voltage
 - max voltage
 - max current</comment>
		</query>
		<query>
			<formula>simulate [&lt;=120;10] {x1, x2, 14.5,  15.5 , 4} under safe</formula>
			<comment>Expect: 1 second

Simulation showing the behaviour under strategy "safe". When there are multiple actions available in "safe" it picks one at random (uniformly). It shows respectively
 - The current, x1
 - The voltage, x2
 - min voltage
 - max voltage
 - max current</comment>
		</query>
		<query>
			<formula>simulate [&lt;=120;10] {x1, x2, 14.5,  15.5 , 4} under S</formula>
			<comment>Expect: 1 second

Simulation showing the behaviour under the safe and optimal strategy "S". It shows respectively
 - The current, x1
 - The voltage, x2
 - min voltage
 - max voltage
 - max current</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>E[&lt;=120;100] (max: switches)</formula>
			<comment>Expect: ±61 | 1 second

Estimate the number of switches under no strategy. (Random actions)</comment>
		</query>
		<query>
			<formula>E[&lt;=120;100] (max: switches) under safe</formula>
			<comment>Expect: ±45 | 1 second

Estimate the number of switches under strategy "safe".  When there are multiple actions available in "safe" it picks one at random (uniformly).</comment>
		</query>
		<query>
			<formula>E[&lt;=120;100] (max: switches) under S</formula>
			<comment>Expect: 34| 1 second

Estimate the number of switches under strategy "S".</comment>
		</query>
		<query>
			<formula>E[&lt;=120;100] (max: Monitor.dist)</formula>
			<comment>Expect: 1090 | 1 second

Estimate the accumulated distance to the reference value under no strategy. (Random actions)</comment>
		</query>
		<query>
			<formula>E[&lt;=120;100] (max: Monitor.dist) under safe</formula>
			<comment>Expect: 25 | 1 second

Estimate the accumulated distance to the reference value under strategy "safe".  When there are multiple actions available in "safe" it picks one at random (uniformly).</comment>
		</query>
		<query>
			<formula>E[&lt;=120;100] (max: Monitor.dist) under S</formula>
			<comment>Expect: 10 | 1 second

Estimate the accumulated distance to the reference value under strategy "S".</comment>
		</query>
	</queries>
</nta>
