<?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>/* Simulation-specific stuff */
double x=0.0;
double t=0.0;
const double epsilon = 0.04;
const double delta_fast = 0.17; 
const double tau_fast = 0.05;
const double delta_slow = 0.1;
const double tau_slow = 0.12;
const double pi = M_PI;

double total_cost = 0.0; 

void updateFast() {
    if (t &gt;= 1 || x &gt;= 1)
        return;
    x = x + delta_fast - epsilon + random(2*epsilon);
    t = t + tau_fast - epsilon + random(2*epsilon);
    total_cost = total_cost + 4.5 + sin(x*pi*4)*1.5;    // Cost function varies based on x. It is almost always cheaper to go Slow.
}


void updateSlow() {
    if (t &gt;= 1 || x &gt;= 1)
        return;
    x = x + delta_slow - epsilon + random(2*epsilon); 
    t = t + tau_slow - epsilon + random(2*epsilon);
    total_cost = total_cost + 2.5 + sin(pi + x*pi*4)*1.5;
}
</declaration>
	<template>
		<name x="5" y="5">Player</name>
		<declaration>// Place local declarations here.
</declaration>
		<location id="id0" x="-8" y="34">
			<committed/>
		</location>
		<location id="id1" x="-102" y="34">
			<name x="-127" y="0">Slow</name>
			<committed/>
		</location>
		<location id="id2" x="93" y="34">
			<name x="76" y="0">Fast</name>
			<committed/>
		</location>
		<init ref="id0"/>
		<transition id="id3" controllable="false">
			<source ref="id2"/>
			<target ref="id0"/>
		</transition>
		<transition id="id4" controllable="false">
			<source ref="id1"/>
			<target ref="id0"/>
		</transition>
		<transition id="id5">
			<source ref="id0"/>
			<target ref="id1"/>
			<label kind="assignment" x="-119" y="76">updateSlow()</label>
			<nail x="-102" y="76"/>
		</transition>
		<transition id="id6">
			<source ref="id0"/>
			<target ref="id2"/>
			<label kind="assignment" x="17" y="76">updateFast()</label>
			<nail x="93" y="76"/>
		</transition>
	</template>
	<system>system Player;
</system>
	<queries>
		<option key="--samples-per-axis" value="4"/>
		<option key="--repeat-samples" value="20"/>
		<option key="--out-of-bounds" value="1"/>
		<query>
			<formula>simulate[#&lt;=30;1] { 1, x, t }</formula>
			<comment>Expect: 1 second

Simulate a run showing progress x and time t, taking random actions.
Notice how the simulation stops once one of the two variables exceed 1.</comment>
		</query>
		<query>
			<formula>Pr[#&lt;=30;10000](&lt;&gt; t&gt;1)</formula>
			<comment>Expect: 0.0433 ± 0.0040 |  1 second

Estimate the probability of exceeding time, i.e. t &gt; 1, while choosing random actions.
The game stops when either time t or progress x exceeds 1.
When choosing randomly between Fast and Slow action, this happens rarely, but it does occur.</comment>
		</query>
		<query>
			<formula>E[#&lt;=30;1000] (max:total_cost)</formula>
			<comment>Expect: 27.59 ± 0.2416| 1 second

Estimate the expected total_cost, from taking random actions. Cost varies based on progress x.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>strategy efficient = minE (total_cost) [#&lt;=30] {} -&gt; {x, t} : &lt;&gt; x&gt;1 or t&gt;1</formula>
			<comment>Expect: "Strategy found" | 1 second

Learn a strategy to minimize total_cost, without regard for how the game ends.
Cost varies with progress x, but generally going Slow is cheaper, thus leading to a strategy that mostly exceeds t &gt; 1 before reaching progress x &gt; 1.
</comment>
		</query>
		<query>
			<formula>simulate[#&lt;=30;1] { 1, x, t } under efficient</formula>
			<comment>Expect: 1 second

Simulate a run showing progress x and time t, under strategy "efficient"
Notice how the simulation stops once one of the two variables exceed 1.</comment>
		</query>
		<query>
			<formula>Pr[#&lt;=30;10000](&lt;&gt; t&gt;=1) under efficient</formula>
			<comment>Expect: between 0.04 and 0.9 |  1 second

High variation based on learning outcome.
Estimate the probability of exceeding time, i.e. t &gt; 1, under strategy "efficient"
The game stops when either time t or progress x exceeds 1.
When choosing only based on cost, the risk of exceeding t increases.</comment>
		</query>
		<query>
			<formula>E[#&lt;=30;1000] (max:total_cost) under efficient</formula>
			<comment>Expect: between 19 and 23 | 1 second

High variation based on learning outcome.
Estimate the expected cost under strategy "efficient". 
A clear improvement should be seen compared to taking random actions.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>strategy safe = acontrol: A[] (t &lt; 1) { x[0, 1.2]:200, t[0, 1.2]:200 }</formula>
			<comment>Expect: "Strategy done"  | 100 seconds

Approximate a strategy for never exceeding t &gt; 1. This is done by reaching progress x &gt; 1 before time t is exceeded.

The strategy abstracts the continuous values of x and t into 200 intervals each.
This results in 200*200=40000 possible locations in the abstract game.

The total_cost variable is left out as it has no bearing on action outcomes, and is just used to keep track of cost.
Instead, total_cost will assume its default (initial) value of 0 in each game location.</comment>
		</query>
		<query>
			<formula>saveStrategy("walk-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("walk-safe.strategy.json")</formula>
			<comment>Expect: 1 second

Load a strategy that has been previously saved.</comment>
		</query>
		<query>
			<formula>simulate[#&lt;=30;1] { 1, x, t } under safe</formula>
			<comment>Expect: 1 second

Simulate a run showing progress x and time t, under strategy "safe".
When the strategy allows multiple actions, it will choose between them at random (uniform distribution).
Notice how t doesn't exceed 1.</comment>
		</query>
		<query>
			<formula>Pr[#&lt;=30;10000](&lt;&gt; t&gt;=1) under safe</formula>
			<comment>Expect: &lt;= 0.0004 | 1 second

Estimate the probability of exceeding time, i.e. t &gt; 1, under strategy "safe"
When the strategy allows multiple actions, it will choose between them at random (uniform distribution).
Under the "safe" strategy, time is never exceeded.</comment>
		</query>
		<query>
			<formula>E[#&lt;=30;1000] (max:total_cost) under safe</formula>
			<comment>Expect: 27.88 ± 0.2360 | 1 second

Estimate the expected cost under strategy "safe". 
When the strategy allows multiple actions, it will choose between them at random (uniform distribution).
It appears similar if not identical to the random distribution.</comment>
		</query>
		<query>
			<formula>saveStrategy("walk-safe.strategy.json", safe)</formula>
			<comment>Expect: "Strategy Saved" | 1 second

 Save the strategy to the home folder.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>strategy safe_and_efficient = minE (total_cost) [#&lt;=30] {} -&gt; {x, t} : &lt;&gt; x&gt;=1 or t&gt;=1 under safe</formula>
			<comment>Expect: "Strategy found" | 1 second

Learn a strategy to minimize total_cost, under the strategy "safe".
Cost varies with progress x, but generally going Slow is cheaper.
When the strategy is in danger of exceeding t, "safe" will intervene and choose the Fast option.
The result is a strategy that is both safe and efficient.
</comment>
		</query>
		<query>
			<formula>simulate[#&lt;=30;1] { 1, x, t } under safe_and_efficient</formula>
			<comment>Expect: 1 second

Simulate a run showing progress x and time t, under strategy "safe_and_efficient".
Notice how t doesn't exceed 1.</comment>
		</query>
		<query>
			<formula>Pr[#&lt;=30;10000](&lt;&gt; t&gt;=1) under safe_and_efficient</formula>
			<comment>Expect: &lt;= 0.0004 | 1 second

Estimate the probability of exceeding time, i.e. t &gt; 1, under strategy "safe_and_efficient".
Like with the "safe" strategy on which it is based, time is never exceeded.</comment>
		</query>
		<query>
			<formula>E[#&lt;=30;100] (max:total_cost) under safe_and_efficient</formula>
			<comment>Expect: 27.88 ± 0.2360 | 1 second

High variation based on learning outcome.
Estimate the expected cost under strategy "safe_and_efficient". 
When the strategy allows multiple actions, it will choose between them at random (uniform distribution).
Despite the variation, it is comparable to the performance of the unsafe "efficient" strategy.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
	</queries>
</nta>
