Parsing parameteric dtmcs and exporting them to smt2

Former-commit-id: c791625d40

src/adapters/ExplicitModelAdapter.h

@@ -158,18 +158,18 @@ namespace storm {
              * @return The explicit model that was given by the probabilistic program.
              */
             static std::unique_ptr<storm::models::AbstractModel<ValueType>> translateProgram(storm::prism::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") {
-                // Start by defining the undefined constants in the model.
+				// Start by defining the undefined constants in the model.
                 // First, we need to parse the constant definition string.
                 std::map<std::string, storm::expressions::Expression> constantDefinitions = parseConstantDefinitionString(program, constantDefinitionString);
                 
                 storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions);
-                LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants.");
+                LOG_THROW((std::is_same<ValueType, RationalFunction>::value || !preparedProgram.hasUndefinedConstants()), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants.");
                 
                 // Now that we have defined all the constants in the program, we need to substitute their appearances in
                 // all expressions in the program so we can then evaluate them without having to store the values of the
                 // constants in the state (i.e., valuation).
                 preparedProgram = preparedProgram.substituteConstants();
-                
+                std::cout << preparedProgram << std::endl;
                 ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModelName);
                 
                 std::unique_ptr<storm::models::AbstractModel<ValueType>> result;
@@ -534,12 +534,15 @@ namespace storm {
                 }
                 for (auto const& module : program.getModules()) {
                     for (auto const& booleanVariable : module.getBooleanVariables()) {
+						std::cout << booleanVariable.getName() << " <-- " << booleanVariable.getInitialValueExpression() << "(= " << booleanVariable.getInitialValueExpression().evaluateAsBool() << " )" << std::endl;
                         initialState->addBooleanIdentifier(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool());
                     }
                     for (auto const& integerVariable : module.getIntegerVariables()) {
                         initialState->addIntegerIdentifier(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt());
                     }
                 }
+				std::cout << "INITIAL STATE:" << std::endl;
+				std::cout << *initialState << std::endl;
         
                 std::pair<bool, uint_fast64_t> addIndexPair = getOrAddStateIndex(initialState, stateInformation);
                 stateInformation.initialStateIndices.push_back(addIndexPair.second);
@@ -696,6 +699,7 @@ namespace storm {
             static ModelComponents buildModelComponents(storm::prism::Program const& program, std::string const& rewardModelName) {
                 ModelComponents modelComponents;
 				expressions::ExpressionEvaluation<ValueType> eval;
+				
                 
                 VariableInformation variableInformation;
                 for (auto const& integerVariable : program.getGlobalIntegerVariables()) {

src/adapters/extendedCarl.h

@@ -9,6 +9,7 @@
 #define STORM_ADAPTERS_EXTENDEDCARL_H_
 
 #include <carl/core/MultivariatePolynomial.h>
+#include <carl/core/RationalFunction.h>
 
 namespace carl
 {
@@ -18,6 +19,13 @@ inline size_t hash_value(carl::MultivariatePolynomial<C,O,P> const& p)
 	std::hash<carl::MultivariatePolynomial<C,O,P>> h;
 	return h(p);
 }
+template<typename Pol>
+inline size_t hash_value(carl::RationalFunction<Pol> const& f)
+{
+	std::hash<Pol> h;
+	return h(f.nominator()) ^ h(f.denominator());
+}
+
 }
 
 #endif

src/modelchecker/reachability/DirectEncoding.h

@@ -20,51 +20,81 @@ namespace storm
 			{
 			public:
 				template<typename T>
-				void encodeAsSmt2(const storm::models::Dtmc<T>& model, storm::storage::BitVector finalStates, T threshold, bool lessequal = true)
+				std::string encodeAsSmt2(const storm::models::Dtmc<T>& model, std::vector<carl::Variable> parameters, storm::storage::BitVector initialStates, storm::storage::BitVector finalStates, const typename T::CoeffType& threshold, bool lessequal = false)
 				{
 					carl::io::WriteTosmt2Stream smt2;
 					uint_fast64_t nrStates = model.getNumberOfStates();
 					carl::VariablePool& vpool = carl::VariablePool::getInstance();
 					std::vector<carl::Variable> stateVars;
-					for(uint_fast64_t state = 0; state < nrStates; ++state)
+					for(carl::Variable p : parameters)
 					{
-						carl::Variable stateVar = vpool.getFreshVariable("s_" + std::to_string(state));
-						stateVars.push_back(stateVar);
 						smt2 << carl::io::smt2flag::ASSERT;
 						smt2 << carl::io::smt2node::AND;
-						smt2 << carl::Constraint<Polynomial>(Polynomial(stateVar), carl::CompareRelation::GE);
-						smt2 << carl::Constraint<Polynomial>(Polynomial(stateVar) - Polynomial(1), carl::CompareRelation::LE);
+						smt2 << carl::Constraint<Polynomial>(Polynomial(p), carl::CompareRelation::GT);
+						smt2 << carl::Constraint<Polynomial>(Polynomial(p) - Polynomial(1), carl::CompareRelation::LT);
 						smt2 << carl::io::smt2node::CLOSENODE;
 					}
+					for(uint_fast64_t state = 0; state < nrStates-1; ++state)
+					{
+						
+						carl::Variable stateVar = vpool.getFreshVariable("s_" + std::to_string(state));
+						stateVars.push_back(stateVar);
+						if(!finalStates[state])
+						{
+							smt2 << carl::io::smt2flag::ASSERT;
+							smt2 << carl::io::smt2node::AND;
+							smt2 << carl::Constraint<Polynomial>(Polynomial(stateVar), carl::CompareRelation::GE);
+							smt2 << carl::Constraint<Polynomial>(Polynomial(stateVar) - Polynomial(1), carl::CompareRelation::LE);
+							smt2 << carl::io::smt2node::CLOSENODE;
+						}
+						
+					}
 					smt2 << carl::io::smt2flag::ASSERT;
 					smt2 << carl::io::smt2node::AND;
 					smt2.setAutomaticLineBreaks(true);
-					Polynomial finalStateReachSum;
-					for(uint_fast64_t state = 0; state < nrStates; ++state)
+					Polynomial initStateReachSum;
+					for(uint_fast64_t state = 0; state < nrStates-1; ++state)
 					{
+						if(initialStates[state])
+						{
+							initStateReachSum += stateVars[state];
+						}
 						if(finalStates[state])
 						{
-							smt2 << carl::Constraint<Polynomial>(Polynomial(stateVars[state]) - Polynomial(1), carl::CompareRelation::EQ);	
-							finalStateReachSum += stateVars[state];
+							//smt2 << carl::Constraint<Polynomial>(Polynomial(stateVars[state]) - Polynomial(1), carl::CompareRelation::EQ);	
 						}
 						else
 						{
-							Polynomial reachpropPol(0);
+							T reachpropPol(0);
 							for(auto const& transition : model.getRows(state))
 							{
-								reachpropPol += stateVars[transition.first] * transition.second;
+								if(finalStates[transition.first])
+								{
+									reachpropPol += transition.second;
+								}
+								else if(transition.first == nrStates - 1)
+								{
+									// intentionally empty.
+								}
+								else
+								{
+									reachpropPol += transition.second * stateVars[transition.first];
+								}
+								
 							}
-							smt2 << carl::Constraint<Polynomial>(reachpropPol - stateVars[state], carl::CompareRelation::EQ);
+							smt2 << carl::Constraint<T>(reachpropPol - stateVars[state], carl::CompareRelation::EQ);
 						}
 					}
+					//smt2 << carl::Constraint<Polynomial>(Polynomial(stateVars[nrStates-1]), carl::CompareRelation::EQ);
 					smt2 << carl::io::smt2node::CLOSENODE;
 					smt2 << carl::io::smt2flag::ASSERT;
 					
 					carl::CompareRelation thresholdRelation = lessequal ? carl::CompareRelation::LE : carl::CompareRelation::GE;
-					smt2 <<  carl::Constraint<Polynomial>(finalStateReachSum - threshold, thresholdRelation);
+					smt2 <<  carl::Constraint<Polynomial>(initStateReachSum - threshold, thresholdRelation);
 					smt2 << carl::io::smt2flag::CHECKSAT;
-					std::cout << smt2;
-	
+					std::stringstream strm;
+					strm << smt2;
+					return strm.str();
 				}
 			};
 		}

src/models/AbstractDeterministicModel.h

@@ -116,6 +116,12 @@ class AbstractDeterministicModel: public AbstractModel<T> {
 
 			this->choiceLabeling.reset(newChoiceLabeling);
 		}
+		
+		virtual void makeAbsorbing(storage::BitVector states) 
+		{
+			assert(states.size() == this->getNumberOfStates());
+			this->transitionMatrix.makeRowsAbsorbing(states);
+		}
 };
 
 } // namespace models

src/models/Ctmdp.h

@@ -129,7 +129,7 @@ private:
 		// Get the settings object to customize linear solving.
 		for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
 			T sum = this->getTransitionMatrix().getRowSum(row);
-			if (sum == 0) continue;
+			if (sum == T(0)) continue;
 			if (storm::utility::isOne(sum)) return false;
 		}
 		return true;

src/models/Mdp.h

@@ -201,7 +201,7 @@ private:
 		for (uint_fast64_t row = 0; row < this->getTransitionMatrix().getRowCount(); row++) {
 			T sum = this->getTransitionMatrix().getRowSum(row);
                         
-			if (sum == 0) continue;
+			if (sum == T(0)) continue;
 			if (!storm::utility::isOne(sum))  {
 				return false;
 			}

src/storage/DeterministicTransition.h

@@ -0,0 +1,56 @@
+/** 
+ * @file:   DeterministicTransition.h
+ * @author: Sebastian Junges
+ *
+ * @since April 24, 2014
+ */
+
+#pragma once
+
+namespace storm
+{
+	namespace storage
+	{
+		typedef uint_fast64_t StateId;
+		
+		template<typename ProbabilityType>
+		class DeterministicTransition 
+		{
+			std::pair<StateId, ProbabilityType> mTransition;
+			
+		public:
+			DeterministicTransition(std::pair<StateId, ProbabilityType> const& transition) :
+			mTransition(transition)
+			{
+			}
+			
+			DeterministicTransition(std::pair<StateId, ProbabilityType> && transition) :
+			mTransition(transition)
+			{
+			}
+			
+			DeterministicTransition(StateId targetState) :
+			DeterministicTransition({targetState, ProbabilityType(0)})
+			{
+				
+			}
+			
+				
+			StateId& targetState() {
+				return mTransition.first;
+			}
+			StateId const& targetState() const {
+				return mTransition.first;
+			}
+			
+			ProbabilityType& probability() {
+				return mTransition.second;
+			}
+			
+			ProbabilityType const& probability() const {
+				return mTransition.second;
+			}
+			
+		};
+	}
+}

src/storage/SparseMatrix.cpp

@@ -936,6 +936,10 @@ namespace storm {
         template class SparseMatrixBuilder<Polynomial>;
         template class SparseMatrix<Polynomial>;
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<Polynomial> const& matrix);
+        template class SparseMatrixBuilder<RationalFunction>;
+        template class SparseMatrix<RationalFunction>;
+        template std::ostream& operator<<(std::ostream& out, SparseMatrix<RationalFunction> const& matrix);
+        
 #endif
         
         

src/storage/expressions/ExpressionEvaluation.h

@@ -13,8 +13,12 @@
 #include "IfThenElseExpression.h"
 #include "DoubleConstantExpression.h"
 #include "DoubleLiteralExpression.h"
+#include "BinaryNumericalFunctionExpression.h"
 
+#include "carl/numbers/DecimalStringToRational.h"
 #include "src/storage/parameters.h"
+#include "IntegerLiteralExpression.h"
+#include "BinaryExpression.h"
 
 namespace storm {
 namespace expressions {
@@ -28,7 +32,13 @@ namespace expressions {
 	template<>
 	struct StateType<Polynomial>
 	{
-		typedef carl::Variable type;
+		typedef std::map<std::string, carl::Variable> type;
+	};
+	
+	template<>
+	struct StateType<RationalFunction>
+	{
+		typedef std::map<std::string, carl::Variable> type;
 	};
 		
 	template<typename T, typename S>
@@ -45,57 +55,93 @@ namespace expressions {
 			
 			virtual void visit(IfThenElseExpression const* expression) 
 			{
-				bool condititionValue = expression->getCondition()->evaluateAsBool();
+				std::cout << "ite" << std::endl;
 				
 			}
 		
             virtual void visit(BinaryBooleanFunctionExpression const* expression) 
 			{
-				
+				std::cout << "bbf" << std::endl;
 			}
             virtual void visit(BinaryNumericalFunctionExpression const* expression) 
 			{
+				ExpressionEvaluationVisitor* visitor = new ExpressionEvaluationVisitor(mSharedState);
+				expression->getFirstOperand()->accept(visitor);
+				mValue = visitor->value();
+				expression->getSecondOperand()->accept(visitor);				
+				switch(expression->getOperatorType())
+				{
+					case BinaryNumericalFunctionExpression::OperatorType::Plus:
+						mValue += visitor->value();
+						break;
+					case BinaryNumericalFunctionExpression::OperatorType::Minus:
+						mValue -= visitor->value();
+						break;
+					case BinaryNumericalFunctionExpression::OperatorType::Times:
+						mValue *= visitor->value();
+						break;
+					case BinaryNumericalFunctionExpression::OperatorType::Divide:
+						mValue /= visitor->value();
+						break;
+					default:
+						// TODO exception.
+						assert(false);
+				}
 				
+				delete visitor;
 			}
             virtual void visit(BinaryRelationExpression const* expression) 
 			{
-				
+				std::cout << "br" << std::endl;
 			}
             virtual void visit(BooleanConstantExpression const* expression) 
 			{
-				
+				std::cout << "bc" << std::endl;
 			}
             virtual void visit(DoubleConstantExpression const* expression) 
 			{
-				
+				auto it =  mSharedState->find(expression->getConstantName());
+				if(it != mSharedState->end())
+				{
+					mValue = T(it->second);
+				}
+				else
+				{
+					carl::Variable nVar = carl::VariablePool::getInstance().getFreshVariable(expression->getConstantName());
+					mSharedState->emplace(expression->getConstantName(),nVar);
+					mValue = T(nVar);
+				}
 			}
             virtual void visit(IntegerConstantExpression const* expression) 
 			{
-				
+				std::cout << "ic" << std::endl;
 			}
             virtual void visit(VariableExpression const* expression) 
 			{
-				
+				std::cout << "ve" << std::endl;
 			}
             virtual void visit(UnaryBooleanFunctionExpression const* expression) 
 			{
-				
+				std::cout << "ubf" << std::endl;
 			}
             virtual void visit(UnaryNumericalFunctionExpression const* expression) 
 			{
-				
+				std::cout << "unf" << std::endl;
 			}
             virtual void visit(BooleanLiteralExpression const* expression) 
 			{
-				
+				std::cout << "bl" << std::endl;
 			}
             virtual void visit(IntegerLiteralExpression const* expression) 
 			{
-				
+				mValue = T(expression->getValue());
 			}
             virtual void visit(DoubleLiteralExpression const* expression) 
 			{
-				
+				std::stringstream str;
+				str << std::fixed << std::setprecision( 3 ) << expression->getValue();
+				carl::DecimalStringToRational<typename T::CoeffType> transform;
+				mValue = T(transform(str.str()));
 			}
 
 		const T& value() const
@@ -121,8 +167,12 @@ namespace expressions {
 		T evaluate(Expression const& expr, storm::expressions::SimpleValuation const* val)
 		{
 			ExpressionEvaluationVisitor<T, typename StateType<T>::type>*  visitor = new ExpressionEvaluationVisitor<T, typename StateType<T>::type>(&mState);
-			//expr.getBaseExpression().accept(visitor);
-			T result = T(mpq_class(expr.evaluateAsDouble(val)));
+			std::cout << expr;
+			std::cout.flush();
+			expr.getBaseExpression().accept(visitor);
+			T result = visitor->value();
+			result.simplify();
+			std::cout << " -> " << result << std::endl;
 			delete visitor;
 			return result;
 		}

src/storage/expressions/SimpleValuation.cpp

@@ -14,7 +14,7 @@ namespace storm {
         
         void SimpleValuation::addBooleanIdentifier(std::string const& name, bool initialValue) {
             this->booleanIdentifierToIndexMap->emplace(name, this->booleanValues.size());
-            this->booleanValues.push_back(false);
+            this->booleanValues.push_back(initialValue);
         }
         
         void SimpleValuation::addIntegerIdentifier(std::string const& name, int_fast64_t initialValue) {

src/storage/parameters.h

@@ -12,6 +12,7 @@ namespace storm
 {
 	typedef carl::MultivariatePolynomial<mpq_class> Polynomial;
 	//typedef Parameter  carl::Variable							;
+	typedef carl::RationalFunction<Polynomial> RationalFunction;
 }
 #endif
 

src/storage/prism/Program.cpp

@@ -264,14 +264,18 @@ namespace storm {
             std::vector<Constant> newConstants(this->getConstants());
             for (uint_fast64_t constantIndex = 0; constantIndex < newConstants.size(); ++constantIndex) {
                 auto const& constant = newConstants[constantIndex];
-                LOG_THROW(constant.isDefined(), storm::exceptions::InvalidArgumentException, "Cannot substitute constants in program that contains undefined constants.");
+                //LOG_THROW(constant.isDefined(), storm::exceptions::InvalidArgumentException, "Cannot substitute constants in program that contains undefined constants.");
                 
                 // Put the corresponding expression in the substitution.
-                constantSubstitution.emplace(constant.getName(), constant.getExpression());
+                if(constant.isDefined())
+                {
+                    constantSubstitution.emplace(constant.getName(), constant.getExpression());
                 
-                // If there is at least one more constant to come, we substitute the costants we have so far.
-                if (constantIndex + 1 < newConstants.size()) {
-                    newConstants[constantIndex + 1] = newConstants[constantIndex + 1].substitute(constantSubstitution);
+                
+                    // If there is at least one more constant to come, we substitute the costants we have so far.
+                    if (constantIndex + 1 < newConstants.size()) {
+                        newConstants[constantIndex + 1] = newConstants[constantIndex + 1].substitute(constantSubstitution);
+                    }
                 }
             }
             

src/storm.cpp

@@ -426,7 +426,7 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
  */
 int main(const int argc, const char* argv[]) {
     // Register a signal handler to catch signals and display a backtrace.
-	installSignalHandler();
+	//installSignalHandler();
     
     // Print an information header.
 	printHeader(argc, argv);

src/stormParametric.cpp

@@ -1,5 +1,14 @@
+#include <memory>
+#include <stdint.h>
+
 #include "stormParametric.h"
 #include "adapters/ExplicitModelAdapter.h"
+#include "utility/graph.h"
+#include "modelchecker/reachability/DirectEncoding.h"
+#include "storage/BitVector.h"
+#include "storage/DeterministicTransition.h"
+
+using storm::storage::StateId;
 
 namespace storm
 {
@@ -7,14 +16,110 @@ namespace storm
 
 void ParametricStormEntryPoint::createModel()
 {
-    std::shared_ptr<storm::models::AbstractModel < Polynomial>> model = storm::adapters::ExplicitModelAdapter<Polynomial>::translateProgram(mProgram, mConstants);
-    model->printModelInformationToStream(std::cout);
+    mModel = storm::adapters::ExplicitModelAdapter<RationalFunction>::translateProgram(mProgram, mConstants);
+    mModel->printModelInformationToStream(std::cout);
 }
 
+std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& label)
+{
+    
+    storm::storage::BitVector phiStates(mModel->getNumberOfStates(), true);
+    storm::storage::BitVector initStates = mModel->getInitialStates();
+    storm::storage::BitVector targetStates = mModel->getLabeledStates(label);
+    
+    std::shared_ptr<models::Dtmc<RationalFunction>> dtmc = mModel->as<models::Dtmc<RationalFunction>>();
+    // 1. make target states absorbing.
+    dtmc->makeAbsorbing(targetStates);
+    // 2. throw away anything which does not add to the reachability probability.
+    // 2a. remove non productive states
+    storm::storage::BitVector productive = utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, targetStates);
+    // 2b. throw away non reachable states
+    storm::storage::BitVector reachable = utility::graph::performProbGreater0(*dtmc, dtmc->getTransitionMatrix(), phiStates, initStates);
+    storm::storage::BitVector bv = productive & reachable;
+    models::Dtmc<RationalFunction> subdtmc = dtmc->getSubDtmc(bv);
+    
+    phiStates = storm::storage::BitVector(subdtmc.getNumberOfStates(), true);
+    initStates = subdtmc.getInitialStates();
+    targetStates = subdtmc.getLabeledStates(label);
+    storm::storage::BitVector deadlockStates(phiStates);
+    deadlockStates.set(subdtmc.getNumberOfStates()-1,false);
+    // Calculate whether there are states which surely lead into the target.
+    storm::storage::BitVector potentialIntoDeadlock = utility::graph::performProbGreater0(subdtmc, subdtmc.getBackwardTransitions(), phiStates, deadlockStates);
+    storm::storage::BitVector extraTargets = ~potentialIntoDeadlock & ~targetStates;
+    if(extraTargets.empty())
+    {
+        // TODO implement this if necessary.
+        std::cout << "Extra targets exist. Please implement!" << std::endl;
+    }
+    // Search for states with only one non-deadlock successor.
+    std::map<StateId, storage::DeterministicTransition<RationalFunction>> chainedStates;
+    StateId nrStates = subdtmc.getNumberOfStates();
+    StateId deadlockState = nrStates - 1;
+    for(StateId source = 0; source < nrStates; ++source)
+    {
+        storage::DeterministicTransition<RationalFunction> productiveTransition(nrStates);
+        for(auto const& transition : subdtmc.getRows(source))
+        {
+            if(productiveTransition.targetState() == nrStates)
+            {
+                // first transition.
+                productiveTransition = transition;
+            }
+            else
+            {
+                // second transition
+                if(transition.first != deadlockState)
+                {
+                    productiveTransition.targetState() = nrStates;
+                    break;
+                }
+            }
+        }
+        if(productiveTransition.targetState() != nrStates)
+        {
+            chainedStates.emplace(source, productiveTransition);
+        }
+        for(auto chainedState : chainedStates)
+        {
+            auto it = chainedStates.find(chainedState.second.targetState());
+            if(it != chainedStates.end())
+            {
+                chainedState.second.targetState() = it->second.targetState();
+                chainedState.second.probability() *= it->second.probability();
+            }
+        }
+    }
+
+    modelchecker::reachability::DirectEncoding dec;
+    std::vector<carl::Variable> parameters;
+    for(auto constant : mProgram.getConstants())
+    {
+        if(!constant.isDefined())
+        {
+            std::cout << constant.getName() << std::endl;
+            carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName());
+            assert(p != carl::Variable::NO_VARIABLE);
+            parameters.push_back(p);
+        }
+    }
+    return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates(label), mpq_class(1,2));
+    
+}
+
+
 void storm_parametric(const std::string& constants, const storm::prism::Program& program)
 {
     ParametricStormEntryPoint entry(constants, program);
     entry.createModel();
+    storm::settings::Settings* s = storm::settings::Settings::getInstance();
+    if(s->isSet("reachability"))
+    {
+        std::ofstream fstream("test.smt2");
+        fstream << entry.reachabilityToSmt2(s->getOptionByLongName("reachability").getArgument(0).getValueAsString());
+        fstream.close();
+    }
+    
+    
 }
 
 }

src/stormParametric.h

@@ -13,7 +13,7 @@ namespace storm
 	private:
 		std::string const& mConstants;
 		storm::prism::Program const& mProgram;
-		std::shared_ptr<storm::models::AbstractModel<Polynomial>> mModel;
+		std::shared_ptr<storm::models::AbstractModel<RationalFunction>> mModel;
 	public:
 		ParametricStormEntryPoint(std::string const& constants, storm::prism::Program const& program) :
 		mConstants(constants),
@@ -23,6 +23,7 @@ namespace storm
 		}
 		
 		void createModel();
+		std::string reachabilityToSmt2(std::string const&);
 		
 		virtual ~ParametricStormEntryPoint() {}
 		

src/utility/StormOptions.cpp

@@ -38,7 +38,7 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings
     
     settings->addOption(storm::settings::OptionBuilder("StoRM Main", "parameters", "", "Enable parameters.").build());
 	
-    settings->addOption(storm::settings::OptionBuilder("StoRM Main", "reachability", "", "Export reachability problem.").build());
+    settings->addOption(storm::settings::OptionBuilder("StoRM Main", "reachability", "", "Export reachability problem.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("label", "The labelling for the reachability state set").build()).build());
     std::vector<std::string> linearEquationSolver;
 	linearEquationSolver.push_back("gmm++");
 	linearEquationSolver.push_back("native");