oopsla testbed

app/RunTestbed.hs

@@ -45,7 +45,7 @@ import           PWhile.Util
 
 main :: IO ()
 main = do
-  let bnch = pldi
+  let bnch = oopsla
   let ?to  = 5
   as <- getArgs
   case as of
@@ -200,6 +200,12 @@ pldi = unsafePerformIO $ Benchmark "pldi" <$> do
   fps <- sort . lines <$> readCreateProcess (shell "find examples/pldi -type f") mempty
   forM fps $ \fp -> Problem fp <$> fromFile' fp
 
+{-# NOINLINE oopsla #-}
+oopsla :: Benchmark
+oopsla = unsafePerformIO $ Benchmark "oopsla" <$> do
+  fps <- sort . lines <$> readCreateProcess (shell "find examples/oopsla -type f") mempty
+  forM fps $ \fp -> Problem fp <$> fromFile' fp
+
 
 printBenchmarkTex :: (?to :: Int) => Benchmark -> IO ()
 printBenchmarkTex (Benchmark _ ps) =

examples/oopsla/absynthLinear/2drwalk.imp

+# 2-d random walk
+# d = |x| + |y|
+
+def f():
+    var x, y, d, n, z
+
+  while d < n:
+    if x > 0:
+      if y > 0:
+        prob(1,3):
+          x = x + 2
+          d = d + 2
+        else:
+          prob(1,2):
+            y = y + 2
+            d = d + 2
+          else:
+            prob(1,1):
+              x = x - 1
+              d = d - 1
+            else:
+              y = y - 1
+              d = d - 1
+      else:
+        if y < 0:
+          prob(1,3):
+            x = x + 2
+            d = d + 2
+          else:
+            prob(1,2):
+              y = y + 1
+              d = d - 1
+            else:
+              prob(1,1):
+                x = x - 1
+                d = d - 1
+              else:
+                y = y - 2
+                d = d + 2
+        else:
+          prob(1,3):
+            x = x + 2
+            d = d + 2
+          else:
+            prob(1,2):
+              y = y + 1
+              d = d + 1
+            else:
+              prob(1,1):
+                x = x - 1
+                d = d - 1
+              else:
+                y = y - 1
+                d = d + 1
+    else:
+      if x < 0:
+        if y > 0:
+          prob(1,3):
+            x = x + 1
+            d = d - 1
+          else:
+            prob(1,2):
+              y = y + 2
+              d = d + 2
+            else:
+              prob(1,1):
+                x = x - 2
+                d = d + 2
+              else:
+                y = y - 1
+                d = d - 1
+        else:
+          if y < 0:
+            prob(1,3):
+              x = x + 1
+              d = d - 1
+            else:
+              prob(1,2):
+                y = y + 1
+                d = d - 1
+              else:
+                prob(1,1):
+                  x = x - 2
+                  d = d + 2
+                else:
+                  y = y - 2
+                  d = d + 2
+          else:
+            prob(1,3):
+              x = x + 1
+              d = d - 1
+            else:
+              prob(1,2):
+                y = y + 1
+                d = d + 1
+              else:
+                prob(1,1):
+                  x = x - 2
+                  d = d + 2
+                else:
+                  y = y - 1
+                  d = d + 1
+      else:
+        if y > 0:
+          prob(1,3):
+            x = x + 1
+            d = d + 1
+          else:
+            prob(1,2):
+              y = y + 2
+              d = d + 2
+            else:
+              prob(1,1):
+                x = x - 1
+                d = d + 1
+              else:
+                y = y - 1
+                d = d - 1
+        else:
+          if y < 0:
+            prob(1,3):
+              x = x + 1
+              d = d + 1
+            else:
+              prob(1,2):
+                y = y + 1
+                d = d - 1
+              else:
+                prob(1,1):
+                  x = x - 1
+                  d = d + 1
+                else:
+                  y = y - 2
+                  d = d + 2
+          else:
+            prob(1,3):
+              x = x + 1
+              d = d + 1
+            else:
+              prob(1,2):
+                y = y + 1
+                d = d + 1
+              else:
+                prob(1,1):
+                  x = x - 1
+                  d = d + 1
+                else:
+                  y = y - 1
+                  d = d + 1
+    tick 1
+

examples/oopsla/absynthLinear/C4B_t09.imp

+# t09 in C4B figure 8
+
+def f():
+  var i, j, x, z
+  i = 1
+  j = 0
+  while j < x:
+    j = j + 1
+    if i >= 4:
+      i = 1
+      tick 40
+    else:
+      z = unif(1,3)
+      i = i + z
+    tick 1

examples/oopsla/absynthLinear/C4B_t13.imp

+# t13 in C4B figure 8
+
+def f():
+  var x, y, t, z
+  assume y >= 0:
+
+    while x > 0:
+      x = x - 1
+      prob(1, 3):
+        y = y + 1
+      else:
+        while y > 0:
+          y = y - 1
+          tick 1
+      tick 1
+

examples/oopsla/absynthLinear/C4B_t15.imp

+# t15 in C4B figure 8
+
+def f():
+  var x, y, t, z
+  assume y >= 0:
+    while x > y:
+      x = x - y
+      x = x - 1
+      t = y
+      while t > 0:
+        z = unif(1,2)
+        t = t - z
+        tick 1
+
+      tick 1
+

examples/oopsla/absynthLinear/C4B_t15_2.imp

+# t15 in C4B figure 8
+
+def f():
+  var x, y, t, z
+  assume y >= 0:
+    while [x >= 0 and y >= 0] x > y:
+      x = x - y
+      x = x - 1
+      t = y
+      while t > 0:
+        z = unif(1,2)
+        t = t - z
+        tick 1
+
+      tick 1
+

examples/oopsla/absynthLinear/C4B_t19.imp

+# t19 in C4B figure 8
+
+def f():
+  var i, k, z
+  while i > 100:
+    prob(1,1):
+      i = i - 1
+    else:
+      i = i - 0
+    tick 1
+
+  i = i + k
+  i = i + 50
+  while i >= 0:
+    i = i - 1
+    tick 1

examples/oopsla/absynthLinear/C4B_t30.imp

+# t30 in C4B figure 8
+
+def f():
+  var x, y, t, z
+  while x > 0:
+    z = unif(1,2)
+    x = x - z
+    t = x
+    x = y
+    y = t
+    tick 1
+

examples/oopsla/absynthLinear/C4B_t30_2.imp

+# t30 in C4B figure 8
+
+def f():
+  var x, y, t, z
+  while [y >= -1] x > 0:
+    z = unif(1,2)
+    x = x - z
+    t = x
+    x = y
+    y = t
+    tick 1
+

examples/oopsla/absynthLinear/C4B_t61.imp

+# tick N = 10
+
+def f():
+  var l, z
+
+  while l >= 8:
+    z = unif(6,8)
+    l = l - z
+    tick 10
+
+  while l > 0:
+    l = l - 1
+    tick 1
+    

examples/oopsla/absynthLinear/bayesian.imp

+# Example of Bayesian Network 
+# Perform n iterations over the network with 5 nodes 
+
+
+def f():
+    var i, d, s, l, g, z
+
+  while n > 0:
+    i = ber(3,10)
+    z = z + 1
+    d = ber(2,5)
+    tick 1
+
+    if i < 1 and d < 1:
+      g = ber(7,10)
+      tick 1
+    else:
+      if i < 1 and d > 0:
+        g = ber(19,20)
+        tick 1
+      else:
+        if i > 0 and d < 1:
+          g = ber(1,10)
+          tick 1
+        else:
+          g = ber(1,2)
+          tick 1
+    if i < 1:
+      s = ber(1,20)
+      tick 1
+    else:
+      s = ber(4,5)
+      tick 1
+    if g < 1:
+      l = ber(1,10)
+      tick 1
+    else:
+      l = ber(3,5)
+      tick 1
+    n = n - 1
+

examples/oopsla/absynthLinear/ber.imp

+def f():
+  var x, n, z
+  
+  while x < n:
+    z = ber(1,2)
+    x = x + z
+    tick 1
+        

examples/oopsla/absynthLinear/bin.imp

+def f():
+  var x, n, z
+  
+  while x < n:
+    prob(9,1):
+      x = x + 1
+    else:
+      x = x + 2
+    tick 1
+

examples/oopsla/absynthLinear/condand.imp

+# conjunction conditional loop
+
+def f():
+  var n, m, z
+  while n > 0 and m > 0:
+    prob(1,1):
+      n = n - 1
+    else:
+      m = m - 1
+    tick 1

examples/oopsla/absynthLinear/cooling.imp

+# probabilistic cooling system
+# every time interval, the system uses a sensor to measure the room temperature 
+# and decreases it if it is higher than the setting one
+# decreasing each temperature unit consumes 1 resource unit
+# compute the expected number of consumed resource units
+
+# mt : measured temperature of the room
+# st : desired setting temperature
+# ti : time interval = 5
+# t  : time of operation
+# each time interval, the room temperature increases randomly from 1 to 3 degrees,
+# with probability 1 : 1/10, 2 : 7/10, 3 : 2/10
+# modeled as a uniform distribution
+# the sensor for measuring the temperature has some error modeling as a uniform 
+# distribution from -1 to 1
+
+# exact value : max(0, mt - st) + (2/5)max(0, t + 5)
+# max(0, mt - st) : the cost for the first time of execution the inner loop
+# max(0, t + 5) : the bound on expected number of outer loop iterations
+# 2/5 : cost for each iteration
+
+def f():
+    var mt, st, t, z
+
+  while t >= 0:
+    # decrease the room temperature if needed
+    while mt > st:
+      mt = mt - 1
+      # consume 1 resource unit
+      tick 1
+    # the room temperature increases randomly
+    assume mt >= st and st >= mt:
+      prob(1,9):
+        mt = mt + 1
+      else:
+        prob(7,2):
+          mt = mt + 2
+        else:
+          mt = mt + 3
+      # error of sensor
+      z = rand(3)
+      mt = mt + (z - 1)
+      # advance to the next time interval
+      t = t - 5

examples/oopsla/absynthLinear/filling.imp

+# filling containers
+
+def f():
+  var volToFill, fast, medium, slow, vol, volMeasured, z
+
+  fast = 10
+  medium = 3
+  slow = 1
+  volMeasured = 0
+  z = unif(0,1)
+  volMeasured = volMeasured + z
+
+  while volMeasured <= volToFill:
+    if volToFill < (volMeasured + fast):
+      z = unif(9,10)
+      volMeasured = volMeasured + z
+    else:
+      if volToFill < (volMeasured + medium):
+        z = unif(2,4)
+        volMeasured = volMeasured + z
+      else:
+        z = unif(0,2)
+        volMeasured = volMeasured + z
+
+    z = unif(0,1)
+    volMeasured = volMeasured + z
+    tick 1
+
+

examples/oopsla/absynthLinear/linear01.imp

+def f():
+  var x, z
+
+  while x >= 2:
+    prob(1,2):
+      x = x - 1
+    else:
+      x = x - 2
+    tick 1
+

examples/oopsla/absynthLinear/miner.imp

+# A miner is sent to a mine, with probability 1/2, the miner is trapped
+# When a miner is trapped, there are 3 doors in the mine
+# The first door leads to a tunnel that will take him to safety after 3 hours
+# The second door leads to a tunnel that returns him to the mine after 5 hours
+# The third door leads to a tunnel that returns him to the mine after 7 hours
+# Compute the expected time to reach safety for n independent times
+# Let X_i be the random variable representing the miner escape time in the ith time and let X = X_1 + ... + X_n
+# We are asking for E(X)
+# Use the law of total expectation to calculate E(X_i), let A be the event that the miner is trapped then
+# E(X_i) = E(X_i|A)*P(A) + 0*P(not A) = E(X_i|A)*1/2. Now use again the law of total expectation to calculate E(X_i|A), 
+# let B be the event that the miner reaches safety in the first try, then we have
+# E(X_i|A) = E((X_i|A)|B)*P(B) + E((X_i|A)| not B)*P(not B) = 3*1/3 + (5*1/2 + 7*1/2 + E(X_i|A))*2/3 = 5 + 2/3*E(X_i|A)
+# E(X_i|A) = 15
+# By linearity of expectation, we get E(X) = E(X_1) + ... + E(X_n) = 15*1/2*n = 7.5*n if n > 0, 0 otherwise
+def f():
+  var i, flag, n, z
+  i = 0
+  while i < n:
+    prob(1,1):
+      flag = 1
+      while flag > 0:
+        prob(1,2):
+          flag = 0
+          z = z + 3
+          tick 3
+        else:
+          prob(1,1):
+            flag = 1
+            z = z + 5
+            tick 5
+          else:
+            flag = 1
+            z = z + 7
+            tick 7
+    i = i + 1
+    

examples/oopsla/absynthLinear/prdwalk.imp

+# figure 3 on right with T = 2, p = 1/2, K1 = 2, K2 = 5
+
+def f():
+  var x, n, z
+  while x < n:
+    prob(1,1):
+      z = rand(2)
+      x = x + z
+    else:
+      z = rand(5)
+      x = x + z
+    tick 2
+

examples/oopsla/absynthLinear/prnes.imp

+# interacting nested loops
+
+def f():
+    var y, n, z
+    assume y >= 0:
+
+      while n < 0:
+        prob(9,1):
+          n = n + 1
+        tick 9
+        nondet:
+          while y >= 100:
+            prob(1,1):
+              y = y - 100
+            else:
+              y = y - 90
+            tick 5
+          y = y + 1000
+