Uppaal Demo: network of TA model of buffer queue

File contents

<?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>// Place global declarations here.
chan a,b,c;
clock x;</declaration><template><name x="5" y="5">P</name><declaration>// Place local declarations here.
</declaration><location id="id0" x="32" y="-144"><label kind="invariant" x="22" y="-129">x&lt;2</label></location><location id="id1" x="-120" y="-136"></location><init ref="id1"/><transition><source ref="id0"/><target ref="id1"/><label kind="synchronisation" x="-48" y="-112">b!</label><nail x="-40" y="-112"/></transition><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="-40" y="-200">a?</label><label kind="assignment" x="-56" y="-176">x:=0</label><nail x="-40" y="-184"/></transition></template><template><name>Q</name><declaration>clock y;</declaration><location id="id2" x="56" y="-32"><name x="46" y="-62">lx</name></location><location id="id3" x="-48" y="-32"><name x="-58" y="-62">l1</name></location><location id="id4" x="-224" y="-24"></location><init ref="id4"/><transition><source ref="id3"/><target ref="id2"/><label kind="guard" x="-8" y="-56">y&lt;1</label></transition><transition><source ref="id3"/><target ref="id4"/><label kind="synchronisation" x="-128" y="0">c!</label><label kind="assignment" x="-144" y="24">y:=0</label><nail x="-128" y="24"/></transition><transition><source ref="id4"/><target ref="id3"/><label kind="guard" x="-136" y="-104">y&gt;1</label><label kind="synchronisation" x="-136" y="-80">b?</label><nail x="-152" y="-80"/><nail x="-96" y="-80"/><nail x="-56" y="-48"/></transition></template><template><name>Env</name><location id="id5" x="0" y="0"></location><init ref="id5"/><transition><source ref="id5"/><target ref="id5"/><label kind="synchronisation" x="56" y="8">c?</label><nail x="56" y="0"/><nail x="40" y="32"/></transition><transition><source ref="id5"/><target ref="id5"/><label kind="synchronisation" x="24" y="-56">a!</label><nail x="-8" y="-56"/><nail x="32" y="-64"/></transition></template><system>// Place template instantiations here.
q = Q();
p = P();
e = Env();

// List one or more processes to be composed into a system.
system p,q,e;</system></nta>