<?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>/*
 * Four vikings are about to cross a damaged bridge in the middle of the
 * night. The bridge can only carry two of the vikings at the time and to
 * find the way over the bridge the vikings need to bring a torch.  The
 * vikings need 5, 10, 20 and 25 minutes (one-way) respectively to cross
 * the bridge.

 * Does a schedule exist which gets all four vikings over the bridge
 * within 60 minutes?
 */

chan take, release;		// Take and release torch
int[0,1] L;		// The side the torch is on
clock time;		// Global time
</declaration><template><name x="32" y="16">Soldier</name><parameter>const int delay</parameter><declaration>clock y;</declaration><location id="id0" x="288" y="80"></location><location id="id1" x="288" y="216"><name x="272" y="232">safe</name></location><location id="id2" x="64" y="216"></location><location id="id3" x="64" y="80"><name x="56" y="48">unsafe</name></location><init ref="id3"/><transition><source ref="id2"/><target ref="id3"/><label kind="guard" x="72" y="176">y &gt;= delay</label><label kind="synchronisation" x="72" y="120">release!</label></transition><transition><source ref="id1"/><target ref="id2"/><label kind="guard" x="208" y="224">L == 1</label><label kind="synchronisation" x="216" y="192">take !</label><label kind="assignment" x="104" y="224">y = 0</label></transition><transition><source ref="id0"/><target ref="id1"/><label kind="guard" x="296" y="112">y &gt;= delay</label><label kind="synchronisation" x="296" y="160">release!</label></transition><transition><source ref="id3"/><target ref="id0"/><label kind="guard" x="120" y="56">L == 0</label><label kind="synchronisation" x="120" y="88">take !</label><label kind="assignment" x="216" y="56">y = 0</label></transition></template><template><name x="32" y="-16">Torch</name><location id="id4" x="200" y="192"><name x="192" y="200">one</name></location><location id="id5" x="200" y="48"><urgent/></location><location id="id6" x="64" y="120"><name x="48" y="88">free</name></location><location id="id7" x="336" y="120"><name x="328" y="88">two</name></location><init ref="id6"/><transition><source ref="id6"/><target ref="id5"/><label kind="synchronisation" x="104" y="56">take?</label></transition><transition><source ref="id5"/><target ref="id4"/></transition><transition><source ref="id5"/><target ref="id7"/><label kind="synchronisation" x="264" y="56">take?</label></transition><transition><source ref="id4"/><target ref="id6"/><label kind="synchronisation" x="96" y="176">release?</label><label kind="assignment" x="32" y="144">L = 1 - L</label></transition><transition><source ref="id7"/><target ref="id4"/><label kind="synchronisation" x="256" y="176">release?</label></transition></template><system>const int fastest = 5;
const int fast    = 10;
const int slow    = 20;
const int slowest = 25;

Viking1 = Soldier(fastest);
Viking2 = Soldier(fast);
Viking3 = Soldier(slow);
Viking4 = Soldier(slowest);

system Viking1, Viking2, Viking3, Viking4, Torch;</system></nta>