From 40a982430c07401dd0162185ef51dc0ce1a325e8 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 22 Aug 2017 15:46:30 +0200
Subject: [PATCH 01/39] cmake for carl: handle situation where carl version
information is missing
Older carl versions don't provide detailed version information, so we
provide an informative error message instead of cmake syntax errors during
the comparison.
---
resources/3rdparty/CMakeLists.txt | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 243c0b0e5..b4f200234 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -215,6 +215,10 @@ if(USE_CARL)
else()
message(SEND_ERROR "File ${carlLOCATION} does not exist, did you build carl?")
endif()
+ if("${carl_MINORYEARVERSION}" STREQUAL "" OR "${carl_MINORMONTHVERSION}" STREQUAL "" OR "${carl_MAINTENANCEVERSION}" STREQUAL "")
+ # don't have detailed version information, probably an old version of carl
+ message(FATAL_ERROR "Carl at ${carlLOCATION} outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}")
+ endif()
if(${carl_MINORYEARVERSION} LESS ${CARL_MINYEAR})
message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}")
elseif(${carl_MINORYEARVERSION} EQUAL ${CARL_MINYEAR})
From 76fa67fd3541ca23ed6f5dea773ab05d1d143570 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 25 Sep 2017 16:26:41 +0200
Subject: [PATCH 02/39] added missing include
---
src/storm/solver/AbstractEquationSolver.h | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h
index 362239360..6ad9c32ad 100644
--- a/src/storm/solver/AbstractEquationSolver.h
+++ b/src/storm/solver/AbstractEquationSolver.h
@@ -2,6 +2,7 @@
#define STORM_SOLVER_ABSTRACTEQUATIONSOLVER_H_
#include <memory>
+#include <chrono>
#include <boost/optional.hpp>
From cb15db041c2ce690d4f551fee01f96691d362506 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 25 Sep 2017 18:12:04 +0200
Subject: [PATCH 03/39] add missing include
---
.../modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h b/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h
index f54c810fb..7f2bb4278 100644
--- a/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h
+++ b/src/storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h
@@ -1,6 +1,7 @@
#pragma once
#include <vector>
+#include <cstdint>
namespace storm {
namespace storage {
From 50ba6866ebb0dd245f8ab1686bd77d750708f67e Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 28 Sep 2017 12:14:27 +0200
Subject: [PATCH 04/39] checking solver requirements for PLA
---
...SparseDtmcParameterLiftingModelChecker.cpp | 48 +++++++++++++++++--
.../SparseDtmcParameterLiftingModelChecker.h | 8 ++--
2 files changed, 49 insertions(+), 7 deletions(-)
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index 119e3791d..150a9d86c 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -6,6 +6,8 @@
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
+#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
@@ -17,6 +19,8 @@
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/UncheckedRequirementException.h"
+
namespace storm {
namespace modelchecker {
@@ -27,7 +31,7 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
- SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)) {
+ SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false) {
// Intentionally left empty
}
@@ -109,6 +113,8 @@ namespace storm {
// We know some bounds for the results so set them
lowerResultBound = storm::utility::zero<ConstantType>();
upperResultBound = storm::utility::one<ConstantType>();
+ // No requirements for bounded formulas
+ solverFactory->setRequirementsChecked(true);
}
template <typename SparseModelType, typename ConstantType>
@@ -139,6 +145,12 @@ namespace storm {
// We know some bounds for the results so set them
lowerResultBound = storm::utility::zero<ConstantType>();
upperResultBound = storm::utility::one<ConstantType>();
+
+ auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::UntilProbabilities);
+ req.clearBounds();
+ req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
+ STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
+ solverFactory->setRequirementsChecked(true);
}
template <typename SparseModelType, typename ConstantType>
@@ -172,6 +184,17 @@ namespace storm {
// We only know a lower bound for the result
lowerResultBound = storm::utility::zero<ConstantType>();
+
+ auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards);
+ req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
+ req.clearLowerBounds();
+ if (req.requiresUpperBounds()) {
+ solvingRequiresUpperRewardBounds = true;
+ req.clearUpperBounds();
+ }
+ STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
+ solverFactory->setRequirementsChecked(true);
+
}
@@ -200,6 +223,9 @@ namespace storm {
// We only know a lower bound for the result
lowerResultBound = storm::utility::zero<ConstantType>();
+
+ // No requirements for bounded reward formula
+ solverFactory->setRequirementsChecked(true);
}
template <typename SparseModelType, typename ConstantType>
@@ -228,7 +254,23 @@ namespace storm {
}
auto solver = solverFactory->create(parameterLifter->getMatrix());
if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
- if (upperResultBound) solver->setUpperBound(upperResultBound.get());
+ if (upperResultBound) {
+ solver->setUpperBound(upperResultBound.get());
+ } else if (solvingRequiresUpperRewardBounds) {
+ // For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17).
+ std::vector<typename SparseModelType::ValueType> oneStepProbs;
+ oneStepProbs.reserve(parameterLifter->getMatrix().getRowCount());
+ for (uint64_t row = 0; row < parameterLifter->getMatrix().getRowCount(); ++row) {
+ oneStepProbs.push_back(storm::utility::one<typename SparseModelType::ValueType>() - parameterLifter->getMatrix().getRowSum(row));
+ }
+ if (dirForParameters == storm::OptimizationDirection::Minimize) {
+ storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<typename SparseModelType::ValueType> dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+ solver->setUpperBounds(dsmpi.computeUpperBounds());
+ } else {
+ storm::modelchecker::helper::BaierUpperRewardBoundsComputer<typename SparseModelType::ValueType> baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+ solver->setUpperBound(baier.computeUpperBound());
+ }
+ }
if (!stepBound) solver->setTrackScheduler(true);
if (storm::solver::minimize(dirForParameters) && minSchedChoices && !stepBound) solver->setInitialScheduler(std::move(minSchedChoices.get()));
if (storm::solver::maximize(dirForParameters) && maxSchedChoices && !stepBound) solver->setInitialScheduler(std::move(maxSchedChoices.get()));
@@ -247,7 +289,7 @@ namespace storm {
}
// Invoke the solver
- if(stepBound) {
+ if (stepBound) {
assert(*stepBound > 0);
x = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
solver->repeatedMultiply(dirForParameters, x, ¶meterLifter->getVector(), *stepBound);
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
index d6f51032b..b4a8644b6 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
@@ -12,7 +12,6 @@
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/logic/FragmentSpecification.h"
-
namespace storm {
namespace modelchecker {
@@ -49,12 +48,13 @@ namespace storm {
storm::storage::BitVector maybeStates;
std::vector<ConstantType> resultsForNonMaybeStates;
boost::optional<uint_fast64_t> stepBound;
-
+
std::unique_ptr<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>> instantiationChecker;
-
+
std::unique_ptr<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>> parameterLifter;
std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>> solverFactory;
-
+ bool solvingRequiresUpperRewardBounds;
+
// Results from the most recent solver call.
boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
std::vector<ConstantType> x;
From 1396de3c5face64731f00f33f0096b41c0957c3c Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 28 Sep 2017 12:15:37 +0200
Subject: [PATCH 05/39] Enforce no end components when we want to compute a
scheduler from a minmax equation system
---
.../IterativeMinMaxLinearEquationSolver.cpp | 5 +++++
src/storm/solver/LpMinMaxLinearEquationSolver.cpp | 15 +++++++++++++++
src/storm/solver/LpMinMaxLinearEquationSolver.h | 2 ++
3 files changed, 22 insertions(+)
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index 0ddd5b5fe..70d2de0c1 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -255,6 +255,11 @@ namespace storm {
// Start by copying the requirements of the linear equation solver.
MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements());
+ // In case we perform value iteration and need to retrieve a scheduler, end components are forbidden
+ if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && isTrackSchedulerSet()) {
+ requirements.requireNoEndComponents();
+ }
+
// Guide requirements by whether or not we force soundness.
if (this->getSettings().getForceSoundness()) {
// Only add requirements for value iteration here as the policy iteration requirements are indifferent
diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
index 2f360f513..0369d301d 100644
--- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
@@ -108,6 +108,21 @@ namespace storm {
StandardMinMaxLinearEquationSolver<ValueType>::clearCache();
}
+
+ template<typename ValueType>
+ MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+
+ MinMaxLinearEquationSolverRequirements requirements;
+
+ // In case we need to retrieve a scheduler, end components are forbidden
+ if (isTrackSchedulerSet()) {
+ requirements.requireNoEndComponents();
+ }
+
+ return requirements;
+ }
+
+
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory<ValueType>(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>()) {
// Intentionally left empty
diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h
index a31ac710b..3e5af458f 100644
--- a/src/storm/solver/LpMinMaxLinearEquationSolver.h
+++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h
@@ -18,6 +18,8 @@ namespace storm {
virtual void clearCache() const override;
+ virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
+
private:
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;
};
From 96f45fe77a28faa03cdc88c55d39aef7c1f19075 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 28 Sep 2017 12:15:54 +0200
Subject: [PATCH 06/39] fixed missing return statements
---
src/storm/settings/modules/EigenEquationSolverSettings.cpp | 1 +
src/storm/settings/modules/NativeEquationSolverSettings.cpp | 1 +
2 files changed, 2 insertions(+)
diff --git a/src/storm/settings/modules/EigenEquationSolverSettings.cpp b/src/storm/settings/modules/EigenEquationSolverSettings.cpp
index 3047a13a4..e43bda28b 100644
--- a/src/storm/settings/modules/EigenEquationSolverSettings.cpp
+++ b/src/storm/settings/modules/EigenEquationSolverSettings.cpp
@@ -113,6 +113,7 @@ namespace storm {
case EigenEquationSolverSettings::LinearEquationMethod::DGMRES: out << "dgmres"; break;
case EigenEquationSolverSettings::LinearEquationMethod::SparseLU: out << "sparselu"; break;
}
+ return out;
}
} // namespace modules
diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp
index d797a968a..d85b10569 100644
--- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp
+++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp
@@ -120,6 +120,7 @@ namespace storm {
case NativeEquationSolverSettings::LinearEquationMethod::WalkerChae: out << "walkerchae"; break;
case NativeEquationSolverSettings::LinearEquationMethod::Power: out << "power"; break;
}
+ return out;
}
} // namespace modules
From f83dbf741bd8011052363908931bb7b1acb5b901 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 2 Oct 2017 12:02:45 +0200
Subject: [PATCH 07/39] fixed wrong template argument
---
.../region/SparseDtmcParameterLiftingModelChecker.cpp | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index 150a9d86c..8ac2bdea8 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -258,16 +258,16 @@ namespace storm {
solver->setUpperBound(upperResultBound.get());
} else if (solvingRequiresUpperRewardBounds) {
// For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17).
- std::vector<typename SparseModelType::ValueType> oneStepProbs;
+ std::vector<ConstantType> oneStepProbs;
oneStepProbs.reserve(parameterLifter->getMatrix().getRowCount());
for (uint64_t row = 0; row < parameterLifter->getMatrix().getRowCount(); ++row) {
- oneStepProbs.push_back(storm::utility::one<typename SparseModelType::ValueType>() - parameterLifter->getMatrix().getRowSum(row));
+ oneStepProbs.push_back(storm::utility::one<ConstantType>() - parameterLifter->getMatrix().getRowSum(row));
}
if (dirForParameters == storm::OptimizationDirection::Minimize) {
- storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<typename SparseModelType::ValueType> dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+ storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<ConstantType> dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
solver->setUpperBounds(dsmpi.computeUpperBounds());
} else {
- storm::modelchecker::helper::BaierUpperRewardBoundsComputer<typename SparseModelType::ValueType> baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+ storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ConstantType> baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
solver->setUpperBound(baier.computeUpperBound());
}
}
From 20960d56e7ca05078694e2705d0d12e09b2d39c5 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 2 Oct 2017 12:05:39 +0200
Subject: [PATCH 08/39] added missing 'this->'. Also avoid in-place matrix
vector multiplication when extracting a scheduler
---
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp | 4 ++--
src/storm/solver/LpMinMaxLinearEquationSolver.cpp | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index 70d2de0c1..a44024125 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -256,7 +256,7 @@ namespace storm {
MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements());
// In case we perform value iteration and need to retrieve a scheduler, end components are forbidden
- if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && isTrackSchedulerSet()) {
+ if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && this->isTrackSchedulerSet()) {
requirements.requireNoEndComponents();
}
@@ -380,7 +380,7 @@ namespace storm {
// If requested, we store the scheduler for retrieval.
if (this->isTrackSchedulerSet()) {
this->schedulerChoices = std::vector<uint_fast64_t>(this->A->getRowGroupCount());
- this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *currentX, &this->schedulerChoices.get());
+ this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *auxiliaryRowGroupVector.get(), &this->schedulerChoices.get());
}
if (!this->isCachingEnabled()) {
diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
index 0369d301d..024bcf260 100644
--- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
@@ -115,7 +115,7 @@ namespace storm {
MinMaxLinearEquationSolverRequirements requirements;
// In case we need to retrieve a scheduler, end components are forbidden
- if (isTrackSchedulerSet()) {
+ if (this->isTrackSchedulerSet()) {
requirements.requireNoEndComponents();
}
From 765890f3f228915b651afcc43eabc7843c605768 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 2 Oct 2017 12:11:05 +0200
Subject: [PATCH 09/39] Moved dockerfiles to own repository
---
travis/dockerfiles/Dockerfile.debian-9 | 16 ----------------
travis/dockerfiles/Dockerfile.storm | 8 --------
travis/dockerfiles/Dockerfile.ubuntu-16.10 | 17 -----------------
travis/dockerfiles/build_carl.sh | 9 ---------
travis/dockerfiles/build_docker.sh | 9 ---------
travis/dockerfiles/build_storm.sh | 9 ---------
6 files changed, 68 deletions(-)
delete mode 100644 travis/dockerfiles/Dockerfile.debian-9
delete mode 100644 travis/dockerfiles/Dockerfile.storm
delete mode 100644 travis/dockerfiles/Dockerfile.ubuntu-16.10
delete mode 100755 travis/dockerfiles/build_carl.sh
delete mode 100755 travis/dockerfiles/build_docker.sh
delete mode 100755 travis/dockerfiles/build_storm.sh
diff --git a/travis/dockerfiles/Dockerfile.debian-9 b/travis/dockerfiles/Dockerfile.debian-9
deleted file mode 100644
index 3735b38fd..000000000
--- a/travis/dockerfiles/Dockerfile.debian-9
+++ /dev/null
@@ -1,16 +0,0 @@
-FROM debian:9
-MAINTAINER Matthias Volk <matthias.volk@cs.rwth-aachen.de>
-
-RUN apt-get update -qq && apt-get install -y --no-install-recommends \
- build-essential \
- ruby \
- git \
- cmake \
- libboost-all-dev \
- libcln-dev \
- libeigen3-dev \
- libgmp-dev \
- libginac-dev \
- automake \
- libglpk-dev \
- libz3-dev
diff --git a/travis/dockerfiles/Dockerfile.storm b/travis/dockerfiles/Dockerfile.storm
deleted file mode 100644
index 272b97825..000000000
--- a/travis/dockerfiles/Dockerfile.storm
+++ /dev/null
@@ -1,8 +0,0 @@
-FROM mvolk/storm-basesystem:ubuntu-16.10
-MAINTAINER Matthias Volk <matthias.volk@cs.rwth-aachen.de>
-
-COPY build_carl.sh /opt
-RUN cd opt && ./build_carl.sh
-
-COPY build_storm.sh /opt
-RUN cd opt && ./build_storm.sh
diff --git a/travis/dockerfiles/Dockerfile.ubuntu-16.10 b/travis/dockerfiles/Dockerfile.ubuntu-16.10
deleted file mode 100644
index a612faccb..000000000
--- a/travis/dockerfiles/Dockerfile.ubuntu-16.10
+++ /dev/null
@@ -1,17 +0,0 @@
-FROM ubuntu:16.10
-MAINTAINER Matthias Volk <matthias.volk@cs.rwth-aachen.de>
-
-RUN apt-get update -qq && apt-get install -y --no-install-recommends \
- build-essential \
- ruby \
- git \
- cmake \
- libboost-all-dev \
- libcln-dev \
- libeigen3-dev \
- libgmp-dev \
- libginac-dev \
- automake \
- libglpk-dev \
- libhwloc-dev \
- libz3-dev
diff --git a/travis/dockerfiles/build_carl.sh b/travis/dockerfiles/build_carl.sh
deleted file mode 100755
index fc3d43d22..000000000
--- a/travis/dockerfiles/build_carl.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/bash
-echo "Building Carl..."
-git clone https://github.com/smtrat/carl.git
-cd carl
-mkdir build
-cd build
-cmake .. -DCMAKE_BUILD_TYPE=Release -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON
-make lib_carl -j2
-echo "Building Carl finished"
diff --git a/travis/dockerfiles/build_docker.sh b/travis/dockerfiles/build_docker.sh
deleted file mode 100755
index 280710566..000000000
--- a/travis/dockerfiles/build_docker.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/bash
-
-# Build Ubuntu 16.10 "Yakkety Yak"
-docker build -t mvolk/storm-basesystem:ubuntu-16.10 -f Dockerfile.ubuntu-16.10 .
-docker push mvolk/storm-basesystem:ubuntu-16.10
-
-# Build Debian 9 "Stretch"
-docker build -t mvolk/storm-basesystem:debian-9 -f Dockerfile.debian-9 .
-docker push mvolk/storm-basesystem:debian-9
diff --git a/travis/dockerfiles/build_storm.sh b/travis/dockerfiles/build_storm.sh
deleted file mode 100755
index 4c11b708d..000000000
--- a/travis/dockerfiles/build_storm.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/bash
-echo "Building Storm..."
-git clone https://github.com/moves-rwth/storm.git
-cd storm
-mkdir build
-cd build
-cmake .. -DCMAKE_BUILD_TYPE=Release
-make storm storm-dft storm-pars -j1
-echo "Building Storm finished"
From bc0e432e116705dab6a508ca29a7b82ac8c645bc Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 2 Oct 2017 14:17:24 +0200
Subject: [PATCH 10/39] Changed compilers in travis
---
.travis.yml | 74 +++++++++++++++++++--------------------
travis/build-helper.sh | 51 +++++----------------------
travis/generate_travis.py | 6 ++--
travis/install_linux.sh | 2 +-
travis/install_osx.sh | 19 ++++------
5 files changed, 56 insertions(+), 96 deletions(-)
diff --git a/.travis.yml b/.travis.yml
index 2b5f50657..697118347 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -7,6 +7,7 @@ branches:
only:
- master
- stable
+sudo: required
dist: trusty
language: cpp
@@ -20,7 +21,6 @@ cache:
# Enable docker support
services:
- docker
-sudo: required
notifications:
email:
@@ -42,8 +42,8 @@ jobs:
# osx
- stage: Build (1st run)
os: osx
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
install:
- rm -rf build
- travis/install_osx.sh
@@ -53,8 +53,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Build (1st run)
os: osx
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
install:
- rm -rf build
- travis/install_osx.sh
@@ -66,7 +66,7 @@ jobs:
- stage: Build (1st run)
os: linux
compiler: gcc
- env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
install:
- rm -rf build
- travis/install_linux.sh
@@ -79,7 +79,7 @@ jobs:
- stage: Build (1st run)
os: linux
compiler: gcc
- env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
install:
- rm -rf build
- travis/install_linux.sh
@@ -97,8 +97,8 @@ jobs:
# osx
- stage: Build (2nd run)
os: osx
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -107,8 +107,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Build (2nd run)
os: osx
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -119,7 +119,7 @@ jobs:
- stage: Build (2nd run)
os: linux
compiler: gcc
- env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
install:
- travis/install_linux.sh
script:
@@ -131,7 +131,7 @@ jobs:
- stage: Build (2nd run)
os: linux
compiler: gcc
- env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
install:
- travis/install_linux.sh
script:
@@ -148,8 +148,8 @@ jobs:
# osx
- stage: Build (3rd run)
os: osx
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -158,8 +158,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Build (3rd run)
os: osx
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -170,7 +170,7 @@ jobs:
- stage: Build (3rd run)
os: linux
compiler: gcc
- env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
install:
- travis/install_linux.sh
script:
@@ -182,7 +182,7 @@ jobs:
- stage: Build (3rd run)
os: linux
compiler: gcc
- env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
install:
- travis/install_linux.sh
script:
@@ -199,8 +199,8 @@ jobs:
# osx
- stage: Build (4th run)
os: osx
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -209,8 +209,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Build (4th run)
os: osx
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -221,7 +221,7 @@ jobs:
- stage: Build (4th run)
os: linux
compiler: gcc
- env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
install:
- travis/install_linux.sh
script:
@@ -233,7 +233,7 @@ jobs:
- stage: Build (4th run)
os: linux
compiler: gcc
- env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
install:
- travis/install_linux.sh
script:
@@ -250,8 +250,8 @@ jobs:
# osx
- stage: Build (5th run)
os: osx
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -260,8 +260,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Build (5th run)
os: osx
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -272,7 +272,7 @@ jobs:
- stage: Build (5th run)
os: linux
compiler: gcc
- env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
install:
- travis/install_linux.sh
script:
@@ -284,7 +284,7 @@ jobs:
- stage: Build (5th run)
os: linux
compiler: gcc
- env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
install:
- travis/install_linux.sh
script:
@@ -301,8 +301,8 @@ jobs:
# osx
- stage: Test all
os: osx
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -311,8 +311,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Test all
os: osx
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang-4.0 STL=libc++
+ compiler: apple-clang
+ env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -323,7 +323,7 @@ jobs:
- stage: Test all
os: linux
compiler: gcc
- env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
install:
- travis/install_linux.sh
script:
@@ -335,7 +335,7 @@ jobs:
- stage: Test all
os: linux
compiler: gcc
- env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc-6
+ env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
install:
- travis/install_linux.sh
script:
diff --git a/travis/build-helper.sh b/travis/build-helper.sh
index 8d73c87e7..5e1b589e3 100755
--- a/travis/build-helper.sh
+++ b/travis/build-helper.sh
@@ -66,57 +66,17 @@ run() {
export PATH="/usr/local/opt/coreutils/libexec/gnubin:$PATH"
case $COMPILER in
-gcc-4.8)
- export CC=gcc-4.8
- export CXX=g++-4.8
- ;;
-
-gcc-4.9)
- export CC=gcc-4.9
- export CXX=g++-4.9
- ;;
-
-gcc-5)
- export CC=gcc-5
- export CXX=g++-5
- ;;
-
gcc-6)
export CC=gcc-6
export CXX=g++-6
;;
-gcc-default)
+gcc)
export CC=gcc
export CXX=g++
;;
-clang-3.5)
- export CC=clang-3.5
- export CXX=clang++-3.5
- ;;
-
-clang-3.6)
- export CC=clang-3.6
- export CXX=clang++-3.6
- ;;
-
-clang-3.7)
- export CC=clang-3.7
- export CXX=clang++-3.7
- ;;
-
-clang-3.8)
- export CC=clang-3.8
- export CXX=clang++-3.8
- ;;
-
-clang-3.9)
- export CC=clang-3.9
- export CXX=clang++-3.9
- ;;
-
-clang-4.0)
+clang-4)
case "$OS" in
linux)
export CC=clang-4.0
@@ -130,7 +90,12 @@ clang-4.0)
esac
;;
-clang-default)
+clang)
+ export CC=clang
+ export CXX=clang++
+ ;;
+
+apple-clang)
export CC=clang
export CXX=clang++
;;
diff --git a/travis/generate_travis.py b/travis/generate_travis.py
index 14e058a85..9fe6f82d0 100644
--- a/travis/generate_travis.py
+++ b/travis/generate_travis.py
@@ -2,14 +2,14 @@
# Configuration for Linux
configs_linux = [
# OS, compiler
- ("ubuntu-16.10", "gcc", "-6"),
+ ("ubuntu-16.10", "gcc", ""),
#("debian-9", "gcc", "-6"),
]
# Configurations for Mac
configs_mac = [
# OS, compiler
- ("osx", "clang", "-4.0"),
+ ("osx", "apple-clang", ""),
]
# Build types
@@ -41,6 +41,7 @@ if __name__ == "__main__":
s += " only:\n"
s += " - master\n"
s += " - stable\n"
+ s += "sudo: required\n"
s += "dist: trusty\n"
s += "language: cpp\n"
s += "\n"
@@ -54,7 +55,6 @@ if __name__ == "__main__":
s += "# Enable docker support\n"
s += "services:\n"
s += "- docker\n"
- s += "sudo: required\n"
s += "\n"
s += "notifications:\n"
diff --git a/travis/install_linux.sh b/travis/install_linux.sh
index c7ef04886..62a7d75f6 100755
--- a/travis/install_linux.sh
+++ b/travis/install_linux.sh
@@ -8,4 +8,4 @@ then
exit 0
fi
-sudo apt-get install -qq -y docker
+#sudo apt-get install -qq -y docker
diff --git a/travis/install_osx.sh b/travis/install_osx.sh
index 8d703a82a..e7fea4dec 100755
--- a/travis/install_osx.sh
+++ b/travis/install_osx.sh
@@ -18,8 +18,7 @@ install_brew_package() {
brew outdated "$1" || brew upgrade "$@"
else
# Package not installed yet, install.
- # If there are conflicts, try overwriting the files (these are in /usr/local anyway so it should be ok).
- brew install "$@" || brew link --overwrite gcc49
+ brew install "$@" || brew link --overwrite "$@"
fi
}
@@ -40,19 +39,15 @@ install_brew_package md5sha1sum
# For `timeout'
install_brew_package coreutils
-which cmake &>/dev/null || install_brew_package cmake
+install_brew_package cmake
# Install compiler
case "${COMPILER}" in
-gcc-4.8) install_brew_package gcc@4.8 ;;
-gcc-4.9) install_brew_package gcc@4.9 ;;
-gcc-5) install_brew_package gcc@5 ;;
-gcc-6) install_brew_package gcc@6 ;;
-clang-default) ;;
-clang-3.7) install_brew_package llvm@3.7 --with-clang --with-libcxx;;
-clang-3.8) install_brew_package llvm@3.8 --with-clang --with-libcxx;;
-clang-3.9) install_brew_package llvm@3.9 --with-clang --with-libcxx;;
-clang-4.0) install_brew_package llvm --with-clang --with-libcxx;;
+gcc) install_brew_package gcc ;;
+gcc-6) install_brew_package gcc@6 ;;
+clang) install_brew_package llvm --with-clang --with-libcxx;;
+clang-4) install_brew_package llvm@4 --with-clang --with-libcxx;;
+apple-clang) ;;
*) echo "Compiler not supported: ${COMPILER}. See travis/install_osx.sh"; exit 1 ;;
esac
travis_fold end brew_install_util
From ba9534da0a5f8073ee915b1a53a1d7e281830976 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 2 Oct 2017 14:36:34 +0200
Subject: [PATCH 11/39] apple-clang was not recognized in travis
---
.travis.yml | 48 +++++++++++++++++++--------------------
travis/build-helper.sh | 5 ----
travis/generate_travis.py | 2 +-
travis/install_osx.sh | 3 +--
4 files changed, 26 insertions(+), 32 deletions(-)
diff --git a/.travis.yml b/.travis.yml
index 697118347..ee40491cb 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -42,8 +42,8 @@ jobs:
# osx
- stage: Build (1st run)
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
install:
- rm -rf build
- travis/install_osx.sh
@@ -53,8 +53,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Build (1st run)
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
install:
- rm -rf build
- travis/install_osx.sh
@@ -97,8 +97,8 @@ jobs:
# osx
- stage: Build (2nd run)
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -107,8 +107,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Build (2nd run)
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -148,8 +148,8 @@ jobs:
# osx
- stage: Build (3rd run)
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -158,8 +158,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Build (3rd run)
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -199,8 +199,8 @@ jobs:
# osx
- stage: Build (4th run)
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -209,8 +209,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Build (4th run)
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -250,8 +250,8 @@ jobs:
# osx
- stage: Build (5th run)
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -260,8 +260,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Build (5th run)
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -301,8 +301,8 @@ jobs:
# osx
- stage: Test all
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultDebug COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
install:
- travis/install_osx.sh
script:
@@ -311,8 +311,8 @@ jobs:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- stage: Test all
os: osx
- compiler: apple-clang
- env: CONFIG=DefaultRelease COMPILER=apple-clang STL=libc++
+ compiler: clang
+ env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
install:
- travis/install_osx.sh
script:
diff --git a/travis/build-helper.sh b/travis/build-helper.sh
index 5e1b589e3..7d722dc99 100755
--- a/travis/build-helper.sh
+++ b/travis/build-helper.sh
@@ -95,11 +95,6 @@ clang)
export CXX=clang++
;;
-apple-clang)
- export CC=clang
- export CXX=clang++
- ;;
-
*)
echo "Unrecognized value of COMPILER: $COMPILER"
exit 1
diff --git a/travis/generate_travis.py b/travis/generate_travis.py
index 9fe6f82d0..13d91e691 100644
--- a/travis/generate_travis.py
+++ b/travis/generate_travis.py
@@ -9,7 +9,7 @@ configs_linux = [
# Configurations for Mac
configs_mac = [
# OS, compiler
- ("osx", "apple-clang", ""),
+ ("osx", "clang", ""),
]
# Build types
diff --git a/travis/install_osx.sh b/travis/install_osx.sh
index e7fea4dec..e308372de 100755
--- a/travis/install_osx.sh
+++ b/travis/install_osx.sh
@@ -45,9 +45,8 @@ install_brew_package cmake
case "${COMPILER}" in
gcc) install_brew_package gcc ;;
gcc-6) install_brew_package gcc@6 ;;
-clang) install_brew_package llvm --with-clang --with-libcxx;;
+clang) ;;
clang-4) install_brew_package llvm@4 --with-clang --with-libcxx;;
-apple-clang) ;;
*) echo "Compiler not supported: ${COMPILER}. See travis/install_osx.sh"; exit 1 ;;
esac
travis_fold end brew_install_util
From 57065bdabd25dd9fe1b0118a2139f8ec6ea0a63a Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 2 Oct 2017 15:27:59 +0200
Subject: [PATCH 12/39] glpk and hwloc now in homebrew/core
---
travis/install_osx.sh | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/travis/install_osx.sh b/travis/install_osx.sh
index e308372de..89e155730 100755
--- a/travis/install_osx.sh
+++ b/travis/install_osx.sh
@@ -60,8 +60,7 @@ install_brew_package ginac
install_brew_package doxygen
install_brew_package boost --c++11
install_brew_package z3 # optional
-brew tap homebrew/science
-install_brew_package homebrew/science/glpk
-install_brew_package homebrew/science/hwloc
+install_brew_package glpk
+install_brew_package hwloc
install_brew_package eigen
travis_fold end brew_install_dependencies
From 4626aa0e69024732749d0667c7b11d37181a218c Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 2 Oct 2017 17:44:01 +0200
Subject: [PATCH 13/39] Updated search for mathsat in cmake and fixed linker
problem
---
resources/3rdparty/CMakeLists.txt | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 3a8a99435..cb7e064ec 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -395,9 +395,9 @@ endif()
set(STORM_HAVE_MSAT ${ENABLE_MSAT})
if (ENABLE_MSAT)
message (STATUS "Storm - Linking with MathSAT.")
- link_directories("${MSAT_ROOT}/lib")
- include_directories("${MSAT_ROOT}/include")
- list(APPEND STORM_LINK_LIBRARIES "mathsat")
+ find_library(MSAT_LIB mathsat PATHS "${MSAT_ROOT}/lib")
+ add_imported_library(msat SHARED ${MSAT_LIB} "${MSAT_ROOT}/include")
+ list(APPEND STORM_DEP_TARGETS msat_SHARED)
endif(ENABLE_MSAT)
#############################################################
From fcf3d984fb30bfb4b07737c20fcbb37befb0b9a7 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 3 Oct 2017 13:09:05 +0200
Subject: [PATCH 14/39] 5th build stage in travis seems not to be needed
anymore
---
.travis.yml | 57 +++------------------------------------
travis/generate_travis.py | 3 +--
2 files changed, 4 insertions(+), 56 deletions(-)
diff --git a/.travis.yml b/.travis.yml
index ee40491cb..a9b1577af 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -198,57 +198,6 @@ jobs:
# osx
- stage: Build (4th run)
- os: osx
- compiler: clang
- env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
- install:
- - travis/install_osx.sh
- script:
- - travis/build.sh Build4
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
- - stage: Build (4th run)
- os: osx
- compiler: clang
- env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
- install:
- - travis/install_osx.sh
- script:
- - travis/build.sh Build4
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
- # ubuntu-16.10
- - stage: Build (4th run)
- os: linux
- compiler: gcc
- env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
- install:
- - travis/install_linux.sh
- script:
- - travis/build.sh Build4
- before_cache:
- - docker cp storm:/storm/. .
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
- - stage: Build (4th run)
- os: linux
- compiler: gcc
- env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
- install:
- - travis/install_linux.sh
- script:
- - travis/build.sh Build4
- before_cache:
- - docker cp storm:/storm/. .
- after_failure:
- - find build -iname '*err*.log' -type f -print -exec cat {} \;
-
- ###
- # Stage: Build (5th run)
- ###
-
- # osx
- - stage: Build (5th run)
os: osx
compiler: clang
env: CONFIG=DefaultDebug COMPILER=clang STL=libc++
@@ -258,7 +207,7 @@ jobs:
- travis/build.sh BuildLast
after_failure:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- - stage: Build (5th run)
+ - stage: Build (4th run)
os: osx
compiler: clang
env: CONFIG=DefaultRelease COMPILER=clang STL=libc++
@@ -269,7 +218,7 @@ jobs:
after_failure:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
# ubuntu-16.10
- - stage: Build (5th run)
+ - stage: Build (4th run)
os: linux
compiler: gcc
env: CONFIG=DefaultDebug LINUX=ubuntu-16.10 COMPILER=gcc
@@ -281,7 +230,7 @@ jobs:
- docker cp storm:/storm/. .
after_failure:
- find build -iname '*err*.log' -type f -print -exec cat {} \;
- - stage: Build (5th run)
+ - stage: Build (4th run)
os: linux
compiler: gcc
env: CONFIG=DefaultRelease LINUX=ubuntu-16.10 COMPILER=gcc
diff --git a/travis/generate_travis.py b/travis/generate_travis.py
index 13d91e691..9b86cd19a 100644
--- a/travis/generate_travis.py
+++ b/travis/generate_travis.py
@@ -23,8 +23,7 @@ stages = [
("Build (1st run)", "Build1"),
("Build (2nd run)", "Build2"),
("Build (3rd run)", "Build3"),
- ("Build (4th run)", "Build4"),
- ("Build (5th run)", "BuildLast"),
+ ("Build (4th run)", "BuildLast"),
("Test all", "TestAll"),
]
From 20a76f01e272390580f34345b85a27122f9c9544 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 5 Oct 2017 11:19:25 +0200
Subject: [PATCH 15/39] Better error output for jit
---
src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 54779b96a..245e9d54d 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -3,6 +3,7 @@
#include <iostream>
#include <cstdio>
#include <chrono>
+#include <errno.h>
#include "storm/solver/SmtSolver.h"
@@ -163,7 +164,7 @@ namespace storm {
STORM_LOG_TRACE("Executing command: " << command);
std::unique_ptr<FILE> pipe(popen(command.c_str(), "r"));
- STORM_LOG_THROW(pipe, storm::exceptions::InvalidStateException, "Call to popen failed.");
+ STORM_LOG_THROW(pipe, storm::exceptions::InvalidStateException, "Call to popen failed: " << strerror(errno));
while (!feof(pipe.get())) {
if (fgets(buffer, 128, pipe.get()) != nullptr)
From 384f17e32ec7c1bb5cb81c52ba97f846dd8e5d39 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 5 Oct 2017 17:09:18 +0200
Subject: [PATCH 16/39] Workaround for jit and sylvan tests on travis
---
travis/build-helper.sh | 8 +++++++-
1 file changed, 7 insertions(+), 1 deletion(-)
diff --git a/travis/build-helper.sh b/travis/build-helper.sh
index 7d722dc99..04c2dc52e 100755
--- a/travis/build-helper.sh
+++ b/travis/build-helper.sh
@@ -50,7 +50,13 @@ run() {
# Test all
travis_fold start test_all
cd build
- ctest test --output-on-failure
+ # Hack to avoid memout problem with jit and sylvan
+ # 1. Run other tests without builder tests
+ ctest test --output-on-failure -E run-test-builder
+ # 2. Run builder tests without sylvan tests
+ ./bin/test-builder --gtest_filter=-"DdJaniModelBuilderTest_Sylvan.*"
+ # 3. Just run sylvan tests
+ ./bin/test-builder --gtest_filter="DdJaniModelBuilderTest_Sylvan.*"
travis_fold end test_all
;;
From 6fa4e6b455375fe93d3354dc81ae26ddf5861029 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 6 Oct 2017 15:15:08 +0200
Subject: [PATCH 17/39] fixed SOR and gaussseidel linear equation solver
methods
---
src/storm/storage/SparseMatrix.cpp | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index b37472baf..3eb71960f 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -1493,8 +1493,9 @@ namespace storm {
typename std::vector<ValueType>::iterator resultIterator = x.end() - 1;
typename std::vector<ValueType>::iterator resultIteratorEnd = x.begin() - 1;
- index_type currentRow = 0;
+ index_type currentRow = getRowCount();
for (; resultIterator != resultIteratorEnd; --rowIterator, --resultIterator, --bIt) {
+ --currentRow;
ValueType tmpValue = storm::utility::zero<ValueType>();
ValueType diagonalElement = storm::utility::zero<ValueType>();
@@ -1505,9 +1506,8 @@ namespace storm {
diagonalElement += it->getValue();
}
}
-
+ assert(!storm::utility::isZero(diagonalElement));
*resultIterator = ((storm::utility::one<ValueType>() - omega) * *resultIterator) + (omega / diagonalElement) * (*bIt - tmpValue);
- ++currentRow;
}
}
From e5387ecc85bc1e0c03c5cc617da4a4cc62f11f16 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 6 Oct 2017 16:31:26 +0200
Subject: [PATCH 18/39] Deactivated conversion to CTMC for trivial
non-determinism in MA as it is not correct at the moment
---
src/storm-cli-utilities/model-handling.h | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index fd2b3d3a3..9b45f08c9 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -232,7 +232,9 @@ namespace storm {
std::shared_ptr<storm::models::sparse::Model<ValueType>> result = model;
model->close();
if (model->hasOnlyTrivialNondeterminism()) {
- result = model->convertToCTMC();
+ STORM_LOG_WARN_COND(false, "Non-deterministic choices in MA seem to be unnecessary. Consider using a CTMC instead.");
+ // Activate again if transformation is correct
+ //result = model->convertToCTMC();
}
return result;
}
From 026cb3dfdf7b6955393c8d19bc14229bf30c2345 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 6 Oct 2017 16:32:00 +0200
Subject: [PATCH 19/39] Small change in travis generation
---
travis/generate_travis.py | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/travis/generate_travis.py b/travis/generate_travis.py
index 9b86cd19a..508568a34 100644
--- a/travis/generate_travis.py
+++ b/travis/generate_travis.py
@@ -3,7 +3,7 @@
configs_linux = [
# OS, compiler
("ubuntu-16.10", "gcc", ""),
- #("debian-9", "gcc", "-6"),
+ #("debian-9", "gcc", ""),
]
# Configurations for Mac
From 94788dbd747eafcbc9e717d4b420bfc64a8a6375 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 6 Oct 2017 16:37:35 +0200
Subject: [PATCH 20/39] Removed old files
---
.gitmodules | 3 -
Jenkinsfile | 44 ---------------
doc/build.md | 37 -------------
doc/dependencies.md | 37 -------------
doc/getting-started.md | 1 -
install.sh | 2 -
util/astyle/options.astyle | 34 ------------
util/checklist/storage.ods | Bin 18701 -> 0 bytes
util/osx-package/package.sh | 10 ----
util/osx-package/packager.py | 103 -----------------------------------
10 files changed, 271 deletions(-)
delete mode 100644 .gitmodules
delete mode 100644 Jenkinsfile
delete mode 100644 doc/build.md
delete mode 100644 doc/dependencies.md
delete mode 100644 doc/getting-started.md
delete mode 100755 install.sh
delete mode 100644 util/astyle/options.astyle
delete mode 100644 util/checklist/storage.ods
delete mode 100644 util/osx-package/package.sh
delete mode 100644 util/osx-package/packager.py
diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index 92b35f18f..000000000
--- a/.gitmodules
+++ /dev/null
@@ -1,3 +0,0 @@
-[submodule "resources/3rdparty/cusplibrary"]
- path = resources/3rdparty/cusplibrary
- url = https://github.com/cusplibrary/cusplibrary.git
diff --git a/Jenkinsfile b/Jenkinsfile
deleted file mode 100644
index fd321e147..000000000
--- a/Jenkinsfile
+++ /dev/null
@@ -1,44 +0,0 @@
-node {
- def cmakeTool
- stage('Preparation') {
- // Get some code from a GitHub repository
- checkout scm
-
- cmakeTool = tool name: 'InSearchPath', type: 'hudson.plugins.cmake.CmakeTool'
-
- sh "rm -rf build"
- sh "mkdir -p build"
- }
- stage('Configure') {
- dir("build") {
- sh "${cmakeTool} .."
- }
-
- }
-
- stage('Build') {
- dir("build") {
- sh "make storm"
- }
-
- }
-
- stage('Build Tests') {
- dir("build") {
- sh "make -j 4 tests"
- }
-
- }
-
- stage('Test') {
- dir("build") {
- sh "make check-verbose"
- }
- }
-
- stage('Archive') {
- archiveArtifacts artifacts: 'build/bin/*', onlyIfSuccessful: true
- archiveArtifacts artifacts: 'build/lib/*', onlyIfSuccessful: true
- archiveArtifacts artifacts: 'build/include/*', onlyIfSuccessful: true
- }
-}
diff --git a/doc/build.md b/doc/build.md
deleted file mode 100644
index 725794034..000000000
--- a/doc/build.md
+++ /dev/null
@@ -1,37 +0,0 @@
-# Building Storm
-
-
-## Requirements
-CMake >= 3.2
- CMake is required as it is used to generate the Makefiles or Projects/Solutions required to build StoRM.
-
-### Compiler:
- A C++11 compliant compiler is required to build StoRM. It is tested and known to work with the following compilers:
- - GCC 5.3
- - Clang 3.5.0
-
- Other versions or compilers might work, but are not tested.
-
- The following Compilers are known NOT to work:
- - Microsoft Visual Studio versions older than 2013,
- - GCC versions 4.9.1 and older.
-
-Prerequisites:
- Boost >= 1.61
- Build using the Boost Build system, for x64 use "bjam address-model=64" or "bjam.exe address-model=64 --build-type=complete"
-
-## Instructions
-
-### General
-
-```bash
-mkdir build
-cd build
-```
-
-It is recommended to make an out-of-source build, meaning that the folder in which CMake generates its Cache, Makefiles and output files should not be the Project Root nor its Source Directory.
-A typical build layout is to create a folder "build" in the project root alongside the CMakeLists.txt file, change into this folder and execute "cmake .." as this will leave all source files untouched
-and makes cleaning up the build tree very easy.
-There are several options available for the CMake Script as to control behaviour and included components.
-If no error occured during the last CMake Configure round, press Generate.
-Now you can build StoRM using the generated project/makefiles in the Build folder you selected.
\ No newline at end of file
diff --git a/doc/dependencies.md b/doc/dependencies.md
deleted file mode 100644
index 34660fdc0..000000000
--- a/doc/dependencies.md
+++ /dev/null
@@ -1,37 +0,0 @@
-# Dependencies
-
-## Included Dependencies:
-- Carl 1.0
-- CUDD 3.0.0
- CUDD is included in the StoRM Sources under /resources/3rdparty/cudd-2.5.0 and builds automatically alongside StoRM.
- Its Sourced where heavily modified as to incorporate newer Versions of Boost, changes in C++ (TR1 to C++11) and
- to remove components only available under UNIX.
-- Eigen 3.3 beta1
- Eigen is included in the StoRM Sources under /resources/3rdparty/eigen and builds automatically alongside StoRM.
-
-
-- GTest 1.7.0
- GTest is included in the StoRM Sources under /resources/3rdparty/gtest-1.7.0 and builds automatically alongside StoRM
-- GMM >= 4.2
- GMM is included in the StoRM Sources under /resources/3rdparty/gmm-4.2 and builds automatically alongside StoRM.
-
-## Optional:
-- Gurobi >= 5.6.2
- Specify the path to the gurobi root dir using -DGUROBI_ROOT=/your/path/to/gurobi
-- Z3 >= 4.3.2
- Specify the path to the z3 root dir using -DZ3_ROOT=/your/path/to/z3
-- MathSAT >= 5.2.11
- Specify the path to the mathsat root dir using -DMSAT_ROOT=/your/path/to/mathsat
-- MPIR >= 2.7.0
- MSVC only and only if linked with MathSAT
- Specify the path to the gmp-include directory -DGMP_INCLUDE_DIR=/your/path/to/mathsat
- Specify the path to the mpir.lib directory -DGMP_MPIR_LIBRARY=/your/path/to/mpir.lib
- Specify the path to the mpirxx.lib directory -DGMP_MPIRXX_LIBRARY=/your/path/to/mpirxx.lib
-- GMP
- clang and gcc only
-- CUDA Toolkit >= 6.5
- Specify the path to the cuda toolkit root dir using -DCUDA_ROOT=/your/path/to/cuda
-- CUSP >= 0.4.0
- Only of built with CUDA Toolkit
- CUSP is included in the StoRM Sources as a git-submodule unter /resources/3rdparty/cusplibrary
-
diff --git a/doc/getting-started.md b/doc/getting-started.md
deleted file mode 100644
index 8b1378917..000000000
--- a/doc/getting-started.md
+++ /dev/null
@@ -1 +0,0 @@
-
diff --git a/install.sh b/install.sh
deleted file mode 100755
index 384bbb2e9..000000000
--- a/install.sh
+++ /dev/null
@@ -1,2 +0,0 @@
-#!/bin/bash
-pip install -ve stormpy
diff --git a/util/astyle/options.astyle b/util/astyle/options.astyle
deleted file mode 100644
index 5f02d356d..000000000
--- a/util/astyle/options.astyle
+++ /dev/null
@@ -1,34 +0,0 @@
-# Select overall style.
---style=google
---mode=c
---recursive
-
-# Attach brackets to namespaces and classes.
---attach-namespaces
---attach-classes
-
-# Of course, namespaces should also be indented.
---indent-namespaces
-
-# C++ comments starting in column 1 are also supposed to be indented properly.
---indent-col1-comments
-
-# Add space padding around operators.
---pad-oper
-
-# Put the pointer/reference operators next to the variable.
---align-pointer=type
-
-# Add brackets to conditional one-line statements.
---add-brackets
-
-# Convert tabs to spaces in non-indentation part of the line as well.
---convert-tabs
-
-# Remove spaces in definition of C++ templates.
---close-templates
-
-# Don't let lines get too long.
---max-code-length=140
-
---verbose
diff --git a/util/checklist/storage.ods b/util/checklist/storage.ods
deleted file mode 100644
index d05761496281c3533609fc6a2e759dbb72e6be50..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001
literal 18701
zcmeFZ1#=xS(<XY%%#N8MW@fe%$IKWrvwcj*%p5Z_#>~vjOffS<%*=G1_wKi~w`#ww
z{Q*~1Q=^*Fw50A<Yr56XC`dy<VgdlL0063Q;P)VFo-jrL0Pyend<3wuurUF-*_jyF
z*;!i{8GtNoflSUoV@6v8M+-+rTRRh=v8|DljR_FM=xFC)VqolOZejvb_zz83SlIv2
z{3P=~%YSH^fD9O2ZLA~XrES+pFoPc6zF>_kK)-TcbGH?Ti<KmVCg=oiPxe>9h~W&)
z`slr;$)st3j{01<55XBP<U$raU}iZqZBUV5uZ7_l@EbOB4$nHW^V*KJN?h8+0P&i)
zFbWGozWZ5qrBM^o_;dIJ>=$WKG~T{Z8a=mYbCw3l?CJid`*WPf56~SN9>zE*eW-|v
zITJ*)xzv~St+`4WEk?F0p>g2f5sbctSO{N@Mj?GP%?<0S&1hx^h<P#!3<L%CyT0ol
zb;Q<oaQYgNpW-=;y*)q&<L@!->Jhm9D!l^@;i>W@qCq!11zwCR1O<u-B6*?P(wI;f
zNn&9d95+%0COn4aCHQ;Qm`0#t1%XNK(&xrI4IHS%L^@$#jBUtxs0uZWJQTbB3M-=A
zN4Q$1e*cBlO8Xw7yO+8i0B*KW`21%Mny6^mo?w~;zIPRdktkbNSKjSdhrWv_@*S#o
zC*m|`(pb^hpw-dQch4y!F7U8@(ufQloNVMV?gNcOJUiRgOy^~ivo{?yc7o;k+rwl%
zF-HS)y0HxFAiVgbW{?&mungU&RlxI1zT_QTK^g`&D)}k30t^5!g8%^jdl4gk3fs{H
z1hN2{IsOy#nTDd{3OA~EmtN0fCbw`eN0xBN^g*1}iYfER`kibe_O$4NI|c4HpSO`E
z<6lNx`dX>Zh4Q`yZ_XVnZ}n{%T|S5!R&d{x_8`g}LDmhvFE|Q<#6MkT$L{$~-Y%mZ
zGbV~r<b1sez}0Qwq>dPB3kF(1Gy8sD5Y9<rRd_Q3NeK7(aKJXhc-q=BBWrI*$n#ze
z^cfPu2v&6~)Wpj+(85~QdHDG1xXM;51g~*3FUn}wJIdhEvN0*aOIYwt)^~R?_}*+9
zSjk<qXB&dGgsk;^T(f8-gjQ5UQXUHv1>|J#e`*%g<yX63r>RmrXdh%r9kbxTktj!$
zpXF+byT>}1AVp7|C6mB_ZFb9~ioAzFTPi}X^BrYoEd+Og^Xg%yy;rVo;&&3p70bE-
zqEYu$drBW;I9Yky``w8H44eq}$`hpi!d3@M@`I3T*}*23c_>#%t8kySMQJgOkv&AW
zxUtX&7^F%;;ICSHXL17)Zpd$X0W7XT{@&u1u#V(n^Ja)7J^%zv4nu;#+)kR?j5{qD
zj?}!id;D(Vr!Yo?06|hu-JL8T$7Mwa(#-;vvyvDshkg3~1;a5EZID4g_a<sziI@d@
zF2=M+?+(AE7_q8X4lcdHB602moqrpG_8X;nR<nR8bfDIEN<(TfM%QK!y#xl^UtXJY
zD+=BtnQ`_WHs@DRtOsa{?%^&UuY^VoM)Znyzr#~Qw7?`e6tHaBdW{FzWam5~{P17)
zx4}A4-mz5*bIMG%t%l)_ad5*3*!w6#c-OtFRt3(u>?)z#9e(6<3Lrm0s;diwuV>&W
z?l1xp3h^NRE?!%egTBL@^WMftVqd!e$)&XAa%tp#sl*8V{mM!Q)tRKBY$($QnJ;*8
z4c^X*akz~Te%X2nJcR;Dnv^^t`C;Shae$N_|Bxr1r@bKfWq5})(ZSS4)w>2jHhhee
zdZ8l35nPh?h2T^4h|VH7G;*S@xF`x^YQyUw2;;E4b+|z{&r>R*Q{?P;-kqVry~QJp
zhW^yLH;DI>#w0=l-`a&j>sN;ZTg=2*`zuECmC2)^yc9yWW@M22k6wi4<4TKKEUc7k
zR>nhemoLvgSK41Xa?iaUl>L*hOIFX~HN7kb-qv45tM)^ze;ys{)0(B=rQWmLk~Gh$
zdL8}Ht!rghc}ryw(XI`A0ad;vM&n93J~WNMljb!uJ&W&S&OY76%-BCMm#N!hV*ar9
zq7v~W2}>Eyk|%kTu#9SrY^gF-Vjg{lg0DF^j{L5dza4iW3-2+Dl+@CAQ=*S!gaa1?
z_rfj+&$7OnM({NPXVxs;Ze{atB;14FTQ1TqzEif4k&Eg|-4fF~Ps7-|GSNHAKiff@
zqE!tJ2>>J#{hw?H!l&&pvIT<v?I-_Cho*+(DkrM<Mb#EHn^#_OU$V+-DrX1LX{yYw
z@iTlZ9Xtl=79c0;{rUVFohBUKsbBH<S%e7O!}I5<<k9^ZEBYis{kGJG)APFS5ZF<f
z@7QJK&DD|1L*dQ+dx#cCrUUVy-*r4}zLOUv!@En2R+@dI$D(9C0i9_xt~8b(u9i=^
zVGPt_vy_0GlL_5mrKr_?Li4DNfyF8-hD~I$?246KXxW;dX?WwfXt-EKt-Pw%K>^yi
z%J2ES6pc<lLz?DS&&5;?{AdB&nx7!-zRH>3i^P#)x~*E^_tLH0f5-~pJy9TISa<K*
zysB~{yK5UCe>K8Oe*FUpvYKTc%UZWA?;(LBN+zhw%%PQ^=sGa4x=0H_GQBsGX}YgV
zXg;Uy%jqaX44}2`KP}((wrv+*lMx~!Uhpo+Yi#}1XiBSh(|pImc1+u)R2nFSs8L;H
z2h*_;lq{fLjLkQKou)PY#leTFWhzilQ~SqiL@>w;g+@Ciek@r;G?*C)5rS!zF;sS%
z`uSog1mzu(tnurC-dE=q_N0*p6Ly_%yOK--NHsH!?Bn%b*8{6~2}`D&=o2LY&ImIK
zFg<EYfo!+Tk@~1@j>zF$4Qs8d#A3QqDicL~xX%L7=A$wFC%RNVgh_W6rRccE79?!Y
z^hVPejVTh#gB)-T<>Mllzcr6Hze2~h#`dItM^U|M?$wdM=GAP(5Z5j7KPv2xguRQz
zU9rKwx=j}MV4UY3-)Sk7vLObYhkwh0s=OKvqQL^WjC$HZTn4ptO`topoElFBzEs}S
z9Uu}yIGTu{+Sh1SscTpaA&KmWusBcn<16R=YPn-+o4~z}qjP0Y;UlITB7({oLeWxq
z9X2%aUZEIQa|zJGMfk(=H)}~oaZjjE1xQe~Zq-`lnMsNDMdQ4!B;%TFb_!2T?@ro;
zXOtbM<~5WeF4MoR_3z-{<QxW=U72~;Tt6>oDqqGha7iap7An0<U#Z0$K0IxdW*HQP
zo;rlJt%B~m*5nsb{7!<}@bo_u-dl{i@N3np7m?2|er=vSW9w@X_dSK_{vu@q(9GH;
zxucEd_R#zp8dCLrWhbPTn~~fsTcu0azu=li1x<Rp1&8s;_5phxz>iiRFJ_0bcmZFn
z#`V1c!$3ALb1qZTX567FW|Por{G!qfYW!(%pka?1PnI?wM;y0z3z}L$Thw%A=IM6J
zbONnN!X2Y&+SlD%11fz(cW)Gx2A!|2)H-?Svb(nlObFXc=U{Y0=V9>)ts2D|{Hwo`
z8x(jU8@^a&fvV)Pu)g$th^)VrEiG80F|;k|vM$$48pZpXbasT;rz^eDL`X-KgM6dd
z6&GeCND>3(Omw>E1oh@qrEM9tz7&BGX$?{LKpe_4y{#TL%iis-KBE&l_%SAkao&aB
zD%2KR7dxjS9(j!vtDlZbvN-<<O8!AG6xhcfpG02xo$-e6=uA~7r{uQ7x$WGbw-EfT
z3l2ZdloDn^Jnz{(mb*!Y2|v&T-Ak->h(kAXpToN&V~Yb>=xI<Cs_gC*-^dIj1=qKu
zYeF;lmd%!!)d;5ymEu{q@n-`D2P4N|yZZXKw8@`t>Tw!eb%&gF9u+3Y@TtpI3mJ3G
zsmr9@B#-c#A)9*?$$BCu1HV~ome<K*Ohb^?scq9uEy=?dS!F1;R#Y>d(*_sncQKjr
z8c%<Fu7qA}!kLa&Bnz#(r(0@);}Rk5ML(cSX5)zGM2kDxv!|VppFG>2LV8XfIW6+&
z@62FJ0{qydCyWX7ERZ?{V5~JLIiiANW>cVgcydNZ{n%vl<u9u-m*#o4u2tKw$v9wO
z0#L@{LlTiJ(22wQdA0&f=$of1lzW`~DeU>He=!^}hy+Xb(y%UG<;Z+{&FJh5E<mxM
z;AZ;@;b(jZP@v?LJADcgA<Fs|v@J>R<mTTUF~d}ud6$_L@cS<vzUf(N^Xy7A0m5L`
z55!#J0<k#34EVYEs}9w3S-zUNq-s*@MN;Gy=U)MN@>d8=*<0+1M`LGhAGDc+a%S=5
zC?9mwfC|JW7*4;<2}$B5NJz-+Uwb)!pMY}DDI92BBU^;)75vO2K2wKY0>HN{i?P%k
zy#dHjZtLb(Ao7cp94?#9R_ylmb(fbySt8=Vab_Gk9drBOqnFZsgQ)F-iI=ZqshHD|
zggVB0TXRc09%obTL{6o=^)tkssycj0K9!w;q|keTx=-OXUCBzBch$X#@Kya&{QZj$
z*uNd^1*;P=6&e7*VEV5e?Z2ETlon56EM@@U--YwJqp6rX*%$&1EUX=wK>t-`v;&%j
zD#(c=!Q;VyHbIh<5LNoT&j0{m09f$PnxuPI5CFimE-5Oa;+k=m38yV{LOi(HGOofl
zAR}X8g#P7AVnP15AY+7OU^pe*pKrOjwPH!|`%Lz#+Cb5TZ@=kHEJVV|1}ch+CF|JP
zQa&<LEz+>|1_jh_yoDaTGk9*Y95-;I9VcJfyWHel7?Tl5VtkU%&0PRwp~A}|3V=~$
ze{cn7R7~I6fE+*qAtY4JDG4>e1V#jmnhzHKe`yj!EbJub*<VsFhTCmO&4{Eafb$V~
zuizXrsodz~9$}*NmxO-H&iA^B9p;mS5IA^ERRn>g2p9@?J2v6cXFoG;uy}nvL=Ti5
zms<ilMp|ofUaql0^}m<Q#QZmT^mb5INxf%!kFW)LuknqGpsb$@4*&_7qThDD0u@rV
z|K`$7S*zT_-oG8dZfU8U>$<JqXcy9y7`~`n?A4f+cNLgZ^T7q4Dk~bsYjwvSkrow8
z9hD!rR%_H=hZ)lYXlXkD4n7YIIj0n;a+bf+eIDzsdXR&tPV$I@kouh+LNMh~1~l;S
z+9?H^ip{T^xO{8lg~Qk^9A|GV%<!;Vz3xXVz#tMoo;v?R*(=J^B#f4#DHn|by6HVH
zGYsIo_$0LEVCvLfJ9GUv_-;-epUk`D&ccOjvZMzMc`SL^Ij_^gm4m*+OW<=OLfdhJ
zq;5=~H`$lbk}#m19eiACS&8@~5j=!bMUk4i@(JvKn@zUZzfUO;+=1iP(arg{Alw^`
zI!vj|gO*MGgoyZ~J>Br=qS(VyiZdLiwTnLDBM!OQPA3l-6DkeV+hlFYI=FhFhVy>Q
z4IT^09J+XDVKWnPrQ)`oBbjt!Gb~%Z_qN6VcaE2PgBWGsJ+vOYTb^(p9)l;(BEA<m
zz)tdU9jo2Xo#~X=QLNQNaIz<4LVnYBqvd&XxTaeet_$K!m~5fCePuI1nQx#ooZJKB
z&$`O0{A~bEHAHfz7@L`qcJocMm16wis#kwAO2*6!ZbOw%B0CNJ1sK07L+Bt*iD*LQ
zmk<PFid1iEYA-JFWq+IZ<jW1o{m~n6=v$el+b)!JW?{-vcPxEAq46F}6e}2$UYbU<
zTZ$e8v`a4|R*uzfqiuH#Npg+j1fAnw`%5we3xoln(uCInD3L9ms-uDF^86LK1jbY&
z>&OHf^@>xw2}0RO!8tDUxVne5a+Teb_hncU<Sap&Lcqo`>#piV>b|N6`VoC;n_Mrv
zEJ>2sQ&v~lY?&~k6`$KgxtdjTK8;)I1&cXWQj0^d+8~rE!~=avNMqsmsVhsuVy#UX
zpj6CC@v6xrfj{9@&Ec{h1VZ1>hU;PeF;Am2jC;(%3Hg`vx|g*Nm7LR7ww%XjFIcz!
zf0xH5x4*a_@$%lAF~7@64(kCIa5tl-T;%`LAkfeGPf?*u(bu-K{qt2WIA*{Vj0(2T
z!#}!#ew4Iy5F}OfRgejx#+P~Cg8`K3tGv$bJPDb`J-?Io1<H0=vl0#+9k2J7k+>@i
zc>9T&6?<qVrYcQiZxK289PR^a<LQ^?TUf+xC1c%@7a@ua<!kUlr9(iv&Kb(mksm|#
zX~jy07nSkuX3AZ*Hh_OB#%|M>YwdHZ8}2B`)b*t)u*n$xujVl1+m-~@^^IZ=q5ZtE
zP<GX;>CGf}x>Af)o#h+<dX@F(tAC77kqmjEH9(WCyOGA~>IvL+%hp)H*ca33Zs_Y$
zy-mQVT<-7rE`#@9Z+4}&9&O@_fMwj1dw02oXH$>QB_5!ttgTD+vwy^Y2HkX%xO%pB
z{iM#5F+U<<KSVJi*Z?yoX<FJA2-h5V!O(nY#(EX7;6j0OiocZ)7C*6Nm+y<2wXC4i
z*Nt}dScMe*Z;AO&W;jg}?*P40_FF9TuTd^f9#LUXOrYDCz8}NGb~wCYnaZ!@wgZr9
zNMx%K$ZWjy&Q?XV1wCAj*NGE3f(Pb1Sg++)mUgGR3nFn{JiB;AKlOqBc(gS09&+WU
zU+?ZVp@iu%$$-TzPg~>_&X!Yu|B)JH%3B4k8#UhuI60D(0~;-jf3CWTe0ca59^oJ2
zb+d>3PMMn-rw~1u1B=`0`|>s~_t2k;3nk)YoUMFC`kOWXPd`Gehb6ApLWs>V2o2ub
zLi;#oPOA#P9)p$M017^z15!3UQ_-jdkv>^dQ|*WP9P3|+YIhhCJgpTxh~s-n=RCPA
zTo@!w351j<WY>;APeF(tnc?5Rs;MmV%Q>G!T>dp_Vmcg)!Z#BZyZ?48%{v=g@o7B6
zOSSCRQ4;BiWi-?IK<bnG=rC=!cujI|f#M>Ob}wrSCabi<RR&^MSZY|onw!WlpLUcx
zK?SybcBXJ;wS87um5IMCzO7IBE1&z-yV0Bq7N%gc``)Fkw>SCL4=l1M|M%ju(K@7B
zdAUEmW<$1VPSPFx?Kd7K{oH9bZUvQ90L#Cn@%Eb=pL$Z;O)V?W&<p)Ev8f?-Vr%)q
zZscTECXZVDG_RbMZ+rYGK$ei%FEUdPCuDS!cP};-{jljm^QyUq)Yep3$|{or4|u{R
zDUQ~v5!+<5gV87N9=0Ct0?#Thp=nictYs=veo^k!^zxtn@~NoKA5%tDwg-v3`%b0|
zy6o#Iy;>UXlw_e+4Y?4MAu+@-hq4wW>@c2n_4~=m>ti=3?AG7ypzAydLsSb1Y6u(L
zCg01u)bKjx5N^yYzc0VFZBbQe&%`=+HJ&zKR4y$CM_hKk>SKQpEswc4Pgld0X)n-E
zg0l*I5kh$X!y<JPK5AuA3y%k_DO-RRF`7|C$zIuhUtPF2+h|216sf1>JeQ2(ApC*<
zKCxSSC5T;jw$$osCx4lix|_?!-+Jrlv*CsY@DpCHLXV_ja|qOuk*er495wGKob9so
z^ZZ9(>U`t4@HmI=Jajh^see>6I}<LF(TVXu3~6tKaYNGR{4Gs~6UxVW0*ujQt=Kz<
zwcFZTQBtRAZ^4RwIN#@ORs!{NGMK9Mf{9%Qo-KZjM%FC`mP*EU{k!G2#gG{r&Kq}*
zzE79{PDSPt=W}VSkn9X&iBkP~-J1(9=+M2zB*M^dVBHrY7Aitc+j!??k6@U3A4T#U
zk4)0>3wKR$xXdGeHY`_K74*A`Vw;o($cjtNXPyG<4s+jZ?w@4Wvz-h~Ryl&ry{IL(
zu#?w^HKct%z=yVeFM7rfCr6ujEG~6H-b6H9a=b!UT@*PhFTX#AF<ng56N-Zs#=>>?
zIrW`x*p^3c9PQvYPvnTNm9?JOEabfQwDNw=3owm17Cka!KSTCtfrFQ1Yz8qc#BOt;
zPcM;opz3u%jg0$R(mQ4CkhD`*C&|>pe<o1AX2Cyy9<Yp9VvRpWG$PrO?Q)98uF`sk
zS1+WFeW;#HNP_4*ZmMOb+oh#_C6ZPS<n57BVC3s(+l7|a(HgrhIA~v$-?%%y@EO#8
zGf|7>N25-8o{_4kDmvtlXt91V^7rGl4frSjSUp{5*q^mEkrno1P84B&`r0`_<2)dR
zc8L|eHkksVH4XI6*=nWVD}QU?DM=UJItvcsikGhhsy5>VGCt_=t*4lVj-krvhEayL
z6%$H9QAKL{n>XLc@1(?;FYKz1T)YvZJG{AexZp<w!$0n~&##oFOwVx`ZWb-&FTxPA
z(HX56%i!TnLdKb9T(%cBo%+D-)@?1X6Y>SlMi_0{s2qPRaeenDK}GZT;QNyN!)ono
zd;+{J*1PQ4&ApAt&edhbRPYqvezZoMlvCZ;gP{%P8>hBIbH`?^;c-Onzx?&Q-S$5;
zk(ll8+^{=7pqvtdo%Z8oL$~UjxAb7#bu~`VJ?)2|XNR<Nj^Hg|M4h?Gel0csy<^er
zO}%y%I-TtwSG0mi0s@eErI^-Lxw5O6@j+?4E*tR^$h8PNi+9aAT*tne`YW5xK7|vz
z{euZH1nLIrxP;Y6QJwJ%Ok5zt%R7=+n>-sDn8OmEn@iLY$XLR3_*Zf!7#xTNLit*s
zv?BhC#we&1rS_(0d7al0Z#`G3&@s8GqWH1yl*Ot7)us!z12w(4i;1?axbaAlZE4@W
zxp{||7&myeMWx*{1@}jgbTQ8`Hk!6EzVjn}L3FQKp!QnEk*0wRglkKP2UeEulQrjn
zIpebD<SfM9sHhXyp(=_l-hG!##Y~S^P2FaxEL!wvU$)%KX7?HcAAJT0$bb})!w-Mf
zvByidJ7<<4guN$(M8=1)xd%?0*|bH7BQ^+O>BQ<M!&xO!aVRb*$D?o;Cbktxdz(ZM
z#x+G#FrjV!E59uNBQg5{E4@n>V=OiQIWDg<(J(Il&3>Dl(22}wEsOZx6<b36lOIVE
zg{bLcc%jC|xMebEh2hs5z)}dMX?6v3OEHB77WBDe!;!St8G8nZZ2~|RY&Zp}9>k=Q
zumT`9bC~ffwfP(W_vXra#5^gHEVlmNSjiBwPOi8~+K|py<usIP>EdH+%Uv3zmm@t@
z!Gs@1QpEY534fm1{0R@Jvg0P>2{T-hwIQ)JT2#;dbPrsas*a+*@93sPtn8822N5Qo
z^YR6E0%M$b9JI-e-ku-La5zqi%}>_9)`cgi81F|qUAe)bxD&SReBpC*4hqJ4i$AJ)
z+_%_}jyjm5j?zGD5OaLlv0+M;5lHS(7G!U4?soZ2WouYtObZNrXRJ?ddh3`KD#&fm
z$zNO;6aV^F{b)DrgT38B7%saT2?<bGJXdreqy9aDwK0^H3iP5qb2)w6Z9;D>M3j`|
zQ$at&bT7TgBM2W`R$MfV?75KD@|toytT61sGtD@uT-SoHKDV$qFe4l!XcIKO_#T;F
zL^W3{Y;(@G4CVN#*Y^-O2vbQ(1A-VUV|<nAnLg|<_DL2itvU}@Und^b)>!uz#i{vd
zGU%_xjTY8XAcDV8_}hbPHDljtH*&)18{f)s=oXq6-^httuDop)aSb2Qi~xlHu;?3t
ziKx|3p~s2sR2==T6!mx>>^25mG|T|T3D;ivK0F+D_crP-Od%}+*6|1oZ>f}~Op6e4
z<r$dWBj^SAiZ5g&A78(<aa#vaIb$A}4jYu6?6Zv?i#A?%29=ia`?KLq@pG=^rX1G^
z&TKzbrr$8SS3UR)u12i?9Gk^Y*U_8WA8}qRoEEGyBIX@nSk2=SVqf89QM8&$*mKjh
zZE898hwQd6c7S56_mW_cb_<)7{M~VSjqNBDNx39%#`aFq1?}0!&D@fMR}<a=j&k+A
zZNSDr%Q&^8Up^UeP3D?4+}Ke~>6gBB1FkIz?+Qvy(3R1G?Q4t)T+(<tzsMhN${%2S
znS!V9v$P>0(8lzx<1UG_gzR8Wyd-f9bV?^z`Sx1X#yb?dUp;VHicJ8{<IjM<tkR#I
z;>Z^&XyUZ*G*&OMDym@0eI<WJUFmftgIgRjC@aV+jGFf9p~Hu(FlJHLnEtu<Eqr+l
zJRq%!n3@-E8)kW6-AV1`<TXV{gaRPyd^=j}j{C(#$?DMmdqw$n+-jxxXp|M;N6SP@
zXjhh&Rz-0c4fmNU_LtpfD^7v1EJZabRmBi!xIm^h4^p+m!OifD^6BG_l?bmFp(<ox
zU6xjMBPWiByH7gFjJyU|54~37%lh)e{m-k$QH>nJ)@XdX1hY4WvG+yR76ZFZtX`&@
z1f|4S^v=q$NarhQX!b&jZUd^8tSh-X;t)XIzM|i(5OnJ^zdMQ;uMJXl|ERR&pKy$1
zH+Y?Ww+<kqT@;vutwyi`TgHOzgCw+?oT?<tdK2Rq0_b|&%y){H6lOv-!NdP~Rpbwe
z`9w7YvhFjQmUJUi^pw#((V4@v?JZn1hdSK`2BMnyi&ih2;bP%k2VukSkekMJ%PN#g
z-s}_h0FH46cJIhEkIf(-H9uw1<h?unq{(0l+cj4PCg2s&A@TcWif*O{=U5b;099Bd
zuDRLG<U47Kp50@MG-QyQg=z80R`?Axu^Tfa51?p!0zYeTxe6$xJQDUZjh+6*|E{K{
zZc2_1WViX!J$|?3Qv31V1b9leu)v16e4Z@GvmHAN2CyoglLK16H^jQI)E~2IqKvoo
zvhsx3aB^?p<7i6iD%V^QeY;C@<<ansRZfPX-{=Ny&-jt@Id{dU+Q(@h`rNyg+@5M8
z#-I}_Ll5C^jmC6~<0;$v&XxIdxm&I8*?l*fU7v|V4*5DtCCiKhEAOI{X4>{ROU>VQ
zSPZuO;2xQ-oz=)#B2x6yKPb#rr2D%Ah{yYtL4T-X)Pqa(xZfl<kFKo|tx2hT=~2IY
zpEY{R!wKw4Y9s{kSIFlbqP)gQlOZW9Q{6Y4>5h@%t*(=+Ew`3v_};x^-b{z<EM}-)
zWgQM)17_^tt{F29gWacj>M`%;A^QAEoYXh%<hZ_=5n3DE<SehfT*>XloeEkfi@&1P
zU-Lb!a~OkV517s1t=TKtQT81&Vwj<Q_IG4+nP)F^h}6$&Dg6#7u2w}IS>e*}4Dx2T
zBOcNcIjePG22OVrwd_~lbYygSF7GIIe)ZD@1)K|&)-r&U2LtG$=g)=m^t`sAh6r@B
zoJ+%<BA+NFU!UM>S!37OIijho@M6=ko{rI75>-KnD*g9#Am4#gLt__LvJX2<h}Z{z
zbxu}WUO=qj9PKdV%n!f$0aQ#>HSA=^Uum8%*l;=eu*s|4CDf&g)6Z#}bap8%90T(p
zW3_A~JIz+!eop*px-lG4cwCg@Q3qCs&0BmPwL=&IS?p_Rl48aMB7D}iIQ$~W?g3TJ
z$$UDe7y4BznJ&k-d(ny(y;PoxiKV9WyEg0T++ZkV%g9LLX5%<DzFH4V!4syN{C(T@
zNW(ppiWz}iGCuY*8(%joy=QT-UDkIiSS2vmCY2$Kn<&P`2|ka9yb?CKHTH9ii^<C<
z!r1e>kTs<@_k}$3sgHu>#RM=Tg!zc(@V+LUWh2$IV@%!fk|P0&!-Jj~ffhiSQPbL(
zw4_~NG><e=tdem=!riv(g?d{?)0#no-iWULP5%%SrbFK|*p_~&%QjS=YKOh0&QqC7
zsZj_s(_ojT*VSB6u~Ugtgu2ONx3YMB7NL0)tH#T+U!sRn_n}{B4Zc((XN6GLGrbUF
zAHOjpf8M+JRuMS+y))AN2!A$5c$$cAgH~b>7FVRLwI1+$(z*fh-Bz<w{u|UX3eQ^x
z`p0RFGLxmJ;?*3>vzZ<Wu5qJje2I2&=2(l%Z`O7eh=&XEo3mPXwv<R(wx|m=p9Hpj
zOXr`Jht&a+3Ar!_7Rkxl*96YH-(?fS+~vKgm`BBC6UX>v296_{^5w?7exvjAPoBCT
zjAy!supVShHF;!kG_cMY4jqv$pQ(Noa&_n<w>R~i>n=x{)S5XATQH*;x7WV2pqyLt
zfqjq3y~?~!X$TY|TQH`nK+Lpr@Ijcxnboo(=}w?6!9Wv|O=GZO_T~<ahjAyP1jhjq
z-mTw6RDYOkVSUD*cXS4SwtM`DSP46!QbS;>xGQmR7pNJ=%piD#b+;lR{nFun52jRl
z+(oGhp5Ghw!Vh#KOJ>xyl~Fkg!da>n<)PUS@wmjA2R);MLFW|=GFWu6rVf;ojMQ!<
z%#B9gRV%osZ{!+kz`Of>P(GURskwQ%Oz`BvgQJ@b()h2RqWp+HzpF(}8!RHgHc*Cd
z9Fo_~a`k_$jI9V$!E{`XylWUP{PLx|wO2cB#d={Z9Zr4UOF-hzy4+eM|E86evOAZP
zw)F*x!ACQiAWU_Gx?uU@edaFKd682O*X1qRrp*LI6V=AgzN0qOVq)g(1EkWmjj*0s
z5;lQ2w~ZuDAubsG0A0-yt9yPMI4kEIE6E%+PD&e)SXu6s%InQz`ieg)2(0`$Xy6dg
zsKc^u0@3h53>Le-loNpliEghVwd@HVb07+YHtyw)wHODBKcI>Cdm`WECD;%}2-zk1
zGB7COf(V;~KU_{E_7x+p?uOgz^dtk98(a{8+Cn~ivfLY6UP{JOw-V?g#RfNuBSnH?
zqvXgcovcc)ND_aw^!=`Iz|Cj&Z~>Yo9`H-bLeX~oWTkLV1hO6Tr;qr<_g{i0SFfQ-
z@Zqt<OLB4+O{}Th<O9@H>AY-ikyxpgq>bLAN8g!v%zfr#Oaq-+d}63zGrQs8Lk47x
zx^43#5ZTjpcS4Qdb92Ujt}9&TspnQh>1w>PaDqE(fG{C;5A=r76F4H%d}xAgbZqI5
zanQ_a=VZqe#4%oil6pst%iUj2g6wf)K481TbRx314}+YENrWP@4Y41Lld#mUsN6J!
z6{VYOyjW?Sue#z}NZ%Q*I>+I2zFC}TN%0HyFakl@2`%gdGWDkrcqQEuie(k2?<Q?2
zS@`_>!^0%)Q(ZAFq>o85sZ4}X5&UhBZ-nQr@Sb+M_?@eag$H6XE?wUM!Zr!#FXMq?
zc{W#qqggx7S7w0x2DQrD1}sbn&=R9*vW~s;$`ju3Bm&Q;q1CdJR$j?+W+rLL(3;4=
za~N-#>ce7)AJa2kY$o8_oja^7-qO&s7C7pU)l!6FQX3011GZ~ydD-YV+T2)7?Tb5F
zQe!OsSP3wR+FXych}b2Hbx8$9+E8_9+?9{P#F7hU3Iqqez#4I_T(3J{g(%_-9P#Z6
zlnwqBl5k6_F&XqzpI2fyGbEwYIXCCh$VRmM3*kbTzQWR$g27?ocUQvh@ifOmjzTSO
zX(Oezw1=pZ)a<2wj}zb}lL)#>^1`Ofdf&X`NhgXc&h<Zp!1hX8BzCCBkHQzqc}W7V
z8INpVooJY_PpiunV(>{Z^?tfMdXq+Z3jhvBv{G0R?o_S;1X*2c(`pPC?A9R9qMPE)
znZ7snEk!PPHtCGF>CF<Bf^(~`G#38!O&pY7Y-$V#tFYIXv0O6mu`390zJf9d0#Adx
zaG(&7(0jtGi=>%=e2WN)6XrsyAj1A&%trzOO9Tuk-~tj8lMmRj`9EDwZ&x~PCQ7I!
z0C{AFW<M(z=#=Mkh}vQ;QCYOMB>aXlANX1p&zqZ(23EPD54MCGvF7OBflXm!KuiL~
zXN(4dL16uM+nHgvWj?2a>vd_tHRhm&=b{8d`{oQIbn~Eg^gvdUlu|iwQs_+z^74R2
zwAlTe#y*<1u!MJR6OjK#g-%&h?Vw@Z-$|>UbyMckC#h*vl_qM4{CVYXCSXx$ClF3a
zS@mf5u>EZcD;57O7?X36Q|PB%>D2LbbSsQ=H5r7He^(d&lU5Q1uKVAI_&4G2ofrfq
zC>Ot$#YXSe>nlM2IH>l?L74<73FE-qrO!_b*{ibM_FwS$n#%)$_C-?)LF5|#X;P+l
z&7VUIu6f-GhbnVQ#GON{kU3g|I6=12vi7~(>Ok<-C`)Qb`BS=;`kjzLQ=Vi+B@v6w
z#H7Mvc+*+=Ah_1m#u43X`mIPcTnf>3R}P}?;vD)y7@9|3XeCRSz<Q65^g8NMQEdZf
zGo3rn%Mrh$3v~NL<;>DmQ{A2N@aFG)x`VYpD*Iz#vpzh1Eb#{mHkq=f#U*TQYZCGm
z0>dgMzmZl&kvW;qE%51Rz$$$Joc&#d%QZ5M(E8nljGwHFiP<^t%ja@O1RXMpv?0KL
z!~$QBUs-DdK$M!Irn|q6dG#b~ff!B<@RB9NT_4R60<IajP@B14FN!p>zYb_c@l}#k
zQE4!L;w<i?MUQ_qCEg@C(Y3P^Nw;u3u$ekL6V*XDpg0}lU%-sg1m5?=p?b!7n;6Gi
zHs4wJd6*bEH}P%zk))KNj_LkBS7@p&^<a_hwe_R`7#QDcUR3A~{yZ1W>1d*mKls~f
zM7ak2TDn9IUou>WPLl+Eh`b1!TRA|*?4A7WfI|0+T6AqH^Q@YS|DQK0-Xbz(1$!W>
zgSFaSR!}^GDhuA^(8B~%#Lu?7QOAg|eZOC-OwL>rsxk&dc9#Th^fFX**UTOS_QmkX
zcC4ZdeN@0%Tyz~?@`mRKsMkAd>~G9GVoR?tw^YF?8G%h3sR)*1c;I9L8-$MXOvQEH
zlRj!Y`N@@Guf->j&`t_Bkb@U&F*@TB5pEa6`g>j(oS@Z$UCV8-DdY`F<x$D;@(<z1
z^@s6LC=Z#68NE`-3i?eQ%;$%!C%!4V4q#eY^N6XZ%v8xf0IQ?5G&W#AlN^6$U6g_8
zVT`t6s%Qu~cyYZlXbUbJ^dR7KnwdM?vs2@X=S0ET7FRF^$*R<AM(My4)LU#-Id{TW
zB#MDEjLdu&;uUY>GSGS&A*;p3d0Pq<C8G%KTg*{w`)6JEZ62%}xrtdHFl|<U+=k7R
zFHWCT`t>at+QHz*0j(>x9b!y87-V?@i2SktBEERP{(T0@{n)s;g)zh~DHlx~@aw=;
z;iht?zPx+)?XYz26)|;uir)e)Ew^%+{t6DUQqoAEtO$<u$2^JI8|W#VbS+0oVDL+J
zfrygVq<HD+T7UKk04cH|+r#|tj4ieb-hvpxypVnSrWee%_K(qRMGT9cEWhmDrsAR{
zbfQ^iLxzxd+W@;@h?xfSw1VzXU?#N((a@ei9@D7R)-(W&%2h3Q*+yjU&b0gy5;~PT
zQcueJ>8$s4hqkdy9!H4-J4hvoEs1ef5t@TMRzQ<vWM$8Sr^GGwN3&HEhg(tAs-feT
zq$Veau>4nbbU0&$OqsuujX+>%rkViq#+;KtzZp#+2`;5SJvu+CY7ItOUZs|dJ}f7N
zA}E4-f)7<S3E_T~J$5>ydEKEByvk&{KEifAPA0f-g%P$soRpd*K}SbJ&RN8U_)U=^
ze5?!2VVzUCt+E#Jd$8(SjIHl*<+IpyzK%@x4=<Oph^EP0HylnH6u1_-v7PhR8K+88
zK1-LknGVDKFc%kS&ka;Qq>U(%PI$7mQnM!k5VmZF5u4fCBRH}-Z7(M*4~sO^X>CRZ
z4VA$Cr5^qUA^KBC8GaRH%emWdg+wjy!Sv}vt?3D>iD2kUM{M|Pdvc&2wG&T#Ex~&}
zU<Q(muj32L#&7T05ZRH}c8a4gpNQcLuLm$+N;4+$L^njf6!tx}_;CC<*5h3<%hUL=
z^&J6nJnnh2uH=zF7Do@k+UawAEG~BqRLE)5o&oFu!;AuC?L}5U)6{>?yA}Ca+0uUw
zh!Ta_U21rWFdxmVdHF)s-~vXe{qCp9k0TU<wBZXAc$bwm2LNe6@r)LjCGrfos59PM
zNogR9px>ap(S;lFM($H`{Pe|oTSp5~2mX)bPMyCGc$>~Ous`wYn-0JFSdW62nRYFv
z4j4Du1&hm?2p0Z+MI-$XKwU18Ss5v19AheRbVd+u*Ordm4A;>X5NRjsSiV4##?6Qi
z(fC=JlOuz9<6+;Y$=4@=%T>QY!hnWH&CNRCD`TNabMVj@!Gw0>Q8Phwq5h_;=*$U8
z2EOv?_&v7jtl1a;aGSU6g`s1Wx*3&hP19?xcc2ZEg45J<$0kGboM$}ezSCH7S4(HL
zgouzl^}l>~_vSio-W451$E31FOTcv`qR?Kro}=jfQvo?U$Y^@N$N?&yp3e1Q6~MZP
ztuxVJ|9JY<7BvAkFAnb|PZ=TjRzz}YM0X<^&(LlZ7|^mE5Xi1?osO0b@Fm4kZXEi<
z7ckOKJ#~j`&*gbix81ltiPYrEzcS>6)5J2!kyh_*^dY(^t$CHc%1?qhGjCypot^eX
zJ+$NCjLA0XwE6UnTy^^fEpIj$7Tzn{4H+ZQ%WkuXGZ{?pq=@y8kwQ-e_`w!FlMJEE
z82*OpUH$bESJIixmD>Za@e%YEvu~_9{@vfT+YYZY33(&qB4m=}3Qr|)<r9k71?MYY
z-wZ!r3J75oC(47HCJn<W@q}IM=llDpcUjc?nu)SyEVYj__t58Yizj@6rsI{Czr-t7
zHJzu{w<aV;qA;~e1X%h~_B=Vsj2~uZ*8n?Jc1-URG1Y{vY4Xs*NF7goG0WF-+23Be
zLxLb)6Hn^mr>9@wCy&9@rx3*_Gfl8#z7H=6T_#pl#Ez!tdkttWjBf1(iU{E?#}4Ib
zt2r4#HnehuWFf|ag#tpn9~lP6c}F2s<+5JYC*eX20U*_trGe&%8~u^?5e&>TbtTMd
zHC#)EtZ3No_U6^xYLsbfgaC_H0H|+Kbsnt^gM*lIci32ZJ_Ejzwqr6<mINU@zUfj9
z==yPN3>~>!K8eqUPnD$f=N+1adU}xYed&J$`t);_@1K6{7!Wgz`VNpOLSnJ#CQ$Ug
zbhU8fx;4>|K$VpvPZ&$)N9wHUm^E}E;|cglpbB*}0;_UUVqIPqtdinF6MN)qf<C_%
zGSbFxLqNR%N27^sL2iS&z2v02Wk87f{GVqxsv}dr4g@M-lM(g_)r;5S4Xl<rrVsr+
zu7NU#Sx3P*&5Y|4t2ghJP~N@Vr`8^JkJ#ka3z<Mc))~I~MqZ2M^$7}GAFiI?7V{q7
z))AO@t`jm}wN@^NccA5sF^aFvE_vBzpH0O=7#5XjP?QV&NyKPcT^WEf`17JSSMrv)
z<ya0HoIf3~CprsKrd!wEBIxN>8J6Qa|CaC@`v=of(U-abdYiUGwt4xc@+iSe4jBE=
z*o`lY@p!v!d**VHJ1Jijy%SWw(rt|SZAN(Ra4Bkwb1{Vc%m7k#tT>+5k$VU}=>C?}
zJtIZz%~}k1S;HZDNHW1ms-2B@;G{8!mQPR)$!`7eme6H%9#)U1U&{^Zo0h?U7~5&t
z@OgdTn0#Z^h+1#~{@vIt06%E3mh@P)ecBFSv}DNzy3&NUHmP2SJua99)CWgjIzMO{
zAgj^CPiJRo3bk6c6;Cxrlj(51-y!C4QkkYd2N(9+P#w(@o((Q7>RLrDvUaakzeP0J
zRuRcHJJr*D3ZW*PN&H`+z}~O(1Nh?k9LrZ%z5-XY;aSJ&b+~q-;T+M-1M|0?G@!mQ
zF+s~tBW5QwUWpAmSthlVYN;)$K=v#%$LQxnJ^M`^vXLB?D;tcPHV=zWdaCM5x>N3c
z*&_U^bd_Kk=eXO%&{0XcY?^=d|0lqS<c^$eOiNIoGF3MMi>GDe!)pUQ*m2Q|A0k#i
zdRJL8KrOe4-X%8Ck-h$#jKnh4TcT;GKN9=x#q}q#XC)K)@!+z>i|D#X9lib$G;_Lx
zz;ovooRa7m547q7c|YFnJAY*&=wkY$UkI6D!@!GH=Q1)9&We!fy#Pp24rY<xQbQ#0
zm*9D}U#6p2qwh+G$G%P0spjD>&~Nw#_UVARqy0yOlQMS$W{4`xo-vr1oJLl5EK)P(
zB9#7FSVf1nfcUZAk{bh4_gX~LvwMzJXIQ!42w<c3^W-7ZP_yctwjHeeh#LYL=2udg
z#aV%R`bj4pUB3iddO-C9YUyJCO?25LA7ka!pKKS}BGOGkr<ZY(I9`Kc;VgKbx96GT
zlpNK{2XTrcEkXbdSx!gM16o75!Ds~YF$zGe20Qk9URW!sxLK%EBIWQ7YQ8>%Lh5DL
zVG;~z0RMrgaH6fh><Fdw&}*>J_LMy4NT17?iYO{SpDHj!EgI>R4n-7qQ-{O8EmDV|
z0m6lf!d$+p3(YZw+r#Jt$Eq8pNVjRqvL?W6#x~gjnlN(|r5xvg{|(XJLCL9{za=_R
zZ<8iVOQt)sB3ed|5;^ln7BQYpW=ipwRC)}MI*$AmTs71=i!E+ZUC#RLu_IL|-vXgP
z)7q1}GU|QL&oL9Co`+-boy0g48@N?*cD+WgAJKfVP0$x@yju2w0f&b{<MFk#Mkb{W
z_?mm}M)oPfY@h4u5j4B+^R8>Ok-IOR)$VHZ%N;{>9k#t}BO~8W{Pg^0kd63!qd7|d
zb!X=sNaRwKI*n3cdF=QnLU7EqBAVX)G|3#hur2QhU)i{zDGd8ViR*sjPS4Tjv~+t<
z+M4r*1&MBR;L~7~F%mgGPfG`v`^awyv0le5uq^na9+zqr(0P_acTozq^wnI7gVX(;
zvfyll8ISb~s`cTmV;5>m<M6S;33{;Q%&heJut@Ct4#Aq#gR+9vuZ${_mOL`MDqm%a
zNl^0DQgLSpKA^g$`##VBIk8&*ODwGW4n}kI=SdGY8{zku-vtx9bWd(oHR1dmSBREn
z+P2QRDeB`=bl=gh837eq;J(H_4`0KA%)?z0tu<mbqZ2Ere~>l75owLQW<zsvB|(!r
zDmk8GGnC!s#&pl^6cX43ONzIF3Fm6aad-sBSF+CA<M_#(uY|6C9>^GJ@kdv$+gSpI
zt~+hsllMY`fDNMB#->prF9nIQ;-X-y$Gl?4xjO7cin{~5G?zPyU(SlucWE?VbvdY%
zA-)hoBpz&pV)JvQuga#*O|)z{<@XGV$};H8U~9rh0&9Tve@my&zcxjzVO_A1;Njpl
zJP&r};kQo}(7bAc*L7G?0YCbV4WR;f6wMCUyOLO7<-^`s1fF?f5D&(moXfH&ee&^(
zX9=&UZf;7Kxe1V~@s}uU)|sB-_2g-R_%eSichz_XnH#^wi5RP=*q>~NXOOG=-DHS7
zQ!xC-(oBFP_Y^2ec{qQcDhpWEYy*FUwmp462$RFnA|1Ij4r$WdF_}-%3?6uTJ|1x8
zjoj91vw|TbI=XxsRqert`q8^;vnoj|C)B8<A5WycaFh0OIz(FESx0^^<4Wf~^Sikx
z9Sv>HoR}Tik&hZL;_Ikq@7%A|x=$B7THIEqwa$WMMGt<@jJ&;R_Zs>@M!|zh#`sLI
z_D-i2%u4><F26+LF?L>My23=se(#0wTRMAXZmU$E;O9Bf>&zb*BVvkrtIL_vO=h0<
zE9t)UCJ7yQHmx=L^$-!u=;YU9uCbV?X+wz~3v<jm=M#XkpYp@8^)01AEVFsKO8J6u
zJl=wUcV%A1sFlcXiH=b^h=Vhnc7BuHPw$I{ruzr-gW@=)*r~>P6+Z^VOabahl=2uj
zJoz{=hejKWZ5i*l-eXZqN3nz}PrOF7RjP`%DToS`)&13p$Ko?$bE(6Ev6jKLX*;xa
zhu4#F&_3B{FW){mU(&^5&+E9dQim!jOwA{AaTTit2>yj#=M1KVPM>F(mq|sBKB!M+
zphfjX9%DIQNd+PHqEvW}!)j=Y5`)1O?_gST!<!Y7z*Isy`KS5RHwv&n%W~!xVM68#
zDe5xlbm#}OtR+8<;~Ot^zI5teUMKw!$0VvO5I~59)W?B>glZ)R8~C9Tmb8`7_wQKb
z&+~a$+C8xojGrf1*6Cj~j0tf;PnLAV<|@NMdc%(9!-Ymd0WR0k*jTQIrkmZ~^6BL>
zykY*CMh|cG->jnFwnm~((F|MoIX&+2`fl?M4^9!IHOv+p&7B#yhbxNx*Ur2q8PT!&
zp{KUTcktVFc^MG*X2v1t9`b#sAiSa(`HB9M4&pYf?TQ}wD`0K4WKuhVjay!4_E0pp
zbTwg@e3d3Gvh1&*5%*+T%aE)Js>jfZtofxkJs<sjaog~ZP`2GXXj2=zjrVuo-BNkF
z-v=ZW+bA@x_zbnbU=a`uco>wdB&@5<7h>)o;l%KyjX2dWJB#3ZDT_nAra1727smx-
zjWukgEcXZ9e-`^|=PTfXTLjrr@EH_bsmM0vA2Xu|Z)pFeQ)6$t4nFH!5Al&^S)Wxw
zO`l8mBA`L}s-($(JQ>3h=iFF5Q+)Xs0iTXg1~}bFSJ-Bqb5F9vp6G@QDye+W)Dty-
zD#+Ey-%u5KyGq<C^#A$0hflCLQ+!>~>}%B@GKk54p=N4t{$U@CSlbXA@8Y%OFjJ_z
zN>@b@>$;wo0`c_*T9sg7NZ~e||I3u`|BI~f|G&xqK3o2O;mbS9U%j0rew9kx&wPJ?
z<PSN~%5VDq|7T>ajRDZY)Wi|Q=wNI*5kCP8U`7qR;14pHToPu2f^wi9ZL!Sm<_P`?
z#dMv9zR?*Kucnw^dYnDCTPeo28C9QtW<W3;UR&Iw!fr%EIVxe^a74%3#@JG@%Db}E
zNJpGTcx4$-kWJg_0;J{9OA2D(LbRT$%cXWryWy8_C+nH#wwFL0tdD|)BZ~ZHakuA*
z$1}MDXR59UI?0J~dms@AU*|2!sf9OaRO$$6B#HGCj)apL4Fm-cw8}{juqE9n^7Q;Z
z+ZodDm<`C~*T1BTnp)cUg;=<+yVX&Bt{t%HnP~2QZshJXJ8-p0o}iz>dM<z5#^?5N
z_|7=>fxA;x?<{I9Jeg<q9CKKIO{^+j^$&_s|6o1?^$AQ4_@BV!|AJ!tW9)ww;?K%=
zTcD|hnUlkRknE1EOcpi<W+skI-z-2j26m22|2^-i{x>fh7#W#Zn|#u;bzm}ba&Y(`
zs6~iRa5T(6pgZ6nj^khX@5%ndemH{MtWEv{m0s640j_f5ymb{ZW9l#YjwGBKhj%RX
zR2%&DrNpVd1;YuA3suS$o=LtvdWglu)gk0qpSH1?R@-|T?z>s1zB{;Asb2Pjm2_)?
z+i}Ajmq@)#NP7C}`tfMxO1K8>YTecl!>E;Wt7VcX`BsvJ8_UMbxW6I?^zWcvB#@?E
zq-6Z1U1mH%r^K7*gwesNwTxD`q~Ztx)TDDzQjX+kGzrfxys++;JyF@(RWXW$l1)Fr
z&9?N6qaSxoxy<bibN-ou!yshspQ$vD_j~t>TZr*cdyo1PWj#FZ-Wxik>d}KpD~oC%
zYWr1@KRUJ#OLV*BmAz52WDQ$hR3-_UZtcdB@)sm5f%?#XeNY-_#Ut-teBMb+^l-*$
zbqawQ^cr%a39o=klErLew<XukrWFV#{vf(-Q*TEKQ~6<LDM=+XXMWE}6EvIUcwS-&
zk$xI{P8P-(>jlh-Hro~#`GSVz>VTD{pX55=#zKL&WeE8zh5$6oS3ey>r1Jz1r)2+|
zKi1m42EqwTP}QYWf48L6jF27Mf)^HwR~pg+K@x+Ann$<Za@p-oeb_hc?xb9VfHd-o
z25{YpsTKR;9CPKBx>8?f7^D0Ha$Y$Fx6a8bNKIF=Mddq;m#45h;~WQmsnR+pUWFx^
zwT|8>_ia8R6@`ps@81330)`NO-BjAz*GEYOMBeYEe8M8jH)F1|DpP?xG~4W`?$;6p
z)}*wh=n|6<&{`GrY1Mb9UXs82;+EI5A?P~?za$Ge`#In8x0sbkT=AR|T}5HL`o?EJ
zuC4z`={mOesIa3~j@uR}W5NgSr^UhTF_T6>A?q6WIr^39{Dgxw`Axm1aEh5@@I^O>
zCJ{dQxfXq*%KRz!S5$3h=Js+}T0|8t<Bh<iK}3QniQlC<xI|(*g~%d%AerA-<u4!_
z*Ngq3>GAwp|J3Kt9GpT7_t;wtvp4^omwF#JdF;l36*O@*`YhVCQ+Cbo2*UH`XuPRR
zv*s6&@hlav7fF39OpAnG0IfW5Jq}#M>AF1Ac{|b~Q|K}!S^dSwm`;tR^iO{{Vm_az
zF&22N0KI|d1q$RQ_8=ukzFd6zjOXc333s*_2CH{Q$ibd$1SiSR@Pxr%fdUZ0x}uQU
z9-(~_ljgkOJToerm6y6#XrjHiA#LT$bFX}t1W|zpeCE3H8J{L^a!2-ft~d8;eiN-+
zZ{wZltmBWc<UFn4y&JAnCw6Q8|Fg6&PsG}P3muHoU%{%XF(pw=`fvJ%kmgnT-FZzc
zJP+TQM=h*XxX{0${7>!Dri~AN*wkO`I+j1_%Fg7jB~7=>rwhE=v21_WFO|UM!Pok&
z>K@uMe%f`{N&7CJMBTIMt5%m|LysI}SmEy#fAAqgB4cZ+uz}#J<>K?-JSe%F71y6S
zr}?)P-{rT7;ns??^uxlvv!XK^UHOW8QmU5OYGl<^f9cd-y8g#So2c0MTVZ|2BCnS0
zV+r0-&T}az*vU5D=flHC_0ODbzaMd3WiO}mZ2D?0zct<8-zXXF=UH%Q<zE}tw2S;3
zjSrt}k9i?37`{<|lE?pVLZ$*+7<N`MUbcQ$ue|8r+C_Wi?q_VNx+=^%t&TJP@+-%^
zmv(w58!NMQ&0D&Eui<=_)xYw0Dj!+29SF=<SV#1S$O>A$yFPD?=YijDtTI)+7qT9g
z|976hwC=)|x4M<myZ=fh+j8Ztoc1DJbHTj6^`5^2>i=0RezR!#n%$gFb}h|xny>Ng
zjdXW#$VRmzcJ;S~7i|sBK9Lfb{#``7-0idO(wke}KP-CY_>gh4Esx%!3dv*L2D^B+
z1-6{=7rClqQt<ok89}yhfm_V%=Y0wIvE^s&#u>8~s$JNll^4ER?LyyQ=Z)=cn`L?b
zFF*VZSn{)TIB#1YP|eD~um!kj4|kC*3M{gHT|*poJ^kGD;ngv4xBA);@4Ukb0(YN_
zh}}MQAuV*FMP$e;&P&VzHf0kM91L7OzU^N7EI4#!j;Zyt@Aqc+-+1G9F3i2-WJS&m
z?)o&*1>e>l+?Oc-`}?n{Z?~=P4bHIgP&wbf>Pq6S8N8<jmxiBI={)5)X~|OlhPBsk
zGEVw4Q(t{qcd2s1*=?&|ow_c`UAnUWu<7p8*RDBUT$uPs?!?u%3rtrnQ*<~S!f`Fb
zRn=E!<I~9rb*m>Y7jWGAlEJ}8XX2v<5&hVE3)L(pN*wNX5Ehskx}=>syWeEn?~FTt
z6?glG98+_AuFikszM`SuSA}CgHbvI|uE^OfxmqvMzuUU<^NpEy$2pbOwqBCb5xMNX
zu(+q*|9yRo@p<!98PyLtJNCIoR3w{3%&1P3{`gw^Mjd$9WLJ;zLq%X!?Fu{#Ai$fE
zNrVCS;WMDB69HgH(ZF=Uj+a3`l>}Vt!nK3|S-|6Kz=zGC>q0({0CZvr0+<79ZRGPy
z&~+m3`vjd=fB?n7-JnRP7r->a+9K%NLJ=BWd2w$Ng_#2LE^=E3)!`Fuf!;-G9>R3O
z>_^zgzyN9sA;1MYB3ed}xPmzYq#4${0kw?~fY%<=FdQu<m<wTsB4<EQ%LoBdfQBO4
kN$C2J6BQ_XB7nFnj?5b1%?gYy1_mx5tO0tY+6}}50P;M~&;S4c
diff --git a/util/osx-package/package.sh b/util/osx-package/package.sh
deleted file mode 100644
index 0db5b2b5d..000000000
--- a/util/osx-package/package.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/bin/sh
-
-DYLIBBUNDLER_DIR=/Users/chris/work/macdylibbundler/
-
-mkdir -p $1
-mkdir -p $1/bin
-mkdir -p $1/lib
-cp $2 $1/bin
-$DYLIBBUNDLER_DIR/dylibbundler -cd -od -b -p @executable_path/../lib -x $1/bin/storm -d $1/lib
-python packager.py --bin storm --dir $1
diff --git a/util/osx-package/packager.py b/util/osx-package/packager.py
deleted file mode 100644
index 60b26a8b8..000000000
--- a/util/osx-package/packager.py
+++ /dev/null
@@ -1,103 +0,0 @@
-import argparse
-import subprocess
-import os
-from shutil import copyfile
-
-def get_dependencies(file):
- # Call otool -L file to obtain the dependencies.
- proc = subprocess.Popen(["otool", "-L", args.binary], stdout=subprocess.PIPE)
- result = {}
- for line_bytes in proc.stdout:
- line = line_bytes.decode("utf-8").strip()
- lib = line.split()[0]
- if (lib.startswith("@")):
- lib = lib.split("/", 1)[1]
- (base, file) = os.path.split(lib)
- print(base + " // " + file)
-
- return result
-
-def create_package(args):
- create_package_dirs(args.dir)
- copy_binary_to_package_dir(args.bin, args.binary_basename, args.dir)
- run_dylibbundler(args.bundler_binary, args.dir, args.binary_basename)
- pass
-
-def parse_arguments():
- parser = argparse.ArgumentParser(description='Package the storm binary on Mac OS.')
- parser.add_argument('--bin', dest='bin', help='the binary to package', default='storm')
- parser.add_argument('--dir', dest='dir', help='the root directory of the package (will be created if it does not exist)', default='.')
- parser.add_argument('--dylibbundler', dest='bundler_binary', help='the binary of the dylibbundler', default='dylibbundler')
- args = parser.parse_args()
- args.binary_dir = os.path.split(args.bin)[0]
- args.binary_basename = os.path.split(args.bin)[1]
- return args
-
-def create_package_dirs(root_dir):
- if not os.path.exists(root_dir):
- os.makedirs(root_dir)
- if not os.path.exists(root_dir + "/bin"):
- os.makedirs(root_dir + "/bin")
- if not os.path.exists(root_dir + "/lib"):
- os.makedirs(root_dir + "/bin")
- pass
-
-def copy_binary_to_package_dir(binary, binary_basename, root_dir):
- copyfile(binary, root_dir + "/bin/storm")
- pass
-
-def run_dylibbundler(bundler_binary, root_dir, binary_basename):
- command = [bundler_binary, "-cd", "-od", "-b", "-p", "@executable_path/../lib", "-x", root_dir + "/bin/" + binary_basename, "-d", root_dir + "/lib"]
- print("executing " + str(command))
- #proc = subprocess.Popen(command, stdin=subprocess.PIPE, stdout=subprocess.PIPE)
- pass
-
-def fix_paths(root_dir, binary_basename):
- fix_paths_file(root_dir + "/bin/" + binary_basename)
- for file in os.listdir(root_dir + "/lib"):
- fix_paths_file(root_dir + "/lib/" + file)
- pass
- pass
-
-def fix_paths_file(file):
- print("fixing paths for " + file)
- fixable_deps = get_fixable_deps(file)
- for (path, lib) in fixable_deps:
- change_fixable_dep(file, path, lib)
-
-native_libs = ["libc++.1.dylib", "libSystem.B.dylib"]
-
-def get_fixable_deps(file):
- # Call otool -L file to obtain the dependencies.
- proc = subprocess.Popen(["otool", "-L", file], stdin=subprocess.PIPE, stdout=subprocess.PIPE)
- result = []
- for line_bytes in proc.stdout:
- line = line_bytes.decode("utf-8").strip()
- lib = line.split()[0]
- if lib.startswith("@rpath/"):
- result.append(("@rpath", lib.split("/", 1)[1]))
- elif lib.startswith("/"):
- path_file = os.path.split(lib)
- if path_file[1] not in native_libs:
- result.append((path_file[0], path_file[1]))
- return result
-
-def change_fixable_dep(file, path, lib):
- # Call install_name_tool to change the fixable dependencies
- command = ["install_name_tool", "-change", path + "/" + lib, "@executable_path/../lib/" + lib, file]
- print("executing " + str(command))
- proc = subprocess.Popen(command, stdout=subprocess.PIPE)
- #print ("after call to install_name_tool")
- #proc = subprocess.Popen(["otool", "-L", file], stdout=subprocess.PIPE)
- #for line_bytes in proc.stdout:
- # line = line_bytes.decode("utf-8").strip()
- # print(line)
- pass
-
-if __name__ == "__main__":
- args = parse_arguments()
-
- #create_package(args)
- fix_paths(args.dir, args.binary_basename)
-
-
From a42e8e965a3ae261023a2ade0d09ad91a31e6d0c Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Tue, 10 Oct 2017 11:54:01 +0200
Subject: [PATCH 21/39] more robust drn parser
---
src/storm/parser/DirectEncodingParser.cpp | 80 +++++++++++++----------
1 file changed, 45 insertions(+), 35 deletions(-)
diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp
index c18d1965c..55953d3c3 100644
--- a/src/storm/parser/DirectEncodingParser.cpp
+++ b/src/storm/parser/DirectEncodingParser.cpp
@@ -2,6 +2,7 @@
#include <iostream>
#include <string>
+#include <boost/algorithm/string/predicate.hpp>
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/Ctmc.h"
@@ -58,46 +59,55 @@ namespace storm {
// Initialize
ValueParser<ValueType> valueParser;
+ bool sawType = false;
+ bool sawParameters = false;
+ size_t nrStates = 0;
+ storm::models::ModelType type;
+
+ std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents;
// Parse header
- std::getline(file, line);
- STORM_LOG_THROW(line == "// Exported by storm", storm::exceptions::WrongFormatException, "Expected header information.");
- std::getline(file, line);
- STORM_LOG_THROW(boost::starts_with(line, "// Original model type: "), storm::exceptions::WrongFormatException, "Expected header information.");
- // Parse model type
- std::getline(file, line);
- STORM_LOG_THROW(boost::starts_with(line, "@type: "), storm::exceptions::WrongFormatException, "Expected model type.");
- storm::models::ModelType type = storm::models::getModelType(line.substr(7));
- STORM_LOG_TRACE("Model type: " << type);
- STORM_LOG_THROW(type != storm::models::ModelType::MarkovAutomaton, storm::exceptions::NotSupportedException, "Markov Automata in DRN format are not supported (unclear indication of Markovian Choices in DRN format)");
- STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Stochastic Two Player Games in DRN format are not supported.");
-
- // Parse parameters
- std::getline(file, line);
- STORM_LOG_THROW(line == "@parameters", storm::exceptions::WrongFormatException, "Expected parameter declaration.");
- std::getline(file, line);
- if (line != "") {
- std::vector<std::string> parameters;
- boost::split(parameters, line, boost::is_any_of(" "));
- for (std::string parameter : parameters) {
- STORM_LOG_TRACE("New parameter: " << parameter);
- valueParser.addParameter(parameter);
+ while(std::getline(file, line)) {
+ if(line.empty() || boost::starts_with(line, "//")) {
+ continue;
}
- }
- // Parse no. states
- std::getline(file, line);
- STORM_LOG_THROW(line == "@nr_states", storm::exceptions::WrongFormatException, "Expected number of states.");
- std::getline(file, line);
- size_t nrStates = boost::lexical_cast<size_t>(line);
- STORM_LOG_TRACE("Model type: " << type);
-
- std::getline(file, line);
- STORM_LOG_THROW(line == "@model", storm::exceptions::WrongFormatException, "Expected model declaration.");
+ if (boost::starts_with(line, "@type: ")) {
+ STORM_LOG_THROW(!sawType, storm::exceptions::WrongFormatException, "Type declared twice");
+ type = storm::models::getModelType(line.substr(7));
+ STORM_LOG_TRACE("Model type: " << type);
+ STORM_LOG_THROW(type != storm::models::ModelType::MarkovAutomaton, storm::exceptions::NotSupportedException, "Markov Automata in DRN format are not supported (unclear indication of Markovian Choices in DRN format)");
+ STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Stochastic Two Player Games in DRN format are not supported.");
+ sawType = true;
+ }
+ if(line == "@parameters") {
+ std::getline(file, line);
+ if (line != "") {
+ std::vector<std::string> parameters;
+ boost::split(parameters, line, boost::is_any_of(" "));
+ for (std::string parameter : parameters) {
+ STORM_LOG_TRACE("New parameter: " << parameter);
+ valueParser.addParameter(parameter);
+ }
+ }
+ sawParameters = true;
+ }
+ if(line == "@nr_states") {
+ STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice");
+ std::getline(file, line);
+ nrStates = boost::lexical_cast<size_t>(line);
- // Construct model components
- std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents = parseStates(file, type, nrStates, valueParser);
-
+ }
+ if(line == "@model") {
+ STORM_LOG_THROW(sawType, storm::exceptions::WrongFormatException, "Type has to be declared before model.");
+ STORM_LOG_THROW(sawParameters, storm::exceptions::WrongFormatException, "Parameters have to be declared before model.");
+ STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "Nr States has to be declared before model.");
+
+ // Construct model components
+ modelComponents = parseStates(file, type, nrStates, valueParser);
+ break;
+ }
+ }
// Done parsing
storm::utility::closeFile(file);
From 73b23e133e9017d005334d7fc4e2ef959106af93 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 11 Oct 2017 10:22:13 +0200
Subject: [PATCH 22/39] DRN parser now supports state rewards
---
src/storm/parser/DirectEncodingParser.cpp | 23 ++++++++++++++++++-----
1 file changed, 18 insertions(+), 5 deletions(-)
diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp
index 55953d3c3..3350d90ee 100644
--- a/src/storm/parser/DirectEncodingParser.cpp
+++ b/src/storm/parser/DirectEncodingParser.cpp
@@ -122,7 +122,8 @@ namespace storm {
bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton);
storm::storage::SparseMatrixBuilder<ValueType> builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, nonDeterministic, 0);
modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize);
-
+ std::vector<std::vector<ValueType>> stateRewards;
+
// We parse rates for continuous time models.
if (type == storm::models::ModelType::Ctmc) {
modelComponents->rateTransitions = true;
@@ -156,10 +157,18 @@ namespace storm {
// Rewards found
size_t posEndReward = line.find(']');
STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
- std::string rewards = line.substr(1, posEndReward-1);
- STORM_LOG_TRACE("State rewards: " << rewards);
- // TODO import rewards
- STORM_LOG_WARN("Rewards were not imported");
+ std::string rewardsStr = line.substr(1, posEndReward-1);
+ STORM_LOG_TRACE("State rewards: " << rewardsStr);
+ std::vector<std::string> rewards;
+ boost::split(rewards, rewardsStr, boost::is_any_of(","));
+ if (stateRewards.size() < rewards.size()) {
+ stateRewards.resize(rewards.size(), std::vector<ValueType>(stateSize, storm::utility::zero<ValueType>()));
+ }
+ auto stateRewardsIt = stateRewards.begin();
+ for (auto const& rew : rewards) {
+ (*stateRewardsIt)[state] = valueParser.parseValue(rew);
+ ++stateRewardsIt;
+ }
line = line.substr(posEndReward+1);
}
// Check for labels
@@ -198,6 +207,7 @@ namespace storm {
STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
std::string rewards = line.substr(1, posEndReward-1);
STORM_LOG_TRACE("Transition rewards: " << rewards);
+ STORM_LOG_WARN("Transition rewards [" << rewards << "] not parsed.");
// TODO save rewards
line = line.substr(posEndReward+1);
}
@@ -217,6 +227,9 @@ namespace storm {
STORM_LOG_TRACE("Finished parsing");
modelComponents->transitionMatrix = builder.build(row + 1, stateSize, nonDeterministic ? stateSize : 0);
+ for (uint64_t i = 0; i < stateRewards.size(); ++i) {
+ modelComponents->rewardModels.emplace("rew" + std::to_string(i), storm::models::sparse::StandardRewardModel<ValueType>(std::move(stateRewards[i])));
+ }
STORM_LOG_TRACE("Built matrix");
return modelComponents;
}
From 1a4bc33e5b2b8692c426414bdbc758bb73c1e7a2 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 10 Oct 2017 11:14:04 +0200
Subject: [PATCH 23/39] Fixed setting of debug settings in storm-dft-cli
---
src/storm-dft-cli/storm-dyftee.cpp | 63 ++++++++++++++++++++----------
1 file changed, 42 insertions(+), 21 deletions(-)
diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index 8eef6f0b5..001adabf4 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -28,6 +28,7 @@
#include "storm-gspn/storm-gspn.h"
#include "storm/settings/modules/GSPNSettings.h"
#include "storm/settings/modules/GSPNExportSettings.h"
+#include "storm-cli-utilities/cli.cpp"
#include <boost/lexical_cast.hpp>
@@ -125,23 +126,12 @@ void initializeSettings() {
storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
}
-/*!
- * Entry point for the DyFTeE backend.
- *
- * @param argc The argc argument of main().
- * @param argv The argv argument of main().
- * @return Return code, 0 if successfull, not 0 otherwise.
- */
-int main(const int argc, const char** argv) {
- try {
- storm::utility::setUp();
- storm::cli::printHeader("Storm-DyFTeE", argc, argv);
- initializeSettings();
-
- bool optionsCorrect = storm::cli::parseOptions(argc, argv);
- if (!optionsCorrect) {
- return -1;
- }
+
+void processOptions() {
+ // Start by setting some urgent options (log levels, resources, etc.)
+ storm::cli::setUrgentOptions();
+
+ storm::cli::processOptions();
storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
@@ -157,7 +147,7 @@ int main(const int argc, const char** argv) {
// Export to json
storm::storage::DftJsonExporter<double>::toFile(dft, dftSettings.getExportJsonFilename());
storm::utility::cleanUp();
- return 0;
+ return;
}
@@ -199,7 +189,7 @@ int main(const int argc, const char** argv) {
delete model;
delete gspn;
storm::utility::cleanUp();
- return 0;
+ return;
}
bool parametric = false;
@@ -216,7 +206,7 @@ int main(const int argc, const char** argv) {
analyzeWithSMT<double>(dftSettings.getDftFilename());
}
storm::utility::cleanUp();
- return 0;
+ return;
}
#endif
@@ -272,7 +262,38 @@ int main(const int argc, const char** argv) {
} else {
analyzeDFT<double>(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
}
-
+}
+
+/*!
+ * Entry point for the DyFTeE backend.
+ *
+ * @param argc The argc argument of main().
+ * @param argv The argv argument of main().
+ * @return Return code, 0 if successfull, not 0 otherwise.
+ */
+/*!
+ * Main entry point of the executable storm-pars.
+ */
+int main(const int argc, const char** argv) {
+ try {
+ storm::utility::setUp();
+ storm::cli::printHeader("Storm-DyFTeE", argc, argv);
+ //storm::settings::initializeParsSettings("Storm-pars", "storm-pars");
+ initializeSettings();
+
+ storm::utility::Stopwatch totalTimer(true);
+ if (!storm::cli::parseOptions(argc, argv)) {
+ return -1;
+ }
+
+ processOptions();
+ //storm::pars::processOptions();
+
+ totalTimer.stop();
+ if (storm::settings::getModule<storm::settings::modules::ResourceSettings>().isPrintTimeAndMemorySet()) {
+ storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds());
+ }
+
// All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp();
return 0;
From 349e276c9b14c39746b4459be354d19f357df24e Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 10 Oct 2017 11:30:25 +0200
Subject: [PATCH 24/39] Removed include of cpp file in storm-pars-cli and
storm-dft-cli
---
src/storm-cli-utilities/cli.cpp | 2 +-
src/storm-cli-utilities/cli.h | 5 +++--
src/storm-dft-cli/CMakeLists.txt | 2 +-
src/storm-dft-cli/storm-dyftee.cpp | 2 --
src/storm-pars-cli/CMakeLists.txt | 2 +-
src/storm-pars-cli/storm-pars.cpp | 3 +--
6 files changed, 7 insertions(+), 9 deletions(-)
diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp
index cb33c3205..3ff4d4593 100644
--- a/src/storm-cli-utilities/cli.cpp
+++ b/src/storm-cli-utilities/cli.cpp
@@ -64,7 +64,7 @@ namespace storm {
}
- void printHeader(std::string const& name, const int argc, const char* argv[]) {
+ void printHeader(std::string const& name, const int argc, const char** argv) {
STORM_PRINT(name << " " << storm::utility::StormVersion::shortVersionString() << std::endl << std::endl);
// "Compute" the command line argument string with which storm was invoked.
diff --git a/src/storm-cli-utilities/cli.h b/src/storm-cli-utilities/cli.h
index 4decbb02c..e8d8601e9 100644
--- a/src/storm-cli-utilities/cli.h
+++ b/src/storm-cli-utilities/cli.h
@@ -11,7 +11,7 @@ namespace storm {
*/
int64_t process(const int argc, const char** argv);
- void printHeader(std::string const& name, const int argc, const char* argv[]);
+ void printHeader(std::string const& name, const int argc, const char** argv);
void printVersion(std::string const& name);
@@ -27,7 +27,8 @@ namespace storm {
bool parseOptions(const int argc, const char* argv[]);
void processOptions();
-
+
+ void setUrgentOptions();
}
}
diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt
index b8cdbbd27..152fc5fc7 100644
--- a/src/storm-dft-cli/CMakeLists.txt
+++ b/src/storm-dft-cli/CMakeLists.txt
@@ -6,4 +6,4 @@ set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft")
add_dependencies(binaries storm-dft-cli)
# installation
-install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
+install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index 001adabf4..b6fb0c751 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -28,8 +28,6 @@
#include "storm-gspn/storm-gspn.h"
#include "storm/settings/modules/GSPNSettings.h"
#include "storm/settings/modules/GSPNExportSettings.h"
-#include "storm-cli-utilities/cli.cpp"
-
#include <boost/lexical_cast.hpp>
#include <memory>
diff --git a/src/storm-pars-cli/CMakeLists.txt b/src/storm-pars-cli/CMakeLists.txt
index bda5ad6c2..9e2f6f315 100644
--- a/src/storm-pars-cli/CMakeLists.txt
+++ b/src/storm-pars-cli/CMakeLists.txt
@@ -1,6 +1,6 @@
# Create storm-pars.
add_executable(storm-pars-cli ${PROJECT_SOURCE_DIR}/src/storm-pars-cli/storm-pars.cpp)
-target_link_libraries(storm-pars-cli storm-pars) # Adding headers for xcode
+target_link_libraries(storm-pars-cli storm-pars storm-cli-utilities) # Adding headers for xcode
set_target_properties(storm-pars-cli PROPERTIES OUTPUT_NAME "storm-pars")
add_dependencies(binaries storm-pars-cli)
diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 5fa744c59..907688ef4 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -7,6 +7,7 @@
#include "storm/settings/SettingsManager.h"
#include "storm/api/storm.h"
#include "storm-cli-utilities/cli.h"
+#include "storm-cli-utilities/model-handling.h"
#include "storm/models/ModelBase.h"
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/utility/file.h"
@@ -23,8 +24,6 @@
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/NotSupportedException.h"
-#include "storm-cli-utilities/cli.cpp"
-
namespace storm {
namespace pars {
From 9350e281c764abe65fd3b6c3656d11e1c61f3e3d Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 10 Oct 2017 11:38:44 +0200
Subject: [PATCH 25/39] Renamed storm-dyftee to storm-dft
---
src/storm-dft-cli/CMakeLists.txt | 2 +-
src/storm-dft-cli/{storm-dyftee.cpp => storm-dft.cpp} | 0
2 files changed, 1 insertion(+), 1 deletion(-)
rename src/storm-dft-cli/{storm-dyftee.cpp => storm-dft.cpp} (100%)
diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt
index 152fc5fc7..4780eef4d 100644
--- a/src/storm-dft-cli/CMakeLists.txt
+++ b/src/storm-dft-cli/CMakeLists.txt
@@ -1,5 +1,5 @@
# Create storm-dft.
-add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp)
+add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dft.cpp)
target_link_libraries(storm-dft-cli storm-dft storm-cli-utilities) # Adding headers for xcode
set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft")
diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dft.cpp
similarity index 100%
rename from src/storm-dft-cli/storm-dyftee.cpp
rename to src/storm-dft-cli/storm-dft.cpp
From 8a74be1b72f429c0959aa351578438792f86d9ed Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 11 Oct 2017 17:57:15 +0200
Subject: [PATCH 26/39] Refactored DFT settings
---
src/storm-dft-cli/storm-dft.cpp | 124 ++++--------
.../builder/ExplicitDFTModelBuilder.cpp | 2 -
.../builder/ExplicitDFTModelBuilderApprox.cpp | 4 +-
.../generator/DftNextStateGenerator.cpp | 4 +-
.../modelchecker/dft/DFTModelChecker.cpp | 4 +-
src/storm-dft/settings/DftSettings.cpp | 51 +++++
src/storm-dft/settings/DftSettings.h | 11 +
.../settings/modules/DFTSettings.cpp | 189 ------------------
.../settings/modules/DftIOSettings.cpp | 123 ++++++++++++
.../{DFTSettings.h => DftIOSettings.h} | 80 +-------
.../settings/modules/FaultTreeSettings.cpp | 93 +++++++++
.../settings/modules/FaultTreeSettings.h | 104 ++++++++++
12 files changed, 432 insertions(+), 357 deletions(-)
create mode 100644 src/storm-dft/settings/DftSettings.cpp
create mode 100644 src/storm-dft/settings/DftSettings.h
delete mode 100644 src/storm-dft/settings/modules/DFTSettings.cpp
create mode 100644 src/storm-dft/settings/modules/DftIOSettings.cpp
rename src/storm-dft/settings/modules/{DFTSettings.h => DftIOSettings.h} (63%)
create mode 100644 src/storm-dft/settings/modules/FaultTreeSettings.cpp
create mode 100644 src/storm-dft/settings/modules/FaultTreeSettings.h
diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index b6fb0c751..3e69fb217 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -1,20 +1,14 @@
-#include "storm/logic/Formula.h"
-#include "storm/utility/initialize.h"
-#include "storm/api/storm.h"
-#include "storm-cli-utilities/cli.h"
-#include "storm/exceptions/BaseException.h"
-
-#include "storm/logic/Formula.h"
+#include "storm-dft/settings/DftSettings.h"
+#include "storm-dft/settings/modules/DftIOSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
#include "storm/settings/modules/IOSettings.h"
-#include "storm/settings/modules/CoreSettings.h"
-#include "storm/settings/modules/DebugSettings.h"
-#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
-#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
-#include "storm/settings/modules/NativeEquationSolverSettings.h"
-#include "storm/settings/modules/EliminationSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
+#include "storm/utility/initialize.h"
+#include "storm/api/storm.h"
+#include "storm-cli-utilities/cli.h"
+
#include "storm-dft/parser/DFTGalileoParser.h"
#include "storm-dft/parser/DFTJsonParser.h"
#include "storm-dft/modelchecker/dft/DFTModelChecker.h"
@@ -22,12 +16,8 @@
#include "storm-dft/transformations/DftToGspnTransformator.h"
#include "storm-dft/storage/dft/DftJsonExporter.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
-
#include "storm-gspn/storage/gspn/GSPN.h"
#include "storm-gspn/storm-gspn.h"
-#include "storm/settings/modules/GSPNSettings.h"
-#include "storm/settings/modules/GSPNExportSettings.h"
#include <boost/lexical_cast.hpp>
#include <memory>
@@ -44,18 +34,18 @@
*/
template <typename ValueType>
void analyzeDFT(std::vector<std::string> const& properties, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
- storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
+ storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
std::shared_ptr<storm::storage::DFT<ValueType>> dft;
// Build DFT from given file.
- if (dftSettings.isDftJsonFileSet()) {
+ if (dftIOSettings.isDftJsonFileSet()) {
storm::parser::DFTJsonParser<ValueType> parser;
- std::cout << "Loading DFT from file " << dftSettings.getDftJsonFilename() << std::endl;
- dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(dftSettings.getDftJsonFilename()));
+ std::cout << "Loading DFT from file " << dftIOSettings.getDftJsonFilename() << std::endl;
+ dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(dftIOSettings.getDftJsonFilename()));
} else {
storm::parser::DFTGalileoParser<ValueType> parser;
- std::cout << "Loading DFT from file " << dftSettings.getDftFilename() << std::endl;
- dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseDFT(dftSettings.getDftFilename()));
+ std::cout << "Loading DFT from file " << dftIOSettings.getDftFilename() << std::endl;
+ dft = std::make_shared<storm::storage::DFT<ValueType>>(parser.parseDFT(dftIOSettings.getDftFilename()));
}
// Build properties
@@ -91,72 +81,39 @@ void analyzeWithSMT(std::string filename) {
//std::cout << "SMT result: " << sat << std::endl;
}
-
-/*!
- * Initialize the settings manager.
- */
-void initializeSettings() {
- storm::settings::mutableManager().setName("Storm-DyFTeE", "storm-dft");
-
- // Register all known settings modules.
- storm::settings::addModule<storm::settings::modules::GeneralSettings>();
- storm::settings::addModule<storm::settings::modules::DFTSettings>();
- storm::settings::addModule<storm::settings::modules::CoreSettings>();
- storm::settings::addModule<storm::settings::modules::DebugSettings>();
- storm::settings::addModule<storm::settings::modules::IOSettings>();
- //storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
- //storm::settings::addModule<storm::settings::modules::CuddSettings>();
- //storm::settings::addModule<storm::settings::modules::SylvanSettings>();
- storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
- storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
- storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
- //storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
- //storm::settings::addModule<storm::settings::modules::GlpkSettings>();
- //storm::settings::addModule<storm::settings::modules::GurobiSettings>();
- //storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
- //storm::settings::addModule<storm::settings::modules::ParametricSettings>();
- storm::settings::addModule<storm::settings::modules::EliminationSettings>();
- storm::settings::addModule<storm::settings::modules::ResourceSettings>();
-
- // For translation into JANI via GSPN.
- storm::settings::addModule<storm::settings::modules::GSPNSettings>();
- storm::settings::addModule<storm::settings::modules::GSPNExportSettings>();
- storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
-}
-
-
void processOptions() {
// Start by setting some urgent options (log levels, resources, etc.)
storm::cli::setUrgentOptions();
storm::cli::processOptions();
- storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
+ storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule<storm::settings::modules::DftIOSettings>();
+ storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule<storm::settings::modules::FaultTreeSettings>();
storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
- if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) {
+ if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
- if (dftSettings.isExportToJson()) {
- STORM_LOG_THROW(dftSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given.");
+ if (dftIOSettings.isExportToJson()) {
+ STORM_LOG_THROW(dftIOSettings.isDftFileSet(), storm::exceptions::InvalidSettingsException, "No input model in Galileo format given.");
storm::parser::DFTGalileoParser<double> parser;
- storm::storage::DFT<double> dft = parser.parseDFT(dftSettings.getDftFilename());
+ storm::storage::DFT<double> dft = parser.parseDFT(dftIOSettings.getDftFilename());
// Export to json
- storm::storage::DftJsonExporter<double>::toFile(dft, dftSettings.getExportJsonFilename());
+ storm::storage::DftJsonExporter<double>::toFile(dft, dftIOSettings.getExportJsonFilename());
storm::utility::cleanUp();
return;
}
- if (dftSettings.isTransformToGspn()) {
+ if (dftIOSettings.isTransformToGspn()) {
std::shared_ptr<storm::storage::DFT<double>> dft;
- if (dftSettings.isDftJsonFileSet()) {
+ if (dftIOSettings.isDftJsonFileSet()) {
storm::parser::DFTJsonParser<double> parser;
- dft = std::make_shared<storm::storage::DFT<double>>(parser.parseJson(dftSettings.getDftJsonFilename()));
+ dft = std::make_shared<storm::storage::DFT<double>>(parser.parseJson(dftIOSettings.getDftJsonFilename()));
} else {
storm::parser::DFTGalileoParser<double> parser(true, false);
- dft = std::make_shared<storm::storage::DFT<double>>(parser.parseDFT(dftSettings.getDftFilename()));
+ dft = std::make_shared<storm::storage::DFT<double>>(parser.parseDFT(dftIOSettings.getDftFilename()));
}
storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(*dft);
gspnTransformator.transform();
@@ -196,12 +153,12 @@ void processOptions() {
#endif
#ifdef STORM_HAVE_Z3
- if (dftSettings.solveWithSMT()) {
+ if (faultTreeSettings.solveWithSMT()) {
// Solve with SMT
if (parametric) {
// analyzeWithSMT<storm::RationalFunction>(dftSettings.getDftFilename());
} else {
- analyzeWithSMT<double>(dftSettings.getDftFilename());
+ analyzeWithSMT<double>(dftIOSettings.getDftFilename());
}
storm::utility::cleanUp();
return;
@@ -210,8 +167,8 @@ void processOptions() {
// Set min or max
std::string optimizationDirection = "min";
- if (dftSettings.isComputeMaximalValue()) {
- STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time.");
+ if (dftIOSettings.isComputeMaximalValue()) {
+ STORM_LOG_THROW(!dftIOSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time.");
optimizationDirection = "max";
}
@@ -221,19 +178,19 @@ void processOptions() {
if (ioSettings.isPropertySet()) {
properties.push_back(ioSettings.getProperty());
}
- if (dftSettings.usePropExpectedTime()) {
+ if (dftIOSettings.usePropExpectedTime()) {
properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]");
}
- if (dftSettings.usePropProbability()) {
+ if (dftIOSettings.usePropProbability()) {
properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]");
}
- if (dftSettings.usePropTimebound()) {
+ if (dftIOSettings.usePropTimebound()) {
std::stringstream stream;
- stream << "P" << optimizationDirection << "=? [F<=" << dftSettings.getPropTimebound() << " \"failed\"]";
+ stream << "P" << optimizationDirection << "=? [F<=" << dftIOSettings.getPropTimebound() << " \"failed\"]";
properties.push_back(stream.str());
}
- if (dftSettings.usePropTimepoints()) {
- for (double timepoint : dftSettings.getPropTimepoints()) {
+ if (dftIOSettings.usePropTimepoints()) {
+ for (double timepoint : dftIOSettings.getPropTimepoints()) {
std::stringstream stream;
stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]";
properties.push_back(stream.str());
@@ -246,19 +203,19 @@ void processOptions() {
// Set possible approximation error
double approximationError = 0.0;
- if (dftSettings.isApproximationErrorSet()) {
- approximationError = dftSettings.getApproximationError();
+ if (faultTreeSettings.isApproximationErrorSet()) {
+ approximationError = faultTreeSettings.getApproximationError();
}
// From this point on we are ready to carry out the actual computations.
if (parametric) {
#ifdef STORM_HAVE_CARL
- analyzeDFT<storm::RationalFunction>(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
+ analyzeDFT<storm::RationalFunction>(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError);
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build.");
#endif
} else {
- analyzeDFT<double>(properties, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
+ analyzeDFT<double>(properties, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), approximationError);
}
}
@@ -275,9 +232,8 @@ void processOptions() {
int main(const int argc, const char** argv) {
try {
storm::utility::setUp();
- storm::cli::printHeader("Storm-DyFTeE", argc, argv);
- //storm::settings::initializeParsSettings("Storm-pars", "storm-pars");
- initializeSettings();
+ storm::cli::printHeader("Storm-dft", argc, argv);
+ storm::settings::initializeDftSettings("Storm-dft", "storm-dft");
storm::utility::Stopwatch totalTimer(true);
if (!storm::cli::parseOptions(argc, argv)) {
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index 4a29b0652..5ef6bd07e 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -9,8 +9,6 @@
#include "storm/exceptions/UnexpectedException.h"
#include "storm/settings/SettingsManager.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
-
namespace storm {
namespace builder {
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
index 0c7d69628..f035b0a55 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -10,7 +10,7 @@
#include "storm/exceptions/UnexpectedException.h"
#include "storm/settings/SettingsManager.h"
#include "storm/logic/AtomicLabelFormula.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
namespace storm {
@@ -55,7 +55,7 @@ namespace storm {
dft(dft),
stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
enableDC(enableDC),
- usedHeuristic(storm::settings::getModule<storm::settings::modules::DFTSettings>().getApproximationHeuristic()),
+ usedHeuristic(storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().getApproximationHeuristic()),
generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
matrixBuilder(!generator.isDeterministicModel()),
stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp
index 7b86d1faa..0002cd6a3 100644
--- a/src/storm-dft/generator/DftNextStateGenerator.cpp
+++ b/src/storm-dft/generator/DftNextStateGenerator.cpp
@@ -4,7 +4,7 @@
#include "storm/utility/macros.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/settings/SettingsManager.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
namespace storm {
namespace generator {
@@ -71,7 +71,7 @@ namespace storm {
// Let BE fail
while (currentFailable < failableCount) {
- if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isTakeFirstDependency() && hasDependencies && currentFailable > 0) {
+ if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isTakeFirstDependency() && hasDependencies && currentFailable > 0) {
// We discard further exploration as we already chose one dependent event
break;
}
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index d6b7e9138..45d97baa6 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -8,7 +8,7 @@
#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h"
#include "storm-dft/storage/dft/DFTIsomorphism.h"
-#include "storm-dft/settings/modules/DFTSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
namespace storm {
@@ -344,7 +344,7 @@ namespace storm {
STORM_LOG_INFO("Building Model...");
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
// TODO Matthias: use only one builder if everything works again
- if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isApproximationErrorSet()) {
+ if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isApproximationErrorSet()) {
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
builder.buildModel(labeloptions, 0, 0.0);
diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp
new file mode 100644
index 000000000..ce48c6fd9
--- /dev/null
+++ b/src/storm-dft/settings/DftSettings.cpp
@@ -0,0 +1,51 @@
+#include "storm-dft/settings/DftSettings.h"
+
+#include "storm-dft/settings/modules/DftIOSettings.h"
+#include "storm-dft/settings/modules/FaultTreeSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/DebugSettings.h"
+#include "storm/settings/modules/EigenEquationSolverSettings.h"
+#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
+#include "storm/settings/modules/NativeEquationSolverSettings.h"
+#include "storm/settings/modules/EliminationSettings.h"
+#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
+#include "storm/settings/modules/BisimulationSettings.h"
+#include "storm/settings/modules/ResourceSettings.h"
+#include "storm/settings/modules/JaniExportSettings.h"
+#include "storm/settings/modules/GSPNSettings.h"
+#include "storm/settings/modules/GSPNExportSettings.h"
+
+
+namespace storm {
+ namespace settings {
+ void initializeDftSettings(std::string const& name, std::string const& executableName) {
+ storm::settings::mutableManager().setName(name, executableName);
+
+ // Register relevant settings modules.
+ storm::settings::addModule<storm::settings::modules::GeneralSettings>();
+ storm::settings::addModule<storm::settings::modules::DftIOSettings>();
+ storm::settings::addModule<storm::settings::modules::FaultTreeSettings>();
+ storm::settings::addModule<storm::settings::modules::IOSettings>();
+ storm::settings::addModule<storm::settings::modules::CoreSettings>();
+
+ storm::settings::addModule<storm::settings::modules::DebugSettings>();
+ storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
+ storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
+ storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>();
+ storm::settings::addModule<storm::settings::modules::EliminationSettings>();
+ storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
+ // storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
+ storm::settings::addModule<storm::settings::modules::ResourceSettings>();
+
+ // For translation into JANI via GSPN.
+ storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
+ storm::settings::addModule<storm::settings::modules::GSPNSettings>();
+ storm::settings::addModule<storm::settings::modules::GSPNExportSettings>();
+ }
+
+ }
+}
diff --git a/src/storm-dft/settings/DftSettings.h b/src/storm-dft/settings/DftSettings.h
new file mode 100644
index 000000000..8f67ec0b7
--- /dev/null
+++ b/src/storm-dft/settings/DftSettings.h
@@ -0,0 +1,11 @@
+#pragma once
+
+#include <string>
+
+namespace storm {
+ namespace settings {
+
+ void initializeDftSettings(std::string const& name, std::string const& executableName);
+
+ }
+}
diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp
deleted file mode 100644
index 1a8d59d70..000000000
--- a/src/storm-dft/settings/modules/DFTSettings.cpp
+++ /dev/null
@@ -1,189 +0,0 @@
-#include "DFTSettings.h"
-
-#include "storm/settings/SettingsManager.h"
-#include "storm/settings/SettingMemento.h"
-#include "storm/settings/Option.h"
-#include "storm/settings/OptionBuilder.h"
-#include "storm/settings/ArgumentBuilder.h"
-#include "storm/settings/Argument.h"
-
-#include "storm/exceptions/InvalidSettingsException.h"
-#include "storm/exceptions/IllegalArgumentValueException.h"
-
-namespace storm {
- namespace settings {
- namespace modules {
-
- const std::string DFTSettings::moduleName = "dft";
- const std::string DFTSettings::dftFileOptionName = "dftfile";
- const std::string DFTSettings::dftFileOptionShortName = "dft";
- const std::string DFTSettings::dftJsonFileOptionName = "dftfile-json";
- const std::string DFTSettings::dftJsonFileOptionShortName = "dftjson";
- const std::string DFTSettings::symmetryReductionOptionName = "symmetryreduction";
- const std::string DFTSettings::symmetryReductionOptionShortName = "symred";
- const std::string DFTSettings::modularisationOptionName = "modularisation";
- const std::string DFTSettings::disableDCOptionName = "disabledc";
- const std::string DFTSettings::approximationErrorOptionName = "approximation";
- const std::string DFTSettings::approximationErrorOptionShortName = "approx";
- const std::string DFTSettings::approximationHeuristicOptionName = "approximationheuristic";
- const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime";
- const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf";
- const std::string DFTSettings::propProbabilityOptionName = "probability";
- const std::string DFTSettings::propTimeboundOptionName = "timebound";
- const std::string DFTSettings::propTimepointsOptionName = "timepoints";
- const std::string DFTSettings::minValueOptionName = "min";
- const std::string DFTSettings::maxValueOptionName = "max";
- const std::string DFTSettings::firstDependencyOptionName = "firstdep";
- const std::string DFTSettings::transformToGspnOptionName = "gspn";
- const std::string DFTSettings::exportToJsonOptionName = "export-json";
-#ifdef STORM_HAVE_Z3
- const std::string DFTSettings::solveWithSmtOptionName = "smt";
-#endif
-
- DFTSettings::DFTSettings() : ModuleSettings(moduleName) {
- this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build());
-#ifdef STORM_HAVE_Z3
- this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build());
-#endif
- this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build());
- }
-
- bool DFTSettings::isDftFileSet() const {
- return this->getOption(dftFileOptionName).getHasOptionBeenSet();
- }
-
- std::string DFTSettings::getDftFilename() const {
- return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString();
- }
-
- bool DFTSettings::isDftJsonFileSet() const {
- return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet();
- }
-
- std::string DFTSettings::getDftJsonFilename() const {
- return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString();
- }
-
- bool DFTSettings::useSymmetryReduction() const {
- return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::useModularisation() const {
- return this->getOption(modularisationOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::isDisableDC() const {
- return this->getOption(disableDCOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::isApproximationErrorSet() const {
- return this->getOption(approximationErrorOptionName).getHasOptionBeenSet();
- }
-
- double DFTSettings::getApproximationError() const {
- return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble();
- }
-
- storm::builder::ApproximationHeuristic DFTSettings::getApproximationHeuristic() const {
- if (!isApproximationErrorSet() || getApproximationError() == 0.0) {
- // No approximation is done
- return storm::builder::ApproximationHeuristic::NONE;
- }
- std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString();
- if (heuristicAsString == "depth") {
- return storm::builder::ApproximationHeuristic::DEPTH;
- } else if (heuristicAsString == "probability") {
- return storm::builder::ApproximationHeuristic::PROBABILITY;
- }
- STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation.");
- }
-
- bool DFTSettings::usePropExpectedTime() const {
- return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::usePropProbability() const {
- return this->getOption(propProbabilityOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::usePropTimebound() const {
- return this->getOption(propTimeboundOptionName).getHasOptionBeenSet();
- }
-
- double DFTSettings::getPropTimebound() const {
- return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble();
- }
-
- bool DFTSettings::usePropTimepoints() const {
- return this->getOption(propTimepointsOptionName).getHasOptionBeenSet();
- }
-
- std::vector<double> DFTSettings::getPropTimepoints() const {
- double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble();
- double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble();
- double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble();
- std::vector<double> timepoints;
- for (double time = starttime; time <= endtime; time += inc) {
- timepoints.push_back(time);
- }
- return timepoints;
- }
-
- bool DFTSettings::isComputeMinimalValue() const {
- return this->getOption(minValueOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::isComputeMaximalValue() const {
- return this->getOption(maxValueOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::isTakeFirstDependency() const {
- return this->getOption(firstDependencyOptionName).getHasOptionBeenSet();
- }
-
-#ifdef STORM_HAVE_Z3
- bool DFTSettings::solveWithSMT() const {
- return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet();
- }
-#endif
-
- bool DFTSettings::isTransformToGspn() const {
- return this->getOption(transformToGspnOptionName).getHasOptionBeenSet();
- }
-
- bool DFTSettings::isExportToJson() const {
- return this->getOption(exportToJsonOptionName).getHasOptionBeenSet();
- }
-
- std::string DFTSettings::getExportJsonFilename() const {
- return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString();
- }
-
- void DFTSettings::finalize() {
- }
-
- bool DFTSettings::check() const {
- // Ensure that at most one of min or max is set
- STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set.");
- return true;
- }
-
- } // namespace modules
- } // namespace settings
-} // namespace storm
diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp
new file mode 100644
index 000000000..cf656333d
--- /dev/null
+++ b/src/storm-dft/settings/modules/DftIOSettings.cpp
@@ -0,0 +1,123 @@
+#include "DftIOSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+#include "storm/exceptions/InvalidSettingsException.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ const std::string DftIOSettings::moduleName = "dftIO";
+ const std::string DftIOSettings::dftFileOptionName = "dftfile";
+ const std::string DftIOSettings::dftFileOptionShortName = "dft";
+ const std::string DftIOSettings::dftJsonFileOptionName = "dftfile-json";
+ const std::string DftIOSettings::dftJsonFileOptionShortName = "dftjson";
+ const std::string DftIOSettings::propExpectedTimeOptionName = "expectedtime";
+ const std::string DftIOSettings::propExpectedTimeOptionShortName = "mttf";
+ const std::string DftIOSettings::propProbabilityOptionName = "probability";
+ const std::string DftIOSettings::propTimeboundOptionName = "timebound";
+ const std::string DftIOSettings::propTimepointsOptionName = "timepoints";
+ const std::string DftIOSettings::minValueOptionName = "min";
+ const std::string DftIOSettings::maxValueOptionName = "max";
+ const std::string DftIOSettings::transformToGspnOptionName = "gspn";
+ const std::string DftIOSettings::exportToJsonOptionName = "export-json";
+
+ DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) {
+ this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build());
+ }
+
+ bool DftIOSettings::isDftFileSet() const {
+ return this->getOption(dftFileOptionName).getHasOptionBeenSet();
+ }
+
+ std::string DftIOSettings::getDftFilename() const {
+ return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString();
+ }
+
+ bool DftIOSettings::isDftJsonFileSet() const {
+ return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet();
+ }
+
+ std::string DftIOSettings::getDftJsonFilename() const {
+ return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString();
+ }
+
+ bool DftIOSettings::usePropExpectedTime() const {
+ return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet();
+ }
+
+ bool DftIOSettings::usePropProbability() const {
+ return this->getOption(propProbabilityOptionName).getHasOptionBeenSet();
+ }
+
+ bool DftIOSettings::usePropTimebound() const {
+ return this->getOption(propTimeboundOptionName).getHasOptionBeenSet();
+ }
+
+ double DftIOSettings::getPropTimebound() const {
+ return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble();
+ }
+
+ bool DftIOSettings::usePropTimepoints() const {
+ return this->getOption(propTimepointsOptionName).getHasOptionBeenSet();
+ }
+
+ std::vector<double> DftIOSettings::getPropTimepoints() const {
+ double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble();
+ double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble();
+ double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble();
+ std::vector<double> timepoints;
+ for (double time = starttime; time <= endtime; time += inc) {
+ timepoints.push_back(time);
+ }
+ return timepoints;
+ }
+
+ bool DftIOSettings::isComputeMinimalValue() const {
+ return this->getOption(minValueOptionName).getHasOptionBeenSet();
+ }
+
+ bool DftIOSettings::isComputeMaximalValue() const {
+ return this->getOption(maxValueOptionName).getHasOptionBeenSet();
+ }
+
+ bool DftIOSettings::isTransformToGspn() const {
+ return this->getOption(transformToGspnOptionName).getHasOptionBeenSet();
+ }
+
+ bool DftIOSettings::isExportToJson() const {
+ return this->getOption(exportToJsonOptionName).getHasOptionBeenSet();
+ }
+
+ std::string DftIOSettings::getExportJsonFilename() const {
+ return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString();
+ }
+
+ void DftIOSettings::finalize() {
+ }
+
+ bool DftIOSettings::check() const {
+ // Ensure that at most one of min or max is set
+ STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set.");
+ return true;
+ }
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h
similarity index 63%
rename from src/storm-dft/settings/modules/DFTSettings.h
rename to src/storm-dft/settings/modules/DftIOSettings.h
index c04ef1a23..8a8fbcdd1 100644
--- a/src/storm-dft/settings/modules/DFTSettings.h
+++ b/src/storm-dft/settings/modules/DftIOSettings.h
@@ -1,24 +1,21 @@
#pragma once
-#include "storm-config.h"
#include "storm/settings/modules/ModuleSettings.h"
-#include "storm-dft/builder/DftExplorationHeuristic.h"
-
namespace storm {
namespace settings {
namespace modules {
/*!
- * This class represents the settings for DFT model checking.
+ * This class represents the settings for IO operations concerning DFTs.
*/
- class DFTSettings : public ModuleSettings {
+ class DftIOSettings : public ModuleSettings {
public:
/*!
- * Creates a new set of DFT settings.
+ * Creates a new set of IO settings for DFTs.
*/
- DFTSettings();
+ DftIOSettings();
/*!
* Retrieves whether the dft file option was set.
@@ -48,48 +45,6 @@ namespace storm {
*/
std::string getDftJsonFilename() const;
- /*!
- * Retrieves whether the option to use symmetry reduction is set.
- *
- * @return True iff the option was set.
- */
- bool useSymmetryReduction() const;
-
- /*!
- * Retrieves whether the option to use modularisation is set.
- *
- * @return True iff the option was set.
- */
- bool useModularisation() const;
-
- /*!
- * Retrieves whether the option to disable Dont Care propagation is set.
- *
- * @return True iff the option was set.
- */
- bool isDisableDC() const;
-
- /*!
- * Retrieves whether the option to compute an approximation is set.
- *
- * @return True iff the option was set.
- */
- bool isApproximationErrorSet() const;
-
- /*!
- * Retrieves the relative error allowed for approximating the model checking result.
- *
- * @return The allowed errorbound.
- */
- double getApproximationError() const;
-
- /*!
- * Retrieves the heuristic used for approximation.
- *
- * @return The heuristic to use.
- */
- storm::builder::ApproximationHeuristic getApproximationHeuristic() const;
-
/*!
* Retrieves whether the property expected time should be used.
*
@@ -146,13 +101,6 @@ namespace storm {
*/
bool isComputeMaximalValue() const;
- /*!
- * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency.
- *
- * @return True iff the option was set.
- */
- bool isTakeFirstDependency() const;
-
/*!
* Retrieves whether the DFT should be transformed into a GSPN.
*
@@ -174,15 +122,6 @@ namespace storm {
*/
std::string getExportJsonFilename() const;
-#ifdef STORM_HAVE_Z3
- /*!
- * Retrieves whether the DFT should be checked via SMT.
- *
- * @return True iff the option was set.
- */
- bool solveWithSMT() const;
-#endif
-
bool check() const override;
void finalize() override;
@@ -195,13 +134,6 @@ namespace storm {
static const std::string dftFileOptionShortName;
static const std::string dftJsonFileOptionName;
static const std::string dftJsonFileOptionShortName;
- static const std::string symmetryReductionOptionName;
- static const std::string symmetryReductionOptionShortName;
- static const std::string modularisationOptionName;
- static const std::string disableDCOptionName;
- static const std::string approximationErrorOptionName;
- static const std::string approximationErrorOptionShortName;
- static const std::string approximationHeuristicOptionName;
static const std::string propExpectedTimeOptionName;
static const std::string propExpectedTimeOptionShortName;
static const std::string propProbabilityOptionName;
@@ -209,10 +141,6 @@ namespace storm {
static const std::string propTimepointsOptionName;
static const std::string minValueOptionName;
static const std::string maxValueOptionName;
- static const std::string firstDependencyOptionName;
-#ifdef STORM_HAVE_Z3
- static const std::string solveWithSmtOptionName;
-#endif
static const std::string transformToGspnOptionName;
static const std::string exportToJsonOptionName;
diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp
new file mode 100644
index 000000000..7c9ef14af
--- /dev/null
+++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp
@@ -0,0 +1,93 @@
+#include "FaultTreeSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+#include "storm/exceptions/IllegalArgumentValueException.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ const std::string FaultTreeSettings::moduleName = "dft";
+ const std::string FaultTreeSettings::symmetryReductionOptionName = "symmetryreduction";
+ const std::string FaultTreeSettings::symmetryReductionOptionShortName = "symred";
+ const std::string FaultTreeSettings::modularisationOptionName = "modularisation";
+ const std::string FaultTreeSettings::disableDCOptionName = "disabledc";
+ const std::string FaultTreeSettings::approximationErrorOptionName = "approximation";
+ const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx";
+ const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic";
+ const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep";
+#ifdef STORM_HAVE_Z3
+ const std::string FaultTreeSettings::solveWithSmtOptionName = "smt";
+#endif
+
+ FaultTreeSettings::FaultTreeSettings() : ModuleSettings(moduleName) {
+ this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build());
+#ifdef STORM_HAVE_Z3
+ this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build());
+#endif
+ }
+
+ bool FaultTreeSettings::useSymmetryReduction() const {
+ return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet();
+ }
+
+ bool FaultTreeSettings::useModularisation() const {
+ return this->getOption(modularisationOptionName).getHasOptionBeenSet();
+ }
+
+ bool FaultTreeSettings::isDisableDC() const {
+ return this->getOption(disableDCOptionName).getHasOptionBeenSet();
+ }
+
+ bool FaultTreeSettings::isApproximationErrorSet() const {
+ return this->getOption(approximationErrorOptionName).getHasOptionBeenSet();
+ }
+
+ double FaultTreeSettings::getApproximationError() const {
+ return this->getOption(approximationErrorOptionName).getArgumentByName("error").getValueAsDouble();
+ }
+
+ storm::builder::ApproximationHeuristic FaultTreeSettings::getApproximationHeuristic() const {
+ if (!isApproximationErrorSet() || getApproximationError() == 0.0) {
+ // No approximation is done
+ return storm::builder::ApproximationHeuristic::NONE;
+ }
+ std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString();
+ if (heuristicAsString == "depth") {
+ return storm::builder::ApproximationHeuristic::DEPTH;
+ } else if (heuristicAsString == "probability") {
+ return storm::builder::ApproximationHeuristic::PROBABILITY;
+ }
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation.");
+ }
+
+ bool FaultTreeSettings::isTakeFirstDependency() const {
+ return this->getOption(firstDependencyOptionName).getHasOptionBeenSet();
+ }
+
+#ifdef STORM_HAVE_Z3
+ bool FaultTreeSettings::solveWithSMT() const {
+ return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet();
+ }
+#endif
+
+ void FaultTreeSettings::finalize() {
+ }
+
+ bool FaultTreeSettings::check() const {
+ return true;
+ }
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h
new file mode 100644
index 000000000..171d5c38e
--- /dev/null
+++ b/src/storm-dft/settings/modules/FaultTreeSettings.h
@@ -0,0 +1,104 @@
+#pragma once
+
+#include "storm/settings/modules/ModuleSettings.h"
+#include "storm-dft/builder/DftExplorationHeuristic.h"
+#include "storm-config.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ /*!
+ * This class represents the settings for DFT model checking.
+ */
+ class FaultTreeSettings : public ModuleSettings {
+ public:
+
+ /*!
+ * Creates a new set of DFT settings.
+ */
+ FaultTreeSettings();
+
+ /*!
+ * Retrieves whether the option to use symmetry reduction is set.
+ *
+ * @return True iff the option was set.
+ */
+ bool useSymmetryReduction() const;
+
+ /*!
+ * Retrieves whether the option to use modularisation is set.
+ *
+ * @return True iff the option was set.
+ */
+ bool useModularisation() const;
+
+ /*!
+ * Retrieves whether the option to disable Dont Care propagation is set.
+ *
+ * @return True iff the option was set.
+ */
+ bool isDisableDC() const;
+
+ /*!
+ * Retrieves whether the option to compute an approximation is set.
+ *
+ * @return True iff the option was set.
+ */
+ bool isApproximationErrorSet() const;
+
+ /*!
+ * Retrieves the relative error allowed for approximating the model checking result.
+ *
+ * @return The allowed errorbound.
+ */
+ double getApproximationError() const;
+
+ /*!
+ * Retrieves the heuristic used for approximation.
+ *
+ * @return The heuristic to use.
+ */
+ storm::builder::ApproximationHeuristic getApproximationHeuristic() const;
+
+ /*!
+ * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency.
+ *
+ * @return True iff the option was set.
+ */
+ bool isTakeFirstDependency() const;
+
+#ifdef STORM_HAVE_Z3
+ /*!
+ * Retrieves whether the DFT should be checked via SMT.
+ *
+ * @return True iff the option was set.
+ */
+ bool solveWithSMT() const;
+#endif
+
+ bool check() const override;
+ void finalize() override;
+
+ // The name of the module.
+ static const std::string moduleName;
+
+ private:
+ // Define the string names of the options as constants.
+ static const std::string symmetryReductionOptionName;
+ static const std::string symmetryReductionOptionShortName;
+ static const std::string modularisationOptionName;
+ static const std::string disableDCOptionName;
+ static const std::string approximationErrorOptionName;
+ static const std::string approximationErrorOptionShortName;
+ static const std::string approximationHeuristicOptionName;
+ static const std::string firstDependencyOptionName;
+#ifdef STORM_HAVE_Z3
+ static const std::string solveWithSmtOptionName;
+#endif
+
+ };
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
From 5ad60051c32c13eeeabaa0cb30853a16f0f33b83 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 11 Oct 2017 18:50:53 +0200
Subject: [PATCH 27/39] Region model checker can now also return a
(quantitative) upper/lower bound for a given region
---
.../modelchecker/region/RegionModelChecker.cpp | 7 +++++++
.../modelchecker/region/RegionModelChecker.h | 2 ++
.../region/SparseParameterLiftingModelChecker.cpp | 13 +++++++++++++
.../region/SparseParameterLiftingModelChecker.h | 3 +++
4 files changed, 25 insertions(+)
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
index 23ba29489..ab0142d0b 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
@@ -17,6 +17,7 @@
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"
+#include "storm/exceptions/NotImplementedException.h"
namespace storm {
@@ -43,6 +44,12 @@ namespace storm {
return std::make_unique<storm::modelchecker::RegionCheckResult<ParametricType>>(std::move(result));
}
+ template <typename ParametricType>
+ ParametricType RegionModelChecker<ParametricType>::getBoundAtInitState(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+ STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The selected region model checker does not support this functionality.");
+ return storm::utility::zero<ParametricType>();
+ }
+
template <typename ParametricType>
std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> RegionModelChecker<ParametricType>::performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold, boost::optional<uint64_t> depthThreshold, RegionResultHypothesis const& hypothesis) {
STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h
index c1a558800..595d1e8f0 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.h
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h
@@ -42,6 +42,8 @@ namespace storm {
*/
std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> analyzeRegions(std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, std::vector<RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegion = false) ;
+ virtual ParametricType getBoundAtInitState(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+
/*!
* Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated).
* @param region the considered region
diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
index d0b2af22b..1accd68cc 100644
--- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
@@ -4,6 +4,7 @@
#include "storm/logic/FragmentSpecification.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/utility/vector.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
@@ -130,6 +131,18 @@ namespace storm {
}
}
+ template <typename SparseModelType, typename ConstantType>
+ std::unique_ptr<QuantitativeCheckResult<ConstantType>> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBound(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+ STORM_LOG_WARN_COND(this->currentCheckTask->getFormula().hasQuantitativeResult(), "Computing quantitative bounds for a qualitative formula...");
+ return std::make_unique<ExplicitQuantitativeCheckResult<ConstantType>>(std::move(computeQuantitativeValues(region, dirForParameters)->template asExplicitQuantitativeCheckResult<ConstantType>()));
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ typename SparseModelType::ValueType SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBoundAtInitState(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+ STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Getting a bound at the initial state requires a model with a single initial state.");
+ return storm::utility::convertNumber<typename SparseModelType::ValueType>(getBound(region, dirForParameters)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()]);
+ }
+
template <typename SparseModelType, typename ConstantType>
SparseModelType const& SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getConsideredParametricModel() const {
return *parametricModel;
diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
index e0cabd5f0..cb993ad4f 100644
--- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
@@ -45,6 +45,9 @@ namespace storm {
*/
std::unique_ptr<CheckResult> check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+ std::unique_ptr<QuantitativeCheckResult<ConstantType>> getBound(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+ virtual typename SparseModelType::ValueType getBoundAtInitState(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
+
SparseModelType const& getConsideredParametricModel() const;
CheckTask<storm::logic::Formula, ConstantType> const& getCurrentCheckTask() const;
From 91bd638c1876120132994acbb3200eaa4c815d33 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 10:46:53 +0200
Subject: [PATCH 28/39] Fixed segfault
---
src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
index f035b0a55..c7d6605f5 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -581,13 +581,13 @@ namespace storm {
maComponents.rateTransitions = true;
maComponents.markovianStates = modelComponents.markovianStates;
maComponents.exitRates = modelComponents.exitRates;
- std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
+ ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
} else {
storm::storage::sparse::ModelComponents<ValueType> maComponents(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
maComponents.rateTransitions = true;
maComponents.markovianStates = std::move(modelComponents.markovianStates);
maComponents.exitRates = std::move(modelComponents.exitRates);
- std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
+ ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(maComponents));
}
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC
From 983e09fd635b1911821e88b7373a1dd58e8bbc1b Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 18:18:36 +0200
Subject: [PATCH 29/39] Fixed possible problem with rates and exit rates in MA
---
src/storm/models/sparse/MarkovAutomaton.cpp | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp
index 485aa8a64..8bc00fa99 100644
--- a/src/storm/models/sparse/MarkovAutomaton.cpp
+++ b/src/storm/models/sparse/MarkovAutomaton.cpp
@@ -50,7 +50,9 @@ namespace storm {
if (components.exitRates) {
exitRates = std::move(components.exitRates.get());
- } else {
+ }
+
+ if (components.rateTransitions) {
this->turnRatesToProbabilities();
}
closed = this->checkIsClosed();
From 88544a9ec79bf7a4613eaf05fba64895701951d3 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 18:19:36 +0200
Subject: [PATCH 30/39] Added assertion for turnRatesToProbabilities in MA
---
src/storm/models/sparse/MarkovAutomaton.cpp | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp
index 8bc00fa99..ca79ccfac 100644
--- a/src/storm/models/sparse/MarkovAutomaton.cpp
+++ b/src/storm/models/sparse/MarkovAutomaton.cpp
@@ -152,7 +152,7 @@ namespace storm {
uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state];
if (this->markovianStates.get(state)) {
if (assertRates) {
- STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << ".");
+ STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << ".");
} else {
this->exitRates.push_back(this->getTransitionMatrix().getRowSum(row));
}
@@ -161,7 +161,11 @@ namespace storm {
}
++row;
} else {
- this->exitRates.push_back(storm::utility::zero<ValueType>());
+ if (assertRates) {
+ STORM_LOG_THROW(storm::utility::isZero<ValueType>(this->exitRates[state]), storm::exceptions::InvalidArgumentException, "The specified exit rate for (non-Markovian) choice should be 0.");
+ } else {
+ this->exitRates.push_back(storm::utility::zero<ValueType>());
+ }
}
for (; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) {
STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Entries of transition matrix do not sum up to one for (non-Markovian) choice " << row << " of state " << state << " (sum is " << this->getTransitionMatrix().getRowSum(row) << ").");
From 4456069e81e995d844bb7e447832f5f258488da5 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 18:19:52 +0200
Subject: [PATCH 31/39] Fixed typo
---
src/storm/models/sparse/MarkovAutomaton.h | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h
index 249766b62..89c73f83c 100644
--- a/src/storm/models/sparse/MarkovAutomaton.h
+++ b/src/storm/models/sparse/MarkovAutomaton.h
@@ -22,7 +22,7 @@ namespace storm {
* For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first
* choice corresponds to the markovian transitions.
*
- * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices).
+ * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (Markovian choices) and probabilities (probabilistic choices).
* @param stateLabeling The labeling of the states.
* @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition).
* @param rewardModels A mapping of reward model names to reward models.
@@ -38,7 +38,7 @@ namespace storm {
* For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first
* choice corresponds to the markovian transitions.
*
- * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices).
+ * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (Markovian choices) and probabilities (probabilistic choices).
* @param stateLabeling The labeling of the states.
* @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition).
* @param rewardModels A mapping of reward model names to reward models.
From 87778a677526a11651a912601b35b45a9896edcf Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 20:33:24 +0200
Subject: [PATCH 32/39] Finally removed old DFTModelBuilder
---
.../builder/ExplicitDFTModelBuilder.cpp | 471 ------------------
.../builder/ExplicitDFTModelBuilder.h | 102 ----
.../modelchecker/dft/DFTModelChecker.cpp | 17 +-
3 files changed, 4 insertions(+), 586 deletions(-)
delete mode 100644 src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
delete mode 100644 src/storm-dft/builder/ExplicitDFTModelBuilder.h
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
deleted file mode 100644
index 5ef6bd07e..000000000
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ /dev/null
@@ -1,471 +0,0 @@
-#include "ExplicitDFTModelBuilder.h"
-
-#include <map>
-
-#include "storm/models/sparse/MarkovAutomaton.h"
-#include "storm/models/sparse/Ctmc.h"
-#include "storm/utility/constants.h"
-#include "storm/utility/vector.h"
-#include "storm/exceptions/UnexpectedException.h"
-#include "storm/settings/SettingsManager.h"
-
-
-namespace storm {
- namespace builder {
-
- template <typename ValueType>
- ExplicitDFTModelBuilder<ValueType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
- // Intentionally left empty.
- }
-
- template <typename ValueType>
- ExplicitDFTModelBuilder<ValueType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : mDft(dft), mStates(((mDft.stateVectorSize() / 64) + 1) * 64, INITIAL_BUCKETSIZE), enableDC(enableDC) {
- // stateVectorSize is bound for size of bitvector
-
- mStateGenerationInfo = std::make_shared<storm::storage::DFTStateGenerationInfo>(mDft.buildStateGenerationInfo(symmetries));
- }
-
-
- template <typename ValueType>
- std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType>::buildModel(LabelOptions const& labelOpts) {
- // Initialize
- bool deterministicModel = false;
- size_t rowOffset = 0;
- ModelComponents modelComponents;
- std::vector<uint_fast64_t> tmpMarkovianStates;
- storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
-
- if(mergeFailedStates) {
- // Introduce explicit fail state
- failedIndex = newIndex;
- newIndex++;
- transitionMatrixBuilder.newRowGroup(failedIndex);
- transitionMatrixBuilder.addNextValue(failedIndex, failedIndex, storm::utility::one<ValueType>());
- STORM_LOG_TRACE("Introduce fail state with id: " << failedIndex);
- modelComponents.exitRates.push_back(storm::utility::one<ValueType>());
- tmpMarkovianStates.push_back(failedIndex);
- }
-
- // Explore state space
- DFTStatePointer state = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, *mStateGenerationInfo, newIndex);
- auto exploreResult = exploreStates(state, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
- initialStateIndex = exploreResult.first;
- bool deterministic = exploreResult.second;
-
- // Before ending the exploration check for pseudo states which are not initialized yet
- for (auto & pseudoStatePair : mPseudoStatesMapping) {
- if (pseudoStatePair.first == 0) {
- // Create state from pseudo state and explore
- STORM_LOG_ASSERT(mStates.contains(pseudoStatePair.second), "Pseudo state not contained.");
- STORM_LOG_ASSERT(mStates.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
- STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second);
- DFTStatePointer pseudoState = std::make_shared<storm::storage::DFTState<ValueType>>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex);
- pseudoState->construct();
- STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide.");
- STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId());
- auto exploreResult = exploreStates(pseudoState, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates);
- deterministic &= exploreResult.second;
- STORM_LOG_ASSERT(pseudoStatePair.first == pseudoState->getId(), "Pseudo state ids do not coincide");
- STORM_LOG_ASSERT(pseudoState->getId() == exploreResult.first, "Pseudo state ids do not coincide.");
- }
- }
-
- // Replace pseudo states in matrix
- std::vector<uint_fast64_t> pseudoStatesVector;
- for (auto const& pseudoStatePair : mPseudoStatesMapping) {
- pseudoStatesVector.push_back(pseudoStatePair.first);
- }
- STORM_LOG_ASSERT(std::find(pseudoStatesVector.begin(), pseudoStatesVector.end(), 0) == pseudoStatesVector.end(), "Unexplored pseudo state still contained.");
- transitionMatrixBuilder.replaceColumns(pseudoStatesVector, OFFSET_PSEUDO_STATE);
-
- STORM_LOG_DEBUG("Generated " << mStates.size() + (mergeFailedStates ? 1 : 0) << " states");
- STORM_LOG_DEBUG("Model is " << (deterministic ? "deterministic" : "non-deterministic"));
-
- size_t stateSize = mStates.size() + (mergeFailedStates ? 1 : 0);
- // Build Markov Automaton
- modelComponents.markovianStates = storm::storage::BitVector(stateSize, tmpMarkovianStates);
- // Build transition matrix
- modelComponents.transitionMatrix = transitionMatrixBuilder.build(stateSize, stateSize);
- if (stateSize <= 15) {
- STORM_LOG_TRACE("Transition matrix: " << std::endl << modelComponents.transitionMatrix);
- } else {
- STORM_LOG_TRACE("Transition matrix: too big to print");
- }
- STORM_LOG_TRACE("Exit rates: " << storm::utility::vector::toString<ValueType>(modelComponents.exitRates));
- STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates);
-
- // Build state labeling
- modelComponents.stateLabeling = storm::models::sparse::StateLabeling(mStates.size() + (mergeFailedStates ? 1 : 0));
- // Initial state is always first state without any failure
- modelComponents.stateLabeling.addLabel("init");
- modelComponents.stateLabeling.addLabelToState("init", initialStateIndex);
- // Label all states corresponding to their status (failed, failsafe, failed BE)
- if(labelOpts.buildFailLabel) {
- modelComponents.stateLabeling.addLabel("failed");
- }
- if(labelOpts.buildFailSafeLabel) {
- modelComponents.stateLabeling.addLabel("failsafe");
- }
-
- // Collect labels for all BE
- std::vector<std::shared_ptr<storage::DFTBE<ValueType>>> basicElements = mDft.getBasicElements();
- for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
- if(labelOpts.beLabels.count(elem->name()) > 0) {
- modelComponents.stateLabeling.addLabel(elem->name() + "_fail");
- }
- }
-
- if(mergeFailedStates) {
- modelComponents.stateLabeling.addLabelToState("failed", failedIndex);
- }
- for (auto const& stateIdPair : mStates) {
- storm::storage::BitVector state = stateIdPair.first;
- size_t stateId = stateIdPair.second;
- if (!mergeFailedStates && labelOpts.buildFailLabel && mDft.hasFailed(state, *mStateGenerationInfo)) {
- modelComponents.stateLabeling.addLabelToState("failed", stateId);
- }
- if (labelOpts.buildFailSafeLabel && mDft.isFailsafe(state, *mStateGenerationInfo)) {
- modelComponents.stateLabeling.addLabelToState("failsafe", stateId);
- };
- // Set fail status for each BE
- for (std::shared_ptr<storage::DFTBE<ValueType>> elem : basicElements) {
- if (labelOpts.beLabels.count(elem->name()) > 0 && storm::storage::DFTState<ValueType>::hasFailed(state, mStateGenerationInfo->getStateIndex(elem->id())) ) {
- modelComponents.stateLabeling.addLabelToState(elem->name() + "_fail", stateId);
- }
- }
- }
-
- std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
- storm::storage::sparse::ModelComponents<ValueType> components(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling));
- components.exitRates = std::move(modelComponents.exitRates);
- if (deterministic) {
- components.transitionMatrix.makeRowGroupingTrivial();
- model = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(std::move(components));
- } else {
- components.markovianStates = std::move(modelComponents.markovianStates);
- std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = std::make_shared<storm::models::sparse::MarkovAutomaton<ValueType>>(std::move(components));
- if (ma->hasOnlyTrivialNondeterminism()) {
- // Markov automaton can be converted into CTMC
- model = ma->convertToCTMC();
- } else {
- model = ma;
- }
- }
-
- return model;
- }
-
- template <typename ValueType>
- std::pair<uint_fast64_t, bool> ExplicitDFTModelBuilder<ValueType>::exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates) {
- STORM_LOG_TRACE("Explore state: " << mDft.getStateString(state));
-
- auto explorePair = checkForExploration(state);
- if (!explorePair.first) {
- // State does not need any exploration
- return std::make_pair(explorePair.second, true);
- }
-
-
- // Initialization
- // TODO Matthias: set Markovian states directly as bitvector?
- std::map<uint_fast64_t, ValueType> outgoingRates;
- std::vector<std::map<uint_fast64_t, ValueType>> outgoingProbabilities;
- bool hasDependencies = state->nrFailableDependencies() > 0;
- size_t failableCount = hasDependencies ? state->nrFailableDependencies() : state->nrFailableBEs();
- size_t smallest = 0;
- ValueType exitRate = storm::utility::zero<ValueType>();
- bool deterministic = !hasDependencies;
-
- // Absorbing state
- if (mDft.hasFailed(state) || mDft.isFailsafe(state) || state->nrFailableBEs() == 0) {
- uint_fast64_t stateId = addState(state);
- STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not coincide.");
-
- // Add self loop
- transitionMatrixBuilder.newRowGroup(stateId + rowOffset);
- transitionMatrixBuilder.addNextValue(stateId + rowOffset, stateId, storm::utility::one<ValueType>());
- STORM_LOG_TRACE("Added self loop for " << stateId);
- exitRates.push_back(storm::utility::one<ValueType>());
- STORM_LOG_ASSERT(exitRates.size()-1 == stateId, "No. of considered states does not match state id.");
- markovianStates.push_back(stateId);
- // No further exploration required
- return std::make_pair(stateId, true);
- }
-
- // Let BE fail
- while (smallest < failableCount) {
- STORM_LOG_ASSERT(!mDft.hasFailed(state), "Dft has failed.");
-
- // Construct new state as copy from original one
- DFTStatePointer newState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
- std::pair<std::shared_ptr<storm::storage::DFTBE<ValueType> const>, bool> nextBEPair = newState->letNextBEFail(smallest++);
- std::shared_ptr<storm::storage::DFTBE<ValueType> const>& nextBE = nextBEPair.first;
- STORM_LOG_ASSERT(nextBE, "NextBE is null.");
- STORM_LOG_ASSERT(nextBEPair.second == hasDependencies, "Failure due to dependencies does not match.");
- STORM_LOG_TRACE("With the failure of: " << nextBE->name() << " [" << nextBE->id() << "] in " << mDft.getStateString(state));
-
- // Propagate failures
- storm::storage::DFTStateSpaceGenerationQueues<ValueType> queues;
-
- for (DFTGatePointer parent : nextBE->parents()) {
- if (newState->isOperational(parent->id())) {
- queues.propagateFailure(parent);
- }
- }
- for (DFTRestrictionPointer restr : nextBE->restrictions()) {
- queues.checkRestrictionLater(restr);
- }
-
- while (!queues.failurePropagationDone()) {
- DFTGatePointer next = queues.nextFailurePropagation();
- next->checkFails(*newState, queues);
- newState->updateFailableDependencies(next->id());
- }
-
- while(!queues.restrictionChecksDone()) {
- DFTRestrictionPointer next = queues.nextRestrictionCheck();
- next->checkFails(*newState, queues);
- newState->updateFailableDependencies(next->id());
- }
-
- if(newState->isInvalid()) {
- continue;
- }
- bool dftFailed = newState->hasFailed(mDft.getTopLevelIndex());
-
- while (!dftFailed && !queues.failsafePropagationDone()) {
- DFTGatePointer next = queues.nextFailsafePropagation();
- next->checkFailsafe(*newState, queues);
- }
-
- while (!dftFailed && enableDC && !queues.dontCarePropagationDone()) {
- DFTElementPointer next = queues.nextDontCarePropagation();
- next->checkDontCareAnymore(*newState, queues);
- }
-
- // Update failable dependencies
- if (!dftFailed) {
- newState->updateFailableDependencies(nextBE->id());
- newState->updateDontCareDependencies(nextBE->id());
- }
-
- uint_fast64_t newStateId;
- if(dftFailed && mergeFailedStates) {
- newStateId = failedIndex;
- } else {
- // Explore new state recursively
- auto explorePair = exploreStates(newState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates);
- newStateId = explorePair.first;
- deterministic &= explorePair.second;
- }
-
- // Set transitions
- if (hasDependencies) {
- // Failure is due to dependency -> add non-deterministic choice
- std::map<uint_fast64_t, ValueType> choiceProbabilities;
- std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(state->getDependencyId(smallest-1));
- choiceProbabilities.insert(std::make_pair(newStateId, dependency->probability()));
- STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << dependency->probability());
-
- if (!storm::utility::isOne(dependency->probability())) {
- // Add transition to state where dependency was unsuccessful
- DFTStatePointer unsuccessfulState = std::make_shared<storm::storage::DFTState<ValueType>>(*state);
- unsuccessfulState->letDependencyBeUnsuccessful(smallest-1);
- auto explorePair = exploreStates(unsuccessfulState, rowOffset, transitionMatrixBuilder, markovianStates, exitRates);
- uint_fast64_t unsuccessfulStateId = explorePair.first;
- deterministic &= explorePair.second;
- ValueType remainingProbability = storm::utility::one<ValueType>() - dependency->probability();
- choiceProbabilities.insert(std::make_pair(unsuccessfulStateId, remainingProbability));
- STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability);
- }
- outgoingProbabilities.push_back(choiceProbabilities);
- } else {
- // Set failure rate according to activation
- bool isActive = true;
- if (mDft.hasRepresentant(nextBE->id())) {
- // Active must be checked for the state we are coming from as this state is responsible for the
- // rate and not the new state we are going to
- isActive = state->isActive(mDft.getRepresentant(nextBE->id()));
- }
- ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
- STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0.");
- auto resultFind = outgoingRates.find(newStateId);
- if (resultFind != outgoingRates.end()) {
- // Add to existing transition
- resultFind->second += rate;
- STORM_LOG_TRACE("Updated transition to " << resultFind->first << " with " << (isActive ? "active" : "passive") << " rate " << rate << " to new rate " << resultFind->second);
- } else {
- // Insert new transition
- outgoingRates.insert(std::make_pair(newStateId, rate));
- STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " rate " << rate);
- }
- exitRate += rate;
- }
-
- } // end while failing BE
-
- // Add state
- uint_fast64_t stateId = addState(state);
- STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match.");
- STORM_LOG_ASSERT(stateId == newIndex-1, "Id does not match no. of states.");
-
- if (hasDependencies) {
- // Add all probability transitions
- STORM_LOG_ASSERT(outgoingRates.empty(), "Outgoing transitions not empty.");
- transitionMatrixBuilder.newRowGroup(stateId + rowOffset);
- for (size_t i = 0; i < outgoingProbabilities.size(); ++i, ++rowOffset) {
- STORM_LOG_ASSERT(outgoingProbabilities[i].size() == 1 || outgoingProbabilities[i].size() == 2, "No. of outgoing transitions is not valid.");
- for (auto it = outgoingProbabilities[i].begin(); it != outgoingProbabilities[i].end(); ++it)
- {
- STORM_LOG_TRACE("Set transition from " << stateId << " to " << it->first << " with probability " << it->second);
- transitionMatrixBuilder.addNextValue(stateId + rowOffset, it->first, it->second);
- }
- }
- rowOffset--; // One increment too many
- } else {
- // Try to merge pseudo states with their instantiation
- // TODO Matthias: improve?
- for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ) {
- if (it->first >= OFFSET_PSEUDO_STATE) {
- uint_fast64_t newId = it->first - OFFSET_PSEUDO_STATE;
- STORM_LOG_ASSERT(newId < mPseudoStatesMapping.size(), "Id is not valid.");
- if (mPseudoStatesMapping[newId].first > 0) {
- // State exists already
- newId = mPseudoStatesMapping[newId].first;
- auto itFind = outgoingRates.find(newId);
- if (itFind != outgoingRates.end()) {
- // Add probability from pseudo state to instantiation
- itFind->second += it->second;
- STORM_LOG_TRACE("Merged pseudo state " << newId << " adding rate " << it->second << " to total rate of " << itFind->second);
- } else {
- // Only change id
- outgoingRates.emplace(newId, it->second);
- STORM_LOG_TRACE("Instantiated pseudo state " << newId << " with rate " << it->second);
- }
- // Remove pseudo state
- it = outgoingRates.erase(it);
- } else {
- ++it;
- }
- } else {
- ++it;
- }
- }
-
- // Add all rate transitions
- STORM_LOG_ASSERT(outgoingProbabilities.empty(), "Outgoing probabilities not empty.");
- transitionMatrixBuilder.newRowGroup(state->getId() + rowOffset);
- STORM_LOG_TRACE("Exit rate for " << state->getId() << ": " << exitRate);
- for (auto it = outgoingRates.begin(); it != outgoingRates.end(); ++it)
- {
- ValueType probability = it->second / exitRate; // Transform rate to probability
- STORM_LOG_TRACE("Set transition from " << state->getId() << " to " << it->first << " with rate " << it->second);
- transitionMatrixBuilder.addNextValue(state->getId() + rowOffset, it->first, probability);
- }
-
- markovianStates.push_back(state->getId());
- }
-
- STORM_LOG_TRACE("Finished exploring state: " << mDft.getStateString(state));
- exitRates.push_back(exitRate);
- STORM_LOG_ASSERT(exitRates.size()-1 == state->getId(), "Id does not match no. of states.");
- return std::make_pair(state->getId(), deterministic);
- }
-
- template <typename ValueType>
- std::pair<bool, uint_fast64_t> ExplicitDFTModelBuilder<ValueType>::checkForExploration(DFTStatePointer const& state) {
- bool changed = false;
- if (mStateGenerationInfo->hasSymmetries()) {
- // Order state by symmetry
- STORM_LOG_TRACE("Check for symmetry: " << mDft.getStateString(state));
- changed = state->orderBySymmetry();
- STORM_LOG_TRACE("State " << (changed ? "changed to " : "did not change") << (changed ? mDft.getStateString(state) : ""));
- }
-
- if (mStates.contains(state->status())) {
- // State already exists
- uint_fast64_t stateId = mStates.getValue(state->status());
- STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists");
-
- if (changed || stateId < OFFSET_PSEUDO_STATE) {
- // State is changed or an explored "normal" state
- return std::make_pair(false, stateId);
- }
-
- stateId -= OFFSET_PSEUDO_STATE;
- STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Id not valid.");
- if (mPseudoStatesMapping[stateId].first > 0) {
- // Pseudo state already explored
- return std::make_pair(false, mPseudoStatesMapping[stateId].first);
- }
-
- STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "States do not coincide.");
- STORM_LOG_TRACE("Pseudo state " << mDft.getStateString(state) << " can be explored now");
- return std::make_pair(true, stateId);
- } else {
- // State does not exists
- if (changed) {
- // Remember state for later creation
- state->setId(mPseudoStatesMapping.size() + OFFSET_PSEUDO_STATE);
- mPseudoStatesMapping.push_back(std::make_pair(0, state->status()));
- mStates.findOrAdd(state->status(), state->getId());
- STORM_LOG_TRACE("Remember state for later creation: " << mDft.getStateString(state));
- return std::make_pair(false, state->getId());
- } else {
- // State needs exploration
- return std::make_pair(true, 0);
- }
- }
- }
-
- template <typename ValueType>
- uint_fast64_t ExplicitDFTModelBuilder<ValueType>::addState(DFTStatePointer const& state) {
- uint_fast64_t stateId;
- // TODO remove
- bool changed = state->orderBySymmetry();
- STORM_LOG_ASSERT(!changed, "State to add has changed by applying symmetry.");
-
- // Check if state already exists
- if (mStates.contains(state->status())) {
- // State already exists
- stateId = mStates.getValue(state->status());
- STORM_LOG_TRACE("State " << mDft.getStateString(state) << " with id " << stateId << " already exists");
-
- // Check if possible pseudo state can be created now
- STORM_LOG_ASSERT(stateId >= OFFSET_PSEUDO_STATE, "State is no pseudo state.");
- stateId -= OFFSET_PSEUDO_STATE;
- STORM_LOG_ASSERT(stateId < mPseudoStatesMapping.size(), "Pseudo state not known.");
- if (mPseudoStatesMapping[stateId].first == 0) {
- // Create pseudo state now
- STORM_LOG_ASSERT(mPseudoStatesMapping[stateId].second == state->status(), "Pseudo states do not coincide.");
- state->setId(newIndex++);
- mPseudoStatesMapping[stateId].first = state->getId();
- stateId = state->getId();
- mStates.setOrAdd(state->status(), stateId);
- STORM_LOG_TRACE("Now create state " << mDft.getStateString(state) << " with id " << stateId);
- return stateId;
- } else {
- STORM_LOG_ASSERT(false, "Pseudo state already created.");
- return 0;
- }
- } else {
- // Create new state
- state->setId(newIndex++);
- stateId = mStates.findOrAdd(state->status(), state->getId());
- STORM_LOG_TRACE("New state: " << mDft.getStateString(state));
- return stateId;
- }
- }
-
-
- // Explicitly instantiate the class.
- template class ExplicitDFTModelBuilder<double>;
-
-#ifdef STORM_HAVE_CARL
- template class ExplicitDFTModelBuilder<storm::RationalFunction>;
-#endif
-
- } // namespace builder
-} // namespace storm
-
-
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
deleted file mode 100644
index 2913a78fa..000000000
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h
+++ /dev/null
@@ -1,102 +0,0 @@
-#pragma once
-
-#include <boost/container/flat_set.hpp>
-#include <boost/optional/optional.hpp>
-#include <stack>
-#include <unordered_set>
-
-
-#include "storm/models/sparse/StateLabeling.h"
-#include "storm/models/sparse/ChoiceLabeling.h"
-#include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/models/sparse/Model.h"
-#include "storm/storage/SparseMatrix.h"
-#include "storm/storage/BitVectorHashMap.h"
-
-#include "storm-dft/storage/dft/DFT.h"
-#include "storm-dft/storage/dft/SymmetricUnits.h"
-
-
-
-
-
-namespace storm {
- namespace builder {
-
- template<typename ValueType>
- class ExplicitDFTModelBuilder {
-
- using DFTElementPointer = std::shared_ptr<storm::storage::DFTElement<ValueType>>;
- using DFTElementCPointer = std::shared_ptr<storm::storage::DFTElement<ValueType> const>;
- using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
- using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
- using DFTRestrictionPointer = std::shared_ptr<storm::storage::DFTRestriction<ValueType>>;
-
-
- // A structure holding the individual components of a model.
- struct ModelComponents {
- ModelComponents();
-
- // The transition matrix.
- storm::storage::SparseMatrix<ValueType> transitionMatrix;
-
- // The state labeling.
- storm::models::sparse::StateLabeling stateLabeling;
-
- // The Markovian states.
- storm::storage::BitVector markovianStates;
-
- // The exit rates.
- std::vector<ValueType> exitRates;
-
- // A vector that stores a labeling for each choice.
- boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
- };
-
- const size_t INITIAL_BUCKETSIZE = 20000;
- const uint_fast64_t OFFSET_PSEUDO_STATE = UINT_FAST64_MAX / 2;
-
- storm::storage::DFT<ValueType> const& mDft;
- std::shared_ptr<storm::storage::DFTStateGenerationInfo> mStateGenerationInfo;
- storm::storage::BitVectorHashMap<uint_fast64_t> mStates;
- std::vector<std::pair<uint_fast64_t, storm::storage::BitVector>> mPseudoStatesMapping; // vector of (id to concrete state, bitvector)
- size_t newIndex = 0;
- bool mergeFailedStates = false;
- bool enableDC = true;
- size_t failedIndex = 0;
- size_t initialStateIndex = 0;
-
- public:
- struct LabelOptions {
- bool buildFailLabel = true;
- bool buildFailSafeLabel = false;
- std::set<std::string> beLabels = {};
- };
-
- ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
-
- std::shared_ptr<storm::models::sparse::Model<ValueType>> buildModel(LabelOptions const& labelOpts);
-
- private:
- std::pair<uint_fast64_t, bool> exploreStates(DFTStatePointer const& state, size_t& rowOffset, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<uint_fast64_t>& markovianStates, std::vector<ValueType>& exitRates);
-
- /*!
- * Adds a state to the explored states and handles pseudo states.
- *
- * @param state The state to add.
- * @return Id of added state.
- */
- uint_fast64_t addState(DFTStatePointer const& state);
-
- /*!
- * Check if state needs an exploration and remember pseudo states for later creation.
- *
- * @param state State which might need exploration.
- * @return Pair of flag indicating whether the state needs exploration now and the state id if the state already
- * exists.
- */
- std::pair<bool, uint_fast64_t> checkForExploration(DFTStatePointer const& state);
-
- };
- }
-}
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 45d97baa6..3a69cb5e4 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -5,7 +5,6 @@
#include "storm/utility/bitoperations.h"
#include "storm/utility/DirectEncodingExporter.h"
-#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h"
#include "storm-dft/storage/dft/DFTIsomorphism.h"
#include "storm-dft/settings/modules/FaultTreeSettings.h"
@@ -342,18 +341,10 @@ namespace storm {
} else {
// Build a single Markov Automaton
STORM_LOG_INFO("Building Model...");
- std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
- // TODO Matthias: use only one builder if everything works again
- if (storm::settings::getModule<storm::settings::modules::FaultTreeSettings>().isApproximationErrorSet()) {
- storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
- builder.buildModel(labeloptions, 0, 0.0);
- model = builder.getModel();
- } else {
- storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions;
- model = builder.buildModel(labeloptions);
- }
+ storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
+ builder.buildModel(labeloptions, 0, 0.0);
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
model->printModelInformationToStream(std::cout);
explorationTimer.stop();
From 0913388cd3cb7952d43b37661547efc7abf64072 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 13 Oct 2017 18:11:05 +0200
Subject: [PATCH 33/39] Renamed ExplicitDFTModelBuilderApprox to
ExplicitDFTModelBuilder
---
...Approx.cpp => ExplicitDFTModelBuilder.cpp} | 46 +++++++++----------
...lderApprox.h => ExplicitDFTModelBuilder.h} | 4 +-
.../modelchecker/dft/DFTModelChecker.cpp | 19 ++++----
3 files changed, 34 insertions(+), 35 deletions(-)
rename src/storm-dft/builder/{ExplicitDFTModelBuilderApprox.cpp => ExplicitDFTModelBuilder.cpp} (94%)
rename src/storm-dft/builder/{ExplicitDFTModelBuilderApprox.h => ExplicitDFTModelBuilder.h} (98%)
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
similarity index 94%
rename from src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
rename to src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index c7d6605f5..2b74432ad 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -1,4 +1,4 @@
-#include "ExplicitDFTModelBuilderApprox.h"
+#include "ExplicitDFTModelBuilder.h"
#include <map>
@@ -17,18 +17,18 @@ namespace storm {
namespace builder {
template<typename ValueType, typename StateType>
- ExplicitDFTModelBuilderApprox<ValueType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
+ ExplicitDFTModelBuilder<ValueType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() {
// Intentionally left empty.
}
template<typename ValueType, typename StateType>
- ExplicitDFTModelBuilderApprox<ValueType, StateType>::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) {
+ ExplicitDFTModelBuilder<ValueType, StateType>::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) {
// Create matrix builder
builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, canHaveNondeterminism, 0);
}
template<typename ValueType, typename StateType>
- ExplicitDFTModelBuilderApprox<ValueType, StateType>::LabelOptions::LabelOptions(std::vector<std::shared_ptr<const storm::logic::Formula>> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) {
+ ExplicitDFTModelBuilder<ValueType, StateType>::LabelOptions::LabelOptions(std::vector<std::shared_ptr<const storm::logic::Formula>> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) {
// Get necessary labels from properties
std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabels;
for (auto property : properties) {
@@ -51,7 +51,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- ExplicitDFTModelBuilderApprox<ValueType, StateType>::ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) :
+ ExplicitDFTModelBuilder<ValueType, StateType>::ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) :
dft(dft),
stateGenerationInfo(std::make_shared<storm::storage::DFTStateGenerationInfo>(dft.buildStateGenerationInfo(symmetries))),
enableDC(enableDC),
@@ -124,7 +124,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) {
+ void ExplicitDFTModelBuilder<ValueType, StateType>::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) {
STORM_LOG_TRACE("Generating DFT state space");
if (iteration < 1) {
@@ -156,7 +156,7 @@ namespace storm {
}
// Build initial state
- this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1));
+ this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1));
STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed.");
initialStateIndex = stateStorage.initialStateIndices[0];
STORM_LOG_TRACE("Initial state: " << initialStateIndex);
@@ -214,7 +214,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::initializeNextIteration() {
+ void ExplicitDFTModelBuilder<ValueType, StateType>::initializeNextIteration() {
STORM_LOG_TRACE("Refining DFT state space");
// TODO Matthias: should be easier now as skipped states all are at the end of the matrix
@@ -316,7 +316,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::exploreStateSpace(double approximationThreshold) {
+ void ExplicitDFTModelBuilder<ValueType, StateType>::exploreStateSpace(double approximationThreshold) {
size_t nrExpandedStates = 0;
size_t nrSkippedStates = 0;
// TODO Matthias: do not empty queue every time but break before
@@ -364,7 +364,7 @@ namespace storm {
} else {
// Explore the current state
++nrExpandedStates;
- storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1));
+ storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1));
STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty.");
setMarkovian(behavior.begin()->isMarkovian());
@@ -424,7 +424,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::buildLabeling(LabelOptions const& labelOpts) {
+ void ExplicitDFTModelBuilder<ValueType, StateType>::buildLabeling(LabelOptions const& labelOpts) {
// Build state labeling
modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount());
// Initial state
@@ -473,13 +473,13 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::getModel() {
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::getModel() {
STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states");
return createModel(false);
}
template<typename ValueType, typename StateType>
- std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::getModelApproximation(bool lowerBound, bool expectedTime) {
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::getModelApproximation(bool lowerBound, bool expectedTime) {
if (expectedTime) {
// TODO Matthias: handle case with no skipped states
changeMatrixBound(modelComponents.transitionMatrix, lowerBound);
@@ -550,7 +550,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilderApprox<ValueType, StateType>::createModel(bool copy) {
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> ExplicitDFTModelBuilder<ValueType, StateType>::createModel(bool copy) {
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
if (modelComponents.deterministicModel) {
@@ -607,7 +607,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const {
+ void ExplicitDFTModelBuilder<ValueType, StateType>::changeMatrixBound(storm::storage::SparseMatrix<ValueType> & matrix, bool lowerBound) const {
// Set lower bound for skipped states
for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) {
auto matrixEntry = matrix.getRow(it->first, 0).begin();
@@ -632,7 +632,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getLowerBound(DFTStatePointer const& state) const {
+ ValueType ExplicitDFTModelBuilder<ValueType, StateType>::getLowerBound(DFTStatePointer const& state) const {
// Get the lower bound by considering the failure of all possible BEs
ValueType lowerBound = storm::utility::zero<ValueType>();
for (size_t index = 0; index < state->nrFailableBEs(); ++index) {
@@ -642,7 +642,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getUpperBound(DFTStatePointer const& state) const {
+ ValueType ExplicitDFTModelBuilder<ValueType, StateType>::getUpperBound(DFTStatePointer const& state) const {
if (state->hasFailed(dft.getTopLevelIndex())) {
return storm::utility::zero<ValueType>();
}
@@ -709,7 +709,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- ValueType ExplicitDFTModelBuilderApprox<ValueType, StateType>::computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const {
+ ValueType ExplicitDFTModelBuilder<ValueType, StateType>::computeMTTFAnd(std::vector<ValueType> const& rates, size_t size) const {
ValueType result = storm::utility::zero<ValueType>();
if (size == 0) {
return result;
@@ -762,7 +762,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- StateType ExplicitDFTModelBuilderApprox<ValueType, StateType>::getOrAddStateIndex(DFTStatePointer const& state) {
+ StateType ExplicitDFTModelBuilder<ValueType, StateType>::getOrAddStateIndex(DFTStatePointer const& state) {
StateType stateId;
bool changed = false;
@@ -811,7 +811,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::setMarkovian(bool markovian) {
+ void ExplicitDFTModelBuilder<ValueType, StateType>::setMarkovian(bool markovian) {
if (matrixBuilder.getCurrentRowGroup() > modelComponents.markovianStates.size()) {
// Resize BitVector
modelComponents.markovianStates.resize(modelComponents.markovianStates.size() + INITIAL_BITVECTOR_SIZE);
@@ -820,7 +820,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
- void ExplicitDFTModelBuilderApprox<ValueType, StateType>::printNotExplored() const {
+ void ExplicitDFTModelBuilder<ValueType, StateType>::printNotExplored() const {
std::cout << "states not explored:" << std::endl;
for (auto it : statesNotExplored) {
std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl;
@@ -829,10 +829,10 @@ namespace storm {
// Explicitly instantiate the class.
- template class ExplicitDFTModelBuilderApprox<double>;
+ template class ExplicitDFTModelBuilder<double>;
#ifdef STORM_HAVE_CARL
- template class ExplicitDFTModelBuilderApprox<storm::RationalFunction>;
+ template class ExplicitDFTModelBuilder<storm::RationalFunction>;
#endif
} // namespace builder
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
similarity index 98%
rename from src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
rename to src/storm-dft/builder/ExplicitDFTModelBuilder.h
index 802aefe1b..b96dea410 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h
@@ -26,7 +26,7 @@ namespace storm {
* Build a Markov chain from DFT.
*/
template<typename ValueType, typename StateType = uint32_t>
- class ExplicitDFTModelBuilderApprox {
+ class ExplicitDFTModelBuilder {
using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
// TODO Matthias: make choosable
@@ -177,7 +177,7 @@ namespace storm {
* @param symmetries Symmetries in the dft.
* @param enableDC Flag indicating if dont care propagation should be used.
*/
- ExplicitDFTModelBuilderApprox(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
+ ExplicitDFTModelBuilder(storm::storage::DFT<ValueType> const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC);
/*!
* Build model from DFT.
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 3a69cb5e4..d2b435c1c 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -5,7 +5,7 @@
#include "storm/utility/bitoperations.h"
#include "storm/utility/DirectEncodingExporter.h"
-#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h"
+#include "storm-dft/builder/ExplicitDFTModelBuilder.h"
#include "storm-dft/storage/dft/DFTIsomorphism.h"
#include "storm-dft/settings/modules/FaultTreeSettings.h"
@@ -191,8 +191,8 @@ namespace storm {
// Build a single CTMC
STORM_LOG_INFO("Building Model...");
- storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(ft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
+ storm::builder::ExplicitDFTModelBuilder<ValueType> builder(ft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
explorationTimer.stop();
@@ -243,9 +243,8 @@ namespace storm {
// Build a single CTMC
STORM_LOG_INFO("Building Model...");
-
- storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
+ storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
model->printModelInformationToStream(std::cout);
@@ -276,8 +275,8 @@ namespace storm {
approximation_result approxResult = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
std::vector<ValueType> newResult;
- storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties);
+ storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties);
// TODO Matthias: compute approximation for all properties simultaneously?
std::shared_ptr<const storm::logic::Formula> property = properties[0];
@@ -341,8 +340,8 @@ namespace storm {
} else {
// Build a single Markov Automaton
STORM_LOG_INFO("Building Model...");
- storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
- typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
+ storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);
+ typename storm::builder::ExplicitDFTModelBuilder<ValueType>::LabelOptions labeloptions(properties, storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet());
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
model->printModelInformationToStream(std::cout);
From 72d58b6155632b30b4910512376bde7f5107e9c0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 13 Oct 2017 20:28:09 +0200
Subject: [PATCH 34/39] fix for sylvan workers not releasing mmap'ed memory
---
resources/3rdparty/sylvan/src/lace.c | 3 +++
1 file changed, 3 insertions(+)
diff --git a/resources/3rdparty/sylvan/src/lace.c b/resources/3rdparty/sylvan/src/lace.c
index 08e9f8843..9315f6895 100755
--- a/resources/3rdparty/sylvan/src/lace.c
+++ b/resources/3rdparty/sylvan/src/lace.c
@@ -715,6 +715,9 @@ VOID_TASK_1(lace_steal_loop, int*, quit)
} while (__lace_worker->enabled == 0);
}
}
+
+ // Unmap the virtual memory from the worker.
+ munmap(workers_memory[worker_id], workers_memory_size);
}
/**
From 02c23865da563a2d3eb72a6424188461e82b648a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 14 Oct 2017 14:24:39 +0200
Subject: [PATCH 35/39] reworked memory leak solution in sylvan according to
Tom van Dijks hints
---
resources/3rdparty/sylvan/src/lace.c | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/resources/3rdparty/sylvan/src/lace.c b/resources/3rdparty/sylvan/src/lace.c
index 9315f6895..64443e23b 100755
--- a/resources/3rdparty/sylvan/src/lace.c
+++ b/resources/3rdparty/sylvan/src/lace.c
@@ -715,9 +715,6 @@ VOID_TASK_1(lace_steal_loop, int*, quit)
} while (__lace_worker->enabled == 0);
}
}
-
- // Unmap the virtual memory from the worker.
- munmap(workers_memory[worker_id], workers_memory_size);
}
/**
@@ -1091,6 +1088,12 @@ void lace_exit()
lace_resume();
lace_barrier();
+ // Free the memory of the workers.
+ for (unsigned int i=0; i<n_workers; i++) munmap(workers_memory[i], workers_memory_size);
+ free(workers_memory);
+ free(workers);
+ free(workers_p);
+
// finally, destroy the barriers
lace_barrier_destroy();
pthread_barrier_destroy(&suspend_barrier);
From 378e2ee40ff11cdcfd3943f2791dad0ee61bc74e Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Sat, 14 Oct 2017 14:13:13 +0200
Subject: [PATCH 36/39] Better error message if expression parser fails
---
src/storm/parser/ExpressionParser.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm/parser/ExpressionParser.cpp
index cd3ccd595..519bc2b9f 100644
--- a/src/storm/parser/ExpressionParser.cpp
+++ b/src/storm/parser/ExpressionParser.cpp
@@ -197,7 +197,7 @@ namespace storm {
try {
// Start parsing.
bool succeeded = qi::phrase_parse(iter, last, *this, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
- STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse expression.");
+ STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse expression '" << expressionString << "'.");
STORM_LOG_DEBUG("Parsed expression successfully.");
} catch (qi::expectation_failure<PositionIteratorType> const& e) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_);
From 6832fc805c2d1a7ea4f0e9b2b6478a7024ab0deb Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Sat, 14 Oct 2017 15:17:38 +0200
Subject: [PATCH 37/39] parser improvements in changelog
---
CHANGELOG.md | 1 +
1 file changed, 1 insertion(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9fafa9849..4005ca0e1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,6 +18,7 @@ Version 1.1.x
- storm-pars: support for welldefinedness constraints in mdps.
- symbolic (MT/BDD) bisimulation
- Fixed issue related to variable names that can not be used in Exprtk.
+- DRN parser improved
### Version 1.1.0 (2017/8)
From 2ce145745a3c20c5493ee06db9876eb33936d57e Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Sat, 14 Oct 2017 15:41:18 +0200
Subject: [PATCH 38/39] parameters from rewards are now also collected in
wellformedness analysis
---
src/storm/analysis/GraphConditions.cpp | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp
index be8073bf7..663bf2b52 100644
--- a/src/storm/analysis/GraphConditions.cpp
+++ b/src/storm/analysis/GraphConditions.cpp
@@ -35,6 +35,8 @@ namespace storm {
void ConstraintCollector<ValueType>::wellformedRequiresNonNegativeEntries(std::vector<ValueType> const& vec) {
for(auto const& entry : vec) {
if (!storm::utility::isConstant(entry)) {
+ auto const& transitionVars = entry.gatherVariables();
+ variableSet.insert(transitionVars.begin(), transitionVars.end());
if (entry.denominator().isConstant()) {
if (entry.denominatorAsNumber() > 0) {
wellformedConstraintSet.emplace(entry.nominator().polynomialWithCoefficient(), storm::CompareRelation::GEQ);
From ccfb1a292c1332d6aff7f4ed429493607180890b Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Sat, 14 Oct 2017 17:22:28 +0200
Subject: [PATCH 39/39] drn parser and exporter use reward names
---
src/storm/parser/DirectEncodingParser.cpp | 23 +++++++++++++++++---
src/storm/parser/DirectEncodingParser.h | 2 +-
src/storm/utility/DirectEncodingExporter.cpp | 5 +++++
3 files changed, 26 insertions(+), 4 deletions(-)
diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp
index 3350d90ee..45768f908 100644
--- a/src/storm/parser/DirectEncodingParser.cpp
+++ b/src/storm/parser/DirectEncodingParser.cpp
@@ -2,6 +2,8 @@
#include <iostream>
#include <string>
+
+#include <boost/algorithm/string.hpp>
#include <boost/algorithm/string/predicate.hpp>
#include "storm/models/sparse/MarkovAutomaton.h"
@@ -19,6 +21,7 @@
#include "storm/utility/macros.h"
#include "storm/utility/file.h"
+
namespace storm {
namespace parser {
@@ -64,6 +67,8 @@ namespace storm {
size_t nrStates = 0;
storm::models::ModelType type;
+ std::vector<std::string> rewardModelNames;
+
std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents;
// Parse header
@@ -92,6 +97,11 @@ namespace storm {
}
sawParameters = true;
}
+ if(line == "@reward_models") {
+ STORM_LOG_THROW(rewardModelNames.size() == 0, storm::exceptions::WrongFormatException, "Reward model names declared twice");
+ std::getline(file, line);
+ boost::split(rewardModelNames, line, boost::is_any_of("\t "));
+ }
if(line == "@nr_states") {
STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice");
std::getline(file, line);
@@ -104,7 +114,7 @@ namespace storm {
STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "Nr States has to be declared before model.");
// Construct model components
- modelComponents = parseStates(file, type, nrStates, valueParser);
+ modelComponents = parseStates(file, type, nrStates, valueParser, rewardModelNames);
break;
}
}
@@ -116,7 +126,7 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType>
- std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> DirectEncodingParser<ValueType, RewardModelType>::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser<ValueType> const& valueParser) {
+ std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> DirectEncodingParser<ValueType, RewardModelType>::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames) {
// Initialize
auto modelComponents = std::make_shared<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>();
bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton);
@@ -227,8 +237,15 @@ namespace storm {
STORM_LOG_TRACE("Finished parsing");
modelComponents->transitionMatrix = builder.build(row + 1, stateSize, nonDeterministic ? stateSize : 0);
+
for (uint64_t i = 0; i < stateRewards.size(); ++i) {
- modelComponents->rewardModels.emplace("rew" + std::to_string(i), storm::models::sparse::StandardRewardModel<ValueType>(std::move(stateRewards[i])));
+ std::string rewardModelName;
+ if (rewardModelNames.size() <= i) {
+ rewardModelName = "rew" + std::to_string(i);
+ } else {
+ rewardModelName = rewardModelNames[i];
+ }
+ modelComponents->rewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel<ValueType>(std::move(stateRewards[i])));
}
STORM_LOG_TRACE("Built matrix");
return modelComponents;
diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h
index 43a5a6f8b..db1bac12e 100644
--- a/src/storm/parser/DirectEncodingParser.h
+++ b/src/storm/parser/DirectEncodingParser.h
@@ -75,7 +75,7 @@ namespace storm {
*
* @return Transition matrix.
*/
- static std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser<ValueType> const& valueParser);
+ static std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser<ValueType> const& valueParser, std::vector<std::string> const& rewardModelNames);
};
} // namespace parser
diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp
index 6bdd629a7..e0913a0f2 100644
--- a/src/storm/utility/DirectEncodingExporter.cpp
+++ b/src/storm/utility/DirectEncodingExporter.cpp
@@ -46,6 +46,11 @@ namespace storm {
}
}
os << std::endl;
+ os << "@reward_models" << std::endl;
+ for (auto const& rewardModel : sparseModel->getRewardModels()) {
+ os << rewardModel.first << " ";
+ }
+ os << std::endl;
os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl;
os << "@model" << std::endl;