Commit cc38993c authored by Thom Badings's avatar Thom Badings
Browse files

changed experiments files

parent 649da580
#!/bin/bash
cd ..;
# To speed up experiments, you can lower the number of samples N and iterations i below:
N_full='(1000,2500,5000,10000,25000)'
N_most='(1000,2500,5000,10000)'
......@@ -10,9 +9,9 @@ ii=5
#
echo -e "++++++++ RUN BRP BENCHMARKS ++++++++\n";
### BRP (256,5)
python3 sampler.py --model models/brp/brp_256_5.pm --property models/brp/brp.prctl --threshold 0.5 --bisimulation weak --comparator '("leq","geq")' --num_samples $N_full--num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.055,0.898)' --outfile 'brp_256_5_output';
python3 sampler.py --model models/brp/brp_256_5.pm --property models/brp/brp.prctl --threshold 0.5 --bisimulation weak --comparator '("leq","geq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.055,0.898)' --outfile 'brp_256_5_output';
### BRP (16,5)
python3 sampler.py --model models/brp/brp_rewards4_16_5.pm --property models/brp/brp_rewards4.prctl --threshold 3 --bisimulation strong --comparator '("leq","geq")' --num_samples $N_full--num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.275,0.676)' --outfile 'brp_16-5_output';
python3 sampler.py --model models/brp/brp_rewards4_16_5.pm --property models/brp/brp_rewards4.prctl --threshold 3 --bisimulation strong --comparator '("leq","geq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.275,0.676)' --outfile 'brp_16-5_output';
### BRP (32,5)
python3 sampler.py --model models/brp/brp_rewards4_32_5.pm --property models/brp/brp_rewards4.prctl --threshold 3 --bisimulation weak --comparator '("leq","geq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.232,0.718)' --outfile 'brp_32-5_output';
#
......@@ -22,13 +21,11 @@ echo -e "++++++++ RUN CROWDS BENCHMARKS ++++++++\n";
python3 sampler.py --model models/crowds/crowds_10_5.pm --property models/crowds/crowds.prctl --threshold 0.9 --bisimulation weak --comparator '("leq","geq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.537,0.413)' --outfile 'crowds_10-5_output';
### CROWDS (15,7)
python3 sampler.py --model models/crowds/crowds_15_7.pm --property models/crowds/crowds.prctl --threshold 0.9 --bisimulation strong --comparator '("leq","geq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.411,0.539)' --outfile 'crowds_15-7_output';
### CROWDS (20,7)
python3 sampler.py --model models/crowds/crowds_20_7.pm --property models/crowds/crowds.prctl --threshold 0.9 --bisimulation strong --comparator '("leq","geq")' --num_samples $N_full--num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.416,0.534)' --outfile 'crowds_20-7_output';
#
#
echo -e "++++++++ RUN CONSENSUS BENCHMARKS ++++++++\n";
### CONSENSUS (2,2)
python3 sampler.py --model models/consensus/coin2.pm --property models/consensus/coin2.prctl --threshold 0.25 --bisimulation strong --comparator '("geq","leq")' --num_samples $N_full--num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.280,0.669)' --outfile 'consensus_2-2_output'
python3 sampler.py --model models/consensus/coin2.pm --property models/consensus/coin2.prctl --threshold 0.25 --bisimulation strong --comparator '("geq","leq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.280,0.669)' --outfile 'consensus_2-2_output';
### CONSENSUS (4,2)
python3 sampler.py --model models/consensus/coin4.pm --property models/consensus/coin2.prctl --threshold 0.25 --bisimulation none --comparator '("geq","leq")' --num_samples $N_most --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.063,0.888)' --outfile 'consensus_4-2_output';
#
......
#!/bin/bash
# To speed up experiments, you can lower the number of samples N and iterations i below:
N_full='(1000,2500,5000)'
N_most='(1000,2500,5000)'
N_drone=1000
i=5
ii=3
#
#
echo -e "++++++++ RUN BRP BENCHMARKS ++++++++\n";
### BRP (256,5)
python3 sampler.py --model models/brp/brp_256_5.pm --property models/brp/brp.prctl --threshold 0.5 --bisimulation weak --comparator '("leq","geq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.055,0.898)' --outfile 'brp_256_5_output';
### BRP (16,5)
python3 sampler.py --model models/brp/brp_rewards4_16_5.pm --property models/brp/brp_rewards4.prctl --threshold 3 --bisimulation strong --comparator '("leq","geq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.275,0.676)' --outfile 'brp_16-5_output';
### BRP (32,5)
python3 sampler.py --model models/brp/brp_rewards4_32_5.pm --property models/brp/brp_rewards4.prctl --threshold 3 --bisimulation weak --comparator '("leq","geq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.232,0.718)' --outfile 'brp_32-5_output';
#
#
echo -e "++++++++ RUN CROWDS BENCHMARKS ++++++++\n";
### CROWDS (10,5)
python3 sampler.py --model models/crowds/crowds_10_5.pm --property models/crowds/crowds.prctl --threshold 0.9 --bisimulation weak --comparator '("leq","geq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.537,0.413)' --outfile 'crowds_10-5_output';
### CROWDS (15,7)
python3 sampler.py --model models/crowds/crowds_15_7.pm --property models/crowds/crowds.prctl --threshold 0.9 --bisimulation strong --comparator '("leq","geq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.411,0.539)' --outfile 'crowds_15-7_output';
#
#
echo -e "++++++++ RUN CONSENSUS BENCHMARKS ++++++++\n";
### CONSENSUS (2,2)
python3 sampler.py --model models/consensus/coin2.pm --property models/consensus/coin2.prctl --threshold 0.25 --bisimulation strong --comparator '("geq","leq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.280,0.669)' --outfile 'consensus_2-2_output';
### CONSENSUS (4,2)
python3 sampler.py --model models/consensus/coin4.pm --property models/consensus/coin2.prctl --threshold 0.25 --bisimulation none --comparator '("geq","leq")' --num_samples $N_most --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.063,0.888)' --outfile 'consensus_4-2_output';
#
#
echo -e "++++++++ RUN DRONE BENCHMARKS ++++++++\n";
## Uniform
python3 sampler.py --model models/drone/drone_model.nm --property models/drone/drone_spec.prctl --threshold 0.90 --bisimulation none --comparator '("geq","leq")' --num_samples $N_drone --num_iter $i --weather "uniform" --eta '(0.90,0.10)' --beta '(0.9,0.99,0.999,0.9999)' --outfile 'drone_uniform_output';
## Wind in positive y direction
python3 sampler.py --model models/drone/drone_model.nm --property models/drone/drone_spec.prctl --threshold 0.90 --bisimulation none --comparator '("geq","leq")' --num_samples $N_drone --num_iter $i --weather "y-pos-bias" --eta '(0.90,0.10)' --beta '(0.9,0.99,0.999,0.9999)' --outfile 'drone_yposbias_output';
## Wind in negative x direction
python3 sampler.py --model models/drone/drone_model.nm --property models/drone/drone_spec.prctl --threshold 0.90 --bisimulation none --comparator '("geq","leq")' --num_samples $N_drone --num_iter $i --weather "x-neg-bias" --eta '(0.90,0.10)' --beta '(0.9,0.99,0.999,0.9999)' --outfile 'drone_xnegbias_output';
#
#
### NAND (10,5)
python3 sampler.py --model models/nand/nand_10_5.pm --property models/nand/nand.prctl --threshold 0.05 --bisimulation weak --comparator '("geq","leq")' --num_samples $N_full --num_iter $i --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.218,0.733)' --outfile 'nand_10-5_output';
### NAND (25,5)
python3 sampler.py --model models/nand/nand_25_5.pm --property models/nand/nand.prctl --threshold 0.05 --bisimulation strong --comparator '("geq","leq")' --num_samples $N_most --num_iter $ii --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.206,0.744)' --outfile 'nand_25-5_output';
\ No newline at end of file
......@@ -84,16 +84,16 @@ if __name__ == '__main__':
str(bet)+' is eta='+str(eta_results[key][N])]
# Write logfile
f = open('output/'+Z['outfile']+'.txt', "w")
f = open('data/'+Z['outfile']+'.txt', "w")
f.writelines(buffer)
f.close()
# Export results for the confidence probability (if a sat.prob. was fixed)
if Z['eta'] != 0:
beta_results.to_csv('output/'+Z['outfile']+'_confprob.csv', sep=';')
beta_results.to_csv('data/'+Z['outfile']+'_confprob.csv', sep=';')
# Export results for the sat.prob. (if a confidence probability was fixed)
if Z['beta'] != 0:
eta_results.to_csv('output/'+Z['outfile']+'_satprob.csv', sep=';')
eta_results.to_csv('data/'+Z['outfile']+'_satprob.csv', sep=';')
print('\n---------------------\n')
\ No newline at end of file
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