From 6843f4349f7b111b1e4e45bdedfea986fb3dbbf4 Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 11 Nov 2016 14:19:53 +0100 Subject: [PATCH] refactorign of gspns: use ints as identifiers on more places, use the builder in the parsing process, split the parsers for project files and pnml, as well as some minor stuff Former-commit-id: f6cab8208b8c02e6bea86eb703bbb139f309fd9b [formerly 9ef5558433ab2f50acb2fcec55e86c85e2dede82] Former-commit-id: cb48f9e55a0ad0054d342595b6a4677a4461b146 --- src/adapters/XercesAdapter.h | 42 + src/builder/ExplicitGspnModelBuilder.cpp | 652 +++++++-------- src/builder/ExplicitGspnModelBuilder.h | 344 ++++---- src/builder/JaniGSPNBuilder.h | 64 +- src/parser/GreatSpnEditorProjectParser.cpp | 343 ++++++++ src/parser/GreatSpnEditorProjectParser.h | 42 + src/parser/GspnParser.cpp | 889 +-------------------- src/parser/GspnParser.h | 169 +--- src/parser/PnmlParser.cpp | 446 +++++++++++ src/parser/PnmlParser.h | 142 ++++ src/storage/gspn/GSPN.cpp | 251 +++--- src/storage/gspn/GSPN.h | 70 +- src/storage/gspn/GspnBuilder.cpp | 141 ++-- src/storage/gspn/GspnBuilder.h | 64 +- src/storage/gspn/ImmediateTransition.h | 2 +- src/storage/jani/JSONExporter.cpp | 4 +- 16 files changed, 1878 insertions(+), 1787 deletions(-) create mode 100644 src/adapters/XercesAdapter.h create mode 100644 src/parser/GreatSpnEditorProjectParser.cpp create mode 100644 src/parser/GreatSpnEditorProjectParser.h create mode 100644 src/parser/PnmlParser.cpp create mode 100644 src/parser/PnmlParser.h diff --git a/src/adapters/XercesAdapter.h b/src/adapters/XercesAdapter.h new file mode 100644 index 000000000..de05ece97 --- /dev/null +++ b/src/adapters/XercesAdapter.h @@ -0,0 +1,42 @@ +#pragma once + + +#include +#include + + +#include +#include +#include + + + +namespace storm { + namespace adapters { + inline std::string XMLtoString(const XMLCh *xmlString) { + char* tmp = xercesc::XMLString::transcode(xmlString); + auto result = std::string(tmp); + delete tmp; + return result; + } + + inline std::string getName(xercesc::DOMNode const* node) { + switch (node->getNodeType()) { + case xercesc::DOMNode::NodeType::ELEMENT_NODE: { + auto elementNode = (xercesc::DOMElement *) node; + return XMLtoString(elementNode->getTagName()); + } + case xercesc::DOMNode::NodeType::TEXT_NODE: { + return XMLtoString(node->getNodeValue()); + } + case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: { + return XMLtoString(node->getNodeName()); + } + default: { + assert(false); + return ""; + } + } + } + } +} diff --git a/src/builder/ExplicitGspnModelBuilder.cpp b/src/builder/ExplicitGspnModelBuilder.cpp index f3682de28..eae1a73b2 100644 --- a/src/builder/ExplicitGspnModelBuilder.cpp +++ b/src/builder/ExplicitGspnModelBuilder.cpp @@ -1,326 +1,326 @@ -#include "src/builder/ExplicitGspnModelBuilder.h" - -#include "src/models/sparse/StandardRewardModel.h" - -#include "src/utility/macros.h" -#include "src/exceptions/NotImplementedException.h" -#include "src/storage/expressions/ExpressionManager.h" -#include "src/parser/FormulaParser.h" -#include "src/storage/expressions/ExpressionEvaluator.h" - -namespace storm { - namespace builder { - - template - storm::models::sparse::MarkovAutomaton ExplicitGspnModelBuilder::translateGspn(storm::gspn::GSPN const& gspn, std::string const& formula) { - // set the given gspn and compute the limits of the net - this->gspn = gspn; - computeCapacities(gspn); - - // markings maps markings to their corresponding rowgroups (indices) - markings = storm::storage::BitVectorHashMap(numberOfTotalBits, 100); - builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, true); - - // add initial marking to todo list - auto bitvector = gspn.getInitialMarking(numberOfBits, numberOfTotalBits)->getBitVector(); - findOrAddBitvectorToMarkings(*bitvector); - currentRowIndex = 0; - - // vector marking markovian states (vector contains an 1 if the state is markovian) - storm::storage::BitVector markovianStates(0); - - // vector containing the exit rates for the markovian states - std::vector exitRates; - - - while (!todo.empty()) { - // take next element from the todo list - auto currentBitvector = todo.front(); - todo.pop_front(); - auto currentMarking = storm::gspn::Marking(gspn.getNumberOfPlaces(), numberOfBits, *currentBitvector); - - // increment list of states by one - markovianStates.resize(markovianStates.size() + 1, 0); - - // create new row group for the current marking - builder.newRowGroup(markings.getValue(*currentBitvector)); - - std::cout << "work on: " << *currentBitvector << std::endl; - - auto enabledImmediateTransitions = getEnabledImmediateTransition(currentMarking); - if (!enabledImmediateTransitions.empty()) { - markovianStates.set(currentRowIndex, 0); - exitRates.push_back(0); - - auto partitions = partitonEnabledImmediateTransitions(currentMarking, enabledImmediateTransitions); - addRowForPartitions(partitions, currentMarking); - } else { - - auto enabledTimedTransitions = getEnabledTimedTransition(currentMarking); - if (!enabledTimedTransitions.empty()) { - markovianStates.set(currentRowIndex, 1); - - auto accRate = getAccumulatedRate(enabledTimedTransitions); - std::cout << "\t\tacc. rate: " << accRate << std::endl; - exitRates.push_back(accRate); - - addRowForTimedTransitions(enabledTimedTransitions, currentMarking, accRate); - } else { - markovianStates.set(currentRowIndex, 1); - } - } - ++currentRowIndex; - } - - auto matrix = builder.build(); - - // create expression manager and add variables from the gspn - auto expressionManager = std::make_shared(); - for (auto& place : gspn.getPlaces()) { - expressionManager->declareIntegerVariable(place.getName()); - } - - // parse formula - storm::parser::FormulaParser formulaParser(expressionManager); - auto formulaPtr = formulaParser.parseSingleFormulaFromString(formula); - auto atomicFormulas = formulaPtr->getAtomicExpressionFormulas(); - - // create empty state labeling - storm::models::sparse::StateLabeling labeling(markings.size()); - storm::expressions::ExpressionEvaluator expressionEvaluator(*expressionManager); - - std::cout << std::endl; - std::cout << "build labeling:" << std::endl; - for (auto& atomicFormula : atomicFormulas) { - std::cout << atomicFormula; - auto label = atomicFormula->toString(); - labeling.addLabel(label); - - for (auto statePair : markings) { - auto marking = storm::gspn::Marking(gspn.getNumberOfPlaces(), numberOfBits, statePair.first); - for (auto& place : gspn.getPlaces()) { - auto variable = expressionManager->getVariable(place.getName()); - expressionEvaluator.setIntegerValue(variable, marking.getNumberOfTokensAt(place.getID())); - } - bool hold = expressionEvaluator.asBool(atomicFormula->getExpression()); - if (hold) { - labeling.addLabelToState(label, statePair.second); - } - } - - } - - //auto labeling = getStateLabeling(); - - return storm::models::sparse::MarkovAutomaton(matrix, labeling, markovianStates, exitRates); - } - - template - void ExplicitGspnModelBuilder::addRowForPartitions(std::vector>>> const& partitions, storm::gspn::Marking const& currentMarking) { - for (auto& partition : partitions) { - std::cout << "\tnew partition:" << std::endl; - auto accWeight = getAccumulatedWeight(partition); - std::cout << "\t\tacc. weight: " << accWeight << std::endl; - - std::map::cmpByIndex> weights; - for (auto& trans : partition) { - std::cout << "\t\ttransname: " << trans->getName() << std::endl; - auto newMarking = trans->fire(currentMarking); - std::cout << "\t\t\t target marking: " << *newMarking.getBitVector() << std::endl; - - findOrAddBitvectorToMarkings(*newMarking.getBitVector()); - - auto it = weights.find(markings.getValue(*newMarking.getBitVector())); - double currentWeight = 0; - if (it != weights.end()) { - currentWeight = weights.at(markings.getValue(*newMarking.getBitVector())); - } - currentWeight += trans->getWeight() / accWeight; - weights[markings.getValue(*newMarking.getBitVector())] = currentWeight; - } - - addValuesToBuilder(weights); - } - } - - template - void ExplicitGspnModelBuilder::addRowForTimedTransitions(std::vector>> const& enabledTimedTransitions, storm::gspn::Marking const& currentMarking, double const& accRate) { - std::map::cmpByIndex> rates; - for (auto& trans : enabledTimedTransitions) { - std::cout << "\t\ttransname: " << trans->getName() << std::endl; - auto newMarking = trans->fire(currentMarking); - std::cout << "\t\t\t target marking: " << *newMarking.getBitVector() << std::endl; - - findOrAddBitvectorToMarkings(*newMarking.getBitVector()); - - auto it = rates.find(markings.getValue(*newMarking.getBitVector())); - double currentWeightRate = 0; - if (it != rates.end()) { - currentWeightRate = rates.at(markings.getValue(*newMarking.getBitVector())); - } - currentWeightRate += trans->getRate() / accRate; - rates[markings.getValue(*newMarking.getBitVector())] = currentWeightRate; - - } - - addValuesToBuilder(rates); - } - - template - void ExplicitGspnModelBuilder::addValuesToBuilder(std::map::cmpByIndex> const& values) { - for (auto& it : values) { - std::cout << "\t\tadd value \"" << it.second << "\" to " << getBitvector(it.first) << std::endl; - builder.addNextValue(currentRowIndex, it.first, it.second); - } - } - - template - std::vector>>> ExplicitGspnModelBuilder::partitonEnabledImmediateTransitions( - storm::gspn::Marking const& marking, - std::vector>> const& enabledImmediateTransitions) { - decltype(partitonEnabledImmediateTransitions(marking, enabledImmediateTransitions)) result; - - std::vector>> weightedTransitions; - - for (auto& trans : enabledImmediateTransitions) { - if (trans->noWeightAttached()) { - decltype(weightedTransitions) singleton; - singleton.push_back(trans); - result.push_back(singleton); - } else { - weightedTransitions.push_back(trans); - } - } - - if (weightedTransitions.size() != 0) { - result.push_back(weightedTransitions); - } - - return result; - } - - template - double ExplicitGspnModelBuilder::getAccumulatedWeight(std::vector>> const& vector) const { - double result = 0; - - for (auto &trans : vector) { - result += trans->getWeight(); - } - - return result; - } - - template - void ExplicitGspnModelBuilder::computeCapacities(storm::gspn::GSPN const& gspn) { - uint_fast64_t sum = 0; - for (auto& place : gspn.getPlaces()) {//TODO - numberOfBits[place.getID()] = 1; - sum += numberOfBits[place.getID()]; - } - - // compute next multiple of 64 - uint_fast64_t rem = sum % 64; - numberOfTotalBits = sum + 64 - rem; - } - - template - std::vector>> ExplicitGspnModelBuilder::getEnabledTimedTransition( - storm::gspn::Marking const& marking) { - std::vector>>result; - - uint_fast64_t highestSeenPriority = 0; - - for (auto& trans_ptr : gspn.getTimedTransitions()) { - if (trans_ptr->isEnabled(marking)) { - if (trans_ptr->getPriority() > highestSeenPriority) { - highestSeenPriority = trans_ptr->getPriority(); - result.clear(); - } - result.push_back(trans_ptr); - } - } - - return result; - } - - template - std::vector>> ExplicitGspnModelBuilder::getEnabledImmediateTransition( - storm::gspn::Marking const& marking) { - std::vector>>result; - - uint_fast64_t highestSeenPriority = 0; - - for (auto& trans_ptr : gspn.getImmediateTransitions()) { - if (trans_ptr->isEnabled(marking)) { - if (trans_ptr->getPriority() > highestSeenPriority) { - highestSeenPriority = trans_ptr->getPriority(); - result.clear(); - } - result.push_back(trans_ptr); - } - } - - return result; - } - - template - double ExplicitGspnModelBuilder::getAccumulatedRate(std::vector>> const& vector) { - double result = 0; - for (auto trans_ptr : vector) { - result += trans_ptr->getRate(); - } - - return result; - } - - template - storm::storage::BitVector ExplicitGspnModelBuilder::getBitvector(uint_fast64_t const& index) { - for (auto it = markings.begin(); it != markings.end(); ++it) { - if (std::get<1>(*it) == index) { - return std::get<0>(*it); - } - } - return storm::storage::BitVector(); - } - - template - uint_fast64_t ExplicitGspnModelBuilder::findOrAddBitvectorToMarkings(storm::storage::BitVector const &bitvector) { - auto index = markings.findOrAdd(bitvector, nextRowGroupIndex); - - if (index == nextRowGroupIndex) { - // bitvector was not already in the map - ++nextRowGroupIndex; - // bitvector was also never in the todo list - todo.push_back(std::make_shared(bitvector)); - } - return index; - } - - template - storm::models::sparse::StateLabeling ExplicitGspnModelBuilder::getStateLabeling() const { - storm::models::sparse::StateLabeling labeling(markings.size()); - - std::map idToName; - for (auto& place : gspn.getPlaces()) { - idToName[place.getID()] = place.getName(); - labeling.addLabel(place.getName()); - } - - auto it = markings.begin(); - for ( ; it != markings.end() ; ++it) { - auto bitvector = std::get<0>(*it); - storm::gspn::Marking marking(gspn.getNumberOfPlaces(), numberOfBits, bitvector); - for (auto i = 0; i < marking.getNumberOfPlaces(); i++) { - if (marking.getNumberOfTokensAt(i) > 0) { - std::cout << i << std::endl; - labeling.addLabelToState(idToName.at(i), i); - } - } - } - - return labeling; - } - - template class ExplicitGspnModelBuilder; - } -} +//#include "src/builder/ExplicitGspnModelBuilder.h" +// +//#include "src/models/sparse/StandardRewardModel.h" +// +//#include "src/utility/macros.h" +//#include "src/exceptions/NotImplementedException.h" +//#include "src/storage/expressions/ExpressionManager.h" +//#include "src/parser/FormulaParser.h" +//#include "src/storage/expressions/ExpressionEvaluator.h" +// +//namespace storm { +// namespace builder { +// +// template +// storm::models::sparse::MarkovAutomaton ExplicitGspnModelBuilder::translateGspn(storm::gspn::GSPN const& gspn, std::string const& formula) { +// // set the given gspn and compute the limits of the net +// this->gspn = gspn; +// computeCapacities(gspn); +// +// // markings maps markings to their corresponding rowgroups (indices) +// markings = storm::storage::BitVectorHashMap(numberOfTotalBits, 100); +// builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, true); +// +// // add initial marking to todo list +// auto bitvector = gspn.getInitialMarking(numberOfBits, numberOfTotalBits)->getBitVector(); +// findOrAddBitvectorToMarkings(*bitvector); +// currentRowIndex = 0; +// +// // vector marking markovian states (vector contains an 1 if the state is markovian) +// storm::storage::BitVector markovianStates(0); +// +// // vector containing the exit rates for the markovian states +// std::vector exitRates; +// +// +// while (!todo.empty()) { +// // take next element from the todo list +// auto currentBitvector = todo.front(); +// todo.pop_front(); +// auto currentMarking = storm::gspn::Marking(gspn.getNumberOfPlaces(), numberOfBits, *currentBitvector); +// +// // increment list of states by one +// markovianStates.resize(markovianStates.size() + 1, 0); +// +// // create new row group for the current marking +// builder.newRowGroup(markings.getValue(*currentBitvector)); +// +// std::cout << "work on: " << *currentBitvector << std::endl; +// +// auto enabledImmediateTransitions = getEnabledImmediateTransition(currentMarking); +// if (!enabledImmediateTransitions.empty()) { +// markovianStates.set(currentRowIndex, 0); +// exitRates.push_back(0); +// +// auto partitions = partitonEnabledImmediateTransitions(currentMarking, enabledImmediateTransitions); +// addRowForPartitions(partitions, currentMarking); +// } else { +// +// auto enabledTimedTransitions = getEnabledTimedTransition(currentMarking); +// if (!enabledTimedTransitions.empty()) { +// markovianStates.set(currentRowIndex, 1); +// +// auto accRate = getAccumulatedRate(enabledTimedTransitions); +// std::cout << "\t\tacc. rate: " << accRate << std::endl; +// exitRates.push_back(accRate); +// +// addRowForTimedTransitions(enabledTimedTransitions, currentMarking, accRate); +// } else { +// markovianStates.set(currentRowIndex, 1); +// } +// } +// ++currentRowIndex; +// } +// +// auto matrix = builder.build(); +// +// // create expression manager and add variables from the gspn +// auto expressionManager = std::make_shared(); +// for (auto& place : gspn.getPlaces()) { +// expressionManager->declareIntegerVariable(place.getName()); +// } +// +// // parse formula +// storm::parser::FormulaParser formulaParser(expressionManager); +// auto formulaPtr = formulaParser.parseSingleFormulaFromString(formula); +// auto atomicFormulas = formulaPtr->getAtomicExpressionFormulas(); +// +// // create empty state labeling +// storm::models::sparse::StateLabeling labeling(markings.size()); +// storm::expressions::ExpressionEvaluator expressionEvaluator(*expressionManager); +// +// std::cout << std::endl; +// std::cout << "build labeling:" << std::endl; +// for (auto& atomicFormula : atomicFormulas) { +// std::cout << atomicFormula; +// auto label = atomicFormula->toString(); +// labeling.addLabel(label); +// +// for (auto statePair : markings) { +// auto marking = storm::gspn::Marking(gspn.getNumberOfPlaces(), numberOfBits, statePair.first); +// for (auto& place : gspn.getPlaces()) { +// auto variable = expressionManager->getVariable(place.getName()); +// expressionEvaluator.setIntegerValue(variable, marking.getNumberOfTokensAt(place.getID())); +// } +// bool hold = expressionEvaluator.asBool(atomicFormula->getExpression()); +// if (hold) { +// labeling.addLabelToState(label, statePair.second); +// } +// } +// +// } +// +// //auto labeling = getStateLabeling(); +// +// return storm::models::sparse::MarkovAutomaton(matrix, labeling, markovianStates, exitRates); +// } +// +// template +// void ExplicitGspnModelBuilder::addRowForPartitions(std::vector>>> const& partitions, storm::gspn::Marking const& currentMarking) { +// for (auto& partition : partitions) { +// std::cout << "\tnew partition:" << std::endl; +// auto accWeight = getAccumulatedWeight(partition); +// std::cout << "\t\tacc. weight: " << accWeight << std::endl; +// +// std::map::cmpByIndex> weights; +// for (auto& trans : partition) { +// std::cout << "\t\ttransname: " << trans.getName() << std::endl; +// auto newMarking = trans.fire(currentMarking); +// std::cout << "\t\t\t target marking: " << *newMarking.getBitVector() << std::endl; +// +// findOrAddBitvectorToMarkings(*newMarking.getBitVector()); +// +// auto it = weights.find(markings.getValue(*newMarking.getBitVector())); +// double currentWeight = 0; +// if (it != weights.end()) { +// currentWeight = weights.at(markings.getValue(*newMarking.getBitVector())); +// } +// currentWeight += trans.getWeight() / accWeight; +// weights[markings.getValue(*newMarking.getBitVector())] = currentWeight; +// } +// +// addValuesToBuilder(weights); +// } +// } +// +// template +// void ExplicitGspnModelBuilder::addRowForTimedTransitions(std::vector>> const& enabledTimedTransitions, storm::gspn::Marking const& currentMarking, double const& accRate) { +// std::map::cmpByIndex> rates; +// for (auto& trans : enabledTimedTransitions) { +// std::cout << "\t\ttransname: " << trans.getName() << std::endl; +// auto newMarking = trans.fire(currentMarking); +// std::cout << "\t\t\t target marking: " << *newMarking.getBitVector() << std::endl; +// +// findOrAddBitvectorToMarkings(*newMarking.getBitVector()); +// +// auto it = rates.find(markings.getValue(*newMarking.getBitVector())); +// double currentWeightRate = 0; +// if (it != rates.end()) { +// currentWeightRate = rates.at(markings.getValue(*newMarking.getBitVector())); +// } +// currentWeightRate += trans.getRate() / accRate; +// rates[markings.getValue(*newMarking.getBitVector())] = currentWeightRate; +// +// } +// +// addValuesToBuilder(rates); +// } +// +// template +// void ExplicitGspnModelBuilder::addValuesToBuilder(std::map::cmpByIndex> const& values) { +// for (auto& it : values) { +// std::cout << "\t\tadd value \"" << it.second << "\" to " << getBitvector(it.first) << std::endl; +// builder.addNextValue(currentRowIndex, it.first, it.second); +// } +// } +// +// template +// std::vector>>> ExplicitGspnModelBuilder::partitonEnabledImmediateTransitions( +// storm::gspn::Marking const& marking, +// std::vector>> const& enabledImmediateTransitions) { +// decltype(partitonEnabledImmediateTransitions(marking, enabledImmediateTransitions)) result; +// +// std::vector>> weightedTransitions; +// +// for (auto& trans : enabledImmediateTransitions) { +// if (trans.noWeightAttached()) { +// decltype(weightedTransitions) singleton; +// singleton.push_back(trans); +// result.push_back(singleton); +// } else { +// weightedTransitions.push_back(trans); +// } +// } +// +// if (weightedTransitions.size() != 0) { +// result.push_back(weightedTransitions); +// } +// +// return result; +// } +// +// template +// double ExplicitGspnModelBuilder::getAccumulatedWeight(std::vector>> const& vector) const { +// double result = 0; +// +// for (auto &trans : vector) { +// result += trans.getWeight(); +// } +// +// return result; +// } +// +// template +// void ExplicitGspnModelBuilder::computeCapacities(storm::gspn::GSPN const& gspn) { +// uint_fast64_t sum = 0; +// for (auto& place : gspn.getPlaces()) {//TODO +// numberOfBits[place.getID()] = 1; +// sum += numberOfBits[place.getID()]; +// } +// +// // compute next multiple of 64 +// uint_fast64_t rem = sum % 64; +// numberOfTotalBits = sum + 64 - rem; +// } +// +// template +// std::vector>> ExplicitGspnModelBuilder::getEnabledTimedTransition( +// storm::gspn::Marking const& marking) { +// std::vector>>result; +// +// uint_fast64_t highestSeenPriority = 0; +// +// for (auto& trans : gspn.getTimedTransitions()) { +// if (trans.isEnabled(marking)) { +// if (trans.getPriority() > highestSeenPriority) { +// highestSeenPriority = trans.getPriority(); +// result.clear(); +// } +// result.push_back(trans); +// } +// } +// +// return result; +// } +// +// template +// std::vector>> ExplicitGspnModelBuilder::getEnabledImmediateTransition( +// storm::gspn::Marking const& marking) { +// std::vector>>result; +// +// uint_fast64_t highestSeenPriority = 0; +// +// for (auto& trans : gspn.getImmediateTransitions()) { +// if (trans.isEnabled(marking)) { +// if (trans.getPriority() > highestSeenPriority) { +// highestSeenPriority = trans.getPriority(); +// result.clear(); +// } +// result.push_back(trans); +// } +// } +// +// return result; +// } +// +// template +// double ExplicitGspnModelBuilder::getAccumulatedRate(std::vector>> const& vector) { +// double result = 0; +// for (auto trans : vector) { +// result += trans.getRate(); +// } +// +// return result; +// } +// +// template +// storm::storage::BitVector ExplicitGspnModelBuilder::getBitvector(uint_fast64_t const& index) { +// for (auto it = markings.begin(); it != markings.end(); ++it) { +// if (std::get<1>(*it) == index) { +// return std::get<0>(*it); +// } +// } +// return storm::storage::BitVector(); +// } +// +// template +// uint_fast64_t ExplicitGspnModelBuilder::findOrAddBitvectorToMarkings(storm::storage::BitVector const &bitvector) { +// auto index = markings.findOrAdd(bitvector, nextRowGroupIndex); +// +// if (index == nextRowGroupIndex) { +// // bitvector was not already in the map +// ++nextRowGroupIndex; +// // bitvector was also never in the todo list +// todo.push_back(std::make_shared(bitvector)); +// } +// return index; +// } +// +// template +// storm::models::sparse::StateLabeling ExplicitGspnModelBuilder::getStateLabeling() const { +// storm::models::sparse::StateLabeling labeling(markings.size()); +// +// std::map idToName; +// for (auto& place : gspn.getPlaces()) { +// idToName[place.getID()] = place.getName(); +// labeling.addLabel(place.getName()); +// } +// +// auto it = markings.begin(); +// for ( ; it != markings.end() ; ++it) { +// auto bitvector = std::get<0>(*it); +// storm::gspn::Marking marking(gspn.getNumberOfPlaces(), numberOfBits, bitvector); +// for (auto i = 0; i < marking.getNumberOfPlaces(); i++) { +// if (marking.getNumberOfTokensAt(i) > 0) { +// std::cout << i << std::endl; +// labeling.addLabelToState(idToName.at(i), i); +// } +// } +// } +// +// return labeling; +// } +// +// template class ExplicitGspnModelBuilder; +// } +//} diff --git a/src/builder/ExplicitGspnModelBuilder.h b/src/builder/ExplicitGspnModelBuilder.h index 38ba60f0b..6173820fb 100644 --- a/src/builder/ExplicitGspnModelBuilder.h +++ b/src/builder/ExplicitGspnModelBuilder.h @@ -1,172 +1,172 @@ -#ifndef STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ -#define STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ - -#include - -#include "src/models/sparse/MarkovAutomaton.h" -#include "src/models/sparse/StandardRewardModel.h" -#include "src/storage/BitVector.h" -#include "src/storage/BitVectorHashMap.h" -#include "src/storage/gspn/GSPN.h" -#include "src/storage/gspn/ImmediateTransition.h" -#include "src/storage/gspn/TimedTransition.h" - -namespace storm { - namespace builder { - - /*! - * This class provides the facilities for building an markov automaton. - */ - template - class ExplicitGspnModelBuilder { - public: - - /*! - * Builds an MarkovAutomaton from the given GSPN. - * - * @param gspn The gspn whose semantic is covered by the MarkovAutomaton - * @return The resulting MarkovAutomaton - */ - storm::models::sparse::MarkovAutomaton translateGspn(storm::gspn::GSPN const& gspn, std::string const& formula); - private: - - /*! - * Add for each partition a new row in the probability matrix. - * - * @param partitions The partitioned immediate transitions. - * @param currentMarking The current marking which is considered at the moment. - */ - void addRowForPartitions(std::vector>>> const& partitions, storm::gspn::Marking const& currentMarking); - - - /*! - * Add row for a markovian state. - * - * @param enabledTimedTransitions List of enabled timed transitions. - * @param currentMarking The current marking which is considered at the moment. - * @param accRate The sum of all rates of the enabled timed transisitons - */ - void addRowForTimedTransitions(std::vector>> const& enabledTimedTransitions, storm::gspn::Marking const& currentMarking, double const& accRate); - - /*! - * Struct for comparing unsigned integer for maps - */ - struct cmpByIndex { - bool operator()(const uint_fast64_t &a, const uint_fast64_t &b) const { - return a < b; - } - }; - - /*! - * This method insert the values from a map into the matrix - * - * @param values The values which are inserted - */ - void addValuesToBuilder(std::map::cmpByIndex> const& values); - - - /*! - * This method partitions all enabled immediate transitions w.r.t. a marking. - * All enabled weighted immediate transitions are in one vector. Between these transitions - * is chosen probabilistically by the weights. - * - * All other enabled non-weighted immediate transitions are in an singleton vector. - * Between different vectors is chosen non-deterministically. - * - * @param marking The current marking which is considered. - * @param enabledImmediateTransistions A vector of enabled immediate transitions. - * @return The vector of vectors which is described above. - */ - std::vector>>> partitonEnabledImmediateTransitions(storm::gspn::Marking const& marking, std::vector>> const& enabledImmediateTransitions); - - /*! - * Computes the accumulated weight of immediate transisions which are stored in a list. - * - * @param vector List of immediate transisitions. - */ - double getAccumulatedWeight(std::vector>> const& vector) const; - - /*! - * Compute the upper bound for the number of tokens in each place. - * Also computes the number of bits which are used to store a marking. - * - * @param gspn The corresponding gspn. - */ - void computeCapacities(storm::gspn::GSPN const& gspn); - - /*! - * Returns the vector of enabled timed transition with the highest priority. - * - * - * @param marking The current marking which is considered. - * @return The vector of enabled timed transitions. - */ - std::vector>> getEnabledTimedTransition( - storm::gspn::Marking const& marking); - - /*! - * Returns the vector of active immediate transition with the highest priority. - * - * @param marking The current marking which is considered. - * @return The vector of enabled immediate transitions. - */ - std::vector>> getEnabledImmediateTransition( - storm::gspn::Marking const& marking); - - /*! - * Computes the accumulated rate of a vector of timed transitions. - * - * @param vector The vector of timed transitions. - * @return The accumulated rate. - */ - double getAccumulatedRate(std::vector>> const& vector); - - // is only needed for debugging purposes - // since markings is injective, we can determine the bitvector - storm::storage::BitVector getBitvector(uint_fast64_t const& index); - - /*! - * Adds the bitvector to the marking-map. - * If the bitvector corresponds to a new marking the bitvector is added to the todo list. - * - * @return The rowGroup index for the bitvector. - */ - uint_fast64_t findOrAddBitvectorToMarkings(storm::storage::BitVector const& bitvector); - - /*! - * Computes the state labeling and returns it. - * Every state is labeled with its name. - * - * @return The computed state labeling. - */ - storm::models::sparse::StateLabeling getStateLabeling() const; - - - // contains the number of bits which are used the store the number of tokens at each place - std::map numberOfBits; - - // contains the number of bits used to create markings - uint_fast64_t numberOfTotalBits; - - // maps bitvectors (markings w.r.t. the capacity) to their rowgroup - storm::storage::BitVectorHashMap markings = storm::storage::BitVectorHashMap(64, 1); - - // a list of markings for which the outgoing edges need to be computed - std::deque> todo; - - //the gspn which is transformed - storm::gspn::GSPN gspn; - - // the next index for a new rowgroup - uint_fast64_t nextRowGroupIndex = 0; - - // builder object which is used to create the probability matrix - storm::storage::SparseMatrixBuilder builder; - - // contains the current row index during the computation - uint_fast64_t currentRowIndex; - }; - } -} - -#endif //STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ +//#ifndef STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ +//#define STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ +// +//#include +// +//#include "src/models/sparse/MarkovAutomaton.h" +//#include "src/models/sparse/StandardRewardModel.h" +//#include "src/storage/BitVector.h" +//#include "src/storage/BitVectorHashMap.h" +//#include "src/storage/gspn/GSPN.h" +//#include "src/storage/gspn/ImmediateTransition.h" +//#include "src/storage/gspn/TimedTransition.h" +// +//namespace storm { +// namespace builder { +// +// /*! +// * This class provides the facilities for building an markov automaton. +// */ +// template +// class ExplicitGspnModelBuilder { +// public: +// +// /*! +// * Builds an MarkovAutomaton from the given GSPN. +// * +// * @param gspn The gspn whose semantic is covered by the MarkovAutomaton +// * @return The resulting MarkovAutomaton +// */ +// storm::models::sparse::MarkovAutomaton translateGspn(storm::gspn::GSPN const& gspn, std::string const& formula); +// private: +// +// /*! +// * Add for each partition a new row in the probability matrix. +// * +// * @param partitions The partitioned immediate transitions. +// * @param currentMarking The current marking which is considered at the moment. +// */ +// void addRowForPartitions(std::vector>>> const& partitions, storm::gspn::Marking const& currentMarking); +// +// +// /*! +// * Add row for a markovian state. +// * +// * @param enabledTimedTransitions List of enabled timed transitions. +// * @param currentMarking The current marking which is considered at the moment. +// * @param accRate The sum of all rates of the enabled timed transisitons +// */ +// void addRowForTimedTransitions(std::vector>> const& enabledTimedTransitions, storm::gspn::Marking const& currentMarking, double const& accRate); +// +// /*! +// * Struct for comparing unsigned integer for maps +// */ +// struct cmpByIndex { +// bool operator()(const uint_fast64_t &a, const uint_fast64_t &b) const { +// return a < b; +// } +// }; +// +// /*! +// * This method insert the values from a map into the matrix +// * +// * @param values The values which are inserted +// */ +// void addValuesToBuilder(std::map::cmpByIndex> const& values); +// +// +// /*! +// * This method partitions all enabled immediate transitions w.r.t. a marking. +// * All enabled weighted immediate transitions are in one vector. Between these transitions +// * is chosen probabilistically by the weights. +// * +// * All other enabled non-weighted immediate transitions are in an singleton vector. +// * Between different vectors is chosen non-deterministically. +// * +// * @param marking The current marking which is considered. +// * @param enabledImmediateTransistions A vector of enabled immediate transitions. +// * @return The vector of vectors which is described above. +// */ +// std::vector>>> partitonEnabledImmediateTransitions(storm::gspn::Marking const& marking, std::vector>> const& enabledImmediateTransitions); +// +// /*! +// * Computes the accumulated weight of immediate transisions which are stored in a list. +// * +// * @param vector List of immediate transisitions. +// */ +// double getAccumulatedWeight(std::vector>> const& vector) const; +// +// /*! +// * Compute the upper bound for the number of tokens in each place. +// * Also computes the number of bits which are used to store a marking. +// * +// * @param gspn The corresponding gspn. +// */ +// void computeCapacities(storm::gspn::GSPN const& gspn); +// +// /*! +// * Returns the vector of enabled timed transition with the highest priority. +// * +// * +// * @param marking The current marking which is considered. +// * @return The vector of enabled timed transitions. +// */ +// std::vector>> getEnabledTimedTransition( +// storm::gspn::Marking const& marking); +// +// /*! +// * Returns the vector of active immediate transition with the highest priority. +// * +// * @param marking The current marking which is considered. +// * @return The vector of enabled immediate transitions. +// */ +// std::vector>> getEnabledImmediateTransition( +// storm::gspn::Marking const& marking); +// +// /*! +// * Computes the accumulated rate of a vector of timed transitions. +// * +// * @param vector The vector of timed transitions. +// * @return The accumulated rate. +// */ +// double getAccumulatedRate(std::vector>> const& vector); +// +// // is only needed for debugging purposes +// // since markings is injective, we can determine the bitvector +// storm::storage::BitVector getBitvector(uint_fast64_t const& index); +// +// /*! +// * Adds the bitvector to the marking-map. +// * If the bitvector corresponds to a new marking the bitvector is added to the todo list. +// * +// * @return The rowGroup index for the bitvector. +// */ +// uint_fast64_t findOrAddBitvectorToMarkings(storm::storage::BitVector const& bitvector); +// +// /*! +// * Computes the state labeling and returns it. +// * Every state is labeled with its name. +// * +// * @return The computed state labeling. +// */ +// storm::models::sparse::StateLabeling getStateLabeling() const; +// +// +// // contains the number of bits which are used the store the number of tokens at each place +// std::map numberOfBits; +// +// // contains the number of bits used to create markings +// uint_fast64_t numberOfTotalBits; +// +// // maps bitvectors (markings w.r.t. the capacity) to their rowgroup +// storm::storage::BitVectorHashMap markings = storm::storage::BitVectorHashMap(64, 1); +// +// // a list of markings for which the outgoing edges need to be computed +// std::deque> todo; +// +// //the gspn which is transformed +// storm::gspn::GSPN gspn; +// +// // the next index for a new rowgroup +// uint_fast64_t nextRowGroupIndex = 0; +// +// // builder object which is used to create the probability matrix +// storm::storage::SparseMatrixBuilder builder; +// +// // contains the current row index during the computation +// uint_fast64_t currentRowIndex; +// }; +// } +//} +// +//#endif //STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_ diff --git a/src/builder/JaniGSPNBuilder.h b/src/builder/JaniGSPNBuilder.h index bfa0d663f..e7da0e776 100644 --- a/src/builder/JaniGSPNBuilder.h +++ b/src/builder/JaniGSPNBuilder.h @@ -18,7 +18,7 @@ namespace storm { } } - bool setIgnoreWeights(bool ignore = true) { + void setIgnoreWeights(bool ignore = true) { ignoreWeights = ignore; } @@ -61,17 +61,17 @@ namespace storm { storm::expressions::Expression guard = expressionManager->boolean(true); for (auto const& trans : gspn.getImmediateTransitions()) { - if (ignoreWeights || trans->noWeightAttached()) { + if (ignoreWeights || trans.noWeightAttached()) { std::vector assignments; - for (auto const& inPlace : trans->getInputPlaces()) { - guard = guard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(*inPlace)); - assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans->getInputArcMultiplicity(*inPlace)) ); + for (auto const& inPlace : trans.getInputPlaces()) { + guard = guard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans.getInputArcMultiplicity(*inPlace)); + assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans.getInputArcMultiplicity(*inPlace)) ); } - for (auto const& inhibPlace : trans->getInhibitionPlaces()) { - guard = guard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(*inhibPlace)); + for (auto const& inhibPlace : trans.getInhibitionPlaces()) { + guard = guard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans.getInhibitionArcMultiplicity(*inhibPlace)); } - for (auto const& outputPlace : trans->getOutputPlaces()) { - assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(*outputPlace)) ); + for (auto const& outputPlace : trans.getOutputPlaces()) { + assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans.getOutputArcMultiplicity(*outputPlace)) ); } storm::jani::OrderedAssignments oa(assignments); storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa); @@ -89,41 +89,41 @@ namespace storm { // Compute enabled weight expression. storm::expressions::Expression totalWeight = expressionManager->rational(0.0); for (auto const& trans : gspn.getImmediateTransitions()) { - if (trans->noWeightAttached()) { + if (trans.noWeightAttached()) { continue; } storm::expressions::Expression destguard = expressionManager->boolean(true); - for (auto const& inPlace : trans->getInputPlaces()) { - destguard = destguard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(*inPlace)); + for (auto const& inPlace : trans.getInputPlaces()) { + destguard = destguard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans.getInputArcMultiplicity(*inPlace)); } - for (auto const& inhibPlace : trans->getInhibitionPlaces()) { - destguard = destguard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(*inhibPlace)); + for (auto const& inhibPlace : trans.getInhibitionPlaces()) { + destguard = destguard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans.getInhibitionArcMultiplicity(*inhibPlace)); } - totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans->getWeight()), expressionManager->rational(0.0)); + totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0)); } totalWeight = totalWeight.simplify(); for (auto const& trans : gspn.getImmediateTransitions()) { - if (trans->noWeightAttached()) { + if (trans.noWeightAttached()) { continue; } storm::expressions::Expression destguard = expressionManager->boolean(true); std::vector assignments; - for (auto const& inPlace : trans->getInputPlaces()) { - destguard = destguard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(*inPlace)); - assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans->getInputArcMultiplicity(*inPlace)) ); + for (auto const& inPlace : trans.getInputPlaces()) { + destguard = destguard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans.getInputArcMultiplicity(*inPlace)); + assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans.getInputArcMultiplicity(*inPlace)) ); } - for (auto const& inhibPlace : trans->getInhibitionPlaces()) { - destguard = destguard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(*inhibPlace)); + for (auto const& inhibPlace : trans.getInhibitionPlaces()) { + destguard = destguard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans.getInhibitionArcMultiplicity(*inhibPlace)); } - for (auto const& outputPlace : trans->getOutputPlaces()) { - assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(*outputPlace)) ); + for (auto const& outputPlace : trans.getOutputPlaces()) { + assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans.getOutputArcMultiplicity(*outputPlace)) ); } destguard = destguard.simplify(); guard = guard || destguard; storm::jani::OrderedAssignments oa(assignments); - storm::jani::EdgeDestination dest(locId, storm::expressions::ite(destguard, (expressionManager->rational(trans->getWeight()) / totalWeight), expressionManager->rational(0.0)), oa); + storm::jani::EdgeDestination dest(locId, storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)), oa); weightedDestinations.push_back(dest); } storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, guard.simplify(), weightedDestinations); @@ -133,19 +133,19 @@ namespace storm { storm::expressions::Expression guard = expressionManager->boolean(true); std::vector assignments; - for (auto const& inPlace : trans->getInputPlaces()) { - guard = guard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(*inPlace)); - assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans->getInputArcMultiplicity(*inPlace)) ); + for (auto const& inPlace : trans.getInputPlaces()) { + guard = guard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans.getInputArcMultiplicity(*inPlace)); + assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans.getInputArcMultiplicity(*inPlace)) ); } - for (auto const& inhibPlace : trans->getInhibitionPlaces()) { - guard = guard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(*inhibPlace)); + for (auto const& inhibPlace : trans.getInhibitionPlaces()) { + guard = guard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans.getInhibitionArcMultiplicity(*inhibPlace)); } - for (auto const& outputPlace : trans->getOutputPlaces()) { - assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(*outputPlace)) ); + for (auto const& outputPlace : trans.getOutputPlaces()) { + assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans.getOutputArcMultiplicity(*outputPlace)) ); } storm::jani::OrderedAssignments oa(assignments); storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa); - storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans->getRate()), guard, {dest}); + storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans.getRate()), guard, {dest}); automaton.addEdge(e); } } diff --git a/src/parser/GreatSpnEditorProjectParser.cpp b/src/parser/GreatSpnEditorProjectParser.cpp new file mode 100644 index 000000000..2a55b4526 --- /dev/null +++ b/src/parser/GreatSpnEditorProjectParser.cpp @@ -0,0 +1,343 @@ +#include "GreatSpnEditorProjectParser.h" + + +#include + +#include "src/adapters/XercesAdapter.h" + +#include "src/exceptions/UnexpectedException.h" +#include "src/exceptions/WrongFormatException.h" +#include "src/utility/macros.h" + +namespace storm { + namespace parser { + storm::gspn::GSPN* GreatSpnEditorProjectParser::parse(xercesc::DOMElement const* elementRoot) { + if (storm::adapters::XMLtoString(elementRoot->getTagName()) == "project") { + GreatSpnEditorProjectParser p; + return p.parse(elementRoot); + } else { + // If the top-level node is not a "pnml" or "" node, then throw an exception. + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n"); + } + + + } + + void GreatSpnEditorProjectParser::traverseProjectElement(xercesc::DOMNode const* const node) { + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + if (name.compare("version") == 0 || + name.compare("name") == 0) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (name.compare("gspn") == 0) { + traverseGspnElement(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + void GreatSpnEditorProjectParser::traverseGspnElement(xercesc::DOMNode const* const node) { + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + if (name.compare("name") == 0) { + builder.setGspnName(storm::adapters::XMLtoString(attr->getNodeValue())); + } else if (name.compare("show-color-cmd") == 0 || + name.compare("show-fluid-cmd") == 0) { + // ignore node + } else { + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG( + "unknown attribute (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (name.compare("nodes") == 0) { + traverseNodesElement(child); + } else if (name.compare("edges") == 0) { + traverseEdgesElement(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + void GreatSpnEditorProjectParser::traverseNodesElement(xercesc::DOMNode const* const node) { + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (name.compare("place") == 0) { + traversePlaceElement(child); + } else if(name.compare("transition") == 0) { + traverseTransitionElement(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + void GreatSpnEditorProjectParser::traverseEdgesElement(xercesc::DOMNode const* const node) { + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (name.compare("arc") == 0) { + traverseArcElement(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + bool ignorePlaceAttribute(std::string const& name) { + // TODO we should probably not ignore x-servers but check that it is 0.5. + if ((name == "label-x") || (name == "label-y") || (name == "x") || (name == "y")) { + return true; + } + return false; + } + + + void GreatSpnEditorProjectParser::traversePlaceElement(xercesc::DOMNode const* const node) { + // traverse attributes + std::string placeName; + uint64_t initialTokens = 0; + + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + if (name.compare("name") == 0) { + placeName = storm::adapters::XMLtoString(attr->getNodeValue()); + } else if (name.compare("marking") == 0) { + initialTokens = std::stoull(storm::adapters::XMLtoString(attr->getNodeValue())); + } else if (ignorePlaceAttribute(name)) { + // ignore node + } else { + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG( + "unknown attribute (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + builder.addPlace(-1, initialTokens, placeName); + } + + bool ignoreTransitionAttribute(std::string const& name) { + // TODO we should probably not ignore x-servers but check that it is 0.5. + if ((name == "label-x") || (name == "label-y") || (name == "x") || (name == "y") || (name == "nservers-x")) { + return true; + } + return false; + } + + void GreatSpnEditorProjectParser::traverseTransitionElement(xercesc::DOMNode const* const node) { + std::string transitionName; + bool immediateTransition; + double rate = 1.0; // The default rate in GreatSPN. + + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + if (name.compare("name") == 0) { + transitionName = storm::adapters::XMLtoString(attr->getNodeValue()); + } else if (name.compare("type") == 0) { + if (storm::adapters::XMLtoString(attr->getNodeValue()).compare("EXP") == 0) { + immediateTransition = false; + } else { + immediateTransition = true; + } + } else if(name.compare("delay") == 0) { + rate = std::stod(storm::adapters::XMLtoString(attr->getNodeValue())); + } else if (ignoreTransitionAttribute(name)) { + // ignore node + } else { + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG( + "unknown attribute (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + if (immediateTransition) { + builder.addImmediateTransition(0, 0, transitionName); + } else { + builder.addTimedTransition(0, rate, transitionName); + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + bool ignoreArcAttribute(std::string const& name) { + if ((name == "mult-x") || (name == "mult-y") || (name == "mult-k")) { + return true; + } + return false; + } + + bool ignoreArcChild(std::string const& name) { + if (name == "point") { + return true; + } + return false; + } + + void GreatSpnEditorProjectParser::traverseArcElement(xercesc::DOMNode const* const node) { + std::string head = "____NOT_SET____"; + std::string tail = "____NOT_SET____"; + std::string kind = "____NOT_SET____"; + uint_fast64_t mult = 1; + + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + if (name.compare("head") == 0) { + head = storm::adapters::XMLtoString(attr->getNodeValue()); + } else if (name.compare("tail") == 0) { + tail = storm::adapters::XMLtoString(attr->getNodeValue()); + } else if (name.compare("kind") == 0) { + kind = storm::adapters::XMLtoString(attr->getNodeValue()); + } else if (name.compare("mult") == 0) { + mult = std::stoull(storm::adapters::XMLtoString(attr->getNodeValue())); + } else if (ignoreArcAttribute(name)) { + // ignore node + } else { + // Found node or attribute which is at the moment not handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG( + "unknown attribute (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + STORM_LOG_THROW(head.compare("____NOT_SET____") != 0, storm::exceptions::WrongFormatException, "Arc must have a head"); + STORM_LOG_THROW(tail.compare("____NOT_SET____") != 0, storm::exceptions::WrongFormatException, "Arc must have a tail"); + STORM_LOG_THROW(kind.compare("____NOT_SET____") != 0, storm::exceptions::WrongFormatException, "Arc must have a kind"); + + + if (kind.compare("INPUT") == 0) { + builder.addInputArc(head, tail, mult); + } else if (kind.compare("INHIBITOR") == 0) { + builder.addInhibitionArc(head, tail, mult); + } else if (kind.compare("OUTPUT") == 0) { + builder.addOutputArc(head, tail, mult); + } else { + // TODO error! + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if(ignoreArcChild(name)) { + // ignore + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + } +} + + diff --git a/src/parser/GreatSpnEditorProjectParser.h b/src/parser/GreatSpnEditorProjectParser.h new file mode 100644 index 000000000..90b8f4f04 --- /dev/null +++ b/src/parser/GreatSpnEditorProjectParser.h @@ -0,0 +1,42 @@ +#pragma once + +#include + +#include +#include + +#include "src/storage/gspn/GSPN.h" + +#include "src/storage/gspn/GspnBuilder.h" + +namespace storm { + namespace parser { + class GreatSpnEditorProjectParser { + + public: + + /*! + * Parses the given file into the GSPN. + * + * @param filename The name of the file to parse. + * @return The resulting GSPN. + */ + storm::gspn::GSPN* parse(xercesc::DOMElement const* elementRoot); + private: + void traverseProjectElement(xercesc::DOMNode const* const node); + + void traverseGspnElement(xercesc::DOMNode const* const node); + void traverseNodesElement(xercesc::DOMNode const* const node); + void traverseEdgesElement(xercesc::DOMNode const* const node); + + void traversePlaceElement(xercesc::DOMNode const* const node); + void traverseTransitionElement(xercesc::DOMNode const* const node); + void traverseArcElement(xercesc::DOMNode const* const node); + + + // the constructed gspn + storm::gspn::GspnBuilder builder; + + }; + } +} diff --git a/src/parser/GspnParser.cpp b/src/parser/GspnParser.cpp index e6bc79a27..bfd455356 100644 --- a/src/parser/GspnParser.cpp +++ b/src/parser/GspnParser.cpp @@ -1,25 +1,19 @@ -#include "src/parser/GspnParser.h" +#include "GspnParser.h" -#include - -#include -#include -#include +#include "src/adapters/XercesAdapter.h" #include "src/exceptions/UnexpectedException.h" #include "src/exceptions/WrongFormatException.h" -#include "src/storage/gspn/Place.h" -#include "src/storage/gspn/ImmediateTransition.h" #include "src/utility/macros.h" +#include "PnmlParser.h" +#include "GreatSpnEditorProjectParser.h" + namespace storm { namespace parser { - storm::gspn::GSPN const& GspnParser::parse(std::string const& filename) { - // initialize parser - newNode = 0; - gspn = storm::gspn::GSPN(); - - // initialize xercesc + + storm::gspn::GSPN* GspnParser::parse(std::string const& filename) { + // initialize xercesc try { xercesc::XMLPlatformUtils::Initialize(); } @@ -27,17 +21,17 @@ namespace storm { // Error occurred during the initialization process. Abort parsing since it is not possible. STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to initialize xercesc\n"); } - + auto parser = new xercesc::XercesDOMParser(); parser->setValidationScheme(xercesc::XercesDOMParser::Val_Always); parser->setDoNamespaces(false); parser->setDoSchema(false); parser->setLoadExternalDTD(false); parser->setIncludeIgnorableWhitespace(false); - + auto errHandler = (xercesc::ErrorHandler*) new xercesc::HandlerBase(); parser->setErrorHandler(errHandler); - + // parse file try { parser->parse(filename.c_str()); @@ -61,865 +55,30 @@ namespace storm { // or the parser run into a problem. STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to parse pnml file.\n"); } - + // build gspn by traversing the DOM object parser->getDocument()->normalizeDocument(); xercesc::DOMElement* elementRoot = parser->getDocument()->getDocumentElement(); - - if (getName(elementRoot).compare("pnml") == 0) { - traversePnmlElement(elementRoot); - } else if (getName(elementRoot).compare("project") == 0) { - traverseProjectElement(elementRoot); + + if (storm::adapters::XMLtoString(elementRoot->getTagName()) == "pnml") { + PnmlParser p; + return p.parse(elementRoot); + } else if (storm::adapters::XMLtoString(elementRoot->getTagName()) == "project") { + GreatSpnEditorProjectParser p; + return p.parse(elementRoot); } else { // If the top-level node is not a "pnml" or "" node, then throw an exception. STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n"); } - - - - - + + + + + // clean up delete parser; delete errHandler; xercesc::XMLPlatformUtils::Terminate(); - - return gspn; - } - - void GspnParser::traversePnmlElement(xercesc::DOMElement const* const element) { - // traverse attributes - for (uint_fast64_t i = 0; i < element->getAttributes()->getLength(); ++i) { - auto attr = element->getAttributes()->item(i); - auto name = getName(attr); - - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown attribute (node=pnml): " + name + "\n"); - } - - // traverse children - for (uint_fast64_t i = 0; i < element->getChildNodes()->getLength(); ++i) { - auto child = element->getChildNodes()->item(i); - auto name = getName(child); - - if (name.compare("net") == 0) { - traverseNetOrPage(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=pnml): " + name + "\n"); - } - } - } - - void GspnParser::traverseNetOrPage(xercesc::DOMNode const* const node) { - // traverse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - if (name.compare("id") == 0) { - gspn.setName(XMLtoString(attr->getNodeValue())); - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - - // traverse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - - if (name.compare("place") == 0) { - traversePlace(child); - } else if (name.compare("transition") == 0) { - traverseTransition(child); - } else if (name.compare("arc") == 0) { - traverseArc(child); - } else if (name.compare("page") == 0) { - // Some pnml files have a child named page. - // The page node has the same children like the net node (e.g., place, transition, arc) - traverseNetOrPage(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - } - - void GspnParser::traversePlace(xercesc::DOMNode const* const node) { - std::string placeName; - // the first entry is false if the corresponding information was not found in the pnml file - std::pair numberOfInitialTokens(false, defaultNumberOfInitialTokens); - std::pair capacity(false, defaultCapacity); - - // traverse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - if (name.compare("id") == 0) { - placeName = XMLtoString(attr->getNodeValue()); - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown attribute (node=place): " + name + "\n"); - } - } - - // traverse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - - if (name.compare("initialMarking") == 0) { - numberOfInitialTokens.first = true; - numberOfInitialTokens.second = traverseInitialMarking(child); - } else if(name.compare("capacity") == 0) { - capacity.first = true; - capacity.second = traverseCapacity(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("name") == 0 || - name.compare("graphics") == 0) { - // ignore these tags - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=place): " + name + "\n"); - } - } - - // build place and add it to the gspn - storm::gspn::Place place; - place.setName(placeName); - if (!numberOfInitialTokens.first) { - // no information about the number of initial tokens is found - // use the default number of initial tokens - STORM_PRINT_AND_LOG("unknown numberOfInitialTokens (place=" + placeName + ")\n"); - } - place.setNumberOfInitialTokens(numberOfInitialTokens.second); - if (!capacity.first) { - // no information about the capacity is found - // use default capacity - STORM_PRINT_AND_LOG("unknown capacity (place=" + placeName + ")\n"); - } - place.setCapacity(capacity.second); - place.setID(newNode); - ++newNode; - gspn.addPlace(place); - } - - void GspnParser::traverseTransition(xercesc::DOMNode const* const node) { - // the first entry is false if the corresponding information was not found in the pnml file - std::pair timed(false, defaultTransitionType); - std::pair value(false, defaultTransitionValue); - std::string id; - uint_fast64_t priority = defaultPriority; - - // parse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - if (name.compare("id") == 0) { - id = XMLtoString(attr->getNodeValue()); - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown attribute (node=transition): " + name + "\n"); - } - } - - // traverse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - - if (name.compare("rate") == 0) { - value.first = true; - value.second = traverseTransitionValue(child); - } else if (name.compare("timed") == 0) { - timed.first = true; - timed.second = traverseTransitionType(child); - } else if (name.compare("priority") == 0) { - priority = traversePriority(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("graphics") == 0 || - name.compare("name") == 0 || - name.compare("orientation") == 0) { - // ignore these tags - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=transition): " + name + "\n"); - } - } - - // build transition and add it to the gspn - if (!timed.first) { - // found unknown transition type - // abort parsing - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "unknown transition type (transition=" + id + ")\n"); - return; - } - - if (timed.second) { - storm::gspn::TimedTransition transition; - if (!value.first) { - // no information about the rate is found - // abort the parsing - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown transition rate (transition=" + id + ")\n"); - } - transition.setRate(std::stod(value.second)); - transition.setName(id); - transition.setPriority(priority); - gspn.addTimedTransition(transition); - } else { - storm::gspn::ImmediateTransition transition; - if (!value.first) { - // no information about the weight is found - // continue with the default weight - STORM_PRINT_AND_LOG("unknown transition weight (transition=" + id + ")\n"); - } - transition.setWeight(std::stod(value.second)); - transition.setName(id); - transition.setPriority(priority); - gspn.addImmediateTransition(transition); - } - } - - void GspnParser::traverseArc(xercesc::DOMNode const* const node) { - // the first entry is false if the corresponding information was not found in the pnml file - std::pair source(false, ""); - std::pair target(false, ""); - std::pair type(false, defaultArcType); - std::pair multiplicity(false, defaultMultiplicity); - std::string id; - - // parse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - if (name.compare("source") == 0) { - source.first = true; - source.second = XMLtoString(attr->getNodeValue()); - } else if (name.compare("target") == 0) { - target.first = true; - target.second = XMLtoString(attr->getNodeValue()); - } else if (name.compare("id") == 0) { - id = XMLtoString(attr->getNodeValue()); - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown attribute (node=arc): " + name + "\n"); - } - } - - // parse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("type") == 0) { - type.first = true; - type.second = traverseArcType(child); - } else if(name.compare("inscription") == 0) { - multiplicity.first = true; - multiplicity.second = traverseMultiplicity(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("graphics") == 0 || - name.compare("arcpath") == 0 || - name.compare("tagged") == 0) { - // ignore these tags - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=arc): " + name + "\n"); - } - } - - // check if all necessary information where stored in the pnml file - if (!source.first) { - // could not find start of the arc - // abort parsing - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc source (arc=" + id + ")\n"); - } - if (!target.first) { - // could not find the target of the arc - // abort parsing - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc target (arc=" + id + ")\n"); - } - if (!multiplicity.first) { - // no information about the multiplicity of the arc - // continue and use the default multiplicity - STORM_PRINT_AND_LOG("unknown multiplicity (node=arc): " + id + "\n"); - } - - //determine if it is an outgoing or incoming arc - { - auto place = gspn.getPlace(source.second); - auto trans = gspn.getTransition(target.second); - if (true == place.first && true == trans.first) { - if (!type.first) { - // no arc type found - // abport parsing - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "unknown arc type (arc=" + id + ")\n"); - } - - // incoming arc - if (type.second.compare("normal") == 0) { - trans.second->setInputArcMultiplicity(*place.second, multiplicity.second); - } else if (type.second.compare("inhibition") == 0) { - trans.second->setInhibitionArcMultiplicity(*place.second, multiplicity.second); - } else { - // unknown arc type - // abort parsing - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "unknown arc type (arc=" + id + ")\n"); - } - return; - } - } - { - auto trans = gspn.getTransition(source.second); - auto place = gspn.getPlace(target.second); - if (true == place.first && true == trans.first) { - // outgoing arc - trans.second->setOutputArcMultiplicity(*place.second, multiplicity.second); - return; - } - } - - // if we reach this line we could not find the corresponding place or transition - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc source or target (arc=" + id + ")\n"); - } - - std::string GspnParser::getName(xercesc::DOMNode *node) { - switch (node->getNodeType()) { - case xercesc::DOMNode::NodeType::ELEMENT_NODE: { - auto elementNode = (xercesc::DOMElement *) node; - return XMLtoString(elementNode->getTagName()); - } - case xercesc::DOMNode::NodeType::TEXT_NODE: { - return XMLtoString(node->getNodeValue()); - } - case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: { - return XMLtoString(node->getNodeName()); - } - default: { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown node type \n"); - return ""; - } - } - } - - uint_fast64_t GspnParser::traverseInitialMarking(xercesc::DOMNode const* const node) { - uint_fast64_t result = defaultNumberOfInitialTokens; - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("text") == 0) { - result = std::stoull(getName(child->getFirstChild())); - } else if (name.compare("value") == 0) { - auto value = getName(child->getFirstChild()); - value = value.substr(std::string("Default,").length()); - result = std::stoull(value); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("graphics") == 0) { - // ignore these tags - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=initialMarking): " + name + "\n"); - } - } - return result; - } - - int_fast64_t GspnParser::traverseCapacity(xercesc::DOMNode const* const node) { - int_fast64_t result= defaultCapacity; - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("value") == 0) { - auto value = getName(child->getFirstChild()); - if (value.find("Default,") == 0) { - value = value.substr(std::string("Default,").length()); - } - result = std::stoull(value); - } else if (name.compare("graphics") == 0) { - // ignore these nodes - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=capacity): " + name + "\n"); - } - } - return result; - } - - uint_fast64_t GspnParser::traverseMultiplicity(xercesc::DOMNode const* const node) { - uint_fast64_t result = defaultMultiplicity; - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("value") == 0) { - auto value = getName(child->getFirstChild()); - if (value.find("Default,") == 0) { - value = value.substr(std::string("Default,").length()); - } - result = std::stoull(value); - } else if (name.compare("graphics") == 0) { - // ignore these nodes - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=inscription): " + name + "\n"); - } - } - return result; - } - - - std::string GspnParser::traverseTransitionValue(xercesc::DOMNode const* const node) { - std::string result = defaultTransitionValue; - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("value") == 0) { - result = getName(child->getFirstChild()); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=rate): " + name + "\n"); - } - } - return result; - } - - bool GspnParser::traverseTransitionType(xercesc::DOMNode const* const node) { - bool result; - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("value") == 0) { - result = getName(child->getFirstChild()).compare("true") == 0 ? true : false; - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=timed): " + name + "\n"); - } - } - return result; - } - - std::string GspnParser::traverseArcType(xercesc::DOMNode const* const node) { - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - if (name.compare("value") == 0) { - return XMLtoString(attr->getNodeValue()); - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=type): " + name + "\n"); - } - } - return defaultArcType; - } - - uint_fast64_t GspnParser::traversePriority(xercesc::DOMNode const* const node) { - uint_fast64_t result = defaultPriority; - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - if (name.compare("text") == 0) { - result = std::stoull(getName(child->getFirstChild())); - } else if (name.compare("value") == 0) { - auto value = getName(child->getFirstChild()); - value = value.substr(std::string("Default,").length()); - result = std::stoull(value); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if (name.compare("graphics") == 0) { - // ignore these tags - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=priority): " + name + "\n"); - } - } - return result; - } - - std::string GspnParser::XMLtoString(const XMLCh *xmlString) { - char* tmp = xercesc::XMLString::transcode(xmlString); - auto result = std::string(tmp); - delete tmp; - return result; - } - - void GspnParser::traverseProjectElement(xercesc::DOMNode const* const node) { - // traverse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - if (name.compare("version") == 0 || - name.compare("name") == 0) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment not handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - - // traverse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - - if (name.compare("gspn") == 0) { - traverseGspnElement(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - } - - void GspnParser::traverseGspnElement(xercesc::DOMNode const* const node) { - // traverse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - if (name.compare("name") == 0) { - gspn.setName(XMLtoString(attr->getNodeValue())); - } else if (name.compare("show-color-cmd") == 0 || - name.compare("show-fluid-cmd") == 0) { - // ignore node - } else { - // Found node or attribute which is at the moment not handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG( - "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - - // traverse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - - if (name.compare("nodes") == 0) { - traverseNodesElement(child); - } else if (name.compare("edges") == 0) { - traverseEdgesElement(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - } - - void GspnParser::traverseNodesElement(xercesc::DOMNode const* const node) { - // traverse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - // Found node or attribute which is at the moment not handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - - // traverse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - - if (name.compare("place") == 0) { - traversePlaceElement(child); - } else if(name.compare("transition") == 0) { - traverseTransitionElement(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - } - - void GspnParser::traverseEdgesElement(xercesc::DOMNode const* const node) { - // traverse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - - // Found node or attribute which is at the moment not handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - - } - - // traverse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - - if (name.compare("arc") == 0) { - traverseArcElement(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - } - - bool ignorePlaceAttribute(std::string const& name) { - // TODO we should probably not ignore x-servers but check that it is 0.5. - if ((name == "label-x") || (name == "label-y") || (name == "x") || (name == "y")) { - return true; - } - return false; - } - - - void GspnParser::traversePlaceElement(xercesc::DOMNode const* const node) { - storm::gspn::Place place; - place.setID(newNode); - ++newNode; - - - // traverse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - if (name.compare("name") == 0) { - place.setName(XMLtoString(attr->getNodeValue())); - } else if (name.compare("marking") == 0) { - place.setNumberOfInitialTokens(std::stoull(XMLtoString(attr->getNodeValue()))); - } else if (ignorePlaceAttribute(name)) { - // ignore node - } else { - // Found node or attribute which is at the moment not handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG( - "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - - // traverse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - - if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - - gspn.addPlace(place); - } - - bool ignoreTransitionAttribute(std::string const& name) { - // TODO we should probably not ignore x-servers but check that it is 0.5. - if ((name == "label-x") || (name == "label-y") || (name == "x") || (name == "y") || (name == "nservers-x")) { - return true; - } - return false; - } - - void GspnParser::traverseTransitionElement(xercesc::DOMNode const* const node) { - std::string transitionName; - bool immediateTransition; - double rate = 1.0; // The default rate in GreatSPN. - - // traverse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - if (name.compare("name") == 0) { - transitionName = XMLtoString(attr->getNodeValue()); - } else if (name.compare("type") == 0) { - if (XMLtoString(attr->getNodeValue()).compare("EXP") == 0) { - immediateTransition = false; - } else { - immediateTransition = true; - } - } else if(name.compare("delay") == 0) { - rate = std::stod(XMLtoString(attr->getNodeValue())); - } else if (ignoreTransitionAttribute(name)) { - // ignore node - } else { - // Found node or attribute which is at the moment not handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG( - "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - - if (immediateTransition) { - auto transition = storm::gspn::ImmediateTransition(); - transition.setName(transitionName); - gspn.addImmediateTransition(transition); - } else { - auto transition = storm::gspn::TimedTransition(); - transition.setName(transitionName); - transition.setRate(rate); - gspn.addTimedTransition(transition); - } - - // traverse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - - if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - } - - bool ignoreArcAttribute(std::string const& name) { - if ((name == "mult-x") || (name == "mult-y") || (name == "mult-k")) { - return true; - } - return false; - } - - bool ignoreArcChild(std::string const& name) { - if (name == "point") { - return true; - } - return false; - } - - void GspnParser::traverseArcElement(xercesc::DOMNode const* const node) { - std::string head = "____NOT_SET____"; - std::string tail = "____NOT_SET____"; - std::string kind = "____NOT_SET____"; - uint_fast64_t mult = 1; - - // traverse attributes - for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { - auto attr = node->getAttributes()->item(i); - auto name = getName(attr); - - if (name.compare("head") == 0) { - head = XMLtoString(attr->getNodeValue()); - } else if (name.compare("tail") == 0) { - tail = XMLtoString(attr->getNodeValue()); - } else if (name.compare("kind") == 0) { - kind = XMLtoString(attr->getNodeValue()); - } else if (name.compare("mult") == 0) { - mult = std::stoull(XMLtoString(attr->getNodeValue())); - } else if (ignoreArcAttribute(name)) { - // ignore node - } else { - // Found node or attribute which is at the moment not handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG( - "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } - - STORM_LOG_THROW(head.compare("____NOT_SET____") != 0, storm::exceptions::WrongFormatException, "Arc must have a head"); - STORM_LOG_THROW(tail.compare("____NOT_SET____") != 0, storm::exceptions::WrongFormatException, "Arc must have a tail"); - STORM_LOG_THROW(kind.compare("____NOT_SET____") != 0, storm::exceptions::WrongFormatException, "Arc must have a kind"); - - - if (kind.compare("INPUT") == 0) { - auto transition = gspn.getTransition(head); - if (!transition.first) { - std::cout << "transition not found" << std::endl; - } - auto place = gspn.getPlace(tail); - if (!place.first) { - std::cout << "place not found" << std::endl; - } - 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); - } else if (kind.compare("OUTPUT") == 0) { - auto transition = gspn.getTransition(tail); - auto place = gspn.getPlace(head); - transition.second->setOutputArcMultiplicity(*place.second, mult); - } else { - // TODO error! - } - - // traverse children - for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { - auto child = node->getChildNodes()->item(i); - auto name = getName(child); - - if (std::all_of(name.begin(), name.end(), isspace)) { - // ignore node (contains only whitespace) - } else if(ignoreArcChild(name)) { - // ignore - } else { - // Found node or attribute which is at the moment nod handled by this parser. - // Notify the user and continue the parsing. - STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n"); - } - } } - - - - - - - - } } - diff --git a/src/parser/GspnParser.h b/src/parser/GspnParser.h index 81b28c40d..cec4c5f6f 100644 --- a/src/parser/GspnParser.h +++ b/src/parser/GspnParser.h @@ -1,177 +1,10 @@ -#ifndef STORM_PARSER_GSPNPARSER_H_ -#define STORM_PARSER_GSPNPARSER_H_ - -#include - -#include -#include - #include "src/storage/gspn/GSPN.h" namespace storm { namespace parser { - - /* Parses a pnml-file to a gspn. - IMPORTANT: The names of places, transitions and arcs must differ from each other. - */ class GspnParser { public: - - /*! - * Parses the given file into the GSPN. - * - * @param filename The name of the file to parse. - * @return The resulting GSPN. - */ - storm::gspn::GSPN const& parse(std::string const& filename); - private: - - /*! - * Traverse the root element. - * - * @param element The root element of the DOM object. - */ - void traversePnmlElement(xercesc::DOMElement const* const element); - - /*! - * Traverse a net or page node. - * - * @param node The net or page node. - */ - void traverseNetOrPage(xercesc::DOMNode const* const node); - - /*! - * Traverse a place node. - * - * @param node The place node. - */ - void traversePlace(xercesc::DOMNode const* const node); - - /*! - * Traverse a transition node. - * - * @param node The transition node. - */ - void traverseTransition(xercesc::DOMNode const* const node); - - /*! - * Traverse an arc node. - * - * @param node The arc node. - */ - void traverseArc(xercesc::DOMNode const* const node); - - /*! - * Traverse an initial marking node. - * - * @param node the initial marking node. - * @return The number of initial tokens. - */ - uint_fast64_t traverseInitialMarking(xercesc::DOMNode const* const node); - - /*! - * Traverse a capacity node. - * - * @param node The capacity node. - * @return The capacity for the place. - */ - int_fast64_t traverseCapacity(xercesc::DOMNode const* const node); - - /*! - * Traverse a inscription node. - * - * @param node The inscription node. - * @return The multiplicty for the arc. - */ - uint_fast64_t traverseMultiplicity(xercesc::DOMNode const* const node); - - /*! - * Traverse a rate node. - * - * @param node The rate node. - * @return The rate or weight of the transition. - */ - std::string traverseTransitionValue(xercesc::DOMNode const* const node); - - /*! - * Traverse a timed node. - * - * @param node The timed node. - * @return False if the tranisition is immediate - */ - bool traverseTransitionType(xercesc::DOMNode const* const node); - - /*! - * Traverse a type node. - * - * @param node The type node. - * @return Returns a string with the arc type. - */ - std::string traverseArcType(xercesc::DOMNode const* const node); - - /** - * Traverse a priority node. - * @param node The priority node. - * @return Returns the priority of the transition. - */ - uint_fast64_t traversePriority(xercesc::DOMNode const* const node); - - /*! - * Gives the name of the current node. - * - * @param node The node. - * @return The name of the node. - */ - std::string getName(xercesc::DOMNode* node); - - /*! - * Transforms the given XML String to a std::string. - * - * @param xmlString The given String in the XML format - * @return The corresponding std::string. - */ - static std::string XMLtoString(const XMLCh* xmlString); - - - void traverseProjectElement(xercesc::DOMNode const* const node); - - void traverseGspnElement(xercesc::DOMNode const* const node); - void traverseNodesElement(xercesc::DOMNode const* const node); - void traverseEdgesElement(xercesc::DOMNode const* const node); - - void traversePlaceElement(xercesc::DOMNode const* const node); - void traverseTransitionElement(xercesc::DOMNode const* const node); - void traverseArcElement(xercesc::DOMNode const* const node); - - - // the constructed gspn - storm::gspn::GSPN gspn; - - // contains the id for a new node - uint_fast64_t newNode = 0; - - // default value for initial tokens - uint_fast64_t defaultNumberOfInitialTokens = 0; - - // default value for capacities - int_fast64_t defaultCapacity = -1; - - // default value for the transition type (false == immediate transition) - bool defaultTransitionType = false; - - // default value for the transition weight or rate - std::string defaultTransitionValue = "1"; // TODO set to 0 - - // default value for the arc type - std::string defaultArcType = "normal"; - - // default multiplicity for arcs - uint_fast64_t defaultMultiplicity = 1; - - //default priority for transitions - uint_fast64_t defaultPriority = 0; + static storm::gspn::GSPN* parse(std::string const& filename); }; } } - -#endif //STORM_PARSER_GSPNPARSER_H_ diff --git a/src/parser/PnmlParser.cpp b/src/parser/PnmlParser.cpp new file mode 100644 index 000000000..46a30f900 --- /dev/null +++ b/src/parser/PnmlParser.cpp @@ -0,0 +1,446 @@ +#include "src/parser/PnmlParser.h" + +#include + +#include "src/adapters/XercesAdapter.h" + +#include "src/exceptions/UnexpectedException.h" +#include "src/exceptions/WrongFormatException.h" +#include "src/utility/macros.h" + +namespace storm { + namespace parser { + storm::gspn::GSPN * PnmlParser::parse(xercesc::DOMElement const* elementRoot ) { + if (storm::adapters::getName(elementRoot) == "pnml") { + traversePnmlElement(elementRoot); + } else { + // If the top-level node is not a "pnml" or "" node, then throw an exception. + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n"); + } + return builder.buildGspn(); + } + + void PnmlParser::traversePnmlElement(xercesc::DOMElement const* const element) { + // traverse attributes + for (uint_fast64_t i = 0; i < element->getAttributes()->getLength(); ++i) { + auto attr = element->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=pnml): " + name + "\n"); + } + + // traverse children + for (uint_fast64_t i = 0; i < element->getChildNodes()->getLength(); ++i) { + auto child = element->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (name.compare("net") == 0) { + traverseNetOrPage(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=pnml): " + name + "\n"); + } + } + } + + void PnmlParser::traverseNetOrPage(xercesc::DOMNode const* const node) { + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + if (name.compare("id") == 0) { + builder.setGspnName(storm::adapters::XMLtoString(attr->getNodeValue())); + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (name.compare("place") == 0) { + traversePlace(child); + } else if (name.compare("transition") == 0) { + traverseTransition(child); + } else if (name.compare("arc") == 0) { + traverseArc(child); + } else if (name.compare("page") == 0) { + // Some pnml files have a child named page. + // The page node has the same children like the net node (e.g., place, transition, arc) + traverseNetOrPage(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=" + storm::adapters::XMLtoString(node->getNodeName()) + "): " + name + "\n"); + } + } + } + + void PnmlParser::traversePlace(xercesc::DOMNode const* const node) { + std::string placeName; + // the first entry is false if the corresponding information was not found in the pnml file + std::pair numberOfInitialTokens(false, defaultNumberOfInitialTokens); + std::pair capacity(false, defaultCapacity); + + // traverse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + if (name.compare("id") == 0) { + placeName = storm::adapters::XMLtoString(attr->getNodeValue()); + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=place): " + name + "\n"); + } + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (name.compare("initialMarking") == 0) { + numberOfInitialTokens.first = true; + numberOfInitialTokens.second = traverseInitialMarking(child); + } else if(name.compare("capacity") == 0) { + capacity.first = true; + capacity.second = traverseCapacity(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("name") == 0 || + name.compare("graphics") == 0) { + // ignore these tags + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=place): " + name + "\n"); + } + } + + if (!numberOfInitialTokens.first) { + // no information about the number of initial tokens is found + // use the default number of initial tokens + STORM_PRINT_AND_LOG("unknown numberOfInitialTokens (place=" + placeName + ")\n"); + } + if (!capacity.first) { + // no information about the capacity is found + // use default capacity + STORM_PRINT_AND_LOG("unknown capacity (place=" + placeName + ")\n"); + } + builder.addPlace(capacity.first ? capacity.second : -1, numberOfInitialTokens.first ? numberOfInitialTokens.second : 0, placeName); + } + + void PnmlParser::traverseTransition(xercesc::DOMNode const* const node) { + // the first entry is false if the corresponding information was not found in the pnml file + std::pair timed(false, defaultTransitionType); + std::pair value(false, ""); + std::string id; + uint_fast64_t priority = defaultPriority; + + // parse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + if (name.compare("id") == 0) { + id = storm::adapters::XMLtoString(attr->getNodeValue()); + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=transition): " + name + "\n"); + } + } + + // traverse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + + if (name.compare("rate") == 0) { + value.first = true; + value.second = traverseTransitionValue(child); + } else if (name.compare("timed") == 0) { + timed.first = true; + timed.second = traverseTransitionType(child); + } else if (name.compare("priority") == 0) { + priority = traversePriority(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("graphics") == 0 || + name.compare("name") == 0 || + name.compare("orientation") == 0) { + // ignore these tags + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=transition): " + name + "\n"); + } + } + + // build transition and add it to the gspn + if (!timed.first) { + // found unknown transition type + // abort parsing + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "unknown transition type (transition=" + id + ")\n"); + return; + } + + if (timed.second) { + if (!value.first) { + // no information about the rate is found + // abort the parsing + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown transition rate (transition=" + id + ")\n"); + } + builder.addTimedTransition(priority, std::stod(value.second), id); + } else { + if (!value.first) { + // no information about the weight is found + // continue with the default weight + STORM_PRINT_AND_LOG("unknown transition weight (transition=" + id + ")\n"); + } + builder.addImmediateTransition(priority, std::stod(value.second), id); + } + } + + void PnmlParser::traverseArc(xercesc::DOMNode const* const node) { + // the first entry is false if the corresponding information was not found in the pnml file + std::pair source(false, ""); + std::pair target(false, ""); + std::pair type(false, defaultArcType); + std::pair multiplicity(false, defaultMultiplicity); + std::string id; + + // parse attributes + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + + if (name.compare("source") == 0) { + source.first = true; + source.second = storm::adapters::XMLtoString(attr->getNodeValue()); + } else if (name.compare("target") == 0) { + target.first = true; + target.second = storm::adapters::XMLtoString(attr->getNodeValue()); + } else if (name.compare("id") == 0) { + id = storm::adapters::XMLtoString(attr->getNodeValue()); + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown attribute (node=arc): " + name + "\n"); + } + } + + // parse children + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + if (name.compare("type") == 0) { + type.first = true; + type.second = traverseArcType(child); + } else if(name.compare("inscription") == 0) { + multiplicity.first = true; + multiplicity.second = traverseMultiplicity(child); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("graphics") == 0 || + name.compare("arcpath") == 0 || + name.compare("tagged") == 0) { + // ignore these tags + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=arc): " + name + "\n"); + } + } + + // check if all necessary information where stored in the pnml file + if (!source.first) { + // could not find start of the arc + // abort parsing + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc source (arc=" + id + ")\n"); + } + if (!target.first) { + // could not find the target of the arc + // abort parsing + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc target (arc=" + id + ")\n"); + } + if (!multiplicity.first) { + // no information about the multiplicity of the arc + // continue and use the default multiplicity + STORM_PRINT_AND_LOG("unknown multiplicity (node=arc): " + id + "\n"); + } + + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "No arc type specified for arc '" + id + "'"); + if (type.second == "normal") { + builder.addNormalArc(source.second, target.second, multiplicity.second); + } else if (type.second == "inhibition") { + builder.addInhibitionArc(source.second, target.second, multiplicity.second); + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Arc type '" << type.second << "' in arc '" << id << "' is unknown."); + } + } + + uint_fast64_t PnmlParser::traverseInitialMarking(xercesc::DOMNode const* const node) { + uint_fast64_t result = defaultNumberOfInitialTokens; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + if (name.compare("text") == 0) { + result = std::stoull(storm::adapters::getName(child->getFirstChild())); + } else if (name.compare("value") == 0) { + auto value = storm::adapters::getName(child->getFirstChild()); + value = value.substr(std::string("Default,").length()); + result = std::stoull(value); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("graphics") == 0) { + // ignore these tags + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=initialMarking): " + name + "\n"); + } + } + return result; + } + + int_fast64_t PnmlParser::traverseCapacity(xercesc::DOMNode const* const node) { + int_fast64_t result= defaultCapacity; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + if (name.compare("value") == 0) { + auto value = storm::adapters::getName(child->getFirstChild()); + if (value.find("Default,") == 0) { + value = value.substr(std::string("Default,").length()); + } + result = std::stoull(value); + } else if (name.compare("graphics") == 0) { + // ignore these nodes + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=capacity): " + name + "\n"); + } + } + return result; + } + + uint_fast64_t PnmlParser::traverseMultiplicity(xercesc::DOMNode const* const node) { + uint_fast64_t result = defaultMultiplicity; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + if (name.compare("value") == 0) { + auto value = storm::adapters::getName(child->getFirstChild()); + if (value.find("Default,") == 0) { + value = value.substr(std::string("Default,").length()); + } + result = std::stoull(value); + } else if (name.compare("graphics") == 0) { + // ignore these nodes + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=inscription): " + name + "\n"); + } + } + return result; + } + + + std::string PnmlParser::traverseTransitionValue(xercesc::DOMNode const* const node) { + std::string result; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + if (name.compare("value") == 0) { + result = storm::adapters::getName(child->getFirstChild()); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=rate): " + name + "\n"); + } + } + return result; + } + + bool PnmlParser::traverseTransitionType(xercesc::DOMNode const* const node) { + bool result; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + if (name.compare("value") == 0) { + result = storm::adapters::getName(child->getFirstChild()).compare("true") == 0 ? true : false; + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=timed): " + name + "\n"); + } + } + return result; + } + + std::string PnmlParser::traverseArcType(xercesc::DOMNode const* const node) { + for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { + auto attr = node->getAttributes()->item(i); + auto name = storm::adapters::getName(attr); + if (name.compare("value") == 0) { + return storm::adapters::XMLtoString(attr->getNodeValue()); + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=type): " + name + "\n"); + } + } + return defaultArcType; + } + + uint_fast64_t PnmlParser::traversePriority(xercesc::DOMNode const* const node) { + uint_fast64_t result = defaultPriority; + for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) { + auto child = node->getChildNodes()->item(i); + auto name = storm::adapters::getName(child); + if (name.compare("text") == 0) { + result = std::stoull(storm::adapters::getName(child->getFirstChild())); + } else if (name.compare("value") == 0) { + auto value = storm::adapters::getName(child->getFirstChild()); + value = value.substr(std::string("Default,").length()); + result = std::stoull(value); + } else if (std::all_of(name.begin(), name.end(), isspace)) { + // ignore node (contains only whitespace) + } else if (name.compare("graphics") == 0) { + // ignore these tags + } else { + // Found node or attribute which is at the moment nod handled by this parser. + // Notify the user and continue the parsing. + STORM_PRINT_AND_LOG("unknown child (node=priority): " + name + "\n"); + } + } + return result; + } + } +} + diff --git a/src/parser/PnmlParser.h b/src/parser/PnmlParser.h new file mode 100644 index 000000000..99a331fe4 --- /dev/null +++ b/src/parser/PnmlParser.h @@ -0,0 +1,142 @@ +#pragma once + +#include + +#include +#include + +#include "src/storage/gspn/GSPN.h" + +#include "src/storage/gspn/GspnBuilder.h" + +namespace storm { + namespace parser { + + /* Parses a pnml-file to a gspn. + IMPORTANT: The names of places, transitions and arcs must differ from each other. + */ + class PnmlParser { + public: + + /*! + * Parses the given file into the GSPN. + * + * @param filename The name of the file to parse. + * @return The resulting GSPN. + */ + storm::gspn::GSPN* parse(xercesc::DOMElement const* elementRoot); + private: + + /*! + * Traverse the root element. + * + * @param element The root element of the DOM object. + */ + void traversePnmlElement(xercesc::DOMElement const* const element); + + /*! + * Traverse a net or page node. + * + * @param node The net or page node. + */ + void traverseNetOrPage(xercesc::DOMNode const* const node); + + /*! + * Traverse a place node. + * + * @param node The place node. + */ + void traversePlace(xercesc::DOMNode const* const node); + + /*! + * Traverse a transition node. + * + * @param node The transition node. + */ + void traverseTransition(xercesc::DOMNode const* const node); + + /*! + * Traverse an arc node. + * + * @param node The arc node. + */ + void traverseArc(xercesc::DOMNode const* const node); + + /*! + * Traverse an initial marking node. + * + * @param node the initial marking node. + * @return The number of initial tokens. + */ + uint_fast64_t traverseInitialMarking(xercesc::DOMNode const* const node); + + /*! + * Traverse a capacity node. + * + * @param node The capacity node. + * @return The capacity for the place. + */ + int_fast64_t traverseCapacity(xercesc::DOMNode const* const node); + + /*! + * Traverse a inscription node. + * + * @param node The inscription node. + * @return The multiplicty for the arc. + */ + uint_fast64_t traverseMultiplicity(xercesc::DOMNode const* const node); + + /*! + * Traverse a rate node. + * + * @param node The rate node. + * @return The rate or weight of the transition. + */ + std::string traverseTransitionValue(xercesc::DOMNode const* const node); + + /*! + * Traverse a timed node. + * + * @param node The timed node. + * @return False if the tranisition is immediate + */ + bool traverseTransitionType(xercesc::DOMNode const* const node); + + /*! + * Traverse a type node. + * + * @param node The type node. + * @return Returns a string with the arc type. + */ + std::string traverseArcType(xercesc::DOMNode const* const node); + + /** + * Traverse a priority node. + * @param node The priority node. + * @return Returns the priority of the transition. + */ + uint_fast64_t traversePriority(xercesc::DOMNode const* const node); + + // the constructed gspn + storm::gspn::GspnBuilder builder; + + // default value for initial tokens + uint_fast64_t defaultNumberOfInitialTokens = 0; + + // default value for capacities + int_fast64_t defaultCapacity = -1; + + // default value for the transition type (false == immediate transition) + bool defaultTransitionType = false; + + // default value for the arc type + std::string defaultArcType = "normal"; + + // default multiplicity for arcs + uint_fast64_t defaultMultiplicity = 1; + + //default priority for transitions + uint_fast64_t defaultPriority = 0; + }; + } +} diff --git a/src/storage/gspn/GSPN.cpp b/src/storage/gspn/GSPN.cpp index 8449181d6..7e7ffbe37 100644 --- a/src/storage/gspn/GSPN.cpp +++ b/src/storage/gspn/GSPN.cpp @@ -8,27 +8,37 @@ namespace storm { namespace gspn { - void GSPN::addImmediateTransition(storm::gspn::ImmediateTransition const& transition) { - this->immediateTransitions.push_back(std::make_shared>(transition)); + uint64_t GSPN::timedTransitionIdToTransitionId(uint64_t ttId) { + return ttId | (1ull << ((sizeof(ttId) * CHAR_BIT) - 1)); } - - void GSPN::addTimedTransition(storm::gspn::TimedTransition const& transition) { - this->timedTransitions.push_back(std::make_shared>(transition)); + + uint64_t GSPN::immediateTransitionIdToTransitionId(uint64_t itId) { + return itId; } - - void GSPN::addPlace(Place const& place) { - this->places.push_back(place); + + uint64_t GSPN::transitionIdToTimedTransitionId(uint64_t tId) { + return (tId << 1) >> 1; } - + + uint64_t GSPN::transitionIdToImmediateTransitionId(uint64_t tId) { + return tId; + } + + GSPN::GSPN(std::string const& name, std::vector const& places, std::vector> const& itransitions, std::vector> const& ttransitions) + : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions) + { + + } + uint_fast64_t GSPN::getNumberOfPlaces() const { return places.size(); } - std::vector>> const& GSPN::getTimedTransitions() const { + std::vector> const& GSPN::getTimedTransitions() const { return this->timedTransitions; } - std::vector>> const& GSPN::getImmediateTransitions() const { + std::vector> const& GSPN::getImmediateTransitions() const { return this->immediateTransitions; } @@ -45,57 +55,65 @@ namespace storm { } - std::pair GSPN::getPlace(uint_fast64_t const& id) const { - for (auto& place : places) { - if (id == place.getID()) { - return std::make_pair(true, &place); - } + storm::gspn::Place const* GSPN::getPlace(uint64_t id) const { + if(id < places.size()) { + assert(places.at(id).getID() == id); + return &places.at(id); + } + return nullptr; + } + + + storm::gspn::Place* GSPN::getPlace(uint64_t id) { + if(id < places.size()) { + assert(places.at(id).getID() == id); + return &places.at(id); } - return std::make_pair(false, nullptr); + return nullptr; } - - std::pair GSPN::getPlace(std::string const& id) { + + storm::gspn::Place const* GSPN::getPlace(std::string const& name) const { for (auto& place : places) { - if (id.compare(place.getName()) == 0) { - return std::make_pair(true, &place); + if (place.getName() == name) { + return &place; } } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "No place with name " << id); + return nullptr; }; - std::pair GSPN::getPlace(std::string const& id) const { + storm::gspn::Place* GSPN::getPlace(std::string const& name) { for (auto& place : places) { - if (id.compare(place.getName()) == 0) { - return std::make_pair(true, &place); + if (place.getName() == name) { + return &place; } } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "No place with name " << id); + return nullptr; }; - std::pair> const> GSPN::getTimedTransition(std::string const& id) const { + storm::gspn::TimedTransition const* GSPN::getTimedTransition(std::string const& name) const { for (auto& trans : timedTransitions) { - if (id.compare(trans->getName()) == 0) { - return std::make_pair> const>(true, static_cast> const>(trans)); + if (name == trans.getName()) { + return &trans; } } - return std::make_pair> const>(false, nullptr); + return nullptr; } - std::pair> const> GSPN::getImmediateTransition(std::string const& id) const { + storm::gspn::ImmediateTransition const* GSPN::getImmediateTransition(std::string const& name) const { for (auto& trans : immediateTransitions) { - if (id.compare(trans->getName()) == 0) { - return std::make_pair> const>(true, static_cast> const>(trans)); + if (name == trans.getName()) { + return &trans; } } - return std::make_pair> const>(false, nullptr); + return nullptr; } - std::pair const> GSPN::getTransition(std::string const& id) const { + storm::gspn::Transition const* GSPN::getTransition(std::string const& id) const { auto trans = getTimedTransition(id); - if (trans.first == true) { + if (trans != nullptr) { return trans; } @@ -104,10 +122,9 @@ namespace storm { 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); + storm::gspn::Place* place = getPlace(entry.first); + STORM_LOG_THROW(place != nullptr, storm::exceptions::InvalidArgumentException, "No place with name " << entry.first); + place->setCapacity(entry.second); } } @@ -130,52 +147,52 @@ namespace storm { // print transitions with weight/rate outStream << "\t" << "node [shape=box]" << std::endl; for (auto& trans : this->getImmediateTransitions()) { - outStream << "\t" << trans->getName() << " [fontcolor=white, style=filled, fillcolor=black, label=\"" << trans->getName() << "\"];" << std::endl; + outStream << "\t" << trans.getName() << " [fontcolor=white, style=filled, fillcolor=black, label=\"" << trans.getName() << "\"];" << std::endl; } for (auto& trans : this->getTimedTransitions()) { - outStream << "\t" << trans->getName() << " [label=\"" << trans->getName(); - outStream << " (" << trans->getRate() << ")\"];" << std::endl; + outStream << "\t" << trans.getName() << " [label=\"" << trans.getName(); + outStream << " (" << trans.getRate() << ")\"];" << std::endl; } // print arcs for (auto& trans : this->getImmediateTransitions()) { - for (auto &placePtr : trans->getInputPlaces()) { - outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[label=\"" << - trans->getInputArcMultiplicity(*placePtr); + for (auto &placePtr : trans.getInputPlaces()) { + outStream << "\t" << placePtr->getName() << " -> " << trans.getName() << "[label=\"" << + trans.getInputArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; } - for (auto &placePtr : trans->getInhibitionPlaces()) { - outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[arrowhead=\"dot\", label=\"" << - trans->getInhibitionArcMultiplicity(*placePtr); + for (auto &placePtr : trans.getInhibitionPlaces()) { + outStream << "\t" << placePtr->getName() << " -> " << trans.getName() << "[arrowhead=\"dot\", label=\"" << + trans.getInhibitionArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; } - for (auto &placePtr : trans->getOutputPlaces()) { - outStream << "\t" << trans->getName() << " -> " << placePtr->getName() << "[label=\"" << - trans->getOutputArcMultiplicity(*placePtr); + for (auto &placePtr : trans.getOutputPlaces()) { + outStream << "\t" << trans.getName() << " -> " << placePtr->getName() << "[label=\"" << + trans.getOutputArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; } } for (auto& trans : this->getTimedTransitions()) { - for (auto &placePtr : trans->getInputPlaces()) { - outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[label=\"" << - trans->getInputArcMultiplicity(*placePtr); + for (auto &placePtr : trans.getInputPlaces()) { + outStream << "\t" << placePtr->getName() << " -> " << trans.getName() << "[label=\"" << + trans.getInputArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; } - for (auto &placePtr : trans->getInhibitionPlaces()) { - outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[arrowhead=\"dot\", label=\"" << - trans->getInhibitionArcMultiplicity(*placePtr); + for (auto &placePtr : trans.getInhibitionPlaces()) { + outStream << "\t" << placePtr->getName() << " -> " << trans.getName() << "[arrowhead=\"dot\", label=\"" << + trans.getInhibitionArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; } - for (auto &placePtr : trans->getOutputPlaces()) { - outStream << "\t" << trans->getName() << " -> " << placePtr->getName() << "[label=\"" << - trans->getOutputArcMultiplicity(*placePtr); + for (auto &placePtr : trans.getOutputPlaces()) { + outStream << "\t" << trans.getName() << " -> " << placePtr->getName() << "[label=\"" << + trans.getOutputArcMultiplicity(*placePtr); outStream << "\"];" << std::endl; } } @@ -229,34 +246,34 @@ namespace storm { bool result = true; for (auto const& transition : this->getImmediateTransitions()) { - if (transition->getInputPlaces().empty() && - transition->getInhibitionPlaces().empty()) { - STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n") + if (transition.getInputPlaces().empty() && + transition.getInhibitionPlaces().empty()) { + STORM_PRINT_AND_LOG("transition \"" + transition.getName() + "\" has no input or inhibition place\n") result = false; } - if (transition->getOutputPlaces().empty()) { - STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n") + if (transition.getOutputPlaces().empty()) { + STORM_PRINT_AND_LOG("transition \"" + transition.getName() + "\" has no output place\n") result = false; } } for (auto const& transition : this->getTimedTransitions()) { - if (transition->getInputPlaces().empty() && - transition->getInputPlaces().empty()) { - STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n") + if (transition.getInputPlaces().empty() && + transition.getInputPlaces().empty()) { + STORM_PRINT_AND_LOG("transition \"" + transition.getName() + "\" has no input or inhibition place\n") result = false; } - if (transition->getOutputPlaces().empty()) { - STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n") + if (transition.getOutputPlaces().empty()) { + STORM_PRINT_AND_LOG("transition \"" + transition.getName() + "\" has no output place\n") result = false; } } //test if places exists in the gspn for (auto const& transition : this->getImmediateTransitions()) { - for (auto &placePtr : transition->getInputPlaces()) { + for (auto &placePtr : transition.getInputPlaces()) { bool foundPlace = false; for (auto const& place : places) { if (place.getName() == placePtr->getName()) { @@ -264,12 +281,12 @@ namespace storm { } } if (!foundPlace) { - STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") result = false; } } - for (auto &placePtr : transition->getInhibitionPlaces()) { + for (auto &placePtr : transition.getInhibitionPlaces()) { bool foundPlace = false; for (auto const& place : places) { if (place.getName() == placePtr->getName()) { @@ -277,12 +294,12 @@ namespace storm { } } if (!foundPlace) { - STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") result = false; } } - for (auto &placePtr : transition->getOutputPlaces()) { + for (auto &placePtr : transition.getOutputPlaces()) { bool foundPlace = false; for (auto const& place : places) { if (place.getName() == placePtr->getName()) { @@ -290,14 +307,14 @@ namespace storm { } } if (!foundPlace) { - STORM_PRINT_AND_LOG("output place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("output place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") result = false; } } } for (auto const& transition : this->getTimedTransitions()) { - for (auto &placePtr : transition->getInputPlaces()) { + for (auto &placePtr : transition.getInputPlaces()) { bool foundPlace = false; for (auto const& place : places) { if (place.getName() == placePtr->getName()) { @@ -305,12 +322,12 @@ namespace storm { } } if (!foundPlace) { - STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") result = false; } } - for (auto &placePtr : transition->getInhibitionPlaces()) { + for (auto &placePtr : transition.getInhibitionPlaces()) { bool foundPlace = false; for (auto const& place : places) { if (place.getName() == placePtr->getName()) { @@ -318,12 +335,12 @@ namespace storm { } } if (!foundPlace) { - STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") result = false; } } - for (auto &placePtr : transition->getOutputPlaces()) { + for (auto &placePtr : transition.getOutputPlaces()) { bool foundPlace = false; for (auto const& place : places) { if (place.getName() == placePtr->getName()) { @@ -331,7 +348,7 @@ namespace storm { } } if (!foundPlace) { - STORM_PRINT_AND_LOG("output place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n") + STORM_PRINT_AND_LOG("output place \"" + placePtr->getName() + "\" of transition \"" + transition.getName() + "\" was not found \n") result = false; } } @@ -361,16 +378,16 @@ namespace storm { } x = 1; for (auto& trans : timedTransitions) { - stream << space3 << "getName() << "\" "; + stream << space3 << "getRate() << "\" "; + stream << "nservers-x=\"" << trans.getRate() << "\" "; stream << "x=\"" << x << "\" "; stream << "y=\"4\" "; stream << "/>" << std::endl; x = x + 3; } for (auto& trans : immediateTransitions) { - stream << space3 << "getName() << "\" "; + stream << space3 << "" << std::endl; for (auto& trans : timedTransitions) { - for (auto &placePtr : trans->getInputPlaces()) { + for (auto &placePtr : trans.getInputPlaces()) { stream << space3 << "getName() << "\" "; + stream << "head=\"" << trans.getName() << "\" "; stream << "tail=\"" << placePtr->getName() << "\" "; stream << "kind=\"INPUT\" "; - stream << "mult=\"" << trans->getInputArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << trans.getInputArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } - for (auto &placePtr : trans->getInhibitionPlaces()) { + for (auto &placePtr : trans.getInhibitionPlaces()) { stream << space3 << "getName() << "\" "; + stream << "head=\"" << trans.getName() << "\" "; stream << "tail=\"" << placePtr->getName() << "\" "; stream << "kind=\"INHIBITOR\" "; - stream << "mult=\"" << trans->getInhibitionArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << trans.getInhibitionArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } - for (auto &placePtr : trans->getOutputPlaces()) { + for (auto &placePtr : trans.getOutputPlaces()) { stream << space3 << "getName() << "\" "; - stream << "tail=\"" << trans->getName() << "\" "; + stream << "tail=\"" << trans.getName() << "\" "; stream << "kind=\"OUTPUT\" "; - stream << "mult=\"" << trans->getOutputArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << trans.getOutputArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } } for (auto& trans : immediateTransitions) { - for (auto &placePtr : trans->getInputPlaces()) { + for (auto &placePtr : trans.getInputPlaces()) { stream << space3 << "getName() << "\" "; + stream << "head=\"" << trans.getName() << "\" "; stream << "tail=\"" << placePtr->getName() << "\" "; stream << "kind=\"INPUT\" "; - stream << "mult=\"" << trans->getInputArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << trans.getInputArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } - for (auto &placePtr : trans->getInhibitionPlaces()) { + for (auto &placePtr : trans.getInhibitionPlaces()) { stream << space3 << "getName() << "\" "; + stream << "head=\"" << trans.getName() << "\" "; stream << "tail=\"" << placePtr->getName() << "\" "; stream << "kind=\"INHIBITOR\" "; - stream << "mult=\"" << trans->getInhibitionArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << trans.getInhibitionArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } - for (auto &placePtr : trans->getOutputPlaces()) { + for (auto &placePtr : trans.getOutputPlaces()) { stream << space3 << "getName() << "\" "; - stream << "tail=\"" << trans->getName() << "\" "; + stream << "tail=\"" << trans.getName() << "\" "; stream << "kind=\"OUTPUT\" "; - stream << "mult=\"" << trans->getOutputArcMultiplicity(*placePtr) << "\" "; + stream << "mult=\"" << trans.getOutputArcMultiplicity(*placePtr) << "\" "; stream << "/>" << std::endl; } } @@ -457,9 +474,9 @@ namespace storm { // add immediate transitions for (const auto &trans : immediateTransitions) { - stream << space2 << "getName() << "\">" << std::endl; + stream << space2 << "" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "" << trans->getWeight() << "" << std::endl; + stream << space4 << "" << trans.getWeight() << "" << std::endl; stream << space3 << "" << std::endl; stream << space3 << "" << std::endl; stream << space4 << "false" << std::endl; @@ -469,9 +486,9 @@ namespace storm { // add timed transitions for (const auto &trans : timedTransitions) { - stream << space2 << "getName() << "\">" << std::endl; + stream << space2 << "" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "" << trans->getRate() << "" << std::endl; + stream << space4 << "" << trans.getRate() << "" << std::endl; stream << space3 << "" << std::endl; stream << space3 << "" << std::endl; stream << space4 << "true" << std::endl; @@ -483,15 +500,15 @@ namespace storm { // add arcs for immediate transitions for (const auto &trans : immediateTransitions) { // add input arcs - for (auto &placePtr : trans->getInputPlaces()) { + for (auto &placePtr : trans.getInputPlaces()) { stream << space2 << "getName() << "\" "; - stream << "target=\"" << trans->getName() << "\" "; + stream << "target=\"" << trans.getName() << "\" "; stream << ">" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "Default," << trans->getInputArcMultiplicity(*placePtr) << "" << std::endl; + stream << space4 << "Default," << trans.getInputArcMultiplicity(*placePtr) << "" << std::endl; stream << space3 << "" << std::endl; stream << space3 << "" << std::endl; @@ -500,15 +517,15 @@ namespace storm { } // add inhibition arcs - for (auto &placePtr : trans->getInhibitionPlaces()) { + for (auto &placePtr : trans.getInhibitionPlaces()) { stream << space2 << "getName() << "\" "; - stream << "target=\"" << trans->getName() << "\" "; + stream << "target=\"" << trans.getName() << "\" "; stream << ">" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "Default," << trans->getInputArcMultiplicity(*placePtr) << "" << std::endl; + stream << space4 << "Default," << trans.getInputArcMultiplicity(*placePtr) << "" << std::endl; stream << space3 << "" << std::endl; stream << space3 << "" << std::endl; @@ -517,15 +534,15 @@ namespace storm { } // add output arcs - for (auto &placePtr : trans->getOutputPlaces()) { + for (auto &placePtr : trans.getOutputPlaces()) { stream << space2 << "getName() << "\" "; + stream << "source=\"" << trans.getName() << "\" "; stream << "target=\"" << placePtr->getName() << "\" "; stream << ">" << std::endl; stream << space3 << "" << std::endl; - stream << space4 << "Default," << trans->getInputArcMultiplicity(*placePtr) << "" << std::endl; + stream << space4 << "Default," << trans.getInputArcMultiplicity(*placePtr) << "" << std::endl; stream << space3 << "" << std::endl; stream << space3 << "" << std::endl; diff --git a/src/storage/gspn/GSPN.h b/src/storage/gspn/GSPN.h index 0d7b6d800..9a9a301b7 100644 --- a/src/storage/gspn/GSPN.h +++ b/src/storage/gspn/GSPN.h @@ -16,31 +16,19 @@ namespace storm { // Stores a GSPN class GSPN { public: + static uint64_t timedTransitionIdToTransitionId(uint64_t); + static uint64_t immediateTransitionIdToTransitionId(uint64_t); + static uint64_t transitionIdToTimedTransitionId(uint64_t); + static uint64_t transitionIdToImmediateTransitionId(uint64_t); + + // Later, the rates and probabilities type should become a template, for now, let it be doubles. typedef double RateType; typedef double WeightType; - - /*! - * Adds an immediate transition to the gspn. - * - * @param transition The transition which is added to the gspn. - */ - void addImmediateTransition(ImmediateTransition const& transition); - - /*! - * Adds a timed transition to the gspn. - * - * @param transition The transition which is added to the gspn. - */ - void addTimedTransition(TimedTransition const& transition); - - /*! - * Adds a place to the gspn. - * - * @param place The place which is added to the gspn. - */ - void addPlace(Place const& place); - + + + GSPN(std::string const& name, std::vector const& places, std::vector> const& itransitions, std::vector> const& ttransitions); + /*! * Returns the number of places in this gspn. * @@ -53,14 +41,14 @@ namespace storm { * * @return The vector of timed transitions. */ - std::vector>> const& getTimedTransitions() const; + std::vector> const& getTimedTransitions() const; /*! * Returns the vector of immediate transitions in this gspn. * * @return The vector of immediate tansitions. */ - std::vector>> const& getImmediateTransitions() const; + std::vector> const& getImmediateTransitions() const; /*! * Returns the places of this gspn @@ -83,38 +71,29 @@ 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(std::string const& id); - std::pair getPlace(std::string const& id) const; + storm::gspn::Place const* getPlace(uint64_t id) const; + storm::gspn::Place const* getPlace(std::string const& name) const; + /*! * Returns the timed transition with the corresponding id. * * @param id The ID of the timed transition. - * @return The first element is true if the transition was found. - * If the first element is true, then the second element is the wanted transition. - * If the first element is false, then the second element is the nullptr. */ - std::pair> const> getTimedTransition(std::string const& id) const; + storm::gspn::TimedTransition const* getTimedTransition(std::string const& id) const; /*! * Returns the immediate transition with the corresponding id. * * @param id The ID of the timed transition. - * @return The first element is true if the transition was found. - * If the first element is true, then the second element is the wanted transition. * If the first element is false, then the second element is the nullptr. */ - std::pair> const> getImmediateTransition(std::string const& id) const; + storm::gspn::ImmediateTransition const* getImmediateTransition(std::string const& id) const; /*! * Returns the transition with the corresponding id. * - * @param id The ID of the transition. - * @return Pointer to the corresponding transition or nullptr if the place does not exists. */ - // std::shared_ptr getTransition(std::string const& id) const; - std::pair const> getTransition(std::string const& id) const; + storm::gspn::Transition const* getTransition(std::string const& id) const; /*! * Write the gspn in a dot(graphviz) configuration. @@ -156,6 +135,9 @@ namespace storm { // TODO doc void toPnml(std::ostream &stream) const; private: + storm::gspn::Place* getPlace(uint64_t id); + storm::gspn::Place* getPlace(std::string const& name); + /*! * Test * - if places are unique (ids and names) @@ -173,14 +155,16 @@ namespace storm { */ bool testTransitions() const; + + // set containing all places + std::vector places; + // set containing all immediate transitions - std::vector>> immediateTransitions; + std::vector> immediateTransitions; // set containing all timed transitions - std::vector>> timedTransitions; + std::vector> timedTransitions; - // set containing all places - std::vector places; // name of the gspn std::string name; diff --git a/src/storage/gspn/GspnBuilder.cpp b/src/storage/gspn/GspnBuilder.cpp index 3a4e1325c..70d4cb39d 100644 --- a/src/storage/gspn/GspnBuilder.cpp +++ b/src/storage/gspn/GspnBuilder.cpp @@ -3,84 +3,133 @@ #include "src/utility/macros.h" #include "src/exceptions/IllegalFunctionCallException.h" +#include "src/exceptions/InvalidArgumentException.h" #include "Place.h" namespace storm { namespace gspn { - uint_fast64_t GspnBuilder::addPlace(int_fast64_t const& capacity, uint_fast64_t const& initialTokens) { + void GspnBuilder::setGspnName(std::string const& name) { + gspnName = name; + } + + uint_fast64_t GspnBuilder::addPlace(int_fast64_t const& capacity, uint_fast64_t const& initialTokens, std::string const& name) { auto place = storm::gspn::Place(); place.setCapacity(capacity); - place.setID(nextStateID); + auto newId = places.size(); + place.setID(newId); place.setNumberOfInitialTokens(initialTokens); - gspn.addPlace(place); - return nextStateID++; + places.push_back(place); + return newId; } - uint_fast64_t GspnBuilder::addImmediateTransition(uint_fast64_t const& priority, double const& weight) { + uint_fast64_t GspnBuilder::addImmediateTransition(uint_fast64_t const& priority, double const& weight, std::string const& name) { auto trans = storm::gspn::ImmediateTransition(); - trans.setName(std::to_string(nextTransitionID)); + auto newId = GSPN::immediateTransitionIdToTransitionId(immediateTransitions.size()); + trans.setName(std::to_string(newId)); trans.setPriority(priority); trans.setWeight(weight); - trans.setID(nextTransitionID); - gspn.addImmediateTransition(trans); - return nextTransitionID++; + trans.setID(newId); + immediateTransitions.push_back(trans); + return newId; + } - uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate) { + uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate, std::string const& name) { auto trans = storm::gspn::TimedTransition(); - trans.setName(std::to_string(nextTransitionID)); + auto newId = GSPN::timedTransitionIdToTransitionId(timedTransitions.size()); + trans.setName(std::to_string(newId)); trans.setPriority(priority); trans.setRate(rate); - trans.setID(nextTransitionID); - gspn.addTimedTransition(trans); - return nextTransitionID++; + trans.setID(newId); + timedTransitions.push_back(trans); + return newId; } + void GspnBuilder::addInputArc(uint_fast64_t const &from, uint_fast64_t const &to, uint_fast64_t const &multiplicity) { - auto transPair = gspn.getTransition(std::to_string(to)); - if (!std::get<0>(transPair)) { - STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist."); - } - - auto placePair = gspn.getPlace(from); - if (!std::get<0>(placePair)) { - 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); + STORM_LOG_THROW(from < places.size(), storm::exceptions::InvalidArgumentException, "No place with id " << from << " known."); + auto place = places.at(from); + getTransition(to).setInputArcMultiplicity(place, multiplicity); + } + + void GspnBuilder::addInputArc(std::string const& from, std::string const& to, uint64_t multiplicity) { + STORM_LOG_THROW(placeNames.count(from) != 0, storm::exceptions::InvalidArgumentException, "Could not find a place with name '" << from << "'"); + STORM_LOG_THROW(transitionNames.count(to) != 0, storm::exceptions::InvalidArgumentException, "Could not find a transition with name << '" << to << "'"); + addInputArc(placeNames.at(from), transitionNames.at(to)); } void GspnBuilder::addInhibitionArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity) { - auto transPair = gspn.getTransition(std::to_string(to)); - if (!std::get<0>(transPair)) { - STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist."); - } + STORM_LOG_THROW(from < places.size(), storm::exceptions::InvalidArgumentException, "No place with id " << from << " known."); + auto place = places.at(from); - auto placePair = gspn.getPlace(from); - if (!std::get<0>(placePair)) { - 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); + getTransition(to).setInhibitionArcMultiplicity(place, multiplicity); + } + + void GspnBuilder::addInhibitionArc(std::string const& from, std::string const& to, uint64_t multiplicity) { + STORM_LOG_THROW(placeNames.count(from) != 0, storm::exceptions::InvalidArgumentException, "Could not find a place with name '" << from << "'"); + STORM_LOG_THROW(transitionNames.count(to) != 0, storm::exceptions::InvalidArgumentException, "Could not find a transition with name << '" << to << "'"); + addInhibitionArc(placeNames.at(from), transitionNames.at(to)); } void GspnBuilder::addOutputArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity) { - auto transPair = gspn.getTransition(std::to_string(from)); - if (!std::get<0>(transPair)) { - STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist."); + STORM_LOG_THROW(to < places.size(), storm::exceptions::InvalidArgumentException, "No place with id " << to << " known."); + auto place = places.at(to); + getTransition(from).setOutputArcMultiplicity(place, multiplicity); + } + + void GspnBuilder::addOutputArc(std::string const& from, std::string const& to, uint64_t multiplicity) { + STORM_LOG_THROW(placeNames.count(to) != 0, storm::exceptions::InvalidArgumentException, "Could not find a place with name '" << to << "'"); + STORM_LOG_THROW(transitionNames.count(from) != 0, storm::exceptions::InvalidArgumentException, "Could not find a transition with name << '" << from << "'"); + addOutputArc(transitionNames.at(from), placeNames.at(to)); + } + + Transition& GspnBuilder::getTransition(uint64_t id) { + if (isTimedTransitionId(id)) { + return timedTransitions.at(id); + } else if(isImmediateTransitionId(id)) { + return immediateTransitions.at(id); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "No transitition with id '" << id << "' known."); } - - auto placePair = gspn.getPlace(to); - if (!std::get<0>(placePair)) { - STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist."); + } + + void GspnBuilder::addNormalArc(std::string const& from, std::string const& to, uint64_t multiplicity) { + if (placeNames.count(from) > 0 && transitionNames.count(to) > 0) { + addInputArc(placeNames.at(from), transitionNames.at(to), multiplicity); + } else if (transitionNames.count(from) > 0 && placeNames.count(to) > 0) { + addOutputArc(transitionNames.at(from), placeNames.at(to), multiplicity); + } else { + // No suitable combination. Provide error message: + if (placeNames.count(from) > 0) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expected a transition with name " << to << " for arc from '" << from << "' to '" << to << "'."); + } + if (transitionNames.count(from) > 0) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expected a place named " << to << " for arc from '" << from << "' to '" << to << "'."); + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expected a place named " << from << " for arc from '" << from << "' to '" << to << "'."); + } - - std::get<1>(transPair)->setOutputArcMultiplicity(*std::get<1>(placePair), multiplicity); } + + bool GspnBuilder::isTimedTransitionId(uint64_t tid) const { + if (tid >> 63) { + return GSPN::transitionIdToTimedTransitionId(tid) < timedTransitions.size(); + } + return false; + } + + bool GspnBuilder::isImmediateTransitionId(uint64_t tid) const { + if (tid >> 63) { + return false; + } + return GSPN::transitionIdToImmediateTransitionId(tid) < immediateTransitions.size(); + } + + - storm::gspn::GSPN const& GspnBuilder::buildGspn() const { - return gspn; + storm::gspn::GSPN* GspnBuilder::buildGspn() const { + return new GSPN(gspnName, places, immediateTransitions, timedTransitions); } } } \ No newline at end of file diff --git a/src/storage/gspn/GspnBuilder.h b/src/storage/gspn/GspnBuilder.h index c5fcf6a5d..59f098a82 100644 --- a/src/storage/gspn/GspnBuilder.h +++ b/src/storage/gspn/GspnBuilder.h @@ -1,5 +1,4 @@ -#ifndef STORM_STORAGE_GSPN_GSPNBUILDER_H -#define STORM_STORAGE_GSPN_GSPNBUILDER_H +#pragma once #include #include @@ -11,6 +10,14 @@ namespace storm { namespace gspn { class GspnBuilder { public: + typedef double RateType; + typedef double WeightType; + + /** + * Set GSPN name + */ + void setGspnName(std::string const& name); + /** * Add a place to the gspn. * @param id The id must be unique for the gspn. @@ -19,7 +26,7 @@ namespace storm { * A capacity of -1 indicates an unbounded place. * @param initialTokens The number of inital tokens in the place. */ - uint_fast64_t addPlace(int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0); + uint_fast64_t addPlace(int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0, std::string const& name = ""); /** * Adds an immediate transition to the gspn. @@ -27,7 +34,7 @@ namespace storm { * @param priority The priority for the transtion. * @param weight The weight for the transition. */ - uint_fast64_t addImmediateTransition(uint_fast64_t const& priority = 0, double const& weight = 0); + uint_fast64_t addImmediateTransition(uint_fast64_t const& priority = 0, WeightType const& weight = 0, std::string const& name = ""); /** * Adds an timed transition to the gspn. @@ -35,7 +42,7 @@ namespace storm { * @param priority The priority for the transtion. * @param weight The weight for the transition. */ - uint_fast64_t addTimedTransition(uint_fast64_t const &priority = 0, double const &rate = 0); + uint_fast64_t addTimedTransition(uint_fast64_t const &priority, RateType const& rate, std::string const& name = ""); /** * Adds an new input arc from a place to an transition. @@ -45,6 +52,7 @@ namespace storm { */ void addInputArc(uint_fast64_t const &from, uint_fast64_t const &to, uint_fast64_t const &multiplicity = 1); + void addInputArc(std::string const& from, std::string const& to, uint64_t multiplicity = 1); /** * Adds an new input arc from a place to an transition. * @param from The place from which the arc is originating. @@ -53,6 +61,8 @@ namespace storm { */ void addInhibitionArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity = 1); + void addInhibitionArc(std::string const& from, std::string const& to, uint64_t multiplicity = 1); + /** * Adds an new input arc from a place to an transition. * @param from The place from which the arc is originating. @@ -60,23 +70,47 @@ namespace storm { * @param multiplicity The multiplicity of the arc. */ void addOutputArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity = 1); + + void addOutputArc(std::string const& from, std::string const& to, uint64_t multiplicity = 1); + + + /** + * Adds an arc from a named element to a named element. + * Can be both input or output arc, but not an inhibition arc. + * Convenience function for textual format parsers. + * + * @param from Source element in the GSPN from where this arc starts + * @param to Target element in the GSPN where this arc ends + * @param multiplicity (Optional) multiplicity for the arc, default = 1 + */ + void addNormalArc(std::string const& from, std::string const& to, uint64_t multiplicity = 1); + + /** * * @return The gspn which is constructed by the builder. */ - storm::gspn::GSPN const& buildGspn() const; + storm::gspn::GSPN* buildGspn() const; private: - // gspn which is returned - storm::gspn::GSPN gspn; - // id for the next state which is added - uint_fast64_t nextStateID = 0; - // id for the next transition (timed or immediate) which is added - uint_fast64_t nextTransitionID = 0; + bool isImmediateTransitionId(uint64_t) const; + bool isTimedTransitionId(uint64_t) const; + Transition& getTransition(uint64_t); + + std::map placeNames; + std::map transitionNames; + + std::string gspnName = "_gspn_"; + + // set containing all immediate transitions + std::vector> immediateTransitions; + + // set containing all timed transitions + std::vector> timedTransitions; + + // set containing all places + std::vector places; }; } } - - -#endif //STORM_STORAGE_GSPN_GSPNBUILDER_H diff --git a/src/storage/gspn/ImmediateTransition.h b/src/storage/gspn/ImmediateTransition.h index cf4839181..2da05f171 100644 --- a/src/storage/gspn/ImmediateTransition.h +++ b/src/storage/gspn/ImmediateTransition.h @@ -30,7 +30,7 @@ namespace storm { /** * True iff no weight is attached. */ - bool noWeightAttached() { + bool noWeightAttached() const { return storm::utility::isZero(weight); } private: diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 13512f554..a460350f4 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -215,7 +215,7 @@ namespace storm { } else { // TODO add checks - opDecl["op"] = "Pmin"; + opDecl["op"] = "Emin"; opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); } opDecl["exp"] = modernjson::json(1); @@ -357,7 +357,7 @@ namespace storm { } else { // TODO add checks - opDecl["op"] = "Pmin"; + opDecl["op"] = "Emin"; opDecl["reach"] = boost::any_cast(f.getSubformula().accept(*this, boost::none)); } opDecl["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT";