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

cleaned experiment files

parent 34bebe32
# Use Storm 1.6.4 docker container
FROM movesrwth/storm:1.6.4
# Use Stormpy 1.6.4 docker container
FROM movesrwth/stormpy:1.6.4
# Activate virtual environment
############################
ENV VIRTUAL_ENV=/opt/venv
ENV PATH="$VIRTUAL_ENV/bin:$PATH"
# Build tool
#############
RUN mkdir /opt/upmdps
......@@ -13,5 +15,5 @@ WORKDIR /opt/upmdps
# Obtain
COPY . .
# Build
RUN pip install --no-cache-dir -r requirements.txt
RUN python setup.py develop
RUN pip3 install --no-cache-dir -r requirements.txt
RUN python3 setup.py develop
OUTPUT FOR MODEL: models/brp/brp_256_5.pm
Run time in Storm per 1000 samples: 1.931
- Confidence probability for eta=0 is beta=1.0
- Lower bound sat.prob. for beta=0.999 is eta=0.0668
\ No newline at end of file
;Confidence probability (beta)
10000-leq;1.0
;0.999-leq
10000;0.0668
......@@ -20,7 +20,7 @@ def parser():
# isn't given
P.add_argument('--model', action="store", dest='model', default=0)
P.add_argument('--property', action="store", dest='property', default=0)
P.add_argument('--bisimulation', action="store", dest='bisim', default=0)
P.add_argument('--bisimulation', action="store", dest='bisim', default='strong')
P.add_argument('--threshold', action="store", dest='threshold', default=0)
P.add_argument('--num_samples', action="store", dest='num_samples',
default=0)
......@@ -30,8 +30,7 @@ def parser():
P.add_argument('--eta', action="store", dest='eta', default=0)
P.add_argument('--beta', action="store", dest='beta', default=0)
P.add_argument('--outfile', action="store", dest='outfile',
default='output.txt')
P.add_argument('--verbose', action="store", dest='verbose', default=0)
default='output')
# Weather conditions for drone
P.add_argument('--weather', action="store", dest='weather', default=0)
......@@ -96,7 +95,6 @@ def parse_settings():
'comparator': comparator,
#
'outfile': str(args.outfile),
'verbose': int(args.verbose),
#
'weather': args.weather
}
......
......@@ -101,7 +101,7 @@ def load_problem(model_file, property_file, bisimulation_type):
return parameters,model,properties
def sample_results(N, parameters, model, properties, model_file, verbose,
def sample_results(N, parameters, model, properties, model_file,
weather=None):
'''
Sample results for instantiated MDPs from Storm.
......@@ -113,7 +113,6 @@ def sample_results(N, parameters, model, properties, model_file, verbose,
model : Model object
properties : Parsed properties in Storm
model_file : String of the model file that is loaded
verbose : If true, more outputs are provided
weather : Weather conditions (optional; only used for drone benchmark)
Returns
......
#!/bin/bash
# Run all benchmarks at once
bash run_all_brp.sh;
bash run_all_crowds.sh;
bash run_all_consensus.sh;
bash run_all_drone.sh;
bash run_all_nand.sh;
\ No newline at end of file
#!/bin/bash
cd ..;
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 '(1000,2500,5000,10000,25000)' --num_iter 10 --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 '(1000,2500,5000,10000,25000)' --num_iter 10 --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 '(1000,2500,5000,10000,25000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.232,0.718)' --outfile 'brp_32-5_output';
\ No newline at end of file
#!/bin/bash
cd ..;
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 '(1000,2500,5000,10000,25000)' --num_iter 10 --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 '(1000,2500,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.063,0.888)' --outfile 'consensus_4-2_output';
\ No newline at end of file
#!/bin/bash
cd ..;
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 '(1000,2500,5000,10000,25000)' --num_iter 10 --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 '(1000,2500,5000,10000,25000)' --num_iter 10 --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 '(1000,2500,5000,10000,25000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta '(0.416,0.534)' --outfile 'crowds_20-7_output' --verbose 1;
\ No newline at end of file
#!/bin/bash
cd ..;
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 5000 --num_iter 10 --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 5000 --num_iter 10 --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 5000 --num_iter 10 --weather "x-neg-bias" --eta '(0.90,0.10)' --beta '(0.9,0.99,0.999,0.9999)' --outfile 'drone_xnegbias_output';
\ No newline at end of file
#!/bin/bash
cd ..;
echo -e "++++++++ RUN NAND BENCHMARKS ++++++++\n";
### 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 '(1000,2500,5000,10000,25000)' --num_iter 10 --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 '(1000,2500,5000,10000)' --num_iter 5 --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
......@@ -4,4 +4,4 @@ numpy==1.21.4
setuptools==58.0.4
tqdm==4.62.3
scipy==1.8.0
stormpy>=1.6.4
\ No newline at end of file
stormpy==1.6.4
#!/bin/bash
# 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)'
N_drone=5000
i=10
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';
### 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';
### 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'
### 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
......@@ -35,7 +35,7 @@ if __name__ == '__main__':
# Sample solutions (using Storm) and save the results plus run time
ticDiff()
sols = sample_results(totalN, parameters, model, properties,
Z['model'], Z['verbose'], Z['weather'])
Z['model'], Z['weather'])
time = np.round(tocDiff(False) / totalN * 1000, 3)
buffer += ['\n','Run time in Storm per 1000 samples: '+str(time),'\n']
......
......@@ -25,7 +25,6 @@ setup(
description='Scenario-Based Verification of Uncertain Parametric MDPs',
long_description=long_description,
long_description_content_type='text/markdown',
packages=['scenario-upMDPs'],
cmdclass={
'test': PyTest
},
......
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