diff --git a/CHANGELOG.md b/CHANGELOG.md
index 21ad6718a..7dd207331 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,15 @@ The releases of major and minor versions contain an overview of changes since th
Version 1.2.x
-------------
+### Version 1.2.4 (2018/08)
+- New binary `storm-conv` that handles conversions between model files (currently: prism to jani)
+- Added support for expected time properties for discrete time models
+- Several bug fixes related to jani
+- `storm-gspn`: Improved .pnpro parser
+- `storm-gspn`: Added support for single/infinite/k-server semantics for GSPNs given in the .pnpro format
+- `storm-gspn`: Added option to set a global capacity for all places
+- `storm-gspn`: Added option to include a set of standard properties when converting GSPNs to jani
+
### Version 1.2.3 (2018/07)
- Fix in version parsing
diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index f60a3ffb5..524d772be 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -18,6 +18,7 @@
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/storage/jani/Property.h"
+#include "storm/logic/RewardAccumulationEliminationVisitor.h"
#include "storm/models/ModelBase.h"
@@ -124,6 +125,10 @@ namespace storm {
}
if (!output.properties.empty()) {
output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions);
+ if (output.model.is_initialized() && output.model->isJaniModel()) {
+ storm::logic::RewardAccumulationEliminationVisitor v(output.model->asJaniModel());
+ v.eliminateRewardAccumulations(output.properties);
+ }
}
// Check whether conversion for PRISM to JANI is requested or necessary.
diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp
index 294beea6b..a499fccf2 100644
--- a/src/storm-conv-cli/storm-conv.cpp
+++ b/src/storm-conv-cli/storm-conv.cpp
@@ -86,11 +86,11 @@ namespace storm {
auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options);
if (outputFilename != "") {
- storm::api::exportJaniToFile(janiModelProperties.first, janiModelProperties.second, outputFilename);
+ storm::api::exportJaniToFile(janiModelProperties.first, janiModelProperties.second, outputFilename, jani.isCompactJsonSet());
}
if (output.isStdOutOutputEnabled()) {
- storm::api::printJaniToStream(janiModelProperties.first, janiModelProperties.second, std::cout);
+ storm::api::printJaniToStream(janiModelProperties.first, janiModelProperties.second, std::cout, jani.isCompactJsonSet());
}
}
diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp
index a8d88a502..aa37dd191 100644
--- a/src/storm-conv/api/storm-conv.cpp
+++ b/src/storm-conv/api/storm-conv.cpp
@@ -58,12 +58,12 @@ namespace storm {
return res;
}
- void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename) {
- storm::jani::JsonExporter::toFile(model, properties, filename);
+ void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename, bool compact) {
+ storm::jani::JsonExporter::toFile(model, properties, filename, true, compact);
}
- void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream) {
- storm::jani::JsonExporter::toStream(model, properties, ostream);
+ void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream, bool compact) {
+ storm::jani::JsonExporter::toStream(model, properties, ostream, true, compact);
}
diff --git a/src/storm-conv/api/storm-conv.h b/src/storm-conv/api/storm-conv.h
index ec8a306df..42cbf804d 100644
--- a/src/storm-conv/api/storm-conv.h
+++ b/src/storm-conv/api/storm-conv.h
@@ -19,9 +19,9 @@ namespace storm {
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties = std::vector<storm::jani::Property>(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions());
- void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename);
+ void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename, bool compact = false);
- void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream);
+ void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream, bool compact = false);
}
diff --git a/src/storm-conv/settings/modules/JaniExportSettings.cpp b/src/storm-conv/settings/modules/JaniExportSettings.cpp
index 588bde61a..707e91dac 100644
--- a/src/storm-conv/settings/modules/JaniExportSettings.cpp
+++ b/src/storm-conv/settings/modules/JaniExportSettings.cpp
@@ -19,13 +19,15 @@ namespace storm {
const std::string JaniExportSettings::exportFlattenOptionName = "flatten";
const std::string JaniExportSettings::locationVariablesOptionName = "location-variables";
const std::string JaniExportSettings::globalVariablesOptionName = "globalvars";
+ const std::string JaniExportSettings::compactJsonOptionName = "compactjson";
JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) {
- this->addOption(storm::settings::OptionBuilder(moduleName, locationVariablesOptionName, true, "Variables to export in the location").addArgument(storm::settings::ArgumentBuilder::createStringArgument("variables", "A comma separated list with local variables.").setDefaultValueString("").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, locationVariablesOptionName, true, "Variables to export in the location").addArgument(storm::settings::ArgumentBuilder::createStringArgument("variables", "A comma separated list of automaton and local variable names seperated by a dot, e.g. A.x,B.y.").setDefaultValueString("").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, standardCompliantOptionName, false, "Export in standard compliant variant.").setShortName(standardCompliantOptionShortName).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, true, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build());
this->addOption(storm::settings::OptionBuilder(moduleName, globalVariablesOptionName, false, "If set, variables will preferably be made global, e.g., to guarantee the same variable order as in the input file.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, compactJsonOptionName, false, "If set, the size of the resulting jani file will be reduced at the cost of (human-)readability.").build());
}
bool JaniExportSettings::isExportAsStandardJaniSet() const {
@@ -59,6 +61,10 @@ namespace storm {
bool JaniExportSettings::isGlobalVarsSet() const {
return this->getOption(globalVariablesOptionName).getHasOptionBeenSet();
}
+
+ bool JaniExportSettings::isCompactJsonSet() const {
+ return this->getOption(compactJsonOptionName).getHasOptionBeenSet();
+ }
void JaniExportSettings::finalize() {
diff --git a/src/storm-conv/settings/modules/JaniExportSettings.h b/src/storm-conv/settings/modules/JaniExportSettings.h
index 90dc532f0..99e00ea9b 100644
--- a/src/storm-conv/settings/modules/JaniExportSettings.h
+++ b/src/storm-conv/settings/modules/JaniExportSettings.h
@@ -14,16 +14,6 @@ namespace storm {
*/
JaniExportSettings();
- /**
- * Retrievew whether the pgcl file option was set
- */
- bool isJaniFileSet() const;
-
- /**
- * Retrieves the pgcl file name
- */
- std::string getJaniFilename() const;
-
bool isExportAsStandardJaniSet() const;
bool isExportFlattenedSet() const;
@@ -31,6 +21,8 @@ namespace storm {
bool isLocationVariablesSet() const;
bool isGlobalVarsSet() const;
+
+ bool isCompactJsonSet() const;
std::vector<std::pair<std::string, std::string>> getLocationVariables() const;
@@ -40,13 +32,12 @@ namespace storm {
static const std::string moduleName;
private:
- static const std::string janiFileOptionName;
- static const std::string janiFileOptionShortName;
static const std::string standardCompliantOptionName;
static const std::string standardCompliantOptionShortName;
static const std::string exportFlattenOptionName;
static const std::string locationVariablesOptionName;
static const std::string globalVariablesOptionName;
+ static const std::string compactJsonOptionName;
};
}
diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp
index 6b9c5e2ee..9d6924297 100644
--- a/src/storm-gspn-cli/storm-gspn.cpp
+++ b/src/storm-gspn-cli/storm-gspn.cpp
@@ -5,9 +5,6 @@
#include "storm-gspn/builder/JaniGSPNBuilder.h"
#include "storm-gspn/api/storm-gspn.h"
-#include "storm/exceptions/BaseException.h"
-#include "storm/exceptions/WrongFormatException.h"
-
#include "storm/utility/macros.h"
#include "storm/utility/initialize.h"
@@ -57,25 +54,6 @@ void initializeSettings() {
}
-std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const& filename) {
- std::unordered_map<std::string, uint64_t> map;
-
- std::ifstream stream;
- storm::utility::openFile(filename, stream);
-
- std::string line;
- while ( std::getline(stream, line) ) {
- std::vector<std::string> strs;
- boost::split(strs, line, boost::is_any_of("\t "));
- STORM_LOG_THROW(strs.size() == 2, storm::exceptions::WrongFormatException, "Expect key value pairs");
- std::cout << std::stoll(strs[1]) << std::endl;
- map[strs[0]] = std::stoll(strs[1]);
- }
- storm::utility::closeFile(stream);
- return map;
-}
-
-
int main(const int argc, const char **argv) {
try {
storm::utility::setUp();
@@ -91,11 +69,17 @@ int main(const int argc, const char **argv) {
// parse gspn from file
if (!gspnSettings.isGspnFileSet()) {
- return -1;
+ // If no gspn file is given, nothing needs to be done.
+ return 0;
+ }
+
+ std::string constantDefinitionString = "";
+ if (gspnSettings.isConstantsSet()) {
+ constantDefinitionString = gspnSettings.getConstantDefinitionString();
}
auto parser = storm::parser::GspnParser();
- auto gspn = parser.parse(gspnSettings.getGspnFilename());
+ auto gspn = parser.parse(gspnSettings.getGspnFilename(), constantDefinitionString);
std::string formulaString = "";
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isPropertySet()) {
@@ -104,13 +88,14 @@ int main(const int argc, const char **argv) {
boost::optional<std::set<std::string>> propertyFilter;
storm::parser::FormulaParser formulaParser(gspn->getExpressionManager());
std::vector<storm::jani::Property> properties = storm::api::parseProperties(formulaParser, formulaString, propertyFilter);
-
+ properties = storm::api::substituteConstantsInProperties(properties, gspn->getConstantsSubstitution());
+
if (!gspn->isValid()) {
STORM_LOG_ERROR("The gspn is not valid.");
}
if(gspnSettings.isCapacitiesFileSet()) {
- auto capacities = parseCapacitiesList(gspnSettings.getCapacitiesFilename());
+ auto capacities = storm::api::parseCapacitiesList(gspnSettings.getCapacitiesFilename(), *gspn);
gspn->setCapacities(capacities);
} else if (gspnSettings.isCapacitySet()) {
uint64_t capacity = gspnSettings.getCapacity();
@@ -126,7 +111,6 @@ int main(const int argc, const char **argv) {
delete gspn;
return 0;
-//
// // construct ma
// auto builder = storm::builder::ExplicitGspnModelBuilder<>();
// auto ma = builder.translateGspn(gspn, formula);
diff --git a/src/storm-gspn/api/storm-gspn.cpp b/src/storm-gspn/api/storm-gspn.cpp
index b972b474c..63da78250 100644
--- a/src/storm-gspn/api/storm-gspn.cpp
+++ b/src/storm-gspn/api/storm-gspn.cpp
@@ -5,7 +5,8 @@
#include "storm-gspn/settings/modules/GSPNExportSettings.h"
#include "storm-conv/settings/modules/JaniExportSettings.h"
#include "storm-conv/api/storm-conv.h"
-
+#include "storm-parsers/parser/ExpressionParser.h"
+#include "storm/exceptions/WrongFormatException.h"
namespace storm {
namespace api {
@@ -71,9 +72,40 @@ namespace storm {
if (exportSettings.isAddJaniPropertiesSet()) {
properties.insert(properties.end(), builder.getStandardProperties().begin(), builder.getStandardProperties().end());
}
- storm::api::exportJaniToFile(*model, properties, exportSettings.getWriteToJaniFilename());
+ storm::api::exportJaniToFile(*model, properties, exportSettings.getWriteToJaniFilename(), jani.isCompactJsonSet());
delete model;
}
}
+
+ std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const& filename, storm::gspn::GSPN const& gspn) {
+ storm::parser::ExpressionParser expressionParser(*gspn.getExpressionManager());
+ std::unordered_map<std::string, storm::expressions::Expression> identifierMapping;
+ for (auto const& var : gspn.getExpressionManager()->getVariables()) {
+ identifierMapping.emplace(var.getName(), var.getExpression());
+ }
+ expressionParser.setIdentifierMapping(identifierMapping);
+ expressionParser.setAcceptDoubleLiterals(false);
+
+ std::unordered_map<std::string, uint64_t> map;
+
+ std::ifstream stream;
+ storm::utility::openFile(filename, stream);
+
+ std::string line;
+ while ( std::getline(stream, line) ) {
+ std::vector<std::string> strs;
+ boost::split(strs, line, boost::is_any_of("\t "));
+ STORM_LOG_THROW(strs.size() == 2, storm::exceptions::WrongFormatException, "Expect key value pairs");
+ storm::expressions::Expression expr = expressionParser.parseFromString(strs[1]);
+ if (!gspn.getConstantsSubstitution().empty()) {
+ expr = expr.substitute(gspn.getConstantsSubstitution());
+ }
+ STORM_LOG_THROW(!expr.containsVariables(), storm::exceptions::WrongFormatException, "The capacity expression '" << strs[1] << "' still contains undefined constants.");
+ map[strs[0]] = expr.evaluateAsInt();
+ }
+ storm::utility::closeFile(stream);
+ return map;
+ }
}
}
+
diff --git a/src/storm-gspn/api/storm-gspn.h b/src/storm-gspn/api/storm-gspn.h
index 7d2360946..a54bd6e28 100644
--- a/src/storm-gspn/api/storm-gspn.h
+++ b/src/storm-gspn/api/storm-gspn.h
@@ -1,5 +1,7 @@
#pragma once
+#include <unordered_map>
+
#include "storm/storage/jani/Model.h"
#include "storm-gspn/storage/gspn/GSPN.h"
#include "storm-gspn/builder/JaniGSPNBuilder.h"
@@ -14,6 +16,8 @@ namespace storm {
void handleGSPNExportSettings(storm::gspn::GSPN const& gspn,
std::function<std::vector<storm::jani::Property>(storm::builder::JaniGSPNBuilder const&)> const& janiProperyGetter = [](storm::builder::JaniGSPNBuilder const&) { return std::vector<storm::jani::Property>(); });
-
+
+ std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const& filename, storm::gspn::GSPN const& gspn);
+
}
}
diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp
index aa8c64a4f..744b76eb4 100644
--- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp
+++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp
@@ -3,11 +3,19 @@
#include <memory>
#include "storm/logic/Formulas.h"
+
+#include "storm/exceptions/InvalidModelException.h"
namespace storm {
namespace builder {
storm::jani::Model* JaniGSPNBuilder::build(std::string const& automatonName, bool buildStandardProperties) {
- storm::jani::Model* model = new storm::jani::Model(gspn.getName(), storm::jani::ModelType::MA, janiVersion, expressionManager);
+ storm::jani::ModelType modelType = storm::jani::ModelType::MA;
+ if (gspn.getNumberOfTimedTransitions() == 0) {
+ storm::jani::ModelType modelType = storm::jani::ModelType::MDP;
+ } else if (gspn.getNumberOfImmediateTransitions() == 0) {
+ storm::jani::ModelType modelType = storm::jani::ModelType::CTMC;
+ }
+ storm::jani::Model* model = new storm::jani::Model(gspn.getName(), modelType, janiVersion, expressionManager);
storm::jani::Automaton mainAutomaton(automatonName, expressionManager->declareIntegerVariable("loc"));
addVariables(model);
uint64_t locId = addLocation(mainAutomaton);
@@ -132,7 +140,7 @@ namespace storm {
}
for (auto const& trans : gspn.getTimedTransitions()) {
storm::expressions::Expression guard = expressionManager->boolean(true);
-
+
std::vector<storm::jani::Assignment> assignments;
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
@@ -153,9 +161,29 @@ namespace storm {
std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(guard);
automaton.registerTemplateEdge(templateEdge);
+
+ storm::expressions::Expression rate = expressionManager->rational(trans.getRate());
+ if (trans.hasInfiniteServerSemantics() || (trans.hasKServerSemantics() && !trans.hasSingleServerSemantics())) {
+ STORM_LOG_THROW(trans.hasKServerSemantics() || !trans.getInputPlaces().empty(), storm::exceptions::InvalidModelException, "Unclear semantics: Found a transition with infinite-server semantics and without input place.");
+ storm::expressions::Expression enablingDegree;
+ bool firstArgumentOfMinExpression = true;
+ if (trans.hasKServerSemantics()) {
+ enablingDegree = expressionManager->integer(trans.getNumberOfServers());
+ firstArgumentOfMinExpression = false;
+ }
+ for (auto const& inPlaceEntry : trans.getInputPlaces()) {
+ storm::expressions::Expression enablingDegreeInPlace = vars[inPlaceEntry.first]->getExpressionVariable() / expressionManager->integer(inPlaceEntry.second); // Integer division!
+ if (firstArgumentOfMinExpression == true) {
+ enablingDegree = enablingDegreeInPlace;
+ } else {
+ enablingDegree = storm::expressions::minimum(enablingDegree, enablingDegreeInPlace);
+ }
+ }
+ rate = rate * enablingDegree;
+ }
templateEdge->addDestination(assignments);
- storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans.getRate()), templateEdge, {locId}, {expressionManager->integer(1)});
+ storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, rate, templateEdge, {locId}, {expressionManager->integer(1)});
automaton.addEdge(e);
}
diff --git a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp
index f4b4418a2..4c77bc3a2 100644
--- a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp
+++ b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp
@@ -23,14 +23,23 @@ namespace {
namespace storm {
namespace parser {
- GreatSpnEditorProjectParser::GreatSpnEditorProjectParser() : manager(std::make_shared<storm::expressions::ExpressionManager>()), expressionParser(*manager) {
- // Intentionally left empty
+ GreatSpnEditorProjectParser::GreatSpnEditorProjectParser(std::string const& constantDefinitionString) : manager(std::make_shared<storm::expressions::ExpressionManager>()) {
+ if (constantDefinitionString != "") {
+ std::vector<std::string> constDefs;
+ boost::split( constDefs, constantDefinitionString, boost::is_any_of(","));
+ for (auto const& pair : constDefs) {
+ std::vector<std::string> keyvaluepair;
+ boost::split( keyvaluepair, pair, boost::is_any_of("="));
+ STORM_LOG_THROW(keyvaluepair.size() == 2, storm::exceptions::WrongFormatException, "Expected a constant definition of the form N=42 but got " << pair);
+ constantDefinitions.emplace(keyvaluepair.at(0), keyvaluepair.at(1));
+ }
+ }
}
storm::gspn::GSPN* GreatSpnEditorProjectParser::parse(xercesc::DOMElement const* elementRoot) {
if (storm::adapters::XMLtoString(elementRoot->getTagName()) == "project") {
traverseProjectElement(elementRoot);
- return builder.buildGspn();
+ return builder.buildGspn(manager, constantsSubstitution);
} else {
// If the top-level node is not a "pnml" or "" node, then throw an exception.
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n");
@@ -121,17 +130,23 @@ namespace storm {
// traverse children
// First pass: find constant definitions
+ constantsSubstitution.clear();
+ expressionParser = std::make_shared<storm::parser::ExpressionParser>(*manager);
std::unordered_map<std::string, storm::expressions::Expression> identifierMapping;
- expressionParser.setIdentifierMapping(identifierMapping);
+ expressionParser->setIdentifierMapping(identifierMapping);
for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
auto child = node->getChildNodes()->item(i);
auto name = storm::adapters::getName(child);
- if (name.compare("constant") == 0) {
- traverseConstantElement(child, identifierMapping);
+ if (name.compare("constant") == 0 || name.compare("template") == 0) {
+ traverseConstantOrTemplateElement(child);
}
}
- expressionParser.setIdentifierMapping(identifierMapping);
-
+ // Update the expression parser to make the newly created variables known to it
+ expressionParser = std::make_shared<storm::parser::ExpressionParser>(*manager);
+ for (auto const& var : manager->getVariables()) {
+ identifierMapping.emplace(var.getName(), var.getExpression());
+ }
+ expressionParser->setIdentifierMapping(identifierMapping);
// Second pass: traverse other children
for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
auto child = node->getChildNodes()->item(i);
@@ -141,7 +156,7 @@ namespace storm {
traversePlaceElement(child);
} else if(name.compare("transition") == 0) {
traverseTransitionElement(child);
- } else if(name.compare("constant") == 0) {
+ } else if(name.compare("constant") == 0 || name.compare("template") == 0) {
// Ignore constant def in second pass
} else if (isOnlyWhitespace(name)) {
// ignore node (contains only whitespace)
@@ -153,7 +168,7 @@ namespace storm {
}
}
- void GreatSpnEditorProjectParser::traverseConstantElement(xercesc::DOMNode const* const node, std::unordered_map<std::string, storm::expressions::Expression>& identifierMapping) {
+ void GreatSpnEditorProjectParser::traverseConstantOrTemplateElement(xercesc::DOMNode const* const node) {
std::string identifier;
storm::expressions::Type type;
std::string valueStr = "";
@@ -165,9 +180,11 @@ namespace storm {
if (name.compare("name") == 0) {
identifier = storm::adapters::XMLtoString(attr->getNodeValue());
- } else if (name.compare("consttype") == 0) {
+ } else if (name.compare("consttype") == 0 || name.compare("type") == 0) {
if (storm::adapters::XMLtoString(attr->getNodeValue()).compare("REAL") == 0) {
type = manager->getRationalType();
+ } else if (storm::adapters::XMLtoString(attr->getNodeValue()).compare("INTEGER") == 0) {
+ type = manager->getIntegerType();
} else {
STORM_PRINT_AND_LOG("Unknown consttype: " << storm::adapters::XMLtoString(attr->getNodeValue()) << std::endl);
}
@@ -182,15 +199,24 @@ namespace storm {
}
}
- storm::expressions::Expression valueExpression;
+ STORM_LOG_THROW(!manager->hasVariable(identifier), storm::exceptions::NotSupportedException, "Multiple definitions of constant '" << identifier << "' were found.");
+ if (valueStr == "") {
+ auto constDef = constantDefinitions.find(identifier);
+ STORM_LOG_THROW(constDef != constantDefinitions.end(), storm::exceptions::NotSupportedException, "Constant '" << identifier << "' has no value defined.");
+ valueStr = constDef->second;
+ }
+ storm::expressions::Variable var;
if (type.isRationalType()) {
- expressionParser.setAcceptDoubleLiterals(true);
- valueExpression = manager->rational(expressionParser.parseFromString(valueStr).evaluateAsRational());
+ var = manager->declareRationalVariable(identifier);
+ expressionParser->setAcceptDoubleLiterals(true);
+ } else if (type.isIntegerType()) {
+ var = manager->declareIntegerVariable(identifier);
+ expressionParser->setAcceptDoubleLiterals(false);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unknown type of constant" << type << ".");
}
- identifierMapping.emplace(identifier, valueExpression);
-
+ constantsSubstitution.emplace(var, expressionParser->parseFromString(valueStr));
+
// traverse children
for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
auto child = node->getChildNodes()->item(i);
@@ -257,7 +283,7 @@ namespace storm {
if (name.compare("name") == 0) {
placeName = storm::adapters::XMLtoString(attr->getNodeValue());
} else if (name.compare("marking") == 0) {
- initialTokens = std::stoull(storm::adapters::XMLtoString(attr->getNodeValue()));
+ initialTokens = parseInt(storm::adapters::XMLtoString(attr->getNodeValue()));
} else if (ignorePlaceAttribute(name)) {
// ignore node
} else {
@@ -297,6 +323,9 @@ namespace storm {
std::string transitionName;
bool immediateTransition;
double rate = 1.0; // The default rate in GreatSPN.
+ double weight = 1.0; // The default weight in GreatSpn
+ uint64_t priority = 1; // The default priority in GreatSpn
+ boost::optional<uint64_t> numServers;
// traverse attributes
for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
@@ -308,12 +337,26 @@ namespace storm {
} else if (name.compare("type") == 0) {
if (storm::adapters::XMLtoString(attr->getNodeValue()).compare("EXP") == 0) {
immediateTransition = false;
- } else {
+ } else if (storm::adapters::XMLtoString(attr->getNodeValue()).compare("IMM") == 0) {
immediateTransition = true;
+ } else {
+ STORM_PRINT_AND_LOG("unknown transition type: " << storm::adapters::XMLtoString(attr->getNodeValue()));
}
} else if(name.compare("delay") == 0) {
- expressionParser.setAcceptDoubleLiterals(true);
- rate = expressionParser.parseFromString(storm::adapters::XMLtoString(attr->getNodeValue())).evaluateAsDouble();
+ rate = parseReal(storm::adapters::XMLtoString(attr->getNodeValue()));
+ } else if(name.compare("weight") == 0) {
+ weight = parseReal(storm::adapters::XMLtoString(attr->getNodeValue()));
+ } else if(name.compare("priority") == 0) {
+ priority = parseInt(storm::adapters::XMLtoString(attr->getNodeValue()));
+ } else if (name.compare("nservers") == 0) {
+ std::string nservers = storm::adapters::XMLtoString(attr->getNodeValue());
+ if (nservers == "Single") {
+ numServers = 1;
+ } else if (nservers == "Infinite") {
+ // Ignore this case as we assume infinite by default (similar to GreatSpn)
+ } else {
+ numServers = parseInt(nservers);
+ }
} else if (ignoreTransitionAttribute(name)) {
// ignore node
} else {
@@ -325,9 +368,9 @@ namespace storm {
}
if (immediateTransition) {
- builder.addImmediateTransition(0, 0, transitionName);
+ builder.addImmediateTransition(priority, weight, transitionName);
} else {
- builder.addTimedTransition(0, rate, transitionName);
+ builder.addTimedTransition(0, rate, numServers, transitionName);
}
// traverse children
@@ -374,10 +417,10 @@ namespace storm {
head = storm::adapters::XMLtoString(attr->getNodeValue());
} else if (name.compare("tail") == 0) {
tail = storm::adapters::XMLtoString(attr->getNodeValue());
- } else if (name.compare("kind") == 0) {
+ } else if (name.compare("kind") == 0 || name.compare("type") == 0) {
kind = storm::adapters::XMLtoString(attr->getNodeValue());
} else if (name.compare("mult") == 0) {
- mult = std::stoull(storm::adapters::XMLtoString(attr->getNodeValue()));
+ mult = parseInt(storm::adapters::XMLtoString(attr->getNodeValue()));
} else if (ignoreArcAttribute(name)) {
// ignore node
} else {
@@ -420,6 +463,21 @@ namespace storm {
}
}
+ int64_t GreatSpnEditorProjectParser::parseInt(std::string str) {
+ expressionParser->setAcceptDoubleLiterals(false);
+ auto expr = expressionParser->parseFromString(str).substitute(constantsSubstitution);
+ STORM_LOG_ASSERT(!expr.containsVariables(), "Can not evaluate expression " << str << " as it contains undefined variables.");
+ return expr.evaluateAsInt();
+ }
+
+ double GreatSpnEditorProjectParser::parseReal(std::string str) {
+ expressionParser->setAcceptDoubleLiterals(true);
+ auto expr = expressionParser->parseFromString(str).substitute(constantsSubstitution);
+ STORM_LOG_ASSERT(!expr.containsVariables(), "Can not evaluate expression " << str << " as it contains undefined variables.");
+ return expr.evaluateAsDouble();
+ }
+
+
}
}
#endif
diff --git a/src/storm-gspn/parser/GreatSpnEditorProjectParser.h b/src/storm-gspn/parser/GreatSpnEditorProjectParser.h
index ba6f67a6a..7663d2a23 100644
--- a/src/storm-gspn/parser/GreatSpnEditorProjectParser.h
+++ b/src/storm-gspn/parser/GreatSpnEditorProjectParser.h
@@ -20,7 +20,7 @@ namespace storm {
public:
- GreatSpnEditorProjectParser();
+ GreatSpnEditorProjectParser(std::string const& constantDefinitionString);
/*!
* Parses the given file into the GSPN.
@@ -36,17 +36,20 @@ namespace storm {
void traverseNodesElement(xercesc::DOMNode const* const node);
void traverseEdgesElement(xercesc::DOMNode const* const node);
- void traverseConstantElement(xercesc::DOMNode const* const node, std::unordered_map<std::string, storm::expressions::Expression>& identifierMapping);
+ void traverseConstantOrTemplateElement(xercesc::DOMNode const* const node);
void traversePlaceElement(xercesc::DOMNode const* const node);
void traverseTransitionElement(xercesc::DOMNode const* const node);
void traverseArcElement(xercesc::DOMNode const* const node);
+ int64_t parseInt(std::string str);
+ double parseReal(std::string str);
// the constructed gspn
storm::gspn::GspnBuilder builder;
std::shared_ptr<storm::expressions::ExpressionManager> manager;
- storm::parser::ExpressionParser expressionParser;
-
+ std::shared_ptr<storm::parser::ExpressionParser> expressionParser;
+ std::unordered_map<std::string, std::string> constantDefinitions;
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution;
};
}
}
diff --git a/src/storm-gspn/parser/GspnParser.cpp b/src/storm-gspn/parser/GspnParser.cpp
index b92b6f006..89a2f57e9 100644
--- a/src/storm-gspn/parser/GspnParser.cpp
+++ b/src/storm-gspn/parser/GspnParser.cpp
@@ -12,7 +12,7 @@
namespace storm {
namespace parser {
- storm::gspn::GSPN* GspnParser::parse(std::string const& filename) {
+ storm::gspn::GSPN* GspnParser::parse(std::string const& filename, std::string const& constantDefinitions) {
#ifdef STORM_HAVE_XERCES
// initialize xercesc
try {
@@ -62,10 +62,11 @@ namespace storm {
xercesc::DOMElement* elementRoot = parser->getDocument()->getDocumentElement();
if (storm::adapters::XMLtoString(elementRoot->getTagName()) == "pnml") {
+ STORM_LOG_WARN_COND(constantDefinitions == "", "Constant definitions for pnml files are currently not supported.");
PnmlParser p;
return p.parse(elementRoot);
} else if (storm::adapters::XMLtoString(elementRoot->getTagName()) == "project") {
- GreatSpnEditorProjectParser p;
+ GreatSpnEditorProjectParser p(constantDefinitions);
return p.parse(elementRoot);
} else {
// If the top-level node is not a "pnml" or "" node, then throw an exception.
diff --git a/src/storm-gspn/parser/GspnParser.h b/src/storm-gspn/parser/GspnParser.h
index 862dfc757..512f0ddd6 100644
--- a/src/storm-gspn/parser/GspnParser.h
+++ b/src/storm-gspn/parser/GspnParser.h
@@ -4,7 +4,7 @@ namespace storm {
namespace parser {
class GspnParser {
public:
- static storm::gspn::GSPN* parse(std::string const& filename);
+ static storm::gspn::GSPN* parse(std::string const& filename, std::string const& constantDefinitions = "");
};
}
}
diff --git a/src/storm-gspn/settings/modules/GSPNSettings.cpp b/src/storm-gspn/settings/modules/GSPNSettings.cpp
index fd274726f..b114559a5 100644
--- a/src/storm-gspn/settings/modules/GSPNSettings.cpp
+++ b/src/storm-gspn/settings/modules/GSPNSettings.cpp
@@ -19,12 +19,16 @@ namespace storm {
const std::string GSPNSettings::capacitiesFileOptionName = "capacitiesfile";
const std::string GSPNSettings::capacitiesFileOptionShortName = "capacities";
const std::string GSPNSettings::capacityOptionName = "capacity";
+ const std::string GSPNSettings::constantsOptionName = "constants";
+ const std::string GSPNSettings::constantsOptionShortName = "const";
+
GSPNSettings::GSPNSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, gspnFileOptionName, false, "Parses the GSPN.").setShortName(gspnFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, capacitiesFileOptionName, false, "Capacaties as invariants for places.").setShortName(capacitiesFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, capacityOptionName, false, "Global capacity as invariants for all places.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "capacity").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedGreaterValidator(0)).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use.").setShortName(constantsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
}
bool GSPNSettings::isGspnFileSet() const {
@@ -51,6 +55,14 @@ namespace storm {
return this->getOption(capacityOptionName).getArgumentByName("value").getValueAsUnsignedInteger();
}
+ bool GSPNSettings::isConstantsSet() const {
+ return this->getOption(constantsOptionName).getHasOptionBeenSet();
+ }
+
+ std::string GSPNSettings::getConstantDefinitionString() const {
+ return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString();
+ }
+
void GSPNSettings::finalize() {
}
diff --git a/src/storm-gspn/settings/modules/GSPNSettings.h b/src/storm-gspn/settings/modules/GSPNSettings.h
index 665e588fb..78586cf9c 100644
--- a/src/storm-gspn/settings/modules/GSPNSettings.h
+++ b/src/storm-gspn/settings/modules/GSPNSettings.h
@@ -44,6 +44,16 @@ namespace storm {
*/
uint64_t getCapacity() const;
+ /*!
+ * Retrieves whether the constants ption was set.
+ */
+ bool isConstantsSet() const;
+
+ /*!
+ * Retrieves the string that defines the constants of a gspn
+ */
+ std::string getConstantDefinitionString() const;
+
bool check() const override;
void finalize() override;
@@ -56,7 +66,8 @@ namespace storm {
static const std::string capacitiesFileOptionName;
static const std::string capacitiesFileOptionShortName;
static const std::string capacityOptionName;
-
+ static const std::string constantsOptionName;
+ static const std::string constantsOptionShortName;
};
}
}
diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp
index c622cc4fe..903425735 100644
--- a/src/storm-gspn/storage/gspn/GSPN.cpp
+++ b/src/storm-gspn/storage/gspn/GSPN.cpp
@@ -26,8 +26,8 @@ namespace storm {
return tId;
}
- GSPN::GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager)
- : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager)
+ GSPN::GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantsSubstitution)
+ : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager), constantsSubstitution(constantsSubstitution)
{
}
@@ -134,12 +134,16 @@ namespace storm {
return getImmediateTransition(id);
}
+
+ std::shared_ptr<storm::expressions::ExpressionManager> const& GSPN::getExpressionManager() const {
+ return exprManager;
+ }
+
+ std::map<storm::expressions::Variable, storm::expressions::Expression> const& GSPN::getConstantsSubstitution() const {
+ return constantsSubstitution;
+ }
- std::shared_ptr<storm::expressions::ExpressionManager> const& GSPN::getExpressionManager() const {
- return exprManager;
- }
-
- void GSPN::setCapacities(std::unordered_map<std::string, uint64_t> const& mapping) {
+ void GSPN::setCapacities(std::unordered_map<std::string, uint64_t> const& mapping) {
for(auto const& entry : mapping) {
storm::gspn::Place* place = getPlace(entry.first);
STORM_LOG_THROW(place != nullptr, storm::exceptions::InvalidArgumentException, "No place with name " << entry.first);
@@ -168,6 +172,7 @@ namespace storm {
for (auto& trans : this->getTimedTransitions()) {
outStream << "\t" << trans.getName() << " [label=\"" << trans.getName();
outStream << "(" << trans.getRate() << ")\"];" << std::endl;
+ STORM_LOG_WARN_COND(trans.hasSingleServerSemantics(), "Unable to export non-trivial transition semantics"); // TODO
}
// print arcs
@@ -555,6 +560,7 @@ namespace storm {
// add timed transitions
for (const auto &trans : timedTransitions) {
+ STORM_LOG_WARN_COND(trans.hasInfiniteServerSemantics(), "Unable to export non-trivial transition semantics"); // TODO
stream << space2 << "<transition id=\"" << trans.getName() << "\">" << std::endl;
stream << space3 << "<rate>" << std::endl;
stream << space4 << "<value>" << trans.getRate() << "</value>" << std::endl;
diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h
index 7b37ed5cb..343dcd887 100644
--- a/src/storm-gspn/storage/gspn/GSPN.h
+++ b/src/storm-gspn/storage/gspn/GSPN.h
@@ -32,7 +32,7 @@ namespace storm {
GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions,
- std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager);
+ std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantsSubstitution = std::map<storm::expressions::Variable, storm::expressions::Expression>());
/*!
* Returns the number of places in this gspn.
@@ -145,8 +145,13 @@ namespace storm {
*/
std::shared_ptr<storm::expressions::ExpressionManager> const& getExpressionManager() const;
+ /*!
+ * Gets an assignment of occurring constants of the GSPN to their value
+ */
+ std::map<storm::expressions::Variable, storm::expressions::Expression> const& getConstantsSubstitution() const;
+
/**
- * Set Capacities according to name->capacity map.
+ * Set Capacities of places according to name->capacity map.
*/
void setCapacities(std::unordered_map<std::string, uint64_t> const& mapping);
@@ -217,6 +222,8 @@ namespace storm {
std::vector<storm::gspn::TransitionPartition> partitions;
std::shared_ptr<storm::expressions::ExpressionManager> exprManager;
+
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution;
// Layout information
mutable std::map<uint64_t, LayoutInfo> placeLayout;
diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp
index e273768ea..c39b5c0f7 100644
--- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp
+++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp
@@ -65,13 +65,22 @@ namespace storm {
return newId;
}
-
+
uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate, std::string const& name) {
+ return addTimedTransition(priority, rate, 1, name);
+ }
+
+ uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate, boost::optional<uint64_t> numServers, std::string const& name) {
auto trans = storm::gspn::TimedTransition<double>();
auto newId = GSPN::timedTransitionIdToTransitionId(timedTransitions.size());
trans.setName(name);
trans.setPriority(priority);
trans.setRate(rate);
+ if (numServers) {
+ trans.setKServerSemantics(numServers.get());
+ } else {
+ trans.setInfiniteServerSemantics();
+ }
trans.setID(newId);
timedTransitions.push_back(trans);
@@ -162,8 +171,13 @@ namespace storm {
- storm::gspn::GSPN* GspnBuilder::buildGspn() const {
- std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
+ storm::gspn::GSPN* GspnBuilder::buildGspn(std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantsSubstitution) const {
+ std::shared_ptr<storm::expressions::ExpressionManager> actualExprManager;
+ if (exprManager) {
+ actualExprManager = exprManager;
+ } else {
+ actualExprManager = std::make_shared<storm::expressions::ExpressionManager>();
+ }
std::vector<TransitionPartition> orderedPartitions;
for(auto const& priorityPartitions : partitions) {
@@ -179,10 +193,10 @@ namespace storm {
}
std::reverse(orderedPartitions.begin(), orderedPartitions.end());
for(auto const& placeEntry : placeNames) {
- exprManager->declareIntegerVariable(placeEntry.first, false);
+ actualExprManager->declareIntegerVariable(placeEntry.first, false);
}
- GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions, exprManager);
+ GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions, actualExprManager, constantsSubstitution);
result->setTransitionLayoutInfo(transitionLayout);
result->setPlaceLayoutInfo(placeLayout);
return result;
diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.h b/src/storm-gspn/storage/gspn/GspnBuilder.h
index a9a99699f..5e4db4a34 100644
--- a/src/storm-gspn/storage/gspn/GspnBuilder.h
+++ b/src/storm-gspn/storage/gspn/GspnBuilder.h
@@ -39,11 +39,20 @@ namespace storm {
/**
* Adds an timed transition to the gspn.
+ * The transition is assumed to have Single-Server-Semantics
* @param priority The priority for the transtion.
- * @param weight The weight for the transition.
+ * @param rate The rate for the transition.
*/
uint_fast64_t addTimedTransition(uint_fast64_t const &priority, RateType const& rate, std::string const& name = "");
+ /**
+ * Adds an timed transition to the gspn.
+ * @param priority The priority for the transtion.
+ * @param rate The rate for the transition.
+ * @param numServers The number of servers this transition has (in case of K-Server semantics) or boost::none (in case of Infinite-Server-Semantics).
+ */
+ uint_fast64_t addTimedTransition(uint_fast64_t const &priority, RateType const& rate, boost::optional<uint64_t> numServers, std::string const& name = "");
+
void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layoutInfo);
@@ -91,10 +100,10 @@ namespace storm {
/**
- *
+ * @param exprManager The expression manager that will be associated with the new gspn. If this is nullptr, a new expressionmanager will be created.
* @return The gspn which is constructed by the builder.
*/
- storm::gspn::GSPN* buildGspn() const;
+ storm::gspn::GSPN* buildGspn(std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = nullptr, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantsSubstitution = std::map<storm::expressions::Variable, storm::expressions::Expression>()) const;
private:
bool isImmediateTransitionId(uint64_t) const;
bool isTimedTransitionId(uint64_t) const;
diff --git a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
index 4e451d094..f4e910b81 100644
--- a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
+++ b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp
@@ -160,7 +160,16 @@ namespace storm {
data["name"] = transition.getName();
data["rate"] = transition.getRate();
data["priority"] = transition.getPriority();
-
+ if (!transition.hasSingleServerSemantics()) {
+ if (transition.hasInfiniteServerSemantics()) {
+ data["server-semantics"] = "infinite";
+ } else if (transition.hasKServerSemantics()) {
+ data["server-semantics"] = transition.getNumberOfServers();
+ } else {
+ STORM_LOG_WARN("Unable to export transition semantics.");
+ }
+ }
+
modernjson::json position;
position["x"] = x * scaleFactor;
position["y"] = y * scaleFactor;
diff --git a/src/storm-gspn/storage/gspn/TimedTransition.h b/src/storm-gspn/storage/gspn/TimedTransition.h
index d8399319d..37b5476f6 100644
--- a/src/storm-gspn/storage/gspn/TimedTransition.h
+++ b/src/storm-gspn/storage/gspn/TimedTransition.h
@@ -1,12 +1,18 @@
#pragma once
#include "storm-gspn/storage/gspn/Transition.h"
+#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace gspn {
template <typename RateType>
class TimedTransition : public storm::gspn::Transition {
public:
+
+ TimedTransition() {
+ setSingleServerSemantics();
+ }
+
/*!
* Sets the rate of this transition to the given value.
*
@@ -15,7 +21,43 @@ namespace storm {
void setRate(RateType const& rate) {
this->rate = rate;
}
-
+
+ /*!
+ * Sets the semantics of this transition
+ */
+ void setKServerSemantics(uint64_t k) {
+ STORM_LOG_THROW(k>0, storm::exceptions::InvalidArgumentException, "Invalid Parameter for server semantics: 0");
+ nServers = k;
+ }
+
+ void setSingleServerSemantics() {
+ nServers = 1;
+ }
+
+ void setInfiniteServerSemantics() {
+ nServers = 0;
+ }
+
+ /*!
+ * Retrieves the semantics of this transition
+ */
+ bool hasKServerSemantics() const {
+ return nServers > 0;
+ }
+
+ bool hasSingleServerSemantics() const {
+ return nServers == 1;
+ }
+
+ bool hasInfiniteServerSemantics() const {
+ return nServers == 0;
+ }
+
+ uint64_t getNumberOfServers() const {
+ STORM_LOG_ASSERT(hasKServerSemantics(), "Tried to get the number of servers of a timed transition although it does not have K-Server-Semantics.");
+ return nServers;
+ }
+
/*!
* Retrieves the rate of this transition.
*
@@ -28,6 +70,9 @@ namespace storm {
private:
// the rate of the transition
RateType rate;
+
+ // the number of servers of this transition. 0 means infinite server semantics.
+ uint64_t nServers;
};
}
}
\ No newline at end of file
diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp
index 6d2df8e36..fc61bed31 100644
--- a/src/storm-parsers/parser/JaniParser.cpp
+++ b/src/storm-parsers/parser/JaniParser.cpp
@@ -92,6 +92,15 @@ namespace storm {
storm::jani::ModelType type = storm::jani::getModelType(modeltypestring);
STORM_LOG_THROW(type != storm::jani::ModelType::UNDEFINED, storm::exceptions::InvalidJaniException, "model type " + modeltypestring + " not recognized");
storm::jani::Model model(name, type, version, expressionManager);
+ size_t featuresCount = parsedStructure.count("features");
+ STORM_LOG_THROW(featuresCount < 2, storm::exceptions::InvalidJaniException, "features-declarations can be given at most once.");
+ if (featuresCount == 1) {
+ std::unordered_set<std::string> supportedFeatures = {"derived-operators", "state-exit-rewards"};
+ for (auto const& feature : parsedStructure.at("features")) {
+ std::string featureStr = getString(feature, "Model feature");
+ STORM_LOG_WARN_COND(supportedFeatures.find(featureStr) != supportedFeatures.end(), "Storm does not support the model feature " << featureStr << ".");
+ }
+ }
size_t actionCount = parsedStructure.count("actions");
STORM_LOG_THROW(actionCount < 2, storm::exceptions::InvalidJaniException, "Action-declarations can be given at most once.");
if (actionCount > 0) {
@@ -190,6 +199,24 @@ namespace storm {
}
+ storm::logic::RewardAccumulation JaniParser::parseRewardAccumulation(json const& accStructure, std::string const& context) {
+ bool accTime = false;
+ bool accSteps = false;
+ bool accExit = false;
+ STORM_LOG_THROW(accStructure.is_array(), storm::exceptions::InvalidJaniException, "Accumulate should be an array");
+ for (auto const& accEntry : accStructure) {
+ if (accEntry == "steps") {
+ accSteps = true;
+ } else if (accEntry == "time") {
+ accTime = true;
+ } else if (accEntry == "exit") {
+ accExit = true;
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "One may only accumulate either 'steps' or 'time' or 'exit', got " << accEntry.dump() << " in " << context);
+ }
+ }
+ return storm::logic::RewardAccumulation(accSteps, accTime, accExit);
+ }
std::shared_ptr<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext,std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::string const& context, boost::optional<storm::logic::Bound> bound) {
if (propertyStructure.is_boolean()) {
@@ -232,29 +259,17 @@ namespace storm {
opInfo.optimalityType = opString == "Emin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
opInfo.bound = bound;
- bool accTime = false;
- bool accSteps = false;
+ storm::logic::RewardAccumulation rewardAccumulation(false, false, false);
if (propertyStructure.count("accumulate") > 0) {
- STORM_LOG_THROW(propertyStructure.at("accumulate").is_array(), storm::exceptions::InvalidJaniException, "Accumulate should be an array");
- for(auto const& accEntry : propertyStructure.at("accumulate")) {
- if (accEntry == "steps") {
- accSteps = true;
- } else if (accEntry == "time") {
- accTime = true;
- } else {
- STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "One may only accumulate either 'steps' or 'time', got " << accEntry.dump() << " in " << context);
- }
- }
+ rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), context);
}
- STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "Storm does not allow to accumulate over both time and steps");
-
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 " + context);
STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a reward-instant in " + context);
storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context, globalVars, constants);
- if(!accTime && !accSteps) {
+ if(rewardAccumulation.isEmpty()) {
if (rewExpr.isVariable()) {
std::string rewardName = rewExpr.getVariables().begin()->getName();
return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(stepInstantExpr, storm::logic::TimeBoundType::Steps), rewardName, opInfo);
@@ -264,7 +279,7 @@ namespace storm {
} else {
if (rewExpr.isVariable()) {
std::string rewardName = rewExpr.getVariables().begin()->getName();
- return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)), rewardName, opInfo);
+ return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps), rewardAccumulation), rewardName, opInfo);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported");
}
@@ -274,7 +289,7 @@ namespace storm {
storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context, globalVars, constants);
- if(!accTime && !accSteps) {
+ if(rewardAccumulation.isEmpty()) {
if (rewExpr.isVariable()) {
std::string rewardName = rewExpr.getVariables().begin()->getName();
return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(timeInstantExpr, storm::logic::TimeBoundType::Time), rewardName, opInfo);
@@ -284,7 +299,7 @@ namespace storm {
} else {
if (rewExpr.isVariable()) {
std::string rewardName = rewExpr.getVariables().begin()->getName();
- return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)), rewardName, opInfo);
+ return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time), rewardAccumulation), rewardName, opInfo);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported");
}
@@ -295,24 +310,14 @@ namespace storm {
for (auto const& rewInst : propertyStructure.at("reward-instants")) {
storm::expressions::Expression rewInstExpression = parseExpression(rewInst.at("exp"), "Reward expression in " + context, globalVars, constants);
STORM_LOG_THROW(!rewInstExpression.isVariable(), storm::exceptions::NotSupportedException, "Reward bounded cumulative reward formulas should only argue over reward expressions.");
- boundReferences.emplace_back(rewInstExpression.getVariables().begin()->getName());
- bool rewInstAccSteps(false), rewInstAccTime(false);
- for (auto const& accEntry : rewInst.at("accumulate")) {
- if (accEntry == "steps") {
- rewInstAccSteps = true;
- } else if (accEntry == "time") {
- rewInstAccTime = true;
- } else {
- STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "One may only accumulate either 'steps' or 'time', got " << accEntry.dump() << " in " << context);
- }
- }
- STORM_LOG_THROW((rewInstAccTime && !rewInstAccSteps) || (!rewInstAccTime && rewInstAccSteps), storm::exceptions::NotSupportedException, "Storm only allows to accumulate either over time or over steps in " + context);
+ storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rewInst.at("accumulate"), context);
+ boundReferences.emplace_back(rewInstExpression.getVariables().begin()->getName(), boundRewardAccumulation);
storm::expressions::Expression rewInstantExpr = parseExpression(rewInst.at("instant"), "reward instant in " + context, globalVars, constants);
bounds.emplace_back(false, rewInstantExpr);
}
if (rewExpr.isVariable()) {
std::string rewardName = rewExpr.getVariables().begin()->getName();
- return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(bounds, boundReferences), rewardName, opInfo);
+ return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(bounds, boundReferences, rewardAccumulation), rewardName, opInfo);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported");
}
@@ -320,9 +325,9 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> subformula;
if (propertyStructure.count("reach") > 0) {
auto context = time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward;
- subformula = std::make_shared<storm::logic::EventuallyFormula>(parseFormula(propertyStructure.at("reach"), context, globalVars, constants, "Reach-expression of operator " + opString), context);
+ subformula = std::make_shared<storm::logic::EventuallyFormula>(parseFormula(propertyStructure.at("reach"), context, globalVars, constants, "Reach-expression of operator " + opString), context, rewardAccumulation);
} else {
- subformula = std::make_shared<storm::logic::TotalRewardFormula>();
+ subformula = std::make_shared<storm::logic::TotalRewardFormula>(rewardAccumulation);
}
if (rewExpr.isVariable()) {
assert(!time);
@@ -404,6 +409,8 @@ namespace storm {
STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context);
storm::expressions::Expression rewExpr = parseExpression(rbStructure.at("exp"), "Reward expression in " + context, globalVars, constants);
STORM_LOG_THROW(rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions.");
+ storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rbStructure.at("accumulate"), context);
+ tbReferences.emplace_back(rewExpr.getVariables().begin()->getName(), boundRewardAccumulation);
std::string rewardName = rewExpr.getVariables().begin()->getName();
STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type.");
if (pi.hasLowerBound()) {
@@ -481,8 +488,6 @@ namespace storm {
} else if(propertyStructure.at("right").count("op") > 0 && (propertyStructure.at("right").at("op") == "Pmin" || propertyStructure.at("right").at("op") == "Pmax" || propertyStructure.at("right").at("op") == "Emin" || propertyStructure.at("right").at("op") == "Emax" || propertyStructure.at("right").at("op") == "Smin" || propertyStructure.at("right").at("op") == "Smax")) {
auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get<std::string>(),{},{});
- STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported");
- // TODO evaluate this expression directly as rational number
return parseFormula(propertyStructure.at("right"),formulaContext, globalVars, constants, "", storm::logic::Bound(ct, expr));
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex comparisons are allowed.");
@@ -999,8 +1004,7 @@ namespace storm {
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
- // TODO implement
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "modulo operation is not yet implemented");
+ return arguments[0] % arguments[1];
} else if (opstring == "max") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
assert(arguments.size() == 2);
@@ -1037,14 +1041,13 @@ namespace storm {
arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
assert(arguments.size() == 1);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
- return storm::expressions::abs(arguments[0]);
+ return storm::expressions::truncate(arguments[0]);
} else if (opstring == "pow") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
assert(arguments.size() == 2);
ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
- // TODO implement
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "pow operation is not yet implemented");
+ return arguments[0]^arguments[1];
} else if (opstring == "exp") {
arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator);
assert(arguments.size() == 2);
diff --git a/src/storm-parsers/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h
index a6141c37c..d14b20259 100644
--- a/src/storm-parsers/parser/JaniParser.h
+++ b/src/storm-parsers/parser/JaniParser.h
@@ -2,6 +2,7 @@
#include "storm/storage/jani/Constant.h"
#include "storm/logic/Formula.h"
#include "storm/logic/Bound.h"
+#include "storm/logic/RewardAccumulation.h"
#include "storm/exceptions/FileIoException.h"
#include "storm/storage/expressions/ExpressionManager.h"
@@ -74,7 +75,8 @@ namespace storm {
std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::string const& context);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::string const& context);
storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants);
-
+ storm::logic::RewardAccumulation parseRewardAccumulation(json const& accStructure, std::string const& context);
+
std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure);
storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp
index 5ae5248b3..fe4585023 100644
--- a/src/storm-pgcl-cli/storm-pgcl.cpp
+++ b/src/storm-pgcl-cli/storm-pgcl.cpp
@@ -43,7 +43,7 @@ void handleJani(storm::jani::Model& model) {
storm::converter::JaniConversionOptions options(jani);
storm::api::postprocessJani(model, options);
if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isToJaniSet()) {
- storm::api::exportJaniToFile(model, {}, storm::settings::getModule<storm::settings::modules::PGCLSettings>().getWriteToJaniFilename());
+ storm::api::exportJaniToFile(model, {}, storm::settings::getModule<storm::settings::modules::PGCLSettings>().getWriteToJaniFilename(), jani.isCompactJsonSet());
} else {
storm::api::printJaniToStream(model, {}, std::cout);
}
diff --git a/src/storm/builder/DdPrismModelBuilder.h b/src/storm/builder/DdPrismModelBuilder.h
index 57d990b23..fb357a6c8 100644
--- a/src/storm/builder/DdPrismModelBuilder.h
+++ b/src/storm/builder/DdPrismModelBuilder.h
@@ -3,6 +3,7 @@
#include <map>
#include <boost/optional.hpp>
+#include <boost/variant.hpp>
#include "storm/storage/prism/Program.h"
diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index 97c768944..6054e7cd3 100644
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@@ -285,7 +285,11 @@ namespace storm {
out << ", ";
}
if (this->getTimeBoundReference(i).isRewardBound()) {
- out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}";
+ out << "rew";
+ if (this->getTimeBoundReference(i).hasRewardAccumulation()) {
+ out << "[" << this->getTimeBoundReference(i).getRewardAccumulation() << "]";
+ }
+ out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}";
} else if (this->getTimeBoundReference(i).isStepBound()) {
out << "steps";
//} else if (this->getTimeBoundReference(i).isStepBound())
diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp
index d97dd41d6..4b427b1dc 100644
--- a/src/storm/logic/CloneVisitor.cpp
+++ b/src/storm/logic/CloneVisitor.cpp
@@ -70,7 +70,11 @@ namespace storm {
boost::any CloneVisitor::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));
- return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext()));
+ if (f.hasRewardAccumulation()) {
+ return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
+ } else {
+ return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext()));
+ }
}
boost::any CloneVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
@@ -119,8 +123,8 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation()));
}
- boost::any CloneVisitor::visit(TotalRewardFormula const&, boost::any const&) const {
- return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>());
+ boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const&) const {
+ return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f));
}
boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp
index 19a60a623..bbf21cbf0 100644
--- a/src/storm/logic/CumulativeRewardFormula.cpp
+++ b/src/storm/logic/CumulativeRewardFormula.cpp
@@ -9,11 +9,11 @@
namespace storm {
namespace logic {
- CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference) : timeBoundReferences({timeBoundReference}), bounds({bound}) {
+ CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference, boost::optional<RewardAccumulation> rewardAccumulation) : timeBoundReferences({timeBoundReference}), bounds({bound}), rewardAccumulation(rewardAccumulation) {
// Intentionally left empty.
}
- CumulativeRewardFormula::CumulativeRewardFormula(std::vector<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences) : timeBoundReferences(timeBoundReferences), bounds(bounds) {
+ CumulativeRewardFormula::CumulativeRewardFormula(std::vector<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences, boost::optional<RewardAccumulation> rewardAccumulation) : timeBoundReferences(timeBoundReferences), bounds(bounds), rewardAccumulation(rewardAccumulation) {
STORM_LOG_ASSERT(this->timeBoundReferences.size() == this->bounds.size(), "Number of time bounds and number of time bound references does not match.");
STORM_LOG_ASSERT(!this->timeBoundReferences.empty(), "No time bounds given.");
@@ -137,12 +137,24 @@ namespace storm {
STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants.");
}
+ bool CumulativeRewardFormula::hasRewardAccumulation() const {
+ return rewardAccumulation.is_initialized();
+ }
+
+ RewardAccumulation const& CumulativeRewardFormula::getRewardAccumulation() const {
+ return rewardAccumulation.get();
+ }
+
+
std::shared_ptr<CumulativeRewardFormula const> CumulativeRewardFormula::restrictToDimension(unsigned i) const {
return std::make_shared<CumulativeRewardFormula const>(bounds.at(i), getTimeBoundReference(i));
}
std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const {
out << "C";
+ if (hasRewardAccumulation()) {
+ out << "[" << getRewardAccumulation() << "]";
+ }
if (this->isMultiDimensional()) {
out << "^{";
}
@@ -151,7 +163,11 @@ namespace storm {
out << ", ";
}
if (this->getTimeBoundReference(i).isRewardBound()) {
- out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}";
+ out << "rew";
+ if (this->getTimeBoundReference(i).hasRewardAccumulation()) {
+ out << "[" << this->getTimeBoundReference(i).getRewardAccumulation() << "]";
+ }
+ out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}";
} else if (this->getTimeBoundReference(i).isStepBound()) {
out << "steps";
//} else if (this->getTimeBoundReference(i).isStepBound())
diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h
index e40370b07..4c436037e 100644
--- a/src/storm/logic/CumulativeRewardFormula.h
+++ b/src/storm/logic/CumulativeRewardFormula.h
@@ -10,8 +10,8 @@ namespace storm {
namespace logic {
class CumulativeRewardFormula : public PathFormula {
public:
- CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time));
- CumulativeRewardFormula(std::vector<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences);
+ CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time), boost::optional<RewardAccumulation> rewardAccumulation = boost::none);
+ CumulativeRewardFormula(std::vector<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences, boost::optional<RewardAccumulation> rewardAccumulation = boost::none);
virtual ~CumulativeRewardFormula() = default;
@@ -47,6 +47,9 @@ namespace storm {
template <typename ValueType>
ValueType getNonStrictBound() const;
+ bool hasRewardAccumulation() const;
+ RewardAccumulation const& getRewardAccumulation() const;
+
std::shared_ptr<CumulativeRewardFormula const> restrictToDimension(unsigned i) const;
private:
@@ -54,6 +57,8 @@ namespace storm {
std::vector<TimeBoundReference> timeBoundReferences;
std::vector<TimeBound> bounds;
+ boost::optional<RewardAccumulation> rewardAccumulation;
+
};
}
}
diff --git a/src/storm/logic/EventuallyFormula.cpp b/src/storm/logic/EventuallyFormula.cpp
index 2f1243f8a..c8ed335e5 100644
--- a/src/storm/logic/EventuallyFormula.cpp
+++ b/src/storm/logic/EventuallyFormula.cpp
@@ -6,8 +6,9 @@
namespace storm {
namespace logic {
- EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context) : UnaryPathFormula(subformula), context(context) {
+ EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context, boost::optional<RewardAccumulation> rewardAccumulation) : UnaryPathFormula(subformula), context(context), rewardAccumulation(rewardAccumulation) {
STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward || context == FormulaContext::Time, storm::exceptions::InvalidPropertyException, "Invalid context for formula.");
+ STORM_LOG_THROW(context != FormulaContext::Probability || !rewardAccumulation.is_initialized(), storm::exceptions::InvalidPropertyException, "Reward accumulations should only be given for time- and reward formulas");
}
FormulaContext const& EventuallyFormula::getContext() const {
@@ -42,6 +43,14 @@ namespace storm {
return this->isReachabilityTimeFormula();
}
+ bool EventuallyFormula::hasRewardAccumulation() const {
+ return rewardAccumulation.is_initialized();
+ }
+
+ RewardAccumulation const& EventuallyFormula::getRewardAccumulation() const {
+ return rewardAccumulation.get();
+ }
+
boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
return visitor.visit(*this, data);
}
@@ -49,6 +58,9 @@ namespace storm {
std::ostream& EventuallyFormula::writeToStream(std::ostream& out) const {
out << "F ";
this->getSubformula().writeToStream(out);
+ if (hasRewardAccumulation()) {
+ out << "[" << getRewardAccumulation() << "]";
+ }
return out;
}
}
diff --git a/src/storm/logic/EventuallyFormula.h b/src/storm/logic/EventuallyFormula.h
index 9cc4d853d..5fa30da6d 100644
--- a/src/storm/logic/EventuallyFormula.h
+++ b/src/storm/logic/EventuallyFormula.h
@@ -1,14 +1,17 @@
#ifndef STORM_LOGIC_EVENTUALLYFORMULA_H_
#define STORM_LOGIC_EVENTUALLYFORMULA_H_
+#include <boost/optional.hpp>
+
#include "storm/logic/UnaryPathFormula.h"
#include "storm/logic/FormulaContext.h"
+#include "storm/logic/RewardAccumulation.h"
namespace storm {
namespace logic {
class EventuallyFormula : public UnaryPathFormula {
public:
- EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context = FormulaContext::Probability);
+ EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context = FormulaContext::Probability, boost::optional<RewardAccumulation> rewardAccumulation = boost::none);
virtual ~EventuallyFormula() {
// Intentionally left empty.
@@ -27,9 +30,12 @@ namespace storm {
virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
virtual std::ostream& writeToStream(std::ostream& out) const override;
+ bool hasRewardAccumulation() const;
+ RewardAccumulation const& getRewardAccumulation() const;
private:
FormulaContext context;
+ boost::optional<RewardAccumulation> rewardAccumulation;
};
}
}
diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp
index 24ad016c8..adc96728b 100644
--- a/src/storm/logic/FragmentChecker.cpp
+++ b/src/storm/logic/FragmentChecker.cpp
@@ -70,6 +70,9 @@ namespace storm {
} else {
assert(tbr.isRewardBound());
result = result && inherited.getSpecification().areRewardBoundedUntilFormulasAllowed();
+ if (tbr.hasRewardAccumulation()) {
+ result = result && inherited.getSpecification().isRewardAccumulationAllowed();
+ }
}
}
@@ -118,6 +121,7 @@ namespace storm {
bool result = inherited.getSpecification().areCumulativeRewardFormulasAllowed();
result = result && (!f.isMultiDimensional() || inherited.getSpecification().areMultiDimensionalCumulativeRewardFormulasAllowed());
+ result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
for (uint64_t i = 0; i < f.getDimension(); ++i) {
auto tbr = f.getTimeBoundReference(i);
if (tbr.isStepBound()) {
@@ -127,6 +131,9 @@ namespace storm {
} else {
assert(tbr.isRewardBound());
result = result && inherited.getSpecification().areRewardBoundedCumulativeRewardFormulasAllowed();
+ if (tbr.hasRewardAccumulation()) {
+ result = result && inherited.getSpecification().isRewardAccumulationAllowed();
+ }
}
}
return result;
@@ -140,12 +147,15 @@ namespace storm {
if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
result = result && !f.getSubformula().isPathFormula();
}
+ result = result && !f.hasRewardAccumulation();
} else if (f.isReachabilityRewardFormula()) {
result = result && inherited.getSpecification().areReachabilityRewardFormulasAllowed();
result = result && f.getSubformula().isStateFormula();
+ result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
} else if (f.isReachabilityTimeFormula()) {
result = result && inherited.getSpecification().areReachbilityTimeFormulasAllowed();
result = result && f.getSubformula().isStateFormula();
+ result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
}
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
return result;
@@ -250,6 +260,7 @@ namespace storm {
result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed());
result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula());
result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == RewardMeasureType::Expectation);
+
if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
} else {
@@ -258,9 +269,11 @@ namespace storm {
return result;
}
- boost::any FragmentChecker::visit(TotalRewardFormula const&, boost::any const& data) const {
+ boost::any FragmentChecker::visit(TotalRewardFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
- return inherited.getSpecification().areTotalRewardFormulasAllowed();
+ bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
+ result = result && inherited.getSpecification().areTotalRewardFormulasAllowed();
+ return result;
}
boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp
index cdcfc6ecd..9b5b8b17e 100644
--- a/src/storm/logic/FragmentSpecification.cpp
+++ b/src/storm/logic/FragmentSpecification.cpp
@@ -1,6 +1,7 @@
#include "storm/logic/FragmentSpecification.h"
#include <iostream>
+#include "storm/logic/RewardAccumulation.h"
namespace storm {
namespace logic {
@@ -161,6 +162,8 @@ namespace storm {
operatorAtTopLevelRequired = false;
multiObjectiveFormulaAtTopLevelRequired = false;
operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false;
+
+ rewardAccumulation = false;
}
FragmentSpecification FragmentSpecification::copy() const {
@@ -564,5 +567,15 @@ namespace storm {
return *this;
}
+ bool FragmentSpecification::isRewardAccumulationAllowed() const {
+ return rewardAccumulation;
+ }
+
+ FragmentSpecification& FragmentSpecification::setRewardAccumulationAllowed(bool newValue) {
+ rewardAccumulation = newValue;
+ return *this;
+ }
+
+
}
}
diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h
index d90ebd5fb..012716c78 100644
--- a/src/storm/logic/FragmentSpecification.h
+++ b/src/storm/logic/FragmentSpecification.h
@@ -1,8 +1,14 @@
#ifndef STORM_LOGIC_FRAGMENTSPECIFICATION_H_
#define STORM_LOGIC_FRAGMENTSPECIFICATION_H_
+#include <map>
+#include <string>
+
namespace storm {
namespace logic {
+
+ class RewardAccumulation;
+
class FragmentSpecification {
public:
FragmentSpecification();
@@ -139,6 +145,10 @@ namespace storm {
bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const;
FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue);
+ bool isRewardAccumulationAllowed() const;
+ FragmentSpecification& setRewardAccumulationAllowed(bool newValue);
+
+
FragmentSpecification& setOperatorsAllowed(bool newValue);
FragmentSpecification& setTimeAllowed(bool newValue);
FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue);
@@ -195,6 +205,8 @@ namespace storm {
bool operatorAtTopLevelRequired;
bool multiObjectiveFormulaAtTopLevelRequired;
bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
+
+ bool rewardAccumulation;
};
// Propositional.
diff --git a/src/storm/logic/RewardAccumulation.cpp b/src/storm/logic/RewardAccumulation.cpp
new file mode 100644
index 000000000..32065268a
--- /dev/null
+++ b/src/storm/logic/RewardAccumulation.cpp
@@ -0,0 +1,51 @@
+#include "storm/logic/RewardAccumulation.h"
+
+namespace storm {
+ namespace logic {
+
+ RewardAccumulation::RewardAccumulation(bool steps, bool time, bool exit) : steps(steps), time(time), exit(exit){
+ // Intentionally left empty
+ }
+
+ bool RewardAccumulation::isStepsSet() const {
+ return steps;
+ }
+
+ bool RewardAccumulation::isTimeSet() const {
+ return time;
+ }
+
+ bool RewardAccumulation::isExitSet() const {
+ return exit;
+ }
+
+ bool RewardAccumulation::isEmpty() const {
+ return !isStepsSet() && !isTimeSet() && !isExitSet();
+ }
+
+ std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc) {
+ bool hasEntry = false;
+ if (acc.isStepsSet()) {
+ out << "steps";
+ hasEntry = true;
+ }
+ if (acc.isTimeSet()) {
+ if (hasEntry) {
+ out << ", ";
+ }
+ out << "time";
+ hasEntry = true;
+ }
+ if (acc.isExitSet()) {
+ if (hasEntry) {
+ out << ", ";
+ }
+ out << "exit";
+ hasEntry = true;
+ }
+
+ return out;
+ }
+
+ }
+}
diff --git a/src/storm/logic/RewardAccumulation.h b/src/storm/logic/RewardAccumulation.h
new file mode 100644
index 000000000..4f8a50b29
--- /dev/null
+++ b/src/storm/logic/RewardAccumulation.h
@@ -0,0 +1,27 @@
+#pragma once
+#include <iostream>
+
+namespace storm {
+ namespace logic {
+
+ class RewardAccumulation {
+ public:
+ RewardAccumulation(bool steps, bool time, bool exit);
+ RewardAccumulation(RewardAccumulation const& other) = default;
+
+ bool isStepsSet() const; // If set, choice rewards and transition rewards are accumulated upon taking the transition
+ bool isTimeSet() const; // If set, state rewards are accumulated over time (assuming 0 time passes in discrete-time model states)
+ bool isExitSet() const; // If set, state rewards are accumulated upon exiting the state
+
+ // Returns true iff accumulation for all types of reward is disabled.
+ bool isEmpty() const;
+
+ private:
+ bool time, steps, exit;
+ };
+
+ std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc);
+
+ }
+}
+
diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp
new file mode 100644
index 000000000..710f959f1
--- /dev/null
+++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp
@@ -0,0 +1,153 @@
+#include "storm/logic/RewardAccumulationEliminationVisitor.h"
+#include "storm/logic/Formulas.h"
+
+#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/traverser/AssignmentsFinder.h"
+#include "storm/utility/macros.h"
+
+#include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+ namespace logic {
+
+ RewardAccumulationEliminationVisitor::RewardAccumulationEliminationVisitor(storm::jani::Model const& model) : model(model) {
+ // Intentionally left empty
+ }
+
+ std::shared_ptr<Formula> RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const {
+ boost::any result = f.accept(*this, boost::any());
+ return boost::any_cast<std::shared_ptr<Formula>>(result);
+ }
+
+ void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(std::vector<storm::jani::Property>& properties) const {
+ for (auto& p : properties) {
+ auto formula = eliminateRewardAccumulations(*p.getFilter().getFormula());
+ auto states = eliminateRewardAccumulations(*p.getFilter().getStatesFormula());
+ storm::jani::FilterExpression fe(formula, p.getFilter().getFilterType(), states);
+ p = storm::jani::Property(p.getName(), storm::jani::FilterExpression(formula, p.getFilter().getFilterType(), states), p.getComment());
+ }
+ }
+
+ boost::any RewardAccumulationEliminationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
+ std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
+ std::vector<TimeBoundReference> timeBoundReferences;
+ for (uint64_t i = 0; i < f.getDimension(); ++i) {
+ if (f.hasLowerBound(i)) {
+ lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i)));
+ } else {
+ lowerBounds.emplace_back();
+ }
+ if (f.hasUpperBound(i)) {
+ upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i)));
+ } else {
+ upperBounds.emplace_back();
+ }
+ storm::logic::TimeBoundReference tbr = f.getTimeBoundReference(i);
+ if (tbr.hasRewardAccumulation() && canEliminate(tbr.getRewardAccumulation(), tbr.getRewardName())) {
+ // Eliminate accumulation
+ tbr = storm::logic::TimeBoundReference(tbr.getRewardName(), boost::none);
+ }
+ timeBoundReferences.push_back(std::move(tbr));
+ }
+ if (f.hasMultiDimensionalSubformulas()) {
+ std::vector<std::shared_ptr<Formula const>> leftSubformulas, rightSubformulas;
+ for (uint64_t i = 0; i < f.getDimension(); ++i) {
+ leftSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula(i).accept(*this, data)));
+ rightSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula(i).accept(*this, data)));
+ }
+ return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
+ } else {
+ std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
+ std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
+ 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::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.");
+ auto rewName = boost::any_cast<boost::optional<std::string>>(data);
+ if (f.hasRewardAccumulation() && !canEliminate(f.getRewardAccumulation(), rewName)) {
+ rewAcc = f.getRewardAccumulation();
+ }
+
+ std::vector<TimeBound> bounds;
+ std::vector<TimeBoundReference> timeBoundReferences;
+ for (uint64_t i = 0; i < f.getDimension(); ++i) {
+ bounds.emplace_back(TimeBound(f.isBoundStrict(i), f.getBound(i)));
+ storm::logic::TimeBoundReference tbr = f.getTimeBoundReference(i);
+ if (tbr.hasRewardAccumulation() && canEliminate(tbr.getRewardAccumulation(), tbr.getRewardName())) {
+ // Eliminate accumulation
+ tbr = storm::logic::TimeBoundReference(tbr.getRewardName(), boost::none);
+ }
+ timeBoundReferences.push_back(std::move(tbr));
+ }
+ return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, rewAcc));
+ }
+
+ 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));
+ if (f.hasRewardAccumulation()) {
+ if (f.isTimePathFormula()) {
+ if (model.isDiscreteTimeModel() && ((!f.getRewardAccumulation().isExitSet() && !f.getRewardAccumulation().isStepsSet()) || (f.getRewardAccumulation().isStepsSet() && f.getRewardAccumulation().isExitSet()))) {
+ return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
+ } else if (!model.isDiscreteTimeModel() && (!f.getRewardAccumulation().isTimeSet() || f.getRewardAccumulation().isExitSet() || f.getRewardAccumulation().isStepsSet())) {
+ return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
+ }
+ } else if (f.isRewardPathFormula()) {
+ 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);
+ if (!canEliminate(f.getRewardAccumulation(), rewName)) {
+ return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
+ }
+ }
+ }
+ 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 {
+ 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()));
+ }
+
+ 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<boost::optional<std::string>>(data);
+ if (f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) {
+ return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>());
+ } else {
+ 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 {
+ STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with for unique reward model.");
+ storm::jani::AssignmentsFinder::ResultType assignmentKinds;
+ STORM_LOG_THROW(model.hasGlobalVariable(rewardModelName.get()), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with name " << rewardModelName.get() << ".");
+ storm::jani::Variable const& transientVar = model.getGlobalVariable(rewardModelName.get());
+ if (transientVar.getInitExpression().containsVariables() || !storm::utility::isZero(transientVar.getInitExpression().evaluateAsRational())) {
+ assignmentKinds.hasLocationAssignment = true;
+ assignmentKinds.hasEdgeAssignment = true;
+ assignmentKinds.hasEdgeDestinationAssignment = true;
+ }
+ assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar);
+ if ((assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment) && !accumulation.isStepsSet()) {
+ return false;
+ }
+ if (assignmentKinds.hasLocationAssignment) {
+ if (model.isDiscreteTimeModel()) {
+ if (!accumulation.isExitSet()) {
+ return false;
+ }
+ // accumulating over time in discrete time models has no effect, i.e., the value of accumulation.isTimeSet() does not matter here.
+ } else {
+ if (accumulation.isExitSet() || !accumulation.isTimeSet()) {
+ return false;
+ }
+ }
+ }
+ return true;
+ }
+ }
+}
diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.h b/src/storm/logic/RewardAccumulationEliminationVisitor.h
new file mode 100644
index 000000000..0b77901d9
--- /dev/null
+++ b/src/storm/logic/RewardAccumulationEliminationVisitor.h
@@ -0,0 +1,39 @@
+#pragma once
+
+#include <unordered_map>
+#include <boost/optional.hpp>
+
+#include "storm/logic/CloneVisitor.h"
+#include "storm/logic/RewardAccumulation.h"
+#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
+
+namespace storm {
+ namespace logic {
+
+ class RewardAccumulationEliminationVisitor : public CloneVisitor {
+ public:
+ RewardAccumulationEliminationVisitor(storm::jani::Model const& model);
+
+ /*!
+ * Eliminates any reward accumulations of the formula, where the presence of the reward accumulation does not change the result of the formula
+ */
+ std::shared_ptr<Formula> eliminateRewardAccumulations(Formula const& f) const;
+
+ void eliminateRewardAccumulations(std::vector<storm::jani::Property>& properties) const;
+
+ virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
+
+
+ private:
+ bool canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const;
+
+ storm::jani::Model const& model;
+ };
+
+ }
+}
diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h
index 0bd6aba0c..ec9a753b0 100644
--- a/src/storm/logic/TimeBoundType.h
+++ b/src/storm/logic/TimeBoundType.h
@@ -1,5 +1,9 @@
#pragma once
+#include <boost/optional.hpp>
+
+#include "storm/logic/RewardAccumulation.h"
+
namespace storm {
namespace logic {
@@ -13,14 +17,15 @@ namespace storm {
class TimeBoundReference {
TimeBoundType type;
std::string rewardName;
-
+ boost::optional<RewardAccumulation> rewardAccumulation;
+
public:
explicit TimeBoundReference(TimeBoundType t) : type(t) {
// For rewards, use the other constructor.
assert(t != TimeBoundType::Reward);
}
- explicit TimeBoundReference(std::string const& rewardName) : type(TimeBoundType::Reward), rewardName(rewardName) {
+ explicit TimeBoundReference(std::string const& rewardName, boost::optional<RewardAccumulation> rewardAccumulation = boost::none) : type(TimeBoundType::Reward), rewardName(rewardName), rewardAccumulation(rewardAccumulation) {
assert(rewardName != ""); // Empty reward name is reserved.
}
@@ -44,6 +49,16 @@ namespace storm {
assert(isRewardBound());
return rewardName;
}
+
+ bool hasRewardAccumulation() const {
+ return rewardAccumulation.is_initialized();
+ }
+
+ RewardAccumulation const& getRewardAccumulation() const {
+ assert(isRewardBound());
+ return rewardAccumulation.get();
+ }
+
};
diff --git a/src/storm/logic/TotalRewardFormula.cpp b/src/storm/logic/TotalRewardFormula.cpp
index 18c79cd67..6136581a3 100644
--- a/src/storm/logic/TotalRewardFormula.cpp
+++ b/src/storm/logic/TotalRewardFormula.cpp
@@ -4,7 +4,7 @@
namespace storm {
namespace logic {
- TotalRewardFormula::TotalRewardFormula() {
+ TotalRewardFormula::TotalRewardFormula(boost::optional<RewardAccumulation> rewardAccumulation) : rewardAccumulation(rewardAccumulation) {
// Intentionally left empty.
}
@@ -16,6 +16,14 @@ namespace storm {
return true;
}
+ bool TotalRewardFormula::hasRewardAccumulation() const {
+ return rewardAccumulation.is_initialized();
+ }
+
+ RewardAccumulation const& TotalRewardFormula::getRewardAccumulation() const {
+ return rewardAccumulation.get();
+ }
+
boost::any TotalRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
return visitor.visit(*this, data);
}
diff --git a/src/storm/logic/TotalRewardFormula.h b/src/storm/logic/TotalRewardFormula.h
index 90caee9e7..a11fb3b03 100644
--- a/src/storm/logic/TotalRewardFormula.h
+++ b/src/storm/logic/TotalRewardFormula.h
@@ -1,15 +1,16 @@
#ifndef STORM_LOGIC_TOTALREWARDFORMULA_H_
#define STORM_LOGIC_TOTALREWARDFORMULA_H_
-#include <boost/variant.hpp>
+#include <boost/optional.hpp>
+#include "storm/logic/RewardAccumulation.h"
#include "storm/logic/PathFormula.h"
namespace storm {
namespace logic {
class TotalRewardFormula : public PathFormula {
public:
- TotalRewardFormula();
+ TotalRewardFormula(boost::optional<RewardAccumulation> rewardAccumulation = boost::none);
virtual ~TotalRewardFormula() {
// Intentionally left empty.
@@ -17,11 +18,15 @@ namespace storm {
virtual bool isTotalRewardFormula() const override;
virtual bool isRewardPathFormula() const override;
-
+ bool hasRewardAccumulation() const;
+ RewardAccumulation const& getRewardAccumulation() const;
+
virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
virtual std::ostream& writeToStream(std::ostream& out) const override;
-
+
+ private:
+ boost::optional<RewardAccumulation> rewardAccumulation;
};
}
}
diff --git a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp
index 7f45240d7..d49b864dd 100644
--- a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp
+++ b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp
@@ -93,7 +93,7 @@ namespace storm {
boost::any SyntacticalEqualityCheckVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
BaseExpression const& otherBaseExpression = boost::any_cast<std::reference_wrapper<BaseExpression const>>(data).get();
- if (otherBaseExpression.isBinaryBooleanFunctionExpression()) {
+ if (otherBaseExpression.isUnaryBooleanFunctionExpression()) {
UnaryBooleanFunctionExpression const& otherExpression = otherBaseExpression.asUnaryBooleanFunctionExpression();
bool result = expression.getOperatorType() == otherExpression.getOperatorType();
@@ -108,7 +108,7 @@ namespace storm {
boost::any SyntacticalEqualityCheckVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
BaseExpression const& otherBaseExpression = boost::any_cast<std::reference_wrapper<BaseExpression const>>(data).get();
- if (otherBaseExpression.isBinaryBooleanFunctionExpression()) {
+ if (otherBaseExpression.isUnaryNumericalFunctionExpression()) {
UnaryNumericalFunctionExpression const& otherExpression = otherBaseExpression.asUnaryNumericalFunctionExpression();
bool result = expression.getOperatorType() == otherExpression.getOperatorType();
diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index cc75d080e..62d2576cf 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -270,6 +270,10 @@ namespace storm {
return ConstEdges(it1, it2);
}
+ EdgeContainer const& Automaton::getEdgeContainer() const {
+ return edges;
+ }
+
void Automaton::addEdge(Edge const& edge) {
STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'.");
assert(validate());
diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h
index eb1362741..869f5cd09 100644
--- a/src/storm/storage/jani/Automaton.h
+++ b/src/storm/storage/jani/Automaton.h
@@ -192,6 +192,8 @@ namespace storm {
*/
ConstEdges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const;
+ EdgeContainer const& getEdgeContainer() const;
+
/*!
* Adds the template edge to the list of edges
*/
diff --git a/src/storm/storage/jani/EdgeContainer.cpp b/src/storm/storage/jani/EdgeContainer.cpp
index b7a9ca1ec..d735bc80d 100644
--- a/src/storm/storage/jani/EdgeContainer.cpp
+++ b/src/storm/storage/jani/EdgeContainer.cpp
@@ -121,8 +121,6 @@ namespace storm {
}
-
-
std::vector<Edge> & EdgeContainer::getConcreteEdges() {
return edges;
}
@@ -130,6 +128,10 @@ namespace storm {
std::vector<Edge> const& EdgeContainer::getConcreteEdges() const {
return edges;
}
+
+ TemplateEdgeContainer const& EdgeContainer::getTemplateEdges() const {
+ return templates;
+ }
std::set<uint64_t> EdgeContainer::getActionIndices() const {
std::set<uint64_t> result;
diff --git a/src/storm/storage/jani/EdgeContainer.h b/src/storm/storage/jani/EdgeContainer.h
index f4738e1e0..c2bdfe80c 100644
--- a/src/storm/storage/jani/EdgeContainer.h
+++ b/src/storm/storage/jani/EdgeContainer.h
@@ -95,6 +95,8 @@ namespace storm {
void clearConcreteEdges();
std::vector<Edge> const& getConcreteEdges() const;
std::vector<Edge> & getConcreteEdges();
+ TemplateEdgeContainer const& getTemplateEdges() const;
+
size_t size() const;
iterator begin();
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index 42bc15d62..cc45468c0 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -11,6 +11,7 @@
#include "storm/exceptions/InvalidJaniException.h"
#include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/storage/expressions/RationalLiteralExpression.h"
#include "storm/storage/expressions/IntegerLiteralExpression.h"
@@ -29,6 +30,7 @@
#include "storm/storage/jani/AutomatonComposition.h"
#include "storm/storage/jani/ParallelComposition.h"
#include "storm/storage/jani/Property.h"
+#include "storm/storage/jani/traverser/AssignmentsFinder.h"
namespace storm {
namespace jani {
@@ -153,9 +155,58 @@ namespace storm {
return iDecl;
}
- modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model) {
+ modernjson::json FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const {
+
+ storm::jani::Variable const& transientVar = model.getGlobalVariable(rewardModelName);
+ storm::jani::AssignmentsFinder::ResultType assignmentKinds;
+ STORM_LOG_THROW(model.hasGlobalVariable(rewardModelName), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with name " << rewardModelName << ".");
+ if (transientVar.getInitExpression().containsVariables() || !storm::utility::isZero(transientVar.getInitExpression().evaluateAsRational())) {
+ assignmentKinds.hasLocationAssignment = true;
+ assignmentKinds.hasEdgeAssignment = true;
+ assignmentKinds.hasEdgeDestinationAssignment = true;
+ }
+ assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar);
+
+ bool steps = rewardAccumulation.isStepsSet() && (assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment);
+ bool time = rewardAccumulation.isTimeSet() && !model.isDiscreteTimeModel() && assignmentKinds.hasLocationAssignment;
+ bool exit = rewardAccumulation.isExitSet() && assignmentKinds.hasLocationAssignment;
+ return constructRewardAccumulation(storm::logic::RewardAccumulation(steps, time, exit));
+ }
+
+ modernjson::json FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const {
+ std::vector<std::string> res;
+ if (rewardAccumulation.isStepsSet()) {
+ res.push_back("steps");
+ }
+ if (rewardAccumulation.isTimeSet()) {
+ res.push_back("time");
+ }
+ if (rewardAccumulation.isExitSet()) {
+ stateExitRewards = true;
+ res.push_back("exit");
+ }
+ return res;
+ }
+
+ modernjson::json FormulaToJaniJson::constructStandardRewardAccumulation(std::string const& rewardModelName) const {
+ if (model.isDiscreteTimeModel()) {
+ return constructRewardAccumulation(storm::logic::RewardAccumulation(true, false, true), rewardModelName);
+ } else {
+ return constructRewardAccumulation(storm::logic::RewardAccumulation(true, true, false), rewardModelName);
+ }
+ }
+
+ modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model, std::set<std::string>& modelFeatures) {
FormulaToJaniJson translator(model);
- return boost::any_cast<modernjson::json>(formula.accept(translator));
+ auto result = boost::any_cast<modernjson::json>(formula.accept(translator));
+ if (translator.containsStateExitRewards()) {
+ modelFeatures.insert("state-exit-rewards");
+ }
+ return result;
+ }
+
+ bool FormulaToJaniJson::containsStateExitRewards() const {
+ return stateExitRewards;
}
boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const&) const {
@@ -209,13 +260,11 @@ namespace storm {
} else if(tbr.isRewardBound()) {
modernjson::json rewbound;
rewbound["exp"] = tbr.getRewardName();
- std::vector<std::string> accvec;
- if (model.isDiscreteTimeModel()) {
- accvec.push_back("steps");
+ if (tbr.hasRewardAccumulation()) {
+ rewbound["accumulate"] = constructRewardAccumulation(tbr.getRewardAccumulation(), tbr.getRewardName());
} else {
- accvec.push_back("time");
+ rewbound["accumulate"] = constructStandardRewardAccumulation(tbr.getRewardName());
}
- rewbound["accumulate"] = modernjson::json(accvec);
rewbound["bounds"] = propertyInterval;
rewardBounds.push_back(std::move(rewbound));
} else {
@@ -249,12 +298,14 @@ namespace storm {
boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
- std::vector<std::string> accvec;
- if (model.isDiscreteTimeModel()) {
- accvec.push_back("steps");
- } else {
- accvec.push_back("time");
+
+ // Create standard reward accumulation for time operator formulas.
+ storm::logic::RewardAccumulation rewAcc(model.isDiscreteTimeModel(), !model.isDiscreteTimeModel(), false);
+ if (f.getSubformula().isEventuallyFormula() && f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) {
+ rewAcc = f.getSubformula().asEventuallyFormula().getRewardAccumulation();
}
+ auto rewAccJson = constructRewardAccumulation(rewAcc);
+
if(f.hasBound()) {
auto bound = f.getBound();
opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
@@ -270,7 +321,7 @@ namespace storm {
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
}
opDecl["left"]["exp"] = modernjson::json(1);
- opDecl["left"]["accumulate"] = modernjson::json(accvec);
+ opDecl["left"]["accumulate"] = rewAccJson;
opDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables());
} else {
if(f.hasOptimalityType()) {
@@ -286,7 +337,7 @@ namespace storm {
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
}
opDecl["exp"] = modernjson::json(1);
- opDecl["accumulate"] = modernjson::json(accvec);
+ opDecl["accumulate"] = rewAccJson;
}
return opDecl;
}
@@ -403,13 +454,11 @@ namespace storm {
boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
- std::vector<std::string> accvec;
+
std::string instantName;
if (model.isDiscreteTimeModel()) {
- accvec.push_back("steps");
instantName = "step-instant";
} else {
- accvec.push_back("time");
instantName = "time-instant";
}
@@ -439,21 +488,29 @@ namespace storm {
}
if (f.getSubformula().isEventuallyFormula()) {
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
+ if (f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) {
+ opDecl["left"]["accumulate"] = constructRewardAccumulation(f.getSubformula().asEventuallyFormula().getRewardAccumulation(), rewardModelName);
+ } else {
+ opDecl["left"]["accumulate"] = constructStandardRewardAccumulation(rewardModelName);
+ }
} else if (f.getSubformula().isCumulativeRewardFormula()) {
+ // TODO: support for reward bounded formulas
+ STORM_LOG_WARN_COND(!f.getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound(), "Export for reward bounded cumulative reward formulas currently unsupported.");
opDecl["left"][instantName] = buildExpression(f.getSubformula().asCumulativeRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables());
+ if (f.getSubformula().asCumulativeRewardFormula().hasRewardAccumulation()) {
+ opDecl["left"]["accumulate"] = constructRewardAccumulation(f.getSubformula().asCumulativeRewardFormula().getRewardAccumulation(), rewardModelName);
+ } else {
+ opDecl["left"]["accumulate"] = constructStandardRewardAccumulation(rewardModelName);
+ }
} else if (f.getSubformula().isInstantaneousRewardFormula()) {
opDecl["left"][instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables());
}
STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion");
opDecl["left"]["exp"] = rewardModelName;
- if (f.getSubformula().isReachabilityRewardFormula() || f.getSubformula().isCumulativeRewardFormula()) {
- opDecl["left"]["accumulate"] = modernjson::json(accvec);
- }
opDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables());
} else {
if (f.hasOptimalityType()) {
opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
-
} else {
// TODO add checks
opDecl["op"] = "Emin";
@@ -461,16 +518,24 @@ namespace storm {
if (f.getSubformula().isEventuallyFormula()) {
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
+ if (f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) {
+ opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asEventuallyFormula().getRewardAccumulation(), rewardModelName);
+ } else {
+ opDecl["accumulate"] = constructStandardRewardAccumulation(rewardModelName);
+ }
} else if (f.getSubformula().isCumulativeRewardFormula()) {
+ // TODO: support for reward bounded formulas
+ STORM_LOG_WARN_COND(!f.getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound(), "Export for reward bounded cumulative reward formulas currently unsupported.");
opDecl[instantName] = buildExpression(f.getSubformula().asCumulativeRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables());
+ if (f.getSubformula().asCumulativeRewardFormula().hasRewardAccumulation()) {
+ opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asCumulativeRewardFormula().getRewardAccumulation(), rewardModelName);
+ } else {
+ opDecl["accumulate"] = constructStandardRewardAccumulation(rewardModelName);
+ }
} else if (f.getSubformula().isInstantaneousRewardFormula()) {
opDecl[instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables());
}
-
opDecl["exp"] = rewardModelName;
- if (f.getSubformula().isReachabilityRewardFormula() || f.getSubformula().isCumulativeRewardFormula()) {
- opDecl["accumulate"] = modernjson::json(accvec);
- }
}
return opDecl;
}
@@ -628,21 +693,27 @@ namespace storm {
return modernjson::json(expression.getValueAsDouble());
}
- void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid) {
+ void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid, bool compact) {
std::ofstream stream;
storm::utility::openFile(filepath, stream);
- toStream(janiModel, formulas, stream, checkValid);
+ toStream(janiModel, formulas, stream, checkValid, compact);
storm::utility::closeFile(stream);
}
- void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& os, bool checkValid) {
+ void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& os, bool checkValid, bool compact) {
if(checkValid) {
janiModel.checkValid();
}
JsonExporter exporter;
- exporter.convertModel(janiModel);
+ exporter.convertModel(janiModel, !compact);
exporter.convertProperties(formulas, janiModel);
- os << exporter.finalize().dump(4) << std::endl;
+ if (compact) {
+ // Dump without line breaks/indents
+ os << exporter.finalize().dump() << std::endl;
+ } else {
+ // Dump with line breaks and indention with 4 spaces
+ os << exporter.finalize().dump(4) << std::endl;
+ }
}
modernjson::json buildActionArray(std::vector<storm::jani::Action> const& actions) {
@@ -838,8 +909,8 @@ namespace storm {
return modernjson::json(automataDeclarations);
}
-
void JsonExporter::convertModel(storm::jani::Model const& janiModel, bool commentExpressions) {
+ modelFeatures = {"derived-operators"};
jsonStruct["jani-version"] = janiModel.getJaniVersion();
jsonStruct["name"] = janiModel.getName();
jsonStruct["type"] = to_string(janiModel.getModelType());
@@ -849,14 +920,8 @@ namespace storm {
jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction(), janiModel.getConstants(), janiModel.getGlobalVariables());
jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), commentExpressions);
jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition());
- std::vector<std::string> standardFeatureVector = {"derived-operators"};
- jsonStruct["features"] = standardFeatureVector;
-
}
-
-
-
std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) {
switch(ft) {
case storm::modelchecker::FilterType::MIN:
@@ -885,12 +950,12 @@ namespace storm {
}
}
- modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model) {
+ modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, std::set<std::string>& modelFeatures) {
modernjson::json propDecl;
propDecl["states"]["op"] = "initial";
propDecl["op"] = "filter";
propDecl["fun"] = janiFilterTypeString(fe.getFilterType());
- propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), model);
+ propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), model, modelFeatures);
return propDecl;
}
@@ -901,7 +966,7 @@ namespace storm {
for(auto const& f : formulas) {
modernjson::json propDecl;
propDecl["name"] = f.getName();
- propDecl["expression"] = convertFilterExpression(f.getFilter(), model);
+ propDecl["expression"] = convertFilterExpression(f.getFilter(), model, modelFeatures);
++index;
properties.push_back(propDecl);
}
diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h
index 1bf098bca..1f1a49db8 100644
--- a/src/storm/storage/jani/JSONExporter.h
+++ b/src/storm/storage/jani/JSONExporter.h
@@ -41,7 +41,8 @@ namespace storm {
class FormulaToJaniJson : public storm::logic::FormulaVisitor {
public:
- static modernjson::json translate(storm::logic::Formula const& formula, storm::jani::Model const& modeln);
+ static modernjson::json translate(storm::logic::Formula const& formula, storm::jani::Model const& model, std::set<std::string>& modelFeatures);
+ bool containsStateExitRewards() const; // Returns true iff the previously translated formula contained state exit rewards
virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const;
@@ -64,19 +65,24 @@ namespace storm {
virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const;
private:
- FormulaToJaniJson(storm::jani::Model const& model) : model(model) { }
+ FormulaToJaniJson(storm::jani::Model const& model) : model(model), stateExitRewards(false) { }
modernjson::json constructPropertyInterval(boost::optional<storm::expressions::Expression> const& lower, boost::optional<bool> const& lowerExclusive, boost::optional<storm::expressions::Expression> const& upper, boost::optional<bool> const& upperExclusive) const;
+
+ modernjson::json constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const;
+ modernjson::json constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const;
+ modernjson::json constructStandardRewardAccumulation(std::string const& rewardModelName) const;
storm::jani::Model const& model;
+ mutable bool stateExitRewards;
};
class JsonExporter {
JsonExporter() = default;
public:
- static void toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid = true);
- static void toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& ostream, bool checkValid = false);
+ static void toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid = true, bool compact = false);
+ static void toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& ostream, bool checkValid = false, bool compact = false);
private:
@@ -85,11 +91,13 @@ namespace storm {
void appendVariableDeclaration(storm::jani::Variable const& variable);
modernjson::json finalize() {
+ std::vector<std::string> featureVector(modelFeatures.begin(), modelFeatures.end());
+ jsonStruct["features"] = featureVector;
return jsonStruct;
}
modernjson::json jsonStruct;
-
+ std::set<std::string> modelFeatures;
};
}
diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp
index 7d1967ff7..9c622fe2b 100644
--- a/src/storm/storage/jani/OrderedAssignments.cpp
+++ b/src/storm/storage/jani/OrderedAssignments.cpp
@@ -27,19 +27,17 @@ namespace storm {
bool OrderedAssignments::add(Assignment const& assignment, bool addToExisting) {
// If the element is contained in this set of assignment, nothing needs to be added.
- if (this->contains(assignment)) {
+ if (!addToExisting && this->contains(assignment)) {
return false;
}
// Otherwise, we find the spot to insert it.
auto it = lowerBound(assignment, allAssignments);
-
- if (it != allAssignments.end()) {
- if ((!addToExisting || !assignment.getExpressionVariable().hasNumericalType())) {
- STORM_LOG_THROW(assignment.getExpressionVariable() != (*it)->getExpressionVariable(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression() << "') to variable '" << (*it)->getVariable().getName() << "' already exists.");
- } else if (addToExisting && assignment.getExpressionVariable().hasNumericalType()) {
- (*it)->setAssignedExpression((*it)->getAssignedExpression() + assignment.getAssignedExpression());
- }
+
+ // Check if an assignment to this variable is already present
+ if (it != allAssignments.end() && assignment.getExpressionVariable() == (*it)->getExpressionVariable()) {
+ STORM_LOG_THROW(addToExisting && assignment.getExpressionVariable().hasNumericalType(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression() << "') to variable '" << (*it)->getVariable().getName() << "' already exists.");
+ (*it)->setAssignedExpression((*it)->getAssignedExpression() + assignment.getAssignedExpression());
} else {
// Finally, insert the new element in the correct vectors.
auto elementToInsert = std::make_shared<Assignment>(assignment);
diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
new file mode 100644
index 000000000..f1450d004
--- /dev/null
+++ b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
@@ -0,0 +1,47 @@
+#include "storm/storage/jani/traverser/AssignmentsFinder.h"
+
+
+namespace storm {
+ namespace jani {
+
+ AssignmentsFinder::ResultType AssignmentsFinder::find(Model const& model, Variable const& variable) {
+ ResultType res;
+ res.hasLocationAssignment = false;
+ res.hasEdgeAssignment = false;
+ res.hasEdgeDestinationAssignment = false;
+ JaniTraverser::traverse(model, std::make_pair(&variable, &res));
+ return res;
+ }
+
+ void AssignmentsFinder::traverse(Location const& location, boost::any const& data) const {
+ auto resVar = boost::any_cast<std::pair<Variable const*, ResultType*>>(data);
+ for (auto const& assignment : location.getAssignments()) {
+ if (assignment.getVariable() == *resVar.first) {
+ resVar.second->hasLocationAssignment = true;
+ }
+ }
+ JaniTraverser::traverse(location, data);
+ }
+
+ void AssignmentsFinder::traverse(TemplateEdge const& templateEdge, boost::any const& data) const {
+ auto resVar = boost::any_cast<std::pair<Variable const*, ResultType*>>(data);
+ for (auto const& assignment : templateEdge.getAssignments()) {
+ if (assignment.getVariable() == *resVar.first) {
+ resVar.second->hasEdgeAssignment = true;
+ }
+ }
+ JaniTraverser::traverse(templateEdge, data);
+ }
+
+ void AssignmentsFinder::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const {
+ auto resVar = boost::any_cast<std::pair<Variable const*, ResultType*>>(data);
+ for (auto const& assignment : templateEdgeDestination.getOrderedAssignments()) {
+ if (assignment.getVariable() == *resVar.first) {
+ resVar.second->hasEdgeDestinationAssignment = true;
+ }
+ }
+ JaniTraverser::traverse(templateEdgeDestination, data);
+ }
+ }
+}
+
diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.h b/src/storm/storage/jani/traverser/AssignmentsFinder.h
new file mode 100644
index 000000000..2a2d2cdd0
--- /dev/null
+++ b/src/storm/storage/jani/traverser/AssignmentsFinder.h
@@ -0,0 +1,29 @@
+#pragma once
+
+
+#include <boost/any.hpp>
+
+#include "storm/storage/jani/traverser/JaniTraverser.h"
+
+namespace storm {
+ namespace jani {
+ class AssignmentsFinder : public JaniTraverser {
+ public:
+
+ struct ResultType {
+ bool hasLocationAssignment, hasEdgeAssignment, hasEdgeDestinationAssignment;
+ };
+
+ AssignmentsFinder() = default;
+
+ ResultType find(Model const& model, Variable const& variable);
+
+ virtual ~AssignmentsFinder() = default;
+
+ virtual void traverse(Location const& location, boost::any const& data) const override;
+ virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const override;
+ virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const override;
+ };
+ }
+}
+
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp
new file mode 100644
index 000000000..2461792b5
--- /dev/null
+++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp
@@ -0,0 +1,138 @@
+#include "storm/storage/jani/traverser/JaniTraverser.h"
+
+
+namespace storm {
+ namespace jani {
+ void JaniTraverser::traverse(Model const& model, boost::any const& data) const {
+ for (auto const& act : model.getActions()) {
+ traverse(act, data);
+ }
+ for (auto const& c : model.getConstants()) {
+ traverse(c, data);
+ }
+ traverse(model.getGlobalVariables(), data);
+ for (auto const& aut : model.getAutomata()) {
+ traverse(aut, data);
+ }
+ if (model.hasInitialStatesRestriction()) {
+ traverse(model.getInitialStatesRestriction(), data);
+ }
+ }
+
+ void JaniTraverser::traverse(Action const& action, boost::any const& data) const {
+ // Intentionally left empty.
+ }
+
+ void JaniTraverser::traverse(Automaton const& automaton, boost::any const& data) const {
+ traverse(automaton.getVariables(), data);
+ for (auto const& loc : automaton.getLocations()) {
+ traverse(loc, data);
+ }
+ traverse(automaton.getEdgeContainer(), data);
+ if (automaton.hasInitialStatesRestriction()) {
+ traverse(automaton.getInitialStatesRestriction(), data);
+ }
+ }
+
+ void JaniTraverser::traverse(Constant const& constant, boost::any const& data) const {
+ if (constant.isDefined()) {
+ traverse(constant.getExpression(), data);
+ }
+ }
+
+ void JaniTraverser::traverse(VariableSet const& variableSet, boost::any const& data) const {
+ for (auto const& v : variableSet.getBooleanVariables()) {
+ traverse(v, data);
+ }
+ for (auto const& v : variableSet.getBoundedIntegerVariables()) {
+ traverse(v, data);
+ }
+ for (auto const& v : variableSet.getUnboundedIntegerVariables()) {
+ traverse(v, data);
+ }
+ for (auto const& v : variableSet.getRealVariables()) {
+ traverse(v, data);
+ }
+ }
+
+ void JaniTraverser::traverse(Location const& location, boost::any const& data) const {
+ traverse(location.getAssignments(), data);
+ }
+
+ void JaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) const {
+ if (variable.hasInitExpression()) {
+ traverse(variable.getInitExpression(), data);
+ }
+ }
+
+ void JaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any const& data) const {
+ if (variable.hasInitExpression()) {
+ traverse(variable.getInitExpression(), data);
+ }
+ traverse(variable.getLowerBound(), data);
+ traverse(variable.getUpperBound(), data);
+ }
+
+ void JaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const {
+ if (variable.hasInitExpression()) {
+ traverse(variable.getInitExpression(), data);
+ }
+ }
+
+ void JaniTraverser::traverse(RealVariable const& variable, boost::any const& data) const {
+ if (variable.hasInitExpression()) {
+ traverse(variable.getInitExpression(), data);
+ }
+ }
+
+ void JaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) const {
+ for (auto const& templateEdge : edgeContainer.getTemplateEdges()) {
+ traverse(*templateEdge, data);
+ }
+ for (auto const& concreteEdge : edgeContainer.getConcreteEdges()) {
+ traverse(concreteEdge, data);
+ }
+ }
+
+ void JaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any const& data) const {
+ traverse(templateEdge.getGuard(), data);
+ for (auto const& dest : templateEdge.getDestinations()) {
+ traverse(dest, data);
+ }
+ traverse(templateEdge.getAssignments(), data);
+ }
+
+ void JaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const {
+ traverse(templateEdgeDestination.getOrderedAssignments(), data);
+ }
+
+ void JaniTraverser::traverse(Edge const& edge, boost::any const& data) const {
+ if (edge.hasRate()) {
+ traverse(edge.getRate(), data);
+ }
+ for (auto const& dest : edge.getDestinations()) {
+ traverse(dest, data);
+ }
+ }
+
+ void JaniTraverser::traverse(EdgeDestination const& edgeDestination, boost::any const& data) const {
+ traverse(edgeDestination.getProbability(), data);
+ }
+
+ void JaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const {
+ for (auto const& assignment : orderedAssignments) {
+ traverse(assignment, data);
+ }
+ }
+
+ void JaniTraverser::traverse(Assignment const& assignment, boost::any const& data) const {
+ traverse(assignment.getAssignedExpression(), data);
+ }
+
+ void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const {
+ // intentionally left empty.
+ }
+
+ }
+}
+
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.h b/src/storm/storage/jani/traverser/JaniTraverser.h
new file mode 100644
index 000000000..905ad0208
--- /dev/null
+++ b/src/storm/storage/jani/traverser/JaniTraverser.h
@@ -0,0 +1,36 @@
+#pragma once
+
+
+#include <boost/any.hpp>
+
+#include "storm/storage/jani/Model.h"
+
+namespace storm {
+ namespace jani {
+ class JaniTraverser {
+ public:
+ virtual ~JaniTraverser() = default;
+
+ virtual void traverse(Model const& model, boost::any const& data) const;
+
+ virtual void traverse(Action const& action, boost::any const& data) const;
+ virtual void traverse(Automaton const& automaton, boost::any const& data) const;
+ virtual void traverse(Constant const& constant, boost::any const& data) const;
+ virtual void traverse(VariableSet const& variableSet, boost::any const& data) const;
+ virtual void traverse(Location const& location, boost::any const& data) const;
+ virtual void traverse(BooleanVariable const& variable, boost::any const& data) const;
+ virtual void traverse(BoundedIntegerVariable const& variable, boost::any const& data) const;
+ virtual void traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const;
+ virtual void traverse(RealVariable const& variable, boost::any const& data) const;
+ virtual void traverse(EdgeContainer const& edgeContainer, boost::any const& data) const;
+ virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const;
+ virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const;
+ virtual void traverse(Edge const& edge, boost::any const& data) const;
+ virtual void traverse(EdgeDestination const& edgeDestination, boost::any const& data) const;
+ virtual void traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const;
+ virtual void traverse(Assignment const& assignment, boost::any const& data) const;
+ virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) const;
+ };
+ }
+}
+