Changes between Version 7 and Version 8 of Introduction

Timestamp:

12/28/18 20:39:21 (7 years ago)

Author:

siegel

Comment:

--

Introduction

@@ -52 +52 @@
 === Verifying CIVL-C Programs ===
 
+Dining philosophers:
+
+{{{
+$input int B = 4; // upper bound on number of philosophers
+$input int n;     // number of philosophers
+$assume(2<=n && n<=B);
+
+_Bool forks[n]; // Each fork will be on the table ($true) or in a hand ($false).
+
+void dine(int id) {
+  int left = id;
+  int right = (id + 1) % n;
+  while (1) {
+    $when (forks[left]) forks[left] = $false;
+    $when (forks[right]) forks[right] = $false;
+    forks[right] = $true;
+    forks[left] = $true;
+  }
+}
+
+void main() {
+  $for(int i: 0..n-1) forks[i] = $true;
+  $parfor(int i: 0..n-1) dine(i);
+}
+}}}
+
 
 === Verifying C Programs ===