diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 49b573f33..fa4047dd6 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -6,6 +6,8 @@ #include "utility/storm.h" #include "storage/dft/DFTIsomorphism.h" +#include + /*! * Load DFT from filename, build corresponding Model and check against given property. * @@ -74,6 +76,20 @@ int main(int argc, char** argv) { } else if (option == "--probability") { assert(pctlFormula.empty()); pctlFormula = "P=? [F \"failed\"]"; + } else if (option == "--timebound") { + assert(pctlFormula.empty()); + ++i; + assert(i < argc); + double timeBound; + try { + timeBound = boost::lexical_cast(argv[i]); + } catch (boost::bad_lexical_cast e) { + std::cerr << "The time bound '" << argv[i] << "' is not valid." << std::endl; + return 2; + } + std::stringstream stream; + stream << "P=? [F<=" << timeBound << " \"failed\"]"; + pctlFormula = stream.str(); } else if (option == "--trace") { level = log4cplus::TRACE_LOG_LEVEL; } else if (option == "--debug") {