Browse Source

fix in getPlace; add capacities, GSPN settings and main file updated

Former-commit-id: 375172b3075605a2c732fde6ca1346675cbb8a40 [formerly b8c1466633712c2afef4c5bbcbec3eb59142ac4a]
Former-commit-id: efaeb8b23872d710d16b6ec12637c8e3ffafc093
tempestpy_adaptions
sjunges 8 years ago
parent
commit
4f1f71ffae
  1. 5
      src/builder/JaniGSPNBuilder.h
  2. 12
      src/parser/GspnParser.cpp
  3. 68
      src/settings/modules/GSPNSettings.cpp
  4. 59
      src/settings/modules/GSPNSettings.h
  5. 45
      src/storage/gspn/GSPN.cpp
  6. 21
      src/storage/gspn/GSPN.h
  7. 6
      src/storage/gspn/GspnBuilder.cpp
  8. 14
      src/storage/gspn/Place.cpp
  9. 14
      src/storage/gspn/Place.h
  10. 2
      src/storage/gspn/Transition.cpp
  11. 189
      src/storm-gspn.cpp

5
src/builder/JaniGSPNBuilder.h

@ -9,7 +9,7 @@ namespace storm {
class JaniGSPNBuilder {
public:
JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr<storm::expressions::ExpressionManager> 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);

12
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!
}

68
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;
}
}
}
}

59
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;
};
}
}
}

45
src/storage/gspn/GSPN.cpp

@ -2,6 +2,7 @@
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
#include <unordered_map>
#include <boost/lexical_cast.hpp>
@ -43,19 +44,30 @@ namespace storm {
return m;
}
std::pair<bool, storm::gspn::Place> GSPN::getPlace(uint_fast64_t const& id) const {
std::pair<bool, storm::gspn::Place const*> GSPN::getPlace(uint_fast64_t const& id) const {
for (auto& place : places) {
if (id == place.getID()) {
return std::make_pair<bool, storm::gspn::Place const&>(true, place);
return std::make_pair<bool, storm::gspn::Place const*>(true, &place);
}
}
return std::make_pair<bool, storm::gspn::Place>(false, storm::gspn::Place());
return std::make_pair<bool, storm::gspn::Place const*>(false, nullptr);
}
std::pair<bool, storm::gspn::Place> GSPN::getPlace(std::string const& id) const {
std::pair<bool, storm::gspn::Place*> GSPN::getPlace(std::string const& id) {
for (auto& place : places) {
if (id.compare(place.getName()) == 0) {
return std::make_pair<bool, storm::gspn::Place*>(true, &place);
}
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "No place with name " << id);
};
std::pair<bool, storm::gspn::Place const*> GSPN::getPlace(std::string const& id) const {
for (auto& place : places) {
if (id.compare(place.getName()) == 0) {
return std::make_pair<bool, storm::gspn::Place const&>(true, place);
return std::make_pair<bool, storm::gspn::Place const*>(true, &place);
}
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "No place with name " << id);
@ -78,6 +90,8 @@ namespace storm {
}
return std::make_pair<bool, std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> const>(false, nullptr);
}
std::pair<bool, std::shared_ptr<storm::gspn::Transition> 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<std::string, uint64_t> 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

21
src/storage/gspn/GSPN.h

@ -1,10 +1,10 @@
#ifndef STORM_STORAGE_GSPN_GSPN_H
#define STORM_STORAGE_GSPN_GSPN_H
#pragma once
#include <iostream>
#include <stdint.h>
#include <vector>
#include <memory>
#include <unordered_map>
#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<bool, storm::gspn::Place> getPlace(uint_fast64_t const& id) const;
std::pair<bool, storm::gspn::Place const*> getPlace(uint_fast64_t const& id) const;
std::pair<bool, storm::gspn::Place> getPlace(std::string const& id) const;
std::pair<bool, storm::gspn::Place*> getPlace(std::string const& id);
std::pair<bool, storm::gspn::Place const*> 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<std::string, uint64_t> const& mapping);
/*!
* Performe some checks
@ -179,6 +186,4 @@ namespace storm {
std::string name;
};
}
}
#endif //STORM_STORAGE_GSPN_GSPN_H
}

6
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 {

14
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;
}
}
}

14
src/storage/gspn/Place.h

@ -2,6 +2,7 @@
#define STORM_STORAGE_GSPN_PLACE_H_
#include <string>
#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<uint64_t> capacity = boost::none;
};
}
}

2
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;
}

189
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 <iostream>
#include <string>
#include <boost/algorithm/string.hpp>
/*!
* 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::modules::GeneralSettings>();
storm::settings::addModule<storm::settings::modules::GSPNSettings>();
storm::settings::addModule<storm::settings::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
}
// 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<std::string, uint64_t> parseCapacitiesList(std::string const& filename) {
std::unordered_map<std::string, uint64_t> map;
std::ifstream ifs;
ifs.open(filename);
std::string line;
while( std::getline(ifs, line) ) {
std::vector<std::string> 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<storm::settings::modules::GSPNSettings>().isGspnFileSet()) {
return -1;
}
auto parser = storm::parser::GspnParser();
auto gspn = parser.parse(inputFile);
auto gspn = parser.parse(storm::settings::getModule<storm::settings::modules::GSPNSettings>().getGspnFilename());
if (!gspn.isValid()) {
STORM_LOG_ERROR("The gspn is not valid.");
}
if(storm::settings::getModule<storm::settings::modules::GSPNSettings>().isCapacitiesFileSet()) {
auto capacities = parseCapacitiesList(storm::settings::getModule<storm::settings::modules::GSPNSettings>().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();
Loading…
Cancel
Save