sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

merge 

Former-commit-id: c51951e3f0
tempestpy_adaptions
sjunges 10 years ago
parent
d8a3009bde 8e2de5fbb1
commit
05e918a484
10 changed files with 146 additions and 85 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 63
      CMakeLists.txt
  2. 47
      resources/cmake/FindZ3.cmake
  3. 2
      src/models/sparse/Dtmc.cpp
  4. 4
      src/models/sparse/Dtmc.h
  5. 2
      src/parser/PrismParser.cpp
  6. 58
      src/storage/SparseMatrix.h
  7. 16
      src/storage/expressions/ExpressionManager.cpp
  8. 30
      src/storage/expressions/ExpressionManager.h
  9. 8
      storm-config.h.in
  10. 1
      test/functional/parser/PrismParserTest.cpp

63
CMakeLists.txt
View File

@ -28,7 +28,6 @@ option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precom
option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF)
option(USE_LIBCXX "Sets whether the standard library is libc++." OFF)
set(GUROBI_ROOT "" CACHE STRING "The root directory of Gurobi (if available).")
set(Z3_ROOT "" CACHE STRING "The root directory of Z3 (if available).")
set(CUDA_ROOT "" CACHE STRING "The root directory of CUDA.")
set(MSAT_ROOT "" CACHE STRING "The root directory of MathSAT (if available).")
set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.")
@ -61,6 +60,7 @@ find_package(Gurobi)
find_package(TBB)
find_package(Threads REQUIRED)
find_package(GMP)
find_package(Z3)
# If the DEBUG option was turned on, we will target a debug version and a release version otherwise.
if (STORM_DEBUG)
@ -82,12 +82,6 @@ else()
set(ENABLE_CUDA ON)
endif()
if ("${Z3_ROOT}" STREQUAL "")
set(ENABLE_Z3 OFF)
else()
set(ENABLE_Z3 ON)
set(Z3_LIB_NAME "z3")
endif()
if ("${MSAT_ROOT}" STREQUAL "")
set(ENABLE_MSAT OFF)
@ -146,10 +140,6 @@ elseif(MSVC)
# since nobody cares at the moment
add_definitions(/wd4250)
if(ENABLE_Z3)
set(Z3_LIB_NAME "libz3")
endif()
# MSVC does not do strict-aliasing, so no option needed
else(CLANG)
set(STORM_COMPILED_BY "Clang (LLVM)")
@ -213,11 +203,7 @@ message(STATUS "StoRM - Version information: ${STORM_CPP_VERSION_MAJOR}.${STORM_
# Base path for test files
set(STORM_CPP_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/test")
# Gurobi Defines
if (ENABLE_GUROBI)
set(STORM_CPP_GUROBI_DEF "define")
else()
set(STORM_CPP_GUROBI_DEF "undef")
endif()
set(STORM_HAVE_GUROBI ${ENABLE_GUROBI})
# CUDA Defines
if (ENABLE_CUDA)
@ -227,24 +213,16 @@ else()
endif()
# glpk defines
set(STORM_CPP_GLPK_DEF "define")
set(STORM_HAVE_GLPK 1)
# CUDA Defines
set(STORM_CPP_CUDAFORSTORM_DEF "undef")
# Z3 Defines
if (ENABLE_Z3)
set(STORM_CPP_Z3_DEF "define")
else()
set(STORM_CPP_Z3_DEF "undef")
endif()
set(STORM_HAVE_Z3 ${FOUND_Z3})
# MathSAT Defines
if (ENABLE_MSAT)
set(STORM_CPP_MSAT_DEF "define")
else()
set(STORM_CPP_MSAT_DEF "undef")
endif()
set(STORM_HAVE_MSAT ${ENABLE_MSAT})
# Intel TBB Defines
if (TBB_FOUND AND STORM_USE_INTELTBB)
@ -478,9 +456,6 @@ if (ENABLE_GUROBI)
endif()
#link_directories("${GUROBI_ROOT}/lib")
endif()
if (ENABLE_Z3)
link_directories("${Z3_ROOT}/bin")
endif()
if (ENABLE_MSAT)
link_directories("${MSAT_ROOT}/lib")
endif()
@ -552,8 +527,6 @@ if (ENABLE_GUROBI)
message (STATUS "StoRM - Linking with Gurobi (include: ${GUROBI_INCLUDE_DIRS})")
include_directories(${GUROBI_INCLUDE_DIRS})
target_link_libraries(storm ${GUROBI_LIBRARY})
target_link_libraries(storm-functional-tests ${GUROBI_LIBRARY})
target_link_libraries(storm-performance-tests ${GUROBI_LIBRARY})
endif(ENABLE_GUROBI)
#############################################################
@ -563,11 +536,8 @@ endif(ENABLE_GUROBI)
#############################################################
if (ENABLE_CUDA)
message (STATUS "StoRM - Linking with CUDA")
target_link_libraries(storm ${STORM_CUDA_LIB_NAME})
target_link_libraries(storm-functional-tests ${STORM_CUDA_LIB_NAME})
target_link_libraries(storm-performance-tests ${STORM_CUDA_LIB_NAME})
include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/")
target_link_libraries(storm ${STORM_CUDA_LIB_NAME})
include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/")
endif(ENABLE_CUDA)
#############################################################
@ -593,11 +563,12 @@ include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/exprtk")
## Z3 (optional)
##
#############################################################
if (ENABLE_Z3)
if(STORM_HAVE_Z3)
message (STATUS "StoRM - Linking with Z3")
include_directories("${Z3_ROOT}/include")
target_link_libraries(storm ${Z3_LIB_NAME})
endif(ENABLE_Z3)
include_directories(${Z3_INCLUDE_DIRS})
target_link_libraries(storm ${Z3_LIBRARIES})
endif(STORM_HAVE_Z3)
#############################################################
##
@ -608,6 +579,7 @@ endif(ENABLE_Z3)
if(STORM_HAVE_CARL)
message(STATUS "StoRM - Linking with carl.")
include_directories("${carl_INCLUDE_DIR}")
<<<<<<< HEAD
target_link_libraries(storm ${carl_LIBRARIES})
target_link_libraries(storm-functional-tests ${carl_LIBRARIES})
target_link_libraries(storm-performance-tests ${carl_LIBRARIES})
@ -625,6 +597,9 @@ message(STATUS "StoRM - Linking with smtrat.")
target_link_libraries(storm ${smtrat_LIBRARIES})
target_link_libraries(storm-functional-tests ${smtrat_LIBRARIES})
target_link_libraries(storm-performance-tests ${smtrat_LIBRARIES})
=======
target_link_libraries(storm lib_carl)
>>>>>>> master
endif()
#############################################################
@ -636,18 +611,12 @@ if (ENABLE_MSAT)
message (STATUS "StoRM - Linking with MathSAT")
include_directories("${MSAT_ROOT}/include")
target_link_libraries(storm "mathsat")
target_link_libraries(storm-functional-tests "mathsat")
target_link_libraries(storm-performance-tests "mathsat")
if(GMP_FOUND)
include_directories("${GMP_INCLUDE_DIR}")
target_link_libraries(storm "gmp")
target_link_libraries(storm-functional-tests "gmp")
target_link_libraries(storm-performance-tests "gmp")
elseif(MPIR_FOUND)
include_directories("${GMP_INCLUDE_DIR}")
target_link_libraries(storm "mpir" "mpirxx")
target_link_libraries(storm-functional-tests "mpir" "mpirxx")
target_link_libraries(storm-performance-tests "mpir" "mpirxx")
else(GMP_FOUND)
message(FATAL_ERROR "GMP is required for MathSAT, but was not found!")
endif(GMP_FOUND)

47
resources/cmake/FindZ3.cmake
View File

@ -0,0 +1,47 @@
# - Try to find libz3
# Once done this will define
# LIBZ3_FOUND - System has libz3
# LIBZ3_INCLUDE_DIRS - The libz3 include directories
# LIBZ3_LIBRARIES - The libraries needed to use libz3
# dependencies
# -- TODO -- needed?
# find include dir by searching for a concrete file, which definetely must be in it
find_path(Z3_INCLUDE_DIR
NAMES src/util/z3_exception.h #exemplary file, should only be available in z3
PATHS ENV PATH INCLUDE
PATH_SUFFIXES z3
)
# find library
find_library(Z3_LIBRARY
NAMES z3
PATHS /usr/local/include/z3/build ENV PATH INCLUDE
)
find_program(Z3_EXEC
NAMES z3
PATHS ENV PATH INCLUDE)
# set up the final variables
set(Z3_LIBRARIES ${Z3_LIBRARY})
set(Z3_INCLUDE_DIRS ${Z3_INCLUDE_DIR}/src/util)
set(Z3_SOLVER ${Z3_EXEC})
# set the LIBZ3_FOUND variable by utilizing the following macro
# (which also handles the REQUIRED and QUIET arguments)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(z3 DEFAULT_MSG
Z3_LIBRARY Z3_INCLUDE_DIR)
IF (NOT Z3_FIND_QUIETLY)
MESSAGE(STATUS "Found Z3: ${Z3_LIBRARY}")
ENDIF (NOT Z3_FIND_QUIETLY)
# debug output to see if everything went well
#message(${Z3_INCLUDE_DIR})
#message(${Z3_LIBRARY})
# make the set variables only visible in advanced mode
mark_as_advanced(Z3_LIBRARY Z3_INCLUDE_DIR Z3_SOLVER)

2
src/models/sparse/Dtmc.cpp
View File

@ -182,6 +182,7 @@ namespace storm {
// return storm::models::Dtmc<ValueType>(newMatBuilder.build(), newLabeling, newStateRewards, std::move(newTransitionRewards), newChoiceLabels);
}
#ifdef STORM_HAVE_CARL
template<typename ValueType>
Dtmc<ValueType>::ConstraintCollector::ConstraintCollector(Dtmc<ValueType> const& dtmc) {
process(dtmc);
@ -221,6 +222,7 @@ namespace storm {
void Dtmc<ValueType>::ConstraintCollector::operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
process(dtmc);
}
#endif
template <typename ValueType>
bool Dtmc<ValueType>::checkValidityOfProbabilityMatrix() const {

4
src/models/sparse/Dtmc.h
View File

@ -59,6 +59,7 @@ namespace storm {
*/
Dtmc<ValueType> getSubDtmc(storm::storage::BitVector const& states) const;
#ifdef STORM_HAVE_CARL
class ConstraintCollector {
private:
// A set of constraints that says that the DTMC actually has valid probability distributions in all states.
@ -109,7 +110,8 @@ namespace storm {
void operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc);
};
#endif
private:
/*!
* Checks the probability matrix for validity.

2
src/parser/PrismParser.cpp
View File

@ -133,7 +133,7 @@ namespace storm {
assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expressionParser > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
assignmentDefinition.name("assignment");
assignmentDefinitionList %= +assignmentDefinition % "&";
assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()];
assignmentDefinitionList.name("assignment list");
updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];

58
src/storage/SparseMatrix.h
View File

@ -385,7 +385,7 @@ namespace storm {
index_type getNumberOfEntries() const;
private:
// The pointer to the columnd and value of the first entry.
// The pointer to the column and value of the first entry.
const_iterator beginIterator;
// The number of non-zero entries in the rows.
@ -492,33 +492,33 @@ namespace storm {
*/
index_type getEntryCount() const;
/*!
* Returns the number of entries in the given row group of the matrix.
*
* @return The number of entries in the given row group of the matrix.
*/
uint_fast64_t getRowGroupEntryCount(uint_fast64_t const group) const;
/*!
* Returns the number of entries in the given row group of the matrix.
*
* @return The number of entries in the given row group of the matrix.
*/
uint_fast64_t getRowGroupEntryCount(uint_fast64_t const group) const;
/*!
* Returns the cached number of nonzero entries in the matrix.
*
* @see updateNonzeroEntryCount()
*
* @return The number of nonzero entries in the matrix.
*/
index_type getNonzeroEntryCount() const;
/*!
* Returns the cached number of nonzero entries in the matrix.
*
* @see updateNonzeroEntryCount()
*
* @return The number of nonzero entries in the matrix.
*/
index_type getNonzeroEntryCount() const;
/*!
* Recompute the nonzero entry count
*/
void updateNonzeroEntryCount() const;
/*!
* Recompute the nonzero entry count
*/
void updateNonzeroEntryCount() const;
/*!
* Change the nonzero entry count by the provided value.
*
* @param difference Difference between old and new nonzero entry count.
*/
void updateNonzeroEntryCount(std::make_signed<index_type>::type difference);
/*!
* Change the nonzero entry count by the provided value.
*
* @param difference Difference between old and new nonzero entry count.
*/
void updateNonzeroEntryCount(std::make_signed<index_type>::type difference);
/*!
* Returns the number of row groups in the matrix.
@ -622,13 +622,13 @@ namespace storm {
/*!
* Transposes the matrix.
*
* @param joinGroups A flag indicating whether the row groups are supposed to be treated as single rows.
* @param keepZeros A flag indicating whether entries with value zero should be kept.
*
* @param joinGroups A flag indicating whether the row groups are supposed to be treated as single rows.
* @param keepZeros A flag indicating whether entries with value zero should be kept.
*
* @return A sparse matrix that represents the transpose of this matrix.
*/
storm::storage::SparseMatrix<value_type> transpose(bool joinGroups = false, bool keepZeros = false) const;
storm::storage::SparseMatrix<value_type> transpose(bool joinGroups = false, bool keepZeros = false) const;
/*!
* Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A).

16
src/storage/expressions/ExpressionManager.cpp
View File

@ -200,11 +200,23 @@ namespace storm {
return nameToIndexMapping.find(name) != nameToIndexMapping.end();
}
Variable ExpressionManager::declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary) {
std::string newName = "__x" + std::to_string(freshVariableCounter++);
Variable ExpressionManager::declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary, std::string const& prefix) {
std::string newName = prefix + std::to_string(freshVariableCounter++);
return declareOrGetVariable(newName, variableType, auxiliary, false);
}
Variable ExpressionManager::declareFreshBooleanVariable(bool auxiliary, const std::string& prefix) {
return declareFreshVariable(this->getBooleanType(), auxiliary, prefix);
}
Variable ExpressionManager::declareFreshIntegerVariable(bool auxiliary, const std::string& prefix) {
return declareFreshVariable(this->getIntegerType(), auxiliary, prefix);
}
Variable ExpressionManager::declareFreshRationalVariable(bool auxiliary, const std::string& prefix) {
return declareFreshVariable(this->getRationalType(), auxiliary, prefix);
}
uint_fast64_t ExpressionManager::getNumberOfVariables(storm::expressions::Type const& variableType) const {
if (variableType.isBooleanType()) {
return numberOfBooleanVariables;

30
src/storage/expressions/ExpressionManager.h
View File

@ -230,9 +230,37 @@ namespace storm {
*
* @param variableType The type of the variable to declare.
* @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable.
* @param prefix The prefix which should be used.
* @return The variable.
*/
Variable declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary = false);
Variable declareFreshVariable(storm::expressions::Type const& variableType, bool auxiliary = false, std::string const& prefix = "x");
/*!
* Declares a variable with rational type whose name is guaranteed to be unique and not yet in use.
*
* @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable.
* @param prefix The prefix which should be used.
* @return The variable.
*/
Variable declareFreshRationalVariable(bool auxiliary = false, std::string const& prefix = "x");
/*!
* Declares a variable with Boolean type whose name is guaranteed to be unique and not yet in use.
*
* @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable.
* @param prefix The prefix which should be used.
* @return The variable.
*/
Variable declareFreshBooleanVariable(bool auxiliary = false, std::string const& prefix = "x");
/*!
* Declares a variable with integer type whose name is guaranteed to be unique and not yet in use.
*
* @param auxiliary A flag indicating whether the new variable should be tagged as an auxiliary variable.
* @param prefix The prefix which should be used.
* @return The variable.
*/
Variable declareFreshIntegerVariable(bool auxiliary = false, std::string const& prefix = "x");
/*!
* Retrieves the number of variables.

8
storm-config.h.in
View File

@ -15,22 +15,22 @@
#define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@"
// Whether Gurobi is available and to be used (define/undef)
#@STORM_CPP_GUROBI_DEF@ STORM_HAVE_GUROBI
#cmakedefine STORM_HAVE_GUROBI
// Whether CUDA is available (define/undef)
#@STORM_CPP_CUDA_DEF@ STORM_HAVE_CUDA
// Whether GLPK is available and to be used (define/undef)
#@STORM_CPP_GLPK_DEF@ STORM_HAVE_GLPK
#cmakedefine STORM_HAVE_GLPK
// Whether CudaForStorm is available and to be used (define/undef)
#@STORM_CPP_CUDAFORSTORM_DEF@ STORM_HAVE_CUDAFORSTORM
// Whether Z3 is available and to be used (define/undef)
#@STORM_CPP_Z3_DEF@ STORM_HAVE_Z3
#cmakedefine STORM_HAVE_Z3
// Whether MathSAT is available and to be used (define/undef)
#@STORM_CPP_MSAT_DEF@ STORM_HAVE_MSAT
#cmakedefine STORM_HAVE_MSAT
// Whether Intel Threading Building Blocks are available and to be used (define/undef)
#@STORM_CPP_INTELTBB_DEF@ STORM_HAVE_INTELTBB

1
test/functional/parser/PrismParserTest.cpp
View File

@ -40,6 +40,7 @@ TEST(PrismParser, SimpleTest) {
[] x=3 -> 1:(x'=1);
[] x=3 -> 1:(x'=4);
[] x=4 -> 1:(x'=5);
[] x=5 -> 1: true;
endmodule)";
EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
EXPECT_EQ(1, result.getNumberOfModules());

Write Preview
Loading…
Cancel
Save