From aea711b9f7326dc74722e98d39c0d66cf02634df Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Mon, 21 Jan 2013 14:34:01 +0100
Subject: [PATCH 01/30] JacobiDecomposition Copy Constructor should throw
exception: Now it throws an InvalidAccessException. This closes #40
---
src/exceptions/InvalidAccessException.h | 19 +++++++++++++++++++
src/storage/JacobiDecomposition.h | 6 +++++-
2 files changed, 24 insertions(+), 1 deletion(-)
create mode 100644 src/exceptions/InvalidAccessException.h
diff --git a/src/exceptions/InvalidAccessException.h b/src/exceptions/InvalidAccessException.h
new file mode 100644
index 000000000..af413b1ed
--- /dev/null
+++ b/src/exceptions/InvalidAccessException.h
@@ -0,0 +1,19 @@
+#ifndef STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_
+#define STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_
+
+#include "src/exceptions/BaseException.h"
+
+namespace storm {
+
+namespace exceptions {
+
+/*!
+ * @brief This exception is thrown when a function is used/accessed that is forbidden to use (e.g. Copy Constructors)
+ */
+STORM_EXCEPTION_DEFINE_NEW(InvalidAccessException)
+
+} // namespace exceptions
+
+} // namespace storm
+
+#endif // STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_
diff --git a/src/storage/JacobiDecomposition.h b/src/storage/JacobiDecomposition.h
index f6de68e98..d02d1ab38 100644
--- a/src/storage/JacobiDecomposition.h
+++ b/src/storage/JacobiDecomposition.h
@@ -6,6 +6,8 @@
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
+#include "src/exceptions/InvalidAccessException.h"
+
extern log4cplus::Logger logger;
namespace storm {
@@ -76,7 +78,9 @@ private:
* The copy constructor is disabled for this class.
*/
//JacobiDecomposition(const JacobiDecomposition<T>& that) = delete; // not possible in VS2012
- JacobiDecomposition(const JacobiDecomposition<T>& that) {}
+ JacobiDecomposition(const JacobiDecomposition<T>& that) {
+ throw new storm::exceptions::InvalidAccessException() << "The copy constructor of JacobiDecomposition is explicitly disabled.";
+ }
/*!
* Pointer to the LU Matrix
From a2c5ee805b244904d2bdc679b20e547fd32956ab Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Mon, 21 Jan 2013 14:40:27 +0100
Subject: [PATCH 02/30] Refactored calls to SetBitCount
---
src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
index c90efc3b0..388c0e42f 100644
--- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
@@ -128,7 +128,8 @@ public:
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
// Only try to solve system if there are states for which the probability is unknown.
- if (maybeStates.getNumberOfSetBits() > 0) {
+ uint_fast64_t mayBeStatesSetBitCount = maybeStates.getNumberOfSetBits();
+ if (mayBeStatesSetBitCount > 0) {
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
@@ -142,11 +143,11 @@ public:
// Initialize the x vector with 0.5 for each element. This is the initial guess for
// the iterative solvers. It should be safe as for all 'maybe' states we know that the
// probability is strictly larger than 0.
- std::vector<Type> x(maybeStates.getNumberOfSetBits(), Type(0.5));
+ std::vector<Type> x(mayBeStatesSetBitCount, Type(0.5));
// Prepare the right-hand side of the equation system. For entry i this corresponds to
// the accumulated probability of going from state i to some 'yes' state.
- std::vector<Type> b(maybeStates.getNumberOfSetBits());
+ std::vector<Type> b(mayBeStatesSetBitCount);
this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &b);
// Solve the corresponding system of linear equations.
From d4b5a24757a47517add8f6ff14cc9b3659bc9dda Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Wed, 23 Jan 2013 20:08:09 +0100
Subject: [PATCH 03/30] Fixed the Jacobi Decomposition in the Matrix, Diagonal
Matrix was not inverted. Implemented solveLinearEquationSystemWithJacobi for
GMM based Solver.
---
src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 66 +++++++++++++++++--
src/storage/SparseMatrix.h | 6 +-
2 files changed, 67 insertions(+), 5 deletions(-)
diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
index 388c0e42f..c2c5663d0 100644
--- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
@@ -18,6 +18,7 @@
#include "src/utility/Settings.h"
#include "src/adapters/GmmxxAdapter.h"
#include "src/exceptions/InvalidPropertyException.h"
+#include "src/storage/JacobiDecomposition.h"
#include "gmm/gmm_matrix.h"
#include "gmm/gmm_iter_solvers.h"
@@ -260,7 +261,8 @@ public:
// Check whether there are states for which we have to compute the result.
storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates;
- if (maybeStates.getNumberOfSetBits() > 0) {
+ const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
+ if (maybeStatesSetBitCount > 0) {
// Now we can eliminate the rows and columns from the original transition probability matrix.
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
// Converting the matrix from the fixpoint notation to the form needed for the equation
@@ -273,10 +275,10 @@ public:
// Initialize the x vector with 1 for each element. This is the initial guess for
// the iterative solvers.
- std::vector<Type> x(maybeStates.getNumberOfSetBits(), storm::utility::constGetOne<Type>());
+ std::vector<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>());
// Prepare the right-hand side of the equation system.
- std::vector<Type>* b = new std::vector<Type>(maybeStates.getNumberOfSetBits());
+ std::vector<Type>* b = new std::vector<Type>(maybeStatesSetBitCount);
if (this->getModel().hasTransitionRewards()) {
// If a transition-based reward model is available, we initialize the right-hand
// side to the vector resulting from summing the rows of the pointwise product
@@ -290,7 +292,7 @@ public:
// as well. As the state reward vector contains entries not just for the states
// that we still consider (i.e. maybeStates), we need to extract these values
// first.
- std::vector<Type>* subStateRewards = new std::vector<Type>(maybeStates.getNumberOfSetBits());
+ std::vector<Type>* subStateRewards = new std::vector<Type>(maybeStatesSetBitCount);
storm::utility::setVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewards());
gmm::add(*subStateRewards, *b);
delete subStateRewards;
@@ -445,6 +447,62 @@ private:
LOG4CPLUS_WARN(logger, "Iterative solver did not converge.");
}
}
+
+ /*!
+ * Solves the linear equation system Ax=b with the given parameters
+ * using the Jacobi Method and therefor the Jacobi Decomposition of A.
+ *
+ * @param A The matrix A specifying the coefficients of the linear equations.
+ * @param x The vector x for which to solve the equations. The initial value of the elements of
+ * this vector are used as the initial guess and might thus influence performance and convergence.
+ * @param b The vector b specifying the values on the right-hand-sides of the equations.
+ * @return The solution of the system of linear equations in form of the elements of the vector
+ * x.
+ */
+ void solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b) const {
+
+ double precision = s->get<double>("precision");
+ if (precision <= 0) {
+ LOG4CPLUS_ERROR(logger, "Precision is not greater Zero");
+ }
+
+ // Get a Jacobi Decomposition of the Input Matrix A
+ storm::storage::JacobiDecomposition<Type>* jacobiDecomposition = A.getJacobiDecomposition();
+
+ // Convert the Diagonal matrix to GMM format
+ gmm::csr_matrix<Type>* gmmxxDiagonalInverted = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(jacobiDecomposition->getJacobiDInv());
+ // Convert the LU Matrix to GMM format
+ gmm::csr_matrix<Type>* gmmxxLU = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(jacobiDecomposition->getJacobiLU());
+
+ delete jacobiDecomposition;
+
+ LOG4CPLUS_INFO(logger, "Starting iterative Jacobi Solver.");
+
+ // x_(k + 1) = D^-1 * (b - R * x_k)
+ std::vector<Type>* xNext = new std::vector<Type>(x.size());
+ const std::vector<Type>* xCopy = xNext;
+ std::vector<Type>* xCurrent = &x;
+
+ uint_fast64_t iterationCount = 0;
+ do {
+ // R * x_k -> xCurrent
+ gmm::mult(*gmmxxLU, *xCurrent, *xNext);
+ // b - R * x_k
+ gmm::add(b, gmm::scaled(*xNext, -1.0), *xNext);
+ // D^-1 * (b - R * x_k)
+ gmm::mult(*gmmxxDiagonalInverted, *xNext, *xNext);
+
+ std::vector<Type>* swap = xNext;
+ xNext = xCurrent;
+ xCurrent = swap;
+
+ ++iterationCount;
+ } while (gmm::vect_norminf(*xCurrent) > precision);
+
+ delete xCopy;
+
+ LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterationCount << " iterations.");
+ }
};
} //namespace modelChecker
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 433501efb..481ddb93e 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -841,9 +841,13 @@ public:
SparseMatrix<T> *resultDinv = new SparseMatrix<T>(rowCount);
// no entries apart from those on the diagonal
resultDinv->initialize(0);
+
+ // constant 1 for diagonal inversion
+ T constOne = storm::utility::constGetOne<T>();
+
// copy diagonal entries to other matrix
for (int i = 0; i < rowCount; ++i) {
- resultDinv->addNextValue(i, i, resultLU->getValue(i, i));
+ resultDinv->addNextValue(i, i, constOne / resultLU->getValue(i, i));
resultLU->getValue(i, i) = storm::utility::constGetZero<T>();
}
From 9e416b69e5783f8e624f9a731e35fc7fe2852212 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Wed, 23 Jan 2013 22:44:34 +0100
Subject: [PATCH 04/30] The GmmxxAdapter converts to a Row-Major Matrix, not
column-major.
---
src/adapters/GmmxxAdapter.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h
index 3fd990a46..1d0fde721 100644
--- a/src/adapters/GmmxxAdapter.h
+++ b/src/adapters/GmmxxAdapter.h
@@ -23,7 +23,7 @@ class GmmxxAdapter {
public:
/*!
* Converts a sparse matrix into the sparse matrix in the gmm++ format.
- * @return A pointer to a column-major sparse matrix in gmm++ format.
+ * @return A pointer to a row-major sparse matrix in gmm++ format.
*/
template<class T>
static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SparseMatrix<T> const& matrix) {
From ad3922ec180edb25e62c8fc0778c60a653375213 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Wed, 23 Jan 2013 22:49:32 +0100
Subject: [PATCH 05/30] Fixed a bug in the GmmAdapter with non-square matrices
being truncated.
---
src/adapters/GmmxxAdapter.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h
index 1d0fde721..96f3505ec 100644
--- a/src/adapters/GmmxxAdapter.h
+++ b/src/adapters/GmmxxAdapter.h
@@ -31,7 +31,7 @@ public:
LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format.");
// Prepare the resulting matrix.
- gmm::csr_matrix<T>* result = new gmm::csr_matrix<T>(matrix.rowCount, matrix.rowCount);
+ gmm::csr_matrix<T>* result = new gmm::csr_matrix<T>(matrix.rowCount, matrix.colCount);
// Copy Row Indications
std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), std::back_inserter(result->jc));
From 4bb76d026895426fd42f8a712fb89d79b89fdb33 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Thu, 24 Jan 2013 01:18:22 +0100
Subject: [PATCH 06/30] Added EigenAdapter and a Test for the Adapter. Fixed a
type in EigenDtmcPrctlModelChecker.h Added missing transitions in one example
input file
---
src/adapters/EigenAdapter.h | 57 +++++++++++
src/modelChecker/EigenDtmcPrctlModelChecker.h | 2 +-
src/storage/SparseMatrix.h | 3 +-
test/eigen/EigenAdapterTest.cpp | 96 +++++++++++++++++++
4 files changed, 156 insertions(+), 2 deletions(-)
create mode 100644 src/adapters/EigenAdapter.h
create mode 100644 test/eigen/EigenAdapterTest.cpp
diff --git a/src/adapters/EigenAdapter.h b/src/adapters/EigenAdapter.h
new file mode 100644
index 000000000..d7c8169e0
--- /dev/null
+++ b/src/adapters/EigenAdapter.h
@@ -0,0 +1,57 @@
+/*
+ * EigenAdapter.h
+ *
+ * Created on: 21.01.2013
+ * Author: Philipp Berger
+ */
+
+#ifndef STORM_ADAPTERS_EIGENADAPTER_H_
+#define STORM_ADAPTERS_EIGENADAPTER_H_
+
+#include "src/storage/SparseMatrix.h"
+#include "Eigen/Sparse"
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+extern log4cplus::Logger logger;
+
+namespace storm {
+
+namespace adapters {
+
+class EigenAdapter {
+public:
+ /*!
+ * Converts a sparse matrix into the sparse matrix in the eigen format.
+ * @return A pointer to a row-major sparse matrix in eigen format.
+ */
+ template<class T>
+ static Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>* toEigenSparseMatrix(storm::storage::SparseMatrix<T> const& matrix) {
+ uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount();
+ LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to Eigen format.");
+
+ // Prepare the resulting matrix.
+ Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>* result = new Eigen::SparseMatrix<T, Eigen::RowMajor, int_fast32_t>(matrix.rowCount, matrix.colCount);
+
+ result->resizeNonZeros(realNonZeros);
+ //result->reserve(realNonZeros);
+
+ // Copy Row Indications
+ std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), (result->outerIndexPtr()));
+ // Copy Columns Indications
+ std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), (result->innerIndexPtr()));
+ // And do the same thing with the actual values.
+ std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), (result->valuePtr()));
+
+ LOG4CPLUS_DEBUG(logger, "Done converting matrix to Eigen format.");
+
+ return result;
+ }
+};
+
+} //namespace adapters
+
+} //namespace storm
+
+#endif /* STORM_ADAPTERS_GMMXXADAPTER_H_ */
diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h
index e6ea58725..26a18cd8d 100644
--- a/src/modelChecker/EigenDtmcPrctlModelChecker.h
+++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h
@@ -87,7 +87,7 @@ public:
// First, we need to compute the states that satisfy the sub-formula of the next-formula.
storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild());
- // Transform the transition probability matrix to the gmm++ format to use its arithmetic.
+ // Transform the transition probability matrix to the eigen format to use its arithmetic.
Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = this->getModel().getTransitionProbabilityMatrix()->toEigenSparseMatrix();
// Create the vector with which to multiply and initialize it correctly.
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 481ddb93e..fb06f905f 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -25,7 +25,7 @@
extern log4cplus::Logger logger;
// Forward declaration for adapter classes.
-namespace storm { namespace adapters{ class GmmxxAdapter; } }
+namespace storm { namespace adapters{ class GmmxxAdapter; class EigenAdapter; } }
namespace storm {
@@ -43,6 +43,7 @@ public:
* Declare adapter classes as friends to use internal data.
*/
friend class storm::adapters::GmmxxAdapter;
+ friend class storm::adapters::EigenAdapter;
/*!
* If we only want to iterate over the columns of the non-zero entries of
diff --git a/test/eigen/EigenAdapterTest.cpp b/test/eigen/EigenAdapterTest.cpp
new file mode 100644
index 000000000..bddb74dd7
--- /dev/null
+++ b/test/eigen/EigenAdapterTest.cpp
@@ -0,0 +1,96 @@
+#include "gtest/gtest.h"
+
+#include "Eigen/Sparse"
+#include "src/adapters/EigenAdapter.h"
+#include "src/exceptions/InvalidArgumentException.h"
+#include "boost/integer/integer_mask.hpp"
+
+#define STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5
+#define STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5
+
+TEST(EigenAdapterTest, SimpleDenseSquareCopy) {
+ // 5 rows
+ storm::storage::SparseMatrix<double> sm(STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
+
+ double values[STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE];
+ sm.initialize(STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
+
+ int row = 0;
+ int col = 0;
+ for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) {
+ values[i] = static_cast<double>(i + 1);
+
+ sm.addNextValue(row, col, values[i]);
+ ++col;
+ if (col == STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) {
+ ++row;
+ col = 0;
+ }
+ }
+ sm.finalize();
+
+ auto esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(sm);
+
+ ASSERT_EQ(esm->rows(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
+ ASSERT_EQ(esm->cols(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
+ ASSERT_EQ(esm->nonZeros(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE);
+
+ row = 0;
+ col = 0;
+ for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) {
+ ASSERT_EQ(values[i], esm->coeff(row, col));
+ ++col;
+ if (col == STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) {
+ ++row;
+ col = 0;
+ }
+ }
+}
+
+TEST(EigenAdapterTest, SimpleSparseSquareCopy) {
+ // 5 rows
+ storm::storage::SparseMatrix<double> sm(STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
+
+ double values[STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE];
+ sm.initialize((STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2);
+
+ int row = 0;
+ int col = 0;
+
+ bool everySecondElement = true;
+
+ for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) {
+ values[i] = static_cast<double>(i + 1);
+ if (everySecondElement) {
+ sm.addNextValue(row, col, values[i]);
+ }
+ everySecondElement = !everySecondElement;
+ ++col;
+ if (col == STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) {
+ ++row;
+ col = 0;
+ }
+ }
+ sm.finalize();
+
+ auto esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(sm);
+
+ ASSERT_EQ(esm->rows(), STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
+ ASSERT_EQ(esm->cols(), STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE);
+ ASSERT_EQ(esm->nonZeros(), (STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2);
+
+ row = 0;
+ col = 0;
+ everySecondElement = true;
+ for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) {
+ if (everySecondElement) {
+ ASSERT_EQ(values[i], esm->coeff(row, col));
+ }
+ everySecondElement = !everySecondElement;
+ ++col;
+ if (col == STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) {
+ ++row;
+ col = 0;
+ }
+ }
+}
From df91728da0de2f8c4e9cd456f591acf8c31efb09 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Thu, 24 Jan 2013 23:28:45 +0100
Subject: [PATCH 07/30] first "kind of working" version.
---
src/formula/AbstractFormula.h | 65 +++++++++++++++++++
...ctlPathFormula.h => AbstractPathFormula.h} | 32 +++++----
...lStateFormula.h => AbstractStateFormula.h} | 31 +++++----
src/formula/And.h | 39 ++++++-----
src/formula/Ap.h | 25 ++++---
src/formula/BoundOperator.h | 38 ++++++-----
src/formula/BoundedEventually.h | 34 ++++++----
src/formula/BoundedUntil.h | 40 +++++++-----
src/formula/CumulativeReward.h | 26 +++++---
src/formula/Eventually.h | 39 ++++++-----
src/formula/Formulas.h | 7 +-
src/formula/Globally.h | 36 ++++++----
src/formula/InstantaneousReward.h | 26 +++++---
src/formula/Next.h | 34 ++++++----
src/formula/NoBoundOperator.h | 38 ++++++-----
src/formula/Not.h | 32 +++++----
src/formula/Or.h | 41 +++++++-----
src/formula/PctlFormula.h | 48 --------------
src/formula/ProbabilisticBoundOperator.h | 18 ++---
src/formula/ProbabilisticNoBoundOperator.h | 18 ++---
src/formula/ReachabilityReward.h | 36 ++++++----
src/formula/RewardBoundOperator.h | 16 ++---
src/formula/RewardNoBoundOperator.h | 18 ++---
src/formula/Until.h | 40 +++++++-----
src/modelChecker/AbstractModelChecker.h | 43 ++++++++++++
src/modelChecker/DtmcPrctlModelChecker.h | 18 ++---
src/parser/PrctlParser.cpp | 6 +-
src/parser/PrctlParser.h | 5 +-
28 files changed, 525 insertions(+), 324 deletions(-)
create mode 100644 src/formula/AbstractFormula.h
rename src/formula/{PctlPathFormula.h => AbstractPathFormula.h} (60%)
rename src/formula/{PctlStateFormula.h => AbstractStateFormula.h} (63%)
delete mode 100644 src/formula/PctlFormula.h
create mode 100644 src/modelChecker/AbstractModelChecker.h
diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
new file mode 100644
index 000000000..8bd8b8782
--- /dev/null
+++ b/src/formula/AbstractFormula.h
@@ -0,0 +1,65 @@
+/*
+ * Abstractformula.h
+ *
+ * Created on: 19.10.2012
+ * Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_AbstractFORMULA_H_
+#define STORM_FORMULA_AbstractFORMULA_H_
+
+#include <string>
+
+namespace storm { namespace formula {
+template <class T> class AbstractFormula;
+}}
+
+#include "src/modelChecker/AbstractModelChecker.h"
+
+namespace storm {
+namespace formula {
+
+
+//abstract
+/*!
+ * @brief
+ * Abstract base class for Abstract formulas in general.
+ *
+ * @attention This class is abstract.
+ * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
+ * the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes
+ * AbstractPathFormula and AbstractStateFormula offer the method clone().
+ */
+template <class T>
+class AbstractFormula {
+
+public:
+ /*!
+ * virtual destructor
+ */
+ virtual ~AbstractFormula() { }
+
+ /*!
+ * @note This function is not implemented in this class.
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const = 0;
+
+ template <template <class Type> class MC>
+ const MC<T>* cast(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ try {
+ const MC<T>& mc = dynamic_cast<const MC<T>&>(modelChecker);
+ return &mc;
+ } catch (std::bad_cast& bc) {
+ std::cerr << "Bad cast: tried to cast " << typeid(modelChecker).name() << " to " << typeid(MC<T>).name() << std::endl;
+
+ }
+ return nullptr;
+ }
+};
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_AbstractFORMULA_H_ */
diff --git a/src/formula/PctlPathFormula.h b/src/formula/AbstractPathFormula.h
similarity index 60%
rename from src/formula/PctlPathFormula.h
rename to src/formula/AbstractPathFormula.h
index f929c642a..cba3425fa 100644
--- a/src/formula/PctlPathFormula.h
+++ b/src/formula/AbstractPathFormula.h
@@ -1,16 +1,23 @@
/*
- * PctlPathFormula.h
+ * AbstractPathFormula.h
*
* Created on: 19.10.2012
* Author: Thomas Heinemann
*/
-#ifndef STORM_FORMULA_PCTLPATHFORMULA_H_
-#define STORM_FORMULA_PCTLPATHFORMULA_H_
+#ifndef STORM_FORMULA_AbstractPATHFORMULA_H_
+#define STORM_FORMULA_AbstractPATHFORMULA_H_
-#include "PctlFormula.h"
-#include "modelChecker/DtmcPrctlModelChecker.h"
+namespace storm { namespace formula {
+template <class T> class AbstractPathFormula;
+}}
+
+#include "src/formula/AbstractFormula.h"
+
+#include "modelChecker/AbstractModelChecker.h"
#include <vector>
+#include <iostream>
+#include <typeinfo>
namespace storm {
@@ -18,7 +25,7 @@ namespace formula {
/*!
* @brief
- * Abstract base class for PCTL path formulas.
+ * Abstract base class for Abstract path formulas.
*
* @attention This class is abstract.
* @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
@@ -26,13 +33,13 @@ namespace formula {
* clone().
*/
template <class T>
-class PctlPathFormula : public PctlFormula<T> {
+class AbstractPathFormula : public virtual AbstractFormula<T> {
public:
/*!
* empty destructor
*/
- virtual ~PctlPathFormula() { }
+ virtual ~AbstractPathFormula() { }
/*!
* Clones the called object.
@@ -42,7 +49,7 @@ public:
* @note This function is not implemented in this class.
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const = 0;
+ virtual AbstractPathFormula<T>* clone() const = 0;
/*!
* Calls the model checker to check this formula.
@@ -55,11 +62,14 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
+ virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
+ return nullptr;
+ }
};
} //namespace formula
} //namespace storm
-#endif /* STORM_FORMULA_PCTLPATHFORMULA_H_ */
+#endif /* STORM_FORMULA_AbstractPATHFORMULA_H_ */
diff --git a/src/formula/PctlStateFormula.h b/src/formula/AbstractStateFormula.h
similarity index 63%
rename from src/formula/PctlStateFormula.h
rename to src/formula/AbstractStateFormula.h
index bfd035e4d..f17f7eda0 100644
--- a/src/formula/PctlStateFormula.h
+++ b/src/formula/AbstractStateFormula.h
@@ -1,16 +1,20 @@
/*
- * PctlStateFormula.h
+ * AbstractStateFormula.h
*
* Created on: 19.10.2012
* Author: Thomas Heinemann
*/
-#ifndef STORM_FORMULA_PCTLSTATEFORMULA_H_
-#define STORM_FORMULA_PCTLSTATEFORMULA_H_
+#ifndef STORM_FORMULA_AbstractSTATEFORMULA_H_
+#define STORM_FORMULA_AbstractSTATEFORMULA_H_
-#include "PctlFormula.h"
-#include "storage/BitVector.h"
-#include "modelChecker/DtmcPrctlModelChecker.h"
+namespace storm { namespace formula {
+template <class T> class AbstractStateFormula;
+}}
+
+#include "AbstractFormula.h"
+#include "src/storage/BitVector.h"
+#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
@@ -18,7 +22,7 @@ namespace formula {
/*!
* @brief
- * Abstract base class for PCTL state formulas.
+ * Abstract base class for Abstract state formulas.
*
* @attention This class is abstract.
* @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
@@ -26,13 +30,13 @@ namespace formula {
* clone().
*/
template <class T>
-class PctlStateFormula : public PctlFormula<T> {
+class AbstractStateFormula : public AbstractFormula<T> {
public:
/*!
* empty destructor
*/
- virtual ~PctlStateFormula() { }
+ virtual ~AbstractStateFormula() { }
/*!
* Clones the called object.
@@ -42,7 +46,7 @@ public:
* @note This function is not implemented in this class.
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const = 0;
+ virtual AbstractStateFormula<T>* clone() const = 0;
/*!
* Calls the model checker to check this formula.
@@ -55,7 +59,10 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
+ virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
+ return nullptr;
+ }
};
} //namespace formula
@@ -63,4 +70,4 @@ public:
} //namespace storm
-#endif /* STORM_FORMULA_PCTLSTATEFORMULA_H_ */
+#endif /* STORM_FORMULA_AbstractSTATEFORMULA_H_ */
diff --git a/src/formula/And.h b/src/formula/And.h
index d166fd7c5..33e69ee1d 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -8,18 +8,25 @@
#ifndef STORM_FORMULA_AND_H_
#define STORM_FORMULA_AND_H_
-#include "PctlStateFormula.h"
+#include "AbstractStateFormula.h"
#include <string>
namespace storm {
-
namespace formula {
+template <class T> class And;
+
+template <class T>
+class IAndModelChecker {
+ public:
+ virtual storm::storage::BitVector* checkAnd(const And<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with AND node as root.
+ * Class for a Abstract formula tree with AND node as root.
*
- * Has two PCTL state formulas as sub formulas/trees.
+ * Has two Abstract state formulas as sub formulas/trees.
*
* As AND is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
@@ -27,11 +34,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
- * @see PctlStateFormula
- * @see PctlFormula
+ * @see AbstractStateFormula
+ * @see AbstractFormula
*/
template <class T>
-class And : public PctlStateFormula<T> {
+class And : public AbstractStateFormula<T> {
public:
/*!
@@ -50,7 +57,7 @@ public:
* @param left The left sub formula
* @param right The right sub formula
*/
- And(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
+ And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
this->left = left;
this->right = right;
}
@@ -75,7 +82,7 @@ public:
*
* @param newLeft the new left child.
*/
- void setLeft(PctlStateFormula<T>* newLeft) {
+ void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@@ -84,21 +91,21 @@ public:
*
* @param newRight the new right child.
*/
- void setRight(PctlStateFormula<T>* newRight) {
+ void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
- const PctlStateFormula<T>& getLeft() const {
+ const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
- const PctlStateFormula<T>& getRight() const {
+ const AbstractStateFormula<T>& getRight() const {
return *right;
}
@@ -121,7 +128,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
And<T>* result = new And();
if (this->left != NULL) {
result->setLeft(left->clone());
@@ -141,13 +148,13 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const IAndModelChecker<T>& modelChecker) const {
return modelChecker.checkAnd(*this);
}
private:
- PctlStateFormula<T>* left;
- PctlStateFormula<T>* right;
+ AbstractStateFormula<T>* left;
+ AbstractStateFormula<T>* right;
};
} //namespace formula
diff --git a/src/formula/Ap.h b/src/formula/Ap.h
index e479d0c61..8eb4dbe5b 100644
--- a/src/formula/Ap.h
+++ b/src/formula/Ap.h
@@ -8,23 +8,32 @@
#ifndef STORM_FORMULA_AP_H_
#define STORM_FORMULA_AP_H_
-#include "PctlStateFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
namespace formula {
+template <class T> class Ap;
+
+template <class T>
+class IApModelChecker {
+ public:
+ virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with atomic proposition as root.
+ * Class for a Abstract formula tree with atomic proposition as root.
*
* This class represents the leaves in the formula tree.
*
- * @see PctlStateFormula
- * @see PctlFormula
+ * @see AbstractStateFormula
+ * @see AbstractFormula
*/
template <class T>
-class Ap : public PctlStateFormula<T> {
+class Ap : public AbstractStateFormula<T> {
public:
/*!
@@ -64,7 +73,7 @@ public:
*
* @returns a new Ap-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
return new Ap(ap);
}
@@ -77,8 +86,8 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkAp(*this);
+ virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return this->template cast<IApModelChecker>(modelChecker)->checkAp(*this);
}
private:
diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h
index 0d0abedbd..2333897e7 100644
--- a/src/formula/BoundOperator.h
+++ b/src/formula/BoundOperator.h
@@ -8,20 +8,28 @@
#ifndef STORM_FORMULA_BOUNDOPERATOR_H_
#define STORM_FORMULA_BOUNDOPERATOR_H_
-#include "PctlStateFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "AbstractPathFormula.h"
#include "utility/ConstTemplates.h"
namespace storm {
namespace formula {
+template <class T> class BoundUntil;
+
+template <class T>
+class IBoundUntilModelChecker {
+ public:
+ virtual storm::storage::BitVector* checkBoundUntil(const BoundUntil<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval
+ * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
* as root.
*
- * Has one PCTL path formula as sub formula/tree.
+ * Has one Abstract path formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff the probability that the path formula holds is inside the bounds
@@ -31,14 +39,14 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template<class T>
-class BoundOperator : public PctlStateFormula<T> {
+class BoundOperator : public AbstractStateFormula<T> {
public:
enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
@@ -50,7 +58,7 @@ public:
* @param upperBound The upper bound for the probability
* @param pathFormula The child node
*/
- BoundOperator(ComparisonType comparisonOperator, T bound, PctlPathFormula<T>* pathFormula)
+ BoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
// Intentionally left empty
}
@@ -68,9 +76,9 @@ public:
}
/*!
- * @returns the child node (representation of a PCTL path formula)
+ * @returns the child node (representation of a Abstract path formula)
*/
- const PctlPathFormula<T>& getPathFormula () const {
+ const AbstractPathFormula<T>& getPathFormula () const {
return *pathFormula;
}
@@ -79,7 +87,7 @@ public:
*
* @param pathFormula the path formula that becomes the new child node
*/
- void setPathFormula(PctlPathFormula<T>* pathFormula) {
+ void setPathFormula(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
@@ -134,7 +142,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const = 0;
+ virtual AbstractStateFormula<T>* clone() const = 0;
/*!
* Calls the model checker to check this formula.
@@ -145,14 +153,14 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const IBoundUntilModelChecker<T>& modelChecker) const {
return modelChecker.checkBoundOperator(*this);
}
private:
ComparisonType comparisonOperator;
T bound;
- PctlPathFormula<T>* pathFormula;
+ AbstractPathFormula<T>* pathFormula;
};
} //namespace formula
diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h
index 0a66f6b83..bb7585ff9 100644
--- a/src/formula/BoundedEventually.h
+++ b/src/formula/BoundedEventually.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_
#define STORM_FORMULA_BOUNDEDEVENTUALLY_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -17,11 +17,19 @@ namespace storm {
namespace formula {
+template <class T> class BoundedEventually;
+
+template <class T>
+class IBoundedEventuallyModelChecker {
+ public:
+ virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a BoundedEventually node as root.
+ * Class for a Abstract (path) formula tree with a BoundedEventually node as root.
*
- * Has one PCTL state formulas as sub formula/tree.
+ * Has one Abstract state formulas as sub formula/tree.
*
* @par Semantics
* The formula holds iff in at most \e bound steps, formula \e child holds.
@@ -29,11 +37,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class BoundedEventually : public PctlPathFormula<T> {
+class BoundedEventually : public AbstractPathFormula<T> {
public:
/*!
@@ -50,7 +58,7 @@ public:
* @param child The child formula subtree
* @param bound The maximal number of steps
*/
- BoundedEventually(PctlStateFormula<T>* child, uint_fast64_t bound) {
+ BoundedEventually(AbstractStateFormula<T>* child, uint_fast64_t bound) {
this->child = child;
this->bound = bound;
}
@@ -70,7 +78,7 @@ public:
/*!
* @returns the child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -78,7 +86,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -116,7 +124,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
BoundedEventually<T>* result = new BoundedEventually<T>();
result->setBound(bound);
if (child != nullptr) {
@@ -135,12 +143,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IBoundedEventuallyModelChecker<T>& modelChecker) const {
return modelChecker.checkBoundedEventually(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
uint_fast64_t bound;
};
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 675138e27..90d5ca10b 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_BOUNDEDUNTIL_H_
#define STORM_FORMULA_BOUNDEDUNTIL_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -17,11 +17,19 @@ namespace storm {
namespace formula {
+template <class T> class BoundedUntil;
+
+template <class T>
+class IBoundedUntilModelChecker {
+ public:
+ virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a BoundedUntil node as root.
+ * Class for a Abstract (path) formula tree with a BoundedUntil node as root.
*
- * Has two PCTL state formulas as sub formulas/trees.
+ * Has two Abstract state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
@@ -30,11 +38,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class BoundedUntil : public PctlPathFormula<T> {
+class BoundedUntil : public AbstractPathFormula<T> {
public:
/*!
@@ -53,7 +61,7 @@ public:
* @param right The left formula subtree
* @param bound The maximal number of steps
*/
- BoundedUntil(PctlStateFormula<T>* left, PctlStateFormula<T>* right,
+ BoundedUntil(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right,
uint_fast64_t bound) {
this->left = left;
this->right = right;
@@ -80,7 +88,7 @@ public:
*
* @param newLeft the new left child.
*/
- void setLeft(PctlStateFormula<T>* newLeft) {
+ void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@@ -89,21 +97,21 @@ public:
*
* @param newRight the new right child.
*/
- void setRight(PctlStateFormula<T>* newRight) {
+ void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
- const PctlStateFormula<T>& getLeft() const {
+ const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
- const PctlStateFormula<T>& getRight() const {
+ const AbstractStateFormula<T>& getRight() const {
return *right;
}
@@ -144,7 +152,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
BoundedUntil<T>* result = new BoundedUntil<T>();
result->setBound(bound);
if (left != NULL) {
@@ -166,13 +174,13 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IBoundedUntilModelChecker<T>& modelChecker) const {
return modelChecker.checkBoundedUntil(*this);
}
private:
- PctlStateFormula<T>* left;
- PctlStateFormula<T>* right;
+ AbstractStateFormula<T>* left;
+ AbstractStateFormula<T>* right;
uint_fast64_t bound;
};
diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h
index cbbf1e18b..2587390ea 100644
--- a/src/formula/CumulativeReward.h
+++ b/src/formula/CumulativeReward.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_CUMULATIVEREWARD_H_
#define STORM_FORMULA_CUMULATIVEREWARD_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -17,18 +17,26 @@ namespace storm {
namespace formula {
+template <class T> class CumulativeReward;
+
+template <class T>
+class ICumulativeRewardModelChecker {
+ public:
+ virtual std::vector<T>* checkCumulativeReward(const CumulativeReward<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a Cumulative Reward node as root.
+ * Class for a Abstract (path) formula tree with a Cumulative Reward node as root.
*
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class CumulativeReward : public PctlPathFormula<T> {
+class CumulativeReward : public AbstractPathFormula<T> {
public:
/*!
@@ -84,9 +92,9 @@ public:
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns a new CumulativeReward-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
return new CumulativeReward(bound);
}
@@ -100,7 +108,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const ICumulativeRewardModelChecker<T>& modelChecker) const {
return modelChecker.checkCumulativeReward(*this);
}
diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h
index 1a781fbb7..32e6d126a 100644
--- a/src/formula/Eventually.h
+++ b/src/formula/Eventually.h
@@ -8,18 +8,27 @@
#ifndef STORM_FORMULA_EVENTUALLY_H_
#define STORM_FORMULA_EVENTUALLY_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
namespace formula {
+template <class T> class Eventually;
+
+template <class T>
+class IEventuallyModelChecker {
+ public:
+ virtual std::vector<T>* checkEventually(const Eventually<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with an Eventually node as root.
+ * Class for a Abstract (path) formula tree with an Eventually node as root.
*
- * Has one PCTL state formula as sub formula/tree.
+ * Has one Abstract state formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff eventually \e child holds.
@@ -27,11 +36,11 @@ namespace formula {
* The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to nullptr before deletion)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class Eventually : public PctlPathFormula<T> {
+class Eventually : public AbstractPathFormula<T> {
public:
/*!
@@ -46,7 +55,7 @@ public:
*
* @param child The child node
*/
- Eventually(PctlStateFormula<T>* child) {
+ Eventually(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -65,7 +74,7 @@ public:
/*!
* @returns the child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -73,7 +82,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -91,9 +100,9 @@ public:
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns a new Eventually-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
Eventually<T>* result = new Eventually<T>();
if (child != nullptr) {
result->setChild(child);
@@ -110,12 +119,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
- return modelChecker.checkEventually(*this);
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return this->template cast<IEventuallyModelChecker>(modelChecker)->checkEventually(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h
index 70ed03c75..09de1acf0 100644
--- a/src/formula/Formulas.h
+++ b/src/formula/Formulas.h
@@ -8,15 +8,16 @@
#ifndef STORM_FORMULA_FORMULAS_H_
#define STORM_FORMULA_FORMULAS_H_
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+
#include "And.h"
#include "Ap.h"
#include "BoundedUntil.h"
#include "Next.h"
#include "Not.h"
#include "Or.h"
-#include "PctlFormula.h"
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
#include "ProbabilisticNoBoundOperator.h"
#include "ProbabilisticBoundOperator.h"
#include "Until.h"
diff --git a/src/formula/Globally.h b/src/formula/Globally.h
index 02a18b884..115d96673 100644
--- a/src/formula/Globally.h
+++ b/src/formula/Globally.h
@@ -8,18 +8,26 @@
#ifndef STORM_FORMULA_GLOBALLY_H_
#define STORM_FORMULA_GLOBALLY_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
+template <class T> class Globally;
+
+template <class T>
+class IGloballyModelChecker {
+ public:
+ virtual std::vector<T>* checkGlobally(const Globally<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a Globally node as root.
+ * Class for a Abstract (path) formula tree with a Globally node as root.
*
- * Has one PCTL state formula as sub formula/tree.
+ * Has one Abstract state formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff globally \e child holds.
@@ -27,11 +35,11 @@ namespace formula {
* The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to nullptr before deletion)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class Globally : public PctlPathFormula<T> {
+class Globally : public AbstractPathFormula<T> {
public:
/*!
@@ -46,7 +54,7 @@ public:
*
* @param child The child node
*/
- Globally(PctlStateFormula<T>* child) {
+ Globally(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -65,7 +73,7 @@ public:
/*!
* @returns the child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -73,7 +81,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -91,9 +99,9 @@ public:
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns a new Globally-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
Next<T>* result = new Next<T>();
if (child != nullptr) {
result->setChild(child);
@@ -110,12 +118,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IGloballyModelChecker<T>& modelChecker) const {
return modelChecker.checkGlobally(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h
index d6067d344..319e38f49 100644
--- a/src/formula/InstantaneousReward.h
+++ b/src/formula/InstantaneousReward.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_INSTANTANEOUSREWARD_H_
#define STORM_FORMULA_INSTANTANEOUSREWARD_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -17,18 +17,26 @@ namespace storm {
namespace formula {
+template <class T> class InstantaneousReward;
+
+template <class T>
+class IInstantaneousRewardModelChecker {
+ public:
+ virtual std::vector<T>* checkInstantaneousReward(const InstantaneousReward<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a Instantaneous Reward node as root.
+ * Class for a Abstract (path) formula tree with a Instantaneous Reward node as root.
*
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class InstantaneousReward : public PctlPathFormula<T> {
+class InstantaneousReward : public AbstractPathFormula<T> {
public:
/*!
@@ -84,9 +92,9 @@ public:
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns a new InstantaneousReward-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
return new InstantaneousReward(bound);
}
@@ -100,7 +108,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IInstantaneousRewardModelChecker<T>& modelChecker) const {
return modelChecker.checkInstantaneousReward(*this);
}
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 7b8214757..501277bba 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -8,18 +8,26 @@
#ifndef STORM_FORMULA_NEXT_H_
#define STORM_FORMULA_NEXT_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
+template <class T> class Next;
+
+template <class T>
+class INextModelChecker {
+ public:
+ virtual std::vector<T>* checkNext(const Next<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with a Next node as root.
+ * Class for a Abstract (path) formula tree with a Next node as root.
*
- * Has two PCTL state formulas as sub formulas/trees.
+ * Has two Abstract state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff in the next step, \e child holds
@@ -27,11 +35,11 @@ namespace formula {
* The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class Next : public PctlPathFormula<T> {
+class Next : public AbstractPathFormula<T> {
public:
/*!
@@ -46,7 +54,7 @@ public:
*
* @param child The child node
*/
- Next(PctlStateFormula<T>* child) {
+ Next(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -65,7 +73,7 @@ public:
/*!
* @returns the child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -73,7 +81,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -95,7 +103,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
Next<T>* result = new Next<T>();
if (child != NULL) {
result->setChild(child);
@@ -112,12 +120,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const INextModelChecker<T>& modelChecker) const {
return modelChecker.checkNext(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h
index 204c102a8..eeb8d2c54 100644
--- a/src/formula/NoBoundOperator.h
+++ b/src/formula/NoBoundOperator.h
@@ -8,26 +8,34 @@
#ifndef STORM_FORMULA_NOBOUNDOPERATOR_H_
#define STORM_FORMULA_NOBOUNDOPERATOR_H_
-#include "PctlFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
namespace storm {
namespace formula {
+template <class T> class NoBoundOperator;
+
+template <class T>
+class INoBoundOperatorModelChecker {
+ public:
+ virtual std::vector<T>* checkNoBoundOperator(const NoBoundOperator<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with a P (probablistic) operator without declaration of probabilities
+ * Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities
* as root.
*
* Checking a formula with this operator as root returns the probabilities that the path formula holds
* (for each state)
*
- * Has one PCTL path formula as sub formula/tree.
+ * Has one Abstract path formula as sub formula/tree.
*
* @note
* This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
- * Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula.
+ * Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula.
*
* @note
* This class does not contain a check() method like the other formula classes.
@@ -39,14 +47,14 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template <class T>
-class NoBoundOperator: public storm::formula::PctlFormula<T> {
+class NoBoundOperator: public storm::formula::AbstractFormula<T> {
public:
/*!
* Empty constructor
@@ -60,7 +68,7 @@ public:
*
* @param pathFormula The child node.
*/
- NoBoundOperator(PctlPathFormula<T>* pathFormula) {
+ NoBoundOperator(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
@@ -74,9 +82,9 @@ public:
}
/*!
- * @returns the child node (representation of a PCTL path formula)
+ * @returns the child node (representation of a Abstract path formula)
*/
- const PctlPathFormula<T>& getPathFormula () const {
+ const AbstractPathFormula<T>& getPathFormula () const {
return *pathFormula;
}
@@ -85,7 +93,7 @@ public:
*
* @param pathFormula the path formula that becomes the new child node
*/
- void setPathFormula(PctlPathFormula<T>* pathFormula) {
+ void setPathFormula(AbstractPathFormula<T>* pathFormula) {
this->pathFormula = pathFormula;
}
@@ -100,7 +108,7 @@ public:
*
* @returns A vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual std::vector<T>* check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T>* check(const INoBoundOperatorModelChecker<T>& modelChecker) const {
return modelChecker.checkNoBoundOperator(*this);
}
@@ -110,7 +118,7 @@ public:
virtual std::string toString() const = 0;
private:
- PctlPathFormula<T>* pathFormula;
+ AbstractPathFormula<T>* pathFormula;
};
} /* namespace formula */
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 03d5cf572..9e211084d 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -8,26 +8,34 @@
#ifndef STORM_FORMULA_NOT_H_
#define STORM_FORMULA_NOT_H_
-#include "PctlStateFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
+template <class T> class Not;
+
+template <class T>
+class INotModelChecker {
+ public:
+ virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with NOT node as root.
+ * Class for a Abstract formula tree with NOT node as root.
*
- * Has one PCTL state formula as sub formula/tree.
+ * Has one Abstract state formula as sub formula/tree.
*
* The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
- * @see PctlStateFormula
- * @see PctlFormula
+ * @see AbstractStateFormula
+ * @see AbstractFormula
*/
template <class T>
-class Not : public PctlStateFormula<T> {
+class Not : public AbstractStateFormula<T> {
public:
/*!
@@ -41,7 +49,7 @@ public:
* Constructor
* @param child The child node
*/
- Not(PctlStateFormula<T>* child) {
+ Not(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -60,7 +68,7 @@ public:
/*!
* @returns The child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -68,7 +76,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -88,7 +96,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
Not<T>* result = new Not<T>();
if (child != NULL) {
result->setChild(child);
@@ -105,12 +113,12 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const INotModelChecker<T>& modelChecker) const {
return modelChecker.checkNot(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/Or.h b/src/formula/Or.h
index 524ca58e7..79e30cdab 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -8,17 +8,24 @@
#ifndef STORM_FORMULA_OR_H_
#define STORM_FORMULA_OR_H_
-#include "PctlStateFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
-
namespace formula {
+template <class T> class Or;
+
+template <class T>
+class IOrModelChecker {
+ public:
+ virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL formula tree with OR node as root.
+ * Class for a Abstract formula tree with OR node as root.
*
- * Has two PCTL state formulas as sub formulas/trees.
+ * Has two Abstract state formulas as sub formulas/trees.
*
* As OR is commutative, the order is \e theoretically not important, but will influence the order in which
* the model checker works.
@@ -26,11 +33,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
- * @see PctlStateFormula
- * @see PctlFormula
+ * @see AbstractStateFormula
+ * @see AbstractFormula
*/
template <class T>
-class Or : public PctlStateFormula<T> {
+class Or : public AbstractStateFormula<T> {
public:
/*!
@@ -49,7 +56,7 @@ public:
* @param left The left sub formula
* @param right The right sub formula
*/
- Or(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
+ Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
this->left = left;
this->right = right;
}
@@ -74,7 +81,7 @@ public:
*
* @param newLeft the new left child.
*/
- void setLeft(PctlStateFormula<T>* newLeft) {
+ void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@@ -83,21 +90,21 @@ public:
*
* @param newRight the new right child.
*/
- void setRight(PctlStateFormula<T>* newRight) {
+ void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
- const PctlStateFormula<T>& getLeft() const {
+ const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
- const PctlStateFormula<T>& getRight() const {
+ const AbstractStateFormula<T>& getRight() const {
return *right;
}
@@ -120,7 +127,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
Or<T>* result = new Or();
if (this->left != NULL) {
result->setLeft(left->clone());
@@ -130,7 +137,7 @@ public:
}
return result;
}
-
+
/*!
* Calls the model checker to check this formula.
* Needed to infer the correct type of formula class.
@@ -140,13 +147,13 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual storm::storage::BitVector *check(const IOrModelChecker<T>& modelChecker) const {
return modelChecker.checkOr(*this);
}
private:
- PctlStateFormula<T>* left;
- PctlStateFormula<T>* right;
+ AbstractStateFormula<T>* left;
+ AbstractStateFormula<T>* right;
};
} //namespace formula
diff --git a/src/formula/PctlFormula.h b/src/formula/PctlFormula.h
deleted file mode 100644
index 394e3cfa2..000000000
--- a/src/formula/PctlFormula.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*
- * Pctlformula.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_PCTLFORMULA_H_
-#define STORM_FORMULA_PCTLFORMULA_H_
-
-#include <string>
-
-namespace storm {
-
-namespace formula {
-
-
-//abstract
-/*!
- * @brief
- * Abstract base class for PCTL formulas in general.
- *
- * @attention This class is abstract.
- * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
- * the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes
- * PctlPathFormula and PctlStateFormula offer the method clone().
- */
-template <class T>
-class PctlFormula {
-
-public:
- /*!
- * virtual destructor
- */
- virtual ~PctlFormula() { }
-
- /*!
- * @note This function is not implemented in this class.
- * @returns a string representation of the formula
- */
- virtual std::string toString() const = 0;
-};
-
-} //namespace formula
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_PCTLFORMULA_H_ */
diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h
index e541619c1..37fe7858d 100644
--- a/src/formula/ProbabilisticBoundOperator.h
+++ b/src/formula/ProbabilisticBoundOperator.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
#define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
-#include "PctlStateFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "AbstractPathFormula.h"
#include "BoundOperator.h"
#include "utility/ConstTemplates.h"
@@ -19,10 +19,10 @@ namespace formula {
/*!
* @brief
- * Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval
+ * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
* as root.
*
- * Has one PCTL path formula as sub formula/tree.
+ * Has one Abstract path formula as sub formula/tree.
*
* @par Semantics
* The formula holds iff the probability that the path formula holds is inside the bounds
@@ -32,11 +32,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template<class T>
class ProbabilisticBoundOperator : public BoundOperator<T> {
@@ -56,7 +56,7 @@ public:
* @param upperBound The upper bound for the probability
* @param pathFormula The child node
*/
- ProbabilisticBoundOperator(T lowerBound, T upperBound, PctlPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
+ ProbabilisticBoundOperator(T lowerBound, T upperBound, AbstractPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
// Intentionally left empty
}
@@ -81,7 +81,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
ProbabilisticBoundOperator<T>* result = new ProbabilisticBoundOperator<T>();
result->setInterval(this->getLowerBound(), this->getUpperBound());
result->setPathFormula(this->getPathFormula()->clone());
diff --git a/src/formula/ProbabilisticNoBoundOperator.h b/src/formula/ProbabilisticNoBoundOperator.h
index ad4ab4851..bfe6f92db 100644
--- a/src/formula/ProbabilisticNoBoundOperator.h
+++ b/src/formula/ProbabilisticNoBoundOperator.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
#define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
-#include "PctlFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
#include "NoBoundOperator.h"
namespace storm {
@@ -18,17 +18,17 @@ namespace formula {
/*!
* @brief
- * Class for a PCTL formula tree with a P (probablistic) operator without declaration of probabilities
+ * Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities
* as root.
*
* Checking a formula with this operator as root returns the probabilities that the path formula holds
* (for each state)
*
- * Has one PCTL path formula as sub formula/tree.
+ * Has one Abstract path formula as sub formula/tree.
*
* @note
* This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
- * Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula.
+ * Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula.
*
* @note
* This class does not contain a check() method like the other formula classes.
@@ -40,11 +40,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template <class T>
class ProbabilisticNoBoundOperator: public NoBoundOperator<T> {
@@ -61,7 +61,7 @@ public:
*
* @param pathFormula The child node.
*/
- ProbabilisticNoBoundOperator(PctlPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
+ ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
// Intentionally left empty
}
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index 9f5d6ee43..6fdfb4733 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -8,27 +8,35 @@
#ifndef STORM_FORMULA_REACHABILITYREWARD_H_
#define STORM_FORMULA_REACHABILITYREWARD_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
+template <class T> class ReachabilityReward;
+
+template <class T>
+class IReachabilityRewardModelChecker {
+ public:
+ virtual std::vector<T>* checkReachabilityReward(const ReachabilityReward<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with an Reachability Reward node as root.
+ * Class for a Abstract (path) formula tree with an Reachability Reward node as root.
*
- * Has one PCTL state formula as sub formula/tree.
+ * Has one Abstract state formula as sub formula/tree.
*
* The subtree is seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to nullptr before deletion)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class ReachabilityReward : public PctlPathFormula<T> {
+class ReachabilityReward : public AbstractPathFormula<T> {
public:
/*!
@@ -43,7 +51,7 @@ public:
*
* @param child The child node
*/
- ReachabilityReward(PctlStateFormula<T>* child) {
+ ReachabilityReward(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -62,7 +70,7 @@ public:
/*!
* @returns the child node
*/
- const PctlStateFormula<T>& getChild() const {
+ const AbstractStateFormula<T>& getChild() const {
return *child;
}
@@ -70,7 +78,7 @@ public:
* Sets the subtree
* @param child the new child node
*/
- void setChild(PctlStateFormula<T>* child) {
+ void setChild(AbstractStateFormula<T>* child) {
this->child = child;
}
@@ -88,9 +96,9 @@ public:
*
* Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
*
- * @returns a new BoundedUntil-object that is identical the called object.
+ * @returns a new ReachabilityReward-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
ReachabilityReward<T>* result = new ReachabilityReward<T>();
if (child != nullptr) {
result->setChild(child);
@@ -107,12 +115,12 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IReachabilityRewardModelChecker<T>& modelChecker) const {
return modelChecker.checkReachabilityReward(*this);
}
private:
- PctlStateFormula<T>* child;
+ AbstractStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h
index 8118fdbe2..26f6ae7aa 100644
--- a/src/formula/RewardBoundOperator.h
+++ b/src/formula/RewardBoundOperator.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_REWARDBOUNDOPERATOR_H_
#define STORM_FORMULA_REWARDBOUNDOPERATOR_H_
-#include "PctlStateFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "AbstractPathFormula.h"
#include "BoundOperator.h"
#include "utility/ConstTemplates.h"
@@ -19,7 +19,7 @@ namespace formula {
/*!
* @brief
- * Class for a PCTL formula tree with a R (reward) operator node over a reward interval as root.
+ * Class for a Abstract formula tree with a R (reward) operator node over a reward interval as root.
*
* Has a reward path formula as sub formula/tree.
*
@@ -31,11 +31,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticNoBoundsOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template<class T>
class RewardBoundOperator : public BoundOperator<T> {
@@ -55,7 +55,7 @@ public:
* @param upperBound The upper bound for the probability
* @param pathFormula The child node
*/
- RewardBoundOperator(T lowerBound, T upperBound, PctlPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
+ RewardBoundOperator(T lowerBound, T upperBound, AbstractPathFormula<T>& pathFormula) : BoundOperator<T>(lowerBound, upperBound, pathFormula) {
// Intentionally left empty
}
@@ -80,7 +80,7 @@ public:
*
* @returns a new AND-object that is identical the called object.
*/
- virtual PctlStateFormula<T>* clone() const {
+ virtual AbstractStateFormula<T>* clone() const {
RewardBoundOperator<T>* result = new RewardBoundOperator<T>();
result->setBound(this->getLowerBound(), this->getUpperBound());
result->setPathFormula(this->getPathFormula()->clone());
diff --git a/src/formula/RewardNoBoundOperator.h b/src/formula/RewardNoBoundOperator.h
index 3362ff136..3752b381a 100644
--- a/src/formula/RewardNoBoundOperator.h
+++ b/src/formula/RewardNoBoundOperator.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_
#define STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_
-#include "PctlFormula.h"
-#include "PctlPathFormula.h"
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
#include "NoBoundOperator.h"
namespace storm {
@@ -18,17 +18,17 @@ namespace formula {
/*!
* @brief
- * Class for a PCTL formula tree with a R (reward) operator without declaration of reward values
+ * Class for a Abstract formula tree with a R (reward) operator without declaration of reward values
* as root.
*
* Checking a formula with this operator as root returns the reward for the reward path formula for
* each state
*
- * Has one PCTL path formula as sub formula/tree.
+ * Has one Abstract path formula as sub formula/tree.
*
* @note
* This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
- * Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula.
+ * Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula.
*
* @note
* This class does not contain a check() method like the other formula classes.
@@ -40,11 +40,11 @@ namespace formula {
* (this behavior can be prevented by setting them to NULL before deletion)
*
*
- * @see PctlStateFormula
- * @see PctlPathFormula
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
* @see ProbabilisticOperator
* @see ProbabilisticIntervalOperator
- * @see PctlFormula
+ * @see AbstractFormula
*/
template <class T>
class RewardNoBoundOperator: public NoBoundOperator<T> {
@@ -61,7 +61,7 @@ public:
*
* @param pathFormula The child node.
*/
- RewardNoBoundOperator(PctlPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
+ RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula) : NoBoundOperator<T>(pathFormula) {
// Intentionally left empty
}
diff --git a/src/formula/Until.h b/src/formula/Until.h
index be86a1153..94f917a60 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -8,18 +8,26 @@
#ifndef STORM_FORMULA_UNTIL_H_
#define STORM_FORMULA_UNTIL_H_
-#include "PctlPathFormula.h"
-#include "PctlStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
namespace storm {
namespace formula {
+template <class T> class Until;
+
+template <class T>
+class IUntilModelChecker {
+ public:
+ virtual std::vector<T>* checkUntil(const Until<T>& obj) const = 0;
+};
+
/*!
* @brief
- * Class for a PCTL (path) formula tree with an Until node as root.
+ * Class for a Abstract (path) formula tree with an Until node as root.
*
- * Has two PCTL state formulas as sub formulas/trees.
+ * Has two Abstract state formulas as sub formulas/trees.
*
* @par Semantics
* The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
@@ -28,11 +36,11 @@ namespace formula {
* The subtrees are seen as part of the object and deleted with the object
* (this behavior can be prevented by setting them to NULL before deletion)
*
- * @see PctlPathFormula
- * @see PctlFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
*/
template <class T>
-class Until : public PctlPathFormula<T> {
+class Until : public AbstractPathFormula<T> {
public:
/*!
@@ -49,7 +57,7 @@ public:
* @param left The left formula subtree
* @param right The left formula subtree
*/
- Until(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
+ Until(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
this->left = left;
this->right = right;
}
@@ -74,7 +82,7 @@ public:
*
* @param newLeft the new left child.
*/
- void setLeft(PctlStateFormula<T>* newLeft) {
+ void setLeft(AbstractStateFormula<T>* newLeft) {
left = newLeft;
}
@@ -83,21 +91,21 @@ public:
*
* @param newRight the new right child.
*/
- void setRight(PctlStateFormula<T>* newRight) {
+ void setRight(AbstractStateFormula<T>* newRight) {
right = newRight;
}
/*!
* @returns a pointer to the left child node
*/
- const PctlStateFormula<T>& getLeft() const {
+ const AbstractStateFormula<T>& getLeft() const {
return *left;
}
/*!
* @returns a pointer to the right child node
*/
- const PctlStateFormula<T>& getRight() const {
+ const AbstractStateFormula<T>& getRight() const {
return *right;
}
@@ -120,7 +128,7 @@ public:
*
* @returns a new BoundedUntil-object that is identical the called object.
*/
- virtual PctlPathFormula<T>* clone() const {
+ virtual AbstractPathFormula<T>* clone() const {
Until<T>* result = new Until();
if (left != NULL) {
result->setLeft(left->clone());
@@ -140,13 +148,13 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+ virtual std::vector<T> *check(const IUntilModelChecker<T>& modelChecker) const {
return modelChecker.checkUntil(*this);
}
private:
- PctlStateFormula<T>* left;
- PctlStateFormula<T>* right;
+ AbstractStateFormula<T>* left;
+ AbstractStateFormula<T>* right;
};
} //namespace formula
diff --git a/src/modelChecker/AbstractModelChecker.h b/src/modelChecker/AbstractModelChecker.h
new file mode 100644
index 000000000..6bac47a04
--- /dev/null
+++ b/src/modelChecker/AbstractModelChecker.h
@@ -0,0 +1,43 @@
+/*
+ * DtmcPrctlModelChecker.h
+ *
+ * Created on: 22.10.2012
+ * Author: Thomas Heinemann
+ */
+
+#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
+#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
+
+namespace storm { namespace modelChecker {
+template <class Type> class AbstractModelChecker;
+}}
+
+//#include "src/formula/Formulas.h"
+#include "src/formula/Or.h"
+#include "src/formula/Ap.h"
+#include "src/storage/BitVector.h"
+
+namespace storm {
+namespace modelChecker {
+
+/*!
+ * @brief
+ * Interface for model checker classes.
+ *
+ * This class provides basic functions that are the same for all subclasses, but mainly only declares
+ * abstract methods that are to be implemented in concrete instances.
+ *
+ * @attention This class is abstract.
+ */
+template<class Type>
+class AbstractModelChecker :
+ public virtual storm::formula::IOrModelChecker<Type>,
+ public virtual storm::formula::IApModelChecker<Type>
+ {
+};
+
+} //namespace modelChecker
+
+} //namespace storm
+
+#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */
diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h
index f443a2ead..16fdc913f 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.h
+++ b/src/modelChecker/DtmcPrctlModelChecker.h
@@ -23,15 +23,13 @@ class DtmcPrctlModelChecker;
}
-#include "src/formula/PctlPathFormula.h"
-#include "src/formula/PctlStateFormula.h"
-
#include "src/formula/Formulas.h"
#include "src/models/Dtmc.h"
#include "src/storage/BitVector.h"
#include "src/exceptions/InvalidPropertyException.h"
#include "src/utility/Vector.h"
+#include "src/modelChecker/AbstractModelChecker.h"
#include <vector>
#include "log4cplus/logger.h"
@@ -53,7 +51,11 @@ namespace modelChecker {
* @attention This class is abstract.
*/
template<class Type>
-class DtmcPrctlModelChecker {
+class DtmcPrctlModelChecker :
+ public virtual AbstractModelChecker<Type>,
+ public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
+ public virtual storm::formula::IEventuallyModelChecker<Type>
+ {
public:
/*!
* Constructor
@@ -100,7 +102,7 @@ public:
* states.
* @param stateFormula The formula to be checked.
*/
- void check(const storm::formula::PctlStateFormula<Type>& stateFormula) const {
+ void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const {
std::cout << std::endl;
LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
@@ -160,7 +162,7 @@ public:
* @param formula The state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
- storm::storage::BitVector* checkStateFormula(const storm::formula::PctlStateFormula<Type>& formula) const {
+ storm::storage::BitVector* checkStateFormula(const storm::formula::AbstractStateFormula<Type>& formula) const {
return formula.check(*this);
}
@@ -216,7 +218,7 @@ public:
* @param formula The Or state formula to check
* @returns The set of states satisfying the formula, represented by a bit vector
*/
- storm::storage::BitVector* checkOr(const storm::formula::Or<Type>& formula) const {
+ virtual storm::storage::BitVector* checkOr(const storm::formula::Or<Type>& formula) const {
storm::storage::BitVector* result = checkStateFormula(formula.getLeft());
storm::storage::BitVector* right = checkStateFormula(formula.getRight());
(*result) |= (*right);
@@ -269,7 +271,7 @@ public:
* @param formula The path formula to check
* @returns for each state the probability that the path formula holds.
*/
- std::vector<Type>* checkPathFormula(const storm::formula::PctlPathFormula<Type>& formula) const {
+ std::vector<Type>* checkPathFormula(const storm::formula::AbstractPathFormula<Type>& formula) const {
return formula.check(*this);
}
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 9c0850ca5..f7288f3fe 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -58,7 +58,7 @@ namespace
/*!
* @brief Resulting formula.
*/
- storm::formula::PctlFormula<double>* result;
+ //storm::formula::PctlFormula<double>* result;
struct dump
{
@@ -141,7 +141,7 @@ storm::parser::PrctlParser::PrctlParser(const char* filename)
std::cout << "File was parsed" << std::endl;
std::string rest(data, file.dataend);
std::cout << "Rest: " << rest << std::endl;
- this->formula = p.result;
+ //this->formula = p.result;
}
- else this->formula = NULL;
+ //else this->formula = NULL;
}
diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h
index 79c2e81c7..70a7da0db 100644
--- a/src/parser/PrctlParser.h
+++ b/src/parser/PrctlParser.h
@@ -1,7 +1,7 @@
#ifndef STORM_PARSER_PRCTLPARSER_H_
#define STORM_PARSER_PRCTLPARSER_H_
-#include "src/formula/PctlFormula.h"
+// #include "src/formula/PctlFormula.h"
#include "src/parser/Parser.h"
namespace storm {
@@ -18,13 +18,14 @@ class PrctlParser : Parser
/*!
* @brief return formula object parsed from file.
*/
- storm::formula::PctlFormula<double>* getFormula()
+/* storm::formula::PctlFormula<double>* getFormula()
{
return this->formula;
}
private:
storm::formula::PctlFormula<double>* formula;
+*/
};
} // namespace parser
From 8a719bed224b295988c69892696ff01e93b0e59f Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sat, 26 Jan 2013 00:54:31 +0100
Subject: [PATCH 08/30] some more form on formulas. seems to work for formula
objects changed yet...
---
src/formula/AbstractStateFormula.h | 5 +++--
src/formula/And.h | 7 ++++---
src/formula/BoundOperator.h | 11 ++++++-----
src/formula/BoundedEventually.h | 5 +++--
src/formula/BoundedUntil.h | 5 +++--
src/formula/Globally.h | 4 ++--
src/formula/Not.h | 5 +++--
src/formula/ReachabilityReward.h | 9 +++++----
src/modelChecker/DtmcPrctlModelChecker.h | 1 +
9 files changed, 30 insertions(+), 22 deletions(-)
diff --git a/src/formula/AbstractStateFormula.h b/src/formula/AbstractStateFormula.h
index f17f7eda0..e356d4325 100644
--- a/src/formula/AbstractStateFormula.h
+++ b/src/formula/AbstractStateFormula.h
@@ -59,10 +59,11 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
+ virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const = 0; // {
+/* std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
return nullptr;
}
+*/
};
} //namespace formula
diff --git a/src/formula/And.h b/src/formula/And.h
index 33e69ee1d..ea017fe81 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -8,7 +8,8 @@
#ifndef STORM_FORMULA_AND_H_
#define STORM_FORMULA_AND_H_
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
#include <string>
namespace storm {
@@ -148,8 +149,8 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const IAndModelChecker<T>& modelChecker) const {
- return modelChecker.checkAnd(*this);
+ virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) {
+ return this->template cast<IAndModelChecker>(modelChecker)->checkAnd(*this);
}
private:
diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h
index 2333897e7..9a3472034 100644
--- a/src/formula/BoundOperator.h
+++ b/src/formula/BoundOperator.h
@@ -8,9 +8,10 @@
#ifndef STORM_FORMULA_BOUNDOPERATOR_H_
#define STORM_FORMULA_BOUNDOPERATOR_H_
-#include "AbstractStateFormula.h"
-#include "AbstractPathFormula.h"
-#include "utility/ConstTemplates.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/utility/ConstTemplates.h"
namespace storm {
@@ -153,8 +154,8 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const IBoundUntilModelChecker<T>& modelChecker) const {
- return modelChecker.checkBoundOperator(*this);
+ virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return this->template cast<IBoundUntilModelChecker>(modelChecker)->checkBoundOperator(*this);
}
private:
diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h
index bb7585ff9..6ccc89714 100644
--- a/src/formula/BoundedEventually.h
+++ b/src/formula/BoundedEventually.h
@@ -12,6 +12,7 @@
#include "AbstractStateFormula.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
+#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
@@ -143,8 +144,8 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const IBoundedEventuallyModelChecker<T>& modelChecker) const {
- return modelChecker.checkBoundedEventually(*this);
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return this->template cast<IBoundedEventuallyModelChecker>(modelChecker)->checkBoundedEventually(*this);
}
private:
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 90d5ca10b..763167cb2 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -174,8 +175,8 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const IBoundedUntilModelChecker<T>& modelChecker) const {
- return modelChecker.checkBoundedUntil(*this);
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return this->template cast<IBoundedUntilModelChecker>(modelChecker)->checkBoundedUntil(*this);
}
private:
diff --git a/src/formula/Globally.h b/src/formula/Globally.h
index 115d96673..116509ed6 100644
--- a/src/formula/Globally.h
+++ b/src/formula/Globally.h
@@ -118,8 +118,8 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const IGloballyModelChecker<T>& modelChecker) const {
- return modelChecker.checkGlobally(*this);
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return this->template cast<IGloballyModelChecker>(modelChecker)->checkGlobally(*this);
}
private:
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 9e211084d..d79e31a34 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -9,6 +9,7 @@
#define STORM_FORMULA_NOT_H_
#include "AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
@@ -113,8 +114,8 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const INotModelChecker<T>& modelChecker) const {
- return modelChecker.checkNot(*this);
+ virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return this->template cast<INotModelChecker>(modelChecker)->checkNot(*this);
}
private:
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index 6fdfb4733..37b7ee7e3 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -8,8 +8,9 @@
#ifndef STORM_FORMULA_REACHABILITYREWARD_H_
#define STORM_FORMULA_REACHABILITYREWARD_H_
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
@@ -115,8 +116,8 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const IReachabilityRewardModelChecker<T>& modelChecker) const {
- return modelChecker.checkReachabilityReward(*this);
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return this->template cast<IReachabilityRewardModelChecker>(modelChecker)->checkReachabilityReward(*this);
}
private:
diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h
index 16fdc913f..0c048dc02 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.h
+++ b/src/modelChecker/DtmcPrctlModelChecker.h
@@ -54,6 +54,7 @@ template<class Type>
class DtmcPrctlModelChecker :
public virtual AbstractModelChecker<Type>,
public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
+ public virtual storm::formula::IReachabilityRewardModelChecker<Type>,
public virtual storm::formula::IEventuallyModelChecker<Type>
{
public:
From 7331544377ed0cd39d48cda479cab5b4b863e324 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 26 Jan 2013 11:23:20 +0100
Subject: [PATCH 09/30] Added output functionality to bit vector and moved
test-checking lines in storm.cpp to the right place.
---
src/storage/BitVector.h | 22 ++++++++++++++++++----
src/storm.cpp | 8 ++++----
2 files changed, 22 insertions(+), 8 deletions(-)
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index 66baf546e..df3f86600 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -387,11 +387,11 @@ public:
* Returns the number of bits that are set (to one) in this bit vector.
* @return The number of bits that are set (to one) in this bit vector.
*/
- uint_fast64_t getNumberOfSetBits() {
+ uint_fast64_t getNumberOfSetBits() const {
return getNumberOfSetBitsBeforeIndex(bucketCount << 6);
}
- uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) {
+ uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) const {
uint_fast64_t result = 0;
// First, count all full buckets.
uint_fast64_t bucket = index >> 6;
@@ -437,7 +437,7 @@ public:
/*!
* Retrieves the number of bits this bit vector can store.
*/
- uint_fast64_t getSize() {
+ uint_fast64_t getSize() const {
return bitCount;
}
@@ -445,7 +445,7 @@ public:
* Returns the size of the bit vector in memory measured in bytes.
* @return The size of the bit vector in memory measured in bytes.
*/
- uint_fast64_t getSizeInMemory() {
+ uint_fast64_t getSizeInMemory() const {
return sizeof(*this) + sizeof(uint_fast64_t) * bucketCount;
}
@@ -463,6 +463,20 @@ public:
return endIterator;
}
+ /*!
+ * Returns a string representation of the bit vector.
+ */
+ std::string toString() const {
+ std::stringstream result;
+ result << "bit vector(" << this->getNumberOfSetBits() << ") [";
+ for (auto index : *this) {
+ result << index << " ";
+ }
+ result << "]";
+
+ return result.str();
+ }
+
private:
/*!
diff --git a/src/storm.cpp b/src/storm.cpp
index 250163f70..9d2fff6d7 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -216,12 +216,12 @@ void testChecking() {
if (parser.getType() == storm::models::DTMC) {
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
dtmc->printModelInformationToStream(std::cout);
+
+ // testCheckingDie(*dtmc);
+ // testCheckingCrowds(*dtmc);
+ // testCheckingSynchronousLeader(*dtmc, 4);
}
else std::cout << "Input is not DTMC" << std::endl;
-
- // testCheckingDie(*dtmc);
- // testCheckingCrowds(*dtmc);
- // testCheckingSynchronousLeader(*dtmc, 4);
}
/*!
From 9d65bdeef307d7732318aec85b84f099a866eff3 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sun, 27 Jan 2013 20:58:22 +0100
Subject: [PATCH 10/30] next iteration on formulas...
removed AbstractFormula::cast() in favor of AbstractModelChecker::as()
changed all formulas to use this new one
actually implement ::check(AbstractModelChecker) for all formulas
---
src/formula/AbstractFormula.h | 12 ------------
src/formula/AbstractPathFormula.h | 5 +----
src/formula/AbstractStateFormula.h | 4 ----
src/formula/And.h | 2 +-
src/formula/Ap.h | 2 +-
src/formula/BoundOperator.h | 2 +-
src/formula/BoundedEventually.h | 2 +-
src/formula/BoundedUntil.h | 2 +-
src/formula/CumulativeReward.h | 4 ++--
src/formula/Eventually.h | 2 +-
src/formula/Globally.h | 2 +-
src/formula/InstantaneousReward.h | 4 ++--
src/formula/Next.h | 4 ++--
src/formula/NoBoundOperator.h | 4 ++--
src/formula/Not.h | 2 +-
src/formula/Or.h | 4 ++--
src/formula/ReachabilityReward.h | 2 +-
src/formula/Until.h | 4 ++--
src/modelChecker/AbstractModelChecker.h | 14 ++++++++++++++
19 files changed, 36 insertions(+), 41 deletions(-)
diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
index 8bd8b8782..ee99f88f2 100644
--- a/src/formula/AbstractFormula.h
+++ b/src/formula/AbstractFormula.h
@@ -44,18 +44,6 @@ public:
* @returns a string representation of the formula
*/
virtual std::string toString() const = 0;
-
- template <template <class Type> class MC>
- const MC<T>* cast(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- try {
- const MC<T>& mc = dynamic_cast<const MC<T>&>(modelChecker);
- return &mc;
- } catch (std::bad_cast& bc) {
- std::cerr << "Bad cast: tried to cast " << typeid(modelChecker).name() << " to " << typeid(MC<T>).name() << std::endl;
-
- }
- return nullptr;
- }
};
} //namespace formula
diff --git a/src/formula/AbstractPathFormula.h b/src/formula/AbstractPathFormula.h
index cba3425fa..a12642002 100644
--- a/src/formula/AbstractPathFormula.h
+++ b/src/formula/AbstractPathFormula.h
@@ -62,10 +62,7 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
- return nullptr;
- }
+ virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const = 0;
};
} //namespace formula
diff --git a/src/formula/AbstractStateFormula.h b/src/formula/AbstractStateFormula.h
index e356d4325..4ce735c75 100644
--- a/src/formula/AbstractStateFormula.h
+++ b/src/formula/AbstractStateFormula.h
@@ -60,10 +60,6 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const = 0; // {
-/* std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
- return nullptr;
- }
-*/
};
} //namespace formula
diff --git a/src/formula/And.h b/src/formula/And.h
index ea017fe81..601872f79 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -150,7 +150,7 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) {
- return this->template cast<IAndModelChecker>(modelChecker)->checkAnd(*this);
+ return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
}
private:
diff --git a/src/formula/Ap.h b/src/formula/Ap.h
index 8eb4dbe5b..ceca11193 100644
--- a/src/formula/Ap.h
+++ b/src/formula/Ap.h
@@ -87,7 +87,7 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- return this->template cast<IApModelChecker>(modelChecker)->checkAp(*this);
+ return modelChecker.template as<IApModelChecker>()->checkAp(*this);
}
private:
diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h
index 9a3472034..67d92df8a 100644
--- a/src/formula/BoundOperator.h
+++ b/src/formula/BoundOperator.h
@@ -155,7 +155,7 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- return this->template cast<IBoundUntilModelChecker>(modelChecker)->checkBoundOperator(*this);
+ return modelChecker.template as<IBoundUntilModelChecker>()->checkBoundOperator(*this);
}
private:
diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h
index 6ccc89714..5c92ea3d8 100644
--- a/src/formula/BoundedEventually.h
+++ b/src/formula/BoundedEventually.h
@@ -145,7 +145,7 @@ public:
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- return this->template cast<IBoundedEventuallyModelChecker>(modelChecker)->checkBoundedEventually(*this);
+ return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
}
private:
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 763167cb2..89ae6e35d 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -176,7 +176,7 @@ public:
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- return this->template cast<IBoundedUntilModelChecker>(modelChecker)->checkBoundedUntil(*this);
+ return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
}
private:
diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h
index 2587390ea..bdc1e70b1 100644
--- a/src/formula/CumulativeReward.h
+++ b/src/formula/CumulativeReward.h
@@ -108,8 +108,8 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const ICumulativeRewardModelChecker<T>& modelChecker) const {
- return modelChecker.checkCumulativeReward(*this);
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this);
}
private:
diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h
index 32e6d126a..ac9d38981 100644
--- a/src/formula/Eventually.h
+++ b/src/formula/Eventually.h
@@ -120,7 +120,7 @@ public:
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- return this->template cast<IEventuallyModelChecker>(modelChecker)->checkEventually(*this);
+ return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
}
private:
diff --git a/src/formula/Globally.h b/src/formula/Globally.h
index 116509ed6..46d464fad 100644
--- a/src/formula/Globally.h
+++ b/src/formula/Globally.h
@@ -119,7 +119,7 @@ public:
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- return this->template cast<IGloballyModelChecker>(modelChecker)->checkGlobally(*this);
+ return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
}
private:
diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h
index 319e38f49..da6d3269b 100644
--- a/src/formula/InstantaneousReward.h
+++ b/src/formula/InstantaneousReward.h
@@ -108,8 +108,8 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const IInstantaneousRewardModelChecker<T>& modelChecker) const {
- return modelChecker.checkInstantaneousReward(*this);
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this);
}
private:
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 501277bba..763d6068c 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -120,8 +120,8 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const INextModelChecker<T>& modelChecker) const {
- return modelChecker.checkNext(*this);
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return modelChecker.template as<INextModelChecker>()->checkNext(*this);
}
private:
diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h
index eeb8d2c54..c2cab764d 100644
--- a/src/formula/NoBoundOperator.h
+++ b/src/formula/NoBoundOperator.h
@@ -108,8 +108,8 @@ public:
*
* @returns A vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual std::vector<T>* check(const INoBoundOperatorModelChecker<T>& modelChecker) const {
- return modelChecker.checkNoBoundOperator(*this);
+ virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return modelChecker.template as<INoBoundOperatorModelChecker>()->checkNoBoundOperator(*this);
}
/*!
diff --git a/src/formula/Not.h b/src/formula/Not.h
index d79e31a34..f3f5186ec 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -115,7 +115,7 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- return this->template cast<INotModelChecker>(modelChecker)->checkNot(*this);
+ return modelChecker.template as<INotModelChecker>()->checkNot(*this);
}
private:
diff --git a/src/formula/Or.h b/src/formula/Or.h
index 79e30cdab..e5143ebeb 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -147,8 +147,8 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const IOrModelChecker<T>& modelChecker) const {
- return modelChecker.checkOr(*this);
+ virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
}
private:
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index 37b7ee7e3..4c214ae12 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -117,7 +117,7 @@ public:
* @returns A vector indicating the probability that the formula holds for each state.
*/
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- return this->template cast<IReachabilityRewardModelChecker>(modelChecker)->checkReachabilityReward(*this);
+ return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this);
}
private:
diff --git a/src/formula/Until.h b/src/formula/Until.h
index 94f917a60..764175f1c 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -148,8 +148,8 @@ public:
*
* @returns A vector indicating the probability that the formula holds for each state.
*/
- virtual std::vector<T> *check(const IUntilModelChecker<T>& modelChecker) const {
- return modelChecker.checkUntil(*this);
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
}
private:
diff --git a/src/modelChecker/AbstractModelChecker.h b/src/modelChecker/AbstractModelChecker.h
index 6bac47a04..110d355dd 100644
--- a/src/modelChecker/AbstractModelChecker.h
+++ b/src/modelChecker/AbstractModelChecker.h
@@ -17,6 +17,8 @@ template <class Type> class AbstractModelChecker;
#include "src/formula/Ap.h"
#include "src/storage/BitVector.h"
+#include <iostream>
+
namespace storm {
namespace modelChecker {
@@ -34,6 +36,18 @@ class AbstractModelChecker :
public virtual storm::formula::IOrModelChecker<Type>,
public virtual storm::formula::IApModelChecker<Type>
{
+
+public:
+ template <template <class T> class Target>
+ const Target<Type>* as() const {
+ try {
+ const Target<Type>* target = dynamic_cast<const Target<Type>*>(this);
+ return target;
+ } catch (std::bad_cast& bc) {
+ std::cerr << "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << std::endl;
+ }
+ return nullptr;
+ }
};
} //namespace modelChecker
From c47b559986608a97129cc5eeeee8a3b522439b04 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 29 Jan 2013 09:13:06 +0100
Subject: [PATCH 11/30] Fixed minor bugs for Jacobi decomposition.
---
src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 4 +++-
src/storage/JacobiDecomposition.h | 2 +-
2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
index c2c5663d0..0c54d63cf 100644
--- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
@@ -460,10 +460,12 @@ private:
* x.
*/
void solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b) const {
+ // Get the settings object to customize linear solving.
+ storm::settings::Settings* s = storm::settings::instance();
double precision = s->get<double>("precision");
if (precision <= 0) {
- LOG4CPLUS_ERROR(logger, "Precision is not greater Zero");
+ LOG4CPLUS_ERROR(logger, "Selected precision for linear equation solving must be strictly greater than zero for Jacobi method.");
}
// Get a Jacobi Decomposition of the Input Matrix A
diff --git a/src/storage/JacobiDecomposition.h b/src/storage/JacobiDecomposition.h
index d02d1ab38..9aec6f061 100644
--- a/src/storage/JacobiDecomposition.h
+++ b/src/storage/JacobiDecomposition.h
@@ -79,7 +79,7 @@ private:
*/
//JacobiDecomposition(const JacobiDecomposition<T>& that) = delete; // not possible in VS2012
JacobiDecomposition(const JacobiDecomposition<T>& that) {
- throw new storm::exceptions::InvalidAccessException() << "The copy constructor of JacobiDecomposition is explicitly disabled.";
+ throw storm::exceptions::InvalidAccessException() << "The copy constructor of JacobiDecomposition is explicitly disabled.";
}
/*!
From 8449c5ee114579fb69298b84852cd42890c9c143 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Tue, 29 Jan 2013 18:44:59 +0100
Subject: [PATCH 12/30] implemented formula checker
---
src/formula/AbstractFormula.h | 3 +++
src/formula/AbstractFormulaChecker.h | 18 ++++++++++++++
src/formula/Ap.h | 7 +++++-
src/formula/BoundedUntil.h | 9 +++++--
src/formula/Eventually.h | 4 ++++
src/formula/NoBoundOperator.h | 5 ++++
src/formula/Not.h | 5 ++++
src/formula/PrctlFormulaChecker.h | 35 ++++++++++++++++++++++++++++
src/formula/ReachabilityReward.h | 5 ++++
src/formula/Until.h | 5 ++++
10 files changed, 93 insertions(+), 3 deletions(-)
create mode 100644 src/formula/AbstractFormulaChecker.h
create mode 100644 src/formula/PrctlFormulaChecker.h
diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
index ee99f88f2..b7d51e70b 100644
--- a/src/formula/AbstractFormula.h
+++ b/src/formula/AbstractFormula.h
@@ -15,6 +15,7 @@ template <class T> class AbstractFormula;
}}
#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
namespace formula {
@@ -44,6 +45,8 @@ public:
* @returns a string representation of the formula
*/
virtual std::string toString() const = 0;
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const = 0;
};
} //namespace formula
diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h
new file mode 100644
index 000000000..9a80b3051
--- /dev/null
+++ b/src/formula/AbstractFormulaChecker.h
@@ -0,0 +1,18 @@
+#ifndef STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
+#define STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
+
+#include "src/formula/AbstractFormula.h"
+
+namespace storm {
+namespace formula {
+
+template <class T>
+class AbstractFormulaChecker {
+ public:
+ virtual bool conforms(const AbstractFormula<T>* formula) const = 0;
+};
+
+}
+}
+
+#endif
\ No newline at end of file
diff --git a/src/formula/Ap.h b/src/formula/Ap.h
index ceca11193..32e6c962e 100644
--- a/src/formula/Ap.h
+++ b/src/formula/Ap.h
@@ -8,7 +8,8 @@
#ifndef STORM_FORMULA_AP_H_
#define STORM_FORMULA_AP_H_
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
@@ -89,6 +90,10 @@ public:
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IApModelChecker>()->checkAp(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return true;
+ }
private:
std::string ap;
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 89ae6e35d..3110ce8be 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -8,11 +8,12 @@
#ifndef STORM_FORMULA_BOUNDEDUNTIL_H_
#define STORM_FORMULA_BOUNDEDUNTIL_H_
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractStateFormula.h"
#include "src/modelChecker/AbstractModelChecker.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
+#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@@ -178,6 +179,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->left) && checker.conforms(this->right);
+ }
private:
AbstractStateFormula<T>* left;
diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h
index ac9d38981..8978510ea 100644
--- a/src/formula/Eventually.h
+++ b/src/formula/Eventually.h
@@ -122,6 +122,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->child);
+ }
private:
AbstractStateFormula<T>* child;
diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h
index c2cab764d..c7a14d155 100644
--- a/src/formula/NoBoundOperator.h
+++ b/src/formula/NoBoundOperator.h
@@ -10,6 +10,7 @@
#include "AbstractFormula.h"
#include "AbstractPathFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@@ -116,6 +117,10 @@ public:
* @returns a string representation of the formula
*/
virtual std::string toString() const = 0;
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->pathFormula);
+ }
private:
AbstractPathFormula<T>* pathFormula;
diff --git a/src/formula/Not.h b/src/formula/Not.h
index f3f5186ec..56eaf6c6a 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -9,6 +9,7 @@
#define STORM_FORMULA_NOT_H_
#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
@@ -117,6 +118,10 @@ public:
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<INotModelChecker>()->checkNot(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->child);
+ }
private:
AbstractStateFormula<T>* child;
diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h
new file mode 100644
index 000000000..2a8d882e7
--- /dev/null
+++ b/src/formula/PrctlFormulaChecker.h
@@ -0,0 +1,35 @@
+#ifndef STORM_FORMULA_PRCTLFORMULACHECKER_H_
+#define STORM_FORMULA_PRCTLFORMULACHECKER_H_
+
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/formula/Formulas.h"
+
+#include <iostream>
+
+namespace storm {
+namespace formula {
+
+template <class T>
+class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
+ public:
+ virtual bool conforms(const AbstractFormula<T>* formula) const {
+ if (
+ dynamic_cast<const And<T>*>(formula) ||
+ dynamic_cast<const Ap<T>*>(formula) ||
+ dynamic_cast<const Eventually<T>*>(formula) ||
+ dynamic_cast<const Not<T>*>(formula) ||
+ dynamic_cast<const Or<T>*>(formula) ||
+ dynamic_cast<const ProbabilisticNoBoundOperator<T>*>(formula)
+ ) {
+ return formula->conforms(*this);
+ }
+ return false;
+ }
+
+ private:
+};
+
+}
+}
+
+#endif
\ No newline at end of file
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index 4c214ae12..cef56ab6d 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -10,6 +10,7 @@
#include "src/formula/AbstractPathFormula.h"
#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
@@ -119,6 +120,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->child);
+ }
private:
AbstractStateFormula<T>* child;
diff --git a/src/formula/Until.h b/src/formula/Until.h
index 764175f1c..cfc186f56 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@@ -151,6 +152,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->left) && checker.conforms(this->right);
+ }
private:
AbstractStateFormula<T>* left;
From 80779523317a0e2ccd66a2d322f9a5c15d3786d4 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Tue, 29 Jan 2013 20:14:38 +0100
Subject: [PATCH 13/30] adding needed methods for more formula classes
---
src/formula/And.h | 7 ++++++-
src/formula/BoundOperator.h | 5 +++++
src/formula/BoundedEventually.h | 5 +++++
src/formula/CumulativeReward.h | 5 +++++
src/formula/Globally.h | 5 +++++
src/formula/InstantaneousReward.h | 5 +++++
src/formula/Next.h | 5 +++++
src/formula/Or.h | 7 ++++++-
src/formula/ProbabilisticBoundOperator.h | 2 ++
src/formula/RewardBoundOperator.h | 1 +
10 files changed, 45 insertions(+), 2 deletions(-)
diff --git a/src/formula/And.h b/src/formula/And.h
index 601872f79..abc407683 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -9,6 +9,7 @@
#define STORM_FORMULA_AND_H_
#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelChecker/AbstractModelChecker.h"
#include <string>
@@ -149,9 +150,13 @@ public:
*
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
- virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) {
+ virtual storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->left) && checker.conforms(this->right);
+ }
private:
AbstractStateFormula<T>* left;
diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h
index 67d92df8a..c86455f60 100644
--- a/src/formula/BoundOperator.h
+++ b/src/formula/BoundOperator.h
@@ -10,6 +10,7 @@
#include "src/formula/AbstractStateFormula.h"
#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelChecker/AbstractModelChecker.h"
#include "src/utility/ConstTemplates.h"
@@ -157,6 +158,10 @@ public:
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IBoundUntilModelChecker>()->checkBoundOperator(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->pathFormula);
+ }
private:
ComparisonType comparisonOperator;
diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h
index 5c92ea3d8..995d4c899 100644
--- a/src/formula/BoundedEventually.h
+++ b/src/formula/BoundedEventually.h
@@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
#include "src/modelChecker/AbstractModelChecker.h"
@@ -147,6 +148,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->child);
+ }
private:
AbstractStateFormula<T>* child;
diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h
index bdc1e70b1..ac8c6eab1 100644
--- a/src/formula/CumulativeReward.h
+++ b/src/formula/CumulativeReward.h
@@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -111,6 +112,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return true;
+ }
private:
uint_fast64_t bound;
diff --git a/src/formula/Globally.h b/src/formula/Globally.h
index 46d464fad..39dad85ff 100644
--- a/src/formula/Globally.h
+++ b/src/formula/Globally.h
@@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@@ -121,6 +122,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->child);
+ }
private:
AbstractStateFormula<T>* child;
diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h
index da6d3269b..3ab36c584 100644
--- a/src/formula/InstantaneousReward.h
+++ b/src/formula/InstantaneousReward.h
@@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
#include "boost/integer/integer_mask.hpp"
#include <string>
@@ -111,6 +112,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return true;
+ }
private:
uint_fast64_t bound;
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 763d6068c..8884ac5b6 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -10,6 +10,7 @@
#include "AbstractPathFormula.h"
#include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@@ -123,6 +124,10 @@ public:
virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<INextModelChecker>()->checkNext(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->child);
+ }
private:
AbstractStateFormula<T>* child;
diff --git a/src/formula/Or.h b/src/formula/Or.h
index e5143ebeb..6a071f395 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -8,7 +8,8 @@
#ifndef STORM_FORMULA_OR_H_
#define STORM_FORMULA_OR_H_
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
namespace formula {
@@ -150,6 +151,10 @@ public:
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
}
+
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ return checker.conforms(this->left) && checker.conforms(this->right);
+ }
private:
AbstractStateFormula<T>* left;
diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h
index 37fe7858d..3e6e7fde6 100644
--- a/src/formula/ProbabilisticBoundOperator.h
+++ b/src/formula/ProbabilisticBoundOperator.h
@@ -45,10 +45,12 @@ public:
/*!
* Empty constructor
*/
+//! TODO: this constructor should give a comparisontype as first argument
ProbabilisticBoundOperator() : BoundOperator<T>(storm::utility::constGetZero<T>(), storm::utility::constGetZero<T>(), nullptr) {
// Intentionally left empty
}
+
/*!
* Constructor
*
diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h
index 26f6ae7aa..b2c6065ff 100644
--- a/src/formula/RewardBoundOperator.h
+++ b/src/formula/RewardBoundOperator.h
@@ -44,6 +44,7 @@ public:
/*!
* Empty constructor
*/
+//! TODO: this constructor should give a comparisontype as first argument
RewardBoundOperator() : BoundOperator<T>(storm::utility::constGetZero<T>(), storm::utility::constGetZero<T>(), nullptr) {
// Intentionally left empty
}
From 3716dedc783278b12ed32664148091f4ecbb04a9 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Tue, 29 Jan 2013 20:40:52 +0100
Subject: [PATCH 14/30] first half of documentation.
---
src/formula/AbstractFormula.h | 43 +++++++++++++++++++---------
src/formula/AbstractFormulaChecker.h | 42 +++++++++++++++++++++++++--
src/formula/AbstractPathFormula.h | 8 ++----
src/formula/AbstractStateFormula.h | 6 ++--
src/formula/And.h | 18 ++++++++++++
src/formula/Ap.h | 21 +++++++++++++-
src/formula/BoundOperator.h | 20 ++++++++++---
src/formula/BoundedEventually.h | 18 ++++++++++++
src/formula/BoundedUntil.h | 19 +++++++++++-
src/formula/CumulativeReward.h | 20 +++++++++++++
src/formula/Eventually.h | 18 ++++++++++++
src/formula/Globally.h | 18 ++++++++++++
12 files changed, 221 insertions(+), 30 deletions(-)
diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
index b7d51e70b..42ba7bc02 100644
--- a/src/formula/AbstractFormula.h
+++ b/src/formula/AbstractFormula.h
@@ -5,8 +5,8 @@
* Author: Thomas Heinemann
*/
-#ifndef STORM_FORMULA_AbstractFORMULA_H_
-#define STORM_FORMULA_AbstractFORMULA_H_
+#ifndef STORM_FORMULA_ABSTRACTFORMULA_H_
+#define STORM_FORMULA_ABSTRACTFORMULA_H_
#include <string>
@@ -23,34 +23,51 @@ namespace formula {
//abstract
/*!
- * @brief
- * Abstract base class for Abstract formulas in general.
+ * @brief Abstract base class for Abstract formulas in general.
*
- * @attention This class is abstract.
- * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
+ * @attention This class is abstract.
+ * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
* the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes
* AbstractPathFormula and AbstractStateFormula offer the method clone().
+ *
+ * This is the base class for every formula class in every logic.
*/
template <class T>
class AbstractFormula {
public:
/*!
- * virtual destructor
+ * Virtual destructor.
*/
virtual ~AbstractFormula() { }
/*!
- * @note This function is not implemented in this class.
- * @returns a string representation of the formula
+ * @brief Return string representation of this formula.
+ *
+ * @note very subclass must implement this method.
+ *
+ * @returns a string representation of the formula
*/
virtual std::string toString() const = 0;
+ /*!
+ * @brief Checks if all subtrees are valid in some logic.
+ *
+ * @note Every subclass must implement this method.
+ *
+ * This method is given a checker object that knows which formula
+ * classes are allowed within the logic the checker represents. Every
+ * subclass is supposed to call checker.conforms() for all child
+ * formulas and return true if and only if all those calls returned
+ * true.
+ *
+ * @param checker Checker object.
+ * @return true iff all subtrees are valid.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const = 0;
};
-} //namespace formula
-
-} //namespace storm
+} // namespace formula
+} // namespace storm
-#endif /* STORM_FORMULA_AbstractFORMULA_H_ */
+#endif /* STORM_FORMULA_ABSTRACTFORMULA_H_ */
diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h
index 9a80b3051..f675a319f 100644
--- a/src/formula/AbstractFormulaChecker.h
+++ b/src/formula/AbstractFormulaChecker.h
@@ -6,13 +6,51 @@
namespace storm {
namespace formula {
+/*!
+ * @brief Base class for all formula checkers.
+ *
+ * A formula checker is used to check if a given formula is valid in some
+ * logic. Hence, this pure virtual base class should be subclassed for
+ * every logic we support.
+ *
+ * Every subclass must implement conforms(). It gets a pointer to an
+ * AbstractFormula object and should return if the subtree represented by
+ * this formula is valid in the logic.
+ *
+ * Usually, this will be implemented like this:
+ * @code
+ * if (
+ * dynamic_cast<const And<T>*>(formula) ||
+ * dynamic_cast<const Not<T>*>(formula) ||
+ * dynamic_cast<const Or<T>*>(formula)
+ * ) {
+ * return formula->conforms(*this);
+ * } else return false;
+ * @endcode
+ *
+ * Every formula class implements a conforms() method itself which calls
+ * conforms() on the given checker for every child in the formula tree.
+ *
+ * If the formula structure is not an actual tree, but an directed acyclic
+ * graph, the shared subtrees will be checked twice. If we have directed
+ * cycles, we will have infinite recursions.
+ */
template <class T>
class AbstractFormulaChecker {
public:
+ /*!
+ * @brief Checks if the given formula is valid in some logic.
+ *
+ * Every subclass must implement this method and check, if the
+ * formula object is valid in the logic of the subclass.
+ *
+ * @param formula A pointer to some formula object.
+ * @return true iff the formula is valid.
+ */
virtual bool conforms(const AbstractFormula<T>* formula) const = 0;
};
-}
-}
+} // namespace formula
+} // namespace storm
#endif
\ No newline at end of file
diff --git a/src/formula/AbstractPathFormula.h b/src/formula/AbstractPathFormula.h
index a12642002..4337cbe19 100644
--- a/src/formula/AbstractPathFormula.h
+++ b/src/formula/AbstractPathFormula.h
@@ -5,8 +5,8 @@
* Author: Thomas Heinemann
*/
-#ifndef STORM_FORMULA_AbstractPATHFORMULA_H_
-#define STORM_FORMULA_AbstractPATHFORMULA_H_
+#ifndef STORM_FORMULA_ABSTRACTPATHFORMULA_H_
+#define STORM_FORMULA_ABSTRACTPATHFORMULA_H_
namespace storm { namespace formula {
template <class T> class AbstractPathFormula;
@@ -20,7 +20,6 @@ template <class T> class AbstractPathFormula;
#include <typeinfo>
namespace storm {
-
namespace formula {
/*!
@@ -66,7 +65,6 @@ public:
};
} //namespace formula
-
} //namespace storm
-#endif /* STORM_FORMULA_AbstractPATHFORMULA_H_ */
+#endif /* STORM_FORMULA_ABSTRACTPATHFORMULA_H_ */
diff --git a/src/formula/AbstractStateFormula.h b/src/formula/AbstractStateFormula.h
index 4ce735c75..9309bf610 100644
--- a/src/formula/AbstractStateFormula.h
+++ b/src/formula/AbstractStateFormula.h
@@ -5,8 +5,8 @@
* Author: Thomas Heinemann
*/
-#ifndef STORM_FORMULA_AbstractSTATEFORMULA_H_
-#define STORM_FORMULA_AbstractSTATEFORMULA_H_
+#ifndef STORM_FORMULA_ABSTRACTSTATEFORMULA_H_
+#define STORM_FORMULA_ABSTRACTSTATEFORMULA_H_
namespace storm { namespace formula {
template <class T> class AbstractStateFormula;
@@ -17,7 +17,6 @@ template <class T> class AbstractStateFormula;
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
-
namespace formula {
/*!
@@ -63,7 +62,6 @@ public:
};
} //namespace formula
-
} //namespace storm
diff --git a/src/formula/And.h b/src/formula/And.h
index abc407683..d8078cd15 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -18,9 +18,21 @@ namespace formula {
template <class T> class And;
+/*!
+ * @brief Interface class for model checkers that support And.
+ *
+ * All model checkers that support the formula class And must inherit
+ * this pure virtual class.
+ */
template <class T>
class IAndModelChecker {
public:
+ /*!
+ * @brief Evaluates And formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual storm::storage::BitVector* checkAnd(const And<T>& obj) const = 0;
};
@@ -154,6 +166,12 @@ public:
return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
diff --git a/src/formula/Ap.h b/src/formula/Ap.h
index 32e6c962e..ba5c13287 100644
--- a/src/formula/Ap.h
+++ b/src/formula/Ap.h
@@ -13,14 +13,25 @@
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
-
namespace formula {
template <class T> class Ap;
+/*!
+ * @brief Interface class for model checkers that support Ap.
+ *
+ * All model checkers that support the formula class Ap must inherit
+ * this pure virtual class.
+ */
template <class T>
class IApModelChecker {
public:
+ /*!
+ * @brief Evaluates Ap formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
};
@@ -91,6 +102,14 @@ public:
return modelChecker.template as<IApModelChecker>()->checkAp(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * As atomic propositions have no subformulas, we return true here.
+ *
+ * @param checker Formula checker object.
+ * @return true
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return true;
}
diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h
index c86455f60..cb57f9edc 100644
--- a/src/formula/BoundOperator.h
+++ b/src/formula/BoundOperator.h
@@ -18,12 +18,18 @@ namespace storm {
namespace formula {
-template <class T> class BoundUntil;
+template <class T> class BoundOperator;
+/*!
+ * @brief Interface class for model checkers that support BoundOperator.
+ *
+ * All model checkers that support the formula class BoundOperator must inherit
+ * this pure virtual class.
+ */
template <class T>
-class IBoundUntilModelChecker {
+class IBoundOperatorModelChecker {
public:
- virtual storm::storage::BitVector* checkBoundUntil(const BoundUntil<T>& obj) const = 0;
+ virtual storm::storage::BitVector* checkBoundOperator(const BoundOperator<T>& obj) const = 0;
};
/*!
@@ -156,9 +162,15 @@ public:
* @returns A bit vector indicating all states that satisfy the formula represented by the called object.
*/
virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
- return modelChecker.template as<IBoundUntilModelChecker>()->checkBoundOperator(*this);
+ return modelChecker.template as<IBoundOperatorModelChecker>()->checkBoundOperator(*this);
}
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->pathFormula);
}
diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h
index 995d4c899..4be075840 100644
--- a/src/formula/BoundedEventually.h
+++ b/src/formula/BoundedEventually.h
@@ -21,9 +21,21 @@ namespace formula {
template <class T> class BoundedEventually;
+/*!
+ * @brief Interface class for model checkers that support BoundedEventually.
+ *
+ * All model checkers that support the formula class BoundedEventually must inherit
+ * this pure virtual class.
+ */
template <class T>
class IBoundedEventuallyModelChecker {
public:
+ /*!
+ * @brief Evaluates BoundedEventually formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj) const = 0;
};
@@ -149,6 +161,12 @@ public:
return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
}
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 3110ce8be..e00acac74 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -16,14 +16,25 @@
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
-
namespace formula {
template <class T> class BoundedUntil;
+/*!
+ * @brief Interface class for model checkers that support BoundedUntil.
+ *
+ * All model checkers that support the formula class BoundedUntil must inherit
+ * this pure virtual class.
+ */
template <class T>
class IBoundedUntilModelChecker {
public:
+ /*!
+ * @brief Evaluates BoundedUntil formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj) const = 0;
};
@@ -180,6 +191,12 @@ public:
return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h
index ac8c6eab1..e89bcfbaf 100644
--- a/src/formula/CumulativeReward.h
+++ b/src/formula/CumulativeReward.h
@@ -20,9 +20,21 @@ namespace formula {
template <class T> class CumulativeReward;
+/*!
+ * @brief Interface class for model checkers that support CumulativeReward.
+ *
+ * All model checkers that support the formula class CumulativeReward must inherit
+ * this pure virtual class.
+ */
template <class T>
class ICumulativeRewardModelChecker {
public:
+ /*!
+ * @brief Evaluates CumulativeReward formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkCumulativeReward(const CumulativeReward<T>& obj) const = 0;
};
@@ -113,6 +125,14 @@ public:
return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * As CumulativeReward objects have no subformulas, we return true here.
+ *
+ * @param checker Formula checker object.
+ * @return true
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return true;
}
diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h
index 8978510ea..4b2ca1ba3 100644
--- a/src/formula/Eventually.h
+++ b/src/formula/Eventually.h
@@ -18,9 +18,21 @@ namespace formula {
template <class T> class Eventually;
+/*!
+ * @brief Interface class for model checkers that support Eventually.
+ *
+ * All model checkers that support the formula class Eventually must inherit
+ * this pure virtual class.
+ */
template <class T>
class IEventuallyModelChecker {
public:
+ /*!
+ * @brief Evaluates Eventually formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkEventually(const Eventually<T>& obj) const = 0;
};
@@ -123,6 +135,12 @@ public:
return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
}
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
diff --git a/src/formula/Globally.h b/src/formula/Globally.h
index 39dad85ff..e42837091 100644
--- a/src/formula/Globally.h
+++ b/src/formula/Globally.h
@@ -18,9 +18,21 @@ namespace formula {
template <class T> class Globally;
+/*!
+ * @brief Interface class for model checkers that support Globally.
+ *
+ * All model checkers that support the formula class Globally must inherit
+ * this pure virtual class.
+ */
template <class T>
class IGloballyModelChecker {
public:
+ /*!
+ * @brief Evaluates Globally formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkGlobally(const Globally<T>& obj) const = 0;
};
@@ -123,6 +135,12 @@ public:
return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
}
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
From 9a73a2740af424f5e0f7a2811ca99a1bd4f7cb6a Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Tue, 29 Jan 2013 20:54:50 +0100
Subject: [PATCH 15/30] second hald of documentation. I guess that's it :-)
---
src/formula/AbstractFormulaChecker.h | 4 ++--
src/formula/InstantaneousReward.h | 20 ++++++++++++++++++++
src/formula/Next.h | 18 ++++++++++++++++++
src/formula/NoBoundOperator.h | 18 ++++++++++++++++++
src/formula/Not.h | 18 ++++++++++++++++++
src/formula/Or.h | 18 ++++++++++++++++++
src/formula/PrctlFormulaChecker.h | 19 +++++++++++++++----
src/formula/ProbabilisticBoundOperator.h | 2 --
src/formula/ProbabilisticNoBoundOperator.h | 2 --
src/formula/ReachabilityReward.h | 20 ++++++++++++++++++--
src/formula/RewardBoundOperator.h | 2 --
src/formula/RewardNoBoundOperator.h | 2 --
src/formula/Until.h | 19 ++++++++++++++++++-
13 files changed, 145 insertions(+), 17 deletions(-)
diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h
index f675a319f..6e74c48a4 100644
--- a/src/formula/AbstractFormulaChecker.h
+++ b/src/formula/AbstractFormulaChecker.h
@@ -19,13 +19,13 @@ namespace formula {
*
* Usually, this will be implemented like this:
* @code
- * if (
+ * if (
* dynamic_cast<const And<T>*>(formula) ||
* dynamic_cast<const Not<T>*>(formula) ||
* dynamic_cast<const Or<T>*>(formula)
* ) {
* return formula->conforms(*this);
- * } else return false;
+ * } else return false;
* @endcode
*
* Every formula class implements a conforms() method itself which calls
diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h
index 3ab36c584..8f55b2c7c 100644
--- a/src/formula/InstantaneousReward.h
+++ b/src/formula/InstantaneousReward.h
@@ -20,9 +20,21 @@ namespace formula {
template <class T> class InstantaneousReward;
+/*!
+ * @brief Interface class for model checkers that support InstantaneousReward.
+ *
+ * All model checkers that support the formula class InstantaneousReward must inherit
+ * this pure virtual class.
+ */
template <class T>
class IInstantaneousRewardModelChecker {
public:
+ /*!
+ * @brief Evaluates InstantaneousReward formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkInstantaneousReward(const InstantaneousReward<T>& obj) const = 0;
};
@@ -113,6 +125,14 @@ public:
return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * As InstantaneousReward formulas have no subformulas, we return true here.
+ *
+ * @param checker Formula checker object.
+ * @return true
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return true;
}
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 8884ac5b6..a91a39ce1 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -18,9 +18,21 @@ namespace formula {
template <class T> class Next;
+/*!
+ * @brief Interface class for model checkers that support Next.
+ *
+ * All model checkers that support the formula class Next must inherit
+ * this pure virtual class.
+ */
template <class T>
class INextModelChecker {
public:
+ /*!
+ * @brief Evaluates Next formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkNext(const Next<T>& obj) const = 0;
};
@@ -125,6 +137,12 @@ public:
return modelChecker.template as<INextModelChecker>()->checkNext(*this);
}
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h
index c7a14d155..4a459c5e8 100644
--- a/src/formula/NoBoundOperator.h
+++ b/src/formula/NoBoundOperator.h
@@ -18,9 +18,21 @@ namespace formula {
template <class T> class NoBoundOperator;
+/*!
+ * @brief Interface class for model checkers that support NoBoundOperator.
+ *
+ * All model checkers that support the formula class NoBoundOperator must inherit
+ * this pure virtual class.
+ */
template <class T>
class INoBoundOperatorModelChecker {
public:
+ /*!
+ * @brief Evaluates NoBoundOperator formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkNoBoundOperator(const NoBoundOperator<T>& obj) const = 0;
};
@@ -118,6 +130,12 @@ public:
*/
virtual std::string toString() const = 0;
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->pathFormula);
}
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 56eaf6c6a..cd7a20399 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -18,9 +18,21 @@ namespace formula {
template <class T> class Not;
+/*!
+ * @brief Interface class for model checkers that support Not.
+ *
+ * All model checkers that support the formula class Not must inherit
+ * this pure virtual class.
+ */
template <class T>
class INotModelChecker {
public:
+ /*!
+ * @brief Evaluates Not formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
};
@@ -119,6 +131,12 @@ public:
return modelChecker.template as<INotModelChecker>()->checkNot(*this);
}
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
diff --git a/src/formula/Or.h b/src/formula/Or.h
index 6a071f395..e7dd117e5 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -16,9 +16,21 @@ namespace formula {
template <class T> class Or;
+/*!
+ * @brief Interface class for model checkers that support Or.
+ *
+ * All model checkers that support the formula class Or must inherit
+ * this pure virtual class.
+ */
template <class T>
class IOrModelChecker {
public:
+ /*!
+ * @brief Evaluates Or formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
};
@@ -152,6 +164,12 @@ public:
return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h
index 2a8d882e7..e99cb0666 100644
--- a/src/formula/PrctlFormulaChecker.h
+++ b/src/formula/PrctlFormulaChecker.h
@@ -9,9 +9,22 @@
namespace storm {
namespace formula {
+/*!
+ * @brief Checks formulas if they are within PRCTL.
+ *
+ * This class implements AbstractFormulaChecker to check if a given formula
+ * is part of PRCTL logic.
+ */
template <class T>
class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
public:
+ /*!
+ * Implementation of AbstractFormulaChecker::conforms() using code
+ * looking exactly like the sample code given there.
+ *
+ * We currently allow And, Ap, Eventually, Not, Or,
+ * ProbabilisticNoBoundOperator.
+ */
virtual bool conforms(const AbstractFormula<T>* formula) const {
if (
dynamic_cast<const And<T>*>(formula) ||
@@ -25,11 +38,9 @@ class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
}
return false;
}
-
- private:
};
-}
-}
+} // namespace formula
+} // namespace storm
#endif
\ No newline at end of file
diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h
index 3e6e7fde6..5ac0ff606 100644
--- a/src/formula/ProbabilisticBoundOperator.h
+++ b/src/formula/ProbabilisticBoundOperator.h
@@ -14,7 +14,6 @@
#include "utility/ConstTemplates.h"
namespace storm {
-
namespace formula {
/*!
@@ -92,7 +91,6 @@ public:
};
} //namespace formula
-
} //namespace storm
#endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */
diff --git a/src/formula/ProbabilisticNoBoundOperator.h b/src/formula/ProbabilisticNoBoundOperator.h
index bfe6f92db..07e79659c 100644
--- a/src/formula/ProbabilisticNoBoundOperator.h
+++ b/src/formula/ProbabilisticNoBoundOperator.h
@@ -13,7 +13,6 @@
#include "NoBoundOperator.h"
namespace storm {
-
namespace formula {
/*!
@@ -77,7 +76,6 @@ public:
};
} /* namespace formula */
-
} /* namespace storm */
#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index cef56ab6d..54e2f447b 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -14,14 +14,25 @@
#include "src/modelChecker/AbstractModelChecker.h"
namespace storm {
-
namespace formula {
template <class T> class ReachabilityReward;
+/*!
+ * @brief Interface class for model checkers that support ReachabilityReward.
+ *
+ * All model checkers that support the formula class ReachabilityReward must inherit
+ * this pure virtual class.
+ */
template <class T>
class IReachabilityRewardModelChecker {
public:
+ /*!
+ * @brief Evaluates ReachabilityReward formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkReachabilityReward(const ReachabilityReward<T>& obj) const = 0;
};
@@ -121,6 +132,12 @@ public:
return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this);
}
+ /*!
+ * @brief Checks if the subtree conforms to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff the subtree conforms to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->child);
}
@@ -130,7 +147,6 @@ private:
};
} //namespace formula
-
} //namespace storm
#endif /* STORM_FORMULA_REACHABILITYREWARD_H_ */
diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h
index b2c6065ff..3f30ec0c7 100644
--- a/src/formula/RewardBoundOperator.h
+++ b/src/formula/RewardBoundOperator.h
@@ -14,7 +14,6 @@
#include "utility/ConstTemplates.h"
namespace storm {
-
namespace formula {
/*!
@@ -90,7 +89,6 @@ public:
};
} //namespace formula
-
} //namespace storm
#endif /* STORM_FORMULA_REWARDBOUNDOPERATOR_H_ */
diff --git a/src/formula/RewardNoBoundOperator.h b/src/formula/RewardNoBoundOperator.h
index 3752b381a..f362a5232 100644
--- a/src/formula/RewardNoBoundOperator.h
+++ b/src/formula/RewardNoBoundOperator.h
@@ -13,7 +13,6 @@
#include "NoBoundOperator.h"
namespace storm {
-
namespace formula {
/*!
@@ -77,7 +76,6 @@ public:
};
} /* namespace formula */
-
} /* namespace storm */
#endif /* STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ */
diff --git a/src/formula/Until.h b/src/formula/Until.h
index cfc186f56..82ac05c9d 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -13,14 +13,25 @@
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
-
namespace formula {
template <class T> class Until;
+/*!
+ * @brief Interface class for model checkers that support Until.
+ *
+ * All model checkers that support the formula class Until must inherit
+ * this pure virtual class.
+ */
template <class T>
class IUntilModelChecker {
public:
+ /*!
+ * @brief Evaluates Until formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
virtual std::vector<T>* checkUntil(const Until<T>& obj) const = 0;
};
@@ -153,6 +164,12 @@ public:
return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
return checker.conforms(this->left) && checker.conforms(this->right);
}
From 1edd3060322155b0a1b696c4acf40e8f271981f7 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 29 Jan 2013 21:16:16 +0100
Subject: [PATCH 16/30] Silenced warning of clang: Changed NULL to nullptr as
this should be used in C++11.
---
src/parser/DeterministicSparseTransitionParser.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index 59eb336d7..632ac78ed 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -164,7 +164,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
*/
LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
this->matrix = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(maxnode + 1));
- if (this->matrix == NULL) {
+ if (this->matrix == nullptr) {
LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
throw std::bad_alloc();
}
From 43b56fce62f13d525d2c4a8e4018396d1fec3cf4 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Tue, 29 Jan 2013 21:22:56 +0100
Subject: [PATCH 17/30] first version of BoundedNaryUntil. clone() does not
work yet...
---
src/formula/BoundedNaryUntil.h | 209 +++++++++++++++++++++++++++++++++
src/formula/Formulas.h | 1 +
2 files changed, 210 insertions(+)
create mode 100644 src/formula/BoundedNaryUntil.h
diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h
new file mode 100644
index 000000000..bbd370cd9
--- /dev/null
+++ b/src/formula/BoundedNaryUntil.h
@@ -0,0 +1,209 @@
+/*
+ * BoundedNaryUntil.h
+ *
+ * Created on: 19.10.2012
+ * Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_BOUNDEDNARYUNTIL_H_
+#define STORM_FORMULA_BOUNDEDNARYUNTIL_H_
+
+#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
+#include "boost/integer/integer_mask.hpp"
+#include <string>
+#include <vector>
+#include <tuple>
+#include <sstream>
+#include "src/formula/AbstractFormulaChecker.h"
+
+namespace storm {
+namespace formula {
+
+template <class T> class BoundedNaryUntil;
+
+/*!
+ * @brief Interface class for model checkers that support BoundedNaryUntil.
+ *
+ * All model checkers that support the formula class BoundedNaryUntil must inherit
+ * this pure virtual class.
+ */
+template <class T>
+class IBoundedNaryUntilModelChecker {
+ public:
+ /*!
+ * @brief Evaluates BoundedNaryUntil formula within a model checker.
+ *
+ * @param obj Formula object with subformulas.
+ * @return Result of the formula for every node.
+ */
+ virtual std::vector<T>* checkBoundedNaryUntil(const BoundedNaryUntil<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a BoundedNaryUntil node as root.
+ *
+ * Has at least two Abstract state formulas as sub formulas and an interval
+ * associated with all but the first sub formula. We'll call the first one
+ * \e left and all other one \e right.
+ *
+ * @par Semantics
+ * The formula holds iff \e left holds until eventually any of the \e right
+ * formulas holds after a number of steps contained in the interval
+ * associated with this formula.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class BoundedNaryUntil : public AbstractPathFormula<T> {
+
+public:
+ /*!
+ * Empty constructor
+ */
+ BoundedNaryUntil() {
+ this->left = NULL;
+ this->right = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>();
+ }
+
+ /*!
+ * Constructor
+ *
+ * @param left The left formula subtree
+ * @param right The left formula subtree
+ * @param bound The maximal number of steps
+ */
+ BoundedNaryUntil(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right,
+ uint_fast64_t bound) {
+ this->left = left;
+ this->right = right;
+ }
+
+ /*!
+ * Destructor.
+ *
+ * Also deletes the subtrees.
+ * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ */
+ virtual ~BoundedNaryUntil() {
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
+ }
+
+ /*!
+ * Sets the left child node.
+ *
+ * @param newLeft the new left child.
+ */
+ void setLeft(AbstractStateFormula<T>* newLeft) {
+ left = newLeft;
+ }
+
+ void setRight(std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newRight) {
+ right = newRight;
+ }
+
+
+ /*!
+ * Sets the right child node.
+ *
+ * @param newRight the new right child.
+ */
+ void addRight(AbstractStateFormula<T>* newRight, T upperBound, T lowerBound) {
+ this->right->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(newRight, upperBound, lowerBound));
+ }
+
+ /*!
+ * @returns a pointer to the left child node
+ */
+ const AbstractStateFormula<T>& getLeft() const {
+ return *left;
+ }
+
+ /*!
+ * @returns a pointer to the right child nodes.
+ */
+ const std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>& getRight() const {
+ return *right;
+ }
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const {
+ std::stringstream result;
+ result << "( " << left->toString();
+ for (auto it = this->right->begin(); it != this->right->end(); ++it) {
+ result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString();
+ }
+ result << ")";
+ return result.str();
+ }
+
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @returns a new BoundedNaryUntil-object that is identical the called object.
+ */
+ virtual AbstractPathFormula<T>* clone() const {
+ BoundedNaryUntil<T>* result = new BoundedNaryUntil<T>();
+ if (left != NULL) {
+ result->setLeft(left->clone());
+ }
+ if (right != NULL) {
+ //TODO: implement clone of std::vector
+ //result->setRight(right->clone());
+ }
+ return result;
+ }
+
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @returns A vector indicating the probability that the formula holds for each state.
+ */
+ virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+ return modelChecker.template as<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this);
+ }
+
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
+ virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+ bool res = checker.conforms(this->left);
+ for (auto it = this->right->begin(); it != this->right->end(); ++it) {
+ res &= checker.conforms(std::get<0>(*it));
+ }
+ return res;
+ }
+
+private:
+ AbstractStateFormula<T>* left;
+ std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right;
+};
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_BOUNDEDNARYUNTIL_H_ */
diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h
index 09de1acf0..1a750f674 100644
--- a/src/formula/Formulas.h
+++ b/src/formula/Formulas.h
@@ -15,6 +15,7 @@
#include "And.h"
#include "Ap.h"
#include "BoundedUntil.h"
+#include "BoundedNaryUntil.h"
#include "Next.h"
#include "Not.h"
#include "Or.h"
From 9a9cd968d9caac0b6dd3bcdb9012fd8f68bb4d72 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Thu, 31 Jan 2013 00:00:47 +0100
Subject: [PATCH 18/30] Added a test to verify the RowSum Function in the
Sparse Matrix. Added an option to the settings for auto-fixing missing
no-selfloop states. Kind of a super-option above fix-nodeadlocks, perhaps
some Cleanup later on. Modified tra Files to comply with formats...
---
.../DeterministicSparseTransitionParser.cpp | 83 +++++++++++++++----
src/storage/SparseMatrix.h | 9 +-
src/utility/Settings.cpp | 1 +
test/storage/SparseMatrixTest.cpp | 9 ++
4 files changed, 84 insertions(+), 18 deletions(-)
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index 632ac78ed..c5668846d 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -66,9 +66,10 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0;
/*
- * Check all transitions for non-zero diagonal entrys.
+ * Check all transitions for existing diagonal entrys.
*/
- int_fast64_t row, lastrow = -1, col;
+ int_fast64_t row, col;
+ int_fast64_t lastDiagonal = -1;
double val;
maxnode = 0;
while (buf[0] != '\0') {
@@ -80,17 +81,29 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
/*
* Check if one is larger than the current maximum id.
*/
- if (row > maxnode) maxnode = row;
- if (col > maxnode) maxnode = col;
+ if (row > maxnode) {
+ maxnode = row;
+ }
+ if (col > maxnode) {
+ maxnode = col;
+ }
/*
- * Check if a node was skipped, i.e. if a node has no outgoing
- * transitions. If so, increase non_zero, as the second pass will
+ * Check if a self-loop was skipped. If so, increase non_zero, as the second pass will
* either throw an exception (in this case, it doesn't matter
* anyway) or add a self-loop (in this case, we'll need the
* additional transition).
*/
- if (lastrow < row - 1) non_zero += row - lastrow - 1;
- lastrow = row;
+ if (lastDiagonal < (row - 1)) {
+ non_zero += row - 1 - lastDiagonal;
+ lastDiagonal = row - 1;
+ }
+ /*
+ * Check if this is a self-loop and remember that
+ */
+ if (row == col) {
+ lastDiagonal = row;
+ }
+
/*
* Read probability of this transition.
* Check, if the value is a probability, i.e. if it is between 0 and 1.
@@ -103,6 +116,10 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
buf = trimWhitespaces(buf);
}
+ if (lastDiagonal < (row - 1)) {
+ non_zero += row - 1 - lastDiagonal;
+ }
+
return non_zero;
}
@@ -171,12 +188,15 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
this->matrix->initialize(non_zero);
int_fast64_t row, lastrow = -1, col;
+ int_fast64_t lastDiagonal = -1;
double val;
bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks");
+ bool fixSelfloops = storm::settings::instance()->isSet("fix-selfloops");
bool hadDeadlocks = false;
+ bool hadNoSelfLoops = false;
/*
- * Read all transitions from file. Note that we assume, that the
+ * Read all transitions from file. Note that we assume that the
* transitions are listed in canonical order, otherwise this will not
* work, i.e. the values in the matrix will be at wrong places.
*/
@@ -189,24 +209,53 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
val = checked_strtod(buf, &buf);
/*
- * Check if we skipped a node, i.e. if a node does not have any
- * outgoing transitions.
+ * Check if a self-loop was skipped.
*/
- for (int_fast64_t node = lastrow + 1; node < row; node++) {
- hadDeadlocks = true;
- if (fixDeadlocks) {
- this->matrix->addNextValue(node, node, 1);
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
+ if (lastDiagonal < (row - 1)) {
+ /*
+ * Check if we skipped a node entirely, i.e. a node does not have any
+ * outgoing transitions.
+ */
+ if ((lastrow + 1) < row) {
+ for (int_fast64_t node = lastrow + 1; node < row; node++) {
+ hadDeadlocks = true;
+ if (fixDeadlocks || fixSelfloops) {
+ this->matrix->addNextValue(node, node, storm::utility::constGetOne<double>());
+ LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
+ } else {
+ LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
+ }
+ }
} else {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
+ // there were other transitions but no self-loop
+ for (int_fast64_t node = lastDiagonal + 1; node < row; node++) {
+ hadNoSelfLoops = true;
+ if (fixSelfloops) {
+ this->matrix->addNextValue(node, node, storm::utility::constGetZero<double>());
+ LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no self transition. A self-loop was inserted.");
+ } else {
+ LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no self transition.");
+ }
+ }
}
+ lastDiagonal = row - 1;
+ }
+
+
+ /*
+ * Check if this is a self-loop and remember that
+ */
+ if (row == col) {
+ lastDiagonal = row;
}
+
lastrow = row;
this->matrix->addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
+ if (!fixSelfloops && hadNoSelfLoops) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had no self loops. You can use --fix-selfloops to insert self-loops on the fly.";
/*
* Finalize Matrix.
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index b7fa94d62..90807f1bc 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -799,22 +799,29 @@ public:
/*!
* Inverts all elements on the diagonal, i.e. sets the diagonal values to 1 minus their previous
* value.
+ * Requires the matrix to contain each diagonal element AND to be square!
*/
void invertDiagonal() {
if (this->getRowCount() != this->getColumnCount()) {
throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!";
}
- T one(1);
+ T one = storm::utility::constGetOne<T>();
+ bool foundRow;
for (uint_fast64_t row = 0; row < rowCount; ++row) {
uint_fast64_t rowStart = rowIndications[row];
uint_fast64_t rowEnd = rowIndications[row + 1];
+ foundRow = false;
while (rowStart < rowEnd) {
if (columnIndications[rowStart] == row) {
valueStorage[rowStart] = one - valueStorage[rowStart];
+ foundRow = true;
break;
}
++rowStart;
}
+ if (!foundRow) {
+ throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to contain all diagonal entries!";
+ }
}
}
diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp
index 26f733071..f983f22fc 100644
--- a/src/utility/Settings.cpp
+++ b/src/utility/Settings.cpp
@@ -139,6 +139,7 @@ void Settings::initDescriptions() {
("transrew", bpo::value<std::string>()->default_value(""), "name of transition reward file")
("staterew", bpo::value<std::string>()->default_value(""), "name of state reward file")
("fix-deadlocks", "insert self-loops for states without outgoing transitions")
+ ("fix-selfloops", "insert self-loops for states without such transitions")
;
}
diff --git a/test/storage/SparseMatrixTest.cpp b/test/storage/SparseMatrixTest.cpp
index 2a29fb736..b3eb68971 100644
--- a/test/storage/SparseMatrixTest.cpp
+++ b/test/storage/SparseMatrixTest.cpp
@@ -94,6 +94,10 @@ TEST(SparseMatrixTest, Test) {
2, 3, 4, 5, 6, 7, 8, 9, 10, 11,
14, 15, 16, 17, 18, 19, 20, 21, 22, 23 /* second to last row */
};
+ int row_sums[25] = {};
+ for (int i = 0; i < 50; ++i) {
+ row_sums[position_row[i]] += values[i];
+ }
ASSERT_NO_THROW(ssm->initialize(50));
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::Initialized);
@@ -123,6 +127,11 @@ TEST(SparseMatrixTest, Test) {
}
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
+ // Test Row Sums
+ for (int row = 0; row < 25; ++row) {
+ ASSERT_EQ(row_sums[row], ssm->getRowSum(row));
+ }
+
delete ssm;
}
From 726569d5f11c44eace4331ee18ef17606e3d0ef9 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 31 Jan 2013 10:40:28 +0100
Subject: [PATCH 19/30] Fixed bug in parser that inserted 0-entries on the
diagonal at the wrong places. Enabled link-time-optimizations for
Release-Build when using clang. Fixed bug in base exception: what() returned
a pointer to a char array belonging to a local variable, which got
deallocated and thus invalidates the char array content.
---
CMakeLists.txt | 2 +-
src/exceptions/BaseException.h | 6 +-
.../DeterministicSparseTransitionParser.cpp | 65 ++++++++-----------
.../DeterministicSparseTransitionParser.h | 2 +-
src/utility/Settings.cpp | 1 -
5 files changed, 35 insertions(+), 41 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 8caf0b081..d17922f26 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -75,7 +75,7 @@ elseif(MSVC)
add_definitions(/D_SCL_SECURE_NO_DEPRECATE)
else(CLANG)
# Set standard flags for clang
- set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
+ set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG -funroll-loops -O4")
set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable")
# Turn on popcnt instruction if desired (yes by default)
diff --git a/src/exceptions/BaseException.h b/src/exceptions/BaseException.h
index c1b6ee054..6c670f88b 100644
--- a/src/exceptions/BaseException.h
+++ b/src/exceptions/BaseException.h
@@ -28,7 +28,11 @@ class BaseException : public std::exception {
}
virtual const char* what() const throw() {
- return this->stream.str().c_str();
+ std::string errorString = this->stream.str();
+ char* result = new char[errorString.size() + 1];
+ result[errorString.size()] = '\0';
+ std::copy(errorString.begin(), errorString.end(), result);
+ return result;
}
private:
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index c5668846d..e9e430988 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -133,7 +133,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
* @return a pointer to the created sparse matrix.
*/
-DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename)
+DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing)
: matrix(nullptr) {
/*
* Enforce locale where decimal point is '.'.
@@ -188,12 +188,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
this->matrix->initialize(non_zero);
int_fast64_t row, lastrow = -1, col;
- int_fast64_t lastDiagonal = -1;
double val;
bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks");
- bool fixSelfloops = storm::settings::instance()->isSet("fix-selfloops");
bool hadDeadlocks = false;
- bool hadNoSelfLoops = false;
+ bool rowHadDiagonalEntry = false;
/*
* Read all transitions from file. Note that we assume that the
@@ -208,45 +206,39 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
+ if (row != lastrow) {
+ rowHadDiagonalEntry = false;
+ }
+
/*
- * Check if a self-loop was skipped.
+ * Check if we skipped a state entirely, i.e. a state does not have any
+ * outgoing transitions.
*/
- if (lastDiagonal < (row - 1)) {
- /*
- * Check if we skipped a node entirely, i.e. a node does not have any
- * outgoing transitions.
- */
- if ((lastrow + 1) < row) {
- for (int_fast64_t node = lastrow + 1; node < row; node++) {
- hadDeadlocks = true;
- if (fixDeadlocks || fixSelfloops) {
- this->matrix->addNextValue(node, node, storm::utility::constGetOne<double>());
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
- } else {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
- }
- }
- } else {
- // there were other transitions but no self-loop
- for (int_fast64_t node = lastDiagonal + 1; node < row; node++) {
- hadNoSelfLoops = true;
- if (fixSelfloops) {
- this->matrix->addNextValue(node, node, storm::utility::constGetZero<double>());
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no self transition. A self-loop was inserted.");
- } else {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no self transition.");
- }
+ if ((lastrow + 1) < row) {
+ for (int_fast64_t state = lastrow + 1; state < row; ++state) {
+ hadDeadlocks = true;
+ if (fixDeadlocks) {
+ this->matrix->addNextValue(state, state, storm::utility::constGetOne<double>());
+ LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << state << " has no outgoing transitions. A self-loop was inserted.");
+ } else {
+ LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << state << " has no outgoing transitions.");
}
}
- lastDiagonal = row - 1;
- }
-
-
+ }
+
+ // Insert the missing diagonal value if requested.
+ if (col > row && !rowHadDiagonalEntry) {
+ if (insertDiagonalEntriesIfMissing) {
+ this->matrix->addNextValue(row, row, storm::utility::constGetZero<double>());
+ }
+ rowHadDiagonalEntry = true;
+ }
+
/*
- * Check if this is a self-loop and remember that
+ * Check if the transition is a self-loop
*/
if (row == col) {
- lastDiagonal = row;
+ rowHadDiagonalEntry = true;
}
lastrow = row;
@@ -255,7 +247,6 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
buf = trimWhitespaces(buf);
}
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
- if (!fixSelfloops && hadNoSelfLoops) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had no self loops. You can use --fix-selfloops to insert self-loops on the fly.";
/*
* Finalize Matrix.
diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h
index 099d0fa4a..2407f3398 100644
--- a/src/parser/DeterministicSparseTransitionParser.h
+++ b/src/parser/DeterministicSparseTransitionParser.h
@@ -17,7 +17,7 @@ namespace parser {
*/
class DeterministicSparseTransitionParser : public Parser {
public:
- DeterministicSparseTransitionParser(std::string const &filename);
+ DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true);
std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
return this->matrix;
diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp
index f983f22fc..26f733071 100644
--- a/src/utility/Settings.cpp
+++ b/src/utility/Settings.cpp
@@ -139,7 +139,6 @@ void Settings::initDescriptions() {
("transrew", bpo::value<std::string>()->default_value(""), "name of transition reward file")
("staterew", bpo::value<std::string>()->default_value(""), "name of state reward file")
("fix-deadlocks", "insert self-loops for states without outgoing transitions")
- ("fix-selfloops", "insert self-loops for states without such transitions")
;
}
From 6fb56748a630d746be69218c6a7f8bc9fc4cc62e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 31 Jan 2013 15:10:36 +0100
Subject: [PATCH 20/30] Bugfix for correctly counting the number of values the
parser inserts.
---
.../DeterministicSparseTransitionParser.cpp | 159 ++++++++++--------
1 file changed, 91 insertions(+), 68 deletions(-)
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index e9e430988..24a5dc489 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -45,7 +45,7 @@ namespace parser {
* @param maxnode Is set to highest id of all nodes.
*/
uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode) {
- uint_fast64_t non_zero = 0;
+ uint_fast64_t nonZeroEntryCount = 0;
/*
* Check file header and extract number of transitions.
@@ -63,64 +63,75 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
return 0;
}
buf += 12; // skip "TRANSITIONS "
- if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0;
+ if ((nonZeroEntryCount = strtol(buf, &buf, 10)) == 0) return 0;
- /*
- * Check all transitions for existing diagonal entrys.
- */
- int_fast64_t row, col;
- int_fast64_t lastDiagonal = -1;
- double val;
- maxnode = 0;
- while (buf[0] != '\0') {
- /*
- * Read row and column.
- */
- row = checked_strtol(buf, &buf);
- col = checked_strtol(buf, &buf);
- /*
- * Check if one is larger than the current maximum id.
- */
- if (row > maxnode) {
- maxnode = row;
- }
- if (col > maxnode) {
- maxnode = col;
- }
- /*
- * Check if a self-loop was skipped. If so, increase non_zero, as the second pass will
- * either throw an exception (in this case, it doesn't matter
- * anyway) or add a self-loop (in this case, we'll need the
- * additional transition).
- */
- if (lastDiagonal < (row - 1)) {
- non_zero += row - 1 - lastDiagonal;
- lastDiagonal = row - 1;
- }
- /*
- * Check if this is a self-loop and remember that
- */
- if (row == col) {
- lastDiagonal = row;
- }
+ /*
+ * Check all transitions for non-zero diagonal entries and deadlock states.
+ */
+ int_fast64_t row, lastRow = -1, col;
+ bool rowHadDiagonalEntry = false;
+ double val;
+ maxnode = 0;
+ while (buf[0] != '\0') {
+ /*
+ * Read row and column.
+ */
+ row = checked_strtol(buf, &buf);
+ col = checked_strtol(buf, &buf);
- /*
- * Read probability of this transition.
- * Check, if the value is a probability, i.e. if it is between 0 and 1.
- */
- val = checked_strtod(buf, &buf);
- if ((val < 0.0) || (val > 1.0)) {
- LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
- return 0;
- }
- buf = trimWhitespaces(buf);
- }
+ /*
+ * If we have switched to the next row, we need to clear the information about
+ * the diagonal entry.
+ */
+ if (row != lastRow) {
+ /*
+ * If the last row did have transitions, but no diagonal element, we need to insert
+ * it as well.
+ */
+ if (!rowHadDiagonalEntry && lastRow != -1) {
+ ++nonZeroEntryCount;
+ }
+ rowHadDiagonalEntry = false;
+ }
- if (lastDiagonal < (row - 1)) {
- non_zero += row - 1 - lastDiagonal;
- }
+ if (row == col) {
+ rowHadDiagonalEntry = true;
+ }
- return non_zero;
+ /*
+ * Check if one is larger than the current maximum id.
+ */
+ if (row > maxnode) maxnode = row;
+ if (col > maxnode) maxnode = col;
+
+ /*
+ * Check if a node was skipped, i.e. if a node has no outgoing
+ * transitions. If so, increase non_zero, as the second pass will
+ * either throw an exception (in this case, it doesn't matter
+ * anyway) or add a self-loop (in this case, we'll need the
+ * additional transition).
+ */
+ if (lastRow < row - 1) {
+ nonZeroEntryCount += row - lastRow - 1;
+ }
+ lastRow = row;
+ /*
+ * Read probability of this transition.
+ * Check, if the value is a probability, i.e. if it is between 0 and 1.
+ */
+ val = checked_strtod(buf, &buf);
+ if ((val < 0.0) || (val > 1.0)) {
+ LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
+ return 0;
+ }
+ buf = trimWhitespaces(buf);
+ }
+
+ if (!rowHadDiagonalEntry) {
+ ++nonZeroEntryCount;
+ }
+
+ return nonZeroEntryCount;
}
@@ -149,12 +160,12 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
/*
* Perform first pass, i.e. count entries that are not zero.
*/
- int_fast64_t maxnode;
- uint_fast64_t non_zero = this->firstPass(file.data, maxnode);
+ int_fast64_t maxStateId;
+ uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId);
/*
* If first pass returned zero, the file format was wrong.
*/
- if (non_zero == 0) {
+ if (nonZeroEntryCount == 0) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format.");
throw storm::exceptions::WrongFileFormatException();
}
@@ -179,15 +190,15 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
* Creating matrix here.
* The number of non-zero elements is computed by firstPass().
*/
- LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
- this->matrix = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(maxnode + 1));
+ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << ".");
+ this->matrix = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(maxStateId + 1));
if (this->matrix == nullptr) {
- LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
+ LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << ".");
throw std::bad_alloc();
}
- this->matrix->initialize(non_zero);
+ this->matrix->initialize(nonZeroEntryCount);
- int_fast64_t row, lastrow = -1, col;
+ int_fast64_t row, lastRow = -1, col;
double val;
bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks");
bool hadDeadlocks = false;
@@ -206,7 +217,14 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
- if (row != lastrow) {
+ if (row != lastRow) {
+ /*
+ * If the previous row did not have a diagonal entry, we need to insert it.
+ */
+ if (!rowHadDiagonalEntry && lastRow != -1) {
+ this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
+ }
+
rowHadDiagonalEntry = false;
}
@@ -214,8 +232,8 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
* Check if we skipped a state entirely, i.e. a state does not have any
* outgoing transitions.
*/
- if ((lastrow + 1) < row) {
- for (int_fast64_t state = lastrow + 1; state < row; ++state) {
+ if ((lastRow + 1) < row) {
+ for (int_fast64_t state = lastRow + 1; state < row; ++state) {
hadDeadlocks = true;
if (fixDeadlocks) {
this->matrix->addNextValue(state, state, storm::utility::constGetOne<double>());
@@ -226,7 +244,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
}
}
- // Insert the missing diagonal value if requested.
+ // Insert the missing diagonal value here, because the input skipped it.
if (col > row && !rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
this->matrix->addNextValue(row, row, storm::utility::constGetZero<double>());
@@ -241,11 +259,16 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
rowHadDiagonalEntry = true;
}
- lastrow = row;
+ lastRow = row;
this->matrix->addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
+
+ if (!rowHadDiagonalEntry) {
+ this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
+ }
+
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
/*
From 02cb1a241812ac8190c9fbf7e709525b99b28aa5 Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Fri, 1 Feb 2013 15:53:40 +0100
Subject: [PATCH 21/30] Replaced all calls to Matrix->toEigenSparseMatrix with
calls to the adapter.
---
src/modelChecker/EigenDtmcPrctlModelChecker.h | 7 ++++---
test/storage/SparseMatrixTest.cpp | 3 ++-
2 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h
index 26a18cd8d..a784ca9d9 100644
--- a/src/modelChecker/EigenDtmcPrctlModelChecker.h
+++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h
@@ -18,6 +18,7 @@
#include "Eigen/Sparse"
#include "Eigen/src/IterativeLinearSolvers/BiCGSTAB.h"
+#include "src/adapters/EigenAdapter.h"
#include "gmm/gmm_matrix.h"
#include "gmm/gmm_iter_solvers.h"
@@ -54,7 +55,7 @@ public:
tmpMatrix.makeRowsAbsorbing((~*leftStates | *rightStates) | *rightStates);
// Transform the transition probability matrix to the eigen format to use its arithmetic.
- Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = tmpMatrix.toEigenSparseMatrix();
+ Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(tmpMatrix);
// Create the vector with which to multiply.
uint_fast64_t stateCount = this->getModel().getNumberOfStates();
@@ -88,7 +89,7 @@ public:
storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild());
// Transform the transition probability matrix to the eigen format to use its arithmetic.
- Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = this->getModel().getTransitionProbabilityMatrix()->toEigenSparseMatrix();
+ Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(this->getModel().getTransitionProbabilityMatrix());
// Create the vector with which to multiply and initialize it correctly.
std::vector<Type> x(this->getModel().getNumberOfStates());
@@ -154,7 +155,7 @@ public:
submatrix->convertToEquationSystem();
// Transform the submatric matrix to the eigen format to use its solvers
- Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenSubMatrix = submatrix->toEigenSparseMatrix();
+ Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenSubMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(submatrix);
delete submatrix;
// Initialize the x vector with 0.5 for each element. This is the initial guess for
diff --git a/test/storage/SparseMatrixTest.cpp b/test/storage/SparseMatrixTest.cpp
index b3eb68971..6a20050dd 100644
--- a/test/storage/SparseMatrixTest.cpp
+++ b/test/storage/SparseMatrixTest.cpp
@@ -2,6 +2,7 @@
#include "src/storage/SparseMatrix.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/OutOfRangeException.h"
+#include "src/adapters/EigenAdapter.h"
TEST(SparseMatrixTest, ZeroRowsTest) {
storm::storage::SparseMatrix<int> *ssm = new storm::storage::SparseMatrix<int>(0);
@@ -322,7 +323,7 @@ TEST(SparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest) {
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
- Eigen::SparseMatrix<int, Eigen::RowMajor, int_fast32_t>* esm = ssm->toEigenSparseMatrix();
+ Eigen::SparseMatrix<int, Eigen::RowMajor, int_fast32_t>* esm = storm::adapters::EigenAdapter::toEigenSparseMatrix<int>(*ssm);
for (uint_fast32_t row = 0; row < 10; ++row) {
for (uint_fast32_t col = 0; col < 10; ++col) {
From a598d3751c3084d3c51db85c17d3d95add4cde9f Mon Sep 17 00:00:00 2001
From: PBerger <philipp.berger@rwth-aachen.de>
Date: Fri, 1 Feb 2013 15:55:13 +0100
Subject: [PATCH 22/30] The DeterministicSparseTransitionParser.cpp was still
broken, rewrote it in a simpler and more convenient way. All Deterministic
Tests complete now.
---
.../DeterministicSparseTransitionParser.cpp | 123 +++++++++---------
test/parser/ParseDtmcTest.cpp | 2 +-
test/parser/ReadTraFileTest.cpp | 52 ++++----
3 files changed, 91 insertions(+), 86 deletions(-)
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index 24a5dc489..b4446be5b 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -46,7 +46,7 @@ namespace parser {
*/
uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode) {
uint_fast64_t nonZeroEntryCount = 0;
-
+ uint_fast64_t inputFileNonZeroEntryCount = 0;
/*
* Check file header and extract number of transitions.
*/
@@ -63,12 +63,13 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
return 0;
}
buf += 12; // skip "TRANSITIONS "
- if ((nonZeroEntryCount = strtol(buf, &buf, 10)) == 0) return 0;
+ if ((inputFileNonZeroEntryCount = strtol(buf, &buf, 10)) == 0) return 0;
/*
* Check all transitions for non-zero diagonal entries and deadlock states.
*/
int_fast64_t row, lastRow = -1, col;
+ uint_fast64_t readTransitionCount = 0;
bool rowHadDiagonalEntry = false;
double val;
maxnode = 0;
@@ -79,24 +80,24 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
- /*
- * If we have switched to the next row, we need to clear the information about
- * the diagonal entry.
- */
- if (row != lastRow) {
- /*
- * If the last row did have transitions, but no diagonal element, we need to insert
- * it as well.
- */
- if (!rowHadDiagonalEntry && lastRow != -1) {
- ++nonZeroEntryCount;
- }
- rowHadDiagonalEntry = false;
- }
+ if (lastRow != row) {
+ if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
+ ++nonZeroEntryCount;
+ rowHadDiagonalEntry = true;
+ }
+ for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
+ ++nonZeroEntryCount;
+ }
+ lastRow = row;
+ rowHadDiagonalEntry = false;
+ }
- if (row == col) {
- rowHadDiagonalEntry = true;
- }
+ if (col == row) {
+ rowHadDiagonalEntry = true;
+ } else if (col > row && !rowHadDiagonalEntry) {
+ rowHadDiagonalEntry = true;
+ ++nonZeroEntryCount;
+ }
/*
* Check if one is larger than the current maximum id.
@@ -104,17 +105,6 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
if (row > maxnode) maxnode = row;
if (col > maxnode) maxnode = col;
- /*
- * Check if a node was skipped, i.e. if a node has no outgoing
- * transitions. If so, increase non_zero, as the second pass will
- * either throw an exception (in this case, it doesn't matter
- * anyway) or add a self-loop (in this case, we'll need the
- * additional transition).
- */
- if (lastRow < row - 1) {
- nonZeroEntryCount += row - lastRow - 1;
- }
- lastRow = row;
/*
* Read probability of this transition.
* Check, if the value is a probability, i.e. if it is between 0 and 1.
@@ -124,6 +114,8 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\".");
return 0;
}
+ ++nonZeroEntryCount;
+ ++readTransitionCount;
buf = trimWhitespaces(buf);
}
@@ -131,6 +123,11 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
++nonZeroEntryCount;
}
+ if (inputFileNonZeroEntryCount != readTransitionCount) {
+ LOG4CPLUS_ERROR(logger, "Input File TRANSITIONS line stated " << inputFileNonZeroEntryCount << " but there were " << readTransitionCount << " transitions afterwards.");
+ return 0;
+ }
+
return nonZeroEntryCount;
}
@@ -162,6 +159,9 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
*/
int_fast64_t maxStateId;
uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId);
+
+ LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros.");
+
/*
* If first pass returned zero, the file format was wrong.
*/
@@ -217,56 +217,55 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
col = checked_strtol(buf, &buf);
val = checked_strtod(buf, &buf);
- if (row != lastRow) {
- /*
- * If the previous row did not have a diagonal entry, we need to insert it.
- */
- if (!rowHadDiagonalEntry && lastRow != -1) {
- this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
+ if (lastRow != row) {
+ if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
+ if (insertDiagonalEntriesIfMissing) {
+ this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
+ LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
+ } else {
+ LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
+ }
+ // No increment for lastRow
+ rowHadDiagonalEntry = true;
}
-
- rowHadDiagonalEntry = false;
- }
-
- /*
- * Check if we skipped a state entirely, i.e. a state does not have any
- * outgoing transitions.
- */
- if ((lastRow + 1) < row) {
- for (int_fast64_t state = lastRow + 1; state < row; ++state) {
+ for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
hadDeadlocks = true;
if (fixDeadlocks) {
- this->matrix->addNextValue(state, state, storm::utility::constGetOne<double>());
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << state << " has no outgoing transitions. A self-loop was inserted.");
+ this->matrix->addNextValue(skippedRow, skippedRow, storm::utility::constGetOne<double>());
+ rowHadDiagonalEntry = true;
+ LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
} else {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << state << " has no outgoing transitions.");
+ LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
+ // FIXME Why no exception at this point? This will break the App.
}
}
+ lastRow = row;
+ rowHadDiagonalEntry = false;
}
- // Insert the missing diagonal value here, because the input skipped it.
- if (col > row && !rowHadDiagonalEntry) {
+ if (col == row) {
+ rowHadDiagonalEntry = true;
+ } else if (col > row && !rowHadDiagonalEntry) {
+ rowHadDiagonalEntry = true;
if (insertDiagonalEntriesIfMissing) {
this->matrix->addNextValue(row, row, storm::utility::constGetZero<double>());
+ LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
+ } else {
+ LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
}
- rowHadDiagonalEntry = true;
}
- /*
- * Check if the transition is a self-loop
- */
- if (row == col) {
- rowHadDiagonalEntry = true;
- }
-
- lastRow = row;
-
this->matrix->addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
if (!rowHadDiagonalEntry) {
- this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
+ if (insertDiagonalEntriesIfMissing) {
+ this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
+ LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
+ } else {
+ LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
+ }
}
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
diff --git a/test/parser/ParseDtmcTest.cpp b/test/parser/ParseDtmcTest.cpp
index f5bd8f163..d99c16f74 100644
--- a/test/parser/ParseDtmcTest.cpp
+++ b/test/parser/ParseDtmcTest.cpp
@@ -12,7 +12,7 @@
#include "src/utility/IoUtility.h"
TEST(ParseDtmcTest, parseAndOutput) {
- storm::parser::DeterministicModelParser* dtmcParser;
+ storm::parser::DeterministicModelParser* dtmcParser = nullptr;
ASSERT_NO_THROW(dtmcParser = new storm::parser::DeterministicModelParser(
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
diff --git a/test/parser/ReadTraFileTest.cpp b/test/parser/ReadTraFileTest.cpp
index 2bda7561e..17cfec798 100644
--- a/test/parser/ReadTraFileTest.cpp
+++ b/test/parser/ReadTraFileTest.cpp
@@ -22,45 +22,51 @@ TEST(ReadTraFileTest, NonExistingFileTest) {
/* The following test case is based on one of the original STORM test cases
*/
TEST(ReadTraFileTest, ParseFileTest1) {
- storm::parser::DeterministicSparseTransitionParser* parser;
+ storm::parser::DeterministicSparseTransitionParser* parser = nullptr;
ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
std::shared_ptr<storm::storage::SparseMatrix<double>> result = parser->getMatrix();
if (result != NULL) {
double val = 0;
- ASSERT_TRUE(result->getValue(1,1,&val));
- ASSERT_EQ(val,0.080645161290322580645161290322581);
+ ASSERT_TRUE(result->getValue(0, 0, &val));
+ ASSERT_EQ(val, 0.0);
- ASSERT_TRUE(result->getValue(1,2,&val));
- ASSERT_EQ(val,0.080645161290322580645161290322581);
+ ASSERT_TRUE(result->getValue(0, 1, &val));
+ ASSERT_EQ(val, 1.0);
+
+ ASSERT_TRUE(result->getValue(1, 1, &val));
+ ASSERT_EQ(val, 0.080645161290322580645161290322581);
+
+ ASSERT_TRUE(result->getValue(1, 2, &val));
+ ASSERT_EQ(val, 0.080645161290322580645161290322581);
//Transition 1->3 was not set in the file, so it is not to appear in the matrix!
- ASSERT_FALSE(result->getValue(1,3,&val));
- ASSERT_EQ(val,0);
+ ASSERT_FALSE(result->getValue(1, 3, &val));
+ ASSERT_EQ(val, 0);
- ASSERT_TRUE(result->getValue(2,1,&val));
- ASSERT_EQ(val,0.04032258064516129032258064516129);
+ ASSERT_TRUE(result->getValue(2, 1, &val));
+ ASSERT_EQ(val, 0.04032258064516129032258064516129);
- ASSERT_TRUE(result->getValue(2,2,&val));
- ASSERT_EQ(val,0.04032258064516129032258064516129);
+ ASSERT_TRUE(result->getValue(2, 2, &val));
+ ASSERT_EQ(val, 0.04032258064516129032258064516129);
- ASSERT_TRUE(result->getValue(2,3,&val));
- ASSERT_EQ(val,0.04032258064516129032258064516129);
+ ASSERT_TRUE(result->getValue(2, 3, &val));
+ ASSERT_EQ(val, 0.04032258064516129032258064516129);
- ASSERT_TRUE(result->getValue(2,4,&val));
- ASSERT_EQ(val,0.04032258064516129032258064516129);
+ ASSERT_TRUE(result->getValue(2, 4, &val));
+ ASSERT_EQ(val, 0.04032258064516129032258064516129);
- ASSERT_TRUE(result->getValue(3,2,&val));
- ASSERT_EQ(val,0.0806451612903225806451612903225812);
+ ASSERT_TRUE(result->getValue(3, 2, &val));
+ ASSERT_EQ(val, 0.0806451612903225806451612903225812);
- ASSERT_FALSE(result->getValue(3,3,&val));
- ASSERT_EQ(val,0);
+ ASSERT_TRUE(result->getValue(3, 3, &val));
+ ASSERT_EQ(val, 0.0);
- ASSERT_TRUE(result->getValue(3,4,&val));
- ASSERT_EQ(val,0.080645161290322580645161290322581);
+ ASSERT_TRUE(result->getValue(3, 4, &val));
+ ASSERT_EQ(val, 0.080645161290322580645161290322581);
- ASSERT_FALSE(result->getValue(4,4,&val));
- ASSERT_EQ(val,0);
+ ASSERT_TRUE(result->getValue(4, 4, &val));
+ ASSERT_EQ(val, 0.0);
delete parser;
} else {
From be182293ee4f3d8ed78fc71e33f97116d766f168 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 2 Feb 2013 20:26:11 +0100
Subject: [PATCH 23/30] Small fix on Eigen-based model checker to make it
compile with clang.
---
src/modelChecker/EigenDtmcPrctlModelChecker.h | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h
index a784ca9d9..25bf4984b 100644
--- a/src/modelChecker/EigenDtmcPrctlModelChecker.h
+++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h
@@ -155,7 +155,7 @@ public:
submatrix->convertToEquationSystem();
// Transform the submatric matrix to the eigen format to use its solvers
- Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenSubMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(submatrix);
+ Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenSubMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix<Type>(submatrix);
delete submatrix;
// Initialize the x vector with 0.5 for each element. This is the initial guess for
From 1d1f9da315c0611057572734454c64a664e42c7c Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sun, 3 Feb 2013 20:42:07 +0100
Subject: [PATCH 24/30] made rowMapping from NDSTParser available in MDP model
class
---
src/models/Mdp.h | 9 +++++++--
src/parser/MdpParser.cpp | 2 +-
src/parser/NonDeterministicSparseTransitionParser.cpp | 6 +++---
src/parser/NonDeterministicSparseTransitionParser.h | 7 ++++---
4 files changed, 15 insertions(+), 9 deletions(-)
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index dc58782a2..26922b573 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -20,6 +20,7 @@
#include "src/utility/CommandLine.h"
#include "src/utility/Settings.h"
#include "src/models/AbstractModel.h"
+#include "src/parser/NonDeterministicSparseTransitionParser.h"
namespace storm {
@@ -44,9 +45,10 @@ public:
*/
Mdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
+ std::shared_ptr<storm::parser::RowStateMapping> rowMapping,
std::shared_ptr<std::vector<T>> stateRewards = nullptr,
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
- : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling),
+ : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping),
stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
backwardTransitions(nullptr) {
if (!this->checkValidityOfProbabilityMatrix()) {
@@ -61,7 +63,7 @@ public:
* @param mdp A reference to the MDP that is to be copied.
*/
Mdp(const Mdp<T> &mdp) : probabilityMatrix(mdp.probabilityMatrix),
- stateLabeling(mdp.stateLabeling), stateRewards(mdp.stateRewards),
+ stateLabeling(mdp.stateLabeling), rowMapping(mdp.rowMapping), stateRewards(mdp.stateRewards),
transitionRewardMatrix(mdp.transitionRewardMatrix) {
if (mdp.backwardTransitions != nullptr) {
this->backwardTransitions = new storm::models::GraphTransitions<T>(*mdp.backwardTransitions);
@@ -225,6 +227,9 @@ private:
/*! The labeling of the states of the MDP. */
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
+
+ /*! The mapping from rows to (state,choice) pairs. */
+ std::shared_ptr<storm::parser::RowStateMapping> rowMapping;
/*! The state-based rewards of the MDP. */
std::shared_ptr<std::vector<T>> stateRewards;
diff --git a/src/parser/MdpParser.cpp b/src/parser/MdpParser.cpp
index f73c0b515..ac73b4e40 100644
--- a/src/parser/MdpParser.cpp
+++ b/src/parser/MdpParser.cpp
@@ -45,7 +45,7 @@ MdpParser::MdpParser(std::string const & transitionSystemFile, std::string const
transitionRewards = trp.getMatrix();
}
- mdp = std::shared_ptr<storm::models::Mdp<double>>(new storm::models::Mdp<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards));
+ mdp = std::shared_ptr<storm::models::Mdp<double>>(new storm::models::Mdp<double>(tp.getMatrix(), lp.getLabeling(), tp.getRowMapping(), stateRewards, transitionRewards));
}
} /* namespace parser */
diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp
index 1eb270739..93c8d779d 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.cpp
+++ b/src/parser/NonDeterministicSparseTransitionParser.cpp
@@ -214,7 +214,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
/*
* Create row mapping.
*/
- this->rowMapping = std::shared_ptr<RowMapping>(new RowMapping());
+ this->rowMapping = std::shared_ptr<RowStateMapping>(new RowStateMapping());
/*
* Parse file content.
@@ -245,7 +245,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
for (int_fast64_t node = lastsource + 1; node < source; node++) {
hadDeadlocks = true;
if (fixDeadlocks) {
- this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, "")));
+ this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, "")));
this->matrix->addNextValue(curRow, node, 1);
curRow++;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
@@ -258,7 +258,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
/*
* Add this source-choice pair to rowMapping.
*/
- this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(source, choice)));
+ this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(source, choice)));
/*
* Skip name of choice.
diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NonDeterministicSparseTransitionParser.h
index 592e2814f..5edc0a72e 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.h
+++ b/src/parser/NonDeterministicSparseTransitionParser.h
@@ -14,6 +14,8 @@
namespace storm {
namespace parser {
+typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowStateMapping;
+
/*!
* @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges
@@ -26,14 +28,13 @@ class NonDeterministicSparseTransitionParser : public Parser {
return this->matrix;
}
- typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowMapping;
- inline std::shared_ptr<RowMapping> getRowMapping() const {
+ inline std::shared_ptr<RowStateMapping> getRowMapping() const {
return this->rowMapping;
}
private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
- std::shared_ptr<RowMapping> rowMapping;
+ std::shared_ptr<RowStateMapping> rowMapping;
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode);
From 583ebf62bd0e2b840ac21408792a7010fea3c9c4 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sun, 3 Feb 2013 20:42:07 +0100
Subject: [PATCH 25/30] made rowMapping from NDSTParser available in MDP model
class
---
src/models/Mdp.h | 9 +++++++--
src/parser/MdpParser.cpp | 2 +-
src/parser/NonDeterministicSparseTransitionParser.cpp | 6 +++---
src/parser/NonDeterministicSparseTransitionParser.h | 7 ++++---
4 files changed, 15 insertions(+), 9 deletions(-)
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index dc58782a2..26922b573 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -20,6 +20,7 @@
#include "src/utility/CommandLine.h"
#include "src/utility/Settings.h"
#include "src/models/AbstractModel.h"
+#include "src/parser/NonDeterministicSparseTransitionParser.h"
namespace storm {
@@ -44,9 +45,10 @@ public:
*/
Mdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
+ std::shared_ptr<storm::parser::RowStateMapping> rowMapping,
std::shared_ptr<std::vector<T>> stateRewards = nullptr,
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
- : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling),
+ : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping),
stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
backwardTransitions(nullptr) {
if (!this->checkValidityOfProbabilityMatrix()) {
@@ -61,7 +63,7 @@ public:
* @param mdp A reference to the MDP that is to be copied.
*/
Mdp(const Mdp<T> &mdp) : probabilityMatrix(mdp.probabilityMatrix),
- stateLabeling(mdp.stateLabeling), stateRewards(mdp.stateRewards),
+ stateLabeling(mdp.stateLabeling), rowMapping(mdp.rowMapping), stateRewards(mdp.stateRewards),
transitionRewardMatrix(mdp.transitionRewardMatrix) {
if (mdp.backwardTransitions != nullptr) {
this->backwardTransitions = new storm::models::GraphTransitions<T>(*mdp.backwardTransitions);
@@ -225,6 +227,9 @@ private:
/*! The labeling of the states of the MDP. */
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
+
+ /*! The mapping from rows to (state,choice) pairs. */
+ std::shared_ptr<storm::parser::RowStateMapping> rowMapping;
/*! The state-based rewards of the MDP. */
std::shared_ptr<std::vector<T>> stateRewards;
diff --git a/src/parser/MdpParser.cpp b/src/parser/MdpParser.cpp
index f73c0b515..ac73b4e40 100644
--- a/src/parser/MdpParser.cpp
+++ b/src/parser/MdpParser.cpp
@@ -45,7 +45,7 @@ MdpParser::MdpParser(std::string const & transitionSystemFile, std::string const
transitionRewards = trp.getMatrix();
}
- mdp = std::shared_ptr<storm::models::Mdp<double>>(new storm::models::Mdp<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards));
+ mdp = std::shared_ptr<storm::models::Mdp<double>>(new storm::models::Mdp<double>(tp.getMatrix(), lp.getLabeling(), tp.getRowMapping(), stateRewards, transitionRewards));
}
} /* namespace parser */
diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp
index 1eb270739..93c8d779d 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.cpp
+++ b/src/parser/NonDeterministicSparseTransitionParser.cpp
@@ -214,7 +214,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
/*
* Create row mapping.
*/
- this->rowMapping = std::shared_ptr<RowMapping>(new RowMapping());
+ this->rowMapping = std::shared_ptr<RowStateMapping>(new RowStateMapping());
/*
* Parse file content.
@@ -245,7 +245,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
for (int_fast64_t node = lastsource + 1; node < source; node++) {
hadDeadlocks = true;
if (fixDeadlocks) {
- this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, "")));
+ this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, "")));
this->matrix->addNextValue(curRow, node, 1);
curRow++;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
@@ -258,7 +258,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
/*
* Add this source-choice pair to rowMapping.
*/
- this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(source, choice)));
+ this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(source, choice)));
/*
* Skip name of choice.
diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NonDeterministicSparseTransitionParser.h
index 592e2814f..5edc0a72e 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.h
+++ b/src/parser/NonDeterministicSparseTransitionParser.h
@@ -14,6 +14,8 @@
namespace storm {
namespace parser {
+typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowStateMapping;
+
/*!
* @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges
@@ -26,14 +28,13 @@ class NonDeterministicSparseTransitionParser : public Parser {
return this->matrix;
}
- typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowMapping;
- inline std::shared_ptr<RowMapping> getRowMapping() const {
+ inline std::shared_ptr<RowStateMapping> getRowMapping() const {
return this->rowMapping;
}
private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
- std::shared_ptr<RowMapping> rowMapping;
+ std::shared_ptr<RowStateMapping> rowMapping;
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode);
From 54565ddd55d44ef04bd2e63c820952ebffbb4522 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Mon, 4 Feb 2013 09:41:09 +0100
Subject: [PATCH 26/30] changed rowMapping to vector<int>
---
src/models/Mdp.h | 6 +++---
.../NonDeterministicSparseTransitionParser.cpp | 15 ++++++++-------
.../NonDeterministicSparseTransitionParser.h | 7 ++-----
3 files changed, 13 insertions(+), 15 deletions(-)
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index 26922b573..5b9d0157f 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -45,7 +45,7 @@ public:
*/
Mdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
- std::shared_ptr<storm::parser::RowStateMapping> rowMapping,
+ std::shared_ptr<std::vector<uint_fast64_t>> rowMapping,
std::shared_ptr<std::vector<T>> stateRewards = nullptr,
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping),
@@ -228,8 +228,8 @@ private:
/*! The labeling of the states of the MDP. */
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
- /*! The mapping from rows to (state,choice) pairs. */
- std::shared_ptr<storm::parser::RowStateMapping> rowMapping;
+ /*! The mapping from states to rows. */
+ std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
/*! The state-based rewards of the MDP. */
std::shared_ptr<std::vector<T>> stateRewards;
diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp
index 93c8d779d..f6b70e719 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.cpp
+++ b/src/parser/NonDeterministicSparseTransitionParser.cpp
@@ -214,7 +214,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
/*
* Create row mapping.
*/
- this->rowMapping = std::shared_ptr<RowStateMapping>(new RowStateMapping());
+ this->rowMapping = std::shared_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>(maxnode+1,0));
/*
* Parse file content.
@@ -245,7 +245,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
for (int_fast64_t node = lastsource + 1; node < source; node++) {
hadDeadlocks = true;
if (fixDeadlocks) {
- this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, "")));
+ this->rowMapping->at(node) = curRow;
this->matrix->addNextValue(curRow, node, 1);
curRow++;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
@@ -253,13 +253,14 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
}
}
+ if (source != lastsource) {
+ /*
+ * Add this source to rowMapping, if this is the first choice we encounter for this state.
+ */
+ this->rowMapping->at(source) = curRow;
+ }
lastsource = source;
- /*
- * Add this source-choice pair to rowMapping.
- */
- this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(source, choice)));
-
/*
* Skip name of choice.
*/
diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NonDeterministicSparseTransitionParser.h
index 5edc0a72e..a0d9ea50a 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.h
+++ b/src/parser/NonDeterministicSparseTransitionParser.h
@@ -6,7 +6,6 @@
#include "src/parser/Parser.h"
#include "src/utility/OsDetection.h"
-#include <boost/bimap.hpp>
#include <utility>
#include <memory>
#include <vector>
@@ -14,8 +13,6 @@
namespace storm {
namespace parser {
-typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowStateMapping;
-
/*!
* @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges
@@ -28,13 +25,13 @@ class NonDeterministicSparseTransitionParser : public Parser {
return this->matrix;
}
- inline std::shared_ptr<RowStateMapping> getRowMapping() const {
+ inline std::shared_ptr<std::vector<uint_fast64_t>> getRowMapping() const {
return this->rowMapping;
}
private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
- std::shared_ptr<RowStateMapping> rowMapping;
+ std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode);
From 55c2d5c03fcf0cf25fcd717b8ac67e4fa8880d58 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Mon, 4 Feb 2013 09:46:44 +0100
Subject: [PATCH 27/30] implemented clone for BoundedNaryUntil
---
src/formula/BoundedNaryUntil.h | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h
index bbd370cd9..2ff54a779 100644
--- a/src/formula/BoundedNaryUntil.h
+++ b/src/formula/BoundedNaryUntil.h
@@ -163,8 +163,11 @@ public:
result->setLeft(left->clone());
}
if (right != NULL) {
- //TODO: implement clone of std::vector
- //result->setRight(right->clone());
+ std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newright = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>();
+ for (auto it = this->right->begin(); it != this->right->end(); ++it) {
+ newright->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(std::get<0>(*it)->clone(), std::get<1>(*it), std::get<2>(*it)));
+ }
+ result->setRight(newright);
}
return result;
}
From d7a288d05a1c7d4ea570175cb4c70cc8236a9328 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Mon, 4 Feb 2013 09:50:09 +0100
Subject: [PATCH 28/30] fixed "copy" constructor
---
src/formula/BoundedNaryUntil.h | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h
index 2ff54a779..c42dab12b 100644
--- a/src/formula/BoundedNaryUntil.h
+++ b/src/formula/BoundedNaryUntil.h
@@ -79,8 +79,7 @@ public:
* @param right The left formula subtree
* @param bound The maximal number of steps
*/
- BoundedNaryUntil(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right,
- uint_fast64_t bound) {
+ BoundedNaryUntil(AbstractStateFormula<T>* left, std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right) {
this->left = left;
this->right = right;
}
From 86965ff12a6eea0a7565c69a8321255daa265e11 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Mon, 4 Feb 2013 16:31:10 +0100
Subject: [PATCH 29/30] removed obsolete typedef
---
src/parser/NonDeterministicSparseTransitionParser.h | 2 --
1 file changed, 2 deletions(-)
diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NonDeterministicSparseTransitionParser.h
index 60695b7e9..a0d9ea50a 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.h
+++ b/src/parser/NonDeterministicSparseTransitionParser.h
@@ -13,8 +13,6 @@
namespace storm {
namespace parser {
-typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowStateMapping;
-
/*!
* @brief Load a nondeterministic transition system from file and create a
* sparse adjacency matrix whose entries represent the weights of the edges
From e52379bb54dbead93c33622cf9e34fd9cf1f887a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 6 Feb 2013 11:52:53 +0100
Subject: [PATCH 30/30] Added XCode stuff to .gitignore. Fixed a few tests to
compile with clang under -Werror.
---
.gitignore | 12 +++++++-----
test/parser/ParseMdpTest.cpp | 2 +-
test/parser/ReadLabFileTest.cpp | 4 ++--
test/parser/ReadTraFileTest.cpp | 2 +-
4 files changed, 11 insertions(+), 9 deletions(-)
diff --git a/.gitignore b/.gitignore
index 6f15a4cb4..750826475 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,8 +1,8 @@
-#Third-Party libs
-resources/3rdparty/log4cplus-1.1.0/
-resources/3rdparty/gtest-1.6.0/
-resources/3rdparty/eigen/
-resources/3rdparty/gmm-4.2/
+##Third-Party libs
+resources/3rdparty/log4cplus-1.1.0/**
+resources/3rdparty/gtest-1.6.0/**
+resources/3rdparty/eigen/**
+resources/3rdparty/gmm-4.2/**
#Visual Studio files
*.[Oo]bj
*.user
@@ -25,6 +25,8 @@ resources/3rdparty/gmm-4.2/
*.sdf
*.opensdf
*.unsuccessfulbuild
+# XCode directories and files
+storm/**
ipch/
obj/
CMakeFiles/
diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp
index 4147c0122..cfa50f1c7 100644
--- a/test/parser/ParseMdpTest.cpp
+++ b/test/parser/ParseMdpTest.cpp
@@ -12,7 +12,7 @@
#include "src/utility/IoUtility.h"
TEST(ParseMdpTest, parseAndOutput) {
- storm::parser::MdpParser* mdpParser;
+ storm::parser::MdpParser* mdpParser = nullptr;
ASSERT_NO_THROW(mdpParser = new storm::parser::MdpParser(
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
diff --git a/test/parser/ReadLabFileTest.cpp b/test/parser/ReadLabFileTest.cpp
index e7e2df029..9b1d72241 100644
--- a/test/parser/ReadLabFileTest.cpp
+++ b/test/parser/ReadLabFileTest.cpp
@@ -23,7 +23,7 @@ TEST(ReadLabFileTest, ParseTest) {
//This test is based on a test case from the original MRMC.
- storm::parser::AtomicPropositionLabelingParser* parser;
+ storm::parser::AtomicPropositionLabelingParser* parser = nullptr;
//Parsing the file
ASSERT_NO_THROW(parser = new storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling(parser->getLabeling());
@@ -32,7 +32,7 @@ TEST(ReadLabFileTest, ParseTest) {
char phi[] = "phi", psi[] = "psi", smth[] = "smth";
- if (labeling != NULL) {
+ if (labeling != nullptr) {
ASSERT_TRUE(labeling->containsAtomicProposition(phi));
ASSERT_TRUE(labeling->containsAtomicProposition(psi));
ASSERT_TRUE(labeling->containsAtomicProposition(smth));
diff --git a/test/parser/ReadTraFileTest.cpp b/test/parser/ReadTraFileTest.cpp
index 17cfec798..6a697536d 100644
--- a/test/parser/ReadTraFileTest.cpp
+++ b/test/parser/ReadTraFileTest.cpp
@@ -26,7 +26,7 @@ TEST(ReadTraFileTest, ParseFileTest1) {
ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
std::shared_ptr<storm::storage::SparseMatrix<double>> result = parser->getMatrix();
- if (result != NULL) {
+ if (result != nullptr) {
double val = 0;
ASSERT_TRUE(result->getValue(0, 0, &val));
ASSERT_EQ(val, 0.0);