Merge branch 'master' into parametricSystems

Former-commit-id: 5763f8b9df

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -1693,7 +1693,7 @@ namespace storm {
                     storm::models::Mdp<T> subMdp = labeledMdp.restrictChoiceLabels(commandSet);
                     storm::modelchecker::SparseMdpPrctlModelChecker<T> modelchecker(subMdp);
                     LOG4CPLUS_DEBUG(logger, "Invoking model checker.");
-                    std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
+                    std::vector<T> result = modelchecker.computeUntilProbabilitiesHelper(false, phiStates, psiStates, false)
                     LOG4CPLUS_DEBUG(logger, "Computed model checking results.");
                     totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock;
 

src/logic/BinaryPathFormula.cpp

@@ -44,10 +44,12 @@ namespace storm {
         
         void BinaryPathFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
             this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+            this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
         }
         
         void BinaryPathFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
             this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+            this->getRightSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
         }
     }
 }

src/logic/BinaryStateFormula.cpp

@@ -44,10 +44,12 @@ namespace storm {
         
         void BinaryStateFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
             this->getLeftSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+            this->getRightSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
         }
         
         void BinaryStateFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
             this->getLeftSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
+            this->getRightSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
         }
     }
 }

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -7,6 +7,11 @@
 #include "src/solver/NondeterministicLinearEquationSolver.h"
 
 namespace storm {
+    namespace counterexamples {
+        template<typename ValueType>
+        class SMTMinimalCommandSetGenerator;
+    }
+    
     namespace modelchecker {
         
         // Forward-declare other model checkers to make them friend classes.
@@ -17,6 +22,7 @@ namespace storm {
         class SparseMdpPrctlModelChecker : public AbstractModelChecker {
         public:
             friend class SparseMarkovAutomatonCslModelChecker<ValueType>;
+            friend class counterexamples::SMTMinimalCommandSetGenerator<ValueType>;
             
             explicit SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model);
             explicit SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver);

src/utility/cli.h

@@ -278,9 +278,8 @@ namespace storm {
                 typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
                 if (formula) {
                     options = storm::builder::ExplicitPrismModelBuilder<double>::Options(*formula.get());
-                } else {
-                    options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
                 }
+                options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
                 
                 // Then, build the model from the symbolic description.
                 result = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);