diff --git a/src/storm/modelchecker/parametric/ParameterLifting.cpp b/src/storm/modelchecker/parametric/ParameterLifting.cpp index a0ab01eeb..01e44a830 100644 --- a/src/storm/modelchecker/parametric/ParameterLifting.cpp +++ b/src/storm/modelchecker/parametric/ParameterLifting.cpp @@ -222,14 +222,15 @@ namespace storm { std::stringstream stream; - uint_fast64_t const size = 64; + uint_fast64_t const sizeX = 128; + uint_fast64_t const sizeY = 64; stream << "Parameter lifting result (visualization):" << std::endl; stream << " \t x-axis: " << x << " \t y-axis: " << y << " \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl; - for (uint_fast64_t i = 0; i < 2*size+2; ++i) stream << "#"; stream << std::endl; + for (uint_fast64_t i = 0; i < sizeX+2; ++i) stream << "#"; stream << std::endl; - ValueType deltaX = (parameterSpace.getUpperBoundary(x) - parameterSpace.getLowerBoundary(x)) / storm::utility::convertNumber(size); - ValueType deltaY = (parameterSpace.getUpperBoundary(y) - parameterSpace.getLowerBoundary(y)) / storm::utility::convertNumber(size); + ValueType deltaX = (parameterSpace.getUpperBoundary(x) - parameterSpace.getLowerBoundary(x)) / storm::utility::convertNumber(sizeX); + ValueType deltaY = (parameterSpace.getUpperBoundary(y) - parameterSpace.getLowerBoundary(y)) / storm::utility::convertNumber(sizeY); ValueType printedRegionArea = deltaX * deltaY; for (ValueType yUpper = parameterSpace.getUpperBoundary(y); yUpper != parameterSpace.getLowerBoundary(y); yUpper -= deltaY) { ValueType yLower = yUpper - deltaY; @@ -257,16 +258,16 @@ namespace storm { } } if (currRegionComplete && currRegionSafe && !currRegionUnSafe) { - stream << "SS"; + stream << "S"; } else if (currRegionComplete && currRegionUnSafe && !currRegionSafe) { - stream << " "; + stream << " "; } else { - stream << "--"; + stream << "-"; } } stream << "#" << std::endl; } - for (uint_fast64_t i = 0; i < 2*size+2; ++i) stream << "#"; stream << std::endl; + for (uint_fast64_t i = 0; i < sizeX+2; ++i) stream << "#"; stream << std::endl; return stream.str(); } diff --git a/src/storm/settings/modules/ParametricSettings.cpp b/src/storm/settings/modules/ParametricSettings.cpp index 844f214c3..76ca0adc9 100644 --- a/src/storm/settings/modules/ParametricSettings.cpp +++ b/src/storm/settings/modules/ParametricSettings.cpp @@ -24,9 +24,9 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, encodeSmt2StrategyOptionName, true, "Set the smt2 encoding strategy.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("strategy", "the used strategy").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportSmt2DestinationPathOptionName, true, "A path to a file where the result should be saved.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportResultDestinationPathOptionName, true, "A path to a file where the smt2 encoding should be saved.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, parameterSpaceOptionName, true, "Sets the considered parameter-space (i.e., the initial region) for parameter lifting.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("region", "The parameter-space (given in format a<=x<=b,c<=y<=d).").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, refinementThresholdOptionName, true, "Parameter space refinement converges if the fraction of unknown area falls below this threshold.")