Commit 15efff2b authored by Thom Badings's avatar Thom Badings
Browse files

Synch before submitting

parent 31a3707d
......@@ -58,16 +58,16 @@ python3 samplingprism.py --model-file consensus/coin4.pm --property-file consens
### DRONE
## Uniform
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction geq --num_samples 1000 --num_iter 5 --weather "uniform" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.90 --bisimulation none --direction geq --num_samples 1000 --num_iter 5 --weather "uniform" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction leq --num_samples 1000 --num_iter 5 --weather "uniform" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.90 --bisimulation none --direction leq --num_samples 1000 --num_iter 5 --weather "uniform" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
## Wind in positive y direction
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction geq --num_samples 1000 --num_iter 5 --weather "y-pos-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.90 --bisimulation none --direction geq --num_samples 1000 --num_iter 5 --weather "y-pos-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction leq --num_samples 1000 --num_iter 5 --weather "y-pos-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.90 --bisimulation none --direction leq --num_samples 1000 --num_iter 5 --weather "y-pos-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
## Wind in negative x direction
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction geq --num_samples 1000 --num_iter 5 --weather "x-neg-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.90 --bisimulation none --direction geq --num_samples 1000 --num_iter 5 --weather "x-neg-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.95 --bisimulation none --direction leq --num_samples 1000 --num_iter 5 --weather "x-neg-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
python3 samplingprism_drone_scenario.py --model-file drone/drone_par_param_effect_example.nm --property-file drone/drone_par.prctl --threshold 0.90 --bisimulation none --direction leq --num_samples 1000 --num_iter 5 --weather "x-neg-bias" --eta 0.90 --beta '(0.9,0.99,0.999,0.9999)'
This diff is collapsed.
This diff is collapsed.
(stormpyenv-upt) mcubuktepe@asg-a32265:~/research/codes/gurobi_parallel/sampler$ python3 samplingprism.py --model-file brp_rewards4.pm --property-file brp_rewards4.pctl --threshold 5.5 --bisimulation strong --direction leq --num_samples 2000 --num_iter 5 --violation_prob 0.4
brp_rewards4.pm
Building model from brp_rewards4.pm
R=? [ F ((s=5) | (s=0&srep=3)) ]
Model supports parameters: True
Number of states before bisim: 1240
Number of params before bisim: 2
Number of states after bisim: 730
Number of params after bisim: 4
40%|██████████████████ | 2/5 [00:01<00:01, 1.50it/s]Average violation so far: 0.3845
60%|███████████████████████████ | 3/5 [00:01<00:01, 1.50it/s]Average violation so far: 0.3821666666666667
80%|████████████████████████████████████ | 4/5 [00:02<00:00, 1.51it/s]Average violation so far: 0.3775
100%|█████████████████████████████████████████████| 5/5 [00:03<00:00, 1.51it/s]
Solver time :3.324021339416504
printing specification violation array
[0.3815, 0.3875, 0.3775, 0.3635, 0.377]
probability of violating the spec less then the threshold for each iter:
[0.95651784 0.87776984 0.98108913 0.99960289 0.98309896]
average value of the array:
0.959615732813661
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