<?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.
clock t,a,v = 2,x;

const double k = 25;</declaration>
	<template>
		<name x="5" y="5">Template</name>
		<declaration>// Place local declarations here.
</declaration>
		<location id="id0" x="-42" y="25">
			<label kind="invariant" x="-52" y="42">t &lt;= 100 &amp;&amp;
a' == 0.001 + 0.2*M_PI*1*cos(0.2*M_PI*t) &amp;&amp;
v' == a &amp;&amp;
x' == v</label>
		</location>
		<location id="id1" x="238" y="-102">
		</location>
		<init ref="id0"/>
		<transition id="id2">
			<source ref="id0"/>
			<target ref="id1"/>
			<label kind="guard" x="42" y="-76">t &gt;= 100</label>
		</transition>
	</template>
	<system>// Place template instantiations here.
Process = Template();
// List one or more processes to be composed into a system.
system Process;
</system>
	<queries>
		<query>
			<formula/>
			<comment/>
		</query>
		<query>
			<formula>simulate [t &lt;= 50] {a, v, x}</formula>
			<comment/>
		</query>
	</queries>
</nta>
