started Smtlib Solver interface and some 'prototypy' method to check parameter regions

Former-commit-id: e3cf6528d9

src/adapters/Smt2ExpressionAdapter.h

@@ -0,0 +1,165 @@
+#ifndef STORM_ADAPTERS_SMT2EXPRESSIONADAPTER_H_
+#define STORM_ADAPTERS_SMT2EXPRESSIONADAPTER_H_
+
+#include <unordered_map>
+
+#include "storm-config.h"
+#include "src/adapters/CarlAdapter.h"
+#include "src/storage/expressions/Expressions.h"
+#include "src/storage/expressions/ExpressionManager.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/ExpressionEvaluationException.h"
+#include "src/exceptions/InvalidTypeException.h"
+#include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/NotImplementedException.h"
+
+namespace storm {
+    namespace adapters {
+
+        class Smt2ExpressionAdapter{
+        public:
+            /*!
+             * Creates an expression adapter that can translate expressions to the format of Smt2.
+			 *
+             * @param manager The manager that can be used to build expressions.
+             * @param useReadableVarNames sets whether the expressions should use human readable names for the variables or the internal representation
+             */
+            Smt2ExpressionAdapter(storm::expressions::ExpressionManager& manager, bool useReadableVarNames) : manager(manager), useReadableVarNames(useReadableVarNames) {
+                declaredVariables.emplace_back(std::set<std::string>());
+            }
+            
+            /*!
+             * Translates the given expression to an equivalent expression for Smt2.
+			 *
+             * @param expression The expression to translate.
+             * @return An equivalent expression for Smt2.
+             */
+            std::string translateExpression(storm::expressions::Expression const& expression) {
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+            }
+            
+#ifdef STORM_HAVE_CARL              
+            /*!
+             * Translates the given constraint "leftHandSide relation rightHandSide" to an equivalent expression for Smt2.
+			 
+             * @param leftHandSide
+             * @param relation
+             * @param RightHandSide
+             * @return An equivalent expression for Smt2.
+             */
+            std::string translateExpression(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide) {
+                                
+                return  "(" + carl::toString(relation) +
+                            " (/ " +
+                                leftHandSide.nominator().toString(false, useReadableVarNames) + " " +
+                                leftHandSide.denominator().toString(false, useReadableVarNames) +
+                            ") (/ " +
+                                rightHandSide.nominator().toString(false, useReadableVarNames) + " " +
+                                rightHandSide.denominator().toString(false, useReadableVarNames) +
+                            ") " +
+                        ")";
+            }
+            
+            /*!
+             * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2.
+			 
+             * @param constraint
+             * @return An equivalent expression for Smt2.
+             */
+            std::string translateExpression(carl::Constraint<storm::RawPolynomial> const& constraint) {
+                                
+                return  "(" + carl::toString(constraint.rel()) + " " +
+                            constraint.lhs().toString(false, useReadableVarNames) + " " +
+                            "0 " +
+                        ")";
+            }
+#endif
+            /*!
+             * Translates the given variable to an equivalent expression for Smt2.
+             *
+             * @param variable The variable to translate.
+             * @return An equivalent expression for smt2.
+             */
+            std::string translateExpression(storm::expressions::Variable const& variable) {
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+            }
+            
+            /*!
+             * Finds the counterpart to the given smt2 variable declaration.
+             *
+             * @param smt2Declaration The declaration for which to find the equivalent.
+             * @return The equivalent counterpart.
+             */
+            storm::expressions::Variable const& getVariable(std::string smt2Declaration) {
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+            }
+            
+            void increaseScope(uint_fast64_t n=1){
+                for(uint_fast64_t i=0; i<n; ++i){
+                    declaredVariables.emplace_back(std::set<std::string>());
+                }
+            }
+            
+            void decreaseScope(uint_fast64_t n=1){
+                STORM_LOG_THROW(declaredVariables.size()>=n, storm::exceptions::InvalidArgumentException, "Scope increased too much. Too many calls of pop()?");
+                for(uint_fast64_t i=0; i<n; ++i){
+                    declaredVariables.pop_back();
+                }
+            }
+            
+            
+#ifdef STORM_HAVE_CARL
+            /*! Checks whether the variables in the given set are already declared and creates them if necessary
+             *  @param variables the set of variables to check
+             */
+            std::vector<std::string> const checkForUndeclaredVariables(std::set<storm::Variable> const& variables){
+                std::vector<std::string> result;
+                carl::VariablePool& vPool = carl::VariablePool::getInstance();
+                for (storm::Variable const& variableToCheck : variables){
+                    std::string const& variableString = vPool.getName(variableToCheck, useReadableVarNames);
+                    // first check if this variable is already declared
+                    bool alreadyDeclared=false;
+                    for(std::set<std::string> const& variables : declaredVariables){
+                        if(variables.find(variableString)!=variables.end()){
+                            alreadyDeclared=true;
+                            break;
+                        } 
+                    }
+                    // secondly, declare the variable if necessary
+                    if(!alreadyDeclared){
+                        STORM_LOG_DEBUG("Declaring the variable " + variableString);
+                        declaredVariables.back().insert(variableString);
+                        std::string varDeclaration = "( declare-fun " + variableString + " () ";
+                        switch (variableToCheck.getType()){
+                            case carl::VariableType::VT_BOOL:
+                                varDeclaration += "Bool";
+                                break;
+                            case carl::VariableType::VT_REAL:
+                                varDeclaration += "Real";
+                                break;
+                            case carl::VariableType::VT_INT:
+                                varDeclaration += "Int";
+                                break;
+                            default:
+                                STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "The type of the variable is not supported");
+                        }
+                        varDeclaration += " )";
+                        result.push_back(varDeclaration);
+                    }
+                }
+                return result;
+            }
+#endif
+            
+        private:
+            // The manager that can be used to build expressions.
+            storm::expressions::ExpressionManager& manager;
+            // A flag to decide whether readable var names should be used instead of intern representation
+            bool useReadableVarNames;
+            // the declared variables for the different scopes
+            std::vector<std::set<std::string>> declaredVariables;
+        };
+    } // namespace adapters
+} // namespace storm
+
+#endif /* STORM_ADAPTERS_SMT2EXPRESSIONADAPTER_H_ */

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -10,6 +10,8 @@
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
+#include "src/solver/Smt2SmtSolver.h"
+
 #include "src/utility/graph.h"
 #include "src/utility/vector.h"
 #include "src/utility/macros.h"
@@ -986,6 +988,36 @@ namespace storm {
             }
         }
         
+        template<>
+        storm::storage::SparseMatrix<double> SparseDtmcEliminationModelChecker<storm::RationalFunction>::FlexibleSparseMatrix::instantiateAsDouble(std::map<storm::Variable, storm::RationalFunction::CoeffType> substitutions){
+            
+            //Check if the CoeffType is as expected
+            STORM_LOG_THROW((std::is_same<storm::RationalFunction::CoeffType, cln::cl_RA>::value), storm::exceptions::IllegalArgumentException, "Unexpected Type of Coefficients");
+            
+            //get a Matrix builder
+            index_type numElements=0;
+            for(row_type const& row : this->data){
+                numElements += row.size();
+            }
+            storm::storage::SparseMatrixBuilder<double> matrixBuilder(this->getNumberOfRows(), this->getNumberOfRows(), numElements);
+            
+            //fill in the data...
+            for(index_type rowIndex=0; rowIndex < this->getNumberOfRows(); ++rowIndex){
+                for(auto const& entry : this->getRow(rowIndex)){
+                    double value = cln::double_approx(entry.getValue().evaluate(substitutions));
+                    matrixBuilder.addNextValue(rowIndex, entry.getColumn(), value);
+                }
+            }
+       
+            return matrixBuilder.build();
+        }
+        
+         template<typename ValueType>
+        storm::storage::SparseMatrix<double> SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::instantiateAsDouble(std::map<storm::Variable, storm::RationalFunction::CoeffType> substitutions){
+            STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Instantiation of flexible matrix is not supported for this type");
+        }
+        
+        
         template<typename ValueType>
         typename SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix SparseDtmcEliminationModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne) {
             FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount());
@@ -1014,6 +1046,285 @@ namespace storm {
             return flexibleMatrix;
         }
         
+        template<>
+        bool SparseDtmcEliminationModelChecker<storm::RationalFunction>::checkRegion(storm::logic::Formula const& formula, std::vector<SparseDtmcEliminationModelChecker<storm::RationalFunction>::ParameterRegion> parameterRegions){
+            //Note: this is an 'experimental' implementation
+            //Start with some preprocessing (inspired by computeUntilProbabilities...)
+            
+            //for simplicity we only support state formulas with eventually (e.g. P<0.5 [ F "target" ])
+            //get the (sub)formulae and the vector of target states
+            STORM_LOG_THROW(formula.isStateFormula(), storm::exceptions::IllegalArgumentException, "expected a stateFormula");
+            STORM_LOG_THROW(formula.asStateFormula().isProbabilityOperatorFormula(), storm::exceptions::IllegalArgumentException, "expected a probabilityOperatorFormula");
+            storm::logic::ProbabilityOperatorFormula const& probOpForm=formula.asStateFormula().asProbabilityOperatorFormula();
+            STORM_LOG_THROW(probOpForm.hasBound(), storm::exceptions::IllegalArgumentException, "The formula has no bound");
+            STORM_LOG_THROW(probOpForm.getSubformula().asPathFormula().isEventuallyFormula(), storm::exceptions::IllegalArgumentException, "expected an eventually subformula");
+            storm::logic::EventuallyFormula const& eventFormula = probOpForm.getSubformula().asPathFormula().asEventuallyFormula();
+            
+            std::unique_ptr<CheckResult> targetStatesResultPtr = this->check(eventFormula.getSubformula());
+            storm::storage::BitVector const& targetStates = targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector();
+            
+            // Do some sanity checks to establish some required properties.
+            STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
+            storm::storage::sparse::state_type initialState = *model.getInitialStates().begin();
+            
+            // Then, compute the subset of states that has a probability of 0 or 1, respectively.
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(model, storm::storage::BitVector(model.getNumberOfStates(),true), targetStates);
+            storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first;
+            std::cout << "states with prob 0" << statesWithProbability0 << std::endl;
+            storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second;
+            storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
+            
+            // If the initial state is known to have either probability 0 or 1, we can directly return the result.
+            if (model.getInitialStates().isDisjointFrom(maybeStates)) {
+                STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step.");
+                double res= statesWithProbability0.get(*model.getInitialStates().begin()) ? 0.0 : 1.0;
+                switch (probOpForm.getComparisonType()){
+                    case storm::logic::ComparisonType::Greater:
+                        return (res > probOpForm.getBound());
+                    case storm::logic::ComparisonType::GreaterEqual:
+                        return (res >= probOpForm.getBound());
+                    case storm::logic::ComparisonType::Less:
+                        return (res < probOpForm.getBound());
+                    case storm::logic::ComparisonType::LessEqual:
+                        return (res <= probOpForm.getBound());
+                    default:
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
+                }
+            }
+            
+            // Determine the set of states that is reachable from the initial state without jumping over a target state.
+            storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(model.getTransitionMatrix(), model.getInitialStates(), maybeStates, statesWithProbability1);
+            
+            // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
+            maybeStates &= reachableStates;
+            
+            // Create a vector for the probabilities to go to a state with probability 1 in one step.
+            std::vector<storm::RationalFunction> oneStepProbabilities = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
+            
+            // Determine the set of initial states of the sub-model.
+            storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates;
+            
+            // We then build the submatrix that only has the transitions of the maybe states.
+            storm::storage::SparseMatrix<storm::RationalFunction> submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
+            storm::storage::SparseMatrix<storm::RationalFunction> submatrixTransposed = submatrix.transpose();
+            
+            // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
+            FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix);
+            FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrixTransposed, true);
+            
+            
+            //TODO...
+            // eliminate some states.. update the one step probabilities!
+
+            // SMT formulation of resulting pdtmc
+            storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions
+            carl::VariablePool& varPool = carl::VariablePool::getInstance();
+            storm::solver::Smt2SmtSolver solver(manager, true);
+
+            // todo maybe introduce the parameters already at this point?
+            
+            // we will introduce a variable for every state which encodes the probability to reach a target state from this state.
+            // we will store them as polynomials to easily use operations with rational functions
+            std::vector<storm::RationalFunction::PolyType> stateProbVars;
+            for (storm::storage::sparse::state_type state = 0; state < flexibleMatrix.getNumberOfRows(); ++state){
+                storm::Variable stateVar = varPool.getFreshVariable("p_" + std::to_string(state));
+                std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>> cache(new carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>());
+                storm::RationalFunction::PolyType stateVarAsPoly(storm::RationalFunction::PolyType::PolyType(stateVar), cache);
+                
+                //each variable is in the interval [0,1]
+                solver.add(storm::RationalFunction(stateVarAsPoly), storm::CompareRelation::GEQ, storm::RationalFunction(0));
+                solver.add(storm::RationalFunction(stateVarAsPoly), storm::CompareRelation::LEQ, storm::RationalFunction(1));
+                stateProbVars.push_back(stateVarAsPoly);
+            }
+            
+            //now lets add the actual transitions
+            for (storm::storage::sparse::state_type state = 0; state < flexibleMatrix.getNumberOfRows(); ++state){
+                storm::RationalFunction reachProbability(oneStepProbabilities[state]);
+                if(!reachProbability.isZero()){
+                    std::cout << "non zero " << state << ":  " << reachProbability << std::endl;
+                }
+                for(auto const& transition : flexibleMatrix.getRow(state)){
+                    reachProbability += transition.getValue() * stateProbVars[transition.getColumn()];
+                }
+                //Todo: depending on the objective (i.e. the formlua) it suffices to use LEQ or GEQ here... maybe this is faster?
+                solver.add(storm::RationalFunction(stateProbVars[state]), storm::CompareRelation::EQ, reachProbability);
+            }
+            
+            //the property should be satisfied in the initial state
+            storm::CompareRelation propertyCompRel;
+            switch (probOpForm.getComparisonType()){
+                case storm::logic::ComparisonType::Greater:
+                    propertyCompRel=storm::CompareRelation::GT;
+                    break;
+                case storm::logic::ComparisonType::GreaterEqual:
+                    propertyCompRel=storm::CompareRelation::GEQ;
+                    break;
+                case storm::logic::ComparisonType::Less:
+                    propertyCompRel=storm::CompareRelation::LT;
+                    break;
+                case storm::logic::ComparisonType::LessEqual:
+                    propertyCompRel=storm::CompareRelation::LEQ;
+                    break;
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
+            }
+            uint_fast64_t thresholdDenominator = 1.0/storm::settings::generalSettings().getPrecision();
+            uint_fast64_t thresholdNumerator = probOpForm.getBound()*thresholdDenominator;
+            storm::RationalFunction threshold(thresholdNumerator);
+            threshold = threshold / thresholdDenominator;
+            solver.add(storm::RationalFunction(stateProbVars[*newInitialStates.begin()]), propertyCompRel, threshold);
+            
+            //the bounds for the parameters
+            solver.push();
+            for(auto param : parameterRegions){
+                storm::RawPolynomial lB(param.variable);
+                lB -= param.lowerBound;
+                solver.add(carl::Constraint<storm::RawPolynomial>(lB,storm::CompareRelation::GEQ));
+                storm::RawPolynomial uB(param.variable);
+                uB -= param.upperBound;
+                solver.add(carl::Constraint<storm::RawPolynomial>(uB,storm::CompareRelation::LEQ));
+            }
+            
+            flexibleMatrix.print();
+                
+            
+            /*
+            //testing stuff...
+            auto varx=varPool.getFreshVariable("x");
+            storm::RawPolynomial px(varx);
+            carl::Constraint<storm::RawPolynomial> cx(px,storm::CompareRelation::GEQ);
+            carl::Constraint<storm::RawPolynomial> cx1(px-storm::RawPolynomial(1),storm::CompareRelation::LEQ);
+            storm::RationalFunction zero(0);
+            storm::RationalFunction one(1);
+            storm::RationalFunction two(2);
+            storm::RationalFunction funcWithpK = flexibleMatrix.getRow(1).begin()->getValue();
+            storm::RationalFunction funcWithpL = flexibleMatrix.getRow(11).begin()->getValue();
+            carl::Constraint<storm::RationalFunction> cpLzero(funcWithpL,storm::CompareRelation::GEQ);
+            
+            solver.add(one,storm::CompareRelation::LEQ, two);
+            solver.add(funcWithpL,storm::CompareRelation::LEQ, one);
+            solver.push();
+            solver.add(funcWithpL,storm::CompareRelation::GEQ, zero);
+            solver.add(funcWithpK,storm::CompareRelation::GEQ, zero);
+            solver.pop();
+            solver.add(funcWithpK,storm::CompareRelation::GEQ, zero);
+            solver.add(cpLzero);
+            solver.add(cx);
+            solver.add(cx1);
+            
+            */
+            /*
+            solver.add(p,storm::CompareRelation::LEQ, two);
+            solver.add(q,storm::CompareRelation::LT, p);
+            solver.add(q-p,storm::CompareRelation::LT);
+            
+            */
+            
+            // find further restriction on probabilities
+            //start solving ...
+            
+            /* maybe useful stuff...
+            // Create a bit vector that represents the subsystem of states we still have to eliminate.
+            storm::storage::BitVector subsystem = storm::storage::BitVector(submatrix.getRowCount(), true);
+            
+            std::vector<std::size_t> statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities);
+            
+
+       //from compute reachability 
+            uint_fast64_t maximalDepth = 0;
+            if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) {
+                // If we are required to do pure state elimination, we simply create a vector of all states to
+                // eliminate and sort it according to the given priorities.
+                
+                // Remove the initial state from the states which we need to eliminate.
+                subsystem &= ~initialStates;
+                std::vector<storm::storage::sparse::state_type> states(subsystem.begin(), subsystem.end());
+                
+                if (statePriorities) {
+                    std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; });
+                }
+                
+                STORM_LOG_DEBUG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl);
+                for (auto const& state : states) {
+                    eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards);
+                }
+                STORM_LOG_DEBUG("Eliminated " << states.size() << " states." << std::endl);
+            } else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) {
+                // When using the hybrid technique, we recursively treat the SCCs up to some size.
+                std::vector<storm::storage::sparse::state_type> entryStateQueue;
+                STORM_LOG_DEBUG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl);
+                maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::sparseDtmcEliminationModelCheckerSettings().getMaximalSccSize(), entryStateQueue, stateRewards, statePriorities);
+                
+                // If the entry states were to be eliminated last, we need to do so now.
+                STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step.");
+                if (storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet()) {
+                    for (auto const& state : entryStateQueue) {
+                        eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards);
+                    }
+                }
+                STORM_LOG_DEBUG("Eliminated " << subsystem.size() << " states." << std::endl);
+            }
+            
+            // Finally eliminate initial state.
+            if (!stateRewards) {
+                // If we are computing probabilities, then we can simply call the state elimination procedure. It
+                // will scale the transition row of the initial state with 1/(1-loopProbability).
+                STORM_LOG_INFO("Eliminating initial state " << *initialStates.begin() << "." << std::endl);
+                eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions, stateRewards);
+            } else {
+                // If we are computing rewards, we cannot call the state elimination procedure for technical reasons.
+                // Instead, we need to get rid of a potential loop in this state explicitly.
+                
+                // Start by finding the self-loop element. Since it can only be the only remaining outgoing transition
+                // of the initial state, this amounts to checking whether the outgoing transitions of the initial
+                // state are non-empty.
+                if (!flexibleMatrix.getRow(*initialStates.begin()).empty()) {
+                    STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).size() == 1, "At most one outgoing transition expected at this point, but found more.");
+                    STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).front().getColumn() == *initialStates.begin(), "Remaining entry should be a self-loop, but it is not.");
+                    ValueType loopProbability = flexibleMatrix.getRow(*initialStates.begin()).front().getValue();
+                    loopProbability = storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - loopProbability);
+                    STORM_LOG_DEBUG("Scaling the reward of the initial state " << stateRewards.get()[(*initialStates.begin())] << " with " << loopProbability);
+                    stateRewards.get()[(*initialStates.begin())] *= loopProbability;
+                    flexibleMatrix.getRow(*initialStates.begin()).clear();
+                }
+            }
+            */
+                        std::cout << std::endl << "-----------------------" << std::endl << "testing stuff..." << std::endl;
+            std::map<storm::Variable, storm::RationalFunction::CoeffType> testmap;
+            
+            storm::Variable pK = varPool.findVariableWithName("pK");
+            storm::Variable pL = varPool.findVariableWithName("pL");
+            storm::Variable bs = varPool.findVariableWithName("bs");
+            std::cout << "pk id is " << pK.getId() << std::endl;
+            std::cout << "pL id is " << pL.getId() << std::endl;
+            std::cout << "bs id is " << bs.getId() << std::endl;
+            if(bs == storm::Variable::NO_VARIABLE){
+                std::cout << "bs is not a variable" << std::endl;
+            }
+            storm::RationalFunction::CoeffType pKSub=4;
+            pKSub= pKSub/10;
+            storm::RationalFunction::CoeffType pLSub=8;
+            pLSub= pLSub/10;
+            testmap[pK]=pKSub;
+            testmap[pL]=pLSub;
+            storm::storage::SparseMatrix<double> resultingMatr = flexibleMatrix.instantiateAsDouble(testmap);
+            std::cout << "Old matrix: column: " << flexibleMatrix.getRow(1).begin()->getColumn() << " value:" << flexibleMatrix.getRow(1).begin()->getValue() << std::endl;
+            std::cout << "New matrix: column: " << resultingMatr.getRow(1).begin()->getColumn() << " value:" << resultingMatr.getRow(1).begin()->getValue() << std::endl;
+            //END OF TESTING STUFF 
+            //*/
+            //from until method
+            //boost::optional<std::vector<ValueType>> missingStateRewards;
+            //return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initialState, computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards, statePriorities)));
+            
+            return false;
+        }
+        
+        template<typename ValueType>
+        bool SparseDtmcEliminationModelChecker<ValueType>::checkRegion(storm::logic::Formula const& formula, std::vector<SparseDtmcEliminationModelChecker<ValueType>::ParameterRegion> parameterRegions){
+            
+            STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Region check is not supported for this type");
+        }
+        
         template class SparseDtmcEliminationModelChecker<double>;
         
 #ifdef STORM_HAVE_CARL

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h

@@ -22,6 +22,20 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
             virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
             
+            struct ParameterRegion{
+                storm::Variable variable;
+                storm::RationalFunction::CoeffType lowerBound;
+                storm::RationalFunction::CoeffType upperBound;
+            };
+            
+            /*!
+             * Checks whether the given formula holds for all possible parameters that satisfy the given parameter regions
+             * ParameterRegions should contain all parameters (not mentioned parameters are assumed to be arbitrary reals)
+             */
+            bool checkRegion(storm::logic::Formula const& formula, std::vector<ParameterRegion> parameterRegions);
+            
+            
+            
         private:
             class FlexibleSparseMatrix {
             public:
@@ -52,6 +66,16 @@ namespace storm {
                  */
                 bool hasSelfLoop(storm::storage::sparse::state_type state);
                 
+                /*!
+                 * Instantiates the matrix, i.e., evaluate the occurring functions according to the given substitution of the variables
+                 * 
+                 * @param substitutions A mapping that assigns a constant value to every variable
+                 * 
+                 * @return A matrix with constant (double) entries
+                 */
+                storm::storage::SparseMatrix<double> instantiateAsDouble(std::map<storm::Variable, storm::RationalFunction::CoeffType> substitutions);
+                
+                
             private:
                 std::vector<row_type> data;
             };

src/settings/modules/GeneralSettings.cpp

@@ -45,6 +45,7 @@ namespace storm {
             
 #ifdef STORM_HAVE_CARL
             const std::string GeneralSettings::parametricOptionName = "parametric";
+            const std::string GeneralSettings::parametricRegionOptionName = "parametricRegion";
 #endif
 
             GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
@@ -93,6 +94,7 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
                 this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to use the parametric engine.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, parametricRegionOptionName, false, "Sets whether to use the parametric Region engine.").build());
 #endif
             }
             
@@ -257,6 +259,9 @@ namespace storm {
             bool GeneralSettings::isParametricSet() const {
                 return this->getOption(parametricOptionName).getHasOptionBeenSet();
             }
+            bool GeneralSettings::isParametricRegionSet() const {
+                return this->getOption(parametricRegionOptionName).getHasOptionBeenSet();
+            }
 #endif
             
             bool GeneralSettings::check() const {

src/settings/modules/GeneralSettings.h

@@ -301,6 +301,13 @@ namespace storm {
                  * @return True iff the option was set.
                  */
                 bool isParametricSet() const;
+                
+                /*!
+                 * Retrieves whether the option enabling parametric region model checking is set.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool isParametricRegionSet() const;
 #endif
                 
                 bool check() const override;
@@ -346,6 +353,7 @@ namespace storm {
                 
 #ifdef STORM_HAVE_CARL
                 static const std::string parametricOptionName;
+                static const std::string parametricRegionOptionName;
 #endif
             };
             

src/solver/Smt2SmtSolver.cpp

@@ -0,0 +1,136 @@
+#include "src/solver/Smt2SmtSolver.h"
+
+#include "src/exceptions/NotSupportedException.h"
+#include "src/exceptions/InvalidStateException.h"
+#include "src/exceptions/NotImplementedException.h"
+#include "utility/macros.h"
+#include "adapters/CarlAdapter.h"
+#include "exceptions/IllegalArgumentException.h"
+#include "exceptions/IllegalFunctionCallException.h"
+
+namespace storm {
+    namespace solver {
+
+        Smt2SmtSolver::Smt2ModelReference::Smt2ModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter) : ModelReference(manager), expressionAdapter(expressionAdapter){
+            // Intentionally left empty.
+        }
+
+        bool Smt2SmtSolver::Smt2ModelReference::getBooleanValue(storm::expressions::Variable const& variable) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+        }
+
+        int_fast64_t Smt2SmtSolver::Smt2ModelReference::getIntegerValue(storm::expressions::Variable const& variable) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+        }
+
+        double Smt2SmtSolver::Smt2ModelReference::getRationalValue(storm::expressions::Variable const& variable) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+        }
+
+        Smt2SmtSolver::Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions) : SmtSolver(manager), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown), useCarlExpressions(useCarlExpressions) {
+#ifndef STORM_HAVE_CARL
+            STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalArgumentException, "Tried to use carl expressions but storm is not linked with CARL");
+#endif
+            expressionAdapter = std::unique_ptr<storm::adapters::Smt2ExpressionAdapter>(new storm::adapters::Smt2ExpressionAdapter(this->getManager(), true));
+            init();
+        }
+
+        Smt2SmtSolver::~Smt2SmtSolver() {
+            writeCommand("( exit )");
+            //todo make sure that the process exits
+        }
+
+        void Smt2SmtSolver::push() {
+            expressionAdapter->increaseScope();
+            writeCommand("( push 1 ) ");
+        }
+
+        void Smt2SmtSolver::pop() {
+            expressionAdapter->decreaseScope();
+            writeCommand("( pop 1 ) ");
+        }
+
+        void Smt2SmtSolver::pop(uint_fast64_t n) {
+            expressionAdapter->decreaseScope(n);
+            writeCommand("( pop " + std::to_string(n) + " ) ");
+        }
+
+        void Smt2SmtSolver::reset() {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+        }
+
+        void Smt2SmtSolver::add(storm::expressions::Expression const& assertion) {
+            STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions");
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+        }
+
+#ifdef STORM_HAVE_CARL        
+        void Smt2SmtSolver::add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide) {
+            STORM_LOG_THROW(useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions");
+            //if some of the occurring variables are not declared yet, we will have to.
+            std::set<storm::Variable> variables;
+            leftHandSide.gatherVariables(variables);
+            rightHandSide.gatherVariables(variables);
+            std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
+            for (auto declaration : varDeclarations){
+                writeCommand(declaration);
+            }
+            writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )");
+        }
+        
+        template<>
+        void Smt2SmtSolver::add(carl::Constraint<storm::RationalFunction> const& constraint) {
+            add(constraint.lhs(), constraint.rel());
+        }
+        
+        template<>
+        void Smt2SmtSolver::add(carl::Constraint<storm::RawPolynomial> const& constraint) {
+            //if some of the occurring variables are not declared yet, we will have to.
+            std::set<storm::Variable> variables = constraint.lhs().gatherVariables();
+            std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
+            for (auto declaration : varDeclarations){
+                writeCommand(declaration);
+            }
+            writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )");
+        }
+        
+        
+#endif
+
+        SmtSolver::CheckResult Smt2SmtSolver::check() {
+            writeCommand("( check-sat )");
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+        }
+
+        SmtSolver::CheckResult Smt2SmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+        }
+
+#ifndef WINDOWS
+
+        SmtSolver::CheckResult Smt2SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+        }
+#endif
+
+        void Smt2SmtSolver::init() {
+            //hard coded output file.. for now
+            commandFile.open("/home/tim/Desktop/smtlibcommand.txt", std::ios::trunc);
+            STORM_LOG_THROW(commandFile.is_open(), storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened");
+
+            //some initial commands
+            writeCommand("( set-logic QF_NRA )");
+
+        }
+
+        void Smt2SmtSolver::writeCommand(std::string smt2Command) {
+            if (commandFile.is_open()) {
+                commandFile << smt2Command << std::endl;
+            } else{
+                std::cout << "COMMAND FILE IS CLOSED" <<std::endl;
+            }
+            
+            //todo actually write to the solver
+        }
+    }
+}

src/solver/Smt2SmtSolver.h

@@ -0,0 +1,112 @@
+#ifndef STORM_SOLVER_SMT2SMTSOLVER
+#define STORM_SOLVER_SMT2SMTSOLVER
+
+#include <iostream>
+#include <fstream>
+
+#include "storm-config.h"
+#include "src/solver/SmtSolver.h"
+#include "src/adapters/Smt2ExpressionAdapter.h"
+#include "src/adapters/CarlAdapter.h"
+
+namespace storm {
+    namespace solver {
+
+        class Smt2SmtSolver : public SmtSolver {
+        public:
+
+            class Smt2ModelReference : public SmtSolver::ModelReference {
+            public:
+                Smt2ModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter);
+                virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
+                virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
+                virtual double getRationalValue(storm::expressions::Variable const& variable) const override;
+
+            private:
+
+                // The expression adapter that is used to translate the variable names.
+                storm::adapters::Smt2ExpressionAdapter& expressionAdapter;
+            };
+
+        public:
+            /*!
+             * Creates a new solver with the given manager.
+             * In addition to storm expressions, this solver also allows carl expressions (but not both).
+             * Hence, there is a flag to chose between the two
+             */
+            Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions = false);
+            virtual ~Smt2SmtSolver();
+
+            virtual void push() override;
+
+            virtual void pop() override;
+
+            virtual void pop(uint_fast64_t n) override;
+
+            virtual void reset() override;
+
+            virtual void add(storm::expressions::Expression const& assertion) override;
+#ifdef STORM_HAVE_CARL         
+            //adds the constraint "leftHandSide relation rightHandSide"
+            virtual void add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide=storm::RationalFunction(0));
+            
+            //adds the given carl constraint
+            template<typename FunctionType>
+            void add(typename carl::Constraint<FunctionType> const& constraint);
+#endif
+
+            virtual CheckResult check() override;
+
+            virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
+
+#ifndef WINDOWS
+            virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
+#endif
+            //Todo: some of these might be added in the future
+            //virtual storm::expressions::SimpleValuation getModelAsValuation() override;
+
+            //virtual std::shared_ptr<SmtSolver::ModelReference> getModel() override;
+
+            //	virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Variable> const& important) override;
+
+            //	virtual uint_fast64_t allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback) override;
+
+            //	virtual uint_fast64_t allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(ModelReference&)> const& callback) override;
+
+            //	virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override;
+
+        private:
+
+
+            /*!
+             * Initializes the solver
+             */
+            void init();
+
+
+            /*! Writes the given command to the solver
+             * @param smt2Command the command that the solver will receive
+             */
+            void writeCommand(std::string smt2Command);
+
+
+
+            // a filestream where the commands that we send to the solver will be stored (can be used for debugging purposes)
+            std::ofstream commandFile;
+
+            // An expression adapter that is used for translating the expression into Smt2's format.
+            std::unique_ptr<storm::adapters::Smt2ExpressionAdapter> expressionAdapter;
+
+            // A flag storing whether the last call to a check method provided aussumptions.
+            bool lastCheckAssumptions;
+
+            // The last result that was returned by any of the check methods.
+            CheckResult lastResult;
+            
+            // A flag that states whether we want to use carl expressions.
+            bool useCarlExpressions;
+
+        };
+    }
+}
+#endif // STORM_SOLVER_SMT2SMTSOLVER

src/utility/cli.h

@@ -445,6 +445,36 @@ namespace storm {
                 std::shared_ptr<storm::models::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::Dtmc<storm::RationalFunction>>();
 
                 std::cout << std::endl << "Model checking property: " << *formula << " ...";
+                //do we want to check for a parameter region?
+                if(settings.isParametricRegionSet()){
+                    std::cout << std::endl;
+                    //experimental implementation! check some hardcoded region
+                    std::vector<storm::modelchecker::SparseDtmcEliminationModelChecker<storm::RationalFunction>::ParameterRegion> regions;
+                    storm::RationalFunction::CoeffType zeroPointOne(1);
+                    zeroPointOne = zeroPointOne/10;
+                    storm::modelchecker::SparseDtmcEliminationModelChecker<storm::RationalFunction>::ParameterRegion param1;
+                    param1.lowerBound= zeroPointOne*2;
+                    param1.upperBound= zeroPointOne*4;
+                    param1.variable=carl::VariablePool::getInstance().findVariableWithName("pL");
+                    regions.push_back(param1);
+                    storm::modelchecker::SparseDtmcEliminationModelChecker<storm::RationalFunction>::ParameterRegion param2;
+                    param2.lowerBound= zeroPointOne*3;
+                    param2.upperBound= zeroPointOne*5;
+                    param2.variable=carl::VariablePool::getInstance().findVariableWithName("pK");
+                    regions.push_back(param2);
+                            
+                    storm::modelchecker::SparseDtmcEliminationModelChecker<storm::RationalFunction> modelchecker(*dtmc);
+                    bool result = modelchecker.checkRegion(*formula.get(), regions);
+                    std::cout << "... done." << std::endl;
+                    if (result){
+                    std::cout << "the property holds for all parameters in the given region" << std::endl;
+                    }else{
+                    std::cout << "the property does NOT hold for all parameters in the given region" << std::endl;
+                    }
+                    
+                    
+                }else{
+                    //just obtain the resulting rational function
                     std::unique_ptr<storm::modelchecker::CheckResult> result;
 
                     storm::modelchecker::SparseDtmcEliminationModelChecker<storm::RationalFunction> modelchecker(*dtmc);
@@ -463,6 +493,7 @@ namespace storm {
                         std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
                     }
                 }
+            }
 #endif
             
             template<typename ValueType>