producer-consumer.xml

<?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_2.dtd'>
<nta>
	<declaration>const int MAX = 6;
typedef int[0, MAX] Data;

chan  comm[Data];
</declaration>
	<template>
		<name x="40" y="16">Producer</name>
		<declaration>Data n;

Data getN()
{
    return n;
}

void incN()
{
    if (n == MAX) {
        n = 0;
    } else {
        n++;
    }
}</declaration>
		<location id="id0" x="-8" y="42">
			<name x="-51" y="8">Producer</name>
		</location>
		<init ref="id0"/>
		<transition>
			<source ref="id0"/>
			<target ref="id0"/>
			<label kind="synchronisation" x="102" y="25">comm[getN()]!</label>
			<label kind="assignment" x="102" y="42">incN()</label>
			<nail x="85" y="85"/>
			<nail x="93" y="0"/>
		</transition>
	</template>
	<template>
		<name x="40" y="16">Consumer</name>
		<declaration>Data myN;

void rec(Data x)
{
    myN = x;
}</declaration>
		<location id="id1" x="192" y="128">
			<name x="208" y="96">Consumer</name>
		</location>
		<init ref="id1"/>
		<transition>
			<source ref="id1"/>
			<target ref="id1"/>
			<label kind="select" x="306" y="187">n : Data</label>
			<label kind="synchronisation" x="306" y="204">comm[n]?</label>
			<label kind="assignment" x="306" y="221">rec(n)</label>
			<nail x="255" y="212"/>
			<nail x="331" y="161"/>
		</transition>
	</template>
	<system>system Producer, Consumer;
</system>
	<queries>
	</queries>
</nta>