refine strategy; thanks Michi!

examples/oopsla/WFGCQS-19/queueing-network.pwhile

@@ -3,7 +3,7 @@ def qn ():
     l1 = 0
     l2 = 0
     i = 0
-    while i <= n:
+    while [l1 >= 0 and l2 >=0] i <= n:
         n = n - 1
         if l1 > 0:
             l1 = l1 - 1

pwhile.cabal

@@ -14,8 +14,8 @@ extra-source-files:
 
 Flag Debug
     Description: Enable debug support
-    Manual: True
-    Default: True
+    Manual: False
+    Default: False
 
 library
   hs-source-dirs: src

src/PWhile/InferEt.hs

@@ -194,10 +194,15 @@ normFromBExp :: BExp -> NormTemplate
 normFromBExp b = sum [ normFromExp (e1 - e2 + 1)
                      | e1 :>=: e2 <- S.toList (literals b) ]
 
-normFromCExp :: C.CExp Rational -> NormTemplate
-normFromCExp d = sum [ normFromBExp b + norm n
-                     | C.GNorm b k n <- varGNorms d
-                     , k > 0, not (C.isZeroN n) ]
+-- normFromCExp :: C.CExp Rational -> NormTemplate
+-- normFromCExp d = sum [ normFromBExp b + norm n
+--                      | C.GNorm b k n <- varGNorms d
+--                      , k > 0, not (C.isZeroN n) ]
+
+-- guardNormsFromCExp :: C.CExp Rational -> NormTemplate
+-- guardNormsFromCExp d = sum [ normFromBExp d
+--                            | C.GNorm b k n <-  varGNorms d
+--                            , k > 0, not (C.isZeroN n) ]
 
 substituteM :: (C.Norm -> SolveM NormTemplate) -> NormTemplate -> SolveM NormTemplate
 substituteM s = P.fromPolynomialM s (pure . P.coefficient)
@@ -315,11 +320,22 @@ expectation r@(E.Rand n) f =
 
 extractRanking :: C -> BExp -> BExp -> CExp -> CExp -> SolveM [C.Norm]
 extractRanking body i c g f = fmap templateToNorms $ do
-  let gNorm = normFromCExp g
-      fNorm = normFromCExp f
-      grdNorm = normFromBExp i + normFromBExp c
-  df <- substituteM delta fNorm
-  let lin = normFromExp 1 + grdNorm + fNorm + gNorm + sum [ normFromBExp c * df ]
+  let gGNs = varGNorms g
+      fGNs = varGNorms f
+      -- fNorm = fNorms + fGrds
+      -- gNorm = gNorms + gGrds
+      gGrds = sum [ normFromBExp b | C.GNorm b _ _ <- gGNs]
+      gNs    = sum [ norm n | C.GNorm _ _ n <- gGNs]
+      gNorms = gNs + gGrds
+
+      fGrds = sum [ normFromBExp b | C.GNorm b _ _ <- fGNs]
+      fNs    = sum [ norm n | C.GNorm _ _ n <- fGNs]
+      fNorms = fNs + fGrds
+
+      grdNorm = normFromBExp i + normFromBExp c -- + gGrds
+  df <- substituteM delta fNs
+  let lin = normFromExp 1 + grdNorm + fNorms + gNorms + sum [ normFromBExp c * df ]
+      -- cAdd = normFromExp 1 + grdNorm + gGrds
   template "linear" (pure lin)
     -- <|> template "shift-avg" (refine shiftAvg lin)
     -- <|> template "conditions" (refine conds lin)
@@ -327,6 +343,7 @@ extractRanking body i c g f = fmap templateToNorms $ do
     -- <|> template "mixed" (pure (grdNorm * grdNorm + lin))
     <|> template "shift-avg" (refine shiftAvg lin)
     <|> template "conditions" (refine conds lin)
+    <|> template "mixed-iteration" (pure (grdNorm * grdNorm + grdNorm))
     <|> template "shift-max" (refine shiftMax lin)
     <|> template "mixed-lin" (pure (grdNorm * lin + lin))
     -- <|> template "mixed-square" (pure (grdNorm * grdNorm + lin))
@@ -349,7 +366,8 @@ extractRanking body i c g f = fmap templateToNorms $ do
     conds = substituteM s where
       s n = do
         evn <- etM Evt body (C.nm 1 n)
-        pure $ norm n + sum [ normFromBExp b | C.GNorm b _ _ <-  varGNorms evn ]
+        pure $ norm n + sum [ normFromBExp b
+                            | C.GNorm b _ _ <-  varGNorms evn ]
 
     delta n@(C.Norm _ e) = do
       ns <- S.toList . C.norms <$> etM Evt body (C.nm 1 n)

src/PWhile/Util.hs

@@ -13,8 +13,9 @@ import qualified Text.PrettyPrint.ANSI.Leijen as PP
 
 renderPretty :: PP.Pretty e => e -> String
 -- TODO
-renderPretty d = ""
--- renderPretty d = PP.displayS (PP.renderSmart 1.0 120 (PP.pretty d)) ""
+-- renderPretty d = ""
+-- renderPretty d = PP.displayS (PP.renderCompact (PP.pretty d)) ""
+renderPretty d = PP.displayS (PP.renderSmart 1.0 12000 (PP.pretty d)) ""
 
 hPutPrettyLn :: PP.Pretty e => IO.Handle -> e -> IO ()
 hPutPrettyLn h = IO.hPutStrLn h . renderPretty