<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'>
<nta>
	<declaration>clock x, y, dx;
clock e;
</declaration>
	<template>
		<name x="5" y="5">Trig1</name>
		<declaration>// Place local declarations here.
</declaration>
		<location id="id0" x="-192" y="-64">
			<urgent/>
		</location>
		<location id="id1" x="-104" y="-120">
			<label kind="invariant" x="-120" y="-88">x'==0 &amp;&amp; 
y'==0 &amp;&amp;
e'==0</label>
			<label kind="exponentialrate" x="-120" y="-104">1000</label>
		</location>
		<init ref="id0"/>
		<transition>
			<source ref="id0"/>
			<target ref="id1"/>
			<label kind="assignment" x="-200" y="-112">x=0, 
y=1</label>
			<nail x="-160" y="-64"/>
			<nail x="-160" y="-96"/>
		</transition>
		<transition>
			<source ref="id1"/>
			<target ref="id1"/>
			<label kind="assignment" x="-192" y="-184">x=x + y*dx,
y=y - x*dx,
dx=0,
e=2*x*y</label>
			<nail x="-136" y="-136"/>
			<nail x="-96" y="-160"/>
		</transition>
	</template>
	<template>
		<name x="5" y="5">Trig2</name>
		<declaration>// Place local declarations here.
</declaration>
		<location id="id2" x="-192" y="-64">
			<urgent/>
		</location>
		<location id="id3" x="-104" y="-120">
			<label kind="invariant" x="-120" y="-104">x'==1*y &amp;&amp; 
y'==-x</label>
		</location>
		<init ref="id2"/>
		<transition>
			<source ref="id2"/>
			<target ref="id3"/>
			<label kind="assignment" x="-200" y="-112">x=0, 
y=1</label>
			<nail x="-160" y="-64"/>
			<nail x="-160" y="-96"/>
		</transition>
	</template>
	<system>system Trig1;
</system>
</nta>
