Commit ce812aa1 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

some parameterized examples

parent 09cd66c6
def seq ():
var n, x, r
x = n
while x >= 0:
x = x + unif(-2,1)
tick 1
x = n
while x >= 0:
x = x + unif(-2,1)
tick 1
def seq ():
var n, x, r
x = n
while x >= 0:
r = unif(-2,1)
x = x + r
tick 1
x = n
while x >= 0:
r = unif(-2,1)
x = x + r
tick 1
def seq ():
var n, x, r
x = n
while x >= 0:
x = x + unif(-2,1)
tick 1
x = n
while x >= 0:
x = x + unif(-2,1)
tick 1
x = n
while x >= 0:
x = x + unif(-2,1)
tick 1
def seq ():
var n, x, r
x = n
while x >= 0:
r = unif(-2,1)
x = x + r
tick 1
x = n
while x >= 0:
r = unif(-2,1)
x = x + r
tick 1
x = n
while x >= 0:
r = unif(-2,1)
x = x + r
tick 1
def qn ():
var l1, l2, n
l1 = 0
l2 = 0
while [l1 >= 0 and l2 >= 0] n>0:
n = n - 1
if l1 > 0:
l1 = l1 - 1
if l2 > 0:
l2 = l2 - 1
prob (49,1):
skip
else:
prob(1,4):
l1 = l1 + 3
else:
prob(1,1):
l2 = l2 + 2
else:
l1 = l1 + 2
l2 = l2 + 1
nondet:
tick l1
else:
tick l2
def seq ():
var n, x
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
n = x
while n >= 0:
prob(1,1):
n = n + 1
else:
n = n - 2
tick 1
x = x + 1
# Variation of linear/trader.imp
def trader():
var price, min, nShares
while price > min and min >= 0:
prob (1,3):
price = price + 1
else:
price = price - 1
nShares = unif(0,10000)
while nShares > 0:
nShares = nShares - 1
tick price
# Variation of linear/trader.imp
def trader():
var price, min, nShares
while price > min and min >= 0:
prob (1,3):
price = price + 1
else:
price = price - 1
nShares = unif(0,100000)
while nShares > 0:
nShares = nShares - 1
tick price
This diff is collapsed.
......@@ -86,8 +86,8 @@ traverseCoeff f = walk where
mapCoeff :: Coeff c' => (c -> c') -> CExp c -> CExp c'
mapCoeff f = runIdentity . traverseCoeff (pure . f)
fromNorm :: Num c => Norm -> CExp c
fromNorm = N 1
fromNorm :: (Eq c, Num c) => Norm -> CExp c
fromNorm = nm 1
zero :: (Num c) => CExp c
zero = N 0 (Norm Top 1)
......@@ -99,7 +99,7 @@ plus :: Coeff c => CExp c -> CExp c -> CExp c
plus (Cond g c1 c2) (Cond g' c1' c2')
| g == g' = Cond g (c1 `plus` c1') (c2 `plus` c2')
plus (Div c1 e1) (Div c2 e2) | e1 == e2 = (c1 `plus` c2) `divBy` e1
plus (N k1 n1) (N k2 n2) | n1 == n2 = nm (k1 + k2) n1 -- | k1 == k2 = nm k1 (n1 `plusN` n2)
plus (N k1 n1) (N k2 n2) | n1 == n2 = nm (k1 + k2) n1
plus c1 c2 | c1 == zero = c2
| c2 == zero = c1
| otherwise = Plus c1 c2
......@@ -188,7 +188,7 @@ instance E.Substitutable Norm where
substitute s e (Norm g f) = norm (E.substitute s e g) (E.substitute s e f)
instance Coeff c => E.Substitutable (CExp c) where
substitute s e (N k n) = N k (E.substitute s e n)
substitute s e (N k n) = nm k (E.substitute s e n)
substitute s e (Div c f) = E.substitute s e c `divBy` E.substitute s e f
substitute s e (Plus c d) = E.substitute s e c `plus` E.substitute s e d
substitute s e (Sup c d) = E.substitute s e c `sup` E.substitute s e d
......
......@@ -295,7 +295,6 @@ extractRanking :: C -> BExp -> BExp -> CExp -> CExp -> SolveM [C.Norm]
extractRanking body i c g f = fmap toNormList $ do
lin <- linearTemplate
template "linear" (pure lin)
<|> template "shift-avg" (refine shiftAvg lin)
<|> template "shift-avg" (refine shiftAvg lin)
<|> template "conditions" (refine conds lin)
<|> template "shift-max" (refine shiftMax lin)
......@@ -312,11 +311,15 @@ extractRanking body i c g f = fmap toNormList $ do
if r' `normTemplateEq` r then empty else pure r'
linearTemplate = do
let gNorm = normFromCExp (C.guarded c g)
fNorm = normFromCExp (C.guarded (neg c) f)
let gNorm = normFromCExp g
fNorm = normFromCExp f
grdNorm = normFromBExp i + normFromBExp c
df <- substituteM delta fNorm
pure (normFromExp 1 + normFromBExp i + normFromBExp c
+ fNorm + gNorm + sum [ normFromBExp c * df ])
logMsg2 "gNorm" gNorm
logMsg2 "fNorm" fNorm
logMsg2 "grdNorm" grdNorm
logMsg2 "fDiff" df
pure (normFromExp 1 + grdNorm + fNorm + gNorm + sum [ normFromBExp c * df ])
shiftAvg = substituteM s where
s n@(C.Norm _ e) = do
......
......@@ -199,7 +199,7 @@ pUnif v = do
pBer :: Exp -> Parser Program
pBer v = do
(a,b) <- symbol "ber" *> pTuple integer
return $ (v .~) $ bernoulli (a, b-1) (fromIntegral 1) (fromIntegral 0)
return $ (v .~) $ bernoulli (fromIntegral a, fromIntegral $ b-a) 1 0
pHyper :: Exp -> Parser Program
pHyper v = do
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment