diff --git a/CMakeLists.txt b/CMakeLists.txt index 4af9a135b..19b9c507f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -241,7 +241,8 @@ include_directories("${PROJECT_BINARY_DIR}/include") file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h) file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/*/*.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) -set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE}") +file(GLOB_RECURSE STORM_PARAMETRIC_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/stormParametric.cpp) +set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE};${STORM_PARAMETRIC_MAIN_FILE};") file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp) file(GLOB STORM_FORMULA_FILES ${PROJECT_SOURCE_DIR}/src/formula/*.h ${PROJECT_SOURCE_DIR}/src/formula/*.cpp) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index c1569be9f..cc2c14c89 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -369,7 +369,7 @@ namespace storm { } // Check that the resulting distribution is in fact a distribution. - LOG_THROW(!storm::utility::isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "'."); + LOG_THROW(storm::utility::isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (sum = " << probabilitySum << ")."); } } @@ -477,7 +477,7 @@ namespace storm { // Check that the resulting distribution is in fact a distribution. if (!storm::utility::isOne(probabilitySum)) { LOG4CPLUS_ERROR(logger, "Sum of update probabilities do not some to one for some command."); - throw storm::exceptions::WrongFormatException() << "Sum of update probabilities do not some to one for some command."; + throw storm::exceptions::WrongFormatException() << "Sum of update probabilities do sum to " << probabilitySum << " to one for some command."; } // Dispose of the temporary maps. diff --git a/src/modelchecker/reachability/DirectEncoding.h b/src/modelchecker/reachability/DirectEncoding.h new file mode 100644 index 000000000..87a151ae4 --- /dev/null +++ b/src/modelchecker/reachability/DirectEncoding.h @@ -0,0 +1,74 @@ +/** + * @file: DirectEncoding.h + * @author: Sebastian Junges + * + * @since April 8, 2014 + */ + +#pragma once + +#ifdef STORM_HAVE_CARL +#include + +namespace storm +{ + namespace modelchecker + { + namespace reachability + { + class DirectEncoding + { + public: + template + void encodeAsSmt2(const storm::models::Dtmc& model, storm::storage::BitVector finalStates, T threshold, bool lessequal = true) + { + carl::io::WriteTosmt2Stream smt2; + uint_fast64_t nrStates = model.getNumberOfStates(); + carl::VariablePool& vpool = carl::VariablePool::getInstance(); + std::vector stateVars; + for(uint_fast64_t state = 0; state < nrStates; ++state) + { + carl::Variable stateVar = vpool.getFreshVariable("s_" + std::to_string(state)); + stateVars.push_back(stateVar); + smt2 << carl::io::smt2flag::ASSERT; + smt2 << carl::io::smt2node::AND; + smt2 << carl::Constraint(Polynomial(stateVar), carl::CompareRelation::GE); + smt2 << carl::Constraint(Polynomial(stateVar) - Polynomial(1), carl::CompareRelation::LE); + smt2 << carl::io::smt2node::CLOSENODE; + } + smt2 << carl::io::smt2flag::ASSERT; + smt2 << carl::io::smt2node::AND; + smt2.setAutomaticLineBreaks(true); + Polynomial finalStateReachSum; + for(uint_fast64_t state = 0; state < nrStates; ++state) + { + if(finalStates[state]) + { + smt2 << carl::Constraint(Polynomial(stateVars[state]) - Polynomial(1), carl::CompareRelation::EQ); + finalStateReachSum += stateVars[state]; + } + else + { + Polynomial reachpropPol(0); + for(auto const& transition : model.getRows(state)) + { + reachpropPol += stateVars[transition.first] * transition.second; + } + smt2 << carl::Constraint(reachpropPol - stateVars[state], carl::CompareRelation::EQ); + } + } + smt2 << carl::io::smt2node::CLOSENODE; + smt2 << carl::io::smt2flag::ASSERT; + + carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LE : carl::CompareRelation::GE; + smt2 << carl::Constraint(finalStateReachSum - threshold, thresholdRelation); + smt2 << carl::io::smt2flag::CHECKSAT; + std::cout << smt2; + + } + }; + } + } +} + +#endif \ No newline at end of file diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index f9a3e12a5..e86c85923 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -314,7 +314,7 @@ private: LOG4CPLUS_ERROR(logger, "Row " << row << " is a deadlock (sum == " << sum << ")."); return false; } - if (storm::utility::isOne(sum)) { + if (!storm::utility::isOne(sum)) { LOG4CPLUS_ERROR(logger, "Row " << row << " has sum " << sum << "."); return false; } diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h index 99d847555..b5ff55e6d 100644 --- a/src/storage/expressions/ExpressionEvaluation.h +++ b/src/storage/expressions/ExpressionEvaluation.h @@ -10,6 +10,11 @@ #include "ExpressionVisitor.h" #include "BaseExpression.h" +#include "IfThenElseExpression.h" +#include "DoubleConstantExpression.h" +#include "DoubleLiteralExpression.h" + +#include "src/storage/parameters.h" namespace storm { namespace expressions { @@ -19,6 +24,12 @@ namespace expressions { { typedef int type; }; + + template<> + struct StateType + { + typedef carl::Variable type; + }; template class ExpressionEvaluationVisitor : public ExpressionVisitor @@ -30,19 +41,62 @@ namespace expressions { } - virtual void visit(IfThenElseExpression const* expression) = 0; - virtual void visit(BinaryBooleanFunctionExpression const* expression) = 0; - virtual void visit(BinaryNumericalFunctionExpression const* expression) = 0; - virtual void visit(BinaryRelationExpression const* expression) = 0; - virtual void visit(BooleanConstantExpression const* expression) = 0; - virtual void visit(DoubleConstantExpression const* expression) = 0; - virtual void visit(IntegerConstantExpression const* expression) = 0; - virtual void visit(VariableExpression const* expression) = 0; - virtual void visit(UnaryBooleanFunctionExpression const* expression) = 0; - virtual void visit(UnaryNumericalFunctionExpression const* expression) = 0; - virtual void visit(BooleanLiteralExpression const* expression) = 0; - virtual void visit(IntegerLiteralExpression const* expression) = 0; - virtual void visit(DoubleLiteralExpression const* expression) = 0; + virtual ~ExpressionEvaluationVisitor() {} + + virtual void visit(IfThenElseExpression const* expression) + { + bool condititionValue = expression->getCondition()->evaluateAsBool(); + + } + + virtual void visit(BinaryBooleanFunctionExpression const* expression) + { + + } + virtual void visit(BinaryNumericalFunctionExpression const* expression) + { + + } + virtual void visit(BinaryRelationExpression const* expression) + { + + } + virtual void visit(BooleanConstantExpression const* expression) + { + + } + virtual void visit(DoubleConstantExpression const* expression) + { + + } + virtual void visit(IntegerConstantExpression const* expression) + { + + } + virtual void visit(VariableExpression const* expression) + { + + } + virtual void visit(UnaryBooleanFunctionExpression const* expression) + { + + } + virtual void visit(UnaryNumericalFunctionExpression const* expression) + { + + } + virtual void visit(BooleanLiteralExpression const* expression) + { + + } + virtual void visit(IntegerLiteralExpression const* expression) + { + + } + virtual void visit(DoubleLiteralExpression const* expression) + { + + } const T& value() const { @@ -64,11 +118,11 @@ namespace expressions { } - T evaluate(Expression const& expr, storm::expressions::SimpleValuation const*) + T evaluate(Expression const& expr, storm::expressions::SimpleValuation const* val) { ExpressionEvaluationVisitor::type>* visitor = new ExpressionEvaluationVisitor::type>(&mState); - expr.getBaseExpression().accept(visitor); - T result = visitor->value(); + //expr.getBaseExpression().accept(visitor); + T result = T(mpq_class(expr.evaluateAsDouble(val))); delete visitor; return result; } diff --git a/src/storm.cpp b/src/storm.cpp index c7b40247a..bb175acbb 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -59,7 +59,7 @@ log4cplus::Logger logger; #include "src/parser/PrismParser.h" #include "src/adapters/ExplicitModelAdapter.h" // #include "src/adapters/SymbolicModelAdapter.h" - +#include "stormParametric.h" #include "src/exceptions/InvalidSettingsException.h" // Includes for the linked libraries and versions header @@ -535,73 +535,85 @@ int main(const int argc, const char* argv[]) { std::string const& programFile = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString(); std::string const& constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString(); storm::prism::Program program = storm::parser::PrismParser::parse(programFile); - std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program, constants); - model->printModelInformationToStream(std::cout); - if (s->isSet("mincmd")) { - if (model->getType() != storm::models::MDP) { - LOG4CPLUS_ERROR(logger, "Minimal command counterexample generation is only supported for models of type MDP."); - throw storm::exceptions::InternalTypeErrorException() << "Minimal command counterexample generation is only supported for models of type MDP."; - } - - std::shared_ptr> mdp = model->as>(); - - // Determine whether we are required to use the MILP-version or the SAT-version. - bool useMILP = s->getOptionByLongName("mincmd").getArgumentByName("method").getValueAsString() == "milp"; - - // Now parse the property file and receive the list of parsed formulas. - std::string const& propertyFile = s->getOptionByLongName("mincmd").getArgumentByName("propertyFile").getValueAsString(); - std::list*> formulaList = storm::parser::PrctlFileParser(propertyFile); - - // Now generate the counterexamples for each formula. - for (storm::property::prctl::AbstractPrctlFormula* formulaPtr : formulaList) { - if (useMILP) { - storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formulaPtr); - } else { - // storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, constants, *mdp, formulaPtr); + if(s->isSet("parameters")) + { + storm::storm_parametric(constants, program); + } + else + { + std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program, constants); + model->printModelInformationToStream(std::cout); + + if (s->isSet("mincmd")) { + if (model->getType() != storm::models::MDP) { + LOG4CPLUS_ERROR(logger, "Minimal command counterexample generation is only supported for models of type MDP."); + throw storm::exceptions::InternalTypeErrorException() << "Minimal command counterexample generation is only supported for models of type MDP."; + } + + std::shared_ptr> mdp = model->as>(); + + // Determine whether we are required to use the MILP-version or the SAT-version. + bool useMILP = s->getOptionByLongName("mincmd").getArgumentByName("method").getValueAsString() == "milp"; + + // Now parse the property file and receive the list of parsed formulas. + std::string const& propertyFile = s->getOptionByLongName("mincmd").getArgumentByName("propertyFile").getValueAsString(); + std::list*> formulaList = storm::parser::PrctlFileParser(propertyFile); + + // Now generate the counterexamples for each formula. + for (storm::property::prctl::AbstractPrctlFormula* formulaPtr : formulaList) { + if (useMILP) { + storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formulaPtr); + } else { + // storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, constants, *mdp, formulaPtr); + } + + // Once we are done with the formula, delete it. + delete formulaPtr; + } + } else if (s->isSet("prctl")) { + // Determine which engine is to be used to choose the right model checker. + LOG4CPLUS_DEBUG(logger, s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString()); + + // Depending on the model type, the appropriate model checking procedure is chosen. + storm::modelchecker::prctl::AbstractModelChecker* modelchecker = nullptr; + + switch (model->getType()) { + case storm::models::DTMC: + LOG4CPLUS_INFO(logger, "Model is a DTMC."); + modelchecker = createPrctlModelChecker(*model->as>()); + checkPrctlFormulae(*modelchecker); + break; + case storm::models::MDP: + LOG4CPLUS_INFO(logger, "Model is an MDP."); + modelchecker = createPrctlModelChecker(*model->as>()); + checkPrctlFormulae(*modelchecker); + break; + case storm::models::CTMC: + LOG4CPLUS_INFO(logger, "Model is a CTMC."); + LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); + break; + case storm::models::CTMDP: + LOG4CPLUS_INFO(logger, "Model is a CTMDP."); + LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); + break; + case storm::models::MA: + LOG4CPLUS_INFO(logger, "Model is a Markov automaton."); + break; + case storm::models::Unknown: + default: + LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); + break; + } + + if (modelchecker != nullptr) { + delete modelchecker; } - - // Once we are done with the formula, delete it. - delete formulaPtr; } - } else if (s->isSet("prctl")) { - // Determine which engine is to be used to choose the right model checker. - LOG4CPLUS_DEBUG(logger, s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString()); - - // Depending on the model type, the appropriate model checking procedure is chosen. - storm::modelchecker::prctl::AbstractModelChecker* modelchecker = nullptr; - - switch (model->getType()) { - case storm::models::DTMC: - LOG4CPLUS_INFO(logger, "Model is a DTMC."); - modelchecker = createPrctlModelChecker(*model->as>()); - checkPrctlFormulae(*modelchecker); - break; - case storm::models::MDP: - LOG4CPLUS_INFO(logger, "Model is an MDP."); - modelchecker = createPrctlModelChecker(*model->as>()); - checkPrctlFormulae(*modelchecker); - break; - case storm::models::CTMC: - LOG4CPLUS_INFO(logger, "Model is a CTMC."); - LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); - break; - case storm::models::CTMDP: - LOG4CPLUS_INFO(logger, "Model is a CTMDP."); - LOG4CPLUS_ERROR(logger, "The selected model type is not supported."); - break; - case storm::models::MA: - LOG4CPLUS_INFO(logger, "Model is a Markov automaton."); - break; - case storm::models::Unknown: - default: - LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); - break; - } - - if (modelchecker != nullptr) { - delete modelchecker; - } + else if (s->isSet("reachability")) + { + LOG4CPLUS_ERROR(logger, "Only supported for parameteric systems."); + } } } diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp new file mode 100644 index 000000000..044cbcc9e --- /dev/null +++ b/src/stormParametric.cpp @@ -0,0 +1,20 @@ +#include "stormParametric.h" +#include "adapters/ExplicitModelAdapter.h" + +namespace storm +{ + + +void ParametricStormEntryPoint::createModel() +{ + std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(mProgram, mConstants); + model->printModelInformationToStream(std::cout); +} + +void storm_parametric(const std::string& constants, const storm::prism::Program& program) +{ + ParametricStormEntryPoint entry(constants, program); + entry.createModel(); +} + +} diff --git a/src/stormParametric.h b/src/stormParametric.h new file mode 100644 index 000000000..e58b45113 --- /dev/null +++ b/src/stormParametric.h @@ -0,0 +1,32 @@ + + + +#pragma once +#include "storage/prism/Program.h" +#include "models/AbstractModel.h" +#include "storage/parameters.h" + +namespace storm +{ + class ParametricStormEntryPoint + { + private: + std::string const& mConstants; + storm::prism::Program const& mProgram; + std::shared_ptr> mModel; + public: + ParametricStormEntryPoint(std::string const& constants, storm::prism::Program const& program) : + mConstants(constants), + mProgram(program) + { + + } + + void createModel(); + + virtual ~ParametricStormEntryPoint() {} + + }; + void storm_parametric(std::string const& constants, storm::prism::Program const&); +} + diff --git a/src/utility/constants.h b/src/utility/constants.h index 2bc527d93..8ec689c8e 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -206,7 +206,7 @@ inline storm::storage::LabeledValues constantInfinity() { template inline bool isOne(T sum) { - return (sum-T(1)).isZero(); + return sum == T(1); } template<>