sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Jani Props may now hold info about shielding query

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
00479b4877
commit
d4d3c0d9ea
6 changed files with 98 additions and 99 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 21
      src/storm-parsers/parser/FormulaParser.cpp
  2. 90
      src/storm-parsers/parser/JaniParser.cpp
  3. 11
      src/storm/api/properties.cpp
  4. 24
      src/storm/logic/RewardAccumulationEliminationVisitor.cpp
  5. 33
      src/storm/storage/jani/Property.cpp
  6. 18
      src/storm/storage/jani/Property.h

21
src/storm-parsers/parser/FormulaParser.cpp
View File

@ -18,7 +18,7 @@
namespace storm { namespace storm {
namespace parser { namespace parser {
FormulaParser::FormulaParser() : manager(new storm::expressions::ExpressionManager()), grammar(new FormulaParserGrammar(manager)) { FormulaParser::FormulaParser() : manager(new storm::expressions::ExpressionManager()), grammar(new FormulaParserGrammar(manager)) {
// Intentionally left empty. // Intentionally left empty.
} }
@ -40,25 +40,25 @@ namespace storm {
FormulaParser::FormulaParser(FormulaParser const& other) : FormulaParser(other.manager) { 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); }); other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); });
} }
FormulaParser& FormulaParser::operator=(FormulaParser const& other) { FormulaParser& FormulaParser::operator=(FormulaParser const& other) {
this->manager = other.manager; this->manager = other.manager;
this->grammar = std::shared_ptr<FormulaParserGrammar>(new FormulaParserGrammar(this->manager)); this->grammar = std::shared_ptr<FormulaParserGrammar>(new FormulaParserGrammar(this->manager));
other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); }); other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); });
return *this; return *this;
} }
std::shared_ptr<storm::logic::Formula const> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const { std::shared_ptr<storm::logic::Formula const> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const {
std::vector<storm::jani::Property> property = parseFromString(formulaString); std::vector<storm::jani::Property> property = parseFromString(formulaString);
STORM_LOG_THROW(property.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << property.size() << " instead."); STORM_LOG_THROW(property.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << property.size() << " instead.");
return property.front().getRawFormula(); return property.front().getRawFormula();
} }
std::vector<storm::jani::Property> FormulaParser::parseFromFile(std::string const& filename) const { std::vector<storm::jani::Property> FormulaParser::parseFromFile(std::string const& filename) const {
// Open file and initialize result. // Open file and initialize result.
std::ifstream inputFileStream; std::ifstream inputFileStream;
storm::utility::openFile(filename, inputFileStream); storm::utility::openFile(filename, inputFileStream);
std::vector<storm::jani::Property> properties; std::vector<storm::jani::Property> properties;
// Now try to parse the contents of the file. // Now try to parse the contents of the file.
@ -75,15 +75,15 @@ namespace storm {
storm::utility::closeFile(inputFileStream); storm::utility::closeFile(inputFileStream);
return properties; return properties;
} }
std::vector<storm::jani::Property> FormulaParser::parseFromString(std::string const& formulaString) const { std::vector<storm::jani::Property> FormulaParser::parseFromString(std::string const& formulaString) const {
PositionIteratorType first(formulaString.begin()); PositionIteratorType first(formulaString.begin());
PositionIteratorType iter = first; PositionIteratorType iter = first;
PositionIteratorType last(formulaString.end()); PositionIteratorType last(formulaString.end());
// Create empty result; // Create empty result;
std::vector<storm::jani::Property> result; std::vector<storm::jani::Property> result;
// Create grammar. // Create grammar.
try { try {
// Start parsing. // Start parsing.
@ -93,15 +93,14 @@ namespace storm {
} catch (qi::expectation_failure<PositionIteratorType> const& e) { } catch (qi::expectation_failure<PositionIteratorType> const& e) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_); STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_);
} }
return result; return result;
} }
void FormulaParser::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { void FormulaParser::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
// Record the mapping and hand it over to the grammar. // Record the mapping and hand it over to the grammar.
this->identifiers_.add(identifier, expression); this->identifiers_.add(identifier, expression);
grammar->addIdentifierExpression(identifier, expression); grammar->addIdentifierExpression(identifier, expression);
} }
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

90
src/storm-parsers/parser/JaniParser.cpp
View File

@ -139,9 +139,9 @@ namespace storm {
if (actionCount > 0) { if (actionCount > 0) {
parseActions(parsedStructure.at("actions"), model); parseActions(parsedStructure.at("actions"), model);
} }
Scope scope(name); Scope scope(name);
// Parse constants // Parse constants
ConstantsMap constants; ConstantsMap constants;
scope.constants = &constants; scope.constants = &constants;
@ -157,7 +157,7 @@ namespace storm {
constants.emplace(constant->getName(), &model.getConstants().back()); constants.emplace(constant->getName(), &model.getConstants().back());
} }
} }
// Parse variables // Parse variables
size_t variablesCount = parsedStructure.count("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."); 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)); globalVars.emplace(variable->getName(), &model.addVariable(*variable));
} }
} }
uint64_t funDeclCount = parsedStructure.count("functions"); uint64_t funDeclCount = parsedStructure.count("functions");
STORM_LOG_THROW(funDeclCount < 2, storm::exceptions::InvalidJaniException, "Model '" << name << "' has more than one list of functions"); STORM_LOG_THROW(funDeclCount < 2, storm::exceptions::InvalidJaniException, "Model '" << name << "' has more than one list of functions");
FunctionsMap globalFuns; FunctionsMap globalFuns;
@ -196,7 +196,7 @@ namespace storm {
globalFuns[funDef.getName()] = &model.addFunctionDefinition(funDef); globalFuns[funDef.getName()] = &model.addFunctionDefinition(funDef);
} }
} }
// Parse Automata // Parse Automata
STORM_LOG_THROW(parsedStructure.count("automata") == 1, storm::exceptions::InvalidJaniException, "Exactly one list of automata must be given"); 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"); 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<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system")); std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system"));
model.setSystemComposition(composition); model.setSystemComposition(composition);
model.finalize(); model.finalize();
// Parse properties // Parse properties
storm::logic::RewardAccumulationEliminationVisitor rewAccEliminator(model); storm::logic::RewardAccumulationEliminationVisitor rewAccEliminator(model);
STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given"); 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); 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)) }; return { parseFormula(model, propertyStructure.at("exp"), formulaContext, scope.refine("Operand of operator " + opstring)) };
} }
template <typename ValueType> template <typename ValueType>
std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser<ValueType>::parseBinaryFormulaArguments(storm::jani::Model& model, Json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) { std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser<ValueType>::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("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); 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)) }; 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 <typename ValueType> template <typename ValueType>
storm::jani::PropertyInterval JaniParser<ValueType>::parsePropertyInterval(Json const& piStructure, Scope const& scope) { storm::jani::PropertyInterval JaniParser<ValueType>::parsePropertyInterval(Json const& piStructure, Scope const& scope) {
storm::jani::PropertyInterval pi; storm::jani::PropertyInterval pi;
@ -260,11 +260,11 @@ namespace storm {
if (piStructure.count("lower-exclusive") > 0) { 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"); 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"); pi.lowerBoundStrict = piStructure.at("lower-exclusive");
} }
if (piStructure.count("upper") > 0) { if (piStructure.count("upper") > 0) {
pi.upperBound = parseExpression(piStructure.at("upper"), scope.refine("Upper bound for property interval")); pi.upperBound = parseExpression(piStructure.at("upper"), scope.refine("Upper bound for property interval"));
} }
if (piStructure.count("upper-exclusive") > 0) { 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"); 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); return storm::logic::RewardAccumulation(accSteps, accTime, accExit);
} }
void insertLowerUpperTimeBounds(std::vector<boost::optional<storm::logic::TimeBound>>& lowerBounds, std::vector<boost::optional<storm::logic::TimeBound>>& upperBounds, storm::jani::PropertyInterval const& pi) { void insertLowerUpperTimeBounds(std::vector<boost::optional<storm::logic::TimeBound>>& lowerBounds, std::vector<boost::optional<storm::logic::TimeBound>>& upperBounds, storm::jani::PropertyInterval const& pi) {
if (pi.hasLowerBound()) { if (pi.hasLowerBound()) {
lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound));
@ -334,7 +334,7 @@ namespace storm {
} }
if (propertyStructure.count("op") == 1) { if (propertyStructure.count("op") == 1) {
std::string opString = getString<ValueType>(propertyStructure.at("op"), "Operation description"); std::string opString = getString<ValueType>(propertyStructure.at("op"), "Operation description");
if(opString == "Pmin" || opString == "Pmax") { if(opString == "Pmin" || opString == "Pmax") {
std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(model, propertyStructure, storm::logic::FormulaContext::Probability, opString, scope); std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(model, propertyStructure, storm::logic::FormulaContext::Probability, opString, scope);
assert(args.size() == 1); assert(args.size() == 1);
@ -342,7 +342,7 @@ namespace storm {
opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
opInfo.bound = bound; opInfo.bound = bound;
return std::make_shared<storm::logic::ProbabilityOperatorFormula>(args[0], opInfo); return std::make_shared<storm::logic::ProbabilityOperatorFormula>(args[0], opInfo);
} else if (opString == "∀" || opString == "∃") { } else if (opString == "∀" || opString == "∃") {
assert(bound == boost::none); assert(bound == boost::none);
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported in " << scope.description); 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::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); STORM_LOG_THROW(rewExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << rewExpr << "' does not have numerical type in " << scope.description);
std::string rewardName = rewExpr.toString(); std::string rewardName = rewExpr.toString();
storm::logic::OperatorInformation opInfo; storm::logic::OperatorInformation opInfo;
opInfo.optimalityType = opString == "Emin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.optimalityType = opString == "Emin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
opInfo.bound = bound; opInfo.bound = bound;
@ -361,7 +361,7 @@ namespace storm {
if (propertyStructure.count("accumulate") > 0) { if (propertyStructure.count("accumulate") > 0) {
rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), scope.description); rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), scope.description);
} }
bool time = false; bool time = false;
if (propertyStructure.count("step-instant") > 0) { 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); 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<storm::logic::LongRunAverageRewardFormula>(rewardAccumulation); auto subformula = std::make_shared<storm::logic::LongRunAverageRewardFormula>(rewardAccumulation);
return std::make_shared<storm::logic::RewardOperatorFormula>(subformula, rewardName, opInfo); return std::make_shared<storm::logic::RewardOperatorFormula>(subformula, rewardName, opInfo);
} else if (opString == "U" || opString == "F") { } else if (opString == "U" || opString == "F") {
assert(bound == boost::none); assert(bound == boost::none);
std::vector<std::shared_ptr<storm::logic::Formula const>> args; std::vector<std::shared_ptr<storm::logic::Formula const>> args;
@ -467,7 +467,7 @@ namespace storm {
args.push_back(args[0]); args.push_back(args[0]);
args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula(); args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula();
} }
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds; std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
std::vector<storm::logic::TimeBoundReference> tbReferences; std::vector<storm::logic::TimeBoundReference> tbReferences;
if (propertyStructure.count("step-bounds") > 0) { if (propertyStructure.count("step-bounds") > 0) {
@ -557,7 +557,7 @@ namespace storm {
} else if (opString == ">") { } else if (opString == ">") {
ct = storm::logic::ComparisonType::Greater; ct = storm::logic::ComparisonType::Greater;
} }
std::vector<std::string> const leftRight = {"left", "right"}; std::vector<std::string> const leftRight = {"left", "right"};
for (uint64_t i = 0; i < 2; ++i) { for (uint64_t i = 0; i < 2; ++i) {
if (propertyStructure.at(leftRight[i]).count("op") > 0) { 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"); STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Looking for operator for formula " << propertyStructure.dump() << ", but did not find one");
} }
} }
template <typename ValueType> template <typename ValueType>
storm::jani::Property JaniParser<ValueType>::parseProperty(storm::jani::Model& model, Json const& propertyStructure, Scope const& scope) { storm::jani::Property JaniParser<ValueType>::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"); 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"); STORM_LOG_THROW(propertyStructure.count("expression") == 1, storm::exceptions::InvalidJaniException, "Property must have an expression");
// Parse filter expression. // Parse filter expression.
Json const& expressionStructure = propertyStructure.at("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.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.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"); STORM_LOG_THROW(expressionStructure.count("fun") == 1, storm::exceptions::InvalidJaniException, "Filter must have a function descritpion");
@ -641,7 +641,7 @@ namespace storm {
} else { } else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown filter description " << funDescr << " in property named " << name); 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"); STORM_LOG_THROW(expressionStructure.count("states") == 1, storm::exceptions::InvalidJaniException, "Filter must have a states description");
std::shared_ptr<storm::logic::Formula const> statesFormula; std::shared_ptr<storm::logic::Formula const> statesFormula;
if (expressionStructure.at("states").count("op") > 0) { 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(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"); 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)); 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 <typename ValueType> template <typename ValueType>
@ -681,11 +681,11 @@ namespace storm {
definingExpression = parseExpression(constantStructure.at("value"), scope.refine("Value of constant " + name)); definingExpression = parseExpression(constantStructure.at("value"), scope.refine("Value of constant " + name));
assert(definingExpression.isInitialized()); assert(definingExpression.isInitialized());
} }
STORM_LOG_THROW(constantStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") must have a (single) type-declaration."); STORM_LOG_THROW(constantStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") must have a (single) type-declaration.");
ParsedType type; ParsedType type;
parseType(type, constantStructure.at("type"), name, scope); 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_LOG_THROW(type.basicType.is_initialized(), storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") has unexpected type");
storm::expressions::Variable var; storm::expressions::Variable var;
switch (type.basicType.get()) { switch (type.basicType.get()) {
@ -710,10 +710,10 @@ namespace storm {
constraintExpression = var.getExpression() <= type.bounds->second; constraintExpression = var.getExpression() <= type.bounds->second;
} }
} }
return std::make_shared<storm::jani::Constant>(name, std::move(var), definingExpression, constraintExpression); return std::make_shared<storm::jani::Constant>(name, std::move(var), definingExpression, constraintExpression);
} }
template <typename ValueType> template <typename ValueType>
void JaniParser<ValueType>::parseType(ParsedType& result, Json const& typeStructure, std::string variableName, Scope const& scope) { void JaniParser<ValueType>::parseType(ParsedType& result, Json const& typeStructure, std::string variableName, Scope const& scope) {
if (typeStructure.is_string()) { if (typeStructure.is_string()) {
@ -779,7 +779,7 @@ namespace storm {
} }
} }
} }
template <typename ValueType> template <typename ValueType>
storm::jani::FunctionDefinition JaniParser<ValueType>::parseFunctionDefinition(Json const& functionDefinitionStructure, Scope const& scope, bool firstPass, std::string const& parameterNamePrefix) { storm::jani::FunctionDefinition JaniParser<ValueType>::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"); 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."); STORM_LOG_THROW(functionDefinitionStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Function definition '" + functionName + "' (scope: " + scope.description + ") must have a (single) type-declaration.");
ParsedType type; ParsedType type;
parseType(type, functionDefinitionStructure.at("type"), functionName, scope); parseType(type, functionDefinitionStructure.at("type"), functionName, scope);
std::unordered_map<std::string, storm::expressions::Variable> parameterNameToVariableMap; std::unordered_map<std::string, storm::expressions::Variable> parameterNameToVariableMap;
std::vector<storm::expressions::Variable> parameters; std::vector<storm::expressions::Variable> parameters;
if (!firstPass && functionDefinitionStructure.count("parameters") > 0) { 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."); 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)); 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."); 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; std::string exprParameterName = parameterNamePrefix + functionName + VARIABLE_AUTOMATON_DELIMITER + parameterName;
parameters.push_back(expressionManager->declareVariable(exprParameterName, parameterType.expressionType)); parameters.push_back(expressionManager->declareVariable(exprParameterName, parameterType.expressionType));
parameterNameToVariableMap.emplace(parameterName, parameters.back()); 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_LOG_THROW(functionDefinitionStructure.count("body") == 1, storm::exceptions::InvalidJaniException, "Function definition '" + functionName + "' (scope: " + scope.description + ") must have a (single) body.");
storm::expressions::Expression functionBody; storm::expressions::Expression functionBody;
if (!firstPass) { if (!firstPass) {
@ -815,7 +815,7 @@ namespace storm {
return storm::jani::FunctionDefinition(functionName, type.expressionType, parameters, functionBody); return storm::jani::FunctionDefinition(functionName, type.expressionType, parameters, functionBody);
} }
template <typename ValueType> template <typename ValueType>
std::shared_ptr<storm::jani::Variable> JaniParser<ValueType>::parseVariable(Json const& variableStructure, bool requireInitialValues, Scope const& scope, std::string const& namePrefix) { std::shared_ptr<storm::jani::Variable> JaniParser<ValueType>::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"); 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 { } else {
assert(!transientVar); assert(!transientVar);
} }
bool setInitValFromDefault = !initVal.is_initialized() && requireInitialValues; bool setInitValFromDefault = !initVal.is_initialized() && requireInitialValues;
if (type.basicType) { if (type.basicType) {
switch (type.basicType.get()) { switch (type.basicType.get()) {
@ -945,7 +945,7 @@ namespace storm {
} }
return result; return result;
} }
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scope.description << ")."); 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) { 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 << "."); 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. * Helper for parse expression.
*/ */
@ -1411,7 +1411,7 @@ namespace storm {
localFuns[funDef.getName()] = &automaton.addFunctionDefinition(funDef); localFuns[funDef.getName()] = &automaton.addFunctionDefinition(funDef);
} }
} }
STORM_LOG_THROW(automatonStructure.count("locations") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' does not have locations."); STORM_LOG_THROW(automatonStructure.count("locations") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' does not have locations.");
std::unordered_map<std::string, uint64_t> locIds; std::unordered_map<std::string, uint64_t> locIds;
for(auto const& locEntry : automatonStructure.at("locations")) { for(auto const& locEntry : automatonStructure.at("locations")) {
@ -1500,7 +1500,7 @@ namespace storm {
templateEdge->getAssignments().add(storm::jani::Assignment(lValue, assignmentExpr, assignmentIndex)); templateEdge->getAssignments().add(storm::jani::Assignment(lValue, assignmentExpr, assignmentIndex));
} }
} }
// destinations // 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 << "'"); 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<std::pair<uint64_t, storm::expressions::Expression>> destinationLocationsAndProbabilities; std::vector<std::pair<uint64_t, storm::expressions::Expression>> destinationLocationsAndProbabilities;
@ -1550,7 +1550,7 @@ namespace storm {
return automaton; return automaton;
} }
template <typename ValueType> template <typename ValueType>
std::vector<storm::jani::SynchronizationVector> parseSyncVectors(typename JaniParser<ValueType>::Json const& syncVectorStructure) { std::vector<storm::jani::SynchronizationVector> parseSyncVectors(typename JaniParser<ValueType>::Json const& syncVectorStructure) {
std::vector<storm::jani::SynchronizationVector> syncVectors; std::vector<storm::jani::SynchronizationVector> syncVectors;
@ -1586,9 +1586,9 @@ namespace storm {
} }
return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(compositionStructure.at("automaton").template get<std::string>(), inputEnabledActions)); return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(compositionStructure.at("automaton").template get<std::string>(), inputEnabledActions));
} }
STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given, got " << compositionStructure.dump()); 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) { if (compositionStructure.at("elements").size() == 1 && compositionStructure.count("syncs") == 0) {
// We might have an automaton. // We might have an automaton.
STORM_LOG_THROW(compositionStructure.at("elements").back().count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in composition"); 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<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(name)); return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(name));
} }
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Trivial nesting parallel composition is not yet supported"); STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Trivial nesting parallel composition is not yet supported");
} }
std::vector<std::shared_ptr<storm::jani::Composition>> compositions; std::vector<std::shared_ptr<storm::jani::Composition>> compositions;
for (auto const& elemDecl : compositionStructure.at("elements")) { for (auto const& elemDecl : compositionStructure.at("elements")) {
if(!allowRecursion) { if(!allowRecursion) {
@ -1608,17 +1608,17 @@ namespace storm {
} }
compositions.push_back(parseComposition(elemDecl)); compositions.push_back(parseComposition(elemDecl));
} }
STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once"); STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once");
std::vector<storm::jani::SynchronizationVector> syncVectors; std::vector<storm::jani::SynchronizationVector> syncVectors;
if (compositionStructure.count("syncs") > 0) { if (compositionStructure.count("syncs") > 0) {
syncVectors = parseSyncVectors<ValueType>(compositionStructure.at("syncs")); syncVectors = parseSyncVectors<ValueType>(compositionStructure.at("syncs"));
} }
return std::shared_ptr<storm::jani::Composition>(new storm::jani::ParallelComposition(compositions, syncVectors)); return std::shared_ptr<storm::jani::Composition>(new storm::jani::ParallelComposition(compositions, syncVectors));
} }
template class JaniParser<double>; template class JaniParser<double>;
template class JaniParser<storm::RationalNumber>; template class JaniParser<storm::RationalNumber>;
} }

11
src/storm/api/properties.cpp
View File

@ -37,19 +37,19 @@ namespace storm {
reducedPropertyNames.insert(property.getName()); reducedPropertyNames.insert(property.getName());
} }
} }
if (reducedPropertyNames.size() < propertyNameSet.size()) { if (reducedPropertyNames.size() < propertyNameSet.size()) {
std::set<std::string> missingProperties; std::set<std::string> missingProperties;
std::set_difference(propertyNameSet.begin(), propertyNameSet.end(), reducedPropertyNames.begin(), reducedPropertyNames.end(), std::inserter(missingProperties, missingProperties.begin())); 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, ", ") << "."); STORM_LOG_WARN("Filtering unknown properties " << boost::join(missingProperties, ", ") << ".");
} }
return result; return result;
} else { } else {
return properties; return properties;
} }
} }
std::vector<std::shared_ptr<storm::logic::Formula const>> extractFormulasFromProperties(std::vector<storm::jani::Property> const& properties) { std::vector<std::shared_ptr<storm::logic::Formula const>> extractFormulasFromProperties(std::vector<storm::jani::Property> const& properties) {
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas; std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
for (auto const& prop : properties) { for (auto const& prop : properties) {
@ -57,7 +57,7 @@ namespace storm {
} }
return formulas; return formulas;
} }
storm::jani::Property createMultiObjectiveProperty(std::vector<storm::jani::Property> const& properties) { storm::jani::Property createMultiObjectiveProperty(std::vector<storm::jani::Property> const& properties) {
std::set<storm::expressions::Variable> undefConstants; std::set<storm::expressions::Variable> undefConstants;
std::string name = ""; std::string name = "";
@ -67,9 +67,10 @@ namespace storm {
name += prop.getName(); name += prop.getName();
comment += prop.getComment(); 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.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<storm::logic::MultiObjectiveFormula>(extractFormulasFromProperties(properties)); auto multiFormula = std::make_shared<storm::logic::MultiObjectiveFormula>(extractFormulasFromProperties(properties));
return storm::jani::Property(name, multiFormula, undefConstants, comment);
return storm::jani::Property(name, multiFormula, undefConstants, nullptr, comment);
} }
} }
} }

24
src/storm/logic/RewardAccumulationEliminationVisitor.cpp
View File

@ -15,25 +15,25 @@ namespace storm {
RewardAccumulationEliminationVisitor::RewardAccumulationEliminationVisitor(storm::jani::Model const& model) : model(model) { RewardAccumulationEliminationVisitor::RewardAccumulationEliminationVisitor(storm::jani::Model const& model) : model(model) {
// Intentionally left empty // Intentionally left empty
} }
std::shared_ptr<Formula> RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const { std::shared_ptr<Formula> RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const {
boost::any result = f.accept(*this, boost::any()); boost::any result = f.accept(*this, boost::any());
return boost::any_cast<std::shared_ptr<Formula>>(result); return boost::any_cast<std::shared_ptr<Formula>>(result);
} }
void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(std::vector<storm::jani::Property>& properties) const { void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(std::vector<storm::jani::Property>& properties) const {
for (auto& p : properties) { for (auto& p : properties) {
eliminateRewardAccumulations(p); eliminateRewardAccumulations(p);
} }
} }
void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(storm::jani::Property& property) const { void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(storm::jani::Property& property) const {
auto formula = eliminateRewardAccumulations(*property.getFilter().getFormula()); auto formula = eliminateRewardAccumulations(*property.getFilter().getFormula());
auto states = eliminateRewardAccumulations(*property.getFilter().getStatesFormula()); auto states = eliminateRewardAccumulations(*property.getFilter().getStatesFormula());
storm::jani::FilterExpression fe(formula, property.getFilter().getFilterType(), states); 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 { boost::any RewardAccumulationEliminationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds; std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
std::vector<TimeBoundReference> timeBoundReferences; std::vector<TimeBoundReference> timeBoundReferences;
@ -68,7 +68,7 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences)); return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
} }
} }
boost::any RewardAccumulationEliminationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { boost::any RewardAccumulationEliminationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
boost::optional<storm::logic::RewardAccumulation> rewAcc; boost::optional<storm::logic::RewardAccumulation> rewAcc;
STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); 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<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, rewAcc)); return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, rewAcc));
} }
boost::any RewardAccumulationEliminationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const { 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."); 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<boost::optional<std::string>>(data); auto rewName = boost::any_cast<boost::optional<std::string>>(data);
@ -100,7 +100,7 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageRewardFormula>(f.getRewardAccumulation())); return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageRewardFormula>(f.getRewardAccumulation()));
} }
} }
boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data)); std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
if (f.hasRewardAccumulation()) { if (f.hasRewardAccumulation()) {
@ -120,12 +120,12 @@ namespace storm {
} }
return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext())); return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext()));
} }
boost::any RewardAccumulationEliminationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { boost::any RewardAccumulationEliminationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, f.getOptionalRewardModelName())); std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, f.getOptionalRewardModelName()));
return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation()));
} }
boost::any RewardAccumulationEliminationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { 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."); 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<boost::optional<std::string>>(data); auto rewName = boost::any_cast<boost::optional<std::string>>(data);
@ -135,11 +135,11 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f.getRewardAccumulation())); return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f.getRewardAccumulation()));
} }
} }
bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const { bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const {
STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable for unique reward model."); 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()); storm::jani::RewardModelInformation info(model, rewardModelName.get());
if ((info.hasActionRewards() || info.hasTransitionRewards()) && !accumulation.isStepsSet()) { if ((info.hasActionRewards() || info.hasTransitionRewards()) && !accumulation.isStepsSet()) {
return false; return false;
} }

33
src/storm/storage/jani/Property.cpp
View File

@ -7,19 +7,18 @@ namespace storm {
return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << *fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'"; 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<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> const& undefinedConstants, std::string const& comment)
: name(name), comment(comment), filterExpression(FilterExpression(formula)), undefinedConstants(undefinedConstants) {
Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> const& undefinedConstants, std::shared_ptr<storm::logic::ShieldExpression const> 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. // Intentionally left empty.
} }
Property::Property(std::string const& name, FilterExpression const& fe, std::set<storm::expressions::Variable> 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<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> 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<storm::expressions::Variable> const& undefinedConstants, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression, std::string const& comment)
: name(name), comment(comment), filterExpression(fe), undefinedConstants(undefinedConstants), shieldingExpression(shieldingExpression) {
// Intentionally left empty. // 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 { std::string const& Property::getName() const {
@ -60,7 +59,7 @@ namespace storm {
remainingUndefinedConstants.insert(constant); 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<storm::expressions::Expression(storm::expressions::Expression const&)> const& substitutionFunction) const { Property Property::substitute(std::function<storm::expressions::Expression(storm::expressions::Expression const&)> const& substitutionFunction) const {
@ -68,19 +67,19 @@ namespace storm {
for (auto const& constant : undefinedConstants) { for (auto const& constant : undefinedConstants) {
substitutionFunction(constant.getExpression()).getBaseExpression().gatherVariables(remainingUndefinedConstants); 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<std::string, std::string> const& substitution) const { Property Property::substituteLabels(std::map<std::string, std::string> 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<std::string, std::string> const& rewardModelNameSubstitution) const { Property Property::substituteRewardModelNames(std::map<std::string, std::string> const& rewardModelNameSubstitution) const {
return Property(name, filterExpression.substituteRewardModelNames(rewardModelNameSubstitution), undefinedConstants, comment);
return Property(name, filterExpression.substituteRewardModelNames(rewardModelNameSubstitution), undefinedConstants, getShieldingExpression(), comment);
} }
Property Property::clone() const { Property Property::clone() const {
return Property(name, filterExpression.clone(), undefinedConstants, comment);
return Property(name, filterExpression.clone(), undefinedConstants, getShieldingExpression(), comment);
} }
FilterExpression const& Property::getFilter() const { FilterExpression const& Property::getFilter() const {
@ -95,6 +94,12 @@ namespace storm {
return shieldingExpression.is_initialized(); return shieldingExpression.is_initialized();
} }
std::shared_ptr<storm::logic::ShieldExpression const> 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<storm::expressions::Variable> const& Property::getUndefinedConstants() const { std::set<storm::expressions::Variable> const& Property::getUndefinedConstants() const {
return undefinedConstants; return undefinedConstants;
} }

18
src/storm/storage/jani/Property.h
View File

@ -102,26 +102,19 @@ namespace storm {
* @param name the name * @param name the name
* @param formula the formula representation * @param formula the formula representation
* @param undefinedConstants the undefined constants used in the property * @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 * @param comment An optional comment
*/ */
Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> const& undefinedConstants, std::string const& comment = "");
Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> const& undefinedConstants, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldExpression = nullptr, std::string const& comment = "");
/** /**
* Constructs the property * Constructs the property
* @param name the name * @param name the name
* @param formula the formula representation * @param formula the formula representation
* @param shieldingExpression An optional expression for a shield to be created
* @param comment An optional comment * @param comment An optional comment
*/ */
Property(std::string const& name, FilterExpression const& fe, std::set<storm::expressions::Variable> 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<storm::logic::Formula const> const& formula, std::set<storm::expressions::Variable> const& undefinedConstants, storm::logic::ShieldExpression shieldExpression, std::string const& comment = "");
Property(std::string const& name, FilterExpression const& fe, std::set<storm::expressions::Variable> const& undefinedConstants, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldExpression = nullptr, std::string const& comment = "");
/** /**
* Get the provided name * Get the provided name
@ -154,6 +147,7 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> getRawFormula() const; std::shared_ptr<storm::logic::Formula const> getRawFormula() const;
bool isShieldingProperty() const; bool isShieldingProperty() const;
std::shared_ptr<storm::logic::ShieldExpression const> getShieldingExpression() const;
private: private:
std::string name; std::string name;
@ -162,7 +156,7 @@ namespace storm {
std::set<storm::expressions::Variable> undefinedConstants; std::set<storm::expressions::Variable> undefinedConstants;
// TODO might need refactoring, this cannot be expressed by JANI yet, so this is totally wrong here. // TODO might need refactoring, this cannot be expressed by JANI yet, so this is totally wrong here.
boost::optional<storm::logic::ShieldExpression> shieldingExpression;
boost::optional<std::shared_ptr<storm::logic::ShieldExpression const>> shieldingExpression;
}; };

Write Preview
Loading…
Cancel
Save