diff --git a/src/storm-parsers/parser/FormulaParser.cpp b/src/storm-parsers/parser/FormulaParser.cpp index 485a4bb18..d37d18a57 100644 --- a/src/storm-parsers/parser/FormulaParser.cpp +++ b/src/storm-parsers/parser/FormulaParser.cpp @@ -18,7 +18,7 @@ namespace storm { namespace parser { - + FormulaParser::FormulaParser() : manager(new storm::expressions::ExpressionManager()), grammar(new FormulaParserGrammar(manager)) { // Intentionally left empty. } @@ -40,25 +40,25 @@ namespace storm { FormulaParser::FormulaParser(FormulaParser const& other) : FormulaParser(other.manager) { other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); }); } - + FormulaParser& FormulaParser::operator=(FormulaParser const& other) { this->manager = other.manager; this->grammar = std::shared_ptr(new FormulaParserGrammar(this->manager)); other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); }); return *this; } - + std::shared_ptr FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const { std::vector property = parseFromString(formulaString); STORM_LOG_THROW(property.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << property.size() << " instead."); return property.front().getRawFormula(); } - + std::vector FormulaParser::parseFromFile(std::string const& filename) const { // Open file and initialize result. std::ifstream inputFileStream; storm::utility::openFile(filename, inputFileStream); - + std::vector properties; // Now try to parse the contents of the file. @@ -75,15 +75,15 @@ namespace storm { storm::utility::closeFile(inputFileStream); return properties; } - + std::vector FormulaParser::parseFromString(std::string const& formulaString) const { PositionIteratorType first(formulaString.begin()); PositionIteratorType iter = first; PositionIteratorType last(formulaString.end()); - + // Create empty result; std::vector result; - + // Create grammar. try { // Start parsing. @@ -93,15 +93,14 @@ namespace storm { } catch (qi::expectation_failure const& e) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_); } - return result; } - + void FormulaParser::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { // Record the mapping and hand it over to the grammar. this->identifiers_.add(identifier, expression); grammar->addIdentifierExpression(identifier, expression); } - + } // namespace parser } // namespace storm diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 72399c314..48918990b 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -139,9 +139,9 @@ namespace storm { if (actionCount > 0) { parseActions(parsedStructure.at("actions"), model); } - + Scope scope(name); - + // Parse constants ConstantsMap constants; scope.constants = &constants; @@ -157,7 +157,7 @@ namespace storm { constants.emplace(constant->getName(), &model.getConstants().back()); } } - + // Parse variables size_t variablesCount = parsedStructure.count("variables"); STORM_LOG_THROW(variablesCount < 2, storm::exceptions::InvalidJaniException, "Variable-declarations can be given at most once for global variables."); @@ -170,7 +170,7 @@ namespace storm { globalVars.emplace(variable->getName(), &model.addVariable(*variable)); } } - + uint64_t funDeclCount = parsedStructure.count("functions"); STORM_LOG_THROW(funDeclCount < 2, storm::exceptions::InvalidJaniException, "Model '" << name << "' has more than one list of functions"); FunctionsMap globalFuns; @@ -196,7 +196,7 @@ namespace storm { globalFuns[funDef.getName()] = &model.addFunctionDefinition(funDef); } } - + // Parse Automata STORM_LOG_THROW(parsedStructure.count("automata") == 1, storm::exceptions::InvalidJaniException, "Exactly one list of automata must be given"); STORM_LOG_THROW(parsedStructure.at("automata").is_array(), storm::exceptions::InvalidJaniException, "Automata must be an array"); @@ -215,7 +215,7 @@ namespace storm { std::shared_ptr composition = parseComposition(parsedStructure.at("system")); model.setSystemComposition(composition); model.finalize(); - + // Parse properties storm::logic::RewardAccumulationEliminationVisitor rewAccEliminator(model); STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given"); @@ -243,14 +243,14 @@ namespace storm { STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << scope.description); return { parseFormula(model, propertyStructure.at("exp"), formulaContext, scope.refine("Operand of operator " + opstring)) }; } - + template std::vector> JaniParser::parseBinaryFormulaArguments(storm::jani::Model& model, Json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) { STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << scope.description); STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << scope.description); return { parseFormula(model, propertyStructure.at("left"), formulaContext, scope.refine("Operand of operator " + opstring)), parseFormula(model, propertyStructure.at("right"), formulaContext, scope.refine("Operand of operator " + opstring)) }; } - + template storm::jani::PropertyInterval JaniParser::parsePropertyInterval(Json const& piStructure, Scope const& scope) { storm::jani::PropertyInterval pi; @@ -260,11 +260,11 @@ namespace storm { if (piStructure.count("lower-exclusive") > 0) { STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); pi.lowerBoundStrict = piStructure.at("lower-exclusive"); - + } if (piStructure.count("upper") > 0) { pi.upperBound = parseExpression(piStructure.at("upper"), scope.refine("Upper bound for property interval")); - + } if (piStructure.count("upper-exclusive") > 0) { STORM_LOG_THROW(pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); @@ -293,7 +293,7 @@ namespace storm { } return storm::logic::RewardAccumulation(accSteps, accTime, accExit); } - + void insertLowerUpperTimeBounds(std::vector>& lowerBounds, std::vector>& upperBounds, storm::jani::PropertyInterval const& pi) { if (pi.hasLowerBound()) { lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); @@ -334,7 +334,7 @@ namespace storm { } if (propertyStructure.count("op") == 1) { std::string opString = getString(propertyStructure.at("op"), "Operation description"); - + if(opString == "Pmin" || opString == "Pmax") { std::vector> args = parseUnaryFormulaArgument(model, propertyStructure, storm::logic::FormulaContext::Probability, opString, scope); assert(args.size() == 1); @@ -342,7 +342,7 @@ namespace storm { opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.bound = bound; return std::make_shared(args[0], opInfo); - + } else if (opString == "∀" || opString == "∃") { assert(bound == boost::none); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported in " << scope.description); @@ -352,7 +352,7 @@ namespace storm { storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), scope.refine("Reward expression")); STORM_LOG_THROW(rewExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << rewExpr << "' does not have numerical type in " << scope.description); std::string rewardName = rewExpr.toString(); - + storm::logic::OperatorInformation opInfo; opInfo.optimalityType = opString == "Emin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.bound = bound; @@ -361,7 +361,7 @@ namespace storm { if (propertyStructure.count("accumulate") > 0) { rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), scope.description); } - + bool time = false; if (propertyStructure.count("step-instant") > 0) { STORM_LOG_THROW(propertyStructure.count("time-instant") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a time-instant in " + scope.description); @@ -455,7 +455,7 @@ namespace storm { } auto subformula = std::make_shared(rewardAccumulation); return std::make_shared(subformula, rewardName, opInfo); - + } else if (opString == "U" || opString == "F") { assert(bound == boost::none); std::vector> args; @@ -467,7 +467,7 @@ namespace storm { args.push_back(args[0]); args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula(); } - + std::vector> lowerBounds, upperBounds; std::vector tbReferences; if (propertyStructure.count("step-bounds") > 0) { @@ -557,7 +557,7 @@ namespace storm { } else if (opString == ">") { ct = storm::logic::ComparisonType::Greater; } - + std::vector const leftRight = {"left", "right"}; for (uint64_t i = 0; i < 2; ++i) { if (propertyStructure.at(leftRight[i]).count("op") > 0) { @@ -598,7 +598,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Looking for operator for formula " << propertyStructure.dump() << ", but did not find one"); } } - + template storm::jani::Property JaniParser::parseProperty(storm::jani::Model& model, Json const& propertyStructure, Scope const& scope) { STORM_LOG_THROW(propertyStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Property must have a name"); @@ -612,7 +612,7 @@ namespace storm { STORM_LOG_THROW(propertyStructure.count("expression") == 1, storm::exceptions::InvalidJaniException, "Property must have an expression"); // Parse filter expression. Json const& expressionStructure = propertyStructure.at("expression"); - + STORM_LOG_THROW(expressionStructure.count("op") == 1, storm::exceptions::InvalidJaniException, "Expression in property must have an operation description"); STORM_LOG_THROW(expressionStructure.at("op") == "filter", storm::exceptions::InvalidJaniException, "Top level operation of a property must be a filter"); STORM_LOG_THROW(expressionStructure.count("fun") == 1, storm::exceptions::InvalidJaniException, "Filter must have a function descritpion"); @@ -641,7 +641,7 @@ namespace storm { } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown filter description " << funDescr << " in property named " << name); } - + STORM_LOG_THROW(expressionStructure.count("states") == 1, storm::exceptions::InvalidJaniException, "Filter must have a states description"); std::shared_ptr statesFormula; if (expressionStructure.at("states").count("op") > 0) { @@ -663,7 +663,7 @@ namespace storm { STORM_LOG_THROW(statesFormula, storm::exceptions::NotImplementedException, "Could not derive states formula."); STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); auto formula = parseFormula(model, expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, scope.refine("Values of property " + name)); - return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), {}, comment); + return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), {}, nullptr, comment); } template @@ -681,11 +681,11 @@ namespace storm { definingExpression = parseExpression(constantStructure.at("value"), scope.refine("Value of constant " + name)); assert(definingExpression.isInitialized()); } - + STORM_LOG_THROW(constantStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") must have a (single) type-declaration."); ParsedType type; parseType(type, constantStructure.at("type"), name, scope); - + STORM_LOG_THROW(type.basicType.is_initialized(), storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") has unexpected type"); storm::expressions::Variable var; switch (type.basicType.get()) { @@ -710,10 +710,10 @@ namespace storm { constraintExpression = var.getExpression() <= type.bounds->second; } } - + return std::make_shared(name, std::move(var), definingExpression, constraintExpression); } - + template void JaniParser::parseType(ParsedType& result, Json const& typeStructure, std::string variableName, Scope const& scope) { if (typeStructure.is_string()) { @@ -779,7 +779,7 @@ namespace storm { } } } - + template storm::jani::FunctionDefinition JaniParser::parseFunctionDefinition(Json const& functionDefinitionStructure, Scope const& scope, bool firstPass, std::string const& parameterNamePrefix) { STORM_LOG_THROW(functionDefinitionStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Function definition (scope: " + scope.description + ") must have a name"); @@ -787,7 +787,7 @@ namespace storm { STORM_LOG_THROW(functionDefinitionStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Function definition '" + functionName + "' (scope: " + scope.description + ") must have a (single) type-declaration."); ParsedType type; parseType(type, functionDefinitionStructure.at("type"), functionName, scope); - + std::unordered_map parameterNameToVariableMap; std::vector parameters; if (!firstPass && functionDefinitionStructure.count("parameters") > 0) { @@ -799,13 +799,13 @@ namespace storm { STORM_LOG_THROW(parameterStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Parameter declaration of parameter " + std::to_string(parameters.size()) + " of Function definition '" + functionName + "' (scope: " + scope.description + ") must have exactly one type."); parseType(parameterType, parameterStructure.at("type"), parameterName, scope.refine("parameter declaration of parameter " + std::to_string(parameters.size()) + " of function definition " + functionName)); STORM_LOG_WARN_COND(!parameterType.bounds.is_initialized(), "Bounds on parameter" + parameterName + " of function definition " + functionName + " will be ignored."); - + std::string exprParameterName = parameterNamePrefix + functionName + VARIABLE_AUTOMATON_DELIMITER + parameterName; parameters.push_back(expressionManager->declareVariable(exprParameterName, parameterType.expressionType)); parameterNameToVariableMap.emplace(parameterName, parameters.back()); } } - + STORM_LOG_THROW(functionDefinitionStructure.count("body") == 1, storm::exceptions::InvalidJaniException, "Function definition '" + functionName + "' (scope: " + scope.description + ") must have a (single) body."); storm::expressions::Expression functionBody; if (!firstPass) { @@ -815,7 +815,7 @@ namespace storm { return storm::jani::FunctionDefinition(functionName, type.expressionType, parameters, functionBody); } - + template std::shared_ptr JaniParser::parseVariable(Json const& variableStructure, bool requireInitialValues, Scope const& scope, std::string const& namePrefix) { STORM_LOG_THROW(variableStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Variable (scope: " + scope.description + ") must have a name"); @@ -845,7 +845,7 @@ namespace storm { } else { assert(!transientVar); } - + bool setInitValFromDefault = !initVal.is_initialized() && requireInitialValues; if (type.basicType) { switch (type.basicType.get()) { @@ -945,7 +945,7 @@ namespace storm { } return result; } - + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scope.description << ")."); } @@ -988,7 +988,7 @@ namespace storm { void ensureIntegerType(storm::expressions::Expression const& expr, std::string const& opstring, unsigned argNr, std::string const& errorInfo) { STORM_LOG_THROW(expr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects argument " + std::to_string(argNr) + " to be numerical in " << errorInfo << "."); } - + /** * Helper for parse expression. */ @@ -1411,7 +1411,7 @@ namespace storm { localFuns[funDef.getName()] = &automaton.addFunctionDefinition(funDef); } } - + STORM_LOG_THROW(automatonStructure.count("locations") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' does not have locations."); std::unordered_map locIds; for(auto const& locEntry : automatonStructure.at("locations")) { @@ -1500,7 +1500,7 @@ namespace storm { templateEdge->getAssignments().add(storm::jani::Assignment(lValue, assignmentExpr, assignmentIndex)); } } - + // destinations STORM_LOG_THROW(edgeEntry.count("destinations") == 1, storm::exceptions::InvalidJaniException, "A single list of destinations must be given in edge from '" << sourceLoc << "' in automaton '" << name << "'"); std::vector> destinationLocationsAndProbabilities; @@ -1550,7 +1550,7 @@ namespace storm { return automaton; } - + template std::vector parseSyncVectors(typename JaniParser::Json const& syncVectorStructure) { std::vector syncVectors; @@ -1586,9 +1586,9 @@ namespace storm { } return std::shared_ptr(new storm::jani::AutomatonComposition(compositionStructure.at("automaton").template get(), inputEnabledActions)); } - + STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given, got " << compositionStructure.dump()); - + if (compositionStructure.at("elements").size() == 1 && compositionStructure.count("syncs") == 0) { // We might have an automaton. STORM_LOG_THROW(compositionStructure.at("elements").back().count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in composition"); @@ -1598,9 +1598,9 @@ namespace storm { return std::shared_ptr(new storm::jani::AutomatonComposition(name)); } STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Trivial nesting parallel composition is not yet supported"); - + } - + std::vector> compositions; for (auto const& elemDecl : compositionStructure.at("elements")) { if(!allowRecursion) { @@ -1608,17 +1608,17 @@ namespace storm { } compositions.push_back(parseComposition(elemDecl)); } - + STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once"); std::vector syncVectors; if (compositionStructure.count("syncs") > 0) { syncVectors = parseSyncVectors(compositionStructure.at("syncs")); } - + return std::shared_ptr(new storm::jani::ParallelComposition(compositions, syncVectors)); - + } - + template class JaniParser; template class JaniParser; } diff --git a/src/storm/api/properties.cpp b/src/storm/api/properties.cpp index bd07cb013..9b134c069 100644 --- a/src/storm/api/properties.cpp +++ b/src/storm/api/properties.cpp @@ -37,19 +37,19 @@ namespace storm { reducedPropertyNames.insert(property.getName()); } } - + if (reducedPropertyNames.size() < propertyNameSet.size()) { std::set missingProperties; std::set_difference(propertyNameSet.begin(), propertyNameSet.end(), reducedPropertyNames.begin(), reducedPropertyNames.end(), std::inserter(missingProperties, missingProperties.begin())); STORM_LOG_WARN("Filtering unknown properties " << boost::join(missingProperties, ", ") << "."); } - + return result; } else { return properties; } } - + std::vector> extractFormulasFromProperties(std::vector const& properties) { std::vector> formulas; for (auto const& prop : properties) { @@ -57,7 +57,7 @@ namespace storm { } return formulas; } - + storm::jani::Property createMultiObjectiveProperty(std::vector const& properties) { std::set undefConstants; std::string name = ""; @@ -67,9 +67,10 @@ namespace storm { name += prop.getName(); comment += prop.getComment(); STORM_LOG_WARN_COND(prop.getFilter().isDefault(), "Non-default property filter of property " + prop.getName() + " will be dropped during conversion to multi-objective property."); + STORM_LOG_WARN_COND(!prop.isShieldingProperty(), "Shielding of multi-objective property is not possible yet. Dropping expression: '" + prop.getShieldingExpression()->toString() + "'."); } auto multiFormula = std::make_shared(extractFormulasFromProperties(properties)); - return storm::jani::Property(name, multiFormula, undefConstants, comment); + return storm::jani::Property(name, multiFormula, undefConstants, nullptr, comment); } } } diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 9169b89f4..2528e6c9a 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -15,25 +15,25 @@ namespace storm { RewardAccumulationEliminationVisitor::RewardAccumulationEliminationVisitor(storm::jani::Model const& model) : model(model) { // Intentionally left empty } - + std::shared_ptr RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const { boost::any result = f.accept(*this, boost::any()); return boost::any_cast>(result); } - + void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(std::vector& properties) const { for (auto& p : properties) { eliminateRewardAccumulations(p); } } - + void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(storm::jani::Property& property) const { auto formula = eliminateRewardAccumulations(*property.getFilter().getFormula()); auto states = eliminateRewardAccumulations(*property.getFilter().getStatesFormula()); storm::jani::FilterExpression fe(formula, property.getFilter().getFilterType(), states); - property = storm::jani::Property(property.getName(), storm::jani::FilterExpression(formula, property.getFilter().getFilterType(), states), property.getUndefinedConstants(), property.getComment()); + property = storm::jani::Property(property.getName(), storm::jani::FilterExpression(formula, property.getFilter().getFilterType(), states), property.getUndefinedConstants(), property.getShieldingExpression(), property.getComment()); } - + boost::any RewardAccumulationEliminationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; @@ -68,7 +68,7 @@ namespace storm { return std::static_pointer_cast(std::make_shared(left, right, lowerBounds, upperBounds, timeBoundReferences)); } } - + boost::any RewardAccumulationEliminationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { boost::optional rewAcc; STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); @@ -90,7 +90,7 @@ namespace storm { } return std::static_pointer_cast(std::make_shared(bounds, timeBoundReferences, rewAcc)); } - + boost::any RewardAccumulationEliminationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); auto rewName = boost::any_cast>(data); @@ -100,7 +100,7 @@ namespace storm { return std::static_pointer_cast(std::make_shared(f.getRewardAccumulation())); } } - + boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); if (f.hasRewardAccumulation()) { @@ -120,12 +120,12 @@ namespace storm { } return std::static_pointer_cast(std::make_shared(subformula, f.getContext())); } - + boost::any RewardAccumulationEliminationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, f.getOptionalRewardModelName())); return std::static_pointer_cast(std::make_shared(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); } - + boost::any RewardAccumulationEliminationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); auto rewName = boost::any_cast>(data); @@ -135,11 +135,11 @@ namespace storm { return std::static_pointer_cast(std::make_shared(f.getRewardAccumulation())); } } - + bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional rewardModelName) const { STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable for unique reward model."); storm::jani::RewardModelInformation info(model, rewardModelName.get()); - + if ((info.hasActionRewards() || info.hasTransitionRewards()) && !accumulation.isStepsSet()) { return false; } diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp index 988d23da4..772f2f1c4 100644 --- a/src/storm/storage/jani/Property.cpp +++ b/src/storm/storage/jani/Property.cpp @@ -7,19 +7,18 @@ namespace storm { return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << *fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'"; } - Property::Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::string const& comment) - : name(name), comment(comment), filterExpression(FilterExpression(formula)), undefinedConstants(undefinedConstants) { + Property::Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::shared_ptr const& shieldingExpression, std::string const& comment) + : name(name), comment(comment), filterExpression(FilterExpression(formula)), undefinedConstants(undefinedConstants), shieldingExpression(shieldingExpression) { + std::cout << "In Property ctor: " << *(this->shieldingExpression.get()) << std::endl; + std::cout << "In Property ctor: " << *(shieldingExpression.get()) << std::endl; // Intentionally left empty. } - Property::Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::string const& comment) - : name(name), comment(comment), filterExpression(fe), undefinedConstants(undefinedConstants) { - // Intentionally left empty. - } - - Property::Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, storm::logic::ShieldExpression shieldExpression, std::string const& comment) - : name(name), comment(comment), filterExpression(FilterExpression(formula)), undefinedConstants(undefinedConstants), shieldingExpression(shieldingExpression) { + Property::Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::shared_ptr const& shieldingExpression, std::string const& comment) + : name(name), comment(comment), filterExpression(fe), undefinedConstants(undefinedConstants), shieldingExpression(shieldingExpression) { // Intentionally left empty. + std::cout << "In Property ctor with filterExpression: " << *(this->shieldingExpression.get()) << std::endl; + std::cout << "In Property ctor with filterExpression: " << *(shieldingExpression.get()) << std::endl; } std::string const& Property::getName() const { @@ -60,7 +59,7 @@ namespace storm { remainingUndefinedConstants.insert(constant); } } - return Property(name, filterExpression.substitute(substitution), remainingUndefinedConstants, comment); + return Property(name, filterExpression.substitute(substitution), remainingUndefinedConstants, getShieldingExpression(), comment); } Property Property::substitute(std::function const& substitutionFunction) const { @@ -68,19 +67,19 @@ namespace storm { for (auto const& constant : undefinedConstants) { substitutionFunction(constant.getExpression()).getBaseExpression().gatherVariables(remainingUndefinedConstants); } - return Property(name, filterExpression.substitute(substitutionFunction), remainingUndefinedConstants, comment); + return Property(name, filterExpression.substitute(substitutionFunction), remainingUndefinedConstants, getShieldingExpression(), comment); } Property Property::substituteLabels(std::map const& substitution) const { - return Property(name, filterExpression.substituteLabels(substitution), undefinedConstants, comment); + return Property(name, filterExpression.substituteLabels(substitution), undefinedConstants, getShieldingExpression(), comment); } Property Property::substituteRewardModelNames(std::map const& rewardModelNameSubstitution) const { - return Property(name, filterExpression.substituteRewardModelNames(rewardModelNameSubstitution), undefinedConstants, comment); + return Property(name, filterExpression.substituteRewardModelNames(rewardModelNameSubstitution), undefinedConstants, getShieldingExpression(), comment); } Property Property::clone() const { - return Property(name, filterExpression.clone(), undefinedConstants, comment); + return Property(name, filterExpression.clone(), undefinedConstants, getShieldingExpression(), comment); } FilterExpression const& Property::getFilter() const { @@ -95,6 +94,12 @@ namespace storm { return shieldingExpression.is_initialized(); } + std::shared_ptr Property::getShieldingExpression() const { + //STORM_LOG_ASSERT(isShieldingProperty(), "This property does not have an associated shielding expression."); + if(!isShieldingProperty()) return nullptr; + return shieldingExpression.get(); + } + std::set const& Property::getUndefinedConstants() const { return undefinedConstants; } diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index 91bb9a22a..d2b4ec32e 100644 --- a/src/storm/storage/jani/Property.h +++ b/src/storm/storage/jani/Property.h @@ -102,26 +102,19 @@ namespace storm { * @param name the name * @param formula the formula representation * @param undefinedConstants the undefined constants used in the property + * @param shieldingExpression An optional expression for a shield to be created * @param comment An optional comment */ - Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::string const& comment = ""); + Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, std::shared_ptr const& shieldExpression = nullptr, std::string const& comment = ""); /** * Constructs the property * @param name the name * @param formula the formula representation + * @param shieldingExpression An optional expression for a shield to be created * @param comment An optional comment */ - Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::string const& comment = ""); - - /** - * Constructs the property - * @param name the name - * @param formula the formula representation - * @param shieldExpression the shielding expression - * @param comment An optional comment - */ - Property(std::string const& name, std::shared_ptr const& formula, std::set const& undefinedConstants, storm::logic::ShieldExpression shieldExpression, std::string const& comment = ""); + Property(std::string const& name, FilterExpression const& fe, std::set const& undefinedConstants, std::shared_ptr const& shieldExpression = nullptr, std::string const& comment = ""); /** * Get the provided name @@ -154,6 +147,7 @@ namespace storm { std::shared_ptr getRawFormula() const; bool isShieldingProperty() const; + std::shared_ptr getShieldingExpression() const; private: std::string name; @@ -162,7 +156,7 @@ namespace storm { std::set undefinedConstants; // TODO might need refactoring, this cannot be expressed by JANI yet, so this is totally wrong here. - boost::optional shieldingExpression; + boost::optional> shieldingExpression; };