#!/bin/bash

# Figure 3 (long-run low priority queue size)

prism -gs -maxiters 1000000 erlangen.prism -const l_init=1,delta2=0.0007,size1=40,size2=4,alpha=48,beta=0.01,mu2=1:10 erlangen.props -prop prog_queue_ss -const l=0:40 -exportresults stdout

# Figure 4 (long-run high priority queue size)

prism -gs -maxiters 1000000 erlangen.prism -const l_init=1,delta2=0.0007,size1=10,size2=10,alpha=48,beta=0.01,mu2=1:10 erlangen.props -prop user_queue_ss -const l=0:10 -exportresults stdout

# Figure 5 (long-run availability)

prism -gs -maxiters 1000000 erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1=10,size2=4,alpha=48,beta=0.01:0.005:0.05 erlangen.props -prop avail_ss -exportresults stdout
prism -gs -maxiters 1000000 erlangen.prism -const l_init=1,mu2=2,delta2=0.0014,size1=10,size2=4,alpha=48,beta=0.01:0.005:0.05 erlangen.props -prop avail_ss -exportresults stdout
prism -gs -maxiters 1000000 erlangen.prism -const l_init=1,mu2=2,delta2=0.0028,size1=10,size2=4,alpha=48,beta=0.01:0.005:0.05 erlangen.props -prop avail_ss -exportresults stdout
prism -gs -maxiters 1000000 erlangen.prism -const l_init=1,mu2=2,delta2=0.0056,size1=10,size2=4,alpha=48,beta=0.01:0.005:0.05 erlangen.props -prop avail_ss -exportresults stdout

# Figure 6 (long-run high throughput)

prism -gs -maxiters 1000000 erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1=10,size2=4,alpha=48,beta=0.01:0.005:0.05 erlangen.props -prop thru_hi_ss -exportresults stdout
prism -gs -maxiters 1000000 erlangen.prism -const l_init=1,mu2=2,delta2=0.0014,size1=10,size2=4,alpha=48,beta=0.01:0.005:0.05 erlangen.props -prop thru_hi_ss -exportresults stdout
prism -gs -maxiters 1000000 erlangen.prism -const l_init=1,mu2=2,delta2=0.0028,size1=10,size2=4,alpha=48,beta=0.01:0.005:0.05 erlangen.props -prop thru_hi_ss -exportresults stdout
prism -gs -maxiters 1000000 erlangen.prism -const l_init=1,mu2=2,delta2=0.0056,size1=10,size2=4,alpha=48,beta=0.01:0.005:0.05 erlangen.props -prop thru_hi_ss -exportresults stdout

# Figure 7 (point availability)

prism -nossdetect erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1=10,size2=4,alpha=48,beta=0.01 erlangen.props -prop avail_tr -const T=100:100:1500 -exportresults stdout
prism -nossdetect erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1=10,size2=4,alpha=48,beta=0.025 erlangen.props -prop avail_tr -const T=100:100:1500 -exportresults stdout
prism -nossdetect erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1=10,size2=4,alpha=48,beta=0.05 erlangen.props -prop avail_tr -const T=100:100:1500 -exportresults stdout

# Figure 8 (point high throughput)

prism -nossdetect erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1=10,size2=4,alpha=48,beta=0.01 erlangen.props -prop thru_hi_tr -const T=100:100:1500 -exportresults stdout
prism -nossdetect erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1=10,size2=4,alpha=48,beta=0.025 erlangen.props -prop thru_hi_tr -const T=100:100:1500 -exportresults stdout
prism -nossdetect erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1=10,size2=4,alpha=48,beta=0.05 erlangen.props -prop thru_hi_tr -const T=100:100:1500 -exportresults stdout

# Figure 9 (point availability for varying initial phase)

prism -nossdetect erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1=10,size2=4,alpha=48,beta=0.01 erlangen.props -prop avail_tr -const T=100:100:1500 -exportresults stdout
prism -nossdetect erlangen.prism -const l_init=1,mu2=2,delta2=0.0007,size1=4,size2=4,alpha=48,beta=0.01 erlangen.props -prop avail_tr -const T=100:100:1500 -exportresults stdout