Organisation; assignment 2

5 files changed, 119 insertions, 0 deletions

diff --git a/assignment1.tex b/assignment1/assignment1.tex
index 6104bdf..6104bdf 100644
--- a/assignment1.tex
+++ b/assignment1/assignment1.tex
diff --git a/assignment2/assignment2.txt b/assignment2/assignment2.txt
new file mode 100644
index 0000000..ceee4fa
--- /dev/null
+++ b/assignment2/assignment2.txt
@@ -0,0 +1,8 @@
+Camil Staps (s4498062)
+
+1.
+De `not blocked[1-i]' en `turn := 1' zijn twee stappen. Als daartussen een context switch plaatsvindt, kunnen beide processen tegelijkertijd in de kritieke sectie terechtkomen. Maken we hetzelfde model waarbij we deze twee stappen samenvoegen, dan is er geen probleem. Zie hyman.xml, hyman.q, hyman.trx.
+
+2.
+Stel dat proces 1 zich in de kritieke sectie bevindt. Als er nu om wat voor reden dan ook nooit een context switch plaatsvindt op het moment dat proces 1 zich in staat `Start' bevindt, dan zal proces 2 nooit opmerken dat proces 1 zijn blocked bit op 0 zet. Proces 2 zou in dat geval dus nooit in de kritieke sectie terechtkomen, maar continue in `WaitBlocked' blijven hangen.
+
diff --git a/assignment2/hyman.q b/assignment2/hyman.q
new file mode 100644
index 0000000..0bd1a71
--- /dev/null
+++ b/assignment2/hyman.q
@@ -0,0 +1,6 @@
+//This file was generated from (Commercial) UPPAAL 4.0.14 (rev. 5615), May 2014
+
+/*
+
+*/
+E<> (p1.CriticalSection && p2.CriticalSection)
diff --git a/assignment2/hyman.xml b/assignment2/hyman.xml
new file mode 100644
index 0000000..fb22f25
--- /dev/null
+++ b/assignment2/hyman.xml
@@ -0,0 +1,10 @@
+<?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.
+typedef int[0,1] ids;
+bool blocked[ids];
+int turn = 0;</declaration><template><name x="5" y="5">Process</name><parameter>ids id</parameter><declaration>// Place local declarations here.
+</declaration><location id="id0" x="-2264" y="-552"></location><location id="id1" x="-2168" y="-472"><name x="-2264" y="-504">WaitBlocked</name></location><location id="id2" x="-2360" y="-336"><name x="-2408" y="-320">CriticalSection</name></location><location id="id3" x="-2360" y="-472"><name x="-2456" y="-456">GainControl</name></location><location id="id4" x="-2576" y="-472"><name x="-2608" y="-512">Start</name></location><init ref="id4"/><transition><source ref="id0"/><target ref="id3"/><label kind="assignment" x="-2368" y="-576">turn := id</label><nail x="-2360" y="-552"/></transition><transition><source ref="id1"/><target ref="id0"/><label kind="guard" x="-2216" y="-576">not blocked[1-id]</label><nail x="-2168" y="-552"/></transition><transition><source ref="id1"/><target ref="id1"/><label kind="guard" x="-2120" y="-456">blocked[1-id]</label><nail x="-2168" y="-432"/><nail x="-2128" y="-432"/><nail x="-2128" y="-472"/></transition><transition><source ref="id3"/><target ref="id1"/><label kind="guard" x="-2312" y="-464">turn != id</label></transition><transition><source ref="id2"/><target ref="id4"/><label kind="assignment" x="-2552" y="-368">blocked[id] := false</label><nail x="-2576" y="-336"/></transition><transition><source ref="id3"/><target ref="id2"/><label kind="guard" x="-2352" y="-424">turn == id</label></transition><transition><source ref="id4"/><target ref="id3"/><label kind="assignment" x="-2536" y="-496">blocked[id] := true</label></transition></template><system>// Place template instantiations here.
+p1 = Process(0);
+p2 = Process(1);
+
+// List one or more processes to be composed into a system.
+system p1, p2;</system></nta>
\ No newline at end of file
diff --git a/assignment2/hyman.xtr b/assignment2/hyman.xtr
new file mode 100644
index 0000000..5dfbf2a
--- /dev/null
+++ b/assignment2/hyman.xtr
@@ -0,0 +1,95 @@
+4
+4
+.
+.
+0
+0
+0
+0
+1
+.
+4
+3
+.
+.
+0
+1
+0
+0
+1
+.
+1 7
+.
+4
+1
+.
+.
+0
+1
+0
+0
+1
+.
+1 4
+.
+4
+0
+.
+.
+0
+1
+0
+0
+1
+.
+1 2
+.
+3
+0
+.
+.
+1
+1
+0
+0
+1
+.
+0 7
+.
+2
+0
+.
+.
+1
+1
+0
+0
+1
+.
+0 6
+.
+2
+3
+.
+.
+1
+1
+1
+0
+1
+.
+1 1
+.
+2
+2
+.
+.
+1
+1
+1
+0
+1
+.
+1 6
+.
+.