Merge branch 'master' into almostsurepomdp

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();

src/storm-dft/builder/ExplicitDFTModelBuilder.cpp

@@ -59,14 +59,14 @@ namespace storm {
                     // Consider all children of the top level gate
                     std::vector<size_t> 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<ValueType>(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<ValueType>(rate)) {
+                                    // Get active failure rate for cold BE
                                     auto beExp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>(be);
                                     rate = beExp->activeFailureRate();
                                     STORM_LOG_ASSERT(!storm::utility::isZero<ValueType>(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

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()};

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;
             }
 
             /*!

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<DdType, ValueType>(model, input, mpi);
-                if (preprocessingResult.changed) {
-                    model = preprocessingResult.model;
-
-                    if (preprocessingResult.formulas) {
-                        std::vector<storm::jani::Property> 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);

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<storm::models::sparse::Pomdp<ValueType>>(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);
                 }

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());
                 

src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp

@@ -4,7 +4,7 @@
 namespace storm {
     namespace simulator {
         template<typename ValueType, typename RewardModelType>
-        DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::DiscreteTimeSparseModelSimulator(storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), currentState(*model.getInitialStates().begin()) {
+        DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::DiscreteTimeSparseModelSimulator(storm::models::sparse::Model<ValueType, RewardModelType> 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<double>;
     }
-}
+}

src/storm/storage/SparseMatrix.cpp

@@ -406,7 +406,12 @@ namespace storm {
         }
         
         template<typename ValueType>
-        SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, ValueType>>&& columnsAndValues, boost::optional<std::vector<index_type>>&& 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<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type>&& rowIndications, std::vector<MatrixEntry<index_type, ValueType>>&& columnsAndValues, boost::optional<std::vector<index_type>>&& 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();
         }
         

src/storm/storage/expressions/Expression.cpp

@@ -133,9 +133,12 @@ namespace storm {
         
         bool Expression::containsVariable(std::set<storm::expressions::Variable> const& variables) const {
             std::set<storm::expressions::Variable> appearingVariables = this->getVariables();
-            std::set<storm::expressions::Variable> 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<storm::expressions::Variable> const& variables) const {

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;

src/storm/storage/jani/JaniScopeChanger.cpp

@@ -24,6 +24,9 @@ namespace storm {
                     bool* result = boost::any_cast<bool *>(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<uint64_t> 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<bool, uint64_t> JaniScopeChanger::canMakeVariableLocal(storm::expressions::Variable const& variable, Model const& model, std::vector<Property> const& properties, boost::optional<uint64_t> 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};
         }
         

src/storm/utility/random.cpp

@@ -10,7 +10,7 @@ namespace storm {
         }
 
         RandomProbabilityGenerator<double>::RandomProbabilityGenerator(uint64_t seed)
-        : engine(seed), distribution(0.0, 1.0)
+        : distribution(0.0, 1.0), engine(seed)
         {
 
         }
@@ -21,4 +21,4 @@ namespace storm {
 
 
     }
-}
+}

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"