Skip to content
GitLab
Commit 105059b5 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

more extensive output of norms

parent 07f3784c
Show whitespace changes
Inline Side-by-side
examples/results
View file @ 105059b5
This source diff could not be displayed because it is too large. You can view the blob instead.
examples/results.txt
View file @ 105059b5
processing ... examples/oopsla/2drobot.imp
 examples/oopsla/2drobot.imp : 2.622s : [Success] 1/2·<a + -2·(a·b) + a^2 + -b + b^2> + 2·<1 + 2·(a) + -2·(a·b) + a^2 + -2·(b) + b^2> + 1267/18·<6 + a + -b>
processing ... examples/oopsla/absynth/linear/2drwalk.imp
 examples/oopsla/absynth/linear/2drwalk.imp : 0.021s : [Success] 2·<1 + -d + n>
processing ... examples/oopsla/absynth/linear/C4B_t09.imp
 examples/oopsla/absynth/linear/C4B_t09.imp : 0.006s : [Success] 41·<x>
processing ... examples/oopsla/absynth/linear/C4B_t13.imp
 examples/oopsla/absynth/linear/C4B_t13.imp : 0.005s : [Success] [y ≥ 0] · (5/4·<x> + <y>)
processing ... examples/oopsla/absynth/linear/C4B_t15.imp
 examples/oopsla/absynth/linear/C4B_t15.imp : 0.137s : [Failed ]
processing ... examples/oopsla/absynth/linear/C4B_t15_2.imp
 examples/oopsla/absynth/linear/C4B_t15_2.imp : 0.005s : [Success] [y ≥ 0] · 2·<1 + x>
processing ... examples/oopsla/absynth/linear/C4B_t19.imp
 examples/oopsla/absynth/linear/C4B_t19.imp : 0.005s : [Success] 2·<-100 + i> + <51 + i + k>
processing ... examples/oopsla/absynth/linear/C4B_t30.imp
 examples/oopsla/absynth/linear/C4B_t30.imp : 0.010s : [Failed ]
processing ... examples/oopsla/absynth/linear/C4B_t30_2.imp
 examples/oopsla/absynth/linear/C4B_t30_2.imp : 0.002s : [Success] [y ≥ -1] · (<2 + y> + <x>)
processing ... examples/oopsla/absynth/linear/C4B_t61.imp
 examples/oopsla/absynth/linear/C4B_t61.imp : 0.005s : [Success] 160/19·<-7 + l> + 7
processing ... examples/oopsla/absynth/linear/bayesian_network.imp
 examples/oopsla/absynth/linear/bayesian_network.: 0.002s : [Success] 5·<n>
processing ... examples/oopsla/absynth/linear/ber.imp
 examples/oopsla/absynth/linear/ber.imp : 0.001s : [Success] 2·<n + -x>
processing ... examples/oopsla/absynth/linear/bin.imp
 examples/oopsla/absynth/linear/bin.imp : 0.006s : [Success] 1024/1023·<n>
processing ... examples/oopsla/absynth/linear/condand.imp
 examples/oopsla/absynth/linear/condand.imp : 0.002s : [Success] 2·<m>
processing ... examples/oopsla/absynth/linear/cooling.pwhile
 examples/oopsla/absynth/linear/cooling.pwhile : 0.015s : [Success] 21/10·<1 + t> + <mt + -st>
processing ... examples/oopsla/absynth/linear/coupon.imp
 examples/oopsla/absynth/linear/coupon.imp : 0.003s : [Success] 25
processing ... examples/oopsla/absynth/linear/cowboy_duel.imp
 examples/oopsla/absynth/linear/cowboy_duel.imp : 0.001s : [Success] 6/5
processing ... examples/oopsla/absynth/linear/cowboy_duel_3way.pwhile
 examples/oopsla/absynth/linear/cowboy_duel_3way.: 0.004s : [Success] 83/24
processing ... examples/oopsla/absynth/linear/fcall.pwhile
 examples/oopsla/absynth/linear/fcall.pwhile : 0.001s : [Success] 2·<n + -x>
processing ... examples/oopsla/absynth/linear/filling_vol.pwhile
 examples/oopsla/absynth/linear/filling_vol.pwhil: 0.009s : [Success] 3/5·<1 + volToFill> + 3/5·<volToFill>
processing ... examples/oopsla/absynth/linear/geo.pwhile
 examples/oopsla/absynth/linear/geo.pwhile : 0.001s : [Success] <1>
processing ... examples/oopsla/absynth/linear/hyper.pwhile
 examples/oopsla/absynth/linear/hyper.pwhile : 0.001s : [Success] 145/28·<-1 + n + -x>
processing ... examples/oopsla/absynth/linear/linear01.imp
 examples/oopsla/absynth/linear/linear01.imp : 0.001s : [Success] <-1 + x>
processing ... examples/oopsla/absynth/linear/no_loop.imp
 examples/oopsla/absynth/linear/no_loop.imp : 0.000s : [Success] 5
processing ... examples/oopsla/absynth/linear/prdwalk.pwhile
 examples/oopsla/absynth/linear/prdwalk.pwhile : 0.002s : [Success] 8/3·<n + -x>
processing ... examples/oopsla/absynth/linear/prnes.pwhile
 examples/oopsla/absynth/linear/prnes.pwhile : 0.145s : [Success] [y ≥ 0] · (50/9·<99·(n) + -n·y> + 250000/81·<n^2>)
processing ... examples/oopsla/absynth/linear/prseq-2.pwhile
 examples/oopsla/absynth/linear/prseq-2.pwhile : 0.010s : [Success] [y ≥ 10] · (3·<x + -y> + 3·<x + -y> + 3/2·<y>)
processing ... examples/oopsla/absynth/linear/prseq.pwhile
 examples/oopsla/absynth/linear/prseq.pwhile : 0.010s : [Success] [y ≥ 10] · (3·<-2 + x + -y> + 3/2·<-9 + y> + 3·<-2 + x + -y>)
processing ... examples/oopsla/absynth/linear/prseq_bin.pwhile
 examples/oopsla/absynth/linear/prseq_bin.pwhile : 0.015s : [Success] [y ≥ 10] · (16/5·<-2 + x + -y> + 3/2·<-9 + y> + 16/5·<-2 + x + -y>)
processing ... examples/oopsla/absynth/linear/prspeed-2.imp
 examples/oopsla/absynth/linear/prspeed-2.imp : 0.012s : [Success] 4/3·<1 + n + -x> + 2·<m + -y>
processing ... examples/oopsla/absynth/linear/prspeed.imp
 examples/oopsla/absynth/linear/prspeed.imp : 0.015s : [Success] 4/3·<-2 + n + -x> + 2·<m + -y>
processing ... examples/oopsla/absynth/linear/race.pwhile
 examples/oopsla/absynth/linear/race.pwhile : 0.011s : [Success] 11/6·<3 + -h + t>
processing ... examples/oopsla/absynth/linear/rdseql.imp
 examples/oopsla/absynth/linear/rdseql.imp : 0.008s : [Success] [y ≥ 0] · (9/4·<x> + <y>)
processing ... examples/oopsla/absynth/linear/rdspeed.pwhile
 examples/oopsla/absynth/linear/rdspeed.pwhile : 0.013s : [Success] 4/3·<-2 + n + -x> + 2·<m + -y>
processing ... examples/oopsla/absynth/linear/rdwalk.imp
 examples/oopsla/absynth/linear/rdwalk.imp : 0.003s : [Success] 2·<1 + n + -x>
processing ... examples/oopsla/absynth/linear/rejection_sampling.imp
 examples/oopsla/absynth/linear/rejection_samplin: 0.002s : [Success] 2·<n>
processing ... examples/oopsla/absynth/linear/rfind_lv.imp
 examples/oopsla/absynth/linear/rfind_lv.imp : 0.001s : [Success] 2
processing ... examples/oopsla/absynth/linear/rfind_mc.imp
 examples/oopsla/absynth/linear/rfind_mc.imp : 0.002s : [Success] <k>
processing ... examples/oopsla/absynth/linear/robot.imp
 examples/oopsla/absynth/linear/robot.imp : 0.005s : [Success] 5/4·<n>
processing ... examples/oopsla/absynth/linear/roulette.pwhile
 examples/oopsla/absynth/linear/roulette.pwhile : 0.027s : [Success] 74/15·<10011 + -n>
processing ... examples/oopsla/absynth/linear/sprdwalk.pwhile
 examples/oopsla/absynth/linear/sprdwalk.pwhile : 0.001s : [Success] 2·<n + -x>
processing ... examples/oopsla/absynth/linear/trapped_miner.imp
 examples/oopsla/absynth/linear/trapped_miner.imp: 0.002s : [Success] 15/2·<n>
processing ... examples/oopsla/absynth/polynomial/complex.pwhile
 examples/oopsla/absynth/polynomial/complex.pwhil: 0.029s : [Success] [M ≥ 0 ∧ y ≥ 0] · (<w> + 18·<M·N + N> + 3·<y>)
processing ... examples/oopsla/absynth/polynomial/multirace.pwhile
 examples/oopsla/absynth/polynomial/multirace.pwh: 0.011s : [Success] [m ≥ 0] · 4·<m·n + n>
processing ... examples/oopsla/absynth/polynomial/pol04.imp
 examples/oopsla/absynth/polynomial/pol04.imp : 0.012s : [Success] 15/2·<x> + 9/2·<x^2>
processing ... examples/oopsla/absynth/polynomial/pol05.pwhile
 examples/oopsla/absynth/polynomial/pol05.pwhile : 0.011s : [Success] 3/4·<x> + 3/2·<x^2>
processing ... examples/oopsla/absynth/polynomial/pol06.pwhile
 examples/oopsla/absynth/polynomial/pol06.pwhile : 0.038s : [Success] <1 + minPrice + minPrice·sPrice + sPrice> + <-minPrice + -minPrice·sPrice + sPrice + sPrice^2>
processing ... examples/oopsla/absynth/polynomial/pol07.imp
 examples/oopsla/absynth/polynomial/pol07.imp : 0.013s : [Success] 3/2·<1 + -2·(n) + n^2>
processing ... examples/oopsla/absynth/polynomial/rdbub.pwhile
 examples/oopsla/absynth/polynomial/rdbub.pwhile : 0.009s : [Success] 3·<n^2>
processing ... examples/oopsla/absynth/polynomial/simple_game.imp
 examples/oopsla/absynth/polynomial/simple_game.i: 0.005s : [Success] 2·<1 + x>
processing ... examples/oopsla/absynth/polynomial/trader.pwhile
 examples/oopsla/absynth/polynomial/trader.pwhile: 0.042s : [Success] 20·<-minPrice + minPrice·sPrice + -minPrice^2 + sPrice> + 10·<-2·(minPrice·sPrice) + minPrice^2 + sPrice^2>
processing ... examples/oopsla/NCH-18/linear/2drwalk.imp
 examples/oopsla/NCH-18/linear/2drwalk.imp : 0.034s : [Success] 2·[1 + -d + n | 1 + -d + n ≥ 0]
processing ... examples/oopsla/NCH-18/linear/C4B_t09.imp
 examples/oopsla/NCH-18/linear/C4B_t09.imp : 0.009s : [Success] 41·[x | x ≥ 0]
processing ... examples/oopsla/NCH-18/linear/C4B_t13.imp
 examples/oopsla/NCH-18/linear/C4B_t13.imp : 0.005s : [Success] [y ≥ 0] · (5/4·[x | x ≥ 0] + [y | y ≥ 0])
processing ... examples/oopsla/NCH-18/linear/C4B_t15.imp
 examples/oopsla/NCH-18/linear/C4B_t15.imp : 0.143s : [Failed ]
processing ... examples/oopsla/NCH-18/linear/C4B_t15_2.imp
 examples/oopsla/NCH-18/linear/C4B_t15_2.imp : 0.005s : [Success] [y ≥ 0] · 2·[1 + x | 1 + x ≥ 0]
processing ... examples/oopsla/NCH-18/linear/C4B_t19.imp
 examples/oopsla/NCH-18/linear/C4B_t19.imp : 0.005s : [Success] 2·[-100 + i | -100 + i ≥ 0] + [51 + i + k | 51 + i + k ≥ 0]
processing ... examples/oopsla/NCH-18/linear/C4B_t30.imp
 examples/oopsla/NCH-18/linear/C4B_t30.imp : 0.011s : [Failed ]
processing ... examples/oopsla/NCH-18/linear/C4B_t30_2.imp
 examples/oopsla/NCH-18/linear/C4B_t30_2.imp : 0.001s : [Success] [y ≥ -1] · ([2 + y | 2 + y ≥ 0] + [x | x ≥ 0])
processing ... examples/oopsla/NCH-18/linear/C4B_t61.imp
 examples/oopsla/NCH-18/linear/C4B_t61.imp : 0.005s : [Success] 160/19·[-7 + l | -7 + l ≥ 0] + 7
processing ... examples/oopsla/NCH-18/linear/bayesian_network.imp
 examples/oopsla/NCH-18/linear/bayesian_network.i: 0.002s : [Success] 5·[n | n ≥ 0]
processing ... examples/oopsla/NCH-18/linear/ber.imp
 examples/oopsla/NCH-18/linear/ber.imp : 0.001s : [Success] 2·[n + -x | n + -x ≥ 0]
processing ... examples/oopsla/NCH-18/linear/bin.imp
 examples/oopsla/NCH-18/linear/bin.imp : 0.006s : [Success] 1024/1023·[n | n ≥ 0]
processing ... examples/oopsla/NCH-18/linear/condand.imp
 examples/oopsla/NCH-18/linear/condand.imp : 0.002s : [Success] 2·[m | m ≥ 0]
processing ... examples/oopsla/NCH-18/linear/cooling.pwhile
 examples/oopsla/NCH-18/linear/cooling.pwhile : 0.016s : [Success] 21/10·[1 + t | 1 + t ≥ 0] + [mt + -st | mt + -st ≥ 0]
processing ... examples/oopsla/NCH-18/linear/coupon.imp
 examples/oopsla/NCH-18/linear/coupon.imp : 0.003s : [Success] 25
processing ... examples/oopsla/NCH-18/linear/cowboy_duel.imp
 examples/oopsla/NCH-18/linear/cowboy_duel.imp : 0.001s : [Success] 6/5
processing ... examples/oopsla/NCH-18/linear/cowboy_duel_3way.pwhile
 examples/oopsla/NCH-18/linear/cowboy_duel_3way.p: 0.004s : [Success] 83/24
processing ... examples/oopsla/NCH-18/linear/fcall.pwhile
 examples/oopsla/NCH-18/linear/fcall.pwhile : 0.001s : [Success] 2·[n + -x | n + -x ≥ 0]
processing ... examples/oopsla/NCH-18/linear/filling_vol.pwhile
 examples/oopsla/NCH-18/linear/filling_vol.pwhile: 0.010s : [Success] 3/5·[1 + volToFill | 1 + volToFill ≥ 0] + 3/5·[volToFill | volToFill ≥ 0]
processing ... examples/oopsla/NCH-18/linear/geo.pwhile
 examples/oopsla/NCH-18/linear/geo.pwhile : 0.001s : [Success] [1 | ⊤]
processing ... examples/oopsla/NCH-18/linear/hyper.pwhile
 examples/oopsla/NCH-18/linear/hyper.pwhile : 0.002s : [Success] 145/28·[-1 + n + -x | -1 + n + -x ≥ 0]
processing ... examples/oopsla/NCH-18/linear/linear01.imp
 examples/oopsla/NCH-18/linear/linear01.imp : 0.001s : [Success] [-1 + x | -1 + x ≥ 0]
processing ... examples/oopsla/NCH-18/linear/no_loop.imp
 examples/oopsla/NCH-18/linear/no_loop.imp : 0.000s : [Success] 5
processing ... examples/oopsla/NCH-18/linear/prdwalk.pwhile
 examples/oopsla/NCH-18/linear/prdwalk.pwhile : 0.003s : [Success] 8/3·[n + -x | n + -x ≥ 0]
processing ... examples/oopsla/NCH-18/linear/prnes.pwhile
 examples/oopsla/NCH-18/linear/prnes.pwhile : 0.146s : [Success] [y ≥ 0] · (50/9·[99·(n) + -n·y | -99 + y ≥ 0 ∧ -n ≥ 0] + 250000/81·[n^2 | -n ≥ 0])
processing ... examples/oopsla/NCH-18/linear/prseq-2.pwhile
 examples/oopsla/NCH-18/linear/prseq-2.pwhile : 0.009s : [Success] [y ≥ 10] · (3·[x + -y | x + -y ≥ 0] + 3·[x + -y | x + -y ≥ 0] + 3/2·[y | y ≥ 0])
processing ... examples/oopsla/NCH-18/linear/prseq.pwhile
 examples/oopsla/NCH-18/linear/prseq.pwhile : 0.010s : [Success] [y ≥ 10] · (3·[-2 + x + -y | -2 + x + -y ≥ 0] + 3/2·[-9 + y | -9 + y ≥ 0] + 3·[-2 + x + -y | -2 + x + -y ≥ 0])
processing ... examples/oopsla/NCH-18/linear/prseq_bin.pwhile
 examples/oopsla/NCH-18/linear/prseq_bin.pwhile : 0.016s : [Success] [y ≥ 10] · (16/5·[-2 + x + -y | -2 + x + -y ≥ 0] + 3/2·[-9 + y | -9 + y ≥ 0] + 16/5·[-2 + x + -y | -2 + x + -y ≥ 0])
processing ... examples/oopsla/NCH-18/linear/prspeed-2.imp
 examples/oopsla/NCH-18/linear/prspeed-2.imp : 0.013s : [Success] 4/3·[1 + n + -x | 1 + n + -x ≥ 0] + 2·[m + -y | m + -y ≥ 0]
processing ... examples/oopsla/NCH-18/linear/prspeed.imp
 examples/oopsla/NCH-18/linear/prspeed.imp : 0.014s : [Success] 4/3·[-2 + n + -x | -2 + n + -x ≥ 0] + 2·[m + -y | m + -y ≥ 0]
processing ... examples/oopsla/NCH-18/linear/race.pwhile
 examples/oopsla/NCH-18/linear/race.pwhile : 0.012s : [Success] 11/6·[3 + -h + t | 3 + -h + t ≥ 0]
processing ... examples/oopsla/NCH-18/linear/rdseql.imp
 examples/oopsla/NCH-18/linear/rdseql.imp : 0.007s : [Success] [y ≥ 0] · (9/4·[x | x ≥ 0] + [y | y ≥ 0])
processing ... examples/oopsla/NCH-18/linear/rdspeed.pwhile
 examples/oopsla/NCH-18/linear/rdspeed.pwhile : 0.013s : [Success] 4/3·[-2 + n + -x | -2 + n + -x ≥ 0] + 2·[m + -y | m + -y ≥ 0]
processing ... examples/oopsla/NCH-18/linear/rdwalk.imp
 examples/oopsla/NCH-18/linear/rdwalk.imp : 0.003s : [Success] 2·[1 + n + -x | 1 + n + -x ≥ 0]
processing ... examples/oopsla/NCH-18/linear/rejection_sampling.imp
 examples/oopsla/NCH-18/linear/rejection_sampling: 0.002s : [Success] 2·[n | n ≥ 0]
processing ... examples/oopsla/NCH-18/linear/rfind_lv.imp
 examples/oopsla/NCH-18/linear/rfind_lv.imp : 0.001s : [Success] 2
processing ... examples/oopsla/NCH-18/linear/rfind_mc.imp
 examples/oopsla/NCH-18/linear/rfind_mc.imp : 0.002s : [Success] [k | k ≥ 0]
processing ... examples/oopsla/NCH-18/linear/robot.imp
 examples/oopsla/NCH-18/linear/robot.imp : 0.026s : [Success] 5/4·[n | n ≥ 0]
processing ... examples/oopsla/NCH-18/linear/roulette.pwhile
 examples/oopsla/NCH-18/linear/roulette.pwhile : 0.031s : [Success] 74/15·[10011 + -n | 10011 + -n ≥ 0]
processing ... examples/oopsla/NCH-18/linear/sprdwalk.pwhile
 examples/oopsla/NCH-18/linear/sprdwalk.pwhile : 0.001s : [Success] 2·[n + -x | n + -x ≥ 0]
processing ... examples/oopsla/NCH-18/linear/trapped_miner.imp
 examples/oopsla/NCH-18/linear/trapped_miner.imp : 0.002s : [Success] 15/2·[n | n ≥ 0]
processing ... examples/oopsla/NCH-18/polynomial/complex.pwhile
 examples/oopsla/NCH-18/polynomial/complex.pwhile: 0.030s : [Success] [M ≥ 0 ∧ y ≥ 0] · ([w | w ≥ 0] + 18·[M·N + N | 3 + 3·(M) ≥ 0 ∧ N ≥ 0] + 3·[y | y ≥ 0])
processing ... examples/oopsla/NCH-18/polynomial/multirace.pwhile
 examples/oopsla/NCH-18/polynomial/multirace.pwhi: 0.012s : [Success] [m ≥ 0] · 4·[m·n + n | 1 + m ≥ 0 ∧ n ≥ 0]
processing ... examples/oopsla/NCH-18/polynomial/pol04.imp
 examples/oopsla/NCH-18/polynomial/pol04.imp : 0.011s : [Success] 15/2·[x | x ≥ 0] + 9/2·[x^2 | x ≥ 0]
processing ... examples/oopsla/NCH-18/polynomial/pol05.pwhile
 examples/oopsla/NCH-18/polynomial/pol05.pwhile : 0.011s : [Success] 3/4·[x | x ≥ 0] + 3/2·[x^2 | x ≥ 0]
processing ... examples/oopsla/NCH-18/polynomial/pol06.pwhile
 examples/oopsla/NCH-18/polynomial/pol06.pwhile : 0.041s : [Success] [1 + minPrice + minPrice·sPrice + sPrice | 1 + minPrice ≥ 0 ∧ 1 + sPrice ≥ 0] + [-minPrice + -minPrice·sPrice + sPrice
+ sPrice^2 | 1 + sPrice ≥ 0 ∧
-minPrice + sPrice ≥ 0]
processing ... examples/oopsla/NCH-18/polynomial/pol07.imp
 examples/oopsla/NCH-18/polynomial/pol07.imp : 0.013s : [Success] 3/2·[1 + -2·(n) + n^2 | -1 + n ≥ 0]
processing ... examples/oopsla/NCH-18/polynomial/rdbub.pwhile
 examples/oopsla/NCH-18/polynomial/rdbub.pwhile : 0.009s : [Success] 3·[n^2 | n ≥ 0]
processing ... examples/oopsla/NCH-18/polynomial/simple_game.imp
 examples/oopsla/NCH-18/polynomial/simple_game.im: 0.005s : [Success] 2·[1 + x | 1 + x ≥ 0]
processing ... examples/oopsla/NCH-18/polynomial/trader.pwhile
 examples/oopsla/NCH-18/polynomial/trader.pwhile : 0.110s : [Success] 20·[-minPrice + minPrice·sPrice + -minPrice^2 + sPrice | 1 + minPrice ≥ 0 ∧ -minPrice + sPrice ≥ 0]
+ 10·[-2·(minPrice·sPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice ≥ 0]
processing ... examples/oopsla/WFGCQS-19/2drobot.imp
 examples/oopsla/WFGCQS-19/2drobot.imp : 60.00s : [Timeout]
processing ... examples/oopsla/WFGCQS-19/queueing-network.pwhile
 examples/oopsla/WFGCQS-19/queueing-network.pwhil: 27.80s : [Success] 2·[-1 + -n | ⊥] + 4/125·[1 + n | 1 + n ≥ 0] + 3/250·[1 + 2·(n) + n^2 | 1 + n ≥ 0]
processing ... examples/oopsla/bridge.imp
 examples/oopsla/bridge.imp : 0.008s : [Success] <-a·b + a·x + b·x + -x^2>
 examples/oopsla/bridge.imp : 0.009s : [Success] [-a·b + a·x + b·x + -x^2 | -a + x ≥ 0 ∧ b + -x ≥ 0]
processing ... examples/oopsla/coupons-10.imp
 examples/oopsla/coupons-10.imp : 0.016s : [Success] 110
 examples/oopsla/coupons-10.imp : 0.028s : [Success] 110
processing ... examples/oopsla/coupons-100.imp
 examples/oopsla/coupons-100.imp : 1.140s : [Success] 10100
 examples/oopsla/coupons-100.imp : 1.237s : [Success] 10100
processing ... examples/oopsla/coupons-50.imp
 examples/oopsla/coupons-50.imp : 0.308s : [Success] 2550
 examples/oopsla/coupons-50.imp : 0.314s : [Success] 2550
processing ... examples/oopsla/coupons-N.pwhile
 examples/oopsla/coupons-N.pwhile : 0.175s : [Success] 1/2 + <N> + 1/2·<N^2>
 examples/oopsla/coupons-N.pwhile : 0.195s : [Success] 1/2 + [N | N ≥ 0] + 1/2·[N^2 | N ≥ 0]
processing ... examples/oopsla/nest-2.pwhile
 examples/oopsla/nest-2.pwhile : 0.075s : [Success] 4·<1 + 2·(n) + n^2> + <1 + n>
 examples/oopsla/nest-2.pwhile : 0.082s : [Success] 4·[1 + 2·(n) + n^2 | 1 + n ≥ 0] + [1 + n | 1 + n ≥ 0]
processing ... examples/oopsla/nest-3.pwhile
 examples/oopsla/nest-3.pwhile : 60.00s : [Timeout]
processing ... examples/oopsla/queueing-network.pwhile
 examples/oopsla/queueing-network.pwhile : 28.18s : [Success] 2·<-1 + -n> + 4/125·<1 + n> + 3/250·<1 + 2·(n) + n^2>
processing ... examples/oopsla/trader-10.pwhile
 examples/oopsla/trader-10.pwhile : 0.045s : [Success] 10·<-min + min·price + -min^2 + price> + 5·<-2·(min·price) + min^2 + price^2>
 examples/oopsla/trader-10.pwhile : 0.044s : [Success] 10·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 5·[-2·(min·price) + min^2 + price^2 | -min
+ price ≥ 0]
processing ... examples/oopsla/trader-100.pwhile
 examples/oopsla/trader-100.pwhile : 0.044s : [Success] 100·<-min + min·price + -min^2 + price> + 50·<-2·(min·price) + min^2 + price^2>
 examples/oopsla/trader-100.pwhile : 0.046s : [Success] 100·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 50·[-2·(min·price) + min^2 + price^2 | -min
+ price ≥ 0]
processing ... examples/oopsla/trader-1000.pwhile
 examples/oopsla/trader-1000.pwhile : 0.063s : [Success] 1000·<-min + min·price + -min^2 + price> + 500·<-2·(min·price) + min^2 + price^2>
 examples/oopsla/trader-1000.pwhile : 0.066s : [Success] 1000·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 500·[-2·(min·price) + min^2 + price^2
| -min + price ≥ 0]
processing ... examples/oopsla/trader-10000.pwhile
 examples/oopsla/trader-10000.pwhile : 0.266s : [Success] 10000·<-min + min·price + -min^2 + price> + 5000·<-2·(min·price) + min^2 + price^2>
 examples/oopsla/trader-10000.pwhile : 0.282s : [Success] 10000·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 5000·[-2·(min·price) + min^2 + price^2
| -min + price ≥ 0]
processing ... examples/oopsla/trader-100000.pwhile
 examples/oopsla/trader-100000.pwhile : 3.982s : [Success] 100000·<-min + min·price + -min^2 + price> + 50000·<-2·(min·price) + min^2 + price^2>
 examples/oopsla/trader-100000.pwhile : 3.009s : [Success] 100000·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 50000·[-2·(min·price) + min^2 + price^2
| -min + price ≥ 0]
processing ... examples/oopsla/trader-1000000.pwhile
 examples/oopsla/trader-1000000.pwhile : 40.99s : [Success] 1000000·<-min + min·price + -min^2 + price> + 500000·<-2·(min·price) + min^2 + price^2>
 examples/oopsla/trader-1000000.pwhile : 21.60s : [Success] 1000000·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 500000·[-2·(min·price) + min^2 + price^2
| -min + price ≥ 0]
processing ... examples/oopsla/trader-50.pwhile
 examples/oopsla/trader-50.pwhile : 0.040s : [Success] 50·<-min + min·price + -min^2 + price> + 25·<-2·(min·price) + min^2 + price^2>
 examples/oopsla/trader-50.pwhile : 0.041s : [Success] 50·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 25·[-2·(min·price) + min^2 + price^2 | -min
+ price ≥ 0]
processing ... examples/oopsla/trader-500.pwhile
 examples/oopsla/trader-500.pwhile : 0.054s : [Success] 500·<-min + min·price + -min^2 + price> + 250·<-2·(min·price) + min^2 + price^2>
 examples/oopsla/trader-500.pwhile : 0.050s : [Success] 500·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 250·[-2·(min·price) + min^2 + price^2 | -min
+ price ≥ 0]
processing ... examples/oopsla/trader-5000.pwhile
 examples/oopsla/trader-5000.pwhile : 0.141s : [Success] 5000·<-min + min·price + -min^2 + price> + 2500·<-2·(min·price) + min^2 + price^2>
 examples/oopsla/trader-5000.pwhile : 0.138s : [Success] 5000·[-min + min·price + -min^2 + price | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 2500·[-2·(min·price) + min^2 + price^2
| -min + price ≥ 0]
processing ... examples/oopsla/trader-N.pwhile
 examples/oopsla/trader-N.pwhile : 3.345s : [Failed ]
 examples/oopsla/trader-N.pwhile : 3.002s : [Failed ]
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