Commit 16a60407 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

network example

parent 615565a3
......@@ -1227,9 +1227,50 @@ tarjan = do
y .= y - 1
n .= n - 1
ifp p c1 c2 = choice [(p, c1), (100 - p, c2)]
-- Wang et al. 2019, Cost Analysis of Nondeterministic Probabilistic Programs
qb :: Program
qb = do
l1 <- var "l1"; l2 <- var "l2"; n <- var "n"
if l1 .>= 1 then l1 .= l1 - 1 else skip
if l2 .>= 1 then l2 .= l2 - 1 else skip
ifp 98 skip $
ifp 20 (l1 .= l1 + 3)
(ifp 50 (l2 .= l2 + 2)
(do
l1 .= l1 + 2
l2 .= l2 + 1))
nondet [consume l1, consume l2]
-- if l1 .>= l2 then consume l1 else consume l2
-- Wang et al. 2019, Cost Analysis of Nondeterministic Probabilistic Programs
queuingNetwork :: Program
queuingNetwork = do
l1 <- var "l1"; l2 <- var "l2"; n <- var "n"
l1 .= 0
l2 .= 0
while' (n .> 0) $ do
assume (l1 .>= 0 .&& l2 .>= 0) $ do
n .= n - 1
if l1 .>= 1 then l1 .= l1 - 1 else skip
if l2 .>= 1 then l2 .= l2 - 1 else skip
ifp 98 skip $
ifp 20 (l1 .= l1 + 3)
(ifp 50 (l2 .= l2 + 2)
(do
l1 .= l1 + 2
l2 .= l2 + 1))
nondet [consume l1, consume l2]
-- if l1 .>= l2 then consume l1 else consume l2
queuingNetwork'' :: Program
queuingNetwork'' = do
l1 <- var "l1"; l2 <- var "l2"; n <- var "n"
l1 .= 0
l2 .= 0
......
Supports Markdown
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