Browse Source

Implemented modularisation for MTTF via parallel composition of CTMCs

Former-commit-id: 552949346b
main
Mavo 9 years ago
parent
commit
6fcc97a7b4
  1. 172
      src/builder/ParallelCompositionBuilder.cpp
  2. 24
      src/builder/ParallelCompositionBuilder.h
  3. 218
      src/modelchecker/dft/DFTModelChecker.cpp
  4. 14
      src/modelchecker/dft/DFTModelChecker.h
  5. 2
      src/storage/dft/DFT.cpp
  6. 6
      src/storm-dyftee.cpp

172
src/builder/ParallelCompositionBuilder.cpp

@ -0,0 +1,172 @@
#include "src/builder/ParallelCompositionBuilder.h"
#include "src/models/sparse/StandardRewardModel.h"
#include <src/utility/constants.h>
namespace storm {
namespace builder {
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ParallelCompositionBuilder<ValueType>::compose(std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmcA, std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmcB, bool labelAnd) {
STORM_LOG_TRACE("Parallel composition");
storm::storage::SparseMatrix<ValueType> matrixA = ctmcA->getTransitionMatrix();
storm::storage::SparseMatrix<ValueType> matrixB = ctmcB->getTransitionMatrix();
storm::models::sparse::StateLabeling labelingA = ctmcA->getStateLabeling();
storm::models::sparse::StateLabeling labelingB = ctmcB->getStateLabeling();
size_t sizeA = ctmcA->getNumberOfStates();
size_t sizeB = ctmcB->getNumberOfStates();
size_t size = sizeA * sizeB;
size_t rowIndex = 0;
// Build matrix
storm::storage::SparseMatrixBuilder<ValueType> builder(size, size, 0, true, false, 0);
for (size_t stateA = 0; stateA < sizeA; ++stateA) {
for (size_t stateB = 0; stateB < sizeB; ++stateB) {
STORM_LOG_ASSERT(rowIndex == stateA * sizeB + stateB, "Row " << rowIndex << " is not correct");
auto rowA = matrixA.getRow(stateA);
auto itA = rowA.begin();
auto rowB = matrixB.getRow(stateB);
auto itB = rowB.begin();
// First consider all target states of A < the current stateA
while (itA != rowA.end() && itA->getColumn() < stateA) {
builder.addNextValue(rowIndex, itA->getColumn() * sizeB + stateB, itA->getValue());
++itA;
}
// Then consider all target states of B
while (itB != rowB.end()) {
builder.addNextValue(rowIndex, stateA * sizeB + itB->getColumn(), itB->getValue());
++itB;
}
// Last consider all remaining target states of A > the current stateA
while (itA != rowA.end()) {
builder.addNextValue(rowIndex, itA->getColumn() * sizeB + stateB, itA->getValue());
++itA;
}
++rowIndex;
}
}
storm::storage::SparseMatrix<ValueType> matrixComposed = builder.build();
STORM_LOG_ASSERT(matrixComposed.getRowCount() == size, "Row count is not correct");
STORM_LOG_ASSERT(matrixComposed.getColumnCount() == size, "Column count is not correct");
// Build labeling
storm::models::sparse::StateLabeling labeling = storm::models::sparse::StateLabeling(sizeA * sizeB);
if (labelAnd) {
for (std::string const& label : labelingA.getLabels()) {
if (labelingB.containsLabel(label)) {
// Only consider labels contained in both CTMCs
storm::storage::BitVector labelStates(size, false);
for (auto entryA : labelingA.getStates(label)) {
for (auto entryB : labelingB.getStates(label)) {
labelStates.set(entryA * sizeB + entryB);
}
}
labeling.addLabel(label, labelStates);
}
}
} else {
// Set labels from A
for (std::string const& label : labelingA.getLabels()) {
if (label == "init") {
// Initial states must be initial in both CTMCs
STORM_LOG_ASSERT(labelingB.containsLabel(label), "B does not have init.");
storm::storage::BitVector labelStates(size, false);
for (auto entryA : labelingA.getStates(label)) {
for (auto entryB : labelingB.getStates(label)) {
labelStates.set(entryA * sizeB + entryB);
}
}
labeling.addLabel(label, labelStates);
} else {
storm::storage::BitVector labelStates(size, false);
for (auto entry : labelingA.getStates(label)) {
for (size_t index = entry * sizeB; index < entry * sizeB + sizeB; ++index) {
labelStates.set(index, true);
}
}
labeling.addLabel(label, labelStates);
}
}
// Set labels from B
for (std::string const& label : labelingB.getLabels()) {
if (label == "init") {
continue;
}
if (labeling.containsLabel(label)) {
// Label is already there from A
for (auto entry : labelingB.getStates(label)) {
for (size_t index = 0; index < sizeA; ++index) {
labeling.addLabelToState(label, index * sizeB + entry);
}
}
} else {
storm::storage::BitVector labelStates(size, false);
for (auto entry : labelingB.getStates(label)) {
for (size_t index = 0; index < sizeA; ++index) {
labelStates.set(index * sizeB + entry, true);
}
}
labeling.addLabel(label, labelStates);
}
}
}
// Build CTMC
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> composedCtmc = std::make_shared<storm::models::sparse::Ctmc<ValueType>>(matrixComposed, labeling);
// Print for debugging
/*std::cout << "Matrix A:" << std::endl;
std::cout << matrixA << std::endl;
std::cout << "Matrix B:" << std::endl;
std::cout << matrixB << std::endl;
std::cout << "Composed matrix: " << std::endl << matrixComposed;
std::cout << "Labeling A" << std::endl;
labelingA.printLabelingInformationToStream(std::cout);
for (size_t stateA = 0; stateA < sizeA; ++stateA) {
std::cout << "State " << stateA << ": ";
for (auto label : labelingA.getLabelsOfState(stateA)) {
std::cout << label << ", ";
}
std::cout << std::endl;
}
std::cout << "Labeling B" << std::endl;
labelingB.printLabelingInformationToStream(std::cout);
for (size_t stateB = 0; stateB < sizeB; ++stateB) {
std::cout << "State " << stateB << ": ";
for (auto label : labelingB.getLabelsOfState(stateB)) {
std::cout << label << ", ";
}
std::cout << std::endl;
}
std::cout << "Labeling Composed" << std::endl;
labeling.printLabelingInformationToStream(std::cout);
for (size_t state = 0; state < size; ++state) {
std::cout << "State " << state << ": ";
for (auto label : labeling.getLabelsOfState(state)) {
std::cout << label << ", ";
}
std::cout << std::endl;
}*/
return composedCtmc;
}
// Explicitly instantiate the class.
template class ParallelCompositionBuilder<double>;
#ifdef STORM_HAVE_CARL
template class ParallelCompositionBuilder<storm::RationalFunction>;
#endif
} // namespace builder
} // namespace storm

24
src/builder/ParallelCompositionBuilder.h

@ -0,0 +1,24 @@
#ifndef PARALLELCOMPOSITIONBUILDER_H
#define PARALLELCOMPOSITIONBUILDER_H
#include <src/models/sparse/Ctmc.h>
namespace storm {
namespace builder {
/*!
* Build a parallel composition of Markov chains.
*/
template<typename ValueType>
class ParallelCompositionBuilder {
public:
static std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> compose(std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmcA, std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> const& ctmcB, bool labelAnd);
};
}
}
#endif /* EXPLICITDFTMODELBUPARALLELCOMPOSITIONBUILDER_HILDERAPPROX_H */

218
src/modelchecker/dft/DFTModelChecker.cpp

@ -2,6 +2,7 @@
#include "src/builder/ExplicitDFTModelBuilder.h"
#include "src/builder/ExplicitDFTModelBuilderApprox.h"
#include "src/builder/ParallelCompositionBuilder.h"
#include "src/storage/dft/DFTIsomorphism.h"
#include "src/settings/modules/DFTSettings.h"
#include "src/utility/bitoperations.h"
@ -28,10 +29,19 @@ namespace storm {
// Optimizing DFT
storm::storage::DFT<ValueType> dft = origDft.optimize();
// TODO Matthias: check that all paths reach the target state!
// TODO Matthias: check that all paths reach the target state for approximation
// Checking DFT
checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC, approximationError);
if (formula->isProbabilityOperatorFormula() || !allowModularisation) {
checkResult = checkHelper(dft, formula, symred, allowModularisation, enableDC, approximationError);
} else {
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelComposition(dft, formula, symred, allowModularisation, enableDC);
// Model checking
std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
checkResult = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
}
this->totalTime = std::chrono::high_resolution_clock::now() - totalStart;
}
@ -85,45 +95,44 @@ namespace storm {
if(modularisationPossible) {
STORM_LOG_TRACE("Recursive CHECK Call");
// TODO Matthias: enable modularisation for approximation
STORM_LOG_ASSERT(approximationError == 0.0, "Modularisation not possible for approximation.");
// Recursively call model checking
std::vector<ValueType> res;
for(auto const ft : dfts) {
dft_result ftResult = checkHelper(ft, formula, symred, true, enableDC, 0.0);
res.push_back(boost::get<ValueType>(ftResult));
}
if (formula->isProbabilityOperatorFormula()) {
// Recursively call model checking
std::vector<ValueType> res;
for(auto const ft : dfts) {
dft_result ftResult = checkHelper(ft, formula, symred, true, enableDC, 0.0);
res.push_back(boost::get<ValueType>(ftResult));
}
// Combine modularisation results
STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" << (invResults?"On":"Off"));
ValueType result = storm::utility::zero<ValueType>();
int limK = invResults ? -1 : nrM+1;
int chK = invResults ? -1 : 1;
// WARNING: there is a bug for computing permutations with more than 32 elements
STORM_LOG_ASSERT(res.size() < 32, "Permutations work only for < 32 elements");
for(int cK = nrK; cK != limK; cK += chK ) {
STORM_LOG_ASSERT(cK >= 0, "ck negative.");
size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(cK));
do {
STORM_LOG_TRACE("Permutation="<<permutation);
ValueType permResult = storm::utility::one<ValueType>();
for(size_t i = 0; i < res.size(); ++i) {
if(permutation & (1 << i)) {
permResult *= res[i];
} else {
permResult *= storm::utility::one<ValueType>() - res[i];
// Combine modularisation results
STORM_LOG_TRACE("Combining all results... K=" << nrK << "; M=" << nrM << "; invResults=" << (invResults?"On":"Off"));
ValueType result = storm::utility::zero<ValueType>();
int limK = invResults ? -1 : nrM+1;
int chK = invResults ? -1 : 1;
// WARNING: there is a bug for computing permutations with more than 32 elements
STORM_LOG_ASSERT(res.size() < 32, "Permutations work only for < 32 elements");
for(int cK = nrK; cK != limK; cK += chK ) {
STORM_LOG_ASSERT(cK >= 0, "ck negative.");
size_t permutation = smallestIntWithNBitsSet(static_cast<size_t>(cK));
do {
STORM_LOG_TRACE("Permutation="<<permutation);
ValueType permResult = storm::utility::one<ValueType>();
for(size_t i = 0; i < res.size(); ++i) {
if(permutation & (1 << i)) {
permResult *= res[i];
} else {
permResult *= storm::utility::one<ValueType>() - res[i];
}
}
}
STORM_LOG_TRACE("Result for permutation:"<<permResult);
permutation = nextBitPermutation(permutation);
result += permResult;
} while(permutation < (1 << nrM) && permutation != 0);
}
if(invResults) {
result = storm::utility::one<ValueType>() - result;
STORM_LOG_TRACE("Result for permutation:"<<permResult);
permutation = nextBitPermutation(permutation);
result += permResult;
} while(permutation < (1 << nrM) && permutation != 0);
}
if(invResults) {
result = storm::utility::one<ValueType>() - result;
}
return result;
}
return result;
}
}
@ -132,6 +141,137 @@ namespace storm {
return checkDFT(dft, formula, symred, enableDC, approximationError);
}
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> DFTModelChecker<ValueType>::buildModelComposition(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC) {
STORM_LOG_TRACE("Build model via composition");
// Use parallel composition for CTMCs for expected time
STORM_LOG_ASSERT(formula->isTimeOperatorFormula(), "Formula is not a time operator formula");
bool modularisationPossible = allowModularisation;
// Try modularisation
if(modularisationPossible) {
std::vector<storm::storage::DFT<ValueType>> dfts;
bool isAnd = true;
switch (dft.topLevelType()) {
case storm::storage::DFTElementType::AND:
STORM_LOG_TRACE("top modularisation called AND");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules.");
modularisationPossible = dfts.size() > 1;
isAnd = true;
break;
case storm::storage::DFTElementType::OR:
STORM_LOG_TRACE("top modularisation called OR");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
modularisationPossible = dfts.size() > 1;
isAnd = false;
break;
case storm::storage::DFTElementType::VOT:
/*STORM_LOG_TRACE("top modularisation called VOT");
dfts = dft.topModularisation();
STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules.");
std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dft.getTopLevelGate())->threshold();
*/
// TODO enable modularisation for voting gate
modularisationPossible = false;
break;
default:
// No static gate -> no modularisation applicable
modularisationPossible = false;
break;
}
if(modularisationPossible) {
STORM_LOG_TRACE("Recursive CHECK Call");
bool firstTime = true;
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> composedModel;
for (auto const ft : dfts) {
STORM_LOG_INFO("Building Model via parallel composition...");
std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now();
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
if(symred) {
auto colouring = ft.colourDFT();
symmetries = ft.findSymmetries(colouring);
STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
}
// Build a single CTMC
STORM_LOG_INFO("Building Model...");
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(ft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
explorationTime += std::chrono::high_resolution_clock::now() - checkingStart;
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
ctmc = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(ctmc, {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
if (firstTime) {
composedModel = ctmc;
firstTime = false;
} else {
composedModel = storm::builder::ParallelCompositionBuilder<ValueType>::compose(composedModel, ctmc, isAnd);
}
// Apply bisimulation
std::chrono::high_resolution_clock::time_point bisimulationStart = std::chrono::high_resolution_clock::now();
composedModel = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now();
bisimulationTime += bisimulationEnd - bisimulationStart;
STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions());
if (composedModel->getNumberOfStates() <= 15) {
STORM_LOG_TRACE("Transition matrix: " << std::endl << composedModel->getTransitionMatrix());
} else {
STORM_LOG_TRACE("Transition matrix: too big to print");
}
}
return composedModel;
}
}
// If we are here, no composition was possible
STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible.");
std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now();
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
if(symred) {
auto colouring = dft.colourDFT();
symmetries = dft.findSymmetries(colouring);
STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries.");
STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries);
}
// Build a single CTMC
STORM_LOG_INFO("Building Model...");
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
builder.buildModel(labeloptions, 0, 0.0);
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = builder.getModel();
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
explorationTime += std::chrono::high_resolution_clock::now() - checkingStart;
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
return model->template as<storm::models::sparse::Ctmc<ValueType>>();
}
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_result DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC, double approximationError) {
std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now();
@ -213,7 +353,7 @@ namespace storm {
if (storm::settings::getModule<storm::settings::modules::DFTSettings>().isApproximationErrorSet()) {
storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
builder.buildModel(labeloptions, 0);
builder.buildModel(labeloptions, 0, 0.0);
model = builder.getModel();
} else {
storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);

14
src/modelchecker/dft/DFTModelChecker.h

@ -83,6 +83,20 @@ namespace storm {
*/
dft_result checkHelper(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError);
/*!
* Internal helper for building a CTMC from a DFT via parallel composition.
*
* @param dft DFT
* @param formula Formula to check for
* @param symred Flag indicating if symmetry reduction should be used
* @param allowModularisation Flag indication if modularisation is allowed
* @param enableDC Flag indicating if dont care propagation should be used
* @param approximationError Error allowed for approximation. Value 0 indicates no approximation
*
* @return CTMC representing the DFT
*/
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> buildModelComposition(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC);
/*!
* Check model generated from DFT.
*

2
src/storage/dft/DFT.cpp

@ -244,7 +244,7 @@ namespace storm {
for(auto const& child : children) {
std::vector<size_t> isubdft;
if(child->nrParents() > 1 || child->hasOutgoingDependencies() || child->hasRestrictions()) {
STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation.");
STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation.");
return {*this};
}
if (isGate(child->id())) {

6
src/storm-dyftee.cpp

@ -142,7 +142,6 @@ int main(const int argc, const char** argv) {
// Construct pctlFormula
std::string pctlFormula = "";
bool allowModular = true;
std::string operatorType = "";
std::string targetFormula = "";
@ -153,7 +152,6 @@ int main(const int argc, const char** argv) {
STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
operatorType = "T";
targetFormula = "F \"failed\"";
allowModular = false;
} else if (dftSettings.usePropProbability()) {
STORM_LOG_THROW(!dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
operatorType = "P";;
@ -180,9 +178,9 @@ int main(const int argc, const char** argv) {
// From this point on we are ready to carry out the actual computations.
if (parametric) {
analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
} else {
analyzeDFT<double>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
analyzeDFT<double>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), dftSettings.useModularisation(), !dftSettings.isDisableDC(), approximationError);
}
// All operations have now been performed, so we clean up everything and terminate.

|||||||
100:0
Loading…
Cancel
Save