<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.5//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_5.dtd'>
<nta>
	<declaration>//Insert declarations of global clocks, variables, constants and channels.

bool spo, eco, loc, com;
clock time;
</declaration>
	<template>
		<name x="5" y="5">Job</name>
		<parameter>bool &amp;sec1, bool &amp;sec2,  bool&amp; sec3,  bool &amp;sec4, const int t1, const int t2, const int t3, const int t4, const int T1, const int T2, const int T3, const int T4, const int R</parameter>
		<declaration>//Insert local declarations of clocks, variables and constants.
clock x;
hybrid clock WTime;</declaration>
		<location id="id0" x="212" y="365">
			<label kind="exponentialrate" x="204" y="333">R</label>
		</location>
		<location id="id1" x="270" y="496">
			<name x="254" y="504">SEC1</name>
			<label kind="invariant" x="254" y="520">x&lt;=T1 &amp;&amp;
WTime'==0</label>
		</location>
		<location id="id2" x="340" y="365">
			<label kind="exponentialrate" x="332" y="333">R</label>
		</location>
		<location id="id3" x="404" y="493">
			<name x="388" y="509">SEC2</name>
			<label kind="invariant" x="388" y="525">x&lt;=T2 &amp;&amp;
WTime'==0</label>
		</location>
		<location id="id4" x="468" y="365">
			<label kind="exponentialrate" x="468" y="333">R</label>
		</location>
		<location id="id5" x="532" y="493">
			<name x="516" y="509">SEC3</name>
			<label kind="invariant" x="516" y="525">x&lt;=T3 &amp;&amp;
WTime'==0</label>
		</location>
		<location id="id6" x="596" y="365">
			<label kind="exponentialrate" x="594" y="333">R</label>
		</location>
		<location id="id7" x="660" y="493">
			<name x="644" y="509">SEC4</name>
			<label kind="invariant" x="644" y="525">x&lt;=T4 &amp;&amp;
WTime'==0</label>
		</location>
		<location id="id8" x="724" y="365">
			<name x="714" y="335">Done</name>
			<label kind="invariant" x="748" y="357">WTime'==0</label>
		</location>
		<init ref="id0"/>
		<transition id="id9">
			<source ref="id0"/>
			<target ref="id1"/>
			<label kind="guard" x="172" y="381">!sec1</label>
			<label kind="assignment" x="212" y="445">sec1=true,
x:=0</label>
		</transition>
		<transition id="id10" controllable="false">
			<source ref="id1"/>
			<target ref="id2"/>
			<label kind="guard" x="292" y="461">x&gt;=t1</label>
			<label kind="assignment" x="252" y="381">sec1=false</label>
		</transition>
		<transition id="id11">
			<source ref="id2"/>
			<target ref="id3"/>
			<label kind="guard" x="356" y="381">!sec2</label>
			<label kind="assignment" x="340" y="453">sec2=true,
x:=0</label>
		</transition>
		<transition id="id12" controllable="false">
			<source ref="id3"/>
			<target ref="id4"/>
			<label kind="guard" x="420" y="461">x&gt;=t2</label>
			<label kind="assignment" x="404" y="397">sec2=false</label>
		</transition>
		<transition id="id13">
			<source ref="id4"/>
			<target ref="id5"/>
			<label kind="guard" x="484" y="381">!sec3</label>
			<label kind="assignment" x="476" y="453">sec3=true,
x:=0</label>
		</transition>
		<transition id="id14" controllable="false">
			<source ref="id5"/>
			<target ref="id6"/>
			<label kind="guard" x="556" y="453">x&gt;=t3</label>
			<label kind="assignment" x="524" y="389">sec3=false</label>
		</transition>
		<transition id="id15">
			<source ref="id6"/>
			<target ref="id7"/>
			<label kind="guard" x="612" y="381">!sec4</label>
			<label kind="assignment" x="596" y="453">sec4=true,
x:=0</label>
		</transition>
		<transition id="id16" controllable="false">
			<source ref="id7"/>
			<target ref="id8"/>
			<label kind="guard" x="684" y="453">x&gt;=t4</label>
			<label kind="assignment" x="668" y="381">sec4=false</label>
		</transition>
	</template>
	<system>//Insert process assignments.
Jakob  = Job(com,spo,loc,eco,10,3,3,1,11,6,6,5,5);
Kim = Job(spo,eco,loc,com,8,20,1,1,10,23,6,12,5);
Marius  = Job(eco,com, loc,spo,13,11,11,1,20,13,23,3,5);
Peter = Job(spo,eco,loc,com,1,1,1,1,3,5,3,4,5);

//Edit system definition.
system Jakob, Kim, Marius, Peter;

gantt {
 Jakob:  Jakob.SEC1 -&gt; 2, Jakob.SEC2 -&gt;4, Jakob.SEC3 -&gt; 3, Jakob.SEC4 -&gt; 1;
  Kim:  Kim.SEC1 -&gt; 1, Kim.SEC2 -&gt; 2, Kim.SEC3 -&gt; 3, Kim.SEC4 -&gt; 4;
 Marius:  Marius.SEC1 -&gt; 4, Marius.SEC2 -&gt; 1, Marius.SEC3 -&gt; 3, Marius.SEC4 -&gt; 2;
 Peter:  Peter.SEC1 -&gt; 2, Peter.SEC2 -&gt; 4, Peter.SEC3 -&gt; 3, Peter.SEC4 -&gt; 1;
}</system>
	<queries>
		<query>
			<formula>E&lt;&gt; Kim.Done and time&lt;=60                             // true</formula>
			<comment>Is it possible for Kim to be finished within 60mins?
Expect true (satisfied) within seconds.</comment>
		</query>
		<query>
			<formula>A&lt;&gt; Kim.Done and time&lt;=60                             // false</formula>
			<comment>Is Kim guaranteed to be finish reading within 60mins?
Expect false (unsatisfied), i.e. there are traces where Kim finishes later.</comment>
		</query>
		<query>
			<formula>Pr[&lt;=60] (&lt;&gt; Kim.Done)                                // 0.69</formula>
			<comment>How likely Kim is going to be finished reading within 60mins?
Expect the property evaluated within 1-2 minutes and the probability is only ~0.69
(not all instances succeed and thus estamation takes longer).</comment>
		</query>
		<query>
			<formula>strategy Travel = control: A&lt;&gt; Kim.Done &amp;&amp; time &lt;= 60
			</formula>
			<comment>Kim is going to travel and needs to leave within 60mins! Can we find a strategy for him?
Expect the strategy to be computed within seconds.
The strategy is kept in memory under name Travel.
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=60] (&lt;&gt; Kim.Done) under Travel                   // &gt;0.99</formula>
			<comment>When is Kim ready to leave?
Expect the property evaluated within seconds.
Expect the probability to aproach to 1, even before &lt;=60 time units.
The plot shows the mean time about 42.96±0.21 (95% CI)
			</comment>
		</query>
		<query>
			<formula>A&lt;&gt; Kim.Done &amp;&amp; time&lt;=60 under Travel                 // true</formula>
			<comment>Is Kim guaranteed to be finished reading under the Travel strategy?</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>E&lt;&gt; Marius.Done &amp;&amp; time &lt;= 60 under Travel            // false
			</formula>
			<comment>Can Marius go with Kim?
Expect the property to be unsatisfied (false) within seconds, meaning that there is no way Marius can make it given that Kim's process ir favored.
			</comment>
		</query>
		<query>
			<formula>E&lt;&gt; Peter.Done &amp;&amp; time &lt;= 60 under Travel             // true
			</formula>
			<comment>Can Peter go with Kim?
Expect the property to be satisfied (true) within seconds.
			</comment>
		</query>
		<query>
			<formula>E&lt;&gt; Jakob.Done &amp;&amp; time &lt;= 60 under Travel             // true
			</formula>
			<comment>Can Jakob go with Kim?
Expect the property to be satisfied (true) within seconds.
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=60] (&lt;&gt; Peter.Done) under Travel                 // 0.82</formula>
			<comment>What is the probablity of Peter finishing when Kim is guaranteed to finish?
Expect ~0.82 within seconds.</comment>
		</query>
		<query>
			<formula>Pr[&lt;=60] (&lt;&gt; Jakob.Done) under Travel                 // 0.67</formula>
			<comment>What is the probablity of Jacob finishing when Kim is guaranteed to finish?
Expect ~0.67 within seconds.
Observe that Jacob's</comment>
		</query>
		<query>
			<formula>Pr[&lt;=50] (&lt;&gt; Peter.Done) under PeterTravel &gt;= Pr[&lt;=50] (&lt;&gt; Peter.Done) under Travel // true
			</formula>
			<comment>Are Peter's chances of going with Kim greater than Jakob's chances?
Expect the property to be satisfied (true) within seconds.
Such comparison query is more efficient than estimating each probability separately.
The plot also shows how probabilities compare over time:
value 0 means false, 1 means true, 0.5 means probabilities are indistinguishable.
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=60] (&lt;&gt; Peter.Done) under PeterTravel &gt;= Pr[&lt;=60] (&lt;&gt; Peter.Done) under Travel // false
			</formula>
			<comment>Are Peter's chances of going with Kim still greater than Jakob's chances if we extend the time limit?
Expect the property to be not satisfied (false) within seconds.
			</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>Pr[&lt;=100] (&lt;&gt; Jakob.Done &amp;&amp; Kim.Done &amp;&amp; Marius.Done &amp;&amp; Peter.Done)           // &gt;0.99, mean time 58.1</formula>
			<comment>Compute probability that we are done with no strategy: click check and expect probability approach to 1 (computes within seconds).
Inspect the probability distribution over time by right-clicking the query and choosing "Cumulative probability distribution".
Expect mean run time: 58.07±0.27 (95% CI)
For more data and better picture: set epsilon=0.001 in Options -&gt; Statistical parameters and re-check the property.</comment>
		</query>
		<query>
			<formula>strategy Opt = minE(time) [&lt;=100]: &lt;&gt; Jakob.Done &amp;&amp; Kim.Done &amp;&amp; Marius.Done &amp;&amp; Peter.Done</formula>
			<comment>Compute unrestricted (near-)optimal strategy with a goal of minimizing the expected time. 
Expect possitive result (strategy exists) (computed within 2-5mins).
Once evaluated, the strategy is stored in the engine memory under variable Opt.
The next property can be evaluated under this strategy.
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100] (&lt;&gt; Jakob.Done &amp;&amp; Kim.Done &amp;&amp; Marius.Done &amp;&amp; Peter.Done) under Opt // &gt;0.99, mean time 55.6</formula>
			<comment>Reevaluate the probability that we are done under the previously computed Opt (near optiomal) strategy. Expect probability approach 1.
Inspect the probability distribution over time by right-clicking this property and choosing Cumulative probability distribution.
Expect mean run time: 55.60±0.25 (95% CI)
Note the improved mean time since the first property: the average (expected) time is shorter under strategy.
Both plots can be super-imposed by Plot composer in the Tools menu.
			</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>strategy PeterTravel = minE(time) [&lt;=60]: &lt;&gt;Peter.Done under Travel
			</formula>
			<comment>Jakob is bussy, so let's optimize Peter's chances to go together with Kim.
Expect the Travel strategy to be refined and stored as PeterTravel within 1-2 minutes.
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=60] (&lt;&gt; Peter.Done) under PeterTravel    // &gt;0.99, mean time 14.6</formula>
			<comment>What is the probability of Peter being done when the strategy is optimized for him?
Expect &gt;0.99 and mean time 14.6</comment>
		</query>
		<query>
			<formula>Pr[&lt;=60] (&lt;&gt; Peter.Done) under Travel         //  0.82, mean time 29.1</formula>
			<comment>What is the probability of Peter being done when the strategy is optimized for him?
Expect 0.82</comment>
		</query>
		<query>
			<formula>Pr[&lt;=60] (&lt;&gt; Peter.Done) under PeterTravel &gt;= Pr[&lt;=60] (&lt;&gt; Peter.Done) under Travel // true
			</formula>
			<comment>Does our learned strategy improve the situation?
Expect the property to be satisfied (true) within seconds.
			</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>simulate [&lt;=100; 100] {Jakob.WTime, Kim.WTime, Marius.WTime, Peter.WTime}</formula>
			<comment>The amount of time they are waiting to get a section.</comment>
		</query>
		<query>
			<formula>E[&lt;=100 ; 100] (max: Peter.WTime)  // 34.6</formula>
			<comment>Estimate Peter's waiting time to get a section.
Expect ~34.6 within seconds.</comment>
		</query>
		<query>
			<formula>E[&lt;=100 ; 100] (max: Jakob.WTime)  // 19.0</formula>
			<comment>Estimate Jacob's waiting time to get a section.
Expect ~19.2 within seconds.
			</comment>
		</query>
		<query>
			<formula>E[&lt;=100 ; 100] (max: Kim.WTime)    // 17.2</formula>
			<comment>Estimate Kim's waiting time to get a section.
Expect ~17.3 within seconds.
			</comment>
		</query>
		<query>
			<formula>E[&lt;=100 ; 100] (max: Marius.WTime) //  0.80</formula>
			<comment>Estimate Marius' waiting time to get a section.
Expect ~0.80 within seconds.
			</comment>
		</query>
		<query>
			<formula>Pr[&lt;=100] (&lt;&gt; Jakob.Done &amp;&amp; Kim.Done &amp;&amp; Marius.Done &amp;&amp; Peter.Done) // &gt;0.99, mean time 58.0</formula>
			<comment>How do the collective newspaper reading perform?
Expect probability &gt;99 and the mean time ~56.1 (in probability plot), computed within seconds.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>strategy OptWaiting = minE(Peter.WTime) [&lt;=100]: &lt;&gt; Peter.Done</formula>
			<comment>Peter often gets cranky from waiting. We try to minimize the time he is in this state.
Expect a strategy to be computed in 3-5min.
			</comment>
		</query>
		<query>
			<formula>E[&lt;=100 ; 100] (max: Peter.WTime)  under OptWaiting // 21.2</formula>
			<comment>Estimate Peter's waiting time to get a section when the behavior is optimized to minimize Peter's waiting time.
Expect ~21.2 within seconds.</comment>
		</query>
		<query>
			<formula>E[&lt;=100 ; 100] (max: Jakob.WTime)  under OptWaiting // 21.2</formula>
			<comment/>
		</query>
		<query>
			<formula>E[&lt;=100 ; 100] (max: Kim.WTime)    under OptWaiting // 15.3</formula>
			<comment/>
		</query>
		<query>
			<formula>E[&lt;=100 ; 100] (max: Marius.WTime) under OptWaiting //  0.0</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[&lt;=100] (&lt;&gt; Jakob.Done &amp;&amp; Kim.Done &amp;&amp; Marius.Done &amp;&amp; Peter.Done) under OptWaiting // &gt;0.99, mean time 56.1</formula>
			<comment>How do the collective newspaper reading perform under this new strategy ?
Expect the mean (in probability plot) to be ~56.1 computed within seconds.</comment>
		</query>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>strategy OptWaitingBoth = minE (Peter.WTime + Jakob.WTime * 0.5) [&lt;=200]: &lt;&gt; Peter.Done &amp;&amp; Jakob.Done
			</formula>
			<comment>Jakob actually also gets cranky, but only half as cranky as Peter.
The query demonstrates extended expressions in the optimization.
The strategy is computed within 2-5min.
			</comment>
		</query>
		<query>
			<formula>Pr [&lt;=200] (&lt;&gt; Jakob.Done &amp;&amp; Kim.Done &amp;&amp; Marius.Done &amp;&amp; Peter.Done) under OptWaitingBoth
			</formula>
			<comment>How do the collective newspaper reading perform under this new strategy, minimizing both Peter and Jakobs crankiness?
The mean time is 63.83±0.62 (99% CI) computed within seconds.
			</comment>
		</query>
	</queries>
</nta>
