diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index e6eab4322..95d39eb6d 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -351,7 +351,6 @@ namespace storm { // behaviour for this is undefined anyway, a warning should be issued in that case. for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { storm::prism::Command const& command = *iteratorList[i]; - std::cout << command << std::endl; for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { storm::prism::Update const& update = command.getUpdate(j); @@ -367,7 +366,6 @@ namespace storm { boost::container::flat_set newLabelSet = valueLabelSetPair.second; newLabelSet.insert(update.getGlobalIndex()); - std::cout << "got new value " << valueLabelSetPair.first << " * " << updateProbability << " = " << valueLabelSetPair.first * updateProbability << std::endl; newProbability.addValue(valueLabelSetPair.first * updateProbability, newLabelSet); } @@ -409,7 +407,6 @@ namespace storm { } ValueType probabilitySum = utility::constantZero(); - std::cout << "resetting prob sum" << std::endl; for (auto const& stateProbabilityPair : *newTargetStates) { std::pair flagTargetStateIndexPair = getOrAddStateIndex(stateProbabilityPair.first, stateInformation); @@ -421,7 +418,6 @@ namespace storm { for (auto const& probabilityLabelPair : stateProbabilityPair.second) { addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityLabelPair.first, probabilityLabelPair.second); probabilitySum += probabilityLabelPair.first; - std::cout << "increasing prob sum by " << probabilityLabelPair.first << std::endl; } } diff --git a/src/modelchecker/reachability/DirectEncoding.h b/src/modelchecker/reachability/DirectEncoding.h index 2c9f43e7c..ef5b8db3f 100644 --- a/src/modelchecker/reachability/DirectEncoding.h +++ b/src/modelchecker/reachability/DirectEncoding.h @@ -1,4 +1,4 @@ -/** +/** * @file: DirectEncoding.h * @author: Sebastian Junges * @@ -12,96 +12,71 @@ namespace storm { - namespace modelchecker - { - namespace reachability - { - class DirectEncoding - { - public: - template - std::string encodeAsSmt2(const storm::models::Dtmc& model, std::vector parameters, storm::storage::BitVector initialStates, storm::storage::BitVector finalStates, const typename T::CoeffType& threshold, bool lessequal = false) - { - carl::io::WriteTosmt2Stream smt2; - uint_fast64_t nrStates = model.getNumberOfStates(); - carl::VariablePool& vpool = carl::VariablePool::getInstance(); - std::vector stateVars; - for(carl::Variable p : parameters) - { - smt2 << ("parameter_bound_" + vpool.getName(p)); - smt2 << carl::io::smt2node::AND; - smt2 << carl::Constraint(Polynomial(p), carl::CompareRelation::GT); - smt2 << carl::Constraint(Polynomial(p) - Polynomial(1), carl::CompareRelation::LT); - smt2 << carl::io::smt2node::CLOSENODE; - } - for(uint_fast64_t state = 0; state < nrStates-1; ++state) - { - - carl::Variable stateVar = vpool.getFreshVariable("s_" + std::to_string(state)); - stateVars.push_back(stateVar); - if(!finalStates[state]) - { - smt2 << ("state_bound_" + std::to_string(state)); - smt2 << carl::io::smt2node::AND; - smt2 << carl::Constraint(Polynomial(stateVar), carl::CompareRelation::GT); - smt2 << carl::Constraint(Polynomial(stateVar) - Polynomial(1), carl::CompareRelation::LT); - smt2 << carl::io::smt2node::CLOSENODE; - } - - } - - smt2.setAutomaticLineBreaks(true); - Polynomial initStateReachSum; - for(uint_fast64_t state = 0; state < nrStates-1; ++state) - { - if(initialStates[state]) - { - initStateReachSum += stateVars[state]; - } - if(finalStates[state]) - { - //smt2 << carl::Constraint(Polynomial(stateVars[state]) - Polynomial(1), carl::CompareRelation::EQ); - } - else - { - T reachpropPol(0); - for(auto const& transition : model.getRows(state)) - { - if(finalStates[transition.first]) - { - reachpropPol += transition.second; - } - else if(transition.first == nrStates - 1) - { - // intentionally empty. - } - else - { - reachpropPol += transition.second * stateVars[transition.first]; - } - - } - smt2 << ("transition_" + std::to_string(state)); - smt2 << carl::Constraint(reachpropPol - stateVars[state], carl::CompareRelation::EQ); - } - } - //smt2 << carl::Constraint(Polynomial(stateVars[nrStates-1]), carl::CompareRelation::EQ); - - - smt2 << ("reachability"); - - carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LEQ : carl::CompareRelation::GEQ; - smt2 << carl::Constraint(initStateReachSum - threshold, thresholdRelation); - smt2 << carl::io::smt2flag::CHECKSAT; - smt2 << carl::io::smt2flag::MODEL; - smt2 << carl::io::smt2flag::UNSAT_CORE; - std::stringstream strm; - strm << smt2; - return strm.str(); - } - }; - } - } + namespace modelchecker + { + namespace reachability + { + class DirectEncoding + { + public: + template + std::string encodeAsSmt2(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& oneStepProbabilities, std::vector const& parameters, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& finalStates, typename T::CoeffType const& threshold, bool lessequal = false) { + + carl::io::WriteTosmt2Stream smt2; + uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); + carl::VariablePool& vpool = carl::VariablePool::getInstance(); + std::vector stateVars; + for (carl::Variable const& p : parameters) { + smt2 << ("parameter_bound_" + vpool.getName(p)); + smt2 << carl::io::smt2node::AND; + smt2 << carl::Constraint(Polynomial::PolyType(p), carl::CompareRelation::GT); + smt2 << carl::Constraint(Polynomial::PolyType(p) - Polynomial::PolyType(1), carl::CompareRelation::LT); + smt2 << carl::io::smt2node::CLOSENODE; + } + + for (uint_fast64_t state = 0; state < numberOfStates; ++state) { + carl::Variable stateVar = vpool.getFreshVariable("s_" + std::to_string(state)); + stateVars.push_back(stateVar); + if (!finalStates[state]) { + smt2 << ("state_bound_" + std::to_string(state)); + smt2 << carl::io::smt2node::AND; + smt2 << carl::Constraint(Polynomial::PolyType(stateVar), carl::CompareRelation::GT); + smt2 << carl::Constraint(Polynomial::PolyType(stateVar) - Polynomial::PolyType(1), carl::CompareRelation::LT); + smt2 << carl::io::smt2node::CLOSENODE; + } + } + + smt2.setAutomaticLineBreaks(true); + Polynomial::PolyType initStateReachSum; + for (uint_fast64_t state = 0; state < numberOfStates; ++state) { + T reachpropPol(0); + for (auto const& transition : transitionMatrix.getRow(state)) { + reachpropPol += transition.getValue() * stateVars[transition.getColumn()]; + } + reachpropPol += oneStepProbabilities[state]; + smt2 << ("transition_" + std::to_string(state)); + smt2 << carl::Constraint(reachpropPol - stateVars[state], carl::CompareRelation::EQ); + } + + smt2 << ("reachability"); + + carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LEQ : carl::CompareRelation::GEQ; + smt2 << carl::io::smt2node::OR; + for (uint_fast64_t state : initialStates) { + smt2 << carl::Constraint(Polynomial::PolyType(stateVars[state]) - threshold, thresholdRelation); + } + smt2 << carl::io::smt2node::CLOSENODE; + + smt2 << carl::io::smt2flag::CHECKSAT; + smt2 << carl::io::smt2flag::MODEL; + smt2 << carl::io::smt2flag::UNSAT_CORE; + std::stringstream strm; + strm << smt2; + return strm.str(); + } + }; + } + } } #endif \ No newline at end of file diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 456d3a179..d3d4a1b8f 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -20,6 +20,7 @@ #include "src/settings/SettingsManager.h" #include "src/utility/vector.h" #include "src/utility/matrix.h" +#include "src/utility/ConstantsComparator.h" namespace storm { @@ -329,24 +330,23 @@ private: * Checks probability matrix if all rows sum up to one. */ bool checkValidityOfProbabilityMatrix() { - // Get the settings object to customize linear solving. - - if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) { // not square LOG4CPLUS_ERROR(logger, "Probability matrix is not square."); return false; } + + storm::utility::ConstantsComparator comparator; for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); ++row) { - T sum = this->getTransitionMatrix().getRowSum(row); - - if (sum == T(0)) { - - LOG4CPLUS_ERROR(logger, "Row " << row << " is a deadlock (sum == " << sum << ")."); - return false; - } - if (!storm::utility::isOne(sum)) { - LOG4CPLUS_ERROR(logger, "Row " << row << " has sum " << sum << "."); + T sum = this->getTransitionMatrix().getRowSum(row); + + // If the sum is not a constant, for example for parametric models, we cannot check whether the sum is one + // or not. + if (!comparator.isConstant(sum)) { + continue; + } + + if (!comparator.isOne(sum)) { return false; } } diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 936a931fa..c0ac68ef2 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -9,7 +9,7 @@ #include "src/utility/export.h" #include "src/modelchecker/reachability/CollectConstraints.h" -//#include "src/modelchecker/reachability/DirectEncoding.h" +#include "src/modelchecker/reachability/DirectEncoding.h" //#include "src/storage/DeterministicModelStrongBisimulationDecomposition.h" #include "src/modelchecker/reachability/SparseSccModelChecker.h" #include "src/storage/parameters.h" @@ -43,7 +43,7 @@ int main(const int argc, const char** argv) { std::shared_ptr> dtmc = model->as>(); - // Perform bisimulation minimization if requested. +// Perform bisimulation minimization if requested. // if (storm::settings::generalSettings().isBisimulationSet()) { // storm::storage::DeterministicModelStrongBisimulationDecomposition bisimulationDecomposition(*dtmc, true); // dtmc = bisimulationDecomposition.getQuotient()->as>(); @@ -80,11 +80,10 @@ int main(const int argc, const char** argv) { storm::utility::exportParametricMcResult(value, constraintCollector); } - if(storm::settings::parametricSettings().exportToSmt2File()) { +// if (storm::settings::parametricSettings().exportToSmt2File()) { // storm::modelchecker::reachability::DirectEncoding dec; -// storm::utility::exportStreamToFile(dec.encodeAsSmt2(modelChecker.getMatrix(), parameters,)); - } - +// storm::utility::exportStringStreamToFile(dec.encodeAsSmt2(modelChecker.getMatrix(), parameters,)); +// } // All operations have now been performed, so we clean up everything and terminate. storm::utility::cli::cleanUp(); diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h index 4936216ca..d3d4fba38 100644 --- a/src/utility/ConstantsComparator.h +++ b/src/utility/ConstantsComparator.h @@ -36,15 +36,15 @@ namespace storm { template class ConstantsComparator { public: - bool isOne(ValueType const& value) { + bool isOne(ValueType const& value) const { return value == one(); } - bool isZero(ValueType const& value) { + bool isZero(ValueType const& value) const { return value == zero(); } - bool isEqual(ValueType const& value1, ValueType const& value2) { + bool isEqual(ValueType const& value1, ValueType const& value2) const { return value1 == value2; } }; @@ -61,18 +61,22 @@ namespace storm { // Intentionally left empty. } - bool isOne(double const& value) { + bool isOne(double const& value) const { return std::abs(value - one()) <= precision; } - bool isZero(double const& value) { + bool isZero(double const& value) const { return std::abs(value) <= precision; } - bool isEqual(double const& value1, double const& value2) { + bool isEqual(double const& value1, double const& value2) const { return std::abs(value1 - value2) <= precision; } + bool isConstant(double const& value) const { + return true; + } + private: // The precision used for comparisons. double precision; @@ -93,6 +97,10 @@ namespace storm { bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) { return value1 == value2; } + + bool isConstant(storm::RationalFunction const& value) const { + return value.isConstant(); + } }; template<> @@ -109,6 +117,10 @@ namespace storm { bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) { return value1 == value2; } + + bool isConstant(storm::Polynomial const& value) const { + return value.isConstant(); + } }; #endif