From ecc74595ba40e711af7bedf1f287d3cf881e2e7b Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 20 Oct 2016 01:40:59 +0200 Subject: [PATCH] several jani related fixes: IsInitialRestrictionSet(), FormulaContext, minor things Former-commit-id: f1a5b2edcf29739de8996cdd42a9456297860bb4 [formerly 6a9cb0a9886a5a2597d83e6fad14add828a08625] Former-commit-id: 11bf234fcc0662135aefef4d2e9eb025b25386b6 --- src/cli/cli.cpp | 4 ++ src/parser/JaniParser.cpp | 59 ++++++++++++++++++----------- src/parser/JaniParser.h | 12 ++++-- src/settings/modules/IOSettings.cpp | 7 +++- src/settings/modules/IOSettings.h | 6 +++ src/storage/jani/Automaton.cpp | 9 ++++- src/storm-pgcl.cpp | 4 +- 7 files changed, 71 insertions(+), 30 deletions(-) diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index a1b20b546..2d0b467aa 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -258,6 +258,10 @@ namespace storm { } } + if (ioSettings.isNoBuildModelSet()) { + return; + } + // Get the string that assigns values to the unknown currently undefined constants in the model. std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); model = model.preprocess(constantDefinitionString); diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index b328969d9..a149a9e92 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -142,16 +142,16 @@ namespace storm { } - std::vector> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context) { + std::vector> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context) { STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << context); - return { parseFormula(propertyStructure.at("exp"), "Operand of operator " + opstring) }; + return { parseFormula(propertyStructure.at("exp"), formulaContext, "Operand of operator " + opstring) }; } - std::vector> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context) { + std::vector> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context) { STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << context); STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << context); - return { parseFormula(propertyStructure.at("left"), "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), "Operand of operator " + opstring) }; + return { parseFormula(propertyStructure.at("left"), formulaContext, "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), formulaContext, "Operand of operator " + opstring) }; } storm::jani::PropertyInterval JaniParser::parsePropertyInterval(json const& piStructure) { @@ -185,8 +185,15 @@ namespace storm { } - std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, std::string const& context, boost::optional> bound) { - + std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional> bound) { + if (propertyStructure.is_boolean()) { + return std::make_shared(propertyStructure.get()); + } + if (propertyStructure.is_string()) { + if (labels.count(propertyStructure.get()) > 0) { + return std::make_shared(propertyStructure.get()); + } + } storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true); if(expr.isInitialized()) { assert(bound == boost::none); @@ -195,7 +202,7 @@ namespace storm { std::string opString = getString(propertyStructure.at("op"), "Operation description"); if(opString == "Pmin" || opString == "Pmax") { - std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + std::vector> args = parseUnaryFormulaArgument(propertyStructure, storm::logic::FormulaContext::Probability, opString, ""); assert(args.size() == 1); storm::logic::OperatorInformation opInfo; opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; @@ -206,9 +213,17 @@ namespace storm { assert(bound == boost::none); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); } else if (opString == "Emin" || opString == "Emax") { + bool time=false; + STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); + storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), "Reward expression in " + context); + if (rewExpr.isVariable()) { + time = false; + } else { + time = true; + } std::shared_ptr reach; if (propertyStructure.count("reach") > 0) { - reach = parseFormula(propertyStructure.at("reach"), "Reach-expression of operator " + opString); + reach = parseFormula(propertyStructure.at("reach"), time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward, "Reach-expression of operator " + opString); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Total reward is currently not supported"); } @@ -216,9 +231,6 @@ namespace storm { opInfo.optimalityType = opString == "Emin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.bound = bound; - STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); - storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), "Reward expression in " + context); - bool accTime = false; bool accSteps = false; if (propertyStructure.count("accumulate") > 0) { @@ -280,8 +292,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently."); } - STORM_LOG_THROW(accTime || accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given."); - assert(!accTime && !accSteps); + //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given."); if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); @@ -311,16 +322,15 @@ namespace storm { } else if (opString == "Smin" || opString == "Smax") { - std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); } else if (opString == "U" || opString == "F") { assert(bound == boost::none); std::vector> args; if (opString == "U") { - args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, ""); } else { assert(opString == "F"); - args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, ""); args.push_back(args[0]); args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula(); } @@ -352,13 +362,13 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); } if (args[0]->isTrueFormula()) { - return std::make_shared(args[1]); + return std::make_shared(args[1], storm::logic::FormulaContext::Reward); } else { return std::make_shared(args[0], args[1]); } } else if (opString == "G") { assert(bound == boost::none); - std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, "Subformula of globally operator " + context); + std::vector> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, "Subformula of globally operator " + context); if (propertyStructure.count("step-bounds") > 0) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and step-bounds are not supported currently"); } else if (propertyStructure.count("time-bounds") > 0) { @@ -376,13 +386,13 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Release is not supported"); } else if (opString == "∧" || opString == "∨") { assert(bound == boost::none); - std::vector> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + std::vector> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, ""); assert(args.size() == 2); storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; return std::make_shared(oper, args[0], args[1]); } else if (opString == "¬") { assert(bound == boost::none); - std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + std::vector> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, ""); assert(args.size() == 1); return std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); @@ -402,12 +412,12 @@ namespace storm { auto expr = parseExpression(propertyStructure.at("right"), "Threshold for operator " + propertyStructure.at("left").at("op").get()); STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); // TODO evaluate this expression directly as rational number - return parseFormula(propertyStructure.at("left"), "", storm::logic::Bound(ct, storm::utility::convertNumber(expr.evaluateAsDouble()))); + return parseFormula(propertyStructure.at("left"), formulaContext, "", storm::logic::Bound(ct, storm::utility::convertNumber(expr.evaluateAsDouble()))); } else if(propertyStructure.at("right").count("op") > 0 && (propertyStructure.at("right").at("op") == "Pmin" || propertyStructure.at("right").at("op") == "Pmax" || propertyStructure.at("right").at("op") == "Emin" || propertyStructure.at("right").at("op") == "Emax" || propertyStructure.at("right").at("op") == "Smin" || propertyStructure.at("right").at("op") == "Smax")) { auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get()); STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); // TODO evaluate this expression directly as rational number - return parseFormula(propertyStructure.at("right"), "", storm::logic::Bound(ct, storm::utility::convertNumber(expr.evaluateAsDouble()))); + return parseFormula(propertyStructure.at("right"),formulaContext, "", storm::logic::Bound(ct, storm::utility::convertNumber(expr.evaluateAsDouble()))); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex comparisons are allowed."); @@ -465,7 +475,7 @@ namespace storm { std::string statesDescr = getString(expressionStructure.at("states").at("op"), "Filtered states in property named " + name); STORM_LOG_THROW(statesDescr == "initial", storm::exceptions::NotImplementedException, "Only initial states are allowed as set of states we are interested in."); STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); - auto formula = parseFormula(expressionStructure.at("values"), "Values of property " + name); + auto formula = parseFormula(expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, "Values of property " + name); return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft), comment); } @@ -581,6 +591,9 @@ namespace storm { initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); } + if(transientVar) { + labels.insert(name); + } return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar); } assert(!transientVar); diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index df36cd43c..438cb93d1 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -20,6 +20,10 @@ namespace storm { class Property; class PropertyInterval; } + + namespace logic { + enum class FormulaContext; + } namespace parser { @@ -54,12 +58,12 @@ namespace storm { * Helper for parsing the actions of a model. */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); - std::shared_ptr parseFormula(json const& propertyStructure, std::string const& context, boost::optional> bound = boost::none); + std::shared_ptr parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional> bound = boost::none); std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); - std::vector> parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context); - std::vector> parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context); + std::vector> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context); + std::vector> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context); storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure); @@ -75,6 +79,8 @@ namespace storm { * The expression manager to be used. */ std::shared_ptr expressionManager; + + std::set labels = {}; bool allowRecursion = true; diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index 868237b1a..84d9b1238 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -30,6 +30,7 @@ namespace storm { const std::string IOSettings::constantsOptionShortName = "const"; const std::string IOSettings::prismCompatibilityOptionName = "prismcompat"; const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; + const std::string IOSettings::noBuildOptionName = "nobuild"; const std::string IOSettings::fullModelBuildOptionName = "buildfull"; const std::string IOSettings::janiPropertyOptionName = "janiproperty"; const std::string IOSettings::janiPropertyOptionShortName = "jprop"; @@ -50,7 +51,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); - + this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); std::vector explorationOrders = {"dfs", "bfs"}; this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) @@ -186,6 +187,10 @@ namespace storm { bool IOSettings::isBuildFullModelSet() const { return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet(); } + + bool IOSettings::isNoBuildModelSet() const { + return this->getOption(noBuildOptionName).getHasOptionBeenSet(); + } void IOSettings::finalize() { } diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index cedbda8aa..d2c2bef58 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -211,6 +211,11 @@ namespace storm { */ bool isPrismCompatibilityEnabled() const; + /** + * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file + */ + bool isNoBuildModelSet() const; + /*! * Retrieves whether the full model should be build, that is, the model including all labels and rewards. * @@ -243,6 +248,7 @@ namespace storm { static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; static const std::string fullModelBuildOptionName; + static const std::string noBuildOptionName; static const std::string janiPropertyOptionName; static const std::string janiPropertyOptionShortName; }; diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 8e99f25c1..8ed71acbc 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -335,7 +335,14 @@ namespace storm { } bool Automaton::hasRestrictedInitialStates() const { - return hasInitialStatesRestriction() && !(getInitialStatesExpression().evaluateAsBool()); + if (!hasInitialStatesRestriction()) { + return false; + } + if (getInitialStatesExpression().containsVariables()) { + return true; + } else { + return !getInitialStatesExpression().evaluateAsBool(); + } } bool Automaton::hasInitialStatesRestriction() const { diff --git a/src/storm-pgcl.cpp b/src/storm-pgcl.cpp index 99ac1c960..a985e3a7b 100644 --- a/src/storm-pgcl.cpp +++ b/src/storm-pgcl.cpp @@ -37,9 +37,9 @@ void initializeSettings() { void handleJani(storm::jani::Model& model) { if (!storm::settings::getModule().isJaniFileSet()) { // For now, we have to have a jani file - storm::jani::JsonExporter::toStream(model, std::cout); + storm::jani::JsonExporter::toStream(model, {}, std::cout); } else { - storm::jani::JsonExporter::toFile(model, storm::settings::getModule().getJaniFilename()); + storm::jani::JsonExporter::toFile(model, {}, storm::settings::getModule().getJaniFilename()); } }