diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp similarity index 94% rename from src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp rename to src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index c7d6605f5..2b74432ad 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -1,4 +1,4 @@ -#include "ExplicitDFTModelBuilderApprox.h" +#include "ExplicitDFTModelBuilder.h" #include @@ -17,18 +17,18 @@ namespace storm { namespace builder { template - ExplicitDFTModelBuilderApprox::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { + ExplicitDFTModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), markovianStates(), exitRates(), choiceLabeling() { // Intentionally left empty. } template - ExplicitDFTModelBuilderApprox::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) { + ExplicitDFTModelBuilder::MatrixBuilder::MatrixBuilder(bool canHaveNondeterminism) : mappingOffset(0), stateRemapping(), currentRowGroup(0), currentRow(0), canHaveNondeterminism((canHaveNondeterminism)) { // Create matrix builder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, canHaveNondeterminism, 0); } template - ExplicitDFTModelBuilderApprox::LabelOptions::LabelOptions(std::vector> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) { + ExplicitDFTModelBuilder::LabelOptions::LabelOptions(std::vector> properties, bool buildAllLabels) : buildFailLabel(true), buildFailSafeLabel(false), buildAllLabels(buildAllLabels) { // Get necessary labels from properties std::vector> atomicLabels; for (auto property : properties) { @@ -51,7 +51,7 @@ namespace storm { } template - ExplicitDFTModelBuilderApprox::ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : + ExplicitDFTModelBuilder::ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC) : dft(dft), stateGenerationInfo(std::make_shared(dft.buildStateGenerationInfo(symmetries))), enableDC(enableDC), @@ -124,7 +124,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) { + void ExplicitDFTModelBuilder::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) { STORM_LOG_TRACE("Generating DFT state space"); if (iteration < 1) { @@ -156,7 +156,7 @@ namespace storm { } // Build initial state - this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1)); + this->stateStorage.initialStateIndices = generator.getInitialStates(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1)); STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed."); initialStateIndex = stateStorage.initialStateIndices[0]; STORM_LOG_TRACE("Initial state: " << initialStateIndex); @@ -214,7 +214,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::initializeNextIteration() { + void ExplicitDFTModelBuilder::initializeNextIteration() { STORM_LOG_TRACE("Refining DFT state space"); // TODO Matthias: should be easier now as skipped states all are at the end of the matrix @@ -316,7 +316,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::exploreStateSpace(double approximationThreshold) { + void ExplicitDFTModelBuilder::exploreStateSpace(double approximationThreshold) { size_t nrExpandedStates = 0; size_t nrSkippedStates = 0; // TODO Matthias: do not empty queue every time but break before @@ -364,7 +364,7 @@ namespace storm { } else { // Explore the current state ++nrExpandedStates; - storm::generator::StateBehavior behavior = generator.expand(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1)); + storm::generator::StateBehavior behavior = generator.expand(std::bind(&ExplicitDFTModelBuilder::getOrAddStateIndex, this, std::placeholders::_1)); STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty."); setMarkovian(behavior.begin()->isMarkovian()); @@ -424,7 +424,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::buildLabeling(LabelOptions const& labelOpts) { + void ExplicitDFTModelBuilder::buildLabeling(LabelOptions const& labelOpts) { // Build state labeling modelComponents.stateLabeling = storm::models::sparse::StateLabeling(modelComponents.transitionMatrix.getRowGroupCount()); // Initial state @@ -473,13 +473,13 @@ namespace storm { } template - std::shared_ptr> ExplicitDFTModelBuilderApprox::getModel() { + std::shared_ptr> ExplicitDFTModelBuilder::getModel() { STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states"); return createModel(false); } template - std::shared_ptr> ExplicitDFTModelBuilderApprox::getModelApproximation(bool lowerBound, bool expectedTime) { + std::shared_ptr> ExplicitDFTModelBuilder::getModelApproximation(bool lowerBound, bool expectedTime) { if (expectedTime) { // TODO Matthias: handle case with no skipped states changeMatrixBound(modelComponents.transitionMatrix, lowerBound); @@ -550,7 +550,7 @@ namespace storm { } template - std::shared_ptr> ExplicitDFTModelBuilderApprox::createModel(bool copy) { + std::shared_ptr> ExplicitDFTModelBuilder::createModel(bool copy) { std::shared_ptr> model; if (modelComponents.deterministicModel) { @@ -607,7 +607,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::changeMatrixBound(storm::storage::SparseMatrix & matrix, bool lowerBound) const { + void ExplicitDFTModelBuilder::changeMatrixBound(storm::storage::SparseMatrix & matrix, bool lowerBound) const { // Set lower bound for skipped states for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { auto matrixEntry = matrix.getRow(it->first, 0).begin(); @@ -632,7 +632,7 @@ namespace storm { } template - ValueType ExplicitDFTModelBuilderApprox::getLowerBound(DFTStatePointer const& state) const { + ValueType ExplicitDFTModelBuilder::getLowerBound(DFTStatePointer const& state) const { // Get the lower bound by considering the failure of all possible BEs ValueType lowerBound = storm::utility::zero(); for (size_t index = 0; index < state->nrFailableBEs(); ++index) { @@ -642,7 +642,7 @@ namespace storm { } template - ValueType ExplicitDFTModelBuilderApprox::getUpperBound(DFTStatePointer const& state) const { + ValueType ExplicitDFTModelBuilder::getUpperBound(DFTStatePointer const& state) const { if (state->hasFailed(dft.getTopLevelIndex())) { return storm::utility::zero(); } @@ -709,7 +709,7 @@ namespace storm { } template - ValueType ExplicitDFTModelBuilderApprox::computeMTTFAnd(std::vector const& rates, size_t size) const { + ValueType ExplicitDFTModelBuilder::computeMTTFAnd(std::vector const& rates, size_t size) const { ValueType result = storm::utility::zero(); if (size == 0) { return result; @@ -762,7 +762,7 @@ namespace storm { } template - StateType ExplicitDFTModelBuilderApprox::getOrAddStateIndex(DFTStatePointer const& state) { + StateType ExplicitDFTModelBuilder::getOrAddStateIndex(DFTStatePointer const& state) { StateType stateId; bool changed = false; @@ -811,7 +811,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::setMarkovian(bool markovian) { + void ExplicitDFTModelBuilder::setMarkovian(bool markovian) { if (matrixBuilder.getCurrentRowGroup() > modelComponents.markovianStates.size()) { // Resize BitVector modelComponents.markovianStates.resize(modelComponents.markovianStates.size() + INITIAL_BITVECTOR_SIZE); @@ -820,7 +820,7 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::printNotExplored() const { + void ExplicitDFTModelBuilder::printNotExplored() const { std::cout << "states not explored:" << std::endl; for (auto it : statesNotExplored) { std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl; @@ -829,10 +829,10 @@ namespace storm { // Explicitly instantiate the class. - template class ExplicitDFTModelBuilderApprox; + template class ExplicitDFTModelBuilder; #ifdef STORM_HAVE_CARL - template class ExplicitDFTModelBuilderApprox; + template class ExplicitDFTModelBuilder; #endif } // namespace builder diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h similarity index 98% rename from src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h rename to src/storm-dft/builder/ExplicitDFTModelBuilder.h index 802aefe1b..b96dea410 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -26,7 +26,7 @@ namespace storm { * Build a Markov chain from DFT. */ template - class ExplicitDFTModelBuilderApprox { + class ExplicitDFTModelBuilder { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable @@ -177,7 +177,7 @@ namespace storm { * @param symmetries Symmetries in the dft. * @param enableDC Flag indicating if dont care propagation should be used. */ - ExplicitDFTModelBuilderApprox(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); + ExplicitDFTModelBuilder(storm::storage::DFT const& dft, storm::storage::DFTIndependentSymmetries const& symmetries, bool enableDC); /*! * Build model from DFT. diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 3a69cb5e4..d2b435c1c 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -5,7 +5,7 @@ #include "storm/utility/bitoperations.h" #include "storm/utility/DirectEncodingExporter.h" -#include "storm-dft/builder/ExplicitDFTModelBuilderApprox.h" +#include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" @@ -191,8 +191,8 @@ namespace storm { // Build a single CTMC STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(ft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + storm::builder::ExplicitDFTModelBuilder builder(ft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); explorationTimer.stop(); @@ -243,9 +243,8 @@ namespace storm { // Build a single CTMC STORM_LOG_INFO("Building Model..."); - - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); model->printModelInformationToStream(std::cout); @@ -276,8 +275,8 @@ namespace storm { approximation_result approxResult = std::make_pair(storm::utility::zero(), storm::utility::zero()); std::shared_ptr> model; std::vector newResult; - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties); // TODO Matthias: compute approximation for all properties simultaneously? std::shared_ptr property = properties[0]; @@ -341,8 +340,8 @@ namespace storm { } else { // Build a single Markov Automaton STORM_LOG_INFO("Building Model..."); - storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); - typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); + storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); + typename storm::builder::ExplicitDFTModelBuilder::LabelOptions labeloptions(properties, storm::settings::getModule().isExportExplicitSet()); builder.buildModel(labeloptions, 0, 0.0); std::shared_ptr> model = builder.getModel(); model->printModelInformationToStream(std::cout);