templates templates templates

examples/2drobot.imp

-# 2D Robot 
-# Chatterjee et al., Cost Analysis of Nondeterministic Programs
-#
-# **2D Robot** We consider a robot walking in a plane. Suppose
-# that the robot is initially located below the line y = x and
-# we want it to cross this line, i.e. the program continues until
-# the robot crosses the line. At each iteration, the robot prob-
-# abilistically chooses one of the following 9 directions and
-# moves in that direction: {0: North, 1: South, 2: East, 3: West, 4:
-# Northeast, 5: Southeast, 6: Northwest, 7: Southwest, 8: Stay}.
-# Moreover, the robot’s step size is a uniformly random vari-
-# able between 1 and 3. At the end of each iteration, a cost is
-# incurred, which is dependent on the distance between the
-# robot and the line y = x.
-
-# Note: use approximation `tick(x-y)` instead of `tick(0.707 * (x-y))`
-
-def f():
-  var x, y, r, a, b
-
-  x = a
-  y = b
-
-  while y <= x:
-    prob(1,4):
-      r = unif(1,3)
-      y = y + r
-    else:
-      prob(1,7):
-        r = unif(1,3)
-        y = y - r
-      else:
-        prob(1,6):
-          r = unif(1,3)
-          x = x + r
-        else:
-          prob(1,5):
-            r = unif(1,3)
-            x = x - r
-          else:
-            prob(1,4):
-              r = unif(1,3)
-              x = x + r
-              r = unif(1,3)
-              y = y + r
-            else:
-              prob(1,3):
-                r = unif(1,3)
-                x = x + r
-                r = unif(1,3)
-                y = y - r
-              else:
-                prob(1,2):
-                  r = unif(1,3)
-                  x = x - r
-                  r = unif(1,3)
-                  y = y + r
-                else:
-                  prob(1,1):
-                    r = unif(1,3)
-                    x = x - r
-                    r = unif(1,3)
-                    y = y - r
-                  else:
-                    skip
-
-		# tick(0.707 * (x-y))
-    tick(x-y)
-

src/Data/PWhile/CostExpression.hs

@@ -34,6 +34,7 @@ mulN :: Norm -> Norm -> Norm
 mulN (Norm _ 1)   n@Norm{}     = n
 mulN n@Norm{}     (Norm _ 1)   = n
 mulN (Norm g1 e1) (Norm g2 e2) = norm (g1 .&& g2) (e1 * e2)
+-- mulN (Norm g1 e1) (Norm g2 e2) = norm (g1 .&& g2) (e1 * e2)
 
 prodN :: [Norm] -> Norm
 prodN = foldl mulN oneN

src/PWhile/InferEt.hs

@@ -12,7 +12,7 @@ module PWhile.InferEt
   , showResult
   ) where
 
-
+import           Data.List                    (nub)
 import           Control.Applicative
 import           Control.Monad.Except
 import qualified Control.Monad.State          as St
@@ -167,7 +167,7 @@ varGNorms = filter (not . C.isConstGN) . C.gNorms
 type NormTemplate = P.Polynomial C.Norm Int
 
 templateToNorms :: NormTemplate -> [C.Norm]
-templateToNorms p =
+templateToNorms p = nub $
   filter (not . zeroN) [ C.prodN [ C.expN n k | (n,k) <- P.toPowers m ]
                        | (_,m) <- P.toMonos p]
   where zeroN (C.Norm _ e) = e == 0
@@ -317,7 +317,8 @@ extractRanking body i c g f = fmap templateToNorms $ do
     <|> template "shift-avg" (refine shiftAvg lin)
     <|> template "conditions" (refine conds lin)
     <|> template "shift-max" (refine shiftMax lin)
-    <|> template "mixed" (pure (grdNorm * grdNorm + lin))
+    <|> template "mixed-lin" (pure (grdNorm * lin + lin))
+    <|> template "mixed-square" (pure (grdNorm * grdNorm + lin))
     <|> template "square" (pure (lin * lin + lin))
    where
     refine m r = do
@@ -411,6 +412,7 @@ et Ect (Seq c1 c2) f
 et t (Seq c1 c2) f         = etM t c1 =<< etM t c2 f
 et t d@(While _  i b c) f  = logBlk "While.step" $ do
   logData "Problem" d
+  logData "f" f
   g <- case t of {Evt -> return C.zero; Ect -> logBlk "Expected Cost Body" $ et Ect c C.zero}
   ns <- logResult "Norms" $ extractRanking c i b g f
   hs <- traverse (et Evt c . C.fromNorm) ns