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

added requirements.txt and license

parent b37c110d
instance,model checking type,Nr. props (Phi),#pars,#states,#trans,time_init,time_sample (x100),scen_opt_N=100,scen_opt_N=200,instantiator
sir20,exact,26,2,216,396,0.07,3.72,3.77,13.56,
kanban3,exact,4,13,58400,446400,6.75,65.8,3.52,9.41,
polling.3,exact,2,2,36,84,0.04,0.12,3.33,10.36,
buffer,exact,2,6,5632,21968,0.85,35.16,3.22,8.89,
tandem15,exact,2,5,496,1619,0.1,147.3,3.72,14.09,
embedded.64,exact,3,6,55868,235793,10.43,16.68,9.97,29.38,
pcs,exact,25,8,2041201,17963509,972.11,48.06,8.12,29.43,DFT (parametric)
rbc,exact,40,6,2269,12930,0.44,2.53,11.62,36.43,DFT (parametric)
dcas,exact,25,10,64,202,0.05,0.72,6.93,24.68,DFT (parametric)
rc.1-1-hc_parametric,exact,25,21,8401,49446,66.91,138.66,12.44,46.72,DFT (parametric)
hecs_2_1,exact,25,5,118945,1018603,42.73,7.2,8.86,29.57,DFT (parametric)
#!/bin/bash
cd ..;
OutputFile='partial_benchmark_stats.csv';
if [ -f "$OutputFile" ] ; then
rm "$OutputFile";
fi
echo -e "RUN PARTIAL SET OF BENCHMARKS\n";
#
# === CTMCS ===
......@@ -29,13 +33,18 @@ timeout 3600s python3 runfile.py --model ctmc/embedded/embedded.64.prism --N [10
#
# === Fault trees ===
echo -e "\n++++++++ START FAULT TREE BENCHMARKS ++++++++\n";
timeout 3600s python3 runfile.py --model sft/pcs/pcs.dft --N [100,200] --dft_checker 'parametric' --export_stats partial_benchmark_stats.csv;
timeout 3600s python3 runfile.py --model sft/pcs/pcs.dft --N 100 --dft_checker 'parametric' --export_stats $OutputFile;
timeout 3600s python3 runfile.py --model sft/pcs/pcs.dft --N 200 --dft_checker 'parametric' --export_stats $OutputFile;
#
timeout 3600s python3 runfile.py --model sft/rbc/rbc.dft --N [100,200] --dft_checker 'parametric' --export_stats partial_benchmark_stats.csv;
timeout 3600s python3 runfile.py --model sft/rbc/rbc.dft --N [100] --dft_checker 'parametric' --export_stats $OutputFile;
timeout 3600s python3 runfile.py --model sft/rbc/rbc.dft --N [200] --dft_checker 'parametric' --export_stats $OutputFile;
#
timeout 3600s python3 runfile.py --model dft/dcas/dcas.dft --N [100,200] --dft_checker 'parametric' --export_stats partial_benchmark_stats.csv;
timeout 3600s python3 runfile.py --model dft/dcas/dcas.dft --N [100] --dft_checker 'parametric' --export_stats $OutputFile;
timeout 3600s python3 runfile.py --model dft/dcas/dcas.dft --N [200] --dft_checker 'parametric' --export_stats $OutputFile;
#
timeout 3600s python3 runfile.py --model dft/rc/rc.1-1-hc_parametric.dft --param_file rc.1-1-hc_parameters.xlsx --prop_file properties.xlsx --N [100,200] --dft_checker 'parametric' --export_stats partial_benchmark_stats.csv;
timeout 3600s python3 runfile.py --model dft/rc/rc.1-1-hc_parametric.dft --param_file rc.1-1-hc_parameters.xlsx --prop_file properties.xlsx --N [100] --dft_checker 'parametric' --export_stats $OutputFile;
timeout 3600s python3 runfile.py --model dft/rc/rc.1-1-hc_parametric.dft --param_file rc.1-1-hc_parameters.xlsx --prop_file properties.xlsx --N [200] --dft_checker 'parametric' --export_stats $OutputFile;
#
timeout 3600s python3 runfile.py --model dft/hecs/hecs_2_1.dft --N [100,200] --dft_checker 'parametric' --export_stats partial_benchmark_stats.csv;
timeout 3600s python3 runfile.py --model dft/hecs/hecs_2_1.dft --N [100] --dft_checker 'parametric' --export_stats $OutputFile;
timeout 3600s python3 runfile.py --model dft/hecs/hecs_2_1.dft --N [200] --dft_checker 'parametric' --export_stats $OutputFile;
#
\ No newline at end of file
#!/bin/bash
cd ..;
echo -e "++++++++ RUN KANBAN(3) BENCHMARK ++++++++\n";
BoundsFile='output/kanban3_bounds.csv';
if [ -f "$BoundsFile" ] ; then
rm "$BoundsFile";
fi
OutputFile='kanban3_Table2.csv';
if [ -f "$OutputFile" ] ; then
rm "$OutputFile";
fi
BoundsFile='kanban3_bounds_Table2.csv';
if [ -f "$BoundsFile" ] ; then
rm "$BoundsFile";
fi
#
python3 runfile.py --model ctmc/kanban/kanban3.sm --N [100,200] --rho 1.1 --no-bisim --Nvalidate 1000 --seeds 2 --export_bounds $BoundsFile;
python3 runfile.py --model ctmc/kanban/kanban3.sm --N [100,200,400,800] --rho 1.1 --no-bisim --Nvalidate 1000 --seeds 10 --export_bounds $BoundsFile;
python3 gen_lower_bounds_table.py --file $BoundsFile --outfile $OutputFile;
#
#
echo -e "\n++++++++ RUN KANBAN(3) BENCHMARK ++++++++\n";
BoundsFile='output/rc1-1_bounds.csv';
if [ -f "$BoundsFile" ] ; then
rm "$BoundsFile";
fi
OutputFile='rc.1-1-hc_parametric_Table2.csv';
if [ -f "$OutputFile" ] ; then
rm "$OutputFile";
fi
BoundsFile='rc1-1_bounds_Table2.csv';
if [ -f "$BoundsFile" ] ; then
rm "$BoundsFile";
fi
#
python3 runfile.py --model dft/rc/rc.1-1-hc_parametric.dft --param_file rc.1-1-hc_parameters.xlsx --N [100,200] --rho 1.1 --Nvalidate 1000 --seeds 10 --export_bounds $BoundsFile;
python3 runfile.py --model dft/rc/rc.1-1-hc_parametric.dft --param_file rc.1-1-hc_parameters.xlsx --N [100,200,400,800] --rho 1.1 --Nvalidate 1000 --seeds 10 --export_bounds $BoundsFile;
python3 gen_lower_bounds_table.py --file $BoundsFile --outfile $OutputFile;
\ No newline at end of file
This diff is collapsed.
import os
import pathlib
import pandas as pd
import re
from slurf.commons import path
......
# -*- coding: utf-8 -*-
from slurf.commons import getDateTime
import pandas as pd
# Helper script to create an empty file for the table of benchmark statistics
EMPTY = pd.DataFrame(columns=['instance'])
EMPTY.set_index('instance', inplace=True)
file = 'Benchmark_statistics_='+str(getDateTime())
EMPTY.to_csv(file+'.csv')
\ No newline at end of file
no_props;100;200
25;0.88;
50;0.88;
100;0.88;
200;0.88;
400;0.88;
800;0.88;
N;0.9_mean;0.9_std;0.99_mean;0.99_std;0.999_mean;0.999_std;Frequentist_mean;Frequentist_std
100;0.862;0.0;0.827;0.0;0.798;0.0;973.0;24.042
200;0.93;0.0;0.911;0.0;0.895;0.0;973.5;6.364
#;N;seed;rho;Frequentist;0.9;0.99;0.999
\ No newline at end of file
instance,model checking type,Nr. props (Phi),#pars,#states,#trans,time_init,time_sample (x100),scen_opt_N=100,scen_opt_N=200,instantiator
sir20,exact,26,2,216,396,3e-02,3.49,2.94,12.32,
kanban3,exact,4,13,58400,446400,13.51,91.31,3.5,9.08,
polling.3,exact,2,2,36,84,0.02,0.1,3.95,10.2,CTMC
N;0.9_mean;0.9_std;0.99_mean;0.99_std;0.999_mean;0.999_std;Frequentist_mean;Frequentist_std
100;0.88;0.018;0.846;0.019;0.818;0.02;950.4;31.454
200;0.94;0.011;0.923;0.012;0.907;0.013;969.8;10.465
# List of used packages
pandas==1.3.5
numpy==1.21.4
setuptools==58.0.4
pytest==6.2.5
cvxpy==1.1.17
tqdm==4.62.3
seaborn==0.11.2
scipy==1.8.0
matplotlib==3.5.1
stormpy>=1.6.3
xlsxwriter==3.0.2
\ No newline at end of file
......@@ -46,6 +46,8 @@ if __name__ == '__main__':
# Parse arguments
ARGS = parse_arguments()
print(ARGS)
# Define dictionary for variables for which we can pass multiple values.
# We will iterate over these variables as iterations of the same experiment
iterate_dict = {'N': ARGS.Nsamples,
......
......@@ -32,13 +32,17 @@ setup(
zip_safe=False,
install_requires=[
'stormpy>=1.6.3', # Back-end model checker
'cvxpy',
'matplotlib',
'numpy',
'cvxpy>=1.1.17',
'matplotlib>=3.5.1',
'numpy>=1.21.4',
'openpyxl', # Read Excel files
'seaborn',
'tqdm', # Progress bar
'xlsxwriter' # Write Excel files
'seaborn>=0.11.2',
'tqdm>=4.62.3', # Progress bar
'xlsxwriter>=3.0.2', # Write Excel files
'pandas>=1.3.5',
'setuptools>=58.0.4',
'pytest>=6.2.5',
'scipy>=1.8.0'
],
setup_requires=['pytest-runner'],
tests_require=['pytest'],
......
no_props;50;100;200;400;800
25;0.55;1.35;5.38;24.27;167.47
100;1.35;3.61;13.72;74.05;310.06
25;2.02;4.91;24.07;;
100;2.02;4.91;24.07;;
200;2.02;4.91;24.07;;
400;2.02;4.91;24.07;;
800;2.02;4.91;24.07;;
......@@ -171,7 +171,9 @@ class ApproximateChecker:
@staticmethod
def formulas_lower_upper(formula, abort_label, model_desc=None):
lb_formula = formula
# TODO once instantiation checker yields transient probabilities, this is no longer necessary
if type(formula.subformula.right_subformula) == sp.logic.AtomicLabelFormula:
reach_label = "\"" + formula.subformula.right_subformula.label + "\""
else:
......
......@@ -6,15 +6,27 @@ import pandas as pd
def path(root_dir, folder, file):
"""
Internal method for simpler listing of examples.
:param folder: Folder.
:param file: Example file.
:return: Complete path to example file.
Parameters
----------
:folder: Folder.
:file: Example file.
----------
Returns
----------
Complete path to example file.
----------
"""
return os.path.join(root_dir, folder, file)
def create_output_folder(root_dir, modelfile):
"""
Create the specified folder.
"""
output_root_dir = path(root_dir, "output", "")
output_subfolder = modelfile.replace(".", "_") + '_date=' + getDateTime()
output_path = path(output_root_dir, output_subfolder, "")
......@@ -24,6 +36,9 @@ def create_output_folder(root_dir, modelfile):
def getTime():
"""
Returns the current time, given a datetime object.
"""
now = datetime.now()
current_time = now.strftime("%H:%M:%S")
......@@ -32,6 +47,9 @@ def getTime():
def getDateTime():
"""
Returns a formatted string of the datetime.
"""
now = datetime.now()
......@@ -39,6 +57,9 @@ def getDateTime():
def print_stats(stats):
"""
Print interesting statistics returned by Storm.
"""
print('-----------------------------------------')
print('MODEL STATISTICS:')
......@@ -50,6 +71,9 @@ def print_stats(stats):
def set_solution_df(exact, solutions):
"""
Define the Pandas DF for storing the solution vectors and return this.
"""
if not exact:
solutions = [[tuple(solutions[i,j,:])
......@@ -63,14 +87,21 @@ def set_solution_df(exact, solutions):
def set_output_path(root_dir, args):
"""
Define and return the full path to the output folder.
"""
output_folder = args.modelfile_nosuffix + "_N=" + str(args.Nsamples)
output_path = create_output_folder(root_dir, output_folder)
return output_path
def append_new_line(file_name, text_to_append):
"""Append given text as a new line at the end of file"""
"""
Append given text as a new line at the end of file
"""
# Open the file in append & read mode ('a+')
with open(file_name, "a+") as file_object:
# Move read cursor to the start of file.
......@@ -81,9 +112,11 @@ def append_new_line(file_name, text_to_append):
file_object.write("\n")
# Append text at the end of file
file_object.write(text_to_append)
def intersect(i1, i2):
'''
"""
Check if two intervals i1, i2 intersect.
'''
"""
return max(i1[0], i2[0]) < min(i1[1], i2[1])
\ No newline at end of file
#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""
Created on Mon Oct 25 17:35:21 2021
@author: thom
"""
import numpy as np
import math
def etaLow(N, k, beta, verbose=False):
'''
"""
Rootfinding problem to compute the lower bound on the satprob (eta)
Parameters
......@@ -27,7 +20,7 @@ def etaLow(N, k, beta, verbose=False):
eta_star : float
Lower bound on the satisfaction probability.
'''
"""
# Compute combination (i, k) in logarithmic base (term 1)
m1 = np.array([np.arange(k,N+1)])
......@@ -50,7 +43,8 @@ def etaLow(N, k, beta, verbose=False):
while t2-t1 > 1E-10:
t = (t1+t2)/2
polyt = 1+(1-beta)/(N) - (1-beta)/(N)*np.sum( np.exp( coeffs1 - (N-m1)*np.log(t) ), axis=1 )
polyt = 1+(1-beta)/(N) - (1-beta)/(N)*np.sum( np.exp(
coeffs1 - (N-m1)*np.log(t) ), axis=1 )
if polyt > 0:
t2 = t
......@@ -65,11 +59,22 @@ def etaLow(N, k, beta, verbose=False):
return eta_star
def remainder(k,N,eta,beta):
"""
Helper function to compute the accuracy of the current solution to the
root finding problem.
"""
return math.comb(N,k) * eta**(N-k) - (1-beta)/N * sum([math.comb(i,k)*eta**(i-k) for i in range(k,N)])
return math.comb(N,k) * eta**(N-k) - (1-beta)/N * \
sum([math.comb(i,k)*eta**(i-k) for i in range(k,N)])
def compute_beta(k,N,eta):
"""
Compute the confidence probability (beta) for a given containment
probability (eta), a given complexity (k) and a given sample size (N)
"""
invbeta = 0
......@@ -83,26 +88,4 @@ def compute_beta(k,N,eta):
beta = 1 - N/invbeta
return beta
# Approximation of binomial cdf with continuity correction for large n
# n: trials, p: success prob, m: starting successes
def BCDF(p, n, m):
return 1-CDF((m-0.5-(n*p))/math.sqrt(n*p*(1-p)))
def CDF(x):
return (1.0 + math.erf(x/math.sqrt(2.0)))/2.0
def determine_discarded(N=1000, beta=1e-6, eta=0.86):
k = 0
res = -1
while res < beta and k < N:
#res = math.comb(N+1, N) * sum([math.comb(N, i)*(eta)**(N-i)*(1-eta)**(i) for i in range(k+1)])
res = sum([math.comb(N, i)*(eta)**(N-i)*(1-eta)**(i) for i in range(k+1)])
k+=1
# print(k,':',res)
print('Number of discarded constraints:',k)
\ No newline at end of file
return beta
\ No newline at end of file
......@@ -11,7 +11,8 @@ import time
class CtmcReliabilityModelSamplerInterface(ModelSamplerInterface):
"""
This simple interface builds a parametric CTMC and then uses an instantiation checker to check the model.
This simple interface builds a parametric CTMC and then uses an
instantiation checker to check the model.
"""
def init_from_model(self, model, bisim=True):
......@@ -22,7 +23,7 @@ class CtmcReliabilityModelSamplerInterface(ModelSamplerInterface):
----------
model CTMC.
Returns Dict of all parameters and their bounds (default [0, infinity)).
Returns Dict of all params. and their bounds (default [0, infinity)).
-------
"""
......@@ -56,7 +57,8 @@ class CtmcReliabilityModelSamplerInterface(ModelSamplerInterface):
Parameters
----------
properties Properties either given as a tuple (event, [time bounds]) or a list of properties.
properties Properties either given as a tuple (event, [time bounds]) or
a list of properties.
-------
"""
......@@ -86,11 +88,12 @@ class CtmcReliabilityModelSamplerInterface(ModelSamplerInterface):
Parameters
----------
model A CTMC with a label.
properties Properties here is either a tuple (event, [time bounds]) or a list of properties.
properties Properties here is either a tuple (event, [time bounds]) or
a list of properties.
bisim Whether to apply bisimulation.
constants Constants for graph changing variables in model description (optional)
constants Constants for graph changing variables (optional)
Returns Dict of all parameters and their bounds (default [0, infinity)).
Returns Dict of all params. and their bounds (default [0, infinity)).
-------
"""
......
......@@ -37,10 +37,10 @@ class DftParametricModelSamplerInterface(DftModelSamplerInterface):
Parameters
----------
model A DFT with parametric failure rates.
properties Properties here is either a tuple (event, [time bounds]) or a list of properties.
bisim Whether to apply bisimulation.
constants Constants for graph changing variables in model description (not required for fault trees)
:model: A DFT with parametric failure rates.
:properties: Properties here is either a tuple (event, [time bounds]) or a list of properties.
:bisim: Whether to apply bisimulation.
:constants: Constants for graph changing variables in model description (not required for fault trees)
Returns Dictionary of parameters and their bounds.
-------
......@@ -90,10 +90,10 @@ class DftConcreteApproximationSamplerInterface(DftModelSamplerInterface):
Parameters
----------
model A DFT with parametric failure rates.
properties Properties here is either a tuple (event, [time bounds]) or a list of properties.
bisim Whether to apply bisimulation.
constants Constants for graph changing variables in model description (not required for fault trees)
:model: A DFT with parametric failure rates.
:properties: Properties here is either a tuple (event, [time bounds]) or a list of properties.
:bisim: Whether to apply bisimulation.
:constants: Constants for graph changing variables in model description (not required for fault trees)
Returns Dictionary of parameters and their bounds.
-------
......
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