From edd3a9a20e8e6c85a22d08fcfee841be26d387e8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 25 Jan 2013 19:43:32 +0100 Subject: [PATCH] Added possibility to evaluate expressions without concrete variables. Fixed some minor things in CUDD Makefiles. Renamed IR adapter. --- CMakeLists.txt | 17 +++ resources/3rdparty/cudd-2.5.0/Makefile | 14 ++- resources/3rdparty/cudd-2.5.0/obj/Makefile | 113 ++++++++++++++++++ ...tationAdapter.h => ExplicitModelAdapter.h} | 37 +++--- src/ir/IntegerVariable.cpp | 11 ++ src/ir/IntegerVariable.h | 12 ++ src/ir/expressions/BaseExpression.h | 6 +- .../BinaryBooleanFunctionExpression.h | 2 +- .../BinaryNumericalFunctionExpression.h | 4 +- src/ir/expressions/BinaryRelationExpression.h | 2 +- .../expressions/BooleanConstantExpression.h | 2 +- src/ir/expressions/BooleanLiteral.h | 2 +- src/ir/expressions/DoubleConstantExpression.h | 2 +- src/ir/expressions/DoubleLiteral.h | 2 +- .../expressions/IntegerConstantExpression.h | 2 +- src/ir/expressions/IntegerLiteral.h | 2 +- .../UnaryBooleanFunctionExpression.h | 2 +- .../UnaryNumericalFunctionExpression.h | 4 +- src/ir/expressions/VariableExpression.h | 20 +++- src/storm.cpp | 8 +- 20 files changed, 214 insertions(+), 50 deletions(-) create mode 100644 resources/3rdparty/cudd-2.5.0/obj/Makefile rename src/adapters/{IntermediateRepresentationAdapter.h => ExplicitModelAdapter.h} (93%) diff --git a/CMakeLists.txt b/CMakeLists.txt index 360907867..0c8983239 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -44,6 +44,12 @@ message(STATUS "EIGEN3_INCLUDE_DIR is ${EIGEN3_INCLUDE_DIR}") set(GMMXX_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-4.2/include) message(STATUS "GMMXX_INCLUDE_DIR is ${GMMXX_INCLUDE_DIR}") +# Set all CUDD references to the version in the repository +set(CUDD_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/include) +set(CUDD_LIBRARY_DIRS ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/cudd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/mtr ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/util ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/st ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/epd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/obj) +message(STATUS "CUDD_INCLUDE_DIR is ${CUDD_INCLUDE_DIR}") +message(STATUS "CUDD_LIBRARY_DIRS is ${CUDD_LIBRARY_DIRS}") + # Now define all available custom options option(DEBUG "Sets whether the DEBUG mode is used" ON) option(USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON) @@ -160,6 +166,13 @@ if (ADDITIONAL_LINK_DIRS) link_directories(${ADDITIONAL_LINK_DIRS}) endif(ADDITIONAL_LINK_DIRS) +if (CUDD_INCLUDE_DIR) + include_directories(${CUDD_INCLUDE_DIR}) +endif(CUDD_INCLUDE_DIR) +if (CUDD_LIBRARY_DIRS) + link_directories(${CUDD_LIBRARY_DIRS}) +endif(CUDD_LIBRARY_DIRS) + # Add the executables # Must be created *after* Boost was added because of LINK_DIRECTORIES add_executable(storm ${STORM_SOURCES} ${STORM_HEADERS}) @@ -211,6 +224,10 @@ if (LOG4CPLUS_INCLUDE_DIR) endif(UNIX AND NOT APPLE) endif(LOG4CPLUS_INCLUDE_DIR) +if (CUDD_LIBRARY_DIRS) + target_link_libraries(storm "-lcudd -lmtr -lst -lutil -lepd -lobj") +endif(CUDD_LIBRARY_DIRS) + if (THREADS_FOUND) include_directories(${THREADS_INCLUDE_DIRS}) target_link_libraries (storm ${CMAKE_THREAD_LIBS_INIT}) diff --git a/resources/3rdparty/cudd-2.5.0/Makefile b/resources/3rdparty/cudd-2.5.0/Makefile index e38ffa6ec..b1b5f32c8 100644 --- a/resources/3rdparty/cudd-2.5.0/Makefile +++ b/resources/3rdparty/cudd-2.5.0/Makefile @@ -7,15 +7,16 @@ # be overridden from the command line. # C++ compiler -CXX = g++ +#CXX = g++ #CXX = icpc #CXX = ecpc #CXX = CC #CXX = /usr/local/opt/SUNWspro/bin/CC #CXX = cxx +CXX = clang++ # Specific options for compilation of C++ files. -CXXFLAGS = +CXXFLAGS = -std=c++11 -stdlib=libc++ # Stricter standard conformance for g++. #CXXFLAGS = -std=c++98 # For Sun CC version 5, this invokes compatibility mode. @@ -27,12 +28,13 @@ CXXFLAGS = # C compiler used for all targets except optimize_dec, which always uses cc. #CC = cc #CC = /usr/local/opt/SUNWspro/bin/cc -CC = gcc +#CC = gcc #CC = icc #CC = ecc #CC = /usr/ucb/cc #CC = c89 #CC = $(CXX) +CC = clang # On some machines ranlib is either non-existent or redundant. # Use the following definition if your machine has ranlib and you think @@ -49,7 +51,7 @@ RANLIB = ranlib #ICFLAGS = # These two are typical settings for optimized code with gcc. #ICFLAGS = -g -O3 -Wall -ICFLAGS = -g -O3 +ICFLAGS = -O3 # Use XCFLAGS to specify machine-dependent compilation flags. # For some platforms no special flags are needed. @@ -59,7 +61,7 @@ ICFLAGS = -g -O3 # Linux # # Gcc 4.2.4 or higher on i686. -XCFLAGS = -mtune=native -malign-double -DHAVE_IEEE_754 -DBSD +XCFLAGS = -arch x86_64 -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8 # Gcc 3.2.2 or higher on i686. #XCFLAGS = -mtune=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD # Gcc 2.8.1 on i686. @@ -198,7 +200,7 @@ DDWDIR = . IDIR = $(DDWDIR)/include INCLUDE = -I$(IDIR) -BDIRS = cudd dddmp mtr st util epd +BDIRS = cudd dddmp mtr st util epd obj DIRS = $(BDIRS) nanotrav #------------------------------------------------------------------------ diff --git a/resources/3rdparty/cudd-2.5.0/obj/Makefile b/resources/3rdparty/cudd-2.5.0/obj/Makefile new file mode 100644 index 000000000..d3f62e1ad --- /dev/null +++ b/resources/3rdparty/cudd-2.5.0/obj/Makefile @@ -0,0 +1,113 @@ +# $Id: Makefile,v 1.3 2001/03/19 07:34:37 fabio Exp fabio $ +# +# obj: CUDD's C++ interface +#--------------------------------------------------------------------------- +.SUFFIXES: .o .cc .u + +#CXX = g++ +CXX = clang++ +RANLIB = ranlib +# Define EXE as .exe for MS-DOS and derivatives. +PURE = +EXE = +#EXE = .exe + +MFLAG = +#ICFLAGS = -g +ICFLAGS = +XCFLAGS = +#CXXFLAGS = +CXXFLAGS = -O3 -std=c++11 -stdlib=libc++ +CFLAGS = $(ICFLAGS) $(MFLAG) $(XCFLAGS) $(CXXFLAGS) +DDDEBUG = + +LINTFLAGS = -u -n -DDD_STATS -DDD_CACHE_PROFILE -DDD_VERBOSE -DDD_DEBUG -DDD_UNIQUE_PROFILE + +# this is to create the lint library +LINTSWITCH = -o + +WHERE = .. + +INCLUDE = $(WHERE)/include + +LIBS = ./libobj.a $(WHERE)/cudd/libcudd.a $(WHERE)/mtr/libmtr.a \ + $(WHERE)/st/libst.a $(WHERE)/util/libutil.a $(WHERE)/epd/libepd.a + +MNEMLIB = + +BLIBS = -kL. -klobj -kL$(WHERE)/cudd -klcudd -kL$(WHERE)/mtr -klmtr \ + -kL$(WHERE)/st -klst -kL$(WHERE)/util -klutil -kL$(WHERE)/epd -klepd + +LINTLIBS = ./llib-lobj.ln $(WHERE)/cudd/llib-lcudd.ln \ + $(WHERE)/mtr/llib-lmtr.ln $(WHERE)/st/llib-lst.ln \ + $(WHERE)/util/llib-lutil.ln $(WHERE)/epd/llib-lepd.ln + +LDFLAGS = + +# files for the package +P = obj +PSRC = cuddObj.cc +PHDR = cuddObj.hh $(INCLUDE)/cudd.h +POBJ = $(PSRC:.cc=.o) +PUBJ = $(PSRC:.cc=.u) +TARGET = test$(P)$(EXE) +TARGETu = test$(P)-u + +# files for the test program +SRC = test$(P).cc +OBJ = $(SRC:.cc=.o) +UBJ = $(SRC:.cc=.u) + +#------------------------------------------------------ + +lib$(P).a: $(POBJ) + ar rv $@ $? + $(RANLIB) $@ + +.cc.o: $(PHDR) + $(CXX) -c $< -I$(INCLUDE) $(CFLAGS) $(DDDEBUG) + +optimize_dec: lib$(P).b + +lib$(P).b: $(PUBJ) + ar rv $@ $? + $(RANLIB) $@ + +.cc.u: $(PHDR) + cxx -j $< -I$(INCLUDE) $(CFLAGS) + +# if the header files change, recompile +$(POBJ): $(PHDR) +$(PUBJ): $(PHDR) +$(OBJ): $(PHDR) +$(UBJ): $(PHDR) + +$(TARGET): $(SRC) $(OBJ) $(HDR) $(LIBS) $(MNEMLIB) + $(PURE) $(CXX) $(CFLAGS) $(LDFLAGS) -o $@ $(OBJ) $(LIBS) $(MNEMLIB) -lm + +# optimize (DECstations and Alphas only: uses u-code) +$(TARGETu): $(SRC) $(UBJ) $(HDR) $(LIBS:.a=.b) + cxx -O3 -Olimit 1000 $(XCFLAGS) $(LDFLAGS) -o $@ $(UBJ) $(BLIBS) -lm + +lint: llib-l$(P).ln + +llib-l$(P).ln: $(PSRC) $(PHDR) + lint $(LINTFLAGS) $(LINTSWITCH)$(P) -I$(INCLUDE) $(PSRC) + +lintpgm: lint + lint $(LINTFLAGS) -I$(INCLUDE) $(SRC) $(LINTLIBS) + +tags: $(PSRC) $(PHDR) + ctags $(PSRC) $(PHDR) + +all: lib$(P).a lib$(P).b llib-l$(P).ln tags + +programs: $(TARGET) $(TARGETu) lintpgm + +clean: + rm -f *.o *.u mon.out gmon.out *.pixie *.Addrs *.Counts mnem.* \ + .pure core *.warnings + +distclean: clean + rm -f $(TARGET) $(TARGETu) lib*.a lib$(P).b llib-l$(P).ln \ + *.bak *~ tags .gdb_history *.qv *.qx diff --git a/src/adapters/IntermediateRepresentationAdapter.h b/src/adapters/ExplicitModelAdapter.h similarity index 93% rename from src/adapters/IntermediateRepresentationAdapter.h rename to src/adapters/ExplicitModelAdapter.h index 6c5774bfc..d056f6849 100644 --- a/src/adapters/IntermediateRepresentationAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -5,8 +5,8 @@ * Author: Christian Dehnert */ -#ifndef STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_ -#define STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_ +#ifndef STORM_IR_EXPLICITMODELADAPTER_H_ +#define STORM_IR_EXPLICITMODELADAPTER_H_ #include "src/storage/SparseMatrix.h" #include "src/utility/Settings.h" @@ -49,7 +49,7 @@ public: } }; -class IntermediateRepresentationAdapter { +class ExplicitModelAdapter { public: template static storm::storage::SparseMatrix* toSparseMatrix(storm::ir::Program const& program) { @@ -89,12 +89,12 @@ public: StateType* initialState = getNewState(numberOfBooleanVariables, numberOfIntegerVariables); for (uint_fast64_t i = 0; i < numberOfBooleanVariables; ++i) { - bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(*initialState); + bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(initialState); std::get<0>(*initialState)[i] = initialValue; } for (uint_fast64_t i = 0; i < numberOfIntegerVariables; ++i) { - int_fast64_t initialValue = integerVariables[i].getInitialValue()->getValueAsInt(*initialState); + int_fast64_t initialValue = integerVariables[i].getInitialValue()->getValueAsInt(initialState); std::get<1>(*initialState)[i] = initialValue; } @@ -124,7 +124,7 @@ public: storm::ir::Command const& command = module.getCommand(j); // Check if this command is enabled in the current state. - if (command.getGuard()->getValueAsBool(*currentState)) { + if (command.getGuard()->getValueAsBool(currentState)) { hasTransition = true; std::unordered_map stateToProbabilityMap; std::queue statesToDelete; @@ -135,12 +135,12 @@ public: // std::cout << "took state: " << newState->first << "/" << newState->second << std::endl; std::map const& booleanAssignmentMap = update.getBooleanAssignments(); for (auto assignedVariable : booleanAssignmentMap) { - setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(*currentState)); + setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(currentState)); } std::map const& integerAssignmentMap = update.getIntegerAssignments(); for (auto assignedVariable : integerAssignmentMap) { // std::cout << "evaluting " << assignedVariable.second.getExpression()->toString() << " as " << assignedVariable.second.getExpression()->getValueAsInt(*currentState) << std::endl; - setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(*currentState)); + setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(currentState)); } // std::cout << "applied: " << update.toString() << std::endl; @@ -148,10 +148,10 @@ public: auto probIt = stateToProbabilityMap.find(newState); if (probIt != stateToProbabilityMap.end()) { - stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(*currentState); + stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(currentState); } else { ++totalNumberOfTransitions; - stateToProbabilityMap[newState] = update.getLikelihoodExpression()->getValueAsDouble(*currentState); + stateToProbabilityMap[newState] = update.getLikelihoodExpression()->getValueAsDouble(currentState); } auto it = stateToIndexMap.find(newState); @@ -204,7 +204,7 @@ public: storm::ir::Command const& command = module.getCommand(j); // Check if this command is enabled in the current state. - if (command.getGuard()->getValueAsBool(*currentState)) { + if (command.getGuard()->getValueAsBool(currentState)) { hasTransition = true; std::map stateIndexToProbabilityMap; for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { @@ -214,11 +214,11 @@ public: std::map const& booleanAssignmentMap = update.getBooleanAssignments(); for (auto assignedVariable : booleanAssignmentMap) { - setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(*currentState)); + setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(currentState)); } std::map const& integerAssignmentMap = update.getIntegerAssignments(); for (auto assignedVariable : integerAssignmentMap) { - setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(*currentState)); + setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(currentState)); } uint_fast64_t targetIndex = (*stateToIndexMap.find(newState)).second; @@ -226,9 +226,9 @@ public: auto probIt = stateIndexToProbabilityMap.find(targetIndex); if (probIt != stateIndexToProbabilityMap.end()) { - stateIndexToProbabilityMap[targetIndex] += update.getLikelihoodExpression()->getValueAsDouble(*currentState); + stateIndexToProbabilityMap[targetIndex] += update.getLikelihoodExpression()->getValueAsDouble(currentState); } else { - stateIndexToProbabilityMap[targetIndex] = update.getLikelihoodExpression()->getValueAsDouble(*currentState); + stateIndexToProbabilityMap[targetIndex] = update.getLikelihoodExpression()->getValueAsDouble(currentState); } } @@ -275,9 +275,8 @@ private: } }; -} +} // namespace adapters -} +} // namespace storm - -#endif /* STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_ */ +#endif /* STORM_IR_EXPLICITMODELADAPTER_H_ */ diff --git a/src/ir/IntegerVariable.cpp b/src/ir/IntegerVariable.cpp index 8374551a9..b07316b65 100644 --- a/src/ir/IntegerVariable.cpp +++ b/src/ir/IntegerVariable.cpp @@ -27,6 +27,17 @@ IntegerVariable::IntegerVariable(uint_fast64_t index, std::string variableName, } } +// Return lower bound for variable. +std::shared_ptr IntegerVariable::getLowerBound() const { + return this->lowerBound; +} + +// Return upper bound for variable. +std::shared_ptr IntegerVariable::getUpperBound() const { + return this->upperBound; +} + + // Build a string representation of the variable. std::string IntegerVariable::toString() const { std::stringstream result; diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h index 86e2dfc1b..a05ef1d7e 100644 --- a/src/ir/IntegerVariable.h +++ b/src/ir/IntegerVariable.h @@ -37,6 +37,18 @@ public: */ IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue = std::shared_ptr(nullptr)); + /*! + * Retrieves the lower bound for this integer variable. + * @returns the lower bound for this integer variable. + */ + std::shared_ptr getLowerBound() const; + + /*! + * Retrieves the upper bound for this integer variable. + * @returns the upper bound for this integer variable. + */ + std::shared_ptr getUpperBound() const; + /*! * Retrieves a string representation of this variable. * @returns a string representation of this variable. diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h index 3e228d5cf..27704b64b 100644 --- a/src/ir/expressions/BaseExpression.h +++ b/src/ir/expressions/BaseExpression.h @@ -37,7 +37,7 @@ public: } - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { if (type != int_) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" << this->getTypeName() << "' as 'int'."; @@ -46,7 +46,7 @@ public: << this->getTypeName() << " because evaluation implementation is missing."; } - virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { if (type != bool_) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" << this->getTypeName() << "' as 'bool'."; @@ -55,7 +55,7 @@ public: << this->getTypeName() << " because evaluation implementation is missing."; } - virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { if (type != bool_) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" << this->getTypeName() << "' as 'double'."; diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h index 957c08658..c7b5a0bdc 100644 --- a/src/ir/expressions/BinaryBooleanFunctionExpression.h +++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h @@ -31,7 +31,7 @@ public: } - virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { bool resultLeft = left->getValueAsBool(variableValues); bool resultRight = right->getValueAsBool(variableValues); switch(functionType) { diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h index 7a76320a9..0d710e785 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.h +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h @@ -28,7 +28,7 @@ public: } - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { if (this->getType() != int_) { BaseExpression::getValueAsInt(variableValues); } @@ -45,7 +45,7 @@ public: } } - virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { if (this->getType() != double_) { BaseExpression::getValueAsDouble(variableValues); } diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h index fe07f0749..83556fa8f 100644 --- a/src/ir/expressions/BinaryRelationExpression.h +++ b/src/ir/expressions/BinaryRelationExpression.h @@ -28,7 +28,7 @@ public: } - virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { int_fast64_t resultLeft = left->getValueAsInt(variableValues); int_fast64_t resultRight = right->getValueAsInt(variableValues); switch(relationType) { diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h index 58204fee4..c4a168838 100644 --- a/src/ir/expressions/BooleanConstantExpression.h +++ b/src/ir/expressions/BooleanConstantExpression.h @@ -29,7 +29,7 @@ public: } - virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { if (!defined) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Boolean constant '" << this->getConstantName() << "' is undefined."; diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h index b7ee88997..55027d6cc 100644 --- a/src/ir/expressions/BooleanLiteral.h +++ b/src/ir/expressions/BooleanLiteral.h @@ -28,7 +28,7 @@ public: } - virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { return value; } diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h index c852329c1..573aeffd3 100644 --- a/src/ir/expressions/DoubleConstantExpression.h +++ b/src/ir/expressions/DoubleConstantExpression.h @@ -26,7 +26,7 @@ public: } - virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { if (!defined) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Double constant '" << this->getConstantName() << "' is undefined."; diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h index 2679a7a5d..4963ff9c2 100644 --- a/src/ir/expressions/DoubleLiteral.h +++ b/src/ir/expressions/DoubleLiteral.h @@ -30,7 +30,7 @@ public: } - virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { return value; } diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h index 250b085a3..7cb25afd9 100644 --- a/src/ir/expressions/IntegerConstantExpression.h +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -26,7 +26,7 @@ public: } - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { if (!defined) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Integer constant '" << this->getConstantName() << "' is undefined."; diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h index c5cd06119..e5883e358 100644 --- a/src/ir/expressions/IntegerLiteral.h +++ b/src/ir/expressions/IntegerLiteral.h @@ -28,7 +28,7 @@ public: } - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { return value; } diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h index e0fae6c5b..9a924d7da 100644 --- a/src/ir/expressions/UnaryBooleanFunctionExpression.h +++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h @@ -28,7 +28,7 @@ public: } - virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { bool resultChild = child->getValueAsBool(variableValues); switch(functionType) { case NOT: return !resultChild; break; diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h index 8b746c1c7..a4498aa08 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.h +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h @@ -28,7 +28,7 @@ public: } - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { if (this->getType() != int_) { BaseExpression::getValueAsInt(variableValues); } @@ -41,7 +41,7 @@ public: } } - virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { if (this->getType() != double_) { BaseExpression::getValueAsDouble(variableValues); } diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h index 47b2087cd..5ef38313c 100644 --- a/src/ir/expressions/VariableExpression.h +++ b/src/ir/expressions/VariableExpression.h @@ -32,23 +32,33 @@ public: return variableName; } - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const& variableValues) const { + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { if (this->getType() != int_) { BaseExpression::getValueAsInt(variableValues); } - return variableValues.second[index]; + if (variableValues != nullptr) { + return variableValues->second[index]; + } else { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression" + << " involving variables without variable values."; + } } - virtual bool getValueAsBool(std::pair, std::vector> const& variableValues) const { + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { if (this->getType() != bool_) { BaseExpression::getValueAsBool(variableValues); } - return variableValues.first[index]; + if (variableValues != nullptr) { + return variableValues->first[index]; + } else { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression" + << " involving variables without variable values."; + } } - virtual double getValueAsDouble(std::pair, std::vector> const& variableValues) const { + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { if (this->getType() != double_) { BaseExpression::getValueAsDouble(variableValues); } diff --git a/src/storm.cpp b/src/storm.cpp index b34529d94..35b25459d 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -36,7 +36,8 @@ #include "log4cplus/fileappender.h" #include "src/parser/PrismParser.h" -#include "src/adapters/IntermediateRepresentationAdapter.h" +#include "src/adapters/ExplicitModelAdapter.h" +#include "src/adapters/SymbolicModelAdapter.h" #include "src/exceptions/InvalidSettingsException.h" @@ -245,9 +246,8 @@ int main(const int argc, const char* argv[]) { storm::parser::PrismParser parser; std::shared_ptr program = parser.parseFile("test.input"); - storm::storage::SparseMatrix* result = storm::adapters::IntermediateRepresentationAdapter::toSparseMatrix(*program); - // result->print(); - delete result; + storm::adapters::SymbolicModelAdapter symbolicAdapter; + symbolicAdapter.toMTBDD(*program); cleanUp(); return 0;