Skip to content
GitLab
Commit f3e68c53 authored by Hans Vrapi's avatar Hans Vrapi
Browse files

add readme files

parent 1a2243f2
Hide whitespace changes
Inline Side-by-side
ace_storm_comparison/disjunction_comparison/README.md 0 → 100644
View file @ f3e68c53
## run_disjunction_experiments.py
- runs all the experiments when considering the disjunction of multiple hypothesis nodes
- generates a csv file that contains information about the inference time for both storm and ace depending on the number of the hypothesis nodes and a plot that visualizes the results
- takes one boolean argument (optional)
- 'true': rerun the experiments, parse the results and plot them (if not set, the existing results will be plotted)
- command to run the script: python3 run_disjunction_experiments.py [true] ([] indicates that the argument is optional)
##disjunction_plot.tex
- latex source code used to visalize the results
ace_storm_comparison/disjunction_comparison/multiple-disjunction-ace-storm.csv deleted 100644 → 0
View file @ 1a2243f2
network,h_size,inference_time(s),scatterclass
hailfinder,2,0.004359633999999999,hail-ace
hailfinder,2,0.011,hail-storm
hailfinder,4,0.005741410999999999,hail-ace
hailfinder,4,0.012,hail-storm
hailfinder,8,0.011068933,hail-ace
hailfinder,8,0.007,hail-storm
hailfinder,16,1000,hail-ace
hailfinder,16,0.002,hail-storm
mildew,2,0.068277586,mild-ace
mildew,2,0.087,mild-storm
mildew,4,1000,mild-ace
mildew,4,0.205,mild-storm
mildew,8,1000,mild-ace
mildew,8,0.164,mild-storm
mildew,16,1000,mild-ace
mildew,16,0.324,mild-storm
win95pts,2,0.001964643,win9-ace
win95pts,2,0.004,win9-storm
win95pts,4,0.0018519139999999999,win9-ace
win95pts,4,0.005,win9-storm
win95pts,8,0.002482437,win9-ace
win95pts,8,0.003,win9-storm
win95pts,16,0.015508118,win9-ace
win95pts,16,0.001,win9-storm
ace_storm_comparison/unary_hypothesis/README.md 0 → 100644
View file @ f3e68c53
## run_unary_hyp_experiments.py
- runs the experiments when considering only one hypothesis node
- generates a csv file that contains information about the inference time for both storm and ace and a plot that visualizes the results
- takes one boolean argument (optional)
- 'true': rerun the experiments, parse the results and plot them (if not set, the existing results will be plotted)
- command to run the script: python3 run_disjunction_experiments.py [true] ([] indicates that the argument is optional)
##unary_hyp_plot.tex
- contains the latex source code used to visalize the results
ace_storm_comparison/unary_hypothesis/unary_hypothesis_ace_storm.csv deleted 100644 → 0
View file @ 1a2243f2
network,ace_inference_time,storm_nobisim_mar_time,scatterclass
alarm,1.51887,2.0,qual3
andes,43.490696,3472.0,qual3
asia,1.001232,0.1,qual3
barley,456.562866,100000.0,qual3
cancer,0.6354719999999999,1.0,qual3
child,1.131651,1.0,qual3
earthquake,0.619634,0.1,qual3
hailfinder,5.8919049999999995,11.0,qual3
hepar2,3.4639599999999997,7.0,qual3
insurance,11.57596,10.0,qual3
mildew,48.48359,442.0,qual3
pathfinder,300000.0,25.0,qual3
sachs,1.0922859999999999,0.1,qual3
survey,0.6524179999999999,0.1,qual3
water,12.981074,14.0,qual3
win95pts,3.005566,3.0,qual3
auxiliary_scripts/Dockerfile deleted 100644 → 0
View file @ 1a2243f2
FROM storm_bn:3
WORKDIR /opt
RUN rm Dockerfile
RUN mkdir storm_bn
RUN declare -a folders=("ace_storm_comparison" "auxiliary_scripts" "bn-mc-transformer" "feasibility_analysis" "parameter_space_partitioning" "psdd_storm_comparison" "sensitivity_analysis" "storm_evidence")
RUN for f in "${folders[@]}"; do mv f /storm_bn/ done
WORKDIR /opt/storm_bn
auxiliary_scripts/README.md 0 → 100644
View file @ f3e68c53
## add_param_to_bif.py
- adds single parameters by giving node, evaluation of parents, ...
- command to run the script: python3 run_disjunction_experiments.py [true] ([] indicates that the argument is optional)
##disjunction_plot.tex
- latex source code used to visalize the results
bn-mc-transformer/README.md
View file @ f3e68c53
Storm - A Modern Probabilistic Model Checker
============================================
## Use the Transformer
[![Build Status](https://github.com/moves-rwth/storm/workflows/Build%20Test/badge.svg)](https://github.com/moves-rwth/storm/actions)
[![GitHub release](https://img.shields.io/github/release/moves-rwth/storm.svg)](https://github.com/moves-rwth/storm/releases/)
[![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.1181896.svg)](https://doi.org/10.5281/zenodo.1181896)
1) Build the target (in ./bn-mc-transformer/build/bin)
mkdir build && cd build && cmake .. && make
For more instructions, check out the documentation found in [Getting Started](http://www.stormchecker.org/getting-started.html).
Benchmarks
----------------------------
Example input files for Storm can be obtained from
https://github.com/moves-rwth/storm-examples.
Various Benchmarks together with example invocations of Storm can be found at the [Quantitative Verification Benchmark Set (QVBS)](http://qcomp.org/benchmarks).
Further examples and benchmarks can be found in the following repositories:
* **Prism files** (DTMC, MDP, CTMC):
http://www.prismmodelchecker.org/benchmarks
* **Jani files** (DTMC, MDP, CTMC, MA):
http://jani-spec.org
* **GSPN**s:
(private, contact: sebastian.junges@cs.rwth-aachen.de)
* **DFT**s:
https://github.com/moves-rwth/dft-examples
* **PGCL**:
(private, contact: sebastian.junges@cs.rwth-aachen.de)
Authors
-----------------------------
Storm has been developed at RWTH Aachen University.
###### Principal developers
* Christian Hensel
* Sebastian Junges
* Joost-Pieter Katoen
* Tim Quatmann
* Matthias Volk
###### Developers (lexicographical order)
* Jana Berger
* Alexander Bork
* David Korzeniewski
* Jip Spel
###### Contributors (lexicographical order)
* Daniel Basgöze
* Dimitri Bohlender
* Harold Bruintjes
* Michael Deutschen
* Linus Heck
* Thomas Heinemann
* Thomas Henn
* Tom Janson
* Jan Karuc
* Joachim Klein
* Gereon Kremer
* Sascha Vincent Kurowski
* Hannah Mertens
* Stefan Pranger
* Svenja Stein
* Manuel Sascha Weiand
* Lukas Westhofen
2) Run the transformer
./Path to bin/storm-bn-robin name of the network
bn-mc-transformer/src/storm-bn-robin-cli/storm-bn-robin.cpp
View file @ f3e68c53
......@@ -35,49 +35,40 @@ int main(const int argc, const char **argv) {
try {
storm::utility::setUp();
storm::cli::printHeader("Storm-bn-robin", argc, argv);
Utils util;
std::string variableFile;
bool findOrdering = false;
if(argc < 4){
std::cout << "Arguments are missing!";
return 1;
}
std::string folder = argv[1];
std::string ev_nodes = argv[2];
std::string fileName = argv[3];
std::string networkName;
std::string folder = "/home/hans/Desktop/Storm-bn/bn-mc-transformer/src/storm-bn-robin/TheBestTopologicalOrderings/evidence_tailored/1/"; //directory with the bif and jani files
std::cin >> networkName; //name of the network for which the jani file needs to be generated
bool isTailored = true; //indicates whether the transformation is evidence-tailored (if set to true) or agnostic (if set to false)
if (findOrdering) {
variableFile.clear();
} else {
variableFile = folder + "var_files/" + fileName + ".var";
std::cout << variableFile;
variableFile = folder + networkName + ".var";
}
BNNetwork network(folder, fileName, ".bif", ev_nodes, variableFile);
BNNetwork network(folder, networkName, ".bif", isTailored, variableFile);
std::string fileContent = VariablesFileCreator::createVariableFileContent(network.getSortedProbabilityTables());
if (!fileContent.empty()) {
JaniFileCreator creator(network);
util.writeToFile(creator.create(), folder + "jani_files/" + ev_nodes + "/" + fileName + ".jani");
util.writeToFile(creator.create(), folder + networkName + ".jani");
}
std::cout << "done." << "\n";
return 0;
}
catch (storm::exceptions::BaseException const&exception) {
STORM_LOG_ERROR(
"An exception caused Storm to terminate. The message of the exception is: " << exception.what());
catch (storm::exceptions::BaseException const&exception) {
STORM_LOG_ERROR(
"An exception caused Storm to terminate. The message of the exception is: " << exception.what());
return 1;
} catch (std::exception const&exception) {
STORM_LOG_ERROR(
"An unexpected exception occurred and caused Storm to terminate. The message of this exception is: "
<< exception.what());
return 2;
}
}
catch (std::exception const&exception) {
STORM_LOG_ERROR(
"An unexpected exception occurred and caused Storm to terminate. The message of this exception is: "
<< exception.what());
return 2;
}
}
bn-mc-transformer/src/storm-bn-robin/TheBestTopologicalOrderings/evidence_tailored/1/cancer.jani
View file @ f3e68c53
......@@ -16,13 +16,13 @@
},
{
"initial-value": false,
"name": "Pollution0",
"name": "Pollution_0",
"transient": true,
"type": "bool"
},
{
"initial-value": false,
"name": "Pollution1",
"name": "Pollution_1",
"transient": true,
"type": "bool"
},
......@@ -38,13 +38,13 @@
},
{
"initial-value": false,
"name": "Smoker0",
"name": "Smoker_0",
"transient": true,
"type": "bool"
},
{
"initial-value": false,
"name": "Smoker1",
"name": "Smoker_1",
"transient": true,
"type": "bool"
},
......@@ -60,13 +60,13 @@
},
{
"initial-value": false,
"name": "Cancer0",
"name": "Cancer_0",
"transient": true,
"type": "bool"
},
{
"initial-value": false,
"name": "Cancer1",
"name": "Cancer_1",
"transient": true,
"type": "bool"
},
......@@ -82,13 +82,13 @@
},
{
"initial-value": false,
"name": "Xray0",
"name": "Xray_0",
"transient": true,
"type": "bool"
},
{
"initial-value": false,
"name": "Xray1",
"name": "Xray_1",
"transient": true,
"type": "bool"
}
......@@ -106,7 +106,7 @@
"name": "loc1",
"transient-values": [
{
"ref": "Pollution0",
"ref": "Pollution_0",
"value": {
"op": "=",
"left": "Pollution",
......@@ -114,7 +114,7 @@
}
},
{
"ref": "Pollution1",
"ref": "Pollution_1",
"value": {
"op": "=",
"left": "Pollution",
......@@ -127,7 +127,7 @@
"name": "loc2",
"transient-values": [
{
"ref": "Smoker0",
"ref": "Smoker_0",
"value": {
"op": "=",
"left": "Smoker",
......@@ -135,7 +135,7 @@
}
},
{
"ref": "Smoker1",
"ref": "Smoker_1",
"value": {
"op": "=",
"left": "Smoker",
......@@ -148,7 +148,7 @@
"name": "loc3",
"transient-values": [
{
"ref": "Cancer0",
"ref": "Cancer_0",
"value": {
"op": "=",
"left": "Cancer",
......@@ -156,7 +156,7 @@
}
},
{
"ref": "Cancer1",
"ref": "Cancer_1",
"value": {
"op": "=",
"left": "Cancer",
......@@ -169,7 +169,7 @@
"name": "loc4",
"transient-values": [
{
"ref": "Xray0",
"ref": "Xray_0",
"value": {
"op": "=",
"left": "Xray",
......@@ -177,7 +177,7 @@
}
},
{
"ref": "Xray1",
"ref": "Xray_1",
"value": {
"op": "=",
"left": "Xray",
......
bn-mc-transformer/src/storm-bn-robin/TheBestTopologicalOrderings/evidence_tailored/1/d.jani deleted 100644 → 0
View file @ 1a2243f2
{
"jani-version": 1,
"name": "d.jani",
"type": "dtmc",
"features": [ "derived-operators" ],
"variables": [
],
"properties": [
],
"automata": [
{
"name": "d",
"locations": [
{
"name": "loc0"
},
],
"initial-locations": ["loc0"],
"edges": [
]
}
],
"system": {
"elements": [ {"automaton": "d"} ]
}
}
bn-mc-transformer/src/storm-bn-robin/src/parser/BNNetwork.cpp
View file @ f3e68c53
......@@ -59,12 +59,12 @@ BNNetwork::BNNetwork(const std::string &networkName, const std::vector<BNNode> &
sortTheTables();
}
BNNetwork::BNNetwork(const std::string &fileLoc, const std::string &fileName, const std::string &fileFormat, const std::string &ev_nodes,
const std::string &varFilePath)
BNNetwork::BNNetwork(const std::string &fileLoc, const std::string &fileName, const std::string &fileFormat, bool isTailored,
const std::string &varFilePath)
{
networkName = fileName;
Utils util;
fileContent = util.readFile(fileLoc + "bif_files/" + ev_nodes + "/" + fileName + fileFormat);
fileContent = util.readFile(fileLoc + fileName + fileFormat);
createEvidenceList();
......@@ -82,67 +82,57 @@ BNNetwork::BNNetwork(const std::string &fileLoc, const std::string &fileName, co
std::vector<std::string> nodesToProcess;
std::vector<std::string> requiredNodesNames;
std::vector<std::string> parentsNames;
for (BNNode n : nodes)
{
if (n.isObserved() || n.isQuestioned())
{
nodesToProcess.push_back(n.getNodeName());
//check whether the transformation needs to be tailored to the evidence and hypothesis nodes or not
if(isTailored == true){
for (BNNode n : nodes){
if (n.isObserved() || n.isQuestioned()){
nodesToProcess.push_back(n.getNodeName());
}
}
}
if (!nodesToProcess.empty())
{
std::vector<std::string> processedNodes;
std::string currentNode;
while (!nodesToProcess.empty())
{
currentNode = nodesToProcess[nodesToProcess.size() - 1];
nodesToProcess.pop_back();
if (!nodesToProcess.empty()){
std::vector<std::string> processedNodes;
std::string currentNode;
while (!nodesToProcess.empty()){
currentNode = nodesToProcess[nodesToProcess.size() - 1];
nodesToProcess.pop_back();
processedNodes.push_back(currentNode);
ProbabilityTable pTable = nodeNameToTableMap[currentNode];
parentsNames = pTable.getParentsNames();
for (std::string pName : parentsNames){
if (std::find(processedNodes.begin(), processedNodes.end(), pName) == processedNodes.end()){
nodesToProcess.push_back(pName);
}
}
}
processedNodes.push_back(currentNode);
ProbabilityTable pTable = nodeNameToTableMap[currentNode];
parentsNames = pTable.getParentsNames();
for (std::string pName : parentsNames)
{
if (std::find(processedNodes.begin(), processedNodes.end(), pName) == processedNodes.end())
{
nodesToProcess.push_back(pName);
for (BNNode n : nodes){
if (std::find(processedNodes.begin(), processedNodes.end(), n.getNodeName()) != processedNodes.end()){
requiredNodesNames.push_back(n.getNodeName());
}
}
}
for (BNNode n : nodes)
{
if (std::find(processedNodes.begin(), processedNodes.end(), n.getNodeName()) != processedNodes.end())
{
requiredNodesNames.push_back(n.getNodeName());
for (std::string nodeName : requiredNodesNames){
requiredProbabilityTables.push_back(nodeNameToTableMap[nodeName]);
requiredNodes.push_back(nameToNodeMap[nodeName]);
}
nodes = requiredNodes;
probabilityTables = requiredProbabilityTables;
}
for (std::string nodeName : requiredNodesNames)
{
requiredProbabilityTables.push_back(nodeNameToTableMap[nodeName]);
requiredNodes.push_back(nameToNodeMap[nodeName]);
std::map<std::string, ProbabilityTable> nodeNameToTableMap_red;
std::map<std::string, int> nodeTopologicalOrder_red;
int order = 1;
for(auto pTable: probabilityTables){
nodeNameToTableMap_red[pTable.getNodeName()] = pTable;
nodeTopologicalOrder_red[pTable.getNodeName()] = order;
order++;
}
nodes = requiredNodes;
probabilityTables = requiredProbabilityTables;
}
std::map<std::string, ProbabilityTable> nodeNameToTableMap_red;
std::map<std::string, int> nodeTopologicalOrder_red;
int order = 1;
for(auto pTable: probabilityTables){
nodeNameToTableMap_red[pTable.getNodeName()] = pTable;
nodeTopologicalOrder_red[pTable.getNodeName()] = order;
order++;
nodeNameToTableMap = nodeNameToTableMap_red;
nodeTopologicalOrder = nodeTopologicalOrder_red;
}
nodeNameToTableMap = nodeNameToTableMap_red;
nodeTopologicalOrder = nodeTopologicalOrder_red;
for (const auto &probabilityTable : probabilityTables)
{
for (const auto &probabilityTable : probabilityTables){
dag.addNode(probabilityTable.getNodeName(), probabilityTable.getPossibleValues().size());
}
......@@ -151,22 +141,19 @@ BNNetwork::BNNetwork(const std::string &fileLoc, const std::string &fileName, co
string line;
string var;
string varFileContent = "";
while (getline(varFile, line))
{
while (getline(varFile, line)){
std::string::size_type pos = line.find('-');
if (pos != std::string::npos)
{
if (pos != std::string::npos){
var = line.substr(0, pos);
}
else
{
}else{
var = line;
}
// check whether variable is still relevant
if (std::find(requiredNodesNames.begin(), requiredNodesNames.end(), var) != requiredNodesNames.end())
{
varFileContent += line + "\n";
if(isTailored){
if (std::find(requiredNodesNames.begin(), requiredNodesNames.end(), var) != requiredNodesNames.end()){
varFileContent += line + "\n";
}
}
// check whether variable is still relevant
}
addEdgesToDAG();
......
bn-mc-transformer/src/storm-bn-robin/src/parser/BNNetwork.h
View file @ f3e68c53
......@@ -31,7 +31,7 @@ public:
const std::vector<Evidence> &evidences, const std::vector<Hypothesis> &hypothesises,
const std::unordered_set<std::string> &parameterNames);
BNNetwork(const std::string& fileLoc, const std::string& fileName, const std::string& fileFormat, const std::string& ev_nodes, const std::string& varFilePath = "");
BNNetwork(const std::string& fileLoc, const std::string& fileName, const std::string& fileFormat, bool isTailored, const std::string& varFilePath = "");
std::vector<BNNode> getNodes() const;
......
psdd_storm_comparison/README.md 0 → 100644
View file @ f3e68c53
## run_psdd_storm_comparison.py
- runs the experiments using psdd and storm for the networks 'andes' and 'win95pts' and outputs a table containing for each pair of method and network the corresponding construction and inference time
- takes one boolean argument (optional)
- 'true': rerun the experiments, parse the results and output them (if not set, the existing results will be parsed)
- command to run the script: python3 run_psdd_storm_comparison.py [true] ([] indicates that the argument is optional)
psdd_storm_comparison/psdd/build/CMakeCache.txt
View file @ f3e68c53
# This is the CMakeCache file.
# For build in directory: /home/hans/Desktop/private/psdd_storm_comparison/psdd/build
# For build in directory: /home/hans/Desktop/Storm-bn/psdd_storm_comparison/psdd/build
# It was generated by CMake: /usr/bin/cmake
# You can edit this file to change values found and used by cmake.
# If you do not want to change any of the values, simply exit the editor.
......@@ -210,10 +210,10 @@ CMAKE_STRIP:FILEPATH=/usr/bin/strip
CMAKE_VERBOSE_MAKEFILE:BOOL=FALSE
//Value Computed by CMake
psdd_BINARY_DIR:STATIC=/home/hans/Desktop/private/psdd_storm_comparison/psdd/build
psdd_BINARY_DIR:STATIC=/home/hans/Desktop/Storm-bn/psdd_storm_comparison/psdd/build
//Value Computed by CMake
psdd_SOURCE_DIR:STATIC=/home/hans/Desktop/private/psdd_storm_comparison/psdd
psdd_SOURCE_DIR:STATIC=/home/hans/Desktop/Storm-bn/psdd_storm_comparison/psdd
########################
......@@ -225,7 +225,7 @@ CMAKE_ADDR2LINE-ADVANCED:INTERNAL=1
//ADVANCED property for variable: CMAKE_AR
CMAKE_AR-ADVANCED:INTERNAL=1
//This is the directory where this CMakeCache.txt was created