diff --git a/CHANGELOG.md b/CHANGELOG.md
index 539f2431a..52bebe6e8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,7 @@ Version 1.3.x
- JANI: Support for non-trivial reward accumulations.
- JANI: Fixed support for reward expressions over non-transient variables.
- DRN: Added support for exact parsing and action-based rewards
+- storm-conv can now apply transformations on a prism file
- Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial)
- Fixed linking with Mathsat on macOS
- Fixed compilation for macOS mojave
diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp
index 1c333f93c..bbd700b53 100644
--- a/src/storm-conv-cli/storm-conv.cpp
+++ b/src/storm-conv-cli/storm-conv.cpp
@@ -6,6 +6,8 @@
#include "storm-conv/settings/modules/ConversionGeneralSettings.h"
#include "storm-conv/settings/modules/ConversionInputSettings.h"
#include "storm-conv/settings/modules/ConversionOutputSettings.h"
+#include "storm-conv/settings/modules/JaniExportSettings.h"
+#include "storm-conv/settings/modules/PrismExportSettings.h"
#include "storm/api/storm.h"
#include "storm-parsers/api/storm-parsers.h"
@@ -117,6 +119,52 @@ namespace storm {
stopStopwatch(exportingTime);
}
+ void processPrismInputPrismOutput(storm::prism::Program const& prismProg, std::vector<storm::jani::Property> const& properties) {
+ auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
+ auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+ auto const& prism = storm::settings::getModule<storm::settings::modules::PrismExportSettings>();
+
+ auto conversionTime = startStopwatch("Processing Prism Program ... " );
+
+ // Get the name of the output file
+ std::string outputFilename = "";
+ if (output.isPrismOutputFilenameSet()) {
+ outputFilename = output.getPrismOutputFilename();
+ } else if (input.isPrismInputSet() && !output.isStdOutOutputEnabled()) {
+ outputFilename = input.getPrismInputFilename();
+ // Remove extension if present
+ auto dotPos = outputFilename.rfind('.');
+ if (dotPos != std::string::npos) {
+ outputFilename.erase(dotPos);
+ }
+ std::string suffix = "";
+ if (input.isConstantsSet()) {
+ suffix = input.getConstantDefinitionString();
+ std::replace(suffix.begin(), suffix.end(), ',', '_');
+ std::replace(suffix.begin(), suffix.end(), '=', '-');
+ }
+ suffix += "_converted.prism";
+ outputFilename += suffix;
+ }
+
+ storm::prism::Program outputProgram = prismProg;
+ std::vector<storm::jani::Property> outputProperties = properties;
+ storm::api::transformPrism(outputProgram, outputProperties, prism.isSimplifySet(), prism.isExportFlattenedSet());
+
+ stopStopwatch(conversionTime);
+ auto exportingTime = startStopwatch("Exporting Prism program ... ");
+
+ if (outputFilename != "") {
+ storm::api::exportPrismToFile(outputProgram, outputProperties, outputFilename);
+ STORM_PRINT_AND_LOG("Stored to file '" << outputFilename << "'");
+ }
+
+ if (output.isStdOutOutputEnabled()) {
+ storm::api::printPrismToStream(outputProgram, outputProperties, std::cout);
+ }
+ stopStopwatch(exportingTime);
+ }
+
void processPrismInput() {
auto parsingTime = startStopwatch("Parsing PRISM input ... " );
@@ -145,6 +193,8 @@ namespace storm {
auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
if (output.isJaniOutputSet()) {
processPrismInputJaniOutput(prismProg.asPrismProgram(), properties);
+ } else if (output.isPrismOutputSet()) {
+ processPrismInputPrismOutput(prismProg.asPrismProgram(), properties);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "There is either no outputformat specified or the provided combination of input and output format is not compatible.");
}
@@ -251,6 +301,7 @@ namespace storm {
if (output.isJaniOutputSet()) {
processJaniInputJaniOutput(janiModel, properties);
} else {
+ STORM_LOG_THROW(!output.isPrismOutputSet(), storm::exceptions::InvalidSettingsException, "Conversion from Jani to Prism is not supported.");
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "There is either no outputformat specified or the provided combination of input and output format is not compatible.");
}
}
diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp
index 9b747fe2c..c133d1673 100644
--- a/src/storm-conv/api/storm-conv.cpp
+++ b/src/storm-conv/api/storm-conv.cpp
@@ -7,6 +7,9 @@
#include "storm/storage/jani/JaniScopeChanger.h"
#include "storm/storage/jani/JSONExporter.h"
+#include "storm/utility/file.h"
+#include "storm/api/properties.h"
+
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"
@@ -79,6 +82,20 @@ namespace storm {
}
+ void transformPrism(storm::prism::Program& prismProgram, std::vector<storm::jani::Property>& properties, bool simplify, bool flatten) {
+ if (simplify) {
+ prismProgram = prismProgram.simplify().simplify();
+ properties = storm::api::substituteConstantsInProperties(properties, prismProgram.getConstantsFormulasSubstitution());
+ }
+ if (flatten) {
+ prismProgram = prismProgram.flattenModules();
+ if (simplify) {
+ // Let's simplify the flattened program again ... just to be sure ... twice ...
+ prismProgram = prismProgram.simplify().simplify();
+ }
+ }
+ }
+
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, storm::converter::PrismToJaniConverterOptions options) {
// Perform conversion
@@ -104,6 +121,28 @@ namespace storm {
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);
}
+
+ void exportPrismToFile(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, std::string const& filename) {
+ std::ofstream stream;
+ storm::utility::openFile(filename, stream);
+ stream << program << std::endl;
+ storm::utility::closeFile(stream);
+
+ if (!properties.empty()) {
+ storm::utility::openFile(filename + ".props", stream);
+ for (auto const& prop : properties) {
+ stream << prop << std::endl;
+ }
+ storm::utility::closeFile(stream);
+ }
+ }
+ void printPrismToStream(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, std::ostream& ostream) {
+ ostream << program << std::endl;
+ for (auto const& prop : properties) {
+ ostream << prop << std::endl;
+ }
+ }
+
}
diff --git a/src/storm-conv/api/storm-conv.h b/src/storm-conv/api/storm-conv.h
index 12e45269d..71c1b8c55 100644
--- a/src/storm-conv/api/storm-conv.h
+++ b/src/storm-conv/api/storm-conv.h
@@ -16,12 +16,15 @@ namespace storm {
namespace api {
void transformJani(storm::jani::Model& janiModel, std::vector<storm::jani::Property>& properties, storm::converter::JaniConversionOptions const& options);
+
+ void transformPrism(storm::prism::Program& prismProgram, std::vector<storm::jani::Property>& properties, bool simplify = false, bool flatten = false);
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, bool compact = false);
-
void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream, bool compact = false);
+ void exportPrismToFile(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, std::string const& filename);
+ void printPrismToStream(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, std::ostream& ostream);
}
diff --git a/src/storm-conv/settings/ConvSettings.cpp b/src/storm-conv/settings/ConvSettings.cpp
index cbb872390..487a57f07 100644
--- a/src/storm-conv/settings/ConvSettings.cpp
+++ b/src/storm-conv/settings/ConvSettings.cpp
@@ -4,6 +4,7 @@
#include "storm-conv/settings/modules/ConversionInputSettings.h"
#include "storm-conv/settings/modules/ConversionOutputSettings.h"
#include "storm-conv/settings/modules/JaniExportSettings.h"
+#include "storm-conv/settings/modules/PrismExportSettings.h"
#include "storm/settings/SettingsManager.h"
@@ -18,6 +19,7 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::ConversionInputSettings>();
storm::settings::addModule<storm::settings::modules::ConversionOutputSettings>();
storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
+ storm::settings::addModule<storm::settings::modules::PrismExportSettings>();
}
}
diff --git a/src/storm-conv/settings/modules/ConversionOutputSettings.cpp b/src/storm-conv/settings/modules/ConversionOutputSettings.cpp
index 61002078d..198b5150d 100644
--- a/src/storm-conv/settings/modules/ConversionOutputSettings.cpp
+++ b/src/storm-conv/settings/modules/ConversionOutputSettings.cpp
@@ -16,10 +16,13 @@ namespace storm {
const std::string ConversionOutputSettings::moduleName = "output";
const std::string ConversionOutputSettings::stdoutOptionName = "stdout";
const std::string ConversionOutputSettings::janiOutputOptionName = "tojani";
+ const std::string ConversionOutputSettings::prismOutputOptionName = "toprism";
ConversionOutputSettings::ConversionOutputSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, stdoutOptionName, false, "If set, the output will be printed to stdout.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, janiOutputOptionName, false, "converts the input model to Jani.")
+ this->addOption(storm::settings::OptionBuilder(moduleName, janiOutputOptionName, false, "exports the model as Jani file.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the output file (if not empty).").setDefaultValueString("").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, prismOutputOptionName, false, "exports the model as Prism file.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the output file (if not empty).").setDefaultValueString("").build()).build());
}
@@ -42,6 +45,22 @@ namespace storm {
STORM_LOG_THROW(isJaniOutputFilenameSet(), storm::exceptions::InvalidOperationException, "Tried to get the jani output name although none was specified.");
return this->getOption(janiOutputOptionName).getArgumentByName("filename").getValueAsString();
}
+
+ bool ConversionOutputSettings::isPrismOutputSet() const {
+ return this->getOption(prismOutputOptionName).getHasOptionBeenSet();
+ }
+
+ bool ConversionOutputSettings::isPrismOutputFilenameSet() const {
+ return isPrismOutputSet()
+ && !this->getOption(prismOutputOptionName).getArgumentByName("filename").wasSetFromDefaultValue()
+ && this->getOption(prismOutputOptionName).getArgumentByName("filename").getHasBeenSet()
+ && this->getOption(prismOutputOptionName).getArgumentByName("filename").getValueAsString() != "";
+ }
+
+ std::string ConversionOutputSettings::getPrismOutputFilename() const {
+ STORM_LOG_THROW(isPrismOutputFilenameSet(), storm::exceptions::InvalidOperationException, "Tried to get the prism output name although none was specified.");
+ return this->getOption(prismOutputOptionName).getArgumentByName("filename").getValueAsString();
+ }
void ConversionOutputSettings::finalize() {
// Intentionally left empty.
@@ -49,6 +68,8 @@ namespace storm {
bool ConversionOutputSettings::check() const {
STORM_LOG_THROW(!isJaniOutputFilenameSet() || ArgumentValidatorFactory::createWritableFileValidator()->isValid(getJaniOutputFilename()), storm::exceptions::InvalidSettingsException, "Unable to write at file " + getJaniOutputFilename());
+ STORM_LOG_THROW(!isPrismOutputFilenameSet() || ArgumentValidatorFactory::createWritableFileValidator()->isValid(getPrismOutputFilename()), storm::exceptions::InvalidSettingsException, "Unable to write at file " + getPrismOutputFilename());
+ STORM_LOG_THROW(!(isJaniOutputSet() && isPrismOutputSet()), storm::exceptions::InvalidSettingsException, "Can not export to both, prism and jani");
return true;
}
diff --git a/src/storm-conv/settings/modules/ConversionOutputSettings.h b/src/storm-conv/settings/modules/ConversionOutputSettings.h
index e429cdd93..fbfee697d 100644
--- a/src/storm-conv/settings/modules/ConversionOutputSettings.h
+++ b/src/storm-conv/settings/modules/ConversionOutputSettings.h
@@ -30,6 +30,21 @@ namespace storm {
*/
std::string getJaniOutputFilename() const;
+ /*!
+ * Retrieves whether the output should be in the Prism format
+ */
+ bool isPrismOutputSet() const;
+
+ /*!
+ * Retrieves whether an output filename for the prism file was specified
+ */
+ bool isPrismOutputFilenameSet() const;
+
+ /*!
+ * Retrieves the name of the prism output (if specified)
+ */
+ std::string getPrismOutputFilename() const;
+
bool check() const override;
void finalize() override;
@@ -41,6 +56,8 @@ namespace storm {
private:
// Define the string names of the options as constants.
static const std::string janiOutputOptionName;
+ // Define the string names of the options as constants.
+ static const std::string prismOutputOptionName;
};
diff --git a/src/storm-conv/settings/modules/PrismExportSettings.cpp b/src/storm-conv/settings/modules/PrismExportSettings.cpp
new file mode 100644
index 000000000..05a9f4c38
--- /dev/null
+++ b/src/storm-conv/settings/modules/PrismExportSettings.cpp
@@ -0,0 +1,42 @@
+#include "PrismExportSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+
+#include <boost/algorithm/string.hpp>
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+ const std::string PrismExportSettings::moduleName = "exportPrism";
+
+ const std::string PrismExportSettings::exportFlattenOptionName = "flatten";
+ const std::string PrismExportSettings::exportSimplifyOptionName = "simplify";
+
+ PrismExportSettings::PrismExportSettings() : ModuleSettings(moduleName) {
+ this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Flattens the composition of modules to obtain an equivalent program that contains exactly one module").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, exportSimplifyOptionName, false, "Applies static analysis to simplify the program.").build());
+ }
+
+ bool PrismExportSettings::isExportFlattenedSet() const {
+ return this->getOption(exportFlattenOptionName).getHasOptionBeenSet();
+ }
+
+ bool PrismExportSettings::isSimplifySet() const {
+ return this->getOption(exportSimplifyOptionName).getHasOptionBeenSet();
+ }
+
+ void PrismExportSettings::finalize() {
+
+ }
+
+ bool PrismExportSettings::check() const {
+ return true;
+ }
+ }
+ }
+}
diff --git a/src/storm-conv/settings/modules/PrismExportSettings.h b/src/storm-conv/settings/modules/PrismExportSettings.h
new file mode 100644
index 000000000..eb3270f2b
--- /dev/null
+++ b/src/storm-conv/settings/modules/PrismExportSettings.h
@@ -0,0 +1,32 @@
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+ class PrismExportSettings : public ModuleSettings {
+ public:
+ /*!
+ * Creates a new PrismExport setting
+ */
+ PrismExportSettings();
+
+ bool isExportFlattenedSet() const;
+ bool isSimplifySet() const;
+
+ bool check() const override;
+ void finalize() override;
+
+ static const std::string moduleName;
+
+ private:
+ static const std::string exportFlattenOptionName;
+ static const std::string exportSimplifyOptionName;
+
+ };
+ }
+ }
+}