diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 5d835b4c7..87338ff30 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -87,6 +87,7 @@ void processOptions() { // Apply transformations // TODO transform later before actual analysis dft = storm::api::applyTransformations(*dft, faultTreeSettings.isUniqueFailedBE(), true); + STORM_LOG_DEBUG(dft->getElementsString()); dft->setDynamicBehaviorInfo(); diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index b5ed7c298..1f5f3c18f 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -59,14 +59,14 @@ namespace storm { // Consider all children of the top level gate std::vector isubdft; if (child->nrParents() > 1 || child->hasOutgoingDependencies()) { - STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); + STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation."); isubdft.clear(); } else if (dft.isGate(child->id())) { isubdft = dft.getGate(child->id())->independentSubDft(false); } else { STORM_LOG_ASSERT(dft.isBasicElement(child->id()), "Child is no BE."); if(dft.getBasicElement(child->id())->hasIngoingDependencies()) { - STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); + STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation."); isubdft.clear(); } else { isubdft = {child->id()}; @@ -745,37 +745,35 @@ namespace storm { storm::storage::BitVector coldBEs(subtree.size(), false); for (size_t i = 0; i < subtree.size(); ++i) { size_t id = subtree[i]; + // Consider only still operational BEs if (state->isOperational(id)) { - // Get BE rate - ValueType rate = state->getBERate(id); - if (storm::utility::isZero(rate)) { - // Get active failure rate for cold BE - auto be = dft.getBasicElement(id); - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: - { + auto be = dft.getBasicElement(id); + switch (be->type()) { + case storm::storage::DFTElementType::BE_EXP: + { + // Get BE rate + ValueType rate = state->getBERate(id); + if (storm::utility::isZero(rate)) { + // Get active failure rate for cold BE auto beExp = std::static_pointer_cast const>(be); rate = beExp->activeFailureRate(); STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Failure rate should not be zero."); // Mark BE as cold coldBEs.set(i, true); - break; } - case storm::storage::DFTElementType::BE_CONST: - { - // Ignore BE which cannot fail - continue; - } - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); - break; + rates.push_back(rate); + rateSum += rate; + break; } + case storm::storage::DFTElementType::BE_CONST: + // Ignore BE which cannot fail + continue; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); + break; } - rates.push_back(rate); - rateSum += rate; } } - STORM_LOG_ASSERT(rates.size() > 0, "No rates failable"); // Sort rates diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index daa6c33f2..6b79e1c1e 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -416,7 +416,7 @@ namespace storm { } else { STORM_LOG_ASSERT(isBasicElement(child->id()), "Child is no BE."); if (getBasicElement(child->id())->hasIngoingDependencies()) { - STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); + STORM_LOG_TRACE("child " << child->name() << " does not allow modularisation."); return {*this}; } else { isubdft = {child->id()}; diff --git a/src/storm-dft/storage/dft/elements/BEExponential.h b/src/storm-dft/storage/dft/elements/BEExponential.h index 8347f3179..1ed6221d6 100644 --- a/src/storm-dft/storage/dft/elements/BEExponential.h +++ b/src/storm-dft/storage/dft/elements/BEExponential.h @@ -67,7 +67,8 @@ namespace storm { } bool canFail() const override { - return !storm::utility::isZero(this->activeFailureRate()); + STORM_LOG_ASSERT(!storm::utility::isZero(this->activeFailureRate()), "BEExp should have failure rate > 0"); + return true; } /*! diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 4ae3fde89..fbb8c5971 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -582,28 +582,6 @@ namespace storm { STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); - - - if (model) { - auto preprocessingResult = storm::pars::preprocessModel(model, input, mpi); - if (preprocessingResult.changed) { - model = preprocessingResult.model; - - if (preprocessingResult.formulas) { - std::vector newProperties; - for (size_t i = 0; i < preprocessingResult.formulas.get().size(); ++i) { - auto formula = preprocessingResult.formulas.get().at(i); - STORM_LOG_ASSERT(i < input.properties.size(), "Index " << i << " greater than number of properties."); - storm::jani::Property property = input.properties.at(i); - newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), property.getComment())); - } - input.properties = newProperties; - } - - model->printModelInformationToStream(std::cout); - } - } - if (monSettings.isMonotonicityAnalysisSet()) { // Simplify the model storm::utility::Stopwatch simplifyingWatch(true); diff --git a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp index 62314426c..783a4782a 100644 --- a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp +++ b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp @@ -148,7 +148,9 @@ namespace storm { newRewardModels, false, boost::none); modelcomponents.observabilityClasses = pomdp.getObservations(); - //modelcomponents.choiceLabeling = pomdp.getChoiceLabeling(); + modelcomponents.stateValuations = pomdp.getOptionalStateValuations(); + modelcomponents.choiceLabeling = pomdp.getChoiceLabeling(); + modelcomponents.choiceLabeling->permuteItems(permutation); return std::make_shared>(modelcomponents, true); } @@ -185,7 +187,15 @@ namespace storm { if (moreActionObservations.get(observation)) { // We have seen this observation previously with multiple actions. Error! // TODO provide more diagnostic information - STORM_LOG_THROW(false, storm::exceptions::AmbiguousModelException, "Observation " << observation << " sometimes provides multiple actions, but in state " << state << " provides one action."); + std::string stateval =""; + if (pomdp.hasStateValuations()) { + stateval = " (" + pomdp.getStateValuations().getStateInfo(state) + ") "; + } + std::string actionval= ""; + if (pomdp.hasChoiceLabeling()) { + actionval = *pomdp.getChoiceLabeling().getLabelsOfChoice(rowIndexFrom).begin(); + } + STORM_LOG_THROW(false, storm::exceptions::AmbiguousModelException, "Observation " << observation << " sometimes provides multiple actions, but in state " << state << stateval << " provides only one action " << actionval << "."); } oneActionObservations.set(observation); @@ -194,7 +204,15 @@ namespace storm { } else { if (oneActionObservations.get(observation)) { // We have seen this observation previously with one action. Error! - STORM_LOG_THROW(false, storm::exceptions::AmbiguousModelException, "Observation " << observation << " sometimes provides one action, but in state " << state << " provides multiple actions."); + std::string stateval =""; + if (pomdp.hasStateValuations()) { + stateval = " (" + pomdp.getStateValuations().getStateInfo(state) + ") "; + } +// std::string actionval= ""; +// if (pomdp.hasChoiceLabeling()) { +// actionval = *pomdp.getChoiceLabeling().getLabelsOfChoice(rowIndexFrom).begin(); +// } + STORM_LOG_THROW(false, storm::exceptions::AmbiguousModelException, "Observation " << observation << " sometimes provides one action, but in state " << state << stateval << " provides " << rowIndexTo - rowIndexFrom << " actions."); } moreActionObservations.set(observation); } diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 55cae421b..ab8912c5d 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -831,7 +831,7 @@ namespace storm { auto subEnv = env; if (subEnv.solver().getLinearEquationSolverType() == storm::solver::EquationSolverType::Topological) { // Topological solver does not make any sense since the BSCC is connected. - subEnv.solver().setLinearEquationSolverType(subEnv.solver().topological().getUnderlyingEquationSolverType()); + subEnv.solver().setLinearEquationSolverType(subEnv.solver().topological().getUnderlyingEquationSolverType(), subEnv.solver().topological().isUnderlyingEquationSolverTypeSetFromDefault()); } subEnv.solver().setLinearEquationSolverPrecision(env.solver().lra().getPrecision(), env.solver().lra().getRelativeTerminationCriterion()); @@ -926,7 +926,7 @@ namespace storm { auto subEnv = env; if (subEnv.solver().getLinearEquationSolverType() == storm::solver::EquationSolverType::Topological) { // Topological solver does not make any sense since the BSCC is connected. - subEnv.solver().setLinearEquationSolverType(subEnv.solver().topological().getUnderlyingEquationSolverType()); + subEnv.solver().setLinearEquationSolverType(subEnv.solver().topological().getUnderlyingEquationSolverType(), subEnv.solver().topological().isUnderlyingEquationSolverTypeSetFromDefault()); } subEnv.solver().setLinearEquationSolverPrecision(env.solver().lra().getPrecision(), env.solver().lra().getRelativeTerminationCriterion()); diff --git a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp index d8fd4a82a..2e9161b8a 100644 --- a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp +++ b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp @@ -4,7 +4,7 @@ namespace storm { namespace simulator { template - DiscreteTimeSparseModelSimulator::DiscreteTimeSparseModelSimulator(storm::models::sparse::Model const& model) : model(model), currentState(*model.getInitialStates().begin()) { + DiscreteTimeSparseModelSimulator::DiscreteTimeSparseModelSimulator(storm::models::sparse::Model const& model) : currentState(*model.getInitialStates().begin()), model(model) { STORM_LOG_WARN_COND(model.getInitialStates().getNumberOfSetBits()==1, "The model has multiple initial states. This simulator assumes it starts from the initial state with the lowest index."); } @@ -47,4 +47,4 @@ namespace storm { template class DiscreteTimeSparseModelSimulator; } -} \ No newline at end of file +} diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 59d158d96..26e1c0dc7 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -406,7 +406,12 @@ namespace storm { } template - SparseMatrix::SparseMatrix(index_type columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, boost::optional>&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), trivialRowGrouping(!rowGroupIndices), rowGroupIndices(std::move(rowGroupIndices)) { + SparseMatrix::SparseMatrix(index_type columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, boost::optional>&& rowGroupIndices) : columnCount(columnCount), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { + // Initialize some variables here which depend on other variables + // This way we are more robust against different initialization orders + this->rowCount = this->rowIndications.size() - 1; + this->entryCount = this->columnsAndValues.size(); + this->trivialRowGrouping = !this->rowGroupIndices; this->updateNonzeroEntryCount(); } diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index 0221628db..520bf1db4 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/src/storm/storage/expressions/Expression.cpp @@ -133,9 +133,12 @@ namespace storm { bool Expression::containsVariable(std::set const& variables) const { std::set appearingVariables = this->getVariables(); - std::set intersection; - std::set_intersection(variables.begin(), variables.end(), appearingVariables.begin(), appearingVariables.end(), std::inserter(intersection, intersection.begin())); - return !intersection.empty(); + for (auto const& v : variables) { + if (appearingVariables.count(v) > 0) { + return true; + } + } + return false; } bool Expression::containsVariableInITEGuard(std::set const& variables) const { diff --git a/src/storm/storage/expressions/ExpressionManager.cpp b/src/storm/storage/expressions/ExpressionManager.cpp index 219e5a521..07a44dd3b 100644 --- a/src/storm/storage/expressions/ExpressionManager.cpp +++ b/src/storm/storage/expressions/ExpressionManager.cpp @@ -324,7 +324,7 @@ namespace storm { out << "manager {" << std::endl; for (auto const& variableTypePair : manager) { - out << "\t" << variableTypePair.second << " " << variableTypePair.first.getName() << " [offset " << variableTypePair.first.getOffset() << "]" << std::endl; + out << "\t" << variableTypePair.second << " " << variableTypePair.first.getName() << " [offset " << variableTypePair.first.getOffset() << ", " << variableTypePair.first.getIndex() <<" ]" << std::endl; } out << "}" << std::endl; diff --git a/src/storm/storage/jani/JaniScopeChanger.cpp b/src/storm/storage/jani/JaniScopeChanger.cpp index 752dc033e..58e0bbbb1 100644 --- a/src/storm/storage/jani/JaniScopeChanger.cpp +++ b/src/storm/storage/jani/JaniScopeChanger.cpp @@ -24,6 +24,9 @@ namespace storm { bool* result = boost::any_cast(data); if (*result) { return; } *result = expression.containsVariable(varSet); + if (*result) { + STORM_LOG_TRACE("The expression " << expression << " 'contains' a variable in the variable set."); + } } private: @@ -34,6 +37,7 @@ namespace storm { std::set res; for (uint64_t i = 0; i < model.getNumberOfAutomata(); ++i) { if (model.getAutomaton(i).getVariables().hasVariable(variable)) { + STORM_LOG_TRACE("The automaton " << model.getAutomaton(i).getName() << " 'has' the variable " << variable.getName() << "."); res.insert(i); } else { VariableAccessedTraverser vat({variable}); @@ -41,6 +45,8 @@ namespace storm { vat.traverse(model.getAutomaton(i), &varAccessed); if (varAccessed) { res.insert(i); + STORM_LOG_TRACE("The automaton " << model.getAutomaton(i).getName() << " 'accesses' the variable " << variable.getName() << "."); + } } } @@ -72,6 +78,8 @@ namespace storm { } bool JaniScopeChanger::canMakeVariableGlobal(storm::expressions::Variable const& variable, Model const& model) const { + STORM_LOG_TRACE("Can the variable " << variable.getName() << " be made global?"); + if (model.hasGlobalVariable(variable.getName())) { return false; } @@ -87,8 +95,12 @@ namespace storm { } return foundVar; } - + + + std::pair JaniScopeChanger::canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model, std::vector const& properties, boost::optional automatonIndex) const { + STORM_LOG_TRACE("Can the variable " << variable.getName() << " be made local?"); + uint64_t index = model.getNumberOfAutomata(); if (!model.getGlobalVariables().hasVariable(variable)) { @@ -97,26 +109,32 @@ namespace storm { auto accessingAutomata = detail::getAutomataAccessingVariable(variable, model); if (accessingAutomata.size() > 1 || (automatonIndex.is_initialized() && accessingAutomata.count(automatonIndex.get()) == 0)) { + STORM_LOG_TRACE(".. no!, multiple automata access the variable, e.g. automata " << model.getAutomaton(*accessingAutomata.begin()).getName() << " and " << model.getAutomaton(*accessingAutomata.rbegin()).getName()); return {false, index}; } if (model.getInitialStatesRestriction().containsVariable({variable})) { + STORM_LOG_TRACE(".. no!, initial states restriction contains variable"); return {false, index}; } for (auto const& rewExp : model.getNonTrivialRewardExpressions()) { if (rewExp.second.containsVariable({variable})) { + STORM_LOG_TRACE(".. no!, non trivial reward expression "); return {false, index}; } } for (auto const& funDef : model.getGlobalFunctionDefinitions()) { if (funDef.second.getFunctionBody().containsVariable({variable})) { + STORM_LOG_TRACE(".. no!, function definition: "); return {false, index}; } } for (auto const& p : properties) { if (p.getUsedVariablesAndConstants().count(variable) > 0) { + STORM_LOG_TRACE(".. no!, used variables definition: "); return {false, index}; } if (p.getUsedLabels().count(variable.getName()) > 0) { + STORM_LOG_TRACE(".. no!, used labels definition: "); return {false, index}; } } @@ -127,6 +145,7 @@ namespace storm { index = *accessingAutomata.begin(); assert(!automatonIndex.is_initialized() || index == automatonIndex.get()); } + STORM_LOG_TRACE(".. Yes, made local in automaton with index " << index ); return {true, index}; } diff --git a/src/storm/utility/random.cpp b/src/storm/utility/random.cpp index 6f3464cdb..ad0afecb0 100644 --- a/src/storm/utility/random.cpp +++ b/src/storm/utility/random.cpp @@ -10,7 +10,7 @@ namespace storm { } RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) - : engine(seed), distribution(0.0, 1.0) + : distribution(0.0, 1.0), engine(seed) { } @@ -21,4 +21,4 @@ namespace storm { } -} \ No newline at end of file +} diff --git a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp index 0df0bea3f..87e670104 100755 --- a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp @@ -1,8 +1,6 @@ #include "test/storm_gtest.h" #include "storm-config.h" -#include "test/storm_gtest.h" - #include "storm/api/builder.h" #include "storm-conv/api/storm-conv.h" #include "storm-parsers/api/model_descriptions.h"