diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 617e75ecc..737c80ba1 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -71,15 +71,20 @@ namespace storm { if (ioSettings.isJaniPropertiesSet()) { if (ioSettings.areJaniPropertiesSelected()) { + // Make sure to preserve the provided order for (auto const& propName : ioSettings.getSelectedJaniProperties()) { - auto propertyIt = janiPropertyInput.find(propName); - STORM_LOG_THROW(propertyIt != janiPropertyInput.end(), storm::exceptions::InvalidArgumentException, "No JANI property with name '" << propName << "' is known."); - input.properties.emplace_back(propertyIt->second); + bool found = false; + for (auto const& property : janiPropertyInput) { + if (property.getName() == propName) { + input.properties.emplace_back(property); + found = true; + break; + } + } + STORM_LOG_THROW(found, storm::exceptions::InvalidArgumentException, "No JANI property with name '" << propName << "' is known."); } } else { - for (auto const& property : janiPropertyInput) { - input.properties.emplace_back(property.second); - } + input.properties = janiPropertyInput; } } } diff --git a/src/storm-parsers/api/model_descriptions.cpp b/src/storm-parsers/api/model_descriptions.cpp index 16419945d..1173651c0 100644 --- a/src/storm-parsers/api/model_descriptions.cpp +++ b/src/storm-parsers/api/model_descriptions.cpp @@ -27,15 +27,19 @@ namespace storm { // Add derived-operators and state-exit-rewards as these can be handled by all model builders features.add(storm::jani::ModelFeature::DerivedOperators); features.add(storm::jani::ModelFeature::StateExitRewards); - return parseJaniModel(filename, features); + auto parsedResult = parseJaniModel(filename, features); + std::map propertyMap; + for (auto const& property : parsedResult.second) { + propertyMap.emplace(property.getName(), property); + } + return std::make_pair(std::move(parsedResult.first), std::move(propertyMap)); } - std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures) { - std::pair> modelAndFormulae = storm::parser::JaniParser::parse(filename); + std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures) { + std::pair> modelAndFormulae = storm::parser::JaniParser::parse(filename); modelAndFormulae.first.checkValid(); - // TODO: properties - auto nonEliminatedFeatures = modelAndFormulae.first.restrictToFeatures(allowedFeatures); + auto nonEliminatedFeatures = modelAndFormulae.first.restrictToFeatures(allowedFeatures, modelAndFormulae.second); STORM_LOG_THROW(nonEliminatedFeatures.empty(), storm::exceptions::NotSupportedException, "The used model feature(s) " << nonEliminatedFeatures.toString() << " is/are not in the list of allowed features."); return modelAndFormulae; } diff --git a/src/storm-parsers/api/model_descriptions.h b/src/storm-parsers/api/model_descriptions.h index e23cf7c33..32bf7aba9 100644 --- a/src/storm-parsers/api/model_descriptions.h +++ b/src/storm-parsers/api/model_descriptions.h @@ -18,7 +18,6 @@ namespace storm { storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false, bool simplify = true); std::pair> parseJaniModel(std::string const& filename); - std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures); - + std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures); } } diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 202a8931e..c7683ee4e 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -68,7 +68,7 @@ namespace storm { return static_cast(num); } - std::pair> JaniParser::parse(std::string const& path) { + std::pair> JaniParser::parse(std::string const& path) { JaniParser parser; parser.readFile(path); return parser.parseModel(); @@ -85,7 +85,7 @@ namespace storm { storm::utility::closeFile(file); } - std::pair> JaniParser::parseModel(bool parseProperties) { + std::pair> JaniParser::parseModel(bool parseProperties) { //jani-version STORM_LOG_THROW(parsedStructure.count("jani-version") == 1, storm::exceptions::InvalidJaniException, "Jani-version must be given exactly once."); uint64_t version = getUnsignedInt(parsedStructure.at("jani-version"), "jani version"); @@ -200,7 +200,7 @@ namespace storm { // Parse properties storm::logic::RewardAccumulationEliminationVisitor rewAccEliminator(model); STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given"); - std::map properties; + std::vector properties; if (parseProperties && parsedStructure.count("properties") == 1) { STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array"); for(auto const& propertyEntry : parsedStructure.at("properties")) { @@ -208,7 +208,7 @@ namespace storm { auto prop = this->parseProperty(propertyEntry, scope.refine("property[" + std::to_string(properties.size()) + "]")); // Eliminate reward accumulations as much as possible rewAccEliminator.eliminateRewardAccumulations(prop); - properties.emplace(prop.getName(), prop); + properties.push_back(prop); } catch (storm::exceptions::NotSupportedException const& ex) { STORM_LOG_WARN("Cannot handle property: " << ex.what()); } catch (storm::exceptions::NotImplementedException const& ex) { diff --git a/src/storm-parsers/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h index 4e7489b32..56174bd44 100644 --- a/src/storm-parsers/parser/JaniParser.h +++ b/src/storm-parsers/parser/JaniParser.h @@ -44,7 +44,7 @@ namespace storm { JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {} JaniParser(std::string const& jsonstring); - static std::pair> parse(std::string const& path); + static std::pair> parse(std::string const& path); protected: void readFile(std::string const& path); @@ -74,7 +74,7 @@ namespace storm { } }; - std::pair> parseModel(bool parseProperties = true); + std::pair> parseModel(bool parseProperties = true); storm::jani::Property parseProperty(json const& propertyStructure, Scope const& scope); storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, Scope const& scope); struct ParsedType {