export LD_LIBRARY_PATH=../lib/

echo "Computing firewire BDD"
java -d64 -Xms400m -Xmx4G -jar ../prism_dectree.jar ../prism-examples/firewire/impl/firewire.nm ../prism-examples/firewire/impl/deadline.pctl -property 2 -const delay=50,deadline=300,fast=0.5 -dectree,bdd,onlyTarget,verify=1000,export=../output/csv/firewire_bdd > ../output/txt/firewire_bdd.txt
column -s "," -t < ../output/csv/firewire_bdd.csv | awk 'NR==1 {print $1,$2,$3,$4}; END{ print $1,$2,$3,$4 }'

echo "Computing investor BDD"
java -d64 -Xms400m -Xmx4G -jar ../prism_dectree.jar ../prism-examples/investor/investor_mdp.prism ../prism-examples/investor/investor.props -property 5 -const vmax=20,vinit=0 -dectree,bdd,onlyTarget,verify=1000,export=../output/csv/investor_bdd > ../output/txt/investor_bdd.txt
column -s "," -t < ../output/csv/investor_bdd.csv | awk 'NR==1 {print $1,$2,$3,$4}; END{ print $1,$2,$3,$4 }'

echo "Computing mer BDD"
java -d64 -Xms400m -Xmx4G -jar ../prism_dectree.jar ../prism-examples/mer/mer2_2_full.nm ../prism-examples/mer/mer.pctl -property 1 -const n=300,x=0.001 -dectree,bdd,onlyTarget,verify=1000,export=../output/csv/mer_bdd > ../output/txt/mer_bdd.txt
column -s "," -t < ../output/csv/mer_bdd.csv | awk 'NR==1 {print $1,$2,$3,$4}; END{ print $1,$2,$3,$4 }'

echo "Computing mer_big BDD"
java -d64 -Xms400m -Xmx4G -jar ../prism_dectree.jar ../prism-examples/mer/mer2_2_full.nm ../prism-examples/mer/mer.pctl -property 1 -const n=2147483646,x=0.001 -dectree,bdd,onlyTarget,verify=1000,export=../output/csv/mer_big_bdd > ../output/txt/mer_big_bdd.txt
column -s "," -t < ../output/csv/mer_big_bdd.csv | awk 'NR==1 {print $1,$2,$3,$4}; END{ print $1,$2,$3,$4 }'

echo "Computing zeroconf BDD"
java -d64 -Xms400m -Xmx4G -jar ../prism_dectree.jar ../prism-examples/zeroconf/zeroconf.nm ../prism-examples/zeroconf/zeroconf.pctl -property 2 -const reset=false,N=1000,K=2,err=0.1 -dectree,bdd,onlyTarget,verify=1000,export=../output/csv/zeroconf_bdd > ../output/txt/zeroconf_bdd.txt
column -s "," -t < ../output/csv/zeroconf_bdd.csv | awk 'NR==1 {print $1,$2,$3,$4}; END{ print $1,$2,$3,$4 }'
