Commit 1f0e2943 authored by Michael Schaper's avatar Michael Schaper
Browse files

add queuingNetwork example

parent 33d10265
......@@ -1226,3 +1226,44 @@ tarjan = do
tick
y .= y - 1
n .= n - 1
-- 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
let
ite g a b = if g then a else b
p1 = do
choice
[ (2, l1 .= l1 + 3)
, (5, l2 .= l2 + 2)
, (3, do {l1 .= l1 + 2; l2 .= l2 + 1}) ]
-- consume (l1 + l2)
nondet[ consume l1,consume l2 ]
-- ite (l1 .>= l2) (consume l1) (consume l2)
p0 = choice [ (1 , p1), (98, skip) ]
assume (l1 .>= 0 .&& l2 .>= 0) skip
n .= n -1
-- ite (l1 .>= 1) (l1 .= l1 - 1) skip
-- ite (l2 .>= 1) (l2 .= l2 - 1) skip
p0
queuingNetwork' :: Program
queuingNetwork' = do
l1 <- var "l1"; l2 <- var "l2"; n <- var "n"
-- l1 .= 0
l2 .= 0
let
ite g a b = if g then a else b
while' (n .> 0) $ do
-- assume (l1 .>= 0 .&& l2 .>= 0) skip
n .= n -1
ite (l1 .>= 1) (l1 .= l1 - 1) skip
consume l1
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