diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index b7ed5da29..b62a8cb2b 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -1,5 +1,5 @@ -#include +#include #include #include "storm-pars/api/storm-pars.h" #include "storm-pars/settings/ParsSettings.h" @@ -437,9 +437,6 @@ namespace storm { storm::pars::verifyWithSparseEngine(model->as>(), input, regions, samples); } - - - template void processInputWithValueTypeAndDdlib(SymbolicInput& input) { auto coreSettings = storm::settings::getModule(); @@ -465,17 +462,32 @@ namespace storm { if (parSettings.isMonotonicityAnalysisSet()) { std::cout << "Hello, Jip1" << std::endl; storm::utility::Stopwatch simplifyingWatch(true); - auto consideredModel = (model->as>()); - // TODO: check if it is a Dtmc - auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*consideredModel); + if (model->isOfType(storm::models::ModelType::Dtmc)) { + auto consideredModel = (model->as>()); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*consideredModel); - std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); - STORM_LOG_THROW(formulas.begin()!=formulas.end(), storm::exceptions::NotSupportedException, "Only one formula at the time supported"); + std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); + STORM_LOG_THROW(formulas.begin()!=formulas.end(), storm::exceptions::NotSupportedException, "Only one formula at the time supported"); - if (!simplifier.simplify(*(formulas[0]))) { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); + if (!simplifier.simplify(*(formulas[0]))) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); + } + model = simplifier.getSimplifiedModel(); + } else if (model->isOfType(storm::models::ModelType::Mdp)) { + auto consideredModel = (model->as>()); + auto simplifier = storm::transformer::SparseParametricMdpSimplifier>(*consideredModel); + + std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); + STORM_LOG_THROW(formulas.begin()!=formulas.end(), storm::exceptions::NotSupportedException, "Only one formula at the time supported"); + + if (!simplifier.simplify(*(formulas[0]))) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull."); + } + model = simplifier.getSimplifiedModel(); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); } - model = simplifier.getSimplifiedModel(); + simplifyingWatch.stop(); STORM_PRINT(std::endl << "Time for model simplification: " << simplifyingWatch << "." << std::endl << std::endl); model->printModelInformationToStream(std::cout); @@ -491,9 +503,9 @@ namespace storm { } if (parSettings.isMonotonicityAnalysisSet()) { - // Do something more fancy. std::cout << "Hello, Jip2" << std::endl; storm::utility::Stopwatch latticeWatch(true); + std::shared_ptr> sparseModel = model->as>(); std::vector> formulas = storm::api::extractFormulasFromProperties(input.properties); @@ -535,11 +547,13 @@ namespace storm { for (auto itr = vars.begin(); itr != vars.end(); ++itr) { auto derivative = val.derivative(*itr); STORM_LOG_THROW(derivative.isConstant(), storm::exceptions::NotSupportedException, "Expecting probability to have at most degree 1"); - auto compare = lattice->compare(first.getColumn(), second.getColumn()); + if (varsMonotoneIncr.find(*itr) == varsMonotoneIncr.end()) { varsMonotoneIncr[*itr] = true; varsMonotoneDecr[*itr] = true; } + + auto compare = lattice->compare(first.getColumn(), second.getColumn()); if (compare == 1) { varsMonotoneIncr.find(*itr)->second &=derivative.constantPart() >= 0; varsMonotoneDecr.find(*itr)->second &=derivative.constantPart() <= 0;