From 22312be09b0e1eb0d9de7c858b672d617246dc90 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Thu, 15 Oct 2015 12:40:19 +0200
Subject: Start working on UPPAAL assignment; finished(?) model

---
 uppaalassignment/dining_savages.q   | 31 +++++++++++++++
 uppaalassignment/dining_savages.xml | 77 +++++++++++++++++++++++++++++++++++++
 2 files changed, 108 insertions(+)
 create mode 100644 uppaalassignment/dining_savages.q
 create mode 100644 uppaalassignment/dining_savages.xml

diff --git a/uppaalassignment/dining_savages.q b/uppaalassignment/dining_savages.q
new file mode 100644
index 0000000..da0f201
--- /dev/null
+++ b/uppaalassignment/dining_savages.q
@@ -0,0 +1,31 @@
+//This file was generated from (Commercial) UPPAAL 4.0.14 (rev. 5615), May 2014
+
+/*
+
+*/
+A[] not deadlock
+
+/*
+
+*/
+E<> servings == 0
+
+/*
+
+*/
+A[] not (Mutex.overflow or FullPot.overflow or EmptyPot.overflow)
+
+/*
+
+*/
+A[] not (cook.put and servings != 0)
+
+/*
+
+*/
+A[] not (s1.eat and servings == 0)
+
+/*
+
+*/
+A[] servings >= 0
diff --git a/uppaalassignment/dining_savages.xml b/uppaalassignment/dining_savages.xml
new file mode 100644
index 0000000..7563fba
--- /dev/null
+++ b/uppaalassignment/dining_savages.xml
@@ -0,0 +1,77 @@
+<?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 an adaptation by Camil Staps of
+//an adaption by Frits Vaandrager of
+//a model made by Martijn Hendriks
+
+// Number of processes in system:
+const int N = 5;
+
+const int emptyPot = 0;
+const int fullPot = 1;
+const int mutex = 2;
+const int nr_sem = 3; // nr. of semaphores
+
+int servings = 5;
+const int max_servings = 5;
+
+// The channels to synchronize with the semafores
+// A call semWait(s) by process p translates to a sequence of two transitions labeled with
+//      semWait(s)(p)!
+//      semGo(s)(p)?
+//A call semSignal(s) by process p translates to a transition labeled with
+//     semSignal(s)(p)!
+chan semWait[nr_sem][N], semGo[nr_sem][N], semSignal[nr_sem][N];</declaration><template><name>Semaphore</name><parameter>const int id,  const int queue_size, const int init_val</parameter><declaration>//The value of the semaphore
+int count = init_val;
+//The queue of the semaphore
+//value -1 denotes an empty array entry
+int[-1,N-1] queue[queue_size];
+//An auxiliary variable used to temporarily store process id
+meta int[0,N-1] q;
+
+void initialize ()
+{
+  for (i : int[0,queue_size-1])
+      {queue[i] = -1;}
+}
+
+void deQueue ()
+{
+  for (i : int[1,queue_size-1])
+    queue[i-1] = queue[i];
+  queue[queue_size-1] = -1;
+}
+
+void enQueue (int p)
+{
+  int i = 0;
+  while (queue[i]&gt;=0){i++;};
+  queue[i]=p;
+}
+
+int[0,N-1] headQueue ( )
+{
+  return queue[0];
+}
+
+bool fullQueue ( )
+{
+  for (i : int[0,queue_size-1])
+   {
+     if (queue[i]==-1) {return false;}
+   }
+  return true;
+}</declaration><location id="id0" x="384" y="64"><committed/></location><location id="id1" x="608" y="320"><committed/></location><location id="id2" x="352" y="96"><name x="288" y="64">overflow</name></location><location id="id3" x="480" y="192"></location><init ref="id0"/><transition><source ref="id0"/><target ref="id3"/><label kind="assignment" x="408" y="72">initialize()</label></transition><transition><source ref="id3"/><target ref="id3"/><label kind="select" x="272" y="192">p:int[0,N-1]</label><label kind="guard" x="272" y="208">count&gt;=0</label><label kind="synchronisation" x="272" y="224">semSignal[id][p]?</label><label kind="assignment" x="272" y="240">count++</label><nail x="352" y="192"/><nail x="352" y="224"/></transition><transition><source ref="id3"/><target ref="id1"/><label kind="select" x="552" y="104">p:int[0,N-1]</label><label kind="guard" x="552" y="120">count&gt;0</label><label kind="synchronisation" x="552" y="136">semWait[id][p]?</label><label kind="assignment" x="552" y="152">count--,
+q=p</label><nail x="608" y="192"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="select" x="248" y="112">p:int[0,N-1]</label><label kind="guard" x="248" y="128">count&lt;=0 &amp;&amp; fullQueue()</label><label kind="synchronisation" x="248" y="144">semWait[id][p]?</label></transition><transition><source ref="id1"/><target ref="id3"/><label kind="synchronisation" x="512" y="208">semGo[id][q]!</label></transition><transition><source ref="id3"/><target ref="id1"/><label kind="select" x="360" y="280">p:int[0,N-1]</label><label kind="guard" x="360" y="296">count&lt;0</label><label kind="synchronisation" x="360" y="312">semSignal[id][p]?</label><label kind="assignment" x="360" y="328">count++,
+q=headQueue(),
+deQueue()</label><nail x="480" y="320"/></transition><transition><source ref="id3"/><target ref="id3"/><label kind="select" x="480" y="-24">p:int[0,N-1]</label><label kind="guard" x="480" y="-8">count&lt;=0 &amp;&amp; not fullQueue()</label><label kind="synchronisation" x="480" y="8">semWait[id][p]?</label><label kind="assignment" x="480" y="24">count--,
+enQueue(p)</label><nail x="480" y="64"/><nail x="512" y="64"/></transition></template><template><name>Cook</name><parameter>const int pid</parameter><location id="id4" x="-400" y="-304"><name x="-376" y="-312">put</name></location><location id="id5" x="-400" y="-456"><name x="-376" y="-464">notify</name></location><location id="id6" x="-640" y="-304"><name x="-696" y="-312">sleep</name></location><location id="id7" x="-640" y="-456"></location><init ref="id7"/><transition><source ref="id4"/><target ref="id5"/><label kind="assignment" x="-384" y="-392">servings := max_servings</label></transition><transition><source ref="id6"/><target ref="id4"/><label kind="synchronisation" x="-600" y="-328">semGo[emptyPot][pid]?</label></transition><transition><source ref="id5"/><target ref="id7"/><label kind="synchronisation" x="-608" y="-480">semSignal[fullPot][pid]!</label></transition><transition><source ref="id7"/><target ref="id6"/><label kind="synchronisation" x="-832" y="-392">semWait[emptyPot][pid]!</label></transition></template><template><name>Savage</name><parameter>const int pid</parameter><location id="id8" x="-560" y="-456"><name x="-536" y="-464">leave_mutex</name></location><location id="id9" x="-840" y="-456"><name x="-832" y="-488">mutex_wait</name></location><location id="id10" x="-928" y="-544"></location><location id="id11" x="-560" y="-168"><name x="-544" y="-176">eat</name></location><location id="id12" x="-752" y="-168"><name x="-864" y="-176">wait_for_cook</name></location><location id="id13" x="-752" y="-272"><name x="-848" y="-280">wake_cook</name></location><location id="id14" x="-752" y="-368"><name x="-744" y="-400">hungry</name></location><init ref="id10"/><transition><source ref="id8"/><target ref="id10"/><label kind="synchronisation" x="-824" y="-568">semSignal[mutex][pid]!</label><nail x="-560" y="-544"/></transition><transition><source ref="id11"/><target ref="id8"/><label kind="assignment" x="-552" y="-336">servings = servings - 1</label></transition><transition><source ref="id9"/><target ref="id14"/><label kind="synchronisation" x="-952" y="-408">semGo[mutex][pid]?</label></transition><transition><source ref="id10"/><target ref="id9"/><label kind="synchronisation" x="-1056" y="-496">semWait[mutex][pid]!</label></transition><transition><source ref="id14"/><target ref="id11"/><label kind="guard" x="-696" y="-280">servings &gt; 0</label></transition><transition><source ref="id12"/><target ref="id11"/><label kind="synchronisation" x="-728" y="-160">semGo[fullPot][pid]?</label></transition><transition><source ref="id13"/><target ref="id12"/><label kind="synchronisation" x="-912" y="-232">semWait[fullPot][pid]!</label></transition><transition><source ref="id14"/><target ref="id13"/><label kind="guard" x="-856" y="-336">servings == 0</label><label kind="synchronisation" x="-944" y="-320">semSignal[emptyPot][pid]!</label></transition></template><system>EmptyPot = Semaphore(emptyPot, N-1, 0);
+FullPot = Semaphore(fullPot, N-1, 0);
+
+cook = Cook(0);
+
+Mutex = Semaphore(mutex, 5, 1);
+s1 = Savage(0);
+s2 = Savage(1);
+s3 = Savage(2);
+s4 = Savage(3);
+
+system EmptyPot, FullPot, Mutex, cook, s1, s2, s3, s4;</system></nta>
\ No newline at end of file
-- 
cgit v1.2.3