<?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.
double w = 1.0;    // water level
double c = 0.0;    // cost

int steps = 0;     // Used in the termination condition for learning query</declaration>
	<template>
		<name x="5" y="5">WaterTank</name>
		<declaration>// Place local declarations here.
</declaration>
		<location id="id0" x="357" y="-34">
			<urgent/>
		</location>
		<location id="id1" x="195" y="-34">
			<urgent/>
		</location>
		<location id="id2" x="34" y="-34">
			<urgent/>
		</location>
		<location id="id3" x="-161" y="-34">
			<urgent/>
		</location>
		<location id="id4" x="-289" y="-42">
			<urgent/>
		</location>
		<location id="id5" x="493" y="-34">
			<urgent/>
		</location>
		<location id="id6" x="629" y="-34">
			<urgent/>
		</location>
		<init ref="id4"/>
		<transition id="id7">
			<source ref="id6"/>
			<target ref="id4"/>
			<label kind="assignment" x="697" y="8">w = w + 0.5,
c = c + w,
steps += 1</label>
			<nail x="688" y="8"/>
			<nail x="688" y="76"/>
			<nail x="-348" y="76"/>
			<nail x="-348" y="-42"/>
		</transition>
		<transition id="id8">
			<source ref="id5"/>
			<target ref="id6"/>
			<label kind="assignment" x="518" y="0">w = w - 0.5,
c = c + w,
steps += 1</label>
			<nail x="561" y="0"/>
		</transition>
		<transition id="id9">
			<source ref="id5"/>
			<target ref="id6"/>
			<label kind="assignment" x="518" y="-127">w = w + 0.5,
c = c + w,
steps += 1</label>
			<nail x="561" y="-68"/>
		</transition>
		<transition id="id10">
			<source ref="id0"/>
			<target ref="id5"/>
			<label kind="assignment" x="391" y="8">w = w - 1,
c = c + w,
steps += 1</label>
			<nail x="416" y="0"/>
		</transition>
		<transition id="id11">
			<source ref="id0"/>
			<target ref="id5"/>
			<label kind="assignment" x="374" y="-127">w = w + 0,
c = c + w,
steps += 1</label>
			<nail x="425" y="-59"/>
		</transition>
		<transition id="id12">
			<source ref="id6"/>
			<target ref="id4"/>
			<label kind="assignment" x="697" y="-136">w = w + 1.5,
c = c + w,
steps += 1</label>
			<nail x="688" y="-76"/>
			<nail x="688" y="-136"/>
			<nail x="-348" y="-136"/>
			<nail x="-348" y="-42"/>
		</transition>
		<transition id="id13">
			<source ref="id1"/>
			<target ref="id0"/>
			<label kind="assignment" x="221" y="0">w = w + 1,
c = c + w,
steps += 1</label>
			<nail x="272" y="-8"/>
		</transition>
		<transition id="id14">
			<source ref="id1"/>
			<target ref="id0"/>
			<label kind="assignment" x="229" y="-127">w = w + 2,
c = c + w,
steps += 1</label>
			<nail x="272" y="-59"/>
		</transition>
		<transition id="id15">
			<source ref="id2"/>
			<target ref="id1"/>
			<label kind="assignment" x="59" y="-127">w = w + 0,
c = c + w,
steps += 1</label>
			<nail x="119" y="-59"/>
		</transition>
		<transition id="id16">
			<source ref="id2"/>
			<target ref="id1"/>
			<label kind="assignment" x="51" y="0">w = w - 1,
c = c + w,
steps += 1</label>
			<nail x="119" y="-8"/>
		</transition>
		<transition id="id17">
			<source ref="id3"/>
			<target ref="id2"/>
			<label kind="assignment" x="-102" y="0">w = w - 0.5,
c = c + w,
steps += 1</label>
			<nail x="-51" y="0"/>
		</transition>
		<transition id="id18">
			<source ref="id3"/>
			<target ref="id2"/>
			<label kind="assignment" x="-102" y="-127">w = w + 0.5,
c = c + w,
steps += 1</label>
			<nail x="-60" y="-68"/>
		</transition>
		<transition id="id19">
			<source ref="id4"/>
			<target ref="id3"/>
			<label kind="assignment" x="-272" y="-8">w = w + 0.5,
c = c + w,
steps += 1</label>
			<nail x="-229" y="-8"/>
		</transition>
		<transition id="id20">
			<source ref="id4"/>
			<target ref="id3"/>
			<label kind="assignment" x="-272" y="-127">w = w + 1.5,
c = c + w,
steps += 1</label>
			<nail x="-229" y="-68"/>
		</transition>
	</template>
	<system>system WaterTank;
</system>
	<queries>
		<option key="--out-of-bounds" value="2"/>
		<query>
			<formula>simulate[#&lt;=100] { w, 0, 10 }</formula>
			<comment>Expect: 1 second.

Simulate a run for 100 steps, showing water-level w.
Without a strategy, the system will pick randomly among available edges.
Note how this random agent will not keep the water-tank within its safe limits of 0 to 10</comment>
		</query>
		<query>
			<formula>E[#&lt;=100;100] (max: c)</formula>
			<comment>Expect: 1900 ± 60 | 1 second

Estimate the expected cost c with no strategy, i.e. taking random actions. 
Cost is accumulated water-level, incremented each step.
The expression [#&lt;=100;100] means respectively 100 steps length of run and 100 runs to evaluate.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>strategy efficient = minE(c) [#&lt;=100] { WaterTank.location } -&gt; { w } : &lt;&gt; steps &gt;= 100</formula>
			<comment>Expect: "Strategy found" | 2 seconds

Learn a strategy minimizing the amount of water kept in the tank.
Cost c is accumulated water-level, incremented each step.
There is no concern for whether the water-level goes below zero. This will be addressed below.
The strategy is set to observe the discrete variable WaterTank.location and the continuous variable w.</comment>
		</query>
		<query>
			<formula>simulate[#&lt;=100] { w, 0, 10 } under efficient</formula>
			<comment>Expect: 1 second.

Simulate a run using the "efficient" strategy for 100 steps, showing water-level w.
The water-level will go far below 0, which is not valid.</comment>
		</query>
		<query>
			<formula>E[#&lt;=100;1] (max: c) under efficient</formula>
			<comment>Expect: ≈3.5 | 1 second

Show the expected cost c of the "efficient" strategy.
Cost is accumulated water-level, incremented each step.
Since the strategy achieves negative water-level, the cost will be impossibly low.
Since both the strategy and the system is deterministic, only 1 evaluation run is needed.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>strategy safe = acontrol: A[] w  &lt; 10 &amp;&amp; w &gt; 0 { WaterTank.location, w[-1, 11]:24 }</formula>
			<comment>Expect: "Strategy done" | 1 second

Synthesize a strategy for keeping the water-level w strictly between 0 and 10.
The strategy will be based on the discrete value WaterTank.location, and the floating-point variable w.
The floating-point value w is divided into 24 intervals between -1 and 11. 
So, e.g. the first interval is [-1, -0.5).
Since there are 5 locations, this gives 7*24=168 abstract states.</comment>
		</query>
		<query>
			<formula>simulate[#&lt;=100] { w, 0, 10 } under safe</formula>
			<comment>Expect: 1 second.

Simulate a run using the "safe" strategy for 100 steps, showing water-level w.
Note how the water-level w stays within safe margins.</comment>
		</query>
		<query>
			<formula>E[#&lt;=100;100] (max: c) under safe</formula>
			<comment>Expect: 790 ± 5 | 1 second

Show the expected cost c of the "safe" strategy.
Cost is accumulated water-level, incremented each step.
Whenever the strategy allows multiple actions, it picks between them at random.
</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>strategy safe_and_efficient = minE(c) [#&lt;=1000] { WaterTank.location } -&gt; { w } : &lt;&gt; steps &gt;= 1000 under safe</formula>
			<comment>Expect: "Strategy found" | 2 seconds

Learn a strategy minimizing the cost c, under the restrictions of the "safe" strategy.
Cost c is accumulated water-level, incremented each step.
The strategy will learn to keep the water-level w as low as possible, but is unable to reach a state where w&lt;=0.
The strategy is set to observe the discrete variable WaterTank.location and the continuous variable w.</comment>
		</query>
		<query>
			<formula>simulate[#&lt;=100] { w, 0, 10 } under safe_and_efficient</formula>
			<comment>Expect: 1 second.

Simulate a run using the "safe_and_efficient" strategy for 100 steps, showing water-level w.
Note how the water-level w is kept low while staying within safe margins.</comment>
		</query>
		<query>
			<formula>E[#&lt;=100;1] (max: c) under safe_and_efficient</formula>
			<comment>Expect: ≈114.5 | 1 second

Show the expected cost c of the "efficient" strategy.
Cost is accumulated water-level, incremented each step.
Note how this strategy achieves a significantly better cost while still staying within safe limits.
Since both the strategy and the system is deterministic, only 1 evaluation run is needed.</comment>
		</query>
	</queries>
</nta>
