diff --git a/src/builder/JaniGSPNBuilder.h b/src/builder/JaniGSPNBuilder.h index 715450b1f..bfa0d663f 100644 --- a/src/builder/JaniGSPNBuilder.h +++ b/src/builder/JaniGSPNBuilder.h @@ -9,7 +9,7 @@ namespace storm { class JaniGSPNBuilder { public: JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr const& expManager) : gspn(gspn), expressionManager(expManager) { - + gspn.writeDotToStream(std::cout); } virtual ~JaniGSPNBuilder() { @@ -37,10 +37,11 @@ namespace storm { void addVariables(storm::jani::Model* model) { for (auto const& place : gspn.getPlaces()) { storm::jani::Variable* janiVar = nullptr; - if (place.getCapacity() == -1) { + if (!place.hasRestrictedCapacity()) { // Effectively no capacity limit known janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), false); } else { + assert(place.hasRestrictedCapacity()); janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity())); } assert(janiVar != nullptr); diff --git a/src/parser/GspnParser.cpp b/src/parser/GspnParser.cpp index be46626d5..e6bc79a27 100644 --- a/src/parser/GspnParser.cpp +++ b/src/parser/GspnParser.cpp @@ -379,9 +379,9 @@ namespace storm { // incoming arc if (type.second.compare("normal") == 0) { - trans.second->setInputArcMultiplicity(place.second, multiplicity.second); + trans.second->setInputArcMultiplicity(*place.second, multiplicity.second); } else if (type.second.compare("inhibition") == 0) { - trans.second->setInhibitionArcMultiplicity(place.second, multiplicity.second); + trans.second->setInhibitionArcMultiplicity(*place.second, multiplicity.second); } else { // unknown arc type // abort parsing @@ -395,7 +395,7 @@ namespace storm { auto place = gspn.getPlace(target.second); if (true == place.first && true == trans.first) { // outgoing arc - trans.second->setOutputArcMultiplicity(place.second, multiplicity.second); + trans.second->setOutputArcMultiplicity(*place.second, multiplicity.second); return; } } @@ -883,15 +883,15 @@ namespace storm { if (!place.first) { std::cout << "place not found" << std::endl; } - transition.second->setInputArcMultiplicity(place.second, mult); + transition.second->setInputArcMultiplicity(*place.second, mult); } else if (kind.compare("INHIBITOR") == 0) { auto transition = gspn.getTransition(head); auto place = gspn.getPlace(tail); - transition.second->setInhibitionArcMultiplicity(place.second, mult); + transition.second->setInhibitionArcMultiplicity(*place.second, mult); } else if (kind.compare("OUTPUT") == 0) { auto transition = gspn.getTransition(tail); auto place = gspn.getPlace(head); - transition.second->setOutputArcMultiplicity(place.second, mult); + transition.second->setOutputArcMultiplicity(*place.second, mult); } else { // TODO error! } diff --git a/src/settings/modules/GSPNSettings.cpp b/src/settings/modules/GSPNSettings.cpp new file mode 100644 index 000000000..b48597eaf --- /dev/null +++ b/src/settings/modules/GSPNSettings.cpp @@ -0,0 +1,68 @@ +#include "GSPNSettings.h" + +#include "src/settings/SettingsManager.h" +#include "src/settings/SettingMemento.h" +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" + +#include "src/exceptions/InvalidSettingsException.h" + +namespace storm { + namespace settings { + namespace modules { + const std::string GSPNSettings::moduleName = "gspn"; + + const std::string GSPNSettings::gspnFileOptionName = "gspnfile"; + const std::string GSPNSettings::gspnFileOptionShortName = "gspn"; + const std::string GSPNSettings::gspnToJaniOptionName = "to-jani"; + const std::string GSPNSettings::gspnToJaniOptionShortName = "tj"; + const std::string GSPNSettings::capacitiesFileOptionName = "capacitiesfile"; + const std::string GSPNSettings::capacitiesFileOptionShortName = "capacities"; + + + GSPNSettings::GSPNSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, gspnFileOptionName, false, "Parses the pgcl program.").setShortName(gspnFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, gspnToJaniOptionName, false, "Transform to JANI.").setShortName(gspnToJaniOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, capacitiesFileOptionName, false, "Restrictions of program variables").setShortName(capacitiesFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); + } + + bool GSPNSettings::isGspnFileSet() const { + return this->getOption(gspnFileOptionName).getHasOptionBeenSet(); + } + + std::string GSPNSettings::getGspnFilename() const { + return this->getOption(gspnFileOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool GSPNSettings::isToJaniSet() const { + return this->getOption(gspnToJaniOptionName).getHasOptionBeenSet(); + } + + bool GSPNSettings::isCapacitiesFileSet() const { + return this->getOption(capacitiesFileOptionName).getHasOptionBeenSet(); + } + + std::string GSPNSettings::getCapacitiesFilename() const { + return this->getOption(capacitiesFileOptionName).getArgumentByName("filename").getValueAsString(); + } + + void GSPNSettings::finalize() { + + } + + bool GSPNSettings::check() const { + if(!isGspnFileSet()) { + if(isToJaniSet()) { + return false; + } + if(isCapacitiesFileSet()) { + return false; + } + } + return true; + } + } + } +} \ No newline at end of file diff --git a/src/settings/modules/GSPNSettings.h b/src/settings/modules/GSPNSettings.h new file mode 100644 index 000000000..7d3cb2729 --- /dev/null +++ b/src/settings/modules/GSPNSettings.h @@ -0,0 +1,59 @@ +#pragma once + +#include "storm-config.h" +#include "src/settings/modules/ModuleSettings.h" + + +namespace storm { + namespace settings { + namespace modules { + class GSPNSettings : public ModuleSettings { + public: + /*! + * Creates a new PGCL setting + */ + GSPNSettings(); + + /** + * Retrievew whether the pgcl file option was set + */ + bool isGspnFileSet() const; + + /** + * Retrieves the gspn file name + */ + std::string getGspnFilename() const; + + /** + * Whether the gspn should be transformed to Jani + */ + bool isToJaniSet() const; + + /** + * Retrievew whether the pgcl file option was set + */ + bool isCapacitiesFileSet() const; + + /** + * Retrieves the gspn file name + */ + std::string getCapacitiesFilename() const; + + + bool check() const override; + void finalize() override; + + static const std::string moduleName; + + private: + static const std::string gspnFileOptionName; + static const std::string gspnFileOptionShortName; + static const std::string gspnToJaniOptionName; + static const std::string gspnToJaniOptionShortName; + static const std::string capacitiesFileOptionName; + static const std::string capacitiesFileOptionShortName; + + }; + } + } +} \ No newline at end of file diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp index 108991162..8449181d6 100644 --- a/src/storage/gspn/GSPN.cpp +++ b/src/storage/gspn/GSPN.cpp @@ -2,6 +2,7 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" +#include #include @@ -43,19 +44,30 @@ namespace storm { return m; } - std::pair GSPN::getPlace(uint_fast64_t const& id) const { + + std::pair GSPN::getPlace(uint_fast64_t const& id) const { for (auto& place : places) { if (id == place.getID()) { - return std::make_pair(true, place); + return std::make_pair(true, &place); } } - return std::make_pair(false, storm::gspn::Place()); + return std::make_pair(false, nullptr); } - - std::pair GSPN::getPlace(std::string const& id) const { + + + std::pair GSPN::getPlace(std::string const& id) { + for (auto& place : places) { + if (id.compare(place.getName()) == 0) { + return std::make_pair(true, &place); + } + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "No place with name " << id); + }; + + std::pair GSPN::getPlace(std::string const& id) const { for (auto& place : places) { if (id.compare(place.getName()) == 0) { - return std::make_pair(true, place); + return std::make_pair(true, &place); } } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "No place with name " << id); @@ -78,6 +90,8 @@ namespace storm { } return std::make_pair> const>(false, nullptr); } + + std::pair const> GSPN::getTransition(std::string const& id) const { auto trans = getTimedTransition(id); @@ -87,15 +101,30 @@ namespace storm { return getImmediateTransition(id); } + + void GSPN::setCapacities(std::unordered_map const& mapping) { + for(auto const& entry : mapping) { + std::cout << "restrict " << entry.first << std::endl; + auto place = getPlace(entry.first); + STORM_LOG_THROW(place.first, storm::exceptions::InvalidArgumentException, "No place with name " << entry.first); + place.second->setCapacity(entry.second); + + } + } - void GSPN::writeDotToStream(std::ostream& outStream) { + void GSPN::writeDotToStream(std::ostream& outStream) const { outStream << "digraph " << this->getName() << " {" << std::endl; // print places with initial marking (not printed is the capacity) outStream << "\t" << "node [shape=ellipse]" << std::endl; for (auto& place : this->getPlaces()) { outStream << "\t" << place.getName() << " [label=\"" << place.getName() << "(" << place.getNumberOfInitialTokens(); - outStream << ")\"];" << std::endl; + outStream << ")"; + if(place.hasRestrictedCapacity()) { + outStream << "c " << place.getCapacity(); + } + + outStream << "\"];" << std::endl; } // print transitions with weight/rate diff --git a/src/storage/gspn/GSPN.h b/src/storage/gspn/GSPN.h index f1b8c8881..0d7b6d800 100644 --- a/src/storage/gspn/GSPN.h +++ b/src/storage/gspn/GSPN.h @@ -1,10 +1,10 @@ -#ifndef STORM_STORAGE_GSPN_GSPN_H -#define STORM_STORAGE_GSPN_GSPN_H +#pragma once #include #include #include #include +#include #include "src/storage/gspn/ImmediateTransition.h" #include "src/storage/gspn/Marking.h" @@ -83,9 +83,10 @@ namespace storm { * If the first element is true, then the second element is the wanted place. * If the first element is false, then the second element is not defined. */ - std::pair getPlace(uint_fast64_t const& id) const; + std::pair getPlace(uint_fast64_t const& id) const; - std::pair getPlace(std::string const& id) const; + std::pair getPlace(std::string const& id); + std::pair getPlace(std::string const& id) const; /*! * Returns the timed transition with the corresponding id. * @@ -120,7 +121,7 @@ namespace storm { * * @param outStream The stream to which the output is written to. */ - void writeDotToStream(std::ostream& outStream); + void writeDotToStream(std::ostream& outStream) const; /*! * Set the name of the gspn to the given name. @@ -135,6 +136,12 @@ namespace storm { * @return The name. */ std::string const& getName() const; + + + /** + * Set Capacities according to name->capacity map. + */ + void setCapacities(std::unordered_map const& mapping); /*! * Performe some checks @@ -179,6 +186,4 @@ namespace storm { std::string name; }; } -} - -#endif //STORM_STORAGE_GSPN_GSPN_H +} \ No newline at end of file diff --git a/src/storage/gspn/GspnBuilder.cpp b/src/storage/gspn/GspnBuilder.cpp index 38c1b773b..3a4e1325c 100644 --- a/src/storage/gspn/GspnBuilder.cpp +++ b/src/storage/gspn/GspnBuilder.cpp @@ -48,7 +48,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist."); } - std::get<1>(transPair)->setInputArcMultiplicity(std::get<1>(placePair), multiplicity); + std::get<1>(transPair)->setInputArcMultiplicity(*std::get<1>(placePair), multiplicity); } void GspnBuilder::addInhibitionArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity) { @@ -62,7 +62,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist."); } - std::get<1>(transPair)->setInhibitionArcMultiplicity(std::get<1>(placePair), multiplicity); + std::get<1>(transPair)->setInhibitionArcMultiplicity(*std::get<1>(placePair), multiplicity); } void GspnBuilder::addOutputArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity) { @@ -76,7 +76,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist."); } - std::get<1>(transPair)->setOutputArcMultiplicity(std::get<1>(placePair), multiplicity); + std::get<1>(transPair)->setOutputArcMultiplicity(*std::get<1>(placePair), multiplicity); } storm::gspn::GSPN const& GspnBuilder::buildGspn() const { diff --git a/src/storage/gspn/Place.cpp b/src/storage/gspn/Place.cpp index 430acb9c9..15ff85b6c 100644 --- a/src/storage/gspn/Place.cpp +++ b/src/storage/gspn/Place.cpp @@ -29,13 +29,17 @@ namespace storm { return this->numberOfInitialTokens; } - void Place::setCapacity(int_fast64_t const& capacity) { - STORM_LOG_THROW(capacity <= -1, storm::exceptions::IllegalArgumentValueException, "The capacity cannot be less than -1."); - this->capacity = capacity; + void Place::setCapacity(uint64_t cap) { + std::cout << this->name << std::endl; + this->capacity = cap; } - int_fast64_t Place::getCapacity() const { - return this->capacity; + uint64_t Place::getCapacity() const { + return capacity.get(); + } + + bool Place::hasRestrictedCapacity() const { + return capacity != boost::none; } } } \ No newline at end of file diff --git a/src/storage/gspn/Place.h b/src/storage/gspn/Place.h index 09b52ef57..7b99fe6d2 100644 --- a/src/storage/gspn/Place.h +++ b/src/storage/gspn/Place.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_GSPN_PLACE_H_ #include +#include "boost/optional.hpp" namespace storm { namespace gspn { @@ -60,14 +61,19 @@ namespace storm { * @param capacity The capacity of this place. A non-negative number represents the capacity. * The value -1 indicates that the capacity is not set. */ - void setCapacity(int_fast64_t const& capacity); + void setCapacity(uint64_t capacity); /*! * Returns the capacity of tokens of this place. * - * @return The capacity of the place. The value -1 indicates that the capacity is not set. + * @return The capacity of the place. Only valid if the capacity is restricted. */ - int_fast64_t getCapacity() const; + uint64_t getCapacity() const; + + /*! + * + */ + bool hasRestrictedCapacity() const; private: // contains the number of initial tokens of this place uint_fast64_t numberOfInitialTokens = 0; @@ -81,7 +87,7 @@ namespace storm { // capacity of this place // -1 indicates that the capacity is not set // other non-negative values represents the capacity - int_fast64_t capacity = -1; + boost::optional capacity = boost::none; }; } } diff --git a/src/storage/gspn/Transition.cpp b/src/storage/gspn/Transition.cpp index a90e70c50..c9f2fb823 100644 --- a/src/storage/gspn/Transition.cpp +++ b/src/storage/gspn/Transition.cpp @@ -92,7 +92,7 @@ namespace storm { } for (auto &placePtr : getOutputPlaces()) { - if (placePtr->getCapacity() >= 0) { + if (placePtr->hasRestrictedCapacity()) { if (marking.getNumberOfTokensAt(placePtr->getID()) + getOutputArcMultiplicity(*placePtr) > placePtr->getCapacity()) { return false; } diff --git a/src/storm-gspn.cpp b/src/storm-gspn.cpp index 0bc3270b0..861e68cf7 100644 --- a/src/storm-gspn.cpp +++ b/src/storm-gspn.cpp @@ -1,11 +1,15 @@ #include "src/builder/ExplicitGspnModelBuilder.h" #include "src/exceptions/BaseException.h" +#include "src/exceptions/WrongFormatException.h" #include "src/parser/GspnParser.h" #include "src/storage/gspn/GSPN.h" #include "src/storage/gspn/GspnBuilder.h" #include "src/utility/macros.h" #include "src/utility/initialize.h" +#include "utility/storm.h" +#include "src/cli/cli.h" + #include "src/storage/expressions/ExpressionManager.h" #include "src/storage/jani/Model.h" #include "src/storage/jani/JsonExporter.h" @@ -14,91 +18,47 @@ #include #include +#include -/*! - * Parses the arguments to storm-gspn - * The read data is stored in the different arguments (e.g., inputFile, formula, ...) - * - * @param begin pointer to the first argument passed to storm-gspn - * @param end pointer to one past the last argument passed to storm-gspn - * @param inputFile the input file is stored in this object - * @param formula the formula is stored in this object - * @param outputFile the output file is stored in this object - * @param outputType the output type is stored in this object - * @return false if the help flag is set or the input file is missing - */ -bool parseArguments(const char **begin, const char **end, std::string &inputFile, std::string &formula, - std::string &outputFile, std::string &outputType) { - bool result = false; - - for (; begin != end; ++begin) { - std::string currentArg = *begin; - - // parse input file argument - if (currentArg == "--input_file" || currentArg == "-i") { - auto next = begin + 1; - if (next != end) { - inputFile = *next; - result = true; - } else { - return -1; - } - continue; - } +#include "src/exceptions/FileIoException.h" - // parse formula argument - if (currentArg == "--formula" || currentArg == "-f") { - auto next = begin + 1; - if (next != end) { - formula = *next; - } else { - return -1; - } - continue; - } +#include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/GspnSettings.h" +#include "src/settings/modules/CoreSettings.h" +#include "src/settings/modules/DebugSettings.h" +#include "src/settings/modules/JaniExportSettings.h" - // parse output file argument - if (currentArg == "--output_file" || currentArg == "-o") { - auto next = begin + 1; - if (next != end) { - outputFile = *next; - } else { - return -1; - } - continue; - } +/*! + * Initialize the settings manager. + */ +void initializeSettings() { + storm::settings::mutableManager().setName("StoRM-GSPN", "storm-gspn"); + + // Register all known settings modules. + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); +} - // parse output file type argument - if (currentArg == "--output_type" || currentArg == "-ot") { - auto next = begin + 1; - if (next != end) { - outputType = *next; - } else { - return -1; - } - continue; - } - // parse help argument - if (currentArg == "--help" || currentArg == "-h") { - return false; - } +std::unordered_map parseCapacitiesList(std::string const& filename) { + std::unordered_map map; + + std::ifstream ifs; + ifs.open(filename); + + std::string line; + while( std::getline(ifs, line) ) { + std::vector 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]); } - - return result; -} - -/*! - * Print the manual of storm-gspn - */ -void printHelp() { - std::cout << "storm-gspn -i input_file [-f formula] [-o output_file] [-ot output_type] [-h]" << std::endl; - std::cout << std::endl; - std::cout << "-i, --input_file: file which contains the gspn" << std::endl; - std::cout << "-f, --formula: formula which should be checked on the gspn" << std::endl; - std::cout << "-o, -output_file: file in which the gspn/markov automaton should be stored" << std::endl - << " requires the option -ot to be set" << std::endl; - std::cout << "-ot, --output_type: possible output types are: pnml, pnpro, dot or ma" << std::endl; + return map; + } void handleJani(storm::gspn::GSPN const& gspn) { @@ -110,23 +70,34 @@ void handleJani(storm::gspn::GSPN const& gspn) { } int main(const int argc, const char **argv) { - std::string inputFile, formula, outputFile, outputType; - if (!parseArguments(argv+1, argv+argc, inputFile, formula, outputFile, outputType)) { - printHelp(); - return 1; - } - try { storm::utility::setUp(); + storm::cli::printHeader("StoRM-GSPN", argc, argv); + initializeSettings(); + + bool optionsCorrect = storm::cli::parseOptions(argc, argv); + if (!optionsCorrect) { + return -1; + } // parse gspn from file + if (!storm::settings::getModule().isGspnFileSet()) { + return -1; + } + auto parser = storm::parser::GspnParser(); - auto gspn = parser.parse(inputFile); + auto gspn = parser.parse(storm::settings::getModule().getGspnFilename()); if (!gspn.isValid()) { STORM_LOG_ERROR("The gspn is not valid."); } + if(storm::settings::getModule().isCapacitiesFileSet()) { + auto capacities = parseCapacitiesList(storm::settings::getModule().getCapacitiesFilename()); + gspn.setCapacities(capacities); + } + + std::ofstream file; file.open("gspn.dot"); @@ -137,29 +108,29 @@ int main(const int argc, const char **argv) { return 0; - - // construct ma - auto builder = storm::builder::ExplicitGspnModelBuilder<>(); - auto ma = builder.translateGspn(gspn, formula); - - // write gspn into output file - if (!outputFile.empty()) { - std::ofstream file; - file.open(outputFile); - if (outputType == "pnml") { - gspn.toPnml(file); - } - if (outputType == "pnpro") { - gspn.toPnpro(file); - } - if (outputType == "dot") { - gspn.writeDotToStream(file); - } - if (outputType == "ma") { - ma.writeDotToStream(file); - } - file.close(); - } +// +// // construct ma +// auto builder = storm::builder::ExplicitGspnModelBuilder<>(); +// auto ma = builder.translateGspn(gspn, formula); +// +// // write gspn into output file +// if (!outputFile.empty()) { +// std::ofstream file; +// file.open(outputFile); +// if (outputType == "pnml") { +// gspn.toPnml(file); +// } +// if (outputType == "pnpro") { +// gspn.toPnpro(file); +// } +// if (outputType == "dot") { +// gspn.writeDotToStream(file); +// } +// if (outputType == "ma") { +// ma.writeDotToStream(file); +// } +// file.close(); +// } // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp();