From 6bd8c8f9b5a195ae7db6db6a28e061f6e537754d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 30 Jun 2017 18:27:27 +0200 Subject: [PATCH] Fixed some typos --- src/storm-dft/CMakeLists.txt | 2 +- src/storm/analysis/GraphConditions.cpp | 1 + src/storm/analysis/GraphConditions.h | 6 +++--- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index 3951551ae..9ec70aed2 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -8,7 +8,7 @@ file(GLOB_RECURSE STORM_DFT_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.cpp) file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h) -# Create storm-pgcl. +# Create storm-dft. add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS}) # Remove define symbol for shared libstorm. diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 9d915e73e..812429dec 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -72,6 +72,7 @@ namespace storm { wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().denominator().polynomial(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ)); // TODO: Assert: transition <= 1 <==> if denom > 0 then nom - denom <= 0 else nom - denom >= 0 } + // Assert: transition > 0 graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::NEQ); } } diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 87b95a78c..c6043fd5a 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -35,7 +35,7 @@ namespace storm { void wellformedRequiresNonNegativeEntries(std::vector const&); public: /*! - * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for + * Constructs a constraint collector for the given DTMC. The constraints are built and ready for * retrieval after the construction. * * @param dtmc The DTMC for which to create the constraints. @@ -47,14 +47,14 @@ namespace storm { * * @return The set of wellformed-ness constraints. */ - std::unordered_set::val> const& getWellformedConstraints() const; + std::unordered_set::val> const& getWellformedConstraints() const; /*! * Returns the set of graph-preserving constraints. * * @return The set of graph-preserving constraints. */ - std::unordered_set::val> const& getGraphPreservingConstraints() const; + std::unordered_set::val> const& getGraphPreservingConstraints() const; /*! * Constructs the constraints for the given DTMC.