From 90e9d91530a91152132631f202a8b42e1b7e6cc3 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 10 Oct 2018 09:11:39 +0200 Subject: [PATCH] add undefined constants in properties to the jani model when converting --- src/storm-conv/api/storm-conv.cpp | 12 ++++++++++++ .../converter/options/JaniConversionOptions.cpp | 4 ++-- .../converter/options/JaniConversionOptions.h | 3 +++ 3 files changed, 17 insertions(+), 2 deletions(-) diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index d9aa2212b..ddbe8abb2 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -2,6 +2,7 @@ #include "storm/storage/prism/Program.h" #include "storm/storage/jani/Property.h" +#include "storm/storage/jani/Constant.h" #include "storm/storage/jani/JaniLocationExpander.h" #include "storm/storage/jani/JSONExporter.h" @@ -45,6 +46,17 @@ namespace storm { if (options.modelName) { janiModel.setName(options.modelName.get()); } + + if (options.addPropertyConstants) { + for (auto& f : properties) { + for (auto const& constant : f.getUndefinedConstants()) { + if (!janiModel.hasConstant(constant.getName())) { + janiModel.addConstant(storm::jani::Constant(constant.getName(), constant)); + } + } + } + } + } std::pair> convertPrismToJani(storm::prism::Program const& program, std::vector const& properties, storm::converter::PrismToJaniConverterOptions options) { diff --git a/src/storm-conv/converter/options/JaniConversionOptions.cpp b/src/storm-conv/converter/options/JaniConversionOptions.cpp index 50a5a568c..df6eed905 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.cpp +++ b/src/storm-conv/converter/options/JaniConversionOptions.cpp @@ -3,11 +3,11 @@ namespace storm { namespace converter { - JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { + JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) { // Intentionally left empty } - JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { + JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true) { if (settings.isEliminateFunctionsSet()) { allowedModelFeatures.remove(storm::jani::ModelFeature::Functions); } diff --git a/src/storm-conv/converter/options/JaniConversionOptions.h b/src/storm-conv/converter/options/JaniConversionOptions.h index e5af6e3d0..f0fc6e62c 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.h +++ b/src/storm-conv/converter/options/JaniConversionOptions.h @@ -33,6 +33,9 @@ namespace storm { /// Only these model features are allowed in the output storm::jani::ModelFeatures allowedModelFeatures; + // Add constants that are defined in the properties to the model + bool addPropertyConstants; + }; } }