Skip to content

GitLab

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

new experiments

parent 13d6ab12
Hide whitespace changes
Inline Side-by-side
examples/oopsla/trader-N.pwhile deleted 100644 → 0
View file @ 13d6ab12
# Variation of linear/trader.imp
def trader():
var price, min, nShares, maxShares
while price > min and min >= 0:
prob (1,3):
price = price + 1
else:
price = price - 1
nShares = rand(maxShares)
while nShares > 0:
nShares = nShares - 1
tick price
examples/results
View file @ ac8b34ea
This source diff could not be displayed because it is too large. You can view the blob instead.
examples/results.txt
View file @ ac8b34ea
processing ... examples/oopsla/NCH-18/linear/2drwalk.imp
 examples/oopsla/NCH-18/linear/2drwalk.imp : 0.033s : [Success] 2·[1 + -d + n | 1 + -d + n ≥ 0]
 examples/oopsla/NCH-18/linear/2drwalk.imp : 0.026s : [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]
 examples/oopsla/NCH-18/linear/C4B_t09.imp : 0.006s : [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.167s : [Failed ]
 examples/oopsla/NCH-18/linear/C4B_t15.imp : 0.152s : [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]
 examples/oopsla/NCH-18/linear/C4B_t15_2.imp : 0.006s : [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.012s : [Failed ]
 examples/oopsla/NCH-18/linear/C4B_t30.imp : 0.010s : [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])
 examples/oopsla/NCH-18/linear/C4B_t30_2.imp : 0.003s : [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
 examples/oopsla/NCH-18/linear/C4B_t61.imp : 0.004s : [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.007s : [Success] 1024/1023·[n | n ≥ 0]
 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]
 examples/oopsla/NCH-18/linear/cooling.pwhile : 0.015s : [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
......@@ -35,118 +35,106 @@ processing ... examples/oopsla/NCH-18/linear/cowboy_duel_3way.pwhile
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]
 examples/oopsla/NCH-18/linear/filling_vol.pwhile: 0.006s : [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.001s : [Success] 145/28·[-1 + n + -x | -1 + n + -x ≥ 0]
 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.003s : [Success] [-1 + x | -1 + x ≥ 0]
 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]
 examples/oopsla/NCH-18/linear/prdwalk.pwhile : 0.002s : [Success] 8/3·[n + -x | n + -x ≥ 0]
processing ... examples/oopsla/NCH-18/linear/prnes.pwhile
 examples/oopsla/NCH-18/linear/prnes.pwhile : 0.157s : [Success] [y ≥ 0] · (50/9·[99·(n) + -n·y | -99 + y ≥ 0 ∧ -n ≥ 0] + 250000/81·[n^2 | -n ≥ 0])
 examples/oopsla/NCH-18/linear/prnes.pwhile : 0.126s : [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.pwhile
 examples/oopsla/NCH-18/linear/prseq.pwhile : 0.011s : [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])
 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.017s : [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])
 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.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]
 examples/oopsla/NCH-18/linear/prspeed.imp : 0.013s : [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.013s : [Success] 11/6·[3 + -h + t | 3 + -h + t ≥ 0]
 examples/oopsla/NCH-18/linear/race.pwhile : 0.010s : [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.008s : [Success] [y ≥ 0] · (9/4·[x | x ≥ 0] + [y | y ≥ 0])
 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]
 examples/oopsla/NCH-18/linear/rdspeed.pwhile : 0.012s : [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.003s : [Success] 2·[n | n ≥ 0]
 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]
 examples/oopsla/NCH-18/linear/robot.imp : 0.006s : [Success] 5/4·[n | n ≥ 0]
processing ... examples/oopsla/NCH-18/linear/roulette.pwhile
 examples/oopsla/NCH-18/linear/roulette.pwhile : 0.032s : [Success] 74/15·[10011 + -n | 10011 + -n ≥ 0]
 examples/oopsla/NCH-18/linear/roulette.pwhile : 0.049s : [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.003s : [Success] 15/2·[n | n ≥ 0]
 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.031s : [Success] [M ≥ 0 ∧ y ≥ 0] · ([w | w ≥ 0] + 18·[M·N + N | 3 + 3·(M) ≥ 0 ∧ N ≥ 0] + 3·[y | y ≥ 0])
 examples/oopsla/NCH-18/polynomial/complex.pwhile: 0.029s : [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]
 examples/oopsla/NCH-18/polynomial/multirace.pwhi: 0.013s : [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.012s : [Success] 15/2·[x | x ≥ 0] + 9/2·[x^2 | x ≥ 0]
 examples/oopsla/NCH-18/polynomial/pol04.imp : 0.007s : [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.012s : [Success] 3/4·[x | x ≥ 0] + 3/2·[x^2 | x ≥ 0]
 examples/oopsla/NCH-18/polynomial/pol05.pwhile : 0.007s : [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.043s : [Success] [1 + minPrice + minPrice·sPrice + sPrice | 1 + minPrice ≥ 0 ∧ 1 + sPrice ≥ 0] + [-minPrice + -minPrice·sPrice + sPrice
+ sPrice^2 | 1 + sPrice ≥ 0 ∧
-minPrice + sPrice ≥ 0]
 examples/oopsla/NCH-18/polynomial/pol06.pwhile : 0.040s : [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.014s : [Success] 3/2·[1 + -2·(n) + n^2 | -1 + n ≥ 0]
 examples/oopsla/NCH-18/polynomial/pol07.imp : 0.015s : [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]
 examples/oopsla/NCH-18/polynomial/rdbub.pwhile : 0.006s : [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]
 examples/oopsla/NCH-18/polynomial/simple_game.im: 0.006s : [Success] 2·[1 + x | 1 + x ≥ 0]
processing ... examples/oopsla/NCH-18/polynomial/trader.pwhile
 examples/oopsla/NCH-18/polynomial/trader.pwhile : 0.112s : [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]
 examples/oopsla/NCH-18/polynomial/trader.pwhile : 0.030s : [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.pwhile
 examples/oopsla/WFGCQS-19/2drobot.pwhile : 60.00s : [Timeout]
 examples/oopsla/WFGCQS-19/2drobot.pwhile : 1.760s : [Success] 1/2·[a + -2·(a·b) + a^2 + -b + b^2 | 1 + a + -b ≥ 0 ∧ a + -b ≥ 0] + 2·[1 + 2·(a) + -2·(a·b) + a^2 + -2·(b) + b^2 | 1 + a + -b ≥ 0] + 1267/18·[6 + a + -b | 6 + a + -b ≥ 0]
processing ... examples/oopsla/WFGCQS-19/queueing-network.pwhile
 examples/oopsla/WFGCQS-19/queueing-network.pwhil: 30.02s : [Success] 4/125·[1 + n | 1 + n ≥ 0] + 3/250·[1 + 2·(n) + n^2 | 1 + n ≥ 0]
 examples/oopsla/WFGCQS-19/queueing-network.pwhil: 2.215s : [Success] 1132981/7411500·[1 + n | 1 + n ≥ 0] + 125/243 + 125/244
processing ... examples/oopsla/bridge.imp
 examples/oopsla/bridge.imp : 0.010s : [Success] [-a·b + a·x + b·x + -x^2 | -a + x ≥ 0 ∧ b + -x ≥ 0]
 examples/oopsla/bridge.imp : 0.005s : [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.029s : [Success] 110
 examples/oopsla/coupons-10.imp : 0.015s : [Success] 110
processing ... examples/oopsla/coupons-100.imp
 examples/oopsla/coupons-100.imp : 1.338s : [Success] 10100
 examples/oopsla/coupons-100.imp : 1.141s : [Success] 10100
processing ... examples/oopsla/coupons-50.imp
 examples/oopsla/coupons-50.imp : 0.345s : [Success] 2550
 examples/oopsla/coupons-50.imp : 0.304s : [Success] 2550
processing ... examples/oopsla/coupons-N.pwhile
 examples/oopsla/coupons-N.pwhile : 0.198s : [Success] 1/2 + [N | N ≥ 0] + 1/2·[N^2 | N ≥ 0]
 examples/oopsla/coupons-N.pwhile : 0.111s : [Success] 1/2 + [N | N ≥ 0] + 1/2·[N^2 | N ≥ 0]
processing ... examples/oopsla/nest-2.pwhile
 examples/oopsla/nest-2.pwhile : 0.021s : [Success] 16·[n·x1 | n ≥ 0 ∧ x1 ≥ 0] + 4·[x1 | x1 ≥ 0]
 examples/oopsla/nest-2.pwhile : 0.019s : [Success] 16·[n^2 | n ≥ 0] + 4·[n | n ≥ 0]
processing ... examples/oopsla/nest-3.pwhile
 examples/oopsla/nest-3.pwhile : 0.095s : [Success] 2·[2 + x1 | 2 + x1 ≥ 0] + 16·[n·x1 | n ≥ 0 ∧ x1 ≥ 0] + 64·[n^2·x1 | n ≥ 0 ∧ x1 ≥ 0]
 examples/oopsla/nest-3.pwhile : 0.068s : [Success] 2·[2 + n | 2 + n ≥ 0] + 16·[n^2 | n ≥ 0] + 64·[n^3 | n ≥ 0]
processing ... examples/oopsla/nest-4.pwhile
 examples/oopsla/nest-4.pwhile : 0.695s : [Success] 144·[2·(n·x1) + n^2·x1 | 2 + n ≥ 0 ∧ n ≥ 0 ∧ x1 ≥ 0] + 10·[2 + x1 | 2 + x1 ≥ 0] + 256·[n^3·x1 | n ≥ 0 ∧ x1 ≥ 0]
 examples/oopsla/nest-4.pwhile : 0.554s : [Success] 144·[2·(n^2) + n^3 | 2 + n ≥ 0 ∧ n ≥ 0] + 10·[2 + n | 2 + n ≥ 0] + 256·[n^4 | n ≥ 0]
processing ... examples/oopsla/prseq-2.pwhile
 examples/oopsla/prseq-2.pwhile : 0.011s : [Success] [y ≥ 10] · (3·[x + -y | x + -y ≥ 0] + 3·[x + -y | x + -y ≥ 0] + 3/2·[y | y ≥ 0])
 examples/oopsla/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/prspeed-2.imp
 examples/oopsla/prspeed-2.imp : 0.014s : [Success] 4/3·[1 + n + -x | 1 + n + -x ≥ 0] + 2·[m + -y | m + -y ≥ 0]
 examples/oopsla/prspeed-2.imp : 0.012s : [Success] 4/3·[1 + n + -x | 1 + n + -x ≥ 0] + 2·[m + -y | m + -y ≥ 0]
processing ... examples/oopsla/trader-10.pwhile
 examples/oopsla/trader-10.pwhile : 0.045s : [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]
 examples/oopsla/trader-10.pwhile : 0.025s : [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.048s : [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]
 examples/oopsla/trader-100.pwhile : 0.027s : [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.069s : [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]
 examples/oopsla/trader-1000.pwhile : 0.039s : [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.270s : [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]
 examples/oopsla/trader-10000.pwhile : 0.163s : [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.146s : [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]
 examples/oopsla/trader-100000.pwhile : 2.113s : [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 : 35.01s : [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]
 examples/oopsla/trader-1000000.pwhile : 21.81s : [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.044s : [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]
 examples/oopsla/trader-50.pwhile : 0.026s : [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 | 1 + min ≥ 0 ∧ -min + price ≥ 0] + 250·[-2·(min·price) + min^2 + price^2 | -min
+ price ≥ 0]
 examples/oopsla/trader-500.pwhile : 0.031s : [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.142s : [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]
 examples/oopsla/trader-5000.pwhile : 0.086s : [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 : 11.90s : [Failed ]
 examples/oopsla/trader-N.pwhile : 10.63s : [Failed ]
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