From d4c2657856da5fbb1c69060e3ac278f430ebdb56 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 24 Apr 2014 11:45:15 +0200 Subject: [PATCH] Parsing parameteric dtmcs and exporting them to smt2 Former-commit-id: c791625d40780cf3d72fad2cbd89e417c3b6aaa7 --- src/adapters/ExplicitModelAdapter.h | 10 +- src/adapters/extendedCarl.h | 8 ++ .../reachability/DirectEncoding.h | 62 +++++++--- src/models/AbstractDeterministicModel.h | 6 + src/models/Ctmdp.h | 2 +- src/models/Mdp.h | 2 +- src/storage/DeterministicTransition.h | 56 +++++++++ src/storage/SparseMatrix.cpp | 4 + .../expressions/ExpressionEvaluation.h | 80 ++++++++++--- src/storage/expressions/SimpleValuation.cpp | 2 +- src/storage/parameters.h | 1 + src/storage/prism/Program.cpp | 14 ++- src/storm.cpp | 2 +- src/stormParametric.cpp | 109 +++++++++++++++++- src/stormParametric.h | 3 +- src/utility/StormOptions.cpp | 2 +- 16 files changed, 316 insertions(+), 47 deletions(-) create mode 100644 src/storage/DeterministicTransition.h diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index cc2c14c89..af7f08d77 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/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> 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 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::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> 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 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 eval; + VariableInformation variableInformation; for (auto const& integerVariable : program.getGlobalIntegerVariables()) { diff --git a/src/adapters/extendedCarl.h b/src/adapters/extendedCarl.h index 6cf548e7c..2b306580e 100644 --- a/src/adapters/extendedCarl.h +++ b/src/adapters/extendedCarl.h @@ -9,6 +9,7 @@ #define STORM_ADAPTERS_EXTENDEDCARL_H_ #include +#include namespace carl { @@ -18,6 +19,13 @@ inline size_t hash_value(carl::MultivariatePolynomial const& p) std::hash> h; return h(p); } +template +inline size_t hash_value(carl::RationalFunction const& f) +{ + std::hash h; + return h(f.nominator()) ^ h(f.denominator()); +} + } #endif \ No newline at end of file diff --git a/src/modelchecker/reachability/DirectEncoding.h b/src/modelchecker/reachability/DirectEncoding.h index 87a151ae4..46ea6fe92 100644 --- a/src/modelchecker/reachability/DirectEncoding.h +++ b/src/modelchecker/reachability/DirectEncoding.h @@ -20,51 +20,81 @@ namespace storm { public: template - void encodeAsSmt2(const storm::models::Dtmc& model, storm::storage::BitVector finalStates, T threshold, bool lessequal = true) + std::string encodeAsSmt2(const storm::models::Dtmc& model, std::vector 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 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(stateVar), carl::CompareRelation::GE); - smt2 << carl::Constraint(Polynomial(stateVar) - Polynomial(1), carl::CompareRelation::LE); + smt2 << carl::Constraint(Polynomial(p), carl::CompareRelation::GT); + smt2 << carl::Constraint(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(stateVar), carl::CompareRelation::GE); + smt2 << carl::Constraint(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(stateVars[state]) - Polynomial(1), carl::CompareRelation::EQ); - finalStateReachSum += stateVars[state]; + //smt2 << carl::Constraint(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(reachpropPol - stateVars[state], carl::CompareRelation::EQ); + smt2 << carl::Constraint(reachpropPol - stateVars[state], carl::CompareRelation::EQ); } } + //smt2 << carl::Constraint(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(finalStateReachSum - threshold, thresholdRelation); + smt2 << carl::Constraint(initStateReachSum - threshold, thresholdRelation); smt2 << carl::io::smt2flag::CHECKSAT; - std::cout << smt2; - + std::stringstream strm; + strm << smt2; + return strm.str(); } }; } diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index c72b914de..561d06e44 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -116,6 +116,12 @@ class AbstractDeterministicModel: public AbstractModel { this->choiceLabeling.reset(newChoiceLabeling); } + + virtual void makeAbsorbing(storage::BitVector states) + { + assert(states.size() == this->getNumberOfStates()); + this->transitionMatrix.makeRowsAbsorbing(states); + } }; } // namespace models diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index 4c5d7da79..5d44935be 100644 --- a/src/models/Ctmdp.h +++ b/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; diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 73a73a1d9..ceb64ee3b 100644 --- a/src/models/Mdp.h +++ b/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; } diff --git a/src/storage/DeterministicTransition.h b/src/storage/DeterministicTransition.h new file mode 100644 index 000000000..1aaa2d583 --- /dev/null +++ b/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 + class DeterministicTransition + { + std::pair mTransition; + + public: + DeterministicTransition(std::pair const& transition) : + mTransition(transition) + { + } + + DeterministicTransition(std::pair && 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; + } + + }; + } +} \ No newline at end of file diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index a3f34dbac..bf5b038a1 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -936,6 +936,10 @@ namespace storm { template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template class SparseMatrixBuilder; + template class SparseMatrix; + template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + #endif diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h index b5ff55e6d..e246833ff 100644 --- a/src/storage/expressions/ExpressionEvaluation.h +++ b/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 { - typedef carl::Variable type; + typedef std::map type; + }; + + template<> + struct StateType + { + typedef std::map type; }; template @@ -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 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::type>* visitor = new ExpressionEvaluationVisitor::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; } diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index fb6f0088c..6674dfbd3 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/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) { diff --git a/src/storage/parameters.h b/src/storage/parameters.h index 22a3753f2..852215b83 100644 --- a/src/storage/parameters.h +++ b/src/storage/parameters.h @@ -12,6 +12,7 @@ namespace storm { typedef carl::MultivariatePolynomial Polynomial; //typedef Parameter carl::Variable ; + typedef carl::RationalFunction RationalFunction; } #endif diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index cdbba3e22..4b2996cb8 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -264,14 +264,18 @@ namespace storm { std::vector 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); + } } } diff --git a/src/storm.cpp b/src/storm.cpp index bb175acbb..d34ff13c1 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -426,7 +426,7 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker */ 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); diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp index 044cbcc9e..81de7704c 100644 --- a/src/stormParametric.cpp +++ b/src/stormParametric.cpp @@ -1,5 +1,14 @@ +#include +#include + #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> model = storm::adapters::ExplicitModelAdapter::translateProgram(mProgram, mConstants); - model->printModelInformationToStream(std::cout); + mModel = storm::adapters::ExplicitModelAdapter::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> dtmc = mModel->as>(); + // 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 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> chainedStates; + StateId nrStates = subdtmc.getNumberOfStates(); + StateId deadlockState = nrStates - 1; + for(StateId source = 0; source < nrStates; ++source) + { + storage::DeterministicTransition 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 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(); + } + + } } diff --git a/src/stormParametric.h b/src/stormParametric.h index e58b45113..b58cfab7c 100644 --- a/src/stormParametric.h +++ b/src/stormParametric.h @@ -13,7 +13,7 @@ namespace storm private: std::string const& mConstants; storm::prism::Program const& mProgram; - std::shared_ptr> mModel; + std::shared_ptr> 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() {} diff --git a/src/utility/StormOptions.cpp b/src/utility/StormOptions.cpp index dd366a076..1fcfb4d06 100644 --- a/src/utility/StormOptions.cpp +++ b/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 linearEquationSolver; linearEquationSolver.push_back("gmm++"); linearEquationSolver.push_back("native");