Commit 266aa412 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

coupon example sec 8.2

parent 1f0e2943
...@@ -1235,7 +1235,7 @@ queuingNetwork = do ...@@ -1235,7 +1235,7 @@ queuingNetwork = do
l2 .= 0 l2 .= 0
while' (n .> 0) $ do while' (n .> 0) $ do
let let
ite g a b = if g then a else b ite g a b = if g then a else b
p1 = do p1 = do
...@@ -1244,14 +1244,14 @@ queuingNetwork = do ...@@ -1244,14 +1244,14 @@ queuingNetwork = do
, (5, l2 .= l2 + 2) , (5, l2 .= l2 + 2)
, (3, do {l1 .= l1 + 2; l2 .= l2 + 1}) ] , (3, do {l1 .= l1 + 2; l2 .= l2 + 1}) ]
-- consume (l1 + l2) -- consume (l1 + l2)
nondet[ consume l1,consume l2 ] -- nondet[ consume l1,consume l2 ]
-- ite (l1 .>= l2) (consume l1) (consume l2) ite (l1 .>= l2) (consume l1) (consume l2)
p0 = choice [ (1 , p1), (98, skip) ] p0 = choice [ (1 , p1), (98, skip) ]
assume (l1 .>= 0 .&& l2 .>= 0) skip assume (l1 .>= 0 .&& l2 .>= 0) skip
n .= n -1 n .= n -1
-- ite (l1 .>= 1) (l1 .= l1 - 1) skip ite (l1 .>= 1) (l1 .= l1 - 1) skip
-- ite (l2 .>= 1) (l2 .= l2 - 1) skip ite (l2 .>= 1) (l2 .= l2 - 1) skip
p0 p0
queuingNetwork' :: Program queuingNetwork' :: Program
...@@ -1259,11 +1259,10 @@ queuingNetwork' = do ...@@ -1259,11 +1259,10 @@ queuingNetwork' = do
l1 <- var "l1"; l2 <- var "l2"; n <- var "n" l1 <- var "l1"; l2 <- var "l2"; n <- var "n"
-- l1 .= 0 -- l1 .= 0
l2 .= 0 l2 .= 0
let let
ite g a b = if g then a else b ite g a b = if g then a else b
while' (n .> 0) $ do while' (n .> 0) $ do
-- assume (l1 .>= 0 .&& l2 .>= 0) skip -- assume (l1 .>= 0 .&& l2 .>= 0) skip
n .= n -1 n .= n -1
ite (l1 .>= 1) (l1 .= l1 - 1) skip ite (l1 .>= 1) (l1 .= l1 - 1) skip
consume l1 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