<?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>/**
The example demonstrates different ways of generating trigonometric functions (sin and cos) over time
using facts that sin'(t)=cos(t) and cos'(t)=-sin(t).
*/</declaration>
	<template>
		<name x="5" y="5">Trig1</name>
		<declaration>/**
Continuous Time Markov Chain example with custom (random) time step integration.
 */

clock sint, cost=1.0, dt;
clock sin2t; // = 2*sin(t)*cos(t) = sin(2*t)  -- expect 2x faster sine.

</declaration>
		<location id="id0" x="-104" y="-120">
			<label kind="invariant" x="-120" y="-88">sint'==0 &amp;&amp; 
cost'==0 &amp;&amp;
sin2t'==0</label>
			<label kind="exponentialrate" x="-120" y="-104">1000</label>
		</location>
		<init ref="id0"/>
		<transition id="id1">
			<source ref="id0"/>
			<target ref="id0"/>
			<label kind="assignment" x="-85" y="-178">sint=sint + cost*dt,
cost=cost - sint*dt,
sin2t=2*sint*cost,
dt=0</label>
			<nail x="-136" y="-136"/>
			<nail x="-96" y="-160"/>
		</transition>
	</template>
	<template>
		<name x="5" y="5">Trig2</name>
		<declaration>/**
Continuous integration of ODE system with fixed time step.
The time step size is controlled in menu Options/Statistical parameters,
"Discretization step for hybrid systems".
 */

clock sint, cost=1.0;

</declaration>
		<location id="id2" x="-104" y="-120">
			<label kind="invariant" x="-120" y="-104">sint'==cost &amp;&amp; 
cost'==-sint</label>
		</location>
		<init ref="id2"/>
	</template>
	<system>clock t;

//system Trig1;
//system Trig2;
system Trig1, Trig2;
</system>
	<queries>
		<query>
			<formula>simulate [&lt;=20] { sin(t), cos(t) }</formula>
			<comment>Computed as algebraic functions of time.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=20] { Trig1.sint, Trig1.cost }</formula>
			<comment>CTMC generated sine and cosine.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=20] { Trig1.sint, Trig2.sint, Trig1.cost, Trig2.cost }</formula>
			<comment/>
		</query>
		<query>
			<formula>simulate [Trig1.cost&lt;=10] { Trig1.sint, Trig1.sin2t } : 1 : t&gt;=20</formula>
			<comment>Alternative simulation plot where cosine is used as x-axis.
Expect an ellipse, which might be incomplete due to Trig1.cost diverging beyond 1 due to numerical errors.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=20] { Trig2.sint, Trig2.cost }		</formula>
			<comment>Continuously integrated sine and cosine.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=20] { Trig1.sint, Trig2.sint, Trig1.cost, Trig2.cost }</formula>
			<comment>Comparison of random step and fixed time step simulations.
Expect overlaping trajectories.</comment>
		</query>
		<query>
			<formula>simulate [Trig2.cost&lt;=10] { Trig2.sint } : 1 : t&gt;=20		</formula>
			<comment>Alternative simulation plot where cosine is used as x-axis.
Expect an ellipse, which might be incomplete due to Trig2.cost diverging beyond 1 due to numerical errors.</comment>
		</query>
		<query>
			<formula/>
			<comment>Alternative simulation plot where cosine is used as x-axis.
Expect an ellipse, which might be incomplete or overlapping multiple times due to Trig1.cost due to numerical errors.
This formula requires some luck: if it takes too long (longer than a few seconds) then cancel and try again.</comment>
		</query>
		<query>
			<formula>simulate [&lt;=10] { Trig2.sint, Trig2.cost, Trig2.sint &gt;? Trig2.cost }</formula>
			<comment>Demonstrates "inline maximum" expression.
Expect the maximum to overlap with the max(sint, cost).</comment>
		</query>
		<query>
			<formula>simulate [&lt;=10] { Trig2.sint, Trig2.cost, Trig2.sint &lt;? Trig2.cost }</formula>
			<comment>Demonstrates "inline minimum" expression.
Expect the minimum to overlap with the min(sint, cost).</comment>
		</query>
		<query>
			<formula>simulate [&lt;=20] { Trig1.sint-sin(t) }</formula>
			<comment>Demonstrates the precision of CTMC generated sine with exact sin(t).</comment>
		</query>
		<query>
			<formula>simulate [&lt;=20] { Trig2.sint-sin(t) }</formula>
			<comment/>
		</query>
		<query>
			<formula>Pr[&lt;=30] (&lt;&gt; fabs(Trig1.sint-sin(t))&gt;0.0003)
			</formula>
			<comment>Estimates the probability of CTMC generated sint deviating from sin(t) by more than 0.0003.
The search is sensitive to SMC parameters (significance beta and precistion epsilon) and usually gives 
more precise probability estimate than diagnostic "simulate" formula above.
Expect probability of ~0.3 and average time to deviation about 20.8 t.u.</comment>
		</query>
	</queries>
</nta>
