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

moved constraint collection to DTMC class 

Former-commit-id: 5471a20bec
tempestpy_adaptions
dehnert 9 years ago
parent
a22c36e38a
commit
4dbbe3c561
5 changed files with 113 additions and 144 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 63
      src/modelchecker/reachability/CollectConstraints.h
  2. 80
      src/modelchecker/reachability/DirectEncoding.h
  3. 40
      src/models/sparse/Dtmc.cpp
  4. 51
      src/models/sparse/Dtmc.h
  5. 23
      src/utility/cli.h

63
src/modelchecker/reachability/CollectConstraints.h
View File

@ -1,63 +0,0 @@
/**
* @file: CollectConstraints.h
* @author: Sebastian Junges
*
* @since October 8, 2014
*/
#pragma once
#include "src/models/Dtmc.h"
namespace storm {
namespace modelchecker {
namespace reachability {
template<typename ValueType>
class CollectConstraints
{
private:
std::unordered_set<carl::Constraint<ValueType>> wellformedConstraintSet;
std::unordered_set<carl::Constraint<ValueType>> graphPreservingConstraintSet;
storm::utility::ConstantsComparator<ValueType> comparator;
public:
std::unordered_set<carl::Constraint<ValueType>> const& wellformedConstraints() const {
return this->wellformedConstraintSet;
}
std::unordered_set<carl::Constraint<ValueType>> const& graphPreservingConstraints() const {
return this->graphPreservingConstraintSet;
}
void process(storm::models::Dtmc<ValueType> const& dtmc)
{
for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state)
{
ValueType sum;
assert(comparator.isZero(sum));
for(auto const& transition : dtmc.getRows(state))
{
sum += transition.getValue();
if(!transition.getValue().isConstant())
{
wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ);
wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ);
graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GT);
}
}
assert(!comparator.isConstant(sum) || comparator.isOne(sum));
if(!sum.isConstant()) {
wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ);
}
}
}
void operator()(storm::models::Dtmc<ValueType> const& dtmc)
{
process(dtmc);
}
};
}
}
}

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

@ -1,80 +0,0 @@
/**
* @file: DirectEncoding.h
* @author: Sebastian Junges
*
* @since April 8, 2014
*/
#pragma once
#ifdef STORM_HAVE_CARL
#include <carl/io/WriteTosmt2Stream.h>
namespace storm
{
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::set<carl::Variable> const& parameters, storm::storage::BitVector const& initialStates, 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);
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;
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<Polynomial::PolyType>(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

40
src/models/sparse/Dtmc.cpp
View File

@ -182,6 +182,46 @@ namespace storm {
// return storm::models::Dtmc<ValueType>(newMatBuilder.build(), newLabeling, newStateRewards, std::move(newTransitionRewards), newChoiceLabels);
}
template<typename ValueType>
Dtmc<ValueType>::ConstraintCollector::ConstraintCollector(Dtmc<ValueType> const& dtmc) {
process(dtmc);
}
template<typename ValueType>
std::unordered_set<carl::Constraint<ValueType>> const& Dtmc<ValueType>::ConstraintCollector::getWellformedConstraints() const {
return this->wellformedConstraintSet;
}
template<typename ValueType>
std::unordered_set<carl::Constraint<ValueType>> const& Dtmc<ValueType>::ConstraintCollector::getGraphPreservingConstraints() const {
return this->graphPreservingConstraintSet;
}
template<typename ValueType>
void Dtmc<ValueType>::ConstraintCollector::process(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) {
ValueType sum = storm::utility::zero<ValueType>();
for (auto const& transition : dtmc.getRows(state)) {
sum += transition.getValue();
if (!comparator.isConstant(transition.getValue())) {
wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ);
wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ);
graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GT);
}
}
STORM_LOG_ASSERT(!comparator.isConstant(sum) || comparator.isOne(sum), "If the sum is a constant, it must be equal to 1.");
if(!comparator.isConstant(sum)) {
wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ);
}
}
}
template<typename ValueType>
void Dtmc<ValueType>::ConstraintCollector::operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
process(dtmc);
}
template <typename ValueType>
bool Dtmc<ValueType>::checkValidityOfProbabilityMatrix() const {
if (this->getTransitionMatrix().getRowCount() != this->getTransitionMatrix().getColumnCount()) {

51
src/models/sparse/Dtmc.h
View File

@ -59,6 +59,57 @@ namespace storm {
*/
Dtmc<ValueType> getSubDtmc(storm::storage::BitVector const& states) const;
class ConstraintCollector {
private:
// A set of constraints that says that the DTMC actually has valid probability distributions in all states.
std::unordered_set<carl::Constraint<ValueType>> wellformedConstraintSet;
// A set of constraints that makes sure that the underlying graph of the model does not change depending
// on the parameter values.
std::unordered_set<carl::Constraint<ValueType>> graphPreservingConstraintSet;
// A comparator that is used for
storm::utility::ConstantsComparator<ValueType> comparator;
public:
/*!
* Constructs the a constraint collector for the given DTMC. The constraints are built and ready for
* retrieval after the construction.
*
* @param dtmc The DTMC for which to create the constraints.
*/
ConstraintCollector(storm::models::sparse::Dtmc<ValueType> const& dtmc);
/*!
* Returns the set of wellformed-ness constraints.
*
* @return The set of wellformed-ness constraints.
*/
std::unordered_set<carl::Constraint<ValueType>> const& getWellformedConstraints() const;
/*!
* Returns the set of graph-preserving constraints.
*
* @return The set of graph-preserving constraints.
*/
std::unordered_set<carl::Constraint<ValueType>> const& getGraphPreservingConstraints() const;
/*!
* Constructs the constraints for the given DTMC.
*
* @param dtmc The DTMC for which to create the constraints.
*/
void process(storm::models::sparse::Dtmc<ValueType> const& dtmc);
/*!
* Constructs the constraints for the given DTMC by calling the process method.
*
* @param dtmc The DTMC for which to create the constraints.
*/
void operator()(storm::models::sparse::Dtmc<ValueType> const& dtmc);
};
private:
/*!
* Checks the probability matrix for validity.

23
src/utility/cli.h
View File

@ -145,7 +145,7 @@ namespace storm {
std::cout << "--------" << std::endl << std::endl;
// std::cout << storm::utility::StormVersion::longVersionString() << std::endl;
std::cout << storm::utility::StormVersion::longVersionString() << std::endl;
#ifdef STORM_HAVE_INTELTBB
std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
#endif
@ -473,6 +473,22 @@ namespace storm {
}
#ifdef STORM_HAVE_CARL
void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
std::ofstream filestream;
filestream.open(path);
// TODO: add checks.
filestream << "!Parameters: ";
std::set<storm::Variable> vars = result.gatherVariables();
std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, ", "));
filestream << std::endl;
filestream << "!Result: " << result << std::endl;
filestream << "!Well-formed Constraints: " << std::endl;
std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator<carl::Constraint<storm::RationalFunction>>(filestream, "\n"));
filestream << "!Graph-preserving Constraints: " << std::endl;
std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator<carl::Constraint<storm::RationalFunction>>(filestream, "\n"));
filestream.close();
}
template<>
void verifySparseModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
@ -498,6 +514,11 @@ namespace storm {
} else {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
}
storm::settings::modules::ParametricSettings const& parametricSettings = storm::settings::parametricSettings();
if (parametricSettings.exportResultToFile()) {
exportParametricResultToFile(result->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*dtmc->getInitialStates().begin()], storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector(*dtmc), parametricSettings.exportResultPath());
}
}
#endif

Write Preview
Loading…
Cancel
Save