From 5817fe50b6e2eb3a55f4b3d3df39b5bd92307676 Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 19 Sep 2014 13:06:31 +0200 Subject: [PATCH] post merge fixes Former-commit-id: 2f9bc01abd64c97dbaede064bcd4d5ec2f3b1ec6 --- src/adapters/ExplicitModelAdapter.h | 2 +- src/adapters/extendedCarl.h | 6 + src/exceptions/ExceptionMacros.h | 9 +- src/extensions/parameters/main.cpp | 22 ++ src/parser/DeterministicModelParser.cpp | 2 +- .../DeterministicSparseTransitionParser.cpp | 37 ++- .../DeterministicSparseTransitionParser.h | 4 +- src/parser/ReadValues.h | 4 +- .../expressions/ExpressionEvaluation.h | 23 +- src/storm.cpp | 6 +- src/stormParametric.cpp | 296 +++++++++--------- src/stormParametric.h | 66 ++-- ...eterministicSparseTransitionParserTest.cpp | 24 +- 13 files changed, 260 insertions(+), 241 deletions(-) create mode 100644 src/extensions/parameters/main.cpp diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 97de75fb5..ea12d02c2 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -666,7 +666,7 @@ namespace storm { // Build the transition and reward matrices. storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); - modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder); + modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder, eval); // Finalize the resulting matrices. modelComponents.transitionMatrix = transitionMatrixBuilder.build(); diff --git a/src/adapters/extendedCarl.h b/src/adapters/extendedCarl.h index 2b306580e..d611e14bc 100644 --- a/src/adapters/extendedCarl.h +++ b/src/adapters/extendedCarl.h @@ -8,9 +8,13 @@ #ifndef STORM_ADAPTERS_EXTENDEDCARL_H_ #define STORM_ADAPTERS_EXTENDEDCARL_H_ + #include #include +#include +#include +#undef LOG_ASSERT namespace carl { template @@ -28,4 +32,6 @@ inline size_t hash_value(carl::RationalFunction const& f) } +#include "src/exceptions/ExceptionMacros.h" + #endif \ No newline at end of file diff --git a/src/exceptions/ExceptionMacros.h b/src/exceptions/ExceptionMacros.h index bbf2f4f36..328b661bb 100644 --- a/src/exceptions/ExceptionMacros.h +++ b/src/exceptions/ExceptionMacros.h @@ -1,5 +1,3 @@ -#ifndef STORM_EXCEPTIONS_EXCEPTIONMACROS_H_ -#define STORM_EXCEPTIONS_EXCEPTIONMACROS_H_ #include @@ -7,7 +5,7 @@ #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; - +#undef LOG_ASSERT #ifndef NDEBUG #define LOG_ASSERT(cond, message) \ { \ @@ -16,6 +14,7 @@ extern log4cplus::Logger logger; assert(cond); \ } \ } while (false) +#undef LOG_DEBUG #define LOG_DEBUG(message) \ { \ LOG4CPLUS_DEBUG(logger, message); \ @@ -24,7 +23,7 @@ extern log4cplus::Logger logger; #define LOG_ASSERT(cond, message) /* empty */ #define LOG_DEBUG(message) /* empty */ #endif - +#undef LOG_THROW #define LOG_THROW(cond, exception, message) \ { \ if (!(cond)) { \ @@ -32,5 +31,3 @@ LOG4CPLUS_ERROR(logger, message); \ throw exception() << message; \ } \ } while (false) - -#endif /* STORM_EXCEPTIONS_EXCEPTIONMACROS_H_ */ \ No newline at end of file diff --git a/src/extensions/parameters/main.cpp b/src/extensions/parameters/main.cpp new file mode 100644 index 000000000..426b2fab9 --- /dev/null +++ b/src/extensions/parameters/main.cpp @@ -0,0 +1,22 @@ +// +//int main(const int argc, const char* argv[]) { +// // Print an information header. +// //printHeader(argc, argv); +// +// // Initialize the logging engine and perform other initalizations. +// initializeLogger(); +// setUp(); +// +// // Program Translation Time Measurement, Start +// std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now(); +// +// // First, we build the model using the given symbolic model description and constant definitions. +// 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); +// +// // Program Translation Time Measurement, End +// std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now(); +// std::cout << "Parsing and translating the Symbolic Input took " << std::chrono::duration_cast(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl; +// storm_parametric(constants, program); +//} \ No newline at end of file diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 379858b24..b2a82bc91 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -20,7 +20,7 @@ namespace storm { DeterministicModelParser::Result DeterministicModelParser::parseDeterministicModel(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename, std::string const & transitionRewardFilename) { // Parse the transitions. - storm::storage::SparseMatrix transitions(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionsFilename))); + storm::storage::SparseMatrix transitions(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionsFilename))); uint_fast64_t stateCount = transitions.getColumnCount(); diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 1aec39978..9dce8bbb1 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -94,7 +94,7 @@ namespace storm { storm::storage::SparseMatrixBuilder resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries); uint_fast64_t lastRow = 0; - DeterministicTransitionEntry trans; + DeterministicTransitionEntry trans; bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); bool hadDeadlocks = false; bool rowHadDiagonalEntry = false; @@ -113,11 +113,11 @@ namespace storm { } } else { // Read first row and add self-loops if necessary. - char const* tmp; - row = checked_strtol(buf, &tmp); - if (row > 0) { - for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) { + readNextTransition(&buf, &trans); + + if (trans.row > 0) { + for (uint_fast64_t skippedRow = 0; skippedRow < trans.row; ++skippedRow) { hadDeadlocks = true; if (fixDeadlocks) { resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); @@ -128,6 +128,8 @@ namespace storm { } } } + addTransitionToMatrix(trans, &resultMatrix); + while (buf[0] != '\0') { @@ -136,7 +138,7 @@ namespace storm { // Test if we moved to a new row. // Handle all incomplete or skipped rows. - if (lastRow != row) { + if (lastRow != trans.row) { if (!rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing) { resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); @@ -147,7 +149,7 @@ namespace storm { // No increment for lastRow. rowHadDiagonalEntry = true; } - for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { + for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < trans.row; ++skippedRow) { hadDeadlocks = true; if (fixDeadlocks) { resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); @@ -157,26 +159,25 @@ namespace storm { // Before throwing the appropriate exception we will give notice of all deadlock states. } } - lastRow = row; + lastRow = trans.row; rowHadDiagonalEntry = false; } - if (col == row) { + if (trans.col == trans.row) { rowHadDiagonalEntry = true; } - if (col > row && !rowHadDiagonalEntry) { + if (trans.col > trans.row && !rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(row, row, storm::utility::constantZero()); - LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); + resultMatrix.addNextValue(trans.row, trans.row, storm::utility::constantZero()); + LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << trans.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."); + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << trans.row << " has no transition to itself."); } rowHadDiagonalEntry = true; } - resultMatrix.addNextValue(row, col, val); - buf = trimWhitespaces(buf); + addTransitionToMatrix(trans, &resultMatrix); } if (!rowHadDiagonalEntry) { @@ -290,7 +291,7 @@ namespace storm { } template - void DeterministicSparseTransitionParser::readNextTransition(char** buf, DeterministicTransitionEntry* trans) + void DeterministicSparseTransitionParser::readNextTransition(char const** buf, DeterministicTransitionEntry* trans) { trans->row = checked_strtol(*buf, buf); trans->col = checked_strtol(*buf, buf); @@ -307,7 +308,7 @@ namespace storm { mat->addNextValue(trans.row, trans.col, trans.val); } - char* DeterministicSparseTransitionParser::skipFormatHint(char* buf) + char const* DeterministicSparseTransitionParser::skipFormatHint(char const* buf) { // Skip the format hint if it is there. buf = trimWhitespaces(buf); @@ -318,6 +319,8 @@ namespace storm { return buf; } + template storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename); + template storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix const & transitionMatrix); } // namespace parser } // namespace storm diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index 75820bd03..5c5b2c315 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -97,13 +97,13 @@ namespace storm { /* */ template - static void readNextTransition(char** buf, DeterministicTransitionEntry* trans ); + static void readNextTransition(char const** buf, DeterministicTransitionEntry* trans ); template static void addTransitionToMatrix(DeterministicTransitionEntry const& trans, storm::storage::SparseMatrixBuilder* mat); - static char* skipFormatHint(char*); + static char const* skipFormatHint(char const*); }; diff --git a/src/parser/ReadValues.h b/src/parser/ReadValues.h index dad3b42b2..01359ff33 100644 --- a/src/parser/ReadValues.h +++ b/src/parser/ReadValues.h @@ -9,10 +9,10 @@ namespace storm { template - T readValue(char* buf); + T readValue(char const* buf); template<> - double readValue(char* buf) + double readValue(char const* buf) { return utility::cstring::checked_strtod(buf, &buf); } diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h index e246833ff..3bf0568c5 100644 --- a/src/storage/expressions/ExpressionEvaluation.h +++ b/src/storage/expressions/ExpressionEvaluation.h @@ -11,11 +11,9 @@ #include "ExpressionVisitor.h" #include "BaseExpression.h" #include "IfThenElseExpression.h" -#include "DoubleConstantExpression.h" #include "DoubleLiteralExpression.h" #include "BinaryNumericalFunctionExpression.h" -#include "carl/numbers/DecimalStringToRational.h" #include "src/storage/parameters.h" #include "IntegerLiteralExpression.h" #include "BinaryExpression.h" @@ -94,32 +92,21 @@ namespace expressions { { std::cout << "br" << std::endl; } - virtual void visit(BooleanConstantExpression const* expression) + virtual void visit(VariableExpression const* expression) { - std::cout << "bc" << std::endl; - } - virtual void visit(DoubleConstantExpression const* expression) - { - auto it = mSharedState->find(expression->getConstantName()); + std::string const& varName= expression->getVariableName(); + auto it = mSharedState->find(varName); if(it != mSharedState->end()) { mValue = T(it->second); } else { - carl::Variable nVar = carl::VariablePool::getInstance().getFreshVariable(expression->getConstantName()); - mSharedState->emplace(expression->getConstantName(),nVar); + carl::Variable nVar = carl::VariablePool::getInstance().getFreshVariable(varName); + mSharedState->emplace(varName,nVar); mValue = T(nVar); } } - virtual void visit(IntegerConstantExpression const* expression) - { - std::cout << "ic" << std::endl; - } - virtual void visit(VariableExpression const* expression) - { - std::cout << "ve" << std::endl; - } virtual void visit(UnaryBooleanFunctionExpression const* expression) { std::cout << "ubf" << std::endl; diff --git a/src/storm.cpp b/src/storm.cpp index 56565304b..5e0b2d724 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -61,9 +61,10 @@ #include "src/parser/PrismParser.h" #include "src/adapters/ExplicitModelAdapter.h" // #include "src/adapters/SymbolicModelAdapter.h" -#include "stormParametric.h" #include "src/exceptions/InvalidSettingsException.h" +#include "storage/parameters.h" + @@ -221,11 +222,14 @@ 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); // Program Translation Time Measurement, End std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now(); std::cout << "Parsing and translating the Symbolic Input took " << std::chrono::duration_cast(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl; + + storm::modelchecker::reachability::SparseSccModelChecker modelChecker; storm::storage::BitVector trueStates(model->getNumberOfStates(), true); storm::storage::BitVector targetStates = model->getLabeledStates("observe0Greater1"); diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 93643dd8a..e9489e077 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -1,148 +1,148 @@ -#include -#include - -#include "stormParametric.h" -#include "adapters/ExplicitModelAdapter.h" -#include "utility/graph.h" -#include "modelchecker/reachability/DirectEncoding.h" -#include "storage/BitVector.h" -#include "storage/DeterministicTransition.h" - -using storm::storage::StateId; - -namespace storm -{ - - -void ParametricStormEntryPoint::createModel() -{ - mModel = storm::adapters::ExplicitModelAdapter::translateProgram(mProgram, mConstants); - mModel->printModelInformationToStream(std::cout); -} - -std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& label) -{ - - storm::storage::BitVector phiStates(mModel->getNumberOfStates(), true); - storm::storage::BitVector initStates = mModel->getInitialStates(); - storm::storage::BitVector targetStates = mModel->getLabeledStates(label); - - std::shared_ptr> dtmc = mModel->as>(); - // 1. make target states absorbing. - dtmc->makeAbsorbing(targetStates); - // 2. throw away anything which does not add to the reachability probability. - // 2a. remove non productive states - storm::storage::BitVector productiveStates = utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, targetStates); - // 2b. calculate set of states wich - storm::storage::BitVector almostSurelyReachingTargetStates = ~utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, ~productiveStates); - // 2c. Make such states also target states. - dtmc->makeAbsorbing(almostSurelyReachingTargetStates); - // 2d. throw away non reachable states - storm::storage::BitVector reachableStates = utility::graph::performProbGreater0(*dtmc, dtmc->getTransitionMatrix(), phiStates, initStates); - storm::storage::BitVector bv = productiveStates & reachableStates; - dtmc->getStateLabeling().addAtomicProposition("__targets__", targetStates | almostSurelyReachingTargetStates); - models::Dtmc subdtmc = dtmc->getSubDtmc(bv); - - phiStates = storm::storage::BitVector(subdtmc.getNumberOfStates(), true); - initStates = subdtmc.getInitialStates(); - targetStates = subdtmc.getLabeledStates("__targets__"); - storm::storage::BitVector deadlockStates(phiStates); - deadlockStates.set(subdtmc.getNumberOfStates()-1,false); - - // Search for states with only one non-deadlock successor. - std::map> chainedStates; - StateId nrStates = subdtmc.getNumberOfStates(); - StateId deadlockState = nrStates - 1; - for(StateId source = 0; source < nrStates - 1; ++source) - { - if(targetStates[source]) - { - continue; - } - storage::DeterministicTransition productiveTransition(nrStates); - for(auto const& transition : subdtmc.getRows(source)) - { - if(productiveTransition.targetState() == nrStates) - { - // first transition. - productiveTransition = transition; - } - else - { - // second transition - if(transition.first != deadlockState) - { - productiveTransition.targetState() = nrStates; - break; - } - } - } - if(productiveTransition.targetState() != nrStates) - { - chainedStates.emplace(source, productiveTransition); - } - } - storage::BitVector eliminatedStates(nrStates, false); - for(auto & chainedState : chainedStates) - { - assert(chainedState.first != chainedState.second.targetState()); - auto it = chainedStates.find(chainedState.second.targetState()); - if(it != chainedStates.end()) - { - //std::cout << "----------------------------" << std::endl; - //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; - //std::cout << it->first << " -- " << it->second.probability() << " --> " << it->second.targetState() << std::endl; - chainedState.second.targetState() = it->second.targetState(); - chainedState.second.probability() *= it->second.probability(); - //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; - //std::cout << "----------------------------" << std::endl; - chainedStates.erase(it); - eliminatedStates.set(it->first, true); - } - } - - - for(auto chainedState : chainedStates) - { - if(!eliminatedStates[chainedState.first]) - { - std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; - } - } - - storage::StronglyConnectedComponentDecomposition sccs(subdtmc); - std::cout << sccs << std::endl; - - modelchecker::reachability::DirectEncoding dec; - std::vector parameters; - for(auto constant : mProgram.getConstants()) - { - if(!constant.isDefined()) - { - std::cout << constant.getName() << std::endl; - carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName()); - assert(p != carl::Variable::NO_VARIABLE); - parameters.push_back(p); - } - } - return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates("__targets__"), mpq_class(1,2)); - -} - - -void storm_parametric(const std::string& constants, const storm::prism::Program& program) -{ - ParametricStormEntryPoint entry(constants, program); - entry.createModel(); - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - if(s->isSet("reachability")) - { - std::ofstream fstream("test.smt2"); - fstream << entry.reachabilityToSmt2(s->getOptionByLongName("reachability").getArgument(0).getValueAsString()); - fstream.close(); - } - - -} - -} +//#include +//#include +// +//#include "stormParametric.h" +//#include "adapters/ExplicitModelAdapter.h" +//#include "utility/graph.h" +//#include "modelchecker/reachability/DirectEncoding.h" +//#include "storage/BitVector.h" +//#include "storage/DeterministicTransition.h" +// +//using storm::storage::StateId; +// +//namespace storm +//{ +// +// +//void ParametricStormEntryPoint::createModel() +//{ +// mModel = storm::adapters::ExplicitModelAdapter::translateProgram(mProgram, mConstants); +// mModel->printModelInformationToStream(std::cout); +//} +// +//std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& label) +//{ +// +// storm::storage::BitVector phiStates(mModel->getNumberOfStates(), true); +// storm::storage::BitVector initStates = mModel->getInitialStates(); +// storm::storage::BitVector targetStates = mModel->getLabeledStates(label); +// +// std::shared_ptr> dtmc = mModel->as>(); +// // 1. make target states absorbing. +// dtmc->makeAbsorbing(targetStates); +// // 2. throw away anything which does not add to the reachability probability. +// // 2a. remove non productive states +// storm::storage::BitVector productiveStates = utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, targetStates); +// // 2b. calculate set of states wich +// storm::storage::BitVector almostSurelyReachingTargetStates = ~utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, ~productiveStates); +// // 2c. Make such states also target states. +// dtmc->makeAbsorbing(almostSurelyReachingTargetStates); +// // 2d. throw away non reachable states +// storm::storage::BitVector reachableStates = utility::graph::performProbGreater0(*dtmc, dtmc->getTransitionMatrix(), phiStates, initStates); +// storm::storage::BitVector bv = productiveStates & reachableStates; +// dtmc->getStateLabeling().addAtomicProposition("__targets__", targetStates | almostSurelyReachingTargetStates); +// models::Dtmc subdtmc = dtmc->getSubDtmc(bv); +// +// phiStates = storm::storage::BitVector(subdtmc.getNumberOfStates(), true); +// initStates = subdtmc.getInitialStates(); +// targetStates = subdtmc.getLabeledStates("__targets__"); +// storm::storage::BitVector deadlockStates(phiStates); +// deadlockStates.set(subdtmc.getNumberOfStates()-1,false); +// +// // Search for states with only one non-deadlock successor. +// std::map> chainedStates; +// StateId nrStates = subdtmc.getNumberOfStates(); +// StateId deadlockState = nrStates - 1; +// for(StateId source = 0; source < nrStates - 1; ++source) +// { +// if(targetStates[source]) +// { +// continue; +// } +// storage::DeterministicTransition productiveTransition(nrStates); +// for(auto const& transition : subdtmc.getRows(source)) +// { +// if(productiveTransition.targetState() == nrStates) +// { +// // first transition. +// productiveTransition = transition; +// } +// else +// { +// // second transition +// if(transition.first != deadlockState) +// { +// productiveTransition.targetState() = nrStates; +// break; +// } +// } +// } +// if(productiveTransition.targetState() != nrStates) +// { +// chainedStates.emplace(source, productiveTransition); +// } +// } +// storage::BitVector eliminatedStates(nrStates, false); +// for(auto & chainedState : chainedStates) +// { +// assert(chainedState.first != chainedState.second.targetState()); +// auto it = chainedStates.find(chainedState.second.targetState()); +// if(it != chainedStates.end()) +// { +// //std::cout << "----------------------------" << std::endl; +// //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; +// //std::cout << it->first << " -- " << it->second.probability() << " --> " << it->second.targetState() << std::endl; +// chainedState.second.targetState() = it->second.targetState(); +// chainedState.second.probability() *= it->second.probability(); +// //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; +// //std::cout << "----------------------------" << std::endl; +// chainedStates.erase(it); +// eliminatedStates.set(it->first, true); +// } +// } +// +// +// for(auto chainedState : chainedStates) +// { +// if(!eliminatedStates[chainedState.first]) +// { +// std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl; +// } +// } +// +// storage::StronglyConnectedComponentDecomposition sccs(subdtmc); +// std::cout << sccs << std::endl; +// +// modelchecker::reachability::DirectEncoding dec; +// std::vector parameters; +// for(auto constant : mProgram.getConstants()) +// { +// if(!constant.isDefined()) +// { +// std::cout << constant.getName() << std::endl; +// carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName()); +// assert(p != carl::Variable::NO_VARIABLE); +// parameters.push_back(p); +// } +// } +// return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates("__targets__"), mpq_class(1,2)); +// +//} +// +// +//void storm_parametric(const std::string& constants, const storm::prism::Program& program) +//{ +// ParametricStormEntryPoint entry(constants, program); +// entry.createModel(); +// storm::settings::Settings* s = storm::settings::Settings::getInstance(); +// if(s->isSet("reachability")) +// { +// std::ofstream fstream("test.smt2"); +// fstream << entry.reachabilityToSmt2(s->getOptionByLongName("reachability").getArgument(0).getValueAsString()); +// fstream.close(); +// } +// +// +//} +// +//} diff --git a/src/stormParametric.h b/src/stormParametric.h index b58cfab7c..cba7e8fe0 100644 --- a/src/stormParametric.h +++ b/src/stormParametric.h @@ -1,33 +1,33 @@ - - - -#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(); - std::string reachabilityToSmt2(std::string const&); - - virtual ~ParametricStormEntryPoint() {} - - }; - void storm_parametric(std::string const& constants, storm::prism::Program const&); -} - +// +// +// +//#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(); +// std::string reachabilityToSmt2(std::string const&); +// +// virtual ~ParametricStormEntryPoint() {} +// +// }; +// void storm_parametric(std::string const& constants, storm::prism::Program const&); +//} +// diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp index 89c5c9c6e..558583795 100644 --- a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp +++ b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp @@ -17,7 +17,7 @@ TEST(DeterministicSparseTransitionParserTest, NonExistingFile) { // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); storm::storage::SparseMatrix nullMatrix; ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not", nullMatrix), storm::exceptions::FileIoException); @@ -27,7 +27,7 @@ TEST(DeterministicSparseTransitionParserTest, NonExistingFile) { TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) { // Parse a deterministic transitions file and test the resulting matrix. - storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra"); + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra"); ASSERT_EQ(8, transitionMatrix.getColumnCount()); ASSERT_EQ(21, transitionMatrix.getEntryCount()); @@ -102,7 +102,7 @@ TEST(DeterministicSparseTransitionParserTest, BasicTransitionsParsing) { TEST(DeterministicSparseTransitionParserTest, BasicTransitionsRewardsParsing) { // First parse a transition file. Then parse a transition reward file for the resulting transition matrix. - storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra"); + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra"); storm::storage::SparseMatrix rewardMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_general.trans.rew", transitionMatrix); @@ -169,8 +169,8 @@ TEST(DeterministicSparseTransitionParserTest, Whitespaces) { // Test the resilience of the parser against whitespaces. // Do so by comparing the hash of the matrix resulting from the file without whitespaces with the hash of the matrix resulting from the file with whitespaces. - uint_fast64_t correctHash = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra").hash(); - storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_whitespaces.tra"); + uint_fast64_t correctHash = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra").hash(); + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_whitespaces.tra"); ASSERT_EQ(correctHash, transitionMatrix.hash()); // Do the same for the corresponding transition rewards file (with and without whitespaces) @@ -181,10 +181,10 @@ TEST(DeterministicSparseTransitionParserTest, Whitespaces) { TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) { // Since the MatrixBuilder needs sequential input of new elements reordering of transitions or states should throw an exception. - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mixedTransitionOrder.tra"), storm::exceptions::InvalidArgumentException); - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mixedStateOrder.tra"), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mixedTransitionOrder.tra"), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mixedStateOrder.tra"), storm::exceptions::InvalidArgumentException); - storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra"); + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra"); ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_mixedTransitionOrder.trans.rew", transitionMatrix), storm::exceptions::InvalidArgumentException); ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_mixedStateOrder.trans.rew", transitionMatrix), storm::exceptions::InvalidArgumentException); } @@ -195,7 +195,7 @@ TEST(DeterministicSparseTransitionParserTest, FixDeadlocks) { storm::settings::InternalOptionMemento setDeadlockOption("fixDeadlocks", true); // Parse a transitions file with the fixDeadlocks Flag set and test if it works. - storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"); + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"); ASSERT_EQ(9, transitionMatrix.getColumnCount()); ASSERT_EQ(23, transitionMatrix.getEntryCount()); @@ -219,20 +219,20 @@ TEST(DeterministicSparseTransitionParserTest, DontFixDeadlocks) { // Try to parse a transitions file containing a deadlock state with the fixDeadlocksFlag unset. This should throw an exception. storm::settings::InternalOptionMemento unsetDeadlockOption("fixDeadlocks", false); - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_deadlock.tra"), storm::exceptions::WrongFormatException); } TEST(DeterministicSparseTransitionParserTest, DoubledLines) { // There is a redundant line in the transition file. As the transition already exists this should throw an exception. // Note: If two consecutive lines are doubled no exception is thrown. - ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_doubledLines.tra"), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_doubledLines.tra"), storm::exceptions::InvalidArgumentException); } TEST(DeterministicSparseTransitionParserTest, RewardForNonExistentTransition) { // First parse a transition file. Then parse a transition reward file for the resulting transition matrix. - storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra"); + storm::storage::SparseMatrix transitionMatrix = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra"); // There is a reward for a transition that does not exist in the transition matrix. ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_rewardForNonExTrans.trans.rew", transitionMatrix), storm::exceptions::WrongFormatException);