Commit 1718c6a1 authored by Thom Badings's avatar Thom Badings
Browse files

backup before cleaning the repo

parent 213c0da2
# Byte-compiled / optimized / DLL files
__pycache__/
*.py[cod]
*$py.class
# C extensions
*.so
# Output folder
output/*
!output/.keep
# Output folder
experiments/results/*
!experiments/results/.keep
# Cache folder
cache/*
!cache/.keep
# Tarball (e.g. docker container)
*.tar
# Distribution / packaging
.Python
build/
develop-eggs/
dist/
downloads/
eggs/
.eggs/
lib/
lib64/
parts/
sdist/
var/
wheels/
share/python-wheels/
*.egg-info/
.installed.cfg
*.egg
MANIFEST
# PyInstaller
# Usually these files are written by a python script from a template
# before PyInstaller builds the exe, so as to inject date/other infos into it.
*.manifest
*.spec
# Installer logs
pip-log.txt
pip-delete-this-directory.txt
# Unit test / coverage reports
htmlcov/
.tox/
.nox/
.coverage
.coverage.*
.cache
nosetests.xml
coverage.xml
*.cover
*.py,cover
.hypothesis/
.pytest_cache/
cover/
# Translations
*.mo
*.pot
# Django stuff:
*.log
local_settings.py
db.sqlite3
db.sqlite3-journal
# Flask stuff:
instance/
.webassets-cache
# Scrapy stuff:
.scrapy
# Sphinx documentation
docs/_build/
# PyBuilder
.pybuilder/
target/
# Jupyter Notebook
.ipynb_checkpoints
# IPython
profile_default/
ipython_config.py
# pyenv
# For a library or package, you might want to ignore these files since the code is
# intended to run in multiple environments; otherwise, check them in:
# .python-version
# pipenv
# According to pypa/pipenv#598, it is recommended to include Pipfile.lock in version control.
# However, in case of collaboration, if having platform-specific dependencies or dependencies
# having no cross-platform support, pipenv may install dependencies that don't work, or not
# install all needed dependencies.
#Pipfile.lock
# PEP 582; used by e.g. github.com/David-OConnor/pyflow
__pypackages__/
# Celery stuff
celerybeat-schedule
celerybeat.pid
# SageMath parsed files
*.sage.py
# Environments
.env
.venv
env/
venv/
ENV/
env.bak/
venv.bak/
# Spyder project settings
.spyderproject
.spyproject
# Rope project settings
.ropeproject
# mkdocs documentation
/site
# mypy
.mypy_cache/
.dmypy.json
dmypy.json
# Pyre type checker
.pyre/
# pytype static type analyzer
.pytype/
# Cython debug symbols
cython_debug/
# PyCharm
.idea/
# Tmp file for CTMC extraction from DFT
tmp_ctmc.drn
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
File mode changed from 100755 to 100644
import numpy as np
import pandas as pd
from functions import ticDiff, tocDiff
from parser import parser, parse_settings
from storm_interface import load_problem, sample_results
from compute_bounds import compute_avg_beta, compute_avg_beta_sttt, \
compute_avg_eta_sttt
args = parser()
Z = parse_settings(args)
# Create buffer for output file
buffer = ['OUTPUT FOR MODEL: '+str(Z['model']),'\n']
# Load problem
parameters,model,properties=load_problem(Z['model'],
Z['property'],
Z['bisim'])
totalN = Z['iterations'] * max(Z['Nsamples'])
ticDiff()
# Sample solutions
solutions = sample_results(totalN, parameters, model, properties,
Z['model'], Z['verbose'])
storm_time = np.round(tocDiff(False) / totalN * 1000, 3)
buffer += ['\n','Run time in Storm per 1000 samples: '+str(storm_time),'\n']
beta_results = pd.Series()
eta_columns = [str(beta)+'-'+str(c) for beta in Z['beta']
for c in Z['comperator']]
eta_index = Z['Nsamples']
eta_results = pd.DataFrame(0, index=eta_index, columns=eta_columns)
# For every number of samples
for n,N in enumerate(Z['Nsamples']):
# For every comperator
for c,thres in zip(Z['comperator'], Z['threshold']):
if c != "leq" and c != "geq":
raise RuntimeError("Invalid direction type, direction type should be 'leq' or 'geq'")
num_iter = np.floor(totalN / N)
violated = np.zerso(num_iter)
# For every iteration
for i in range(num_iter):
start_idx = i * N
end_idx = start_idx + N
if c == "leq":
violated[i] = np.sum( solutions[start_idx:end_idx] > thres )
else:
violated[i] = np.sum( solutions[start_idx:end_idx] < thres )
# Compute bounds
if Z['eta'] != 0:
print('\nCOMPUTE BETA BASED ON ETA...')
print('\n------------\nNEW THEOREM:')
key = str(N)+'-'+str(c)
beta_results[key] = np.round(compute_avg_beta_sttt(violated, N, Z['eta']), 5)
buffer += ['\nConfidence probability for eta='+str(Z['eta'])+' is beta='+str(beta_results[key])]
if Z['beta'] != 0:
print('\nCOMPUTE ETA BASED ON BETA...')
print('\n------------\nNEW THEOREM:')
for i,bet in enumerate(Z['beta']):
print('\nCompute eta for beta='+str(bet))
key = str(bet)+'-'+str(c)
eta_results[key][N] = np.round(compute_avg_eta_sttt(violated, N, bet), 5)
buffer += ['\nLower bound sat.prob. for beta='+str(bet)+' is eta='+str(eta_star[n,i])]
beta_star = np.zeros(len(num_samples))
eta_star = np.zeros((len(num_samples), len(beta)))
storm_timePerIter = np.zeros(len(num_samples))
guarantee_time = np.zeros(len(num_samples))
for n,N in enumerate(num_samples):
N = int(N)
print('\n >> Start for N='+str(N))
buffer += ['\n----------','\nStart for N='+str(N)]
ticDiff()
counter_array=run_sample(numiter, N, threshold, direction, parameters,
model, properties, model_file, verbose)
print("printing specification violation array")
print(counter_array)
#this is violation probability
storm_timePerIter[n] = np.round(tocDiff(False) / numiter, 3)
buffer += ['\n','Run time per iteration (of N samples) in Storm: '+str(storm_timePerIter[n]),'\n']
if eta != 0:
print('\nCOMPUTE BETA BASED ON ETA...')
print('\n------------\nOLD THEOREM:')
compute_avg_beta(counter_array, N, eta)
print('\n------------\nNEW THEOREM:')
beta_star[n] = np.round(compute_avg_beta_sttt(counter_array, N, eta), 5)
buffer += ['\nConfidence probability for eta='+str(eta)+' is beta='+str(beta_star[n])]
if beta != 0:
print('\nCOMPUTE ETA BASED ON BETA...')
print('\n------------\nNEW THEOREM:')
for i,bet in enumerate(beta):
print('\nCompute eta for beta='+str(bet))
eta_star[n,i] = np.round(compute_avg_eta_sttt(counter_array, N, bet), 5)
buffer += ['\nLower bound sat.prob. for beta='+str(bet)+' is eta='+str(eta_star[n,i])]
guarantee_time[n] = tocDiff(False)
buffer += ['\nTime required to compute guarantees: '+str(guarantee_time[n])]
f = open('output/'+outfile+'.txt', "w")
f.writelines(buffer)
f.close()
import pandas as pd
# Create a Pandas Excel writer using XlsxWriter as the engine.
writer = pd.ExcelWriter('output/'+outfile+'.xlsx', engine='xlsxwriter')
if eta != 0:
beta_df = pd.DataFrame(data=beta_star, index=num_samples, columns=[outfile])
beta_df.to_excel(writer, sheet_name='Confidence (beta)')
if beta != 0:
eta_df = pd.DataFrame(data=eta_star, index=num_samples, columns=beta)
eta_df.to_excel(writer, sheet_name='Sat.probability (eta)')
time_df = pd.DataFrame(data=storm_timePerIter, index=num_samples, columns=[outfile])
time_df.to_excel(writer, sheet_name='Time in storm')
time2_df = pd.DataFrame(data=guarantee_time, index=num_samples, columns=[outfile])
time2_df.to_excel(writer, sheet_name='Time for bounds')
# Close the Pandas Excel writer and output the Excel file.
writer.save()
print('\n\n---------------------\n\n')
\ No newline at end of file
### BRP (256,5)
python3 samplingprism.py --model-file brp/brp_256_5.pm --property-file brp/brp.prctl --threshold 0.5 --bisimulation weak --direction leq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.055 --outfile brp_256_5_sat.txt
python3 samplingprism.py --model-file brp/brp_256_5.pm --property-file brp/brp.prctl --threshold 0.5 --bisimulation weak --direction geq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.898 --outfile brp_256_5_unsat.txt
### BRP (16,5)
python3 samplingprism.py --model-file brp/brp_rewards4_16_5.pm --property-file brp/brp_rewards4.prctl --threshold 3 --bisimulation strong --direction leq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.275 --outfile brp_16-5_sat_output.txt
python3 samplingprism.py --model-file brp/brp_rewards4_16_5.pm --property-file brp/brp_rewards4.prctl --threshold 3 --bisimulation strong --direction geq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.676 --outfile brp_16-5_unsat_output.txt
### BRP (32,5)
python3 samplingprism.py --model-file brp/brp_rewards4_32_5.pm --property-file brp/brp_rewards4.prctl --threshold 3 --bisimulation weak --direction leq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.232 --outfile brp_32-5_sat_output.txt
python3 samplingprism.py --model-file brp/brp_rewards4_32_5.pm --property-file brp/brp_rewards4.prctl --threshold 3 --bisimulation weak --direction geq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.718 --outfile brp_32-5_unsat_output.txt
### CROWDS (10,5)
python3 samplingprism.py --model-file crowds/crowds_10_5.pm --property-file crowds/crowds.prctl --threshold 0.9 --bisimulation weak --direction leq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.537 --outfile crowds_10-5_sat_output.txt
python3 samplingprism.py --model-file crowds/crowds_10_5.pm --property-file crowds/crowds.prctl --threshold 0.9 --bisimulation weak --direction geq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.413 --outfile crows_10-5_unsat_output.txt
### CROWDS (15,7)
python3 samplingprism.py --model-file crowds/crowds_15_7.pm --property-file crowds/crowds.prctl --threshold 0.9 --bisimulation strong --direction leq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.411 --outfile crowds_15-7_sat_output.txt
python3 samplingprism.py --model-file crowds/crowds_15_7.pm --property-file crowds/crowds.prctl --threshold 0.9 --bisimulation strong --direction geq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.539 --outfile crowds_15-7_unsat_output.txt
### CROWDS (20,7)
python3 samplingprism.py --model-file crowds/crowds_20_7.pm --property-file crowds/crowds.prctl --threshold 0.9 --bisimulation strong --direction leq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.416 --outfile crowds_20-7_sat_output.txt --verbose 1
python3 samplingprism.py --model-file crowds/crowds_20_7.pm --property-file crowds/crowds.prctl --threshold 0.9 --bisimulation strong --direction geq --num_samples '(100,500,1000,5000,10000)' --num_iter 5 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.534 --outfile crowds_20-7_unsat_output.txt
### NAND (10,5)
python3 samplingprism.py --model-file nand/nand_10_5.pm --property-file nand/nand.prctl --threshold 0.05 --bisimulation weak --direction geq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.218 --outfile nand_10-5_sat_output.txt
python3 samplingprism.py --model-file nand/nand_10_5.pm --property-file nand/nand.prctl --threshold 0.05 --bisimulation weak --direction leq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.733 --outfile nand_10-5_unsat_output.txt
### NAND (25,5)
python3 samplingprism.py --model-file nand/nand_25_5.pm --property-file nand/nand.prctl --threshold 0.05 --bisimulation strong --direction geq --num_samples '(100,500,1000,5000,10000)' --num_iter 5 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.206 --outfile nand_25-5_sat_output.txt
python3 samplingprism.py --model-file nand/nand_25_5.pm --property-file nand/nand.prctl --threshold 0.05 --bisimulation strong --direction leq --num_samples '(100,500,1000,5000,10000)' --num_iter 5 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.744 --outfile nand_25-5_unsat_output.txt
### CONSENSUS (2,2)
python3 samplingprism.py --model-file consensus/coin2.pm --property-file consensus/coin2.prctl --threshold 0.25 --bisimulation strong --direction geq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.280 --outfile consensus_2-2_sat_output.txt
python3 samplingprism.py --model-file consensus/coin2.pm --property-file consensus/coin2.prctl --threshold 0.25 --bisimulation strong --direction leq --num_samples '(100,500,1000,5000,10000)' --num_iter 10 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.669 --outfile consensus_2-2_unsat_output.txt
### CONSENSUS (4,2)
python3 samplingprism.py --model-file consensus/coin4.pm --property-file consensus/coin2.prctl --threshold 0.25 --bisimulation strong --direction geq --num_samples '(100,1000,10000)' --num_iter 5 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.063 --outfile consensus_4-2_sat_output.txt
python3 samplingprism.py --model-file consensus/coin4.pm --property-file consensus/coin2.prctl --threshold 0.25 --bisimulation strong --direction leq --num_samples '(100,1000,10000)' --num_iter 5 --beta '(0.9,0.99,0.999,0.9999)' --eta 0.888 --outfile consensus_4-2_unsat_output.txt
### DRONE
## Uniform
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.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.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.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.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.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)'
(stormpyenv-upt) mcubuktepe@asg-a32265:~/research/codes/gurobi_parallel/sampler$ python3 samplingprism.py --model-file brp/brp_256_5.pm --property-file brp/brp.prctl --threshold 0.5 --bisimulation weak --direction leq --num_samples 1000 --num_iter 5 --violation_prob 0.945
Building model from brp/brp_256_5.pm
Model supports parameters: True
Number of states before bisim: 19720
Number of params before bisim: 2
Number of states after bisim: 3074
Number of params after bisim: 2
40%|██████████████████ | 2/5 [00:06<00:08, 2.72s/it]Average violation so far: 0.9175
60%|███████████████████████████ | 3/5 [00:09<00:05, 2.80s/it]Average violation so far: 0.915
80%|████████████████████████████████████ | 4/5 [00:11<00:02, 2.81s/it]Average violation so far: 0.9167500000000001
100%|█████████████████████████████████████████████| 5/5 [00:14<00:00, 2.91s/it]
Average solver time :2.946276569366455
printing specification violation array
[0.912, 0.923, 0.91, 0.922, 0.946]
probability of violating the spec less then the threshold for each iter:
[1.68618000e-06 9.01377110e-04 4.23643313e-07 5.57754162e-04
5.27646157e-01]
average alpha_nu values of the array:
0.10582147965735555
(stormpyenv-upt) mcubuktepe@asg-a32265:~/research/codes/gurobi_parallel/sampler$ python3 samplingprism.py --model-file brp/brp_256_5.pm --property-file brp/brp.prctl --threshold 0.5 --bisimulation weak --direction geq --num_samples 1000 --num_iter 5 --violation_prob 0.898
Building model from brp/brp_256_5.pm
Model supports parameters: True
Number of states before bisim: 19720
Number of params before bisim: 2
Number of states after bisim: 3074
Number of params after bisim: 2
40%|██████████████████ | 2/5 [00:03<00:05, 1.79s/it]Average violation so far: 0.086
60%|███████████████████████████ | 3/5 [00:05<00:03, 1.76s/it]Average violation so far: 0.084
80%|████████████████████████████████████ | 4/5 [00:07<00:01, 1.77s/it]Average violation so far: 0.086
100%|█████████████████████████████████████████████| 5/5 [00:08<00:00, 1.78s/it]
Average solver time :1.89861273765564
printing specification violation array
[0.09, 0.082, 0.08, 0.092, 0.065]
probability of violating the spec less then the threshold for each iter:
[1.14759450e-01 2.08002769e-02 1.23370286e-02 1.60446289e-01
6.84311516e-05]
average alpha_nu values of the array:
0.06168229511648571
(stormpyenv-upt) mcubuktepe@asg-a32265:~/research/codes/gurobi_parallel/sampler$ python3 samplingprism.py --model-file brp/brp_rewards4_16_5.pm --property-file brp/brp_rewards4.prctl --threshold 3 --bisimulation strong --direction leq --num_samples 1000 --num_iter 5 --violation_prob 0.725
Building model from brp/brp_rewards4_16_5.pm
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:02, 1.38it/s]Average violation so far: 0.7004999999999999
60%|███████████████████████████ | 3/5 [00:02<00:01, 1.23it/s]Average violation so far: 0.693
80%|████████████████████████████████████ | 4/5 [00:03<00:00, 1.10it/s]Average violation so far: 0.69
100%|█████████████████████████████████████████████| 5/5 [00:04<00:00, 1.03it/s]
Average solver time :0.968598937988281
printing specification violation array
[0.697, 0.704, 0.678, 0.681, 0.684]
probability of violating the spec less then the threshold for each iter:
[0.02177426 0.06392182 0.00038408 0.00081202 0.00164589]
average alpha_nu values of the array:
0.017707615704551705
(stormpyenv-upt) mcubuktepe@asg-a32265:~/research/codes/gurobi_parallel/sampler$ python3 samplingprism.py --model-file brp/brp_rewards4_16_5.pm --property-file brp/brp_rewards4.prctl --threshold 3 --bisimulation weak --direction leq --num_samples 1000 --num_iter 5 --violation_prob 0.725
Building model from brp/brp_rewards4_16_5.pm
Model supports parameters: True
Number of states before bisim: 1240
Number of params before bisim: 2
Number of states after bisim: 356
Number of params after bisim: 4
40%|██████████████████ | 2/5 [00:01<00:01, 1.64it/s]Average violation so far: 0.688
60%|███████████████████████████ | 3/5 [00:01<00:01, 1.67it/s]Average violation so far: 0.6999999999999998
80%|████████████████████████████████████ | 4/5 [00:02<00:00, 1.59it/s]Average violation so far: 0.6942499999999999
100%|█████████████████████████████████████████████| 5/5 [00:03<00:00, 1.58it/s]
Average solver time :0.681861639022827
printing specification violation array
[0.689, 0.687, 0.724, 0.677, 0.699]
probability of violating the spec less then the threshold for each iter:
[4.86920483e-03 3.19928760e-03 4.57699088e-01 2.96452958e-04
3.02749686e-02]
average alpha_nu values of the array:
0.09926780033866511
(stormpyenv-upt) mcubuktepe@asg-a32265:~/research/codes/gurobi_parallel/sampler$ python3 samplingprism.py --model-file brp/brp_rewards4_16_5.pm --property-file brp/brp_rewards4.prctl --threshold 3 --bisimulation weak --direction geq --num_samples 1000 --num_iter 5 --violation_prob 0.676
Building model from brp/brp_rewards4_16_5.pm
Model supports parameters: True
Number of states before bisim: 1240
Number of params before bisim: 2
Number of states after bisim: 356
Number of params after bisim: 4
40%|██████████████████ | 2/5 [00:01<00:01, 1.58it/s]Average violation so far: 0.298
60%|███████████████████████████ | 3/5 [00:01<00:01, 1.60it/s]Average violation so far: 0.296
80%|████████████████████████████████████ | 4/5 [00:02<00:00, 1.64it/s]Average violation so far: 0.29374999999999996
100%|█████████████████████████████████████████████| 5/5 [00:03<00:00, 1.64it/s]
Average solver time :0.614540147781372
printing specification violation array
[0.299, 0.297, 0.292, 0.287, 0.302]
probability of violating the spec less then the threshold for each iter:
[0.04891502 0.03667828 0.01664964 0.00682573 0.07314579]
average alpha_nu values of the array:
0.03644289047345837
(stormpyenv-upt) mcubuktepe@asg-a32265:~/research/codes/gurobi_parallel/sampler$ python3 samplingprism.py --model-file brp/brp_rewards4_32_5.pm --property-file brp/brp_rewards4.prctl --threshold 3 --bisimulation weak --direction leq --num_samples 1000 --num_iter 5 --violation_prob 0.768
Building model from brp/brp_rewards4_32_5.pm
Model supports parameters: True
Number of states before bisim: 2472
Number of params before bisim: 2
Number of states after bisim: 708
Number of params after bisim: 4
40%|██████████████████ | 2/5 [00:02<00:03, 1.23s/it]Average violation so far: 0.7495
60%|███████████████████████████ | 3/5 [00:03<00:02, 1.17s/it]Average violation so far: 0.747
80%|████████████████████████████████████ | 4/5 [00:04<00:01, 1.13s/it]Average violation so far: 0.745
100%|█████████████████████████████████████████████| 5/5 [00:05<00:00, 1.11s/it]
Average solver time :1.185850954055786
printing specification violation array
[0.749, 0.75, 0.742, 0.739, 0.75]
probability of violating the spec less then the threshold for each iter:
[0.07202628 0.0828813 0.02355679 0.01355167 0.0828813 ]
average alpha_nu values of the array:
0.05497946848141699
(stormpyenv-upt) mcubuktepe@asg-a32265:~/research/codes/gurobi_parallel/sampler$ python3 samplingprism.py --model-file brp/brp_rewards4_32_5.pm --property-file brp/brp_rewards4.prctl --threshold 3 --bisimulation weak --direction geq --num_samples 1000 --num_iter 5 --violation_prob 0.718
Building model from brp/brp_rewards4_32_5.pm
Model supports parameters: True
Number of states before bisim: 2472
Number of params before bisim: 2
Number of states after bisim: 708
Number of params after bisim: 4
40%|██████████████████ | 2/5 [00:01<00:02, 1.28it/s]Average violation so far: 0.257
60%|███████████████████████████ | 3/5 [00:02<00:01, 1.21it/s]Average violation so far: 0.249
80%|████████████████████████████████████ | 4/5 [00:03<00:00, 1.16it/s]Average violation so far: 0.2505
100%|█████████████████████████████████████████████| 5/5 [00:04<00:00, 1.13it/s]
Average solver time :0.924500226974487
printing specification violation array
[0.27, 0.244, 0.233, 0.255, 0.264]
probability of violating the spec less then the threshold for each iter:
[0.2094919 0.00420206 0.00032668 0.03127755 0.1093771 ]
average alpha_nu values of the array:
0.07093505981477459
(stormpyenv-upt) mcubuktepe@asg-a32265:~/research/codes/gurobi_parallel/sampler$ python3 samplingprism.py --model-file consensus/coin2.pm --property-file consensus/coin2.prctl --threshold 0.25 --bisimulation strong --direction leq --num_samples 1000 --num_iter 5 --violation_prob 0.331
Building model from consensus/coin2.pm
ModelType.MDP
Model supports parameters: True
Number of states before bisim: 272
Number of params before bisim: 2
Number of states after bisim: 153
Number of params after bisim: 2
40%|██████████████████ | 2/5 [00:00<00:01, 2.40it/s]Average violation so far: 0.3075
60%|███████████████████████████ | 3/5 [00:01<00:00, 2.42it/s]Average violation so far: 0.3113333333333333
80%|████████████████████████████████████ | 4/5 [00:01<00:00, 2.44it/s]Average violation so far: 0.30974999999999997
100%|█████████████████████████████████████████████| 5/5 [00:02<00:00, 2.42it/s]
Average solver time : 0.41347403526306153
printing specification violation array
[0.292, 0.323, 0.319, 0.305, 0.339]
probability of violating the spec less then the threshold for each iter:
[0.00397222 0.2839304 0.2004522 0.03747133 0.69287081]
average alpha_nu values of the array:
0.24373939271900946
(stormpyenv-upt) mcubuktepe@asg-a32265:~/research/codes/gurobi_parallel/sampler$ python3 samplingprism.py --model-file consensus/coin2.pm --property-file consensus/coin2.prctl --threshold 0.25 --bisimulation strong --direction geq --num_samples 1000 --num_iter 5 --violation_prob 0.280
Building model from consensus/coin2.pm
ModelType.MDP
Model supports parameters: True
Number of states before bisim: 272
Number of params before bisim: 2
Number of states after bisim: 153
Number of params after bisim: 2
40%|██████████████████ | 2/5 [00:00<00:01, 2.42it/s]Average violation so far: 0.69
60%|███████████████████████████ | 3/5 [00:01<00:00, 2.40it/s]Average violation so far: 0.6890000000000001
80%|████████████████████████████████████ | 4/5 [00:01<00:00, 2.36it/s]Average violation so far: 0.6867500000000001
100%|█████████████████████████████████████████████| 5/5 [00:02<00:00, 2.29it/s]
Average solver time : 0.43737068176269533
printing specification violation array
[0.684, 0.696, 0.687, 0.68, 0.704]
probability of violating the spec less then the threshold for each iter:
[0.00755319 0.04895274 0.01325936 0.00334861 0.13749182]
average alpha_nu values of the array:
0.04212114438788554
import numpy as np
from core.functions import compute_eta, compute_beta
# def compute_avg_beta(counterarray,N,eta):
# '''
# :param counterarray: approximate satisfaction probs
# :param N: number of samples
# :param eps:
# :param direction: if True, then the spec is \geq, if False, then it is \leq
# :return:
# '''
# #storing probabilities for each iteration
# valuearray = np.zeros(len(counterarray))
# for iters in range(len(counterarray)):
# #compute number of constraints to remove in the LP
# removeconstraints = int(N * (counterarray[iters]))
# #approximately compute the confidence prob
# val3 = BCDF(1-eta, N, removeconstraints)
# valuearray[iters] = val3
# print("average eta value of the array:")