Merge remote-tracking branch 'origin/master' into janiTests

CHANGELOG.md

@@ -8,10 +8,15 @@ Version 1.2.x
 -------------
 
 ### Version 1.2.4 (2018/08)
-- New binary `storm-conv` that handles conversions between model files (currently: prism to jani)
+- Heavily extended JANI support, in particular:
+	 * arrays, functions, state-exit-rewards (all engines)
+	 * indexed assignments, complex reward expressions (sparse engine)
+	 * several jani-related bug fixes
+- New binary `storm-conv` that handles conversions between model files
+- New binary `storm-pomdp` that handles the translation of POMDPs to pMCs.
+- Closing a Markov automaton now removes unreachable states
 - Added support for expected time properties for discrete time models
 - Bug fix in the parser for DRN (MDPs and MAs might have been affected).
-- Several bug fixes related to jani
 - `storm-gspn`: Improved .pnpro parser
 - `storm-gspn`: Added support for single/infinite/k-server semantics for GSPNs given in the .pnpro format
 - `storm-gspn`: Added option to set a global capacity for all places

src/storm-conv/converter/options/JaniConversionOptions.cpp

@@ -5,7 +5,7 @@ namespace storm {
 
         JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) {
             // Intentionally left empty
-        };
+        }
 
         JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) {
             if (settings.isEliminateFunctionsSet()) {
@@ -14,7 +14,7 @@ namespace storm {
             if (settings.isEliminateArraysSet()) {
                 allowedModelFeatures.remove(storm::jani::ModelFeature::Arrays);
             }
-        };
+        }
     }
 }
 

src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp

@@ -6,7 +6,7 @@ namespace storm {
 
         PrismToJaniConverterOptions::PrismToJaniConverterOptions() : allVariablesGlobal(false), suffix("") {
             // Intentionally left empty
-        };
+        }
     }
 }
 

src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

@@ -1,6 +1,9 @@
 #include "DFTASFChecker.h"
 #include <string>
 #include "storm/utility/file.h"
+#include "storm/utility/bitoperations.h"
+#include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/NotSupportedException.h"
 
 namespace storm {
     
@@ -12,11 +15,9 @@ namespace storm {
         class IsMaximum : public DFTConstraint {
         public:
             IsMaximum(uint64_t varIndex, std::vector<uint64_t> const& varIndices) : varIndex(varIndex), varIndices(varIndices) {
-                
             }
             
             virtual ~IsMaximum() {
-                
             }
             
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
@@ -34,26 +35,23 @@ namespace storm {
                 sstr << ")"; // end of the or
                 sstr << ")"; // end outer and.
                 return sstr.str();
-                
             }
 
-                
         private:
             uint64_t varIndex;
             std::vector<uint64_t> varIndices;
         };
+
+
         /*
          * First is the minimum of the others
          */
         class IsMinimum : public DFTConstraint {
         public:
             IsMinimum(uint64_t varIndex, std::vector<uint64_t> const& varIndices) : varIndex(varIndex), varIndices(varIndices) {
-                        
             }
 
-                    
             virtual ~IsMinimum() {
-                        
             }
 
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
@@ -71,22 +69,19 @@ namespace storm {
                 sstr << ")"; // end of the or
                 sstr << ")"; // end outer and.
                 return sstr.str();
-                        
             }
 
-                    
         private:
             uint64_t varIndex;
             std::vector<uint64_t> varIndices;
         };
                 
+
         class BetweenValues : public DFTConstraint {
         public:
             BetweenValues(uint64_t varIndex, uint64_t lower, uint64_t upper) : varIndex(varIndex), upperBound(upper) , lowerBound(lower) {
-                        
             }
             virtual ~BetweenValues() {
-                        
             }
 
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
@@ -104,34 +99,83 @@ namespace storm {
             uint64_t lowerBound;
         };
 
+
         class And : public DFTConstraint {
         public:
-                    And(std::vector<std::shared_ptr<DFTConstraint>> const& constraints) : constraints(constraints) {}
-                    
+            And(std::vector<std::shared_ptr<DFTConstraint>> const& constraints) : constraints(constraints) {
+            }
             virtual ~And() {
-                        
             }
 
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
                 std::stringstream sstr;
+                if (constraints.empty()) {
+                    sstr << "true";
+                } else {
                     sstr << "(and";
                     for(auto const& c : constraints) {
                         sstr << " " << c->toSmtlib2(varNames);
                     }
                     sstr << ")";
+                }
                 return sstr.str();
             }
+
         private:
             std::vector<std::shared_ptr<DFTConstraint>> constraints;
 
         };
 
-                class Iff : public DFTConstraint {
+
+        class Or : public DFTConstraint {
         public:
-                    Iff(std::shared_ptr<DFTConstraint> l, std::shared_ptr<DFTConstraint> r) : lhs(l), rhs(r) {
+            Or(std::vector<std::shared_ptr<DFTConstraint>> const& constraints) : constraints(constraints) {
+            }
+
+            virtual ~Or() {
+            }
+
+            std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                std::stringstream sstr;
+                if (constraints.empty()) {
+                    sstr << "false";
+                } else {
+                    sstr << "(or";
+                    for(auto const& c : constraints) {
+                        sstr << " " << c->toSmtlib2(varNames);
+                    }
+                    sstr << ")";
+                }
+                return sstr.str();
+            }
+
+        private:
+            std::vector<std::shared_ptr<DFTConstraint>> constraints;
+
+        };
+
 
+        class Implies : public DFTConstraint {
+        public:
+            Implies(std::shared_ptr<DFTConstraint> l, std::shared_ptr<DFTConstraint> r) : lhs(l), rhs(r) {
             }
 
+            std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                std::stringstream sstr;
+                sstr << "(=> " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")";
+                return sstr.str();
+            }
+
+        private:
+            std::shared_ptr<DFTConstraint> lhs;
+            std::shared_ptr<DFTConstraint> rhs;
+        };
+
+
+        class Iff : public DFTConstraint {
+        public:
+            Iff(std::shared_ptr<DFTConstraint> l, std::shared_ptr<DFTConstraint> r) : lhs(l), rhs(r) {
+            }
 
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
                 std::stringstream sstr;
@@ -144,14 +188,57 @@ namespace storm {
             std::shared_ptr<DFTConstraint> rhs;
         };
 
+
+        class IsTrue : public DFTConstraint {
+        public:
+            IsTrue(bool val) :value(val) {
+            }
+
+            virtual ~IsTrue() {
+            }
+
+            std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                std::stringstream sstr;
+                sstr << (value ? "true" : "false");
+                return sstr.str();
+            }
+
+        private:
+            bool value;
+        };
+
+
+        class IsBoolValue : public DFTConstraint {
+        public:
+            IsBoolValue(uint64_t varIndex, bool val) : varIndex(varIndex), value(val) {
+            }
+
+            virtual ~IsBoolValue() {
+            }
+
+            std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                std::stringstream sstr;
+                assert(varIndex < varNames.size());
+                if (value) {
+                    sstr << varNames.at(varIndex);
+                } else {
+                    sstr << "(not " << varNames.at(varIndex) << ")";
+                }
+                return sstr.str();
+            }
+
+        private:
+            uint64_t varIndex;
+            bool value;
+        };
+
+
         class IsConstantValue : public DFTConstraint {
         public:
             IsConstantValue(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) {
-                        
             }
 
             virtual ~IsConstantValue() {
-                        
             }
 
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
@@ -166,18 +253,58 @@ namespace storm {
             uint64_t value;
         };
 
+
+        class IsLessConstant : public DFTConstraint {
+        public:
+            IsLessConstant(uint64_t varIndex, uint64_t val) :varIndex(varIndex), value(val) {
+            }
+
+            virtual ~IsLessConstant() {
+            }
+
+            std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                std::stringstream sstr;
+                assert(varIndex < varNames.size());
+                sstr << "(< " << varNames.at(varIndex) << " " << value << ")";
+                return sstr.str();
+            }
+
+        private:
+            uint64_t varIndex;
+            uint64_t value;
+        };
+
+        class IsLessEqualConstant : public DFTConstraint {
+        public:
+            IsLessEqualConstant(uint64_t varIndex, uint64_t val) :varIndex(varIndex), value(val) {
+            }
+
+            virtual ~IsLessEqualConstant() {
+            }
+
+            std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
+                std::stringstream sstr;
+                assert(varIndex < varNames.size());
+                sstr << "(<= " << varNames.at(varIndex) << " " << value << ")";
+                return sstr.str();
+            }
+
+        private:
+            uint64_t varIndex;
+            uint64_t value;
+        };
+
+
         class IsEqual : public DFTConstraint {
         public:
             IsEqual(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) {
-                        
             }
 
             virtual ~IsEqual() {
-                        
             }
 
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
-                        return "(= " + varNames.at(var1Index) + " " +  varNames.at(var2Index) + " )";
+                return "(= " + varNames.at(var1Index) + " " +  varNames.at(var2Index) + ")";
             }
 
         private:
@@ -185,18 +312,17 @@ namespace storm {
             uint64_t var2Index;
         };
 
-                class IsLEqual : public DFTConstraint {
-                public:
-                    IsLEqual(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) {
 
+        class IsLess : public DFTConstraint {
+        public:
+            IsLess(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) {
             }
 
-                    virtual ~IsLEqual() {
-                        
+            virtual ~IsLess() {
             }
 
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
-                        return "(<= " + varNames.at(var1Index) + " " +  varNames.at(var2Index) + " )";
+                return "(< " + varNames.at(var1Index) + " " +  varNames.at(var2Index) + ")";
             }
 
         private:
@@ -204,13 +330,12 @@ namespace storm {
             uint64_t var2Index;
         };
 
+
         class PairwiseDifferent : public DFTConstraint {
         public:
             PairwiseDifferent(std::vector<uint64_t> const& indices) : varIndices(indices) {
-                        
             }
             virtual ~PairwiseDifferent() {
-                        
             }
 
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
@@ -232,14 +357,13 @@ namespace storm {
             std::vector<uint64_t> varIndices;
         };
 
+
         class Sorted : public DFTConstraint {
         public:
             Sorted(std::vector<uint64_t> varIndices) : varIndices(varIndices) {
-                        
             }
 
             virtual ~Sorted() {
-                        
             }
 
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
@@ -252,15 +376,14 @@ namespace storm {
                 return sstr.str();
             }
 
-                    
         private:
             std::vector<uint64_t> varIndices;
         };
 
+
         class IfThenElse : public DFTConstraint {
         public:
             IfThenElse(std::shared_ptr<DFTConstraint> ifC, std::shared_ptr<DFTConstraint> thenC, std::shared_ptr<DFTConstraint> elseC) : ifConstraint(ifC), thenConstraint(thenC), elseConstraint(elseC) {
-                        
             }
 
             std::string toSmtlib2(std::vector<std::string> const& varNames) const override {
@@ -285,9 +408,10 @@ namespace storm {
         }
 
         void DFTASFChecker::convert() {
-                    
             std::vector<uint64_t> beVariables;
-                    // Convert all elements
+            notFailed = dft.nrBasicElements()+1; // Value indicating the element is not failed
+
+            // Initialize variables
             for (size_t i = 0; i < dft.nrElements(); ++i) {
                 std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
                 varNames.push_back("t_" + element->name());
@@ -309,91 +433,307 @@ namespace storm {
                         break;
                 }
             }
+            // Initialize variables indicating Markovian states
+            for (size_t i = 0; i < dft.nrBasicElements(); ++i) {
+                varNames.push_back("m_" + std::to_string(i));
+                markovianVariables.emplace(i, varNames.size() - 1);
+            }
 
-                    // BE
-                    constraints.push_back(std::make_shared<PairwiseDifferent>(beVariables));
-                    constraints.back()->setDescription("No two BEs fail at the same time");
-                    for( auto const& beV : beVariables) {
+
+            // Generate constraints
+
+            // All BEs have to fail (first part of constraint 12)
+            for (auto const& beV : beVariables) {
                 constraints.push_back(std::make_shared<BetweenValues>(beV, 1, dft.nrBasicElements()));
             }
 
-                    // Claim variables
-                    for (auto const& csvV : claimVariables) {
-                        constraints.push_back(std::make_shared<BetweenValues>(csvV.second, 0, dft.nrBasicElements() + 1));
+            // No two BEs fail at the same time (second part of constraint 12)
+            constraints.push_back(std::make_shared<PairwiseDifferent>(beVariables));
+            constraints.back()->setDescription("No two BEs fail at the same time");
+
+            // Initialize claim variables in [1, |BE|+1]
+            for (auto const& claimVariable : claimVariables) {
+                constraints.push_back(std::make_shared<BetweenValues>(claimVariable.second, 0, notFailed));
             }
 
+            // Encoding for gates
             for (size_t i = 0; i < dft.nrElements(); ++i) {
                 std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
-                        if(element->isSpareGate()) {
-                            auto spare = std::static_pointer_cast<storm::storage::DFTSpare<double> const>(element);
-                            auto const& spareChild = spare->children().front();
-                            constraints.push_back(std::make_shared<IsConstantValue>(getClaimVariableIndex(spare->id(), spareChild->id()), 0));
-                            constraints.back()->setDescription("Spare " + spare->name() + " claims first child");
-                            
-                        }
-                    }
+                STORM_LOG_ASSERT(i == element->id(), "Id and index should match.");
 
-                    
-                    for (size_t i = 0; i < dft.nrElements(); ++i) {
+                // Get indices for gate children
                 std::vector<uint64_t> childVarIndices;
-                        if (dft.isGate(i)) {
+                if (element->isGate()) {
                     std::shared_ptr<storm::storage::DFTGate<ValueType> const> gate = dft.getGate(i);
                     for (auto const& child : gate->children()) {
                         childVarIndices.push_back(timePointVariables.at(child->id()));
                     }
                 }
 
-                        std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
                 switch (element->type()) {
+                    case storm::storage::DFTElementType::BE:
+                        // BEs were already considered before
+                        break;
                     case storm::storage::DFTElementType::AND:
+                        // Constraint for AND gate (constraint 1)
                         constraints.push_back(std::make_shared<IsMaximum>(timePointVariables.at(i), childVarIndices));
-                                constraints.back()->setDescription("And gate");
+                        constraints.back()->setDescription("AND gate " + element->name());
                         break;
                     case storm::storage::DFTElementType::OR:
+                        // Constraint for OR gate (constraint 2)
                         constraints.push_back(std::make_shared<IsMinimum>(timePointVariables.at(i), childVarIndices));
-                                constraints.back()->setDescription("Or gate");
+                        constraints.back()->setDescription("OR gate " + element->name());
+                        break;
+                    case storm::storage::DFTElementType::VOT:
+                    {
+                        // VOTs are implemented via OR over ANDs with all possible combinations
+                        auto vot = std::static_pointer_cast<storm::storage::DFTVot<double> const>(element);
+                        std::vector<uint64_t> tmpVars;
+                        size_t k = 0;
+                        // Generate all permutations of k out of n
+                        size_t combination = smallestIntWithNBitsSet(static_cast<size_t>(vot->threshold()));
+                        do {
+                            // Construct selected children from combination
+                            std::vector<uint64_t> combinationChildren;
+                            for (size_t j = 0; j < vot->nrChildren(); ++j) {
+                                if (combination & (1 << j)) {
+                                    combinationChildren.push_back(childVarIndices.at(j));
+                                }
+                            }
+                            // Introduce temporary variable for this AND
+                            varNames.push_back("v_" + vot->name() + "_" + std::to_string(k));
+                            size_t index = varNames.size() - 1;
+                            tmpVars.push_back(index);
+                            tmpTimePointVariables.push_back(index);
+                            // AND over the selected children
+                            constraints.push_back(std::make_shared<IsMaximum>(index, combinationChildren));
+                            constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(k));
+                            // Generate next permutation
+                            combination = nextBitPermutation(combination);
+                            ++k;
+                        } while(combination < (1 << vot->nrChildren()) && combination != 0);
+
+                        // Constraint is OR over all possible combinations
+                        constraints.push_back(std::make_shared<IsMinimum>(timePointVariables.at(i), tmpVars));
+                        constraints.back()->setDescription("VOT gate " + element->name() + ": OR");
                         break;
+                    }
                     case storm::storage::DFTElementType::PAND:
-                                constraints.push_back(std::make_shared<IfThenElse>(std::make_shared<Sorted>(childVarIndices), std::make_shared<IsEqual>(timePointVariables.at(i), timePointVariables.at(childVarIndices.back())), std::make_shared<IsConstantValue>(timePointVariables.at(i), dft.nrBasicElements()+1)));
-                                constraints.back()->setDescription("Pand gate");
+                    {
+                        // Constraint for PAND gate (constraint 3)
+                        std::shared_ptr<DFTConstraint> ifC = std::make_shared<Sorted>(childVarIndices);
+                        std::shared_ptr<DFTConstraint> thenC = std::make_shared<IsEqual>(timePointVariables.at(i), childVarIndices.back());
+                        std::shared_ptr<DFTConstraint> elseC = std::make_shared<IsConstantValue>(timePointVariables.at(i), notFailed);
+                        constraints.push_back(std::make_shared<IfThenElse>(ifC, thenC, elseC));
+                        constraints.back()->setDescription("PAND gate " + element->name());
+                        break;
+                    }
+                    case storm::storage::DFTElementType::POR:
+                    {
+                        // Constraint for POR gate
+                        // First child fails before all others
+                        std::vector<std::shared_ptr<DFTConstraint>> firstSmallestC;
+                        uint64_t timeFirstChild = childVarIndices.front();
+                        for (uint64_t i = 1; i < childVarIndices.size(); ++i) {
+                            firstSmallestC.push_back(std::make_shared<IsLess>(timeFirstChild, childVarIndices.at(i)));
+                        }
+                        std::shared_ptr<DFTConstraint> ifC = std::make_shared<And>(firstSmallestC);
+                        std::shared_ptr<DFTConstraint> thenC = std::make_shared<IsEqual>(timePointVariables.at(i), childVarIndices.front());
+                        std::shared_ptr<DFTConstraint> elseC = std::make_shared<IsConstantValue>(timePointVariables.at(i), notFailed);
+                        constraints.push_back(std::make_shared<IfThenElse>(ifC, thenC, elseC));
+                        constraints.back()->setDescription("POR gate " + element->name());
+                        break;
+                    }
+                    case storm::storage::DFTElementType::SEQ:
+                    {
+                        // Constraint for SEQ gate (constraint 4)
+                        // As the restriction is not a gate we have to enumerate its children here
+                        auto seq = std::static_pointer_cast<storm::storage::DFTRestriction<double> const>(element);
+                        for (auto const& child : seq->children()) {
+                            childVarIndices.push_back(timePointVariables.at(child->id()));
+                        }
+
+                        constraints.push_back(std::make_shared<Sorted>(childVarIndices));
+                        constraints.back()->setDescription("SEQ gate " + element->name());
+                        break;
+                    }
                     case storm::storage::DFTElementType::SPARE:
                     {
                         auto spare = std::static_pointer_cast<storm::storage::DFTSpare<double> const>(element);
                         auto const& children = spare->children();
+                        uint64_t firstChild = children.front()->id();
+                        uint64_t lastChild = children.back()->id();
+
+                        // First child of each spare is claimed in the beginning
+                        constraints.push_back(std::make_shared<IsConstantValue>(getClaimVariableIndex(spare->id(), firstChild), 0));
+                        constraints.back()->setDescription("SPARE gate " + spare->name() + " claims first child");
 
-                                constraints.push_back(std::make_shared<Iff>(std::make_shared<IsLEqual>(getClaimVariableIndex(spare->id(), children.back()->id()), childVarIndices.back()), std::make_shared<IsEqual>(timePointVariables.at(i), childVarIndices.back())));
-                                constraints.back()->setDescription("Last child & claimed -> spare fails");
-                                
-                                std::shared_ptr<DFTConstraint> elseCase = nullptr;
-                                for( uint64_t j = 0; j < children.size(); ++j) {
-                                    uint64_t currChild = children.size() - 2 - j;
-                                    std::vector<std::shared_ptr<DFTConstraint>> ifcs;
-                                    uint64_t xv = childVarIndices.at(currChild); // if v is the child, xv is the time x fails.
-                                    uint64_t csn = getClaimVariableIndex(spare->id(), childVarIndices.at(currChild+1)); // csn is the moment the spare claims the next child
-                                    uint64_t xn = childVarIndices.at(currChild+1); // xn is the moment the next child fails
-                                    if (j == 0) {
-                                        elseCase = std::make_shared<IsEqual>(timePointVariables.at(i),  xv);
-                                    }
-                                    ifcs.push_back(std::make_shared<IsLEqual>(xv, xn));
-                                    for(auto const& otherSpare : children.at(currChild+1)->parents()) {
-                                        if(otherSpare->id() == i) { continue; }// not a OTHER spare.
-                                        ifcs.push_back(std::make_shared<IsConstantValue>(getClaimVariableIndex(otherSpare->id(), children.at(currChild+1)->id()), dft.nrBasicElements()+1));
-                                    }
-                                    std::shared_ptr<DFTConstraint> ite = std::make_shared<IfThenElse>(std::make_shared<And>(ifcs), std::make_shared<IsEqual>(csn, xv), elseCase);
-                                    elseCase = ite;
-                                    constraints.push_back(std::make_shared<Iff>(std::make_shared<IsLEqual>(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), xv), ite));
-                                    constraints.back()->setDescription(std::to_string(j+1) + " but last child & claimed");
+                        // If last child is claimed before failure, then the spare fails when the last child fails (constraint 5)
+                        std::shared_ptr<DFTConstraint> leftC = std::make_shared<IsLess>(getClaimVariableIndex(spare->id(), lastChild), childVarIndices.back());
+                        constraints.push_back(std::make_shared<Implies>(leftC, std::make_shared<IsEqual>(timePointVariables.at(i), childVarIndices.back())));
+                        constraints.back()->setDescription("Last child & claimed -> SPARE fails");
+
+                        // Construct constraint for trying to claim next child
+                        STORM_LOG_ASSERT(children.size() >= 2, "Spare has only one child");
+                        for (uint64_t currChild = 0; currChild < children.size() - 1; ++currChild) {
+                            uint64_t timeCurrChild = childVarIndices.at(currChild); // Moment when current child fails
+
+                            // If i-th child fails after being claimed, then try to claim next child (constraint 6)
+                            std::shared_ptr<DFTConstraint> tryClaimC = generateTryToClaimConstraint(spare, currChild + 1, timeCurrChild);
+                            constraints.push_back(std::make_shared<Iff>(std::make_shared<IsLess>(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), timeCurrChild), tryClaimC));
+                            constraints.back()->setDescription("Try to claim " + std::to_string(currChild+2) + "th child");
                         }
                         break;
                     }
+                    case storm::storage::DFTElementType::PDEP:
+                        // FDEPs are considered later in the Markovian constraints
+                        break;
                     default:
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "SMT encoding for type '" << element->type() << "' is not supported.");
                         break;
                 }
             }
 
-                    constraints.push_back(std::make_shared<IsConstantValue>(dft.getTopLevelIndex(), dft.nrBasicElements()+1));
+            // Only one spare can claim a child (constraint 8)
+            // and only not failed childs can be claimed (addition to constrain 8)
+            for (size_t i = 0; i < dft.nrElements(); ++i) {
+                std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
+                if (element->isSpareGate()) {
+                    auto spare = std::static_pointer_cast<storm::storage::DFTSpare<double> const>(element);
+                    for (auto const& child : spare->children()) {
+                        std::vector<std::shared_ptr<DFTConstraint>> additionalC;
+                        uint64_t timeClaiming = getClaimVariableIndex(spare->id(), child->id());
+                        std::shared_ptr<DFTConstraint> leftC = std::make_shared<IsLessConstant>(timeClaiming, notFailed);
+                        // Child must be operational at time of claiming
+                        additionalC.push_back(std::make_shared<IsLess>(timeClaiming, timePointVariables.at(child->id())));
+                        // No other spare claims this child
+                        for (auto const& parent : child->parents()) {
+                            if (parent->isSpareGate() && parent->id() != spare->id()) {
+                                // Different spare
+                                additionalC.push_back(std::make_shared<IsConstantValue>(getClaimVariableIndex(parent->id(), child->id()), notFailed));
+                            }
+                        }
+                        constraints.push_back(std::make_shared<Implies>(leftC, std::make_shared<And>(additionalC)));
+                        constraints.back()->setDescription("Child " + child->name() + " must be operational at time of claiming by spare " + spare->name() + " and can only be claimed by one spare.");
+                    }
+                }
+            }
+
+            // Handle dependencies
+            addMarkovianConstraints();
+
+            // Toplevel element will not fail (part of constraint 13)
+            constraints.push_back(std::make_shared<IsConstantValue>(timePointVariables.at(dft.getTopLevelIndex()), notFailed));
+            constraints.back()->setDescription("Toplevel element should not fail");
+        }
+
+        std::shared_ptr<DFTConstraint> DFTASFChecker::generateTryToClaimConstraint(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> spare, uint64_t childIndex, uint64_t timepoint) const {
+            auto child = spare->children().at(childIndex);
+            uint64_t timeChild = timePointVariables.at(child->id()); // Moment when the child fails
+            uint64_t claimChild = getClaimVariableIndex(spare->id(), child->id()); // Moment the spare claims the child
+
+            std::vector<std::shared_ptr<DFTConstraint>> noClaimingPossible;
+            // Child cannot be claimed.
+            if (childIndex + 1 < spare->children().size()) {
+                // Consider next child for claiming (second case in constraint 7)
+                noClaimingPossible.push_back(generateTryToClaimConstraint(spare, childIndex+1, timepoint));
+            } else {
+                // Last child: spare fails at same point as this child (third case in constraint 7)
+                noClaimingPossible.push_back(std::make_shared<IsEqual>(timePointVariables.at(spare->id()), timepoint));
+            }
+            std::shared_ptr<DFTConstraint> elseCaseC = std::make_shared<And>(noClaimingPossible);
+
+            // Check if next child is availble (first case in constraint 7)
+            std::vector<std::shared_ptr<DFTConstraint>> claimingPossibleC;
+            // Next child is not yet failed
+            claimingPossibleC.push_back(std::make_shared<IsLess>(timepoint, timeChild));
+            // Child is not yet claimed by a different spare
+            for (auto const& otherSpare : child->parents()) {
+                if (otherSpare->id() == spare->id()) {
+                    // not a different spare.
+                    continue;
+                }
+                claimingPossibleC.push_back(std::make_shared<IsConstantValue>(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed));
+            }
+
+            // Claim child if available
+            std::shared_ptr<DFTConstraint> firstCaseC = std::make_shared<IfThenElse>(std::make_shared<And>(claimingPossibleC), std::make_shared<IsEqual>(claimChild, timepoint), elseCaseC);
+            return firstCaseC;
         }
 
+        void DFTASFChecker::addMarkovianConstraints() {
+            uint64_t nrMarkovian = dft.nrBasicElements();
+            // Vector containing (non-)Markovian constraints for each timepoint
+            std::vector<std::vector<std::shared_ptr<DFTConstraint>>> markovianC(nrMarkovian);
+            std::vector<std::vector<std::shared_ptr<DFTConstraint>>> nonMarkovianC(nrMarkovian);
+            std::vector<std::vector<std::shared_ptr<DFTConstraint>>> notColdC(nrMarkovian);
+
+            // All dependent events of a failed trigger have failed as well (constraint 9)
+            for (size_t j = 0; j < dft.nrElements(); ++j) {
+                std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(j);
+                if (element->hasOutgoingDependencies()) {
+                    for (uint64_t i = 0; i < nrMarkovian; ++i) {
+                        std::shared_ptr<DFTConstraint> triggerFailed = std::make_shared<IsLessEqualConstant>(timePointVariables.at(j), i);
+                        std::vector<std::shared_ptr<DFTConstraint>> depFailed;
+                        for (auto const& dependency : element->outgoingDependencies()) {
+                            for (auto const& depElement : dependency->dependentEvents()) {
+                                depFailed.push_back(std::make_shared<IsLessEqualConstant>(timePointVariables.at(depElement->id()), i));
+                            }
+                        }
+                        markovianC[i].push_back(std::make_shared<Implies>(triggerFailed, std::make_shared<And>(depFailed)));
+                    }
+                }
+            }
+            for (uint64_t i = 0; i < nrMarkovian; ++i) {
+                constraints.push_back(std::make_shared<Iff>(std::make_shared<IsBoolValue>(markovianVariables.at(i), true), std::make_shared<And>(markovianC[i])));
+                constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") iff all dependent events which trigger failed also failed.");
+            }
+
+            // In non-Markovian steps the next failed element is a dependent BE (constraint 10)
+            for (size_t j = 0; j < dft.nrElements(); ++j) {
+                std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(j);
+                if (element->isBasicElement()) {
+                    auto be = std::static_pointer_cast<storm::storage::DFTBE<double> const>(element);
+
+                    if (be->hasIngoingDependencies()) {
+                        for (uint64_t i = 0; i < nrMarkovian -1; ++i) {
+                            std::shared_ptr<DFTConstraint> nextFailure = std::make_shared<IsConstantValue>(timePointVariables.at(j), i+1);
+                            std::vector<std::shared_ptr<DFTConstraint>> triggerFailed;
+                            for (auto const& dependency : be->ingoingDependencies()) {
+                                triggerFailed.push_back(std::make_shared<IsLessEqualConstant>(timePointVariables.at(dependency->triggerEvent()->id()), i));
+                            }
+                            nonMarkovianC[i].push_back(std::make_shared<Implies>(nextFailure, std::make_shared<Or>(triggerFailed)));
+                        }
+                    }
+                }
+            }
+            for (uint64_t i = 0; i < nrMarkovian; ++i) {
+                constraints.push_back(std::make_shared<Implies>(std::make_shared<IsBoolValue>(markovianVariables.at(i), false), std::make_shared<And>(nonMarkovianC[i])));
+                constraints.back()->setDescription("Non-Markovian (" + std::to_string(i) + ") -> next failure is dependent BE.");
+            }
+
+            // In Markovian steps the failure rate is positive (constraint 11)
+            for (size_t j = 0; j < dft.nrElements(); ++j) {
+                std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(j);
+                if (element->isBasicElement()) {
+                    auto be = std::static_pointer_cast<storm::storage::DFTBE<double> const>(element);
+                    for (uint64_t i = 0; i < nrMarkovian; ++i) {
+                        std::shared_ptr<DFTConstraint> nextFailure = std::make_shared<IsConstantValue>(timePointVariables.at(j), i+1);
+                        // BE is not cold
+                        // TODO: implement use of activation variables here
+                        bool cold = storm::utility::isZero<ValueType>(be->activeFailureRate());
+                        notColdC[i].push_back(std::make_shared<Implies>(nextFailure, std::make_shared<IsTrue>(!cold)));
+                    }
+                }
+            }
+            for (uint64_t i = 0; i < nrMarkovian; ++i) {
+                constraints.push_back(std::make_shared<Implies>(std::make_shared<IsBoolValue>(markovianVariables.at(i), true), std::make_shared<And>(notColdC[i])));
+                constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") -> positive failure rate.");
+            }
+
+        }
+
+
         void DFTASFChecker::toFile(std::string const& filename) {
             std::ofstream stream;
             storm::utility::openFile(filename, stream);
@@ -405,8 +745,20 @@ namespace storm {
             for (auto const& claimVarEntry : claimVariables) {
                 stream << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl;
             }
+            stream << "; Markovian variables" << std::endl;
+            for (auto const& markovianVarEntry : markovianVariables) {
+                stream << "(declare-fun " << varNames[markovianVarEntry.second] << "() Bool)" << std::endl;
+            }
+            if (!tmpTimePointVariables.empty()) {
+                stream << "; Temporary variables" << std::endl;
+                for (auto const& tmpVar : tmpTimePointVariables) {
+                    stream << "(declare-fun " << varNames[tmpVar] << "() Int)" << std::endl;
+                }
+            }
             for (auto const& constraint : constraints) {
+                if (!constraint->description().empty()) {
                     stream << "; " << constraint->description() << std::endl;
+                }
                 stream << "(assert " << constraint->toSmtlib2(varNames) << ")" << std::endl;
             }
             stream << "(check-sat)" << std::endl;

src/storm-dft/modelchecker/dft/DFTASFChecker.h

@@ -12,11 +12,13 @@ namespace storm {
         class DFTConstraint {
         public:
             virtual ~DFTConstraint() {
-                
             }
             
             virtual std::string toSmtlib2(std::vector<std::string> const& varNames) const = 0;
-            virtual std::string description() const { return descript; }
+
+            virtual std::string description() const {
+                return descript;
+            }
 
             void setDescription(std::string const& descr) {
                 descript = descr;
@@ -27,10 +29,8 @@ namespace storm {
         };
         
         class SpareAndChildPair {
-            
         public:
             SpareAndChildPair(uint64_t spareIndex, uint64_t childIndex) : spareIndex(spareIndex), childIndex(childIndex) {
-                
             }
             
             friend bool operator<(SpareAndChildPair const& p1, SpareAndChildPair const& p2) {
@@ -45,7 +45,6 @@ namespace storm {
         
         class DFTASFChecker {
             using ValueType = double;
-            
         public:
             DFTASFChecker(storm::storage::DFT<ValueType> const&);
             void convert();
@@ -54,11 +53,32 @@ namespace storm {
         private:
             uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const;
 
+            /**
+             * Generate constraint for 'spare (s) tries to claim the child (i) at the given timepoint (t)'.
+             * This corresponds to the function \phi^s_i(t) in constraint 7.
+             *
+             * @param spare Spare.
+             * @param childIndex Index of child to consider in spare children.
+             * @param timepoint Timepoint to try to claim.
+             *
+             * @return Constraint encoding the claiming.
+             */
+            std::shared_ptr<DFTConstraint> generateTryToClaimConstraint(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> spare, uint64_t childIndex, uint64_t timepoint) const;
+
+            /**
+             * Add constraints encoding Markovian states.
+             * This corresponds to constraints (9), (10) and (11)
+             */
+            void addMarkovianConstraints();
+            
             storm::storage::DFT<ValueType> const& dft;
             std::vector<std::string> varNames;
             std::unordered_map<uint64_t, uint64_t> timePointVariables;
             std::vector<std::shared_ptr<DFTConstraint>> constraints;
             std::map<SpareAndChildPair, uint64_t> claimVariables;
+            std::unordered_map<uint64_t, uint64_t> markovianVariables;
+            std::vector<uint64_t> tmpTimePointVariables;
+            uint64_t notFailed;
         };
     }
 }

src/storm-parsers/parser/JaniParser.cpp

@@ -205,7 +205,11 @@ namespace storm {
                 STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array");
                 for(auto const& propertyEntry : parsedStructure.at("properties")) {
                     try {
+                        nonTrivialRewardModelExpressions.clear();
                         auto prop = this->parseProperty(propertyEntry, scope.refine("property[" + std::to_string(properties.size()) + "]"));
+                        for (auto const& nonTrivRewExpr : nonTrivialRewardModelExpressions) {
+                            model.addNonTrivialRewardExpression(nonTrivRewExpr.first, nonTrivRewExpr.second);
+                        }
                         // Eliminate reward accumulations as much as possible
                         rewAccEliminator.eliminateRewardAccumulations(prop);
                         properties.push_back(prop);
@@ -321,7 +325,10 @@ namespace storm {
                         STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a reward-instant in " + scope.description);
 
                         storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), scope.refine("Step instant"));
-                        if(rewardAccumulation.isEmpty()) {
+                        if (!rewExpr.isVariable()) {
+                            nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
+                        }
+                        if (rewardAccumulation.isEmpty()) {
                              return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(stepInstantExpr, storm::logic::TimeBoundType::Steps), rewardName, opInfo);
                         } else {
                             return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps), rewardAccumulation), rewardName, opInfo);
@@ -329,7 +336,10 @@ namespace storm {
                     } else if (propertyStructure.count("time-instant") > 0) {
                         STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a time-instant and a reward-instant in " + scope.description);
                         storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), scope.refine("time instant"));
-                        if(rewardAccumulation.isEmpty()) {
+                        if (!rewExpr.isVariable()) {
+                            nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
+                        }
+                        if (rewardAccumulation.isEmpty()) {
                             return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(timeInstantExpr, storm::logic::TimeBoundType::Time), rewardName, opInfo);
                         } else {
                             return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time), rewardAccumulation), rewardName, opInfo);
@@ -349,6 +359,9 @@ namespace storm {
                             storm::expressions::Expression rewInstantExpr = parseExpression(rewInst.at("instant"), scope.refine("reward instant"));
                             bounds.emplace_back(false, rewInstantExpr);
                         }
+                        if (!rewExpr.isVariable()) {
+                            nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
+                        }
                         return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(bounds, boundReferences, rewardAccumulation), rewardName, opInfo);
                     } else {
                         time = !rewExpr.containsVariables() && storm::utility::isOne(rewExpr.evaluateAsRational());
@@ -363,11 +376,11 @@ namespace storm {
                             assert(subformula->isTotalRewardFormula() || subformula->isTimePathFormula());
                             return std::make_shared<storm::logic::TimeOperatorFormula>(subformula, opInfo);
                         } else {
-                            return std::make_shared<storm::logic::RewardOperatorFormula>(subformula, rewardName, opInfo);
+                            if (!rewExpr.isVariable()) {
+                                nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
                             }
+                            return std::make_shared<storm::logic::RewardOperatorFormula>(subformula, rewardName, opInfo);
                         }
-                    if (!time && !rewExpr.isVariable()) {
-                        nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr);
                     }
                 } else if (opString == "Smin" || opString == "Smax") {
                     STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported");
@@ -829,9 +842,9 @@ namespace storm {
                             }
                         } else {
                             if (type.bounds) {
-                                return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar);
-                            } else {
                                 return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), boost::none, false, type.bounds->first, type.bounds->second);
+                            } else {
+                                return std::make_shared<storm::jani::UnboundedIntegerVariable>(name, expressionManager->declareIntegerVariable(exprManagerName));
                             }
                         }
                         break;
@@ -1403,6 +1416,7 @@ namespace storm {
                     STORM_LOG_THROW(edgeEntry.at("rate").count("exp") == 1, storm::exceptions::InvalidJaniException, "Rate in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a defing expression.");
                     rateExpr = parseExpression(edgeEntry.at("rate").at("exp"), scope.refine("rate expression in edge from '" + sourceLoc));
                     STORM_LOG_THROW(rateExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Rate '" << rateExpr << "' has not a numerical type");
+                    STORM_LOG_THROW(rateExpr.containsVariables() || rateExpr.evaluateAsRational() > storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidJaniException, "Only positive rates are allowed but rate '" << rateExpr << " was found.");
                 }
                 // guard
                 STORM_LOG_THROW(edgeEntry.count("guard") <= 1, storm::exceptions::InvalidJaniException, "Guard can be given at most once in edge from '" << sourceLoc << "' in automaton '" << name << "'");

src/storm-parsers/parser/PrismParser.cpp

@@ -561,7 +561,6 @@ namespace storm {
             bool observable = this->observables.count(variableName) > 0;
             if(observable) {
                 this->observables.erase(variableName);
-                std::cout << variableName << " is observable." << std::endl;
             }
             return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, observable, this->getFilename());
         }
@@ -582,7 +581,6 @@ namespace storm {
             bool observable = this->observables.count(variableName) > 0;
             if(observable) {
                 this->observables.erase(variableName);
-                std::cout << variableName << " is observable." << std::endl;
             }
 
             return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable, this->getFilename());
@@ -613,7 +611,6 @@ namespace storm {
                     this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
                     if(this->observables.count(renamingPair->second) > 0) {
                         this->observables.erase(renamingPair->second);
-                        std::cout << renamingPair->second << " is observable." << std::endl;
                     }
                 }
                 for (auto const& variable : moduleToRename.getIntegerVariables()) {
@@ -623,7 +620,6 @@ namespace storm {
                     this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
                     if(this->observables.count(renamingPair->second) > 0) {
                         this->observables.erase(renamingPair->second);
-                        std::cout << renamingPair->second << " is observable." << std::endl;
                     }
                 }
                 
@@ -666,7 +662,6 @@ namespace storm {
                     bool observable = this->observables.count(renamingPair->second) > 0;
                     if(observable) {
                         this->observables.erase(renamingPair->second);
-                        std::cout << renamingPair->second << " is observable." << std::endl;
                     }
                     booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1)));
                 }
@@ -679,7 +674,6 @@ namespace storm {
                     bool observable = this->observables.count(renamingPair->second) > 0;
                     if(observable) {
                         this->observables.erase(renamingPair->second);
-                        std::cout << renamingPair->second << " is observable." << std::endl;
                     }
                     integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1)));
                 }

src/storm/logic/RewardAccumulationEliminationVisitor.cpp

@@ -3,6 +3,7 @@
 
 #include "storm/storage/jani/Model.h"
 #include "storm/storage/jani/traverser/AssignmentsFinder.h"
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 #include "storm/utility/macros.h"
 
 #include "storm/exceptions/UnexpectedException.h"
@@ -126,20 +127,33 @@ namespace storm {
         }
         
         bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const {
-            STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with for unique reward model.");
-            storm::jani::AssignmentsFinder::ResultType assignmentKinds;
-            STORM_LOG_THROW(model.hasGlobalVariable(rewardModelName.get()), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with name " << rewardModelName.get() << ".");
-            storm::jani::Variable const& transientVar = model.getGlobalVariable(rewardModelName.get());
-            if (transientVar.getInitExpression().containsVariables() || !storm::utility::isZero(transientVar.getInitExpression().evaluateAsRational())) {
-                assignmentKinds.hasLocationAssignment = true;
-                assignmentKinds.hasEdgeAssignment = true;
-                assignmentKinds.hasEdgeDestinationAssignment = true;
-            }
-            assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar);
-            if ((assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment) && !accumulation.isStepsSet()) {
+            STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable for unique reward model.");
+            storm::expressions::Expression rewardExpression = model.getRewardModelExpression(rewardModelName.get());
+            bool hasStateRewards = false;
+            bool hasActionOrTransitionRewards = false;
+            auto variablesInRewardExpression = rewardExpression.getVariables();
+            std::map<storm::expressions::Variable, storm::expressions::Expression> initialSubstitution;
+            for (auto const& v : variablesInRewardExpression) {
+                STORM_LOG_ASSERT(model.hasGlobalVariable(v.getName()), "Unable to find global variable " << v.getName() << " occurring in a reward expression.");
+                auto const& janiVar = model.getGlobalVariable(v.getName());
+                if (janiVar.hasInitExpression()) {
+                    initialSubstitution.emplace(v, janiVar.getInitExpression());
+                }
+                auto assignmentKinds = storm::jani::AssignmentsFinder().find(model, v);
+                hasActionOrTransitionRewards = hasActionOrTransitionRewards || assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment;
+                hasStateRewards = hasStateRewards || assignmentKinds.hasLocationAssignment;
+            }
+            rewardExpression = storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution);
+            if (rewardExpression.containsVariables() || !storm::utility::isZero(rewardExpression.evaluateAsRational())) {
+                hasStateRewards = true;
+                hasActionOrTransitionRewards = true;
+            }
+            
+            
+            if (hasActionOrTransitionRewards && !accumulation.isStepsSet()) {
                 return false;
             }
-            if (assignmentKinds.hasLocationAssignment) {
+            if (hasStateRewards) {
                 if (model.isDiscreteTimeModel()) {
                     if (!accumulation.isExitSet()) {
                         return false;

src/storm/storage/jani/Automaton.cpp

@@ -445,7 +445,9 @@ namespace storm {
                 location.substitute(substitution);
             }
 
+            if (hasInitialStatesRestriction()) {
                 this->setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), substitution));
+            }
 
             edges.substitute(substitution);
         }

src/storm/storage/jani/JSONExporter.cpp

@@ -183,7 +183,7 @@ namespace storm {
                 time = time || (!model.isDeterministicModel() && assignmentKinds.hasLocationAssignment);
                 exit = exit || assignmentKinds.hasLocationAssignment;
             }
-            storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution);
+            rewardExpression = storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution);
             if (rewardExpression.containsVariables() || !storm::utility::isZero(rewardExpression.evaluateAsRational())) {
                 steps = true;
                 time = true;
@@ -1118,6 +1118,10 @@ namespace storm {
             
             // Unset model-features that only relate to properties. These are only set if such properties actually exist.
             modelFeatures.remove(storm::jani::ModelFeature::StateExitRewards);
+            if (formulas.empty()) {
+                jsonStruct["properties"] = modernjson::json(modernjson::json::value_t::array);
+                return;
+            }
 
             uint64_t index = 0;
             for(auto const& f : formulas) {

src/storm/storage/jani/Model.cpp

@@ -118,6 +118,10 @@ namespace storm {
             return modelType;
         }
 
+        void Model::setModelType(ModelType const& newModelType) {
+            modelType = newModelType;
+        }
+        
         ModelFeatures const& Model::getModelFeatures() const {
             return modelFeatures;
         }
@@ -634,6 +638,22 @@ namespace storm {
             return constantToIndex.find(name) != constantToIndex.end();
         }
 
+
+        void Model::removeConstant(std::string const& name) {
+            auto pos = constantToIndex.find(name);
+            if (pos != constantToIndex.end()) {
+                uint64_t index = pos->second;
+                constants.erase(constants.begin() + index);
+                constantToIndex.erase(pos);
+                for (auto& entry : constantToIndex) {
+                    if(entry.second > index) {
+                        entry.second--;
+                    }
+                }
+            }
+
+        }
+        
         Constant const& Model::getConstant(std::string const& name) const {
             auto it = constantToIndex.find(name);
             STORM_LOG_THROW(it != constantToIndex.end(), storm::exceptions::WrongFormatException, "Unable to retrieve unknown constant '" << name << "'.");

src/storm/storage/jani/Model.h

@@ -80,6 +80,12 @@ namespace storm {
              */
             ModelType const& getModelType() const;
 
+            /*!
+             * Changes (only) the type declaration of the model. Notice that this operation should be applied with great care, as it may break several algorithms.
+             * The operation is useful to e.g. make a deterministic model into a non-deterministic one.
+             */
+            void setModelType(ModelType const&);
+
             /*!
              * Retrieves the enabled model features
              */
@@ -164,6 +170,11 @@ namespace storm {
              */
             bool hasConstant(std::string const& name) const;
 
+            /*!
+             * Removes (without checks) a constant from the model.
+             */
+            void removeConstant(std::string const& name);
+            
             /*!
              * Retrieves the constants of the model.
              */

src/storm/storage/prism/Program.cpp

@@ -1820,6 +1820,8 @@ namespace storm {
             std::vector<storm::jani::Property> newProperties;
             if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) {
                 newProperties = converter.applyRenaming(properties);
+            } else {
+                newProperties = properties;  // Nothing to be done here. Notice that the copy operation is suboptimal. 
             }
             return std::make_pair(janiModel, newProperties);
         }

src/storm/transformer/SubsystemBuilder.cpp

@@ -65,7 +65,6 @@ namespace storm {
             result.keptActions = storm::storage::BitVector(originalModel.getTransitionMatrix().getRowCount(), false);
             for (auto subsysState : subsystemStates) {
                 result.newToOldStateIndexMapping.push_back(subsysState);
-                bool stateHasOneChoiceLeft = false;
                 for (uint_fast64_t row = subsystemActions.getNextSetIndex(originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]); row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; row = subsystemActions.getNextSetIndex(row+1)) {
                     bool allRowEntriesStayInSubsys = true;
                     for (auto const& entry : originalModel.getTransitionMatrix().getRow(row)) {
@@ -74,10 +73,8 @@ namespace storm {
                             break;
                         }
                     }
-                    stateHasOneChoiceLeft |= allRowEntriesStayInSubsys;
                     result.keptActions.set(row, allRowEntriesStayInSubsys);
                 }
-                 STORM_LOG_THROW(stateHasOneChoiceLeft, storm::exceptions::InvalidArgumentException, "The subsystem would contain a deadlock state.");
             }
             
             // Transform the components of the model

src/storm/utility/graph.cpp

@@ -1555,28 +1555,9 @@ namespace storm {
                 return SymbolicGameProb01Result<Type>(maybePlayer1States, maybePlayer2States, player1StrategyBdd, player2StrategyBdd);
             }
 
-            template <typename T>
-            std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix) {
-                if (matrix.getRowCount() != matrix.getColumnCount()) {
-                    STORM_LOG_ERROR("Provided matrix is required to be square.");
-                    throw storm::exceptions::InvalidArgumentException() << "Provided matrix is required to be square.";
-                }
-                
-                uint_fast64_t numberOfStates = matrix.getRowCount();
-                
-                // Prepare the result. This relies on the matrix being square.
-                std::vector<uint_fast64_t> topologicalSort;
-                topologicalSort.reserve(numberOfStates);
 
-                // Prepare the stacks needed for recursion.
-                std::vector<uint_fast64_t> recursionStack;
-                recursionStack.reserve(matrix.getRowCount());
-                std::vector<typename storm::storage::SparseMatrix<T>::const_iterator> iteratorRecursionStack;
-                iteratorRecursionStack.reserve(numberOfStates);
-                
-                // Perform a depth-first search over the given transitions and record states in the reverse order they were visited.
-                storm::storage::BitVector visitedStates(numberOfStates);
-                for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
+            template<typename T>
+            void topologicalSortHelper(storm::storage::SparseMatrix<T> const& matrix, uint64_t state, std::vector<uint_fast64_t>& topologicalSort, std::vector<uint_fast64_t>& recursionStack, std::vector<typename storm::storage::SparseMatrix<T>::const_iterator>& iteratorRecursionStack, storm::storage::BitVector& visitedStates) {
                 if (!visitedStates.get(state)) {
                     recursionStack.push_back(state);
                     iteratorRecursionStack.push_back(matrix.begin(state));
@@ -1621,6 +1602,34 @@ namespace storm {
                 }
             }
 
+            template <typename T>
+            std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix, std::vector<uint64_t> const& firstStates) {
+                if (matrix.getRowCount() != matrix.getColumnCount()) {
+                    STORM_LOG_ERROR("Provided matrix is required to be square.");
+                    throw storm::exceptions::InvalidArgumentException() << "Provided matrix is required to be square.";
+                }
+                
+                uint_fast64_t numberOfStates = matrix.getRowCount();
+                
+                // Prepare the result. This relies on the matrix being square.
+                std::vector<uint_fast64_t> topologicalSort;
+                topologicalSort.reserve(numberOfStates);
+                
+                // Prepare the stacks needed for recursion.
+                std::vector<uint_fast64_t> recursionStack;
+                recursionStack.reserve(matrix.getRowCount());
+                std::vector<typename storm::storage::SparseMatrix<T>::const_iterator> iteratorRecursionStack;
+                iteratorRecursionStack.reserve(numberOfStates);
+                
+                // Perform a depth-first search over the given transitions and record states in the reverse order they were visited.
+                storm::storage::BitVector visitedStates(numberOfStates);
+                for (auto const state : firstStates ) {
+                    topologicalSortHelper<T>(matrix, state, topologicalSort, recursionStack, iteratorRecursionStack, visitedStates);
+                }
+                for (uint_fast64_t state = 0; state < numberOfStates; ++state) {
+                    topologicalSortHelper<T>(matrix, state, topologicalSort, recursionStack, iteratorRecursionStack, visitedStates);
+                }
+                
                 return topologicalSort;
             }
 
@@ -1696,7 +1705,7 @@ namespace storm {
             
             template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<double> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional<storm::storage::BitVector> const& player1Candidates);
             
-            template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<double> const& matrix) ;
+            template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<double> const& matrix,  std::vector<uint64_t> const& firstStates) ;
             
             // Instantiations for storm::RationalNumber.
 #ifdef STORM_HAVE_CARL
@@ -1752,7 +1761,7 @@ namespace storm {
             
             template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<storm::RationalNumber> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional<storm::storage::BitVector> const& player1Candidates);
             
-            template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
+            template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix,  std::vector<uint64_t> const& firstStates);
             // End of instantiations for storm::RationalNumber.
             
             template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional<storm::storage::BitVector> const& choiceFilter);
@@ -1804,7 +1813,7 @@ namespace storm {
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
             
-            template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<storm::RationalFunction> const& matrix);
+            template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<storm::RationalFunction> const& matrix,  std::vector<uint64_t> const& firstStates);
             
 #endif
             

src/storm/utility/graph.h

@@ -683,7 +683,7 @@ namespace storm {
              * @return A vector of indices that is a topological sort of the states.
              */
             template <typename T>
-            std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix) ;
+            std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix, std::vector<uint64_t> const& firstStates = {}) ;
 
         } // namespace graph
     } // namespace utility

src/storm/utility/shortestPaths.h

@@ -235,7 +235,8 @@ namespace storm {
 
                         // only non-zero entries (i.e. true transitions) are added to the map
                         if (probEntry != 0) {
-                            assert(0 < probEntry <= 1);
+                            assert(0 < probEntry);
+                            assert(probEntry <= 1);
                             stateProbMap.emplace(i, probEntry);
                         }
                     }