newXMLSystem3
<?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>broadcast chan pub, grant, patent, coin, tea, cof;</declaration><template><name>Administration</name><declaration>clock z;</declaration><location id="id0" x="130" y="300" color="#3f51b5"><name x="130" y="270">L3</name><label kind="invariant" x="0" y="0">z&lt;=2</label></location><location id="id1" x="310" y="300" color="#3f51b5"><name x="310" y="270">L2</name></location><location id="id2" x="310" y="100" color="#3f51b5"><name x="310" y="70">L1</name><label kind="invariant" x="0" y="0">z &lt;= 2</label></location><location id="id3" x="130" y="100" color="#3f51b5"><name x="130" y="70">L0</name></location><location id="id4" x="0" y="0" color="#455a64"><name x="0" y="-30">Inconsistent</name><urgent/></location><location id="id5" x="0" y="0" color="#455a64"><name x="0" y="-30">Universal</name></location><init ref="id3"/><transition><source ref="id0"/><target ref="id0"/><label kind="synchronisation" x="40" y="260">pub?</label><nail x="90" y="280"/><nail x="90" y="300"/></transition><transition><source ref="id0"/><target ref="id0"/><label kind="synchronisation" x="110" y="350">grant?</label><nail x="130" y="340"/><nail x="110" y="340"/></transition><transition><source ref="id1"/><target ref="id1"/><label kind="synchronisation" x="330" y="260">grant?</label><nail x="350" y="300"/><nail x="350" y="320"/></transition><transition><source ref="id2"/><target ref="id2"/><label kind="synchronisation" x="360" y="90">pub?</label><nail x="350" y="100"/><nail x="350" y="120"/></transition><transition><source ref="id2"/><target ref="id2"/><label kind="synchronisation" x="320" y="40">grant?</label><nail x="310" y="60"/><nail x="290" y="60"/></transition><transition controllable="false"><source ref="id0"/><target ref="id3"/><label kind="synchronisation" x="140" y="190">patent!</label><nail x="130" y="200"/></transition><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="230" y="260">pub?</label><label kind="assignment" x="180" y="260">z=0</label><nail x="250" y="300"/><nail x="200" y="300"/></transition><transition controllable="false"><source ref="id2"/><target ref="id1"/><label kind="synchronisation" x="320" y="180">coin!</label><nail x="310" y="190"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="160" y="70">grant?</label><label kind="assignment" x="210" y="70">z=0</label><nail x="180" y="100"/><nail x="230" y="100"/></transition><transition controllable="false"><source ref="id5"/><target ref="id5"/><label kind="synchronisation" x="60" y="0">patent!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition controllable="false"><source ref="id5"/><target ref="id5"/><label kind="synchronisation" x="60" y="0">coin!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition><source ref="id5"/><target ref="id5"/><label kind="synchronisation" x="-60" y="0">pub?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition><transition><source ref="id5"/><target ref="id5"/><label kind="synchronisation" x="-60" y="0">grant?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition></template><template><name>HalfAdm1</name><declaration>clock x;</declaration><location id="id6" x="130" y="200" color="#d32f2f"><name x="130" y="170">L13</name><label kind="invariant" x="0" y="0">x&lt;=2</label></location><location id="id7" x="130" y="90" color="#d32f2f"><name x="130" y="60">L12</name></location><location id="id8" x="0" y="0" color="#455a64"><name x="0" y="-30">Inconsistent</name><urgent/></location><location id="id9" x="0" y="0" color="#455a64"><name x="0" y="-30">Universal</name></location><init ref="id7"/><transition controllable="false"><source ref="id7"/><target ref="id7"/><label kind="synchronisation" x="180" y="60">patent!</label><nail x="170" y="70"/><nail x="170" y="90"/></transition><transition><source ref="id7"/><target ref="id7"/><label kind="synchronisation" x="30" y="70">pub?</label><nail x="90" y="80"/><nail x="100" y="60"/></transition><transition><source ref="id6"/><target ref="id6"/><label kind="synchronisation" x="180" y="220">grant?</label><nail x="170" y="230"/><nail x="170" y="210"/></transition><transition><source ref="id6"/><target ref="id6"/><label kind="synchronisation" x="100" y="260">pub?</label><nail x="120" y="240"/><nail x="140" y="240"/></transition><transition controllable="false"><source ref="id6"/><target ref="id6"/><label kind="synchronisation" x="30" y="190">patent!</label><nail x="80" y="200"/><nail x="80" y="220"/></transition><transition controllable="false"><source ref="id6"/><target ref="id7"/><label kind="synchronisation" x="50" y="130">coin!</label><nail x="110" y="140"/></transition><transition><source ref="id7"/><target ref="id6"/><label kind="synchronisation" x="160" y="120">grant?</label><label kind="assignment" x="160" y="140">x=0</label><nail x="150" y="130"/><nail x="150" y="150"/></transition><transition controllable="false"><source ref="id9"/><target ref="id9"/><label kind="synchronisation" x="60" y="0">patent!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition controllable="false"><source ref="id9"/><target ref="id9"/><label kind="synchronisation" x="60" y="0">coin!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="synchronisation" x="-60" y="0">pub?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition><transition><source ref="id9"/><target ref="id9"/><label kind="synchronisation" x="-60" y="0">grant?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition></template><template><name>HalfAdm2</name><declaration>clock y;</declaration><location id="id10" x="160" y="220" color="#e64a19"><name x="160" y="190">L15</name><label kind="invariant" x="0" y="0">y&lt;=2</label></location><location id="id11" x="160" y="110" color="#e64a19"><name x="160" y="80">L14</name></location><location id="id12" x="0" y="0" color="#455a64"><name x="0" y="-30">Inconsistent</name><urgent/></location><location id="id13" x="0" y="0" color="#455a64"><name x="0" y="-30">Universal</name></location><init ref="id11"/><transition controllable="false"><source ref="id11"/><target ref="id11"/><label kind="synchronisation" x="170" y="40">coin!</label><nail x="180" y="70"/><nail x="200" y="80"/></transition><transition><source ref="id11"/><target ref="id11"/><label kind="synchronisation" x="100" y="40">grant?</label><nail x="120" y="80"/><nail x="140" y="70"/></transition><transition><source ref="id10"/><target ref="id10"/><label kind="synchronisation" x="180" y="280">grant?</label><nail x="190" y="260"/><nail x="200" y="240"/></transition><transition><source ref="id10"/><target ref="id10"/><label kind="synchronisation" x="110" y="270">pub?</label><nail x="140" y="250"/><nail x="160" y="260"/></transition><transition controllable="false"><source ref="id10"/><target ref="id10"/><label kind="synchronisation" x="50" y="210">coin!</label><nail x="110" y="220"/><nail x="120" y="240"/></transition><transition controllable="false"><source ref="id10"/><target ref="id11"/><label kind="synchronisation" x="90" y="150">patent!</label><nail x="140" y="160"/></transition><transition><source ref="id11"/><target ref="id10"/><label kind="synchronisation" x="190" y="140">pub?</label><label kind="assignment" x="190" y="170">y=0</label><nail x="180" y="150"/><nail x="180" y="180"/></transition><transition controllable="false"><source ref="id13"/><target ref="id13"/><label kind="synchronisation" x="60" y="0">patent!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition controllable="false"><source ref="id13"/><target ref="id13"/><label kind="synchronisation" x="60" y="0">coin!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition><source ref="id13"/><target ref="id13"/><label kind="synchronisation" x="-60" y="0">pub?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition><transition><source ref="id13"/><target ref="id13"/><label kind="synchronisation" x="-60" y="0">grant?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition></template><template><name>Machine</name><declaration>clock y;</declaration><location id="id14" x="140" y="100" color="#0097a7"><name x="140" y="70">L5</name></location><location id="id15" x="140" y="300" color="#0097a7"><name x="140" y="270">L4</name><label kind="invariant" x="0" y="0">y&lt;=6</label></location><location id="id16" x="0" y="0" color="#455a64"><name x="0" y="-30">Inconsistent</name><urgent/></location><location id="id17" x="0" y="0" color="#455a64"><name x="0" y="-30">Universal</name></location><init ref="id14"/><transition controllable="false"><source ref="id14"/><target ref="id14"/><label kind="guard" x="180" y="40">y&gt;=2</label><label kind="synchronisation" x="120" y="30">tea!</label><nail x="170" y="60"/><nail x="140" y="60"/></transition><transition><source ref="id15"/><target ref="id15"/><label kind="synchronisation" x="70" y="340">coin?</label><nail x="130" y="350"/><nail x="160" y="350"/></transition><transition><source ref="id14"/><target ref="id15"/><label kind="synchronisation" x="160" y="210">coin?</label><label kind="assignment" x="150" y="180">y=0</label><nail x="140" y="220"/><nail x="140" y="190"/></transition><transition controllable="false"><source ref="id15"/><target ref="id14"/><label kind="synchronisation" x="230" y="190">tea!</label><nail x="210" y="200"/></transition><transition controllable="false"><source ref="id15"/><target ref="id14"/><label kind="guard" x="30" y="220">y&gt;=4</label><label kind="synchronisation" x="30" y="170">cof!</label><nail x="100" y="230"/><nail x="100" y="180"/></transition><transition controllable="false"><source ref="id17"/><target ref="id17"/><label kind="synchronisation" x="60" y="0">tea!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition controllable="false"><source ref="id17"/><target ref="id17"/><label kind="synchronisation" x="60" y="0">cof!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition><source ref="id17"/><target ref="id17"/><label kind="synchronisation" x="-60" y="0">coin?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition></template><template><name>Machine2</name><location id="id18" x="120" y="80" color="#e91e63"><name x="120" y="50">L11</name></location><location id="id19" x="120" y="170" color="#e91e63"><name x="120" y="140">L10</name></location><location id="id20" x="0" y="0" color="#455a64"><name x="0" y="-30">Inconsistent</name><urgent/></location><location id="id21" x="0" y="0" color="#455a64"><name x="0" y="-30">Universal</name></location><init ref="id18"/><transition controllable="false"><source ref="id19"/><target ref="id18"/><label kind="synchronisation" x="50" y="110">cof!</label><nail x="100" y="120"/></transition><transition controllable="false"><source ref="id18"/><target ref="id18"/><label kind="synchronisation" x="130" y="30">tea!</label><nail x="120" y="40"/><nail x="100" y="40"/></transition><transition><source ref="id19"/><target ref="id19"/><label kind="synchronisation" x="50" y="200">coin?</label><nail x="100" y="210"/><nail x="120" y="210"/></transition><transition><source ref="id18"/><target ref="id19"/><label kind="synchronisation" x="150" y="110">coin?</label><nail x="140" y="120"/></transition><transition controllable="false"><source ref="id21"/><target ref="id21"/><label kind="synchronisation" x="60" y="0">tea!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition controllable="false"><source ref="id21"/><target ref="id21"/><label kind="synchronisation" x="60" y="0">cof!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition><source ref="id21"/><target ref="id21"/><label kind="synchronisation" x="-60" y="0">coin?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition></template><template><name>Researcher</name><declaration>clock x;</declaration><location id="id22" x="310" y="130" color="#43a047"><name x="310" y="100">L6</name></location><location id="id23" x="110" y="130" color="#43a047"><name x="110" y="100">L9</name><label kind="invariant" x="0" y="0">x&lt;=4</label></location><location id="id24" x="310" y="300" color="#43a047"><name x="310" y="270">L7</name><label kind="invariant" x="0" y="0">x &lt;=8</label></location><location id="id25" x="0" y="0" color="#455a64"><name x="0" y="-30">Inconsistent</name><urgent/></location><location id="id26" x="0" y="0" color="#455a64"><name x="0" y="-30">Universal</name></location><init ref="id22"/><transition><source ref="id22"/><target ref="id26"/><label kind="guard" x="330" y="50">x&gt;15</label><label kind="synchronisation" x="380" y="50">tea?</label><nail x="350" y="90"/><nail x="400" y="90"/></transition><transition controllable="false"><source ref="id24"/><target ref="id22"/><label kind="guard" x="350" y="230">x&gt;=4</label><label kind="synchronisation" x="350" y="210">pub!</label><label kind="assignment" x="350" y="190">x=0</label><nail x="340" y="240"/><nail x="340" y="220"/><nail x="330" y="200"/></transition><transition controllable="false"><source ref="id23"/><target ref="id22"/><label kind="guard" x="130" y="70">x&gt;=2</label><label kind="synchronisation" x="180" y="70">pub!</label><label kind="assignment" x="220" y="70">x=0</label><nail x="170" y="110"/><nail x="200" y="110"/><nail x="240" y="110"/></transition><transition><source ref="id22"/><target ref="id24"/><label kind="guard" x="220" y="190">x&lt;=15</label><label kind="synchronisation" x="220" y="210">tea?</label><label kind="assignment" x="220" y="230">x=0</label><nail x="290" y="200"/><nail x="290" y="220"/><nail x="290" y="240"/></transition><transition><source ref="id22"/><target ref="id23"/><label kind="synchronisation" x="220" y="150">cof?</label><label kind="assignment" x="180" y="150">x=0</label><nail x="240" y="140"/><nail x="200" y="140"/></transition><transition><source ref="id24"/><target ref="id24"/><label kind="synchronisation" x="370" y="310">tea?</label><nail x="350" y="320"/><nail x="350" y="300"/></transition><transition><source ref="id24"/><target ref="id24"/><label kind="synchronisation" x="210" y="290">cof?</label><nail x="270" y="300"/><nail x="270" y="320"/></transition><transition><source ref="id23"/><target ref="id23"/><label kind="synchronisation" x="70" y="180">tea?</label><nail x="90" y="170"/><nail x="110" y="170"/></transition><transition><source ref="id23"/><target ref="id23"/><label kind="synchronisation" x="20" y="90">cof?</label><nail x="70" y="110"/><nail x="70" y="130"/></transition><transition controllable="false"><source ref="id26"/><target ref="id26"/><label kind="synchronisation" x="60" y="0">pub!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition><source ref="id26"/><target ref="id26"/><label kind="synchronisation" x="-60" y="0">tea?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition><transition><source ref="id26"/><target ref="id26"/><label kind="synchronisation" x="-60" y="0">cof?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition></template><template><name>Spec</name><declaration>clock u;</declaration><location id="id27" x="90" y="120" color="#1e88e5"><name x="90" y="90">L18</name></location><location id="id28" x="370" y="120" color="#1e88e5"><name x="370" y="90">L17</name><label kind="invariant" x="0" y="0">u&lt;=20</label></location><location id="id29" x="240" y="120" color="#1e88e5"><name x="240" y="90">L16</name></location><location id="id30" x="0" y="0" color="#455a64"><name x="0" y="-30">Inconsistent</name><urgent/></location><location id="id31" x="0" y="0" color="#455a64"><name x="0" y="-30">Universal</name></location><init ref="id29"/><transition><source ref="id27"/><target ref="id27"/><label kind="synchronisation" x="50" y="170">grant?</label><nail x="70" y="160"/><nail x="90" y="160"/></transition><transition controllable="false"><source ref="id27"/><target ref="id27"/><label kind="synchronisation" x="70" y="50">patent!</label><nail x="90" y="80"/><nail x="70" y="80"/></transition><transition><source ref="id29"/><target ref="id27"/><label kind="guard" x="180" y="90">u&gt;2</label><label kind="synchronisation" x="130" y="90">grant?</label><nail x="200" y="120"/><nail x="150" y="120"/></transition><transition controllable="false"><source ref="id28"/><target ref="id29"/><label kind="synchronisation" x="350" y="200">patent!</label><label kind="assignment" x="260" y="210">u=0</label><nail x="370" y="190"/><nail x="280" y="190"/><nail x="240" y="190"/></transition><transition><source ref="id28"/><target ref="id28"/><label kind="synchronisation" x="390" y="90">grant?</label><nail x="410" y="120"/><nail x="410" y="140"/></transition><transition><source ref="id29"/><target ref="id28"/><label kind="guard" x="250" y="70">u&lt;=2</label><label kind="synchronisation" x="250" y="40">grant?</label><label kind="assignment" x="300" y="20">u=0</label><nail x="240" y="80"/><nail x="240" y="50"/><nail x="320" y="50"/><nail x="370" y="50"/></transition><transition controllable="false"><source ref="id31"/><target ref="id31"/><label kind="synchronisation" x="60" y="0">patent!</label><nail x="40" y="-10"/><nail x="60" y="0"/><nail x="40" y="10"/></transition><transition><source ref="id31"/><target ref="id31"/><label kind="synchronisation" x="-60" y="0">grant?</label><nail x="-40" y="-10"/><nail x="-60" y="0"/><nail x="-40" y="10"/></transition></template><system>system Spec, Machine, Machine2, Administration, HalfAdm1, HalfAdm2, Researcher;

IO Spec { grant?, patent! }
IO Machine { coin?, tea!, cof! }
IO Machine2 { coin?, tea!, cof! }
IO Administration { grant?, pub?, coin!, patent! }
IO HalfAdm1 { grant?, pub?, coin!, patent! }
IO HalfAdm2 { grant?, pub?, coin!, patent! }
IO Researcher { cof?, tea?, pub! }</system></nta>

.
getInitialState
concreteGetInitial
getTransitions
2
0
0
3
1
1
0
.
0
1
0
.
1
2
0
.
2
3
0
.
3
4
0
.
4
5
0
.
5
6
0
.
6
1
0
.
.
.