Browse Source

Some refactoring

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
256137b080
  1. 34
      src/storm-dft-cli/storm-dft.cpp
  2. 19
      src/storm-dft/api/storm-dft.h

34
src/storm-dft-cli/storm-dft.cpp

@ -1,17 +1,17 @@
#include <storm/exceptions/UnmetRequirementException.h>
#include "storm-dft/api/storm-dft.h" #include "storm-dft/api/storm-dft.h"
#include "storm-dft/settings/DftSettings.h" #include "storm-dft/settings/DftSettings.h"
#include "storm-dft/settings/modules/DftGspnSettings.h"
#include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/settings/modules/DftIOSettings.h"
#include "storm-dft/settings/modules/FaultTreeSettings.h" #include "storm-dft/settings/modules/FaultTreeSettings.h"
#include "storm-dft/settings/modules/DftGspnSettings.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm-parsers/api/storm-parsers.h"
#include "storm/utility/initialize.h" #include "storm/utility/initialize.h"
#include "storm-cli-utilities/cli.h" #include "storm-cli-utilities/cli.h"
#include "storm-parsers/api/storm-parsers.h"
/*! /*!
* Process commandline options and start computations. * Process commandline options and start computations.
@ -28,7 +28,7 @@ void processOptions() {
if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given.");
} }
// Build DFT from given file // Build DFT from given file
@ -48,13 +48,12 @@ void processOptions() {
if (dftIOSettings.isExportToJson()) { if (dftIOSettings.isExportToJson()) {
// Export to json // Export to json
storm::api::exportDFTToJsonFile<ValueType>(*dft, dftIOSettings.getExportJsonFilename()); storm::api::exportDFTToJsonFile<ValueType>(*dft, dftIOSettings.getExportJsonFilename());
return;
} }
// Check well-formedness of DFT // Check well-formedness of DFT
std::stringstream stream; std::stringstream stream;
if (!dft->checkWellFormedness(stream)) { if (!dft->checkWellFormedness(stream)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "DFT is not well-formed: " << stream.str());
STORM_LOG_THROW(false, storm::exceptions::UnmetRequirementException, "DFT is not well-formed: " << stream.str());
} }
if (dftGspnSettings.isTransformToGspn()) { if (dftGspnSettings.isTransformToGspn()) {
@ -82,14 +81,16 @@ void processOptions() {
} }
#endif #endif
// From now on we analyse DFT via model checking
// Set min or max // Set min or max
std::string optimizationDirection = "min"; std::string optimizationDirection = "min";
if (dftIOSettings.isComputeMaximalValue()) { if (dftIOSettings.isComputeMaximalValue()) {
STORM_LOG_THROW(!dftIOSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time.");
optimizationDirection = "max"; optimizationDirection = "max";
} }
// Construct properties to analyse
// Construct properties to analyse.
// We allow multiple properties to be checked at once.
std::vector<std::string> properties; std::vector<std::string> properties;
if (ioSettings.isPropertySet()) { if (ioSettings.isPropertySet()) {
properties.push_back(ioSettings.getProperty()); properties.push_back(ioSettings.getProperty());
@ -114,10 +115,13 @@ void processOptions() {
} }
// Build properties // Build properties
STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidSettingsException, "No property given.");
std::string propString = properties[0];
for (size_t i = 1; i < properties.size(); ++i) {
propString += ";" + properties[i];
STORM_LOG_WARN_COND(!properties.empty(), "No property given.");
std::string propString;
for (size_t i = 0; i < properties.size(); ++i) {
if (i + 1 < properties.size()) {
propString += ";";
}
propString += properties[i];
} }
std::vector<std::shared_ptr<storm::logic::Formula const>> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString)); std::vector<std::shared_ptr<storm::logic::Formula const>> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString));
@ -159,7 +163,7 @@ void processOptions() {
* *
* @param argc The argc argument of main(). * @param argc The argc argument of main().
* @param argv The argv argument of main(). * @param argv The argv argument of main().
* @return Return code, 0 if successfull, not 0 otherwise.
* @return Return code, 0 if successful, > 0 otherwise.
*/ */
int main(const int argc, const char** argv) { int main(const int argc, const char** argv) {
try { try {

19
src/storm-dft/api/storm-dft.h

@ -5,11 +5,10 @@
#include "storm-dft/parser/DFTGalileoParser.h" #include "storm-dft/parser/DFTGalileoParser.h"
#include "storm-dft/parser/DFTJsonParser.h" #include "storm-dft/parser/DFTJsonParser.h"
#include "storm-dft/storage/dft/DftJsonExporter.h" #include "storm-dft/storage/dft/DftJsonExporter.h"
#include "storm-dft/modelchecker/dft/DFTModelChecker.h" #include "storm-dft/modelchecker/dft/DFTModelChecker.h"
#include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm-dft/modelchecker/dft/DFTASFChecker.h"
#include "storm-dft/transformations/DftToGspnTransformator.h" #include "storm-dft/transformations/DftToGspnTransformator.h"
#include "storm-gspn/api/storm-gspn.h" #include "storm-gspn/api/storm-gspn.h"
namespace storm { namespace storm {
@ -19,38 +18,35 @@ namespace storm {
* Load DFT from Galileo file. * Load DFT from Galileo file.
* *
* @param file File containing DFT description in Galileo format. * @param file File containing DFT description in Galileo format.
*
* @return DFT. * @return DFT.
*/ */
template<typename ValueType> template<typename ValueType>
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTGalileoFile(std::string const& file) { std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTGalileoFile(std::string const& file) {
return std::make_shared<storm::storage::DFT<ValueType>>(storm::parser::DFTGalileoParser<ValueType>::parseDFT(file));
return std::make_shared<storm::storage::DFT<ValueType>>(storm::parser::DFTGalileoParser<ValueType>::parseDFT(file));
} }
/*! /*!
* Load DFT from JSON string. * Load DFT from JSON string.
* *
* @param jsonString String containing DFT description in JSON format. * @param jsonString String containing DFT description in JSON format.
*
* @return DFT. * @return DFT.
*/ */
template<typename ValueType> template<typename ValueType>
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJsonString(std::string const& jsonString) { std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJsonString(std::string const& jsonString) {
storm::parser::DFTJsonParser<ValueType> parser;
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromString(jsonString));
storm::parser::DFTJsonParser<ValueType> parser;
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromString(jsonString));
} }
/*! /*!
* Load DFT from JSON file. * Load DFT from JSON file.
* *
* @param file File containing DFT description in JSON format. * @param file File containing DFT description in JSON format.
*
* @return DFT. * @return DFT.
*/ */
template<typename ValueType> template<typename ValueType>
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJsonFile(std::string const& file) { std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJsonFile(std::string const& file) {
storm::parser::DFTJsonParser<ValueType> parser;
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromFile(file));
storm::parser::DFTJsonParser<ValueType> parser;
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromFile(file));
} }
/*! /*!
@ -107,6 +103,7 @@ namespace storm {
* Export DFT to JSON string. * Export DFT to JSON string.
* *
* @param dft DFT. * @param dft DFT.
* @return DFT in JSON format.
*/ */
template<typename ValueType> template<typename ValueType>
std::string exportDFTToJsonString(storm::storage::DFT<ValueType> const& dft); std::string exportDFTToJsonString(storm::storage::DFT<ValueType> const& dft);
@ -124,7 +121,6 @@ namespace storm {
* Transform DFT to GSPN. * Transform DFT to GSPN.
* *
* @param dft DFT. * @param dft DFT.
*
* @return Pair of GSPN and id of failed place corresponding to the top level element. * @return Pair of GSPN and id of failed place corresponding to the top level element.
*/ */
template<typename ValueType> template<typename ValueType>
@ -135,7 +131,6 @@ namespace storm {
* *
* @param gspn GSPN. * @param gspn GSPN.
* @param toplevelFailedPlace Id of the failed place in the GSPN for the top level element in the DFT. * @param toplevelFailedPlace Id of the failed place in the GSPN for the top level element in the DFT.
*
* @return JANI model. * @return JANI model.
*/ */
std::shared_ptr<storm::jani::Model> transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace); std::shared_ptr<storm::jani::Model> transformToJani(storm::gspn::GSPN const& gspn, uint64_t toplevelFailedPlace);

Loading…
Cancel
Save