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

Merged master and started to fix DirectEncoding.h. Removed some debug output. 

Former-commit-id: d4fe7bfd6a
main
dehnert 11 years ago
parent
aa6e44a1e2 843a1d1fdf
commit
946311469b
5 changed files with 101 additions and 119 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/adapters/ExplicitModelAdapter.h
  2. 157
      src/modelchecker/reachability/DirectEncoding.h
  3. 24
      src/models/Dtmc.h
  4. 11
      src/stormParametric.cpp
  5. 24
      src/utility/ConstantsComparator.h

4
src/adapters/ExplicitModelAdapter.h
View File

@ -351,7 +351,6 @@ namespace storm {
// behaviour for this is undefined anyway, a warning should be issued in that case. // behaviour for this is undefined anyway, a warning should be issued in that case.
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
storm::prism::Command const& command = *iteratorList[i]; storm::prism::Command const& command = *iteratorList[i];
std::cout << command << std::endl;
for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
storm::prism::Update const& update = command.getUpdate(j); storm::prism::Update const& update = command.getUpdate(j);
@ -367,7 +366,6 @@ namespace storm {
boost::container::flat_set<uint_fast64_t> newLabelSet = valueLabelSetPair.second; boost::container::flat_set<uint_fast64_t> newLabelSet = valueLabelSetPair.second;
newLabelSet.insert(update.getGlobalIndex()); newLabelSet.insert(update.getGlobalIndex());
std::cout << "got new value " << valueLabelSetPair.first << " * " << updateProbability << " = " << valueLabelSetPair.first * updateProbability << std::endl;
newProbability.addValue(valueLabelSetPair.first * updateProbability, newLabelSet); newProbability.addValue(valueLabelSetPair.first * updateProbability, newLabelSet);
} }
@ -409,7 +407,6 @@ namespace storm {
} }
ValueType probabilitySum = utility::constantZero<ValueType>(); ValueType probabilitySum = utility::constantZero<ValueType>();
std::cout << "resetting prob sum" << std::endl;
for (auto const& stateProbabilityPair : *newTargetStates) { for (auto const& stateProbabilityPair : *newTargetStates) {
std::pair<bool, uint_fast64_t> flagTargetStateIndexPair = getOrAddStateIndex(stateProbabilityPair.first, stateInformation); std::pair<bool, uint_fast64_t> flagTargetStateIndexPair = getOrAddStateIndex(stateProbabilityPair.first, stateInformation);
@ -421,7 +418,6 @@ namespace storm {
for (auto const& probabilityLabelPair : stateProbabilityPair.second) { for (auto const& probabilityLabelPair : stateProbabilityPair.second) {
addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityLabelPair.first, probabilityLabelPair.second); addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityLabelPair.first, probabilityLabelPair.second);
probabilitySum += probabilityLabelPair.first; probabilitySum += probabilityLabelPair.first;
std::cout << "increasing prob sum by " << probabilityLabelPair.first << std::endl;
} }
} }

157
src/modelchecker/reachability/DirectEncoding.h
View File

@ -1,4 +1,4 @@
/**
/**
* @file: DirectEncoding.h * @file: DirectEncoding.h
* @author: Sebastian Junges * @author: Sebastian Junges
* *
@ -12,96 +12,71 @@
namespace storm namespace storm
{ {
namespace modelchecker
{
namespace reachability
{
class DirectEncoding
{
public:
template<typename T>
std::string encodeAsSmt2(const storm::models::Dtmc<T>& model, std::vector<carl::Variable> 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<carl::Variable> stateVars;
for(carl::Variable p : parameters)
{
smt2 << ("parameter_bound_" + vpool.getName(p));
smt2 << carl::io::smt2node::AND;
smt2 << carl::Constraint<Polynomial>(Polynomial(p), carl::CompareRelation::GT);
smt2 << carl::Constraint<Polynomial>(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>(Polynomial(stateVar), carl::CompareRelation::GT);
smt2 << carl::Constraint<Polynomial>(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>(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<T>(reachpropPol - stateVars[state], carl::CompareRelation::EQ);
}
}
//smt2 << carl::Constraint<Polynomial>(Polynomial(stateVars[nrStates-1]), carl::CompareRelation::EQ);
smt2 << ("reachability");
carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LEQ : carl::CompareRelation::GEQ;
smt2 << carl::Constraint<Polynomial>(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<typename T>
std::string encodeAsSmt2(storm::storage::SparseMatrix<T> const& transitionMatrix, std::vector<T> const& oneStepProbabilities, std::vector<carl::Variable> 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<carl::Variable> stateVars;
for (carl::Variable const& p : parameters) {
smt2 << ("parameter_bound_" + vpool.getName(p));
smt2 << carl::io::smt2node::AND;
smt2 << carl::Constraint<Polynomial::PolyType>(Polynomial::PolyType(p), carl::CompareRelation::GT);
smt2 << carl::Constraint<Polynomial::PolyType>(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>(Polynomial::PolyType(stateVar), carl::CompareRelation::GT);
smt2 << carl::Constraint<Polynomial::PolyType>(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<T>(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>(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 #endif

24
src/models/Dtmc.h
View File

@ -20,6 +20,7 @@
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
#include "src/utility/vector.h" #include "src/utility/vector.h"
#include "src/utility/matrix.h" #include "src/utility/matrix.h"
#include "src/utility/ConstantsComparator.h"
namespace storm { namespace storm {
@ -329,24 +330,23 @@ private:
* Checks probability matrix if all rows sum up to one. * Checks probability matrix if all rows sum up to one.
*/ */
bool checkValidityOfProbabilityMatrix() { bool checkValidityOfProbabilityMatrix() {
// Get the settings object to customize linear solving.
if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) { if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) {
// not square // not square
LOG4CPLUS_ERROR(logger, "Probability matrix is not square."); LOG4CPLUS_ERROR(logger, "Probability matrix is not square.");
return false; return false;
} }
storm::utility::ConstantsComparator<T> comparator;
for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); ++row) { 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; return false;
} }
} }

11
src/stormParametric.cpp
View File

@ -9,7 +9,7 @@
#include "src/utility/export.h" #include "src/utility/export.h"
#include "src/modelchecker/reachability/CollectConstraints.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/storage/DeterministicModelStrongBisimulationDecomposition.h"
#include "src/modelchecker/reachability/SparseSccModelChecker.h" #include "src/modelchecker/reachability/SparseSccModelChecker.h"
#include "src/storage/parameters.h" #include "src/storage/parameters.h"
@ -43,7 +43,7 @@ int main(const int argc, const char** argv) {
std::shared_ptr<storm::models::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::Dtmc<storm::RationalFunction>>(); std::shared_ptr<storm::models::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::Dtmc<storm::RationalFunction>>();
// Perform bisimulation minimization if requested.
// Perform bisimulation minimization if requested.
// if (storm::settings::generalSettings().isBisimulationSet()) { // if (storm::settings::generalSettings().isBisimulationSet()) {
// storm::storage::DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, true); // storm::storage::DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, true);
// dtmc = bisimulationDecomposition.getQuotient()->as<storm::models::Dtmc<storm::RationalFunction>>(); // dtmc = bisimulationDecomposition.getQuotient()->as<storm::models::Dtmc<storm::RationalFunction>>();
@ -80,11 +80,10 @@ int main(const int argc, const char** argv) {
storm::utility::exportParametricMcResult(value, constraintCollector); storm::utility::exportParametricMcResult(value, constraintCollector);
} }
if(storm::settings::parametricSettings().exportToSmt2File()) {
// if (storm::settings::parametricSettings().exportToSmt2File()) {
// storm::modelchecker::reachability::DirectEncoding dec; // 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. // All operations have now been performed, so we clean up everything and terminate.
storm::utility::cli::cleanUp(); storm::utility::cli::cleanUp();

24
src/utility/ConstantsComparator.h
View File

@ -36,15 +36,15 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
class ConstantsComparator { class ConstantsComparator {
public: public:
bool isOne(ValueType const& value) {
bool isOne(ValueType const& value) const {
return value == one<ValueType>(); return value == one<ValueType>();
} }
bool isZero(ValueType const& value) {
bool isZero(ValueType const& value) const {
return value == zero<ValueType>(); return value == zero<ValueType>();
} }
bool isEqual(ValueType const& value1, ValueType const& value2) {
bool isEqual(ValueType const& value1, ValueType const& value2) const {
return value1 == value2; return value1 == value2;
} }
}; };
@ -61,18 +61,22 @@ namespace storm {
// Intentionally left empty. // Intentionally left empty.
} }
bool isOne(double const& value) {
bool isOne(double const& value) const {
return std::abs(value - one<double>()) <= precision; return std::abs(value - one<double>()) <= precision;
} }
bool isZero(double const& value) {
bool isZero(double const& value) const {
return std::abs(value) <= precision; 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; return std::abs(value1 - value2) <= precision;
} }
bool isConstant(double const& value) const {
return true;
}
private: private:
// The precision used for comparisons. // The precision used for comparisons.
double precision; double precision;
@ -93,6 +97,10 @@ namespace storm {
bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) { bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) {
return value1 == value2; return value1 == value2;
} }
bool isConstant(storm::RationalFunction const& value) const {
return value.isConstant();
}
}; };
template<> template<>
@ -109,6 +117,10 @@ namespace storm {
bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) { bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) {
return value1 == value2; return value1 == value2;
} }
bool isConstant(storm::Polynomial const& value) const {
return value.isConstant();
}
}; };
#endif #endif

Write Preview
Loading…
Cancel
Save