<?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>// This model is based on the example of Section 2 in
// Priorities in Process Algebras, by Rance Cleveland and
// Matthew Hennesy (Information and Computation, 1990).

// The interrupt controller INT should communicate 'i'
// whenever possible, so that C cannot receive 'up' or 'down'
// after INT has received 'shut_down'.

// Uncomment one of the priority specifications to make the model work,
// by using channel priorities (end of these declarations), or
// process priorities (system declaration).

// Input to the counter
chan up, down;

// Shut down request
chan shut_down;

// Internal communication
chan i;

// Counter modulo (wrap-around).
const int MODULO = 16;

// Counter value
int[0,MODULO-1] count = 0;

// Channel priority declarations
// =============================
// Uncomment one of the priority specifications to make the model work.

// (1) 'i' has higher priority than others.
//chan priority default &lt; i;

// (2) 'i' has higher priority than 'up' and 'down'
//chan priority up, down &lt; i;
</declaration><template><name x="5" y="5">INT</name><location id="id0" x="-232" y="-104"></location><location id="id1" x="-232" y="-192"></location><location id="id2" x="-232" y="-280"></location><init ref="id2"/><transition><source ref="id1"/><target ref="id0"/><label kind="synchronisation" x="-224" y="-160">i!</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="synchronisation" x="-224" y="-248">shut_down?</label></transition></template><template><name>C</name><declaration>
void count_up()
{
  count = (count + 1) % MODULO;
}

void count_down()
{
  count = count &gt; 0 ? (count - 1) % MODULO : 0;
}
</declaration><location id="id3" x="-384" y="-224"></location><location id="id4" x="-384" y="-312"></location><init ref="id4"/><transition><source ref="id4"/><target ref="id4"/><label kind="synchronisation" x="-480" y="-344">up?</label><label kind="assignment" x="-520" y="-328">count_up()</label><nail x="-448" y="-312"/><nail x="-448" y="-344"/></transition><transition><source ref="id4"/><target ref="id4"/><label kind="synchronisation" x="-320" y="-344">down?</label><label kind="assignment" x="-320" y="-328">count_down()</label><nail x="-328" y="-312"/><nail x="-328" y="-344"/></transition><transition><source ref="id4"/><target ref="id3"/><label kind="synchronisation" x="-376" y="-280">i?</label></transition></template><template><name>env</name><location id="id5" x="-176" y="64"><name x="-152" y="56">ERROR</name></location><location id="id6" x="-176" y="-40"><name x="-160" y="-48">OFF</name></location><location id="id7" x="-176" y="-136"><name x="-184" y="-176">ON</name></location><init ref="id7"/><transition><source ref="id6"/><target ref="id5"/><label kind="synchronisation" x="-248" y="0">down!</label><nail x="-208" y="-16"/><nail x="-208" y="32"/><nail x="-192" y="48"/></transition><transition><source ref="id6"/><target ref="id5"/><label kind="synchronisation" x="-200" y="0">up!</label></transition><transition><source ref="id7"/><target ref="id6"/><label kind="synchronisation" x="-168" y="-96">shut_down!</label></transition><transition><source ref="id7"/><target ref="id7"/><label kind="synchronisation" x="-288" y="-160">down!</label><nail x="-240" y="-136"/><nail x="-240" y="-168"/></transition><transition><source ref="id7"/><target ref="id7"/><label kind="synchronisation" x="-104" y="-160">up!</label><nail x="-112" y="-168"/><nail x="-112" y="-136"/></transition></template><system>system INT,C,env;

// Use this system line to specify process priorities:
//system C,env &lt; INT;
</system></nta>