experiments table

examples/oopsla/NCH-18/linear/prseq-2.absynth

-# sequential loops program so that 
-# the second loop depends on the first
-# both are probabilistic loops
-
-def f():
-    var x, y
-    assume y >= 10
-
-    while x - y > 0:
-        y = y + unif(1, 3)
-        tick 3
-    while y > 0:
-        prob(2,1):
-            y = y - 10
-        else:
-            y = y - 0
-        tick 1
-

examples/oopsla/NCH-18/linear/prseq-2.pwhile

-# sequential loops program so that
-# the second loop depends on the first
-# both are probabilistic loops
-
-def f():
-    var x, y, r
-    assume y >= 10
-
-    while x - y > 0:
-        r = unif(1, 3)
-        y = y + r
-        tick 3
-    while y > 0:
-        prob(2,1):
-            y = y - 10
-        else:
-            y = y - 0
-        tick 1

examples/oopsla/NCH-18/linear/prspeed-2.imp

-def f():
-    var x, y, m, n
-
-    while x <= n:
-        if y < m:
-            prob(1,1):
-                y = y + 1
-            else:
-                y = y + 0
-        else:
-            prob(1,3):
-                x = x + 0
-            else:
-                prob(1,2):
-                  x = x + 1
-                else:
-                    prob(1,1):
-                        x = x + 2
-                    else:
-                        x = x + 3
-        tick 1

src/Data/PWhile/CostExpression.hs

@@ -72,6 +72,7 @@ data CExp c =
 
 nm :: (Eq c, Num c) => c -> Norm -> CExp c
 nm 0 _                       = zero
+nm _ (Norm Bot _)            = zero
 nm c (Norm _ (E.Constant i)) = N (c * fromIntegral i) (norm Top 1)
 nm c (Norm b e)              = N (c * fromIntegral k) (norm b e')
   where (k,e') = E.cfactor e