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

synch

parent dcc8fb8c
......@@ -8,8 +8,8 @@ ENV PATH="$VIRTUAL_ENV/bin:$PATH"
# Build tool
#############
RUN mkdir /opt/slurf
WORKDIR /opt/slurf
RUN mkdir /opt/upmdps
WORKDIR /opt/upmdps
# Obtain
COPY . .
# Build
......
......@@ -24,8 +24,8 @@ def parser():
P.add_argument('--threshold', action="store", dest='threshold', default=0)
P.add_argument('--num_samples', action="store", dest='num_samples',
default=0)
P.add_argument('--num_iter', action="store", dest='num_iter', default=0)
P.add_argument('--comperator', action="store", dest='comperator',
P.add_argument('--num_iter', action="store", dest='num_iter', default=1)
P.add_argument('--comparator', action="store", dest='comparator',
default=0)
P.add_argument('--eta', action="store", dest='eta', default=0)
P.add_argument('--beta', action="store", dest='beta', default=0)
......@@ -74,11 +74,11 @@ def parse_settings():
eta = list(literal_eval(args.eta))
try:
comperator = literal_eval(args.comperator)
comparator = literal_eval(args.comparator)
except:
comperator = args.property
comparator = [args.comparator]
if any([c != "leq" and c != "geq" for c in comperator]):
if any([c != "leq" and c != "geq" for c in comparator]):
raise RuntimeError("Invalid direction type: should be 'leq' or 'geq'")
# Store arguments in dictionary
......@@ -93,7 +93,7 @@ def parse_settings():
'beta': beta,
#
'threshold': float(args.threshold),
'comperator': comperator,
'comparator': comparator,
#
'outfile': str(args.outfile),
'verbose': int(args.verbose),
......
......@@ -2,8 +2,8 @@
cd ..;
echo -e "++++++++ RUN BRP BENCHMARKS ++++++++\n";
### BRP (256,5)
python3 sampler.py --model brp/brp_256_5.pm --property brp/brp.prctl --threshold 0.5 --bisimulation weak --comperator '("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';
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 brp/brp_rewards4_16_5.pm --property brp/brp_rewards4.prctl --threshold 3 --bisimulation strong --comperator '("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';
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 brp/brp_rewards4_32_5.pm --property brp/brp_rewards4.prctl --threshold 3 --bisimulation weak --comperator '("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
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
......@@ -2,6 +2,6 @@
cd ..;
echo -e "++++++++ RUN CONSENSUS BENCHMARKS ++++++++\n";
### CONSENSUS (2,2)
python3 sampler.py --model consensus/coin2.pm --property consensus/coin2.prctl --threshold 0.25 --bisimulation strong --comperator '("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'
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 consensus/coin4.pm --property consensus/coin2.prctl --threshold 0.25 --bisimulation none --comperator '("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
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
......@@ -2,8 +2,8 @@
cd ..;
echo -e "++++++++ RUN CROWDS BENCHMARKS ++++++++\n";
### CROWDS (10,5)
python3 sampler.py --model crowds/crowds_10_5.pm --property crowds/crowds.prctl --threshold 0.9 --bisimulation weak --comperator '("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';
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 crowds/crowds_15_7.pm --property crowds/crowds.prctl --threshold 0.9 --bisimulation strong --comperator '("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';
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 crowds/crowds_20_7.pm --property crowds/crowds.prctl --threshold 0.9 --bisimulation strong --comperator '("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
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
......@@ -2,8 +2,8 @@
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 --comperator '("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';
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 --comperator '("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';
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 --comperator '("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
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
......@@ -2,6 +2,6 @@
cd ..;
echo -e "++++++++ RUN NAND BENCHMARKS ++++++++\n";
### NAND (10,5)
python3 sampler.py --model nand/nand_10_5.pm --property nand/nand.prctl --threshold 0.05 --bisimulation weak --comperator '("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';
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 nand/nand_25_5.pm --property nand/nand.prctl --threshold 0.05 --bisimulation strong --comperator '("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
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
......@@ -17,7 +17,8 @@ from core.storm_interface import load_problem, sample_results
from core.compute_bounds import compute_avg_beta, compute_avg_eta
if __name__ == '__main__':
np.random.seed(0)
# Parse arguments provided via the command line
Z = parse_settings()
......@@ -44,8 +45,8 @@ if __name__ == '__main__':
# For every number of samples
for n,N in enumerate(Z['Nsamples']):
# For every comperator
for c,C in enumerate(Z['comperator']):
# For every comparator
for c,C in enumerate(Z['comparator']):
# We perform as much iterations as possible, given sample size N
num_iter = int(np.floor(totalN / N))
......@@ -53,7 +54,7 @@ if __name__ == '__main__':
# For every iteration
for i in range(num_iter):
# Depending on comperator (leq/geq), compute nr of violations
# Depending on comparator (leq/geq), compute nr of violations
if C == "leq":
violated[i] = np.sum(sols[i*N:(i+1)*N] > Z['threshold'])
else:
......@@ -61,7 +62,7 @@ if __name__ == '__main__':
# Compute bounds on the confidence probability
if Z['eta'] != 0:
print('\nCOMPUTE BETA BASED ON ETA (comperator: '+str(C)+')')
print('\nCOMPUTE BETA BASED ON ETA (comparator: '+str(C)+')')
key = str(N)+'-'+str(C)
beta_results[key] = compute_avg_beta(violated, N, Z['eta'][c])
......@@ -71,7 +72,7 @@ if __name__ == '__main__':
# Compute bounds on the satisfaction probability
if Z['beta'] != 0:
print('\nCOMPUTE ETA BASED ON BETA (comperator: '+str(C)+')')
print('\nCOMPUTE ETA BASED ON BETA (comparator: '+str(C)+')')
for bet in Z['beta']:
print('\nCompute eta for beta='+str(bet))
......
......@@ -18,14 +18,14 @@ class PyTest(test):
setup(
name='sampverify-upMDP',
name='scenario-upMDPs',
version='0.1',
author='T. Badings, M. Cubuktepe',
author_email='thom.badings@ru.nl',
description='Scenario-Based Verification of Uncertain Parametric MDPs',
long_description=long_description,
long_description_content_type='text/markdown',
packages=['sampverify-upMDP'],
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