sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge branch 'gspn' into jani_gspn_support 

Former-commit-id: f5d1a9fb6a [formerly 5fdac9a9f0]
Former-commit-id: e8e48b198d
main
sjunges 9 years ago
parent
09ea2d680e 86c87ad6d1
commit
3892fb923a
34 changed files with 138376 additions and 54 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      CMakeLists.txt
  2. 41034
      examples/gspn/HypercubeGrid/hc3k4p4b12.pnml
  3. 87274
      examples/gspn/HypercubeGrid/hc4k3p3b12.pnml
  4. 1
      examples/gspn/HypercubeGrid/hc5k3p3b15.pnml.REMOVED.git-id
  5. 5554
      examples/gspn/ibm319/IBM319.pnml
  6. 148
      examples/gspn/tiny/tiny01.pnml
  7. 1236
      examples/gspn/workflow_cluster/workflow_cluster.pnml
  8. 9
      src/CMakeLists.txt
  9. 14
      src/adapters/CarlAdapter.h
  10. 2
      src/builder/ExplicitDFTModelBuilder.cpp
  11. 326
      src/builder/ExplicitGspnModelBuilder.cpp
  12. 172
      src/builder/ExplicitGspnModelBuilder.h
  13. 573
      src/parser/GspnParser.cpp
  14. 165
      src/parser/GspnParser.h
  15. 10
      src/solver/stateelimination/EliminatorBase.cpp
  16. 516
      src/storage/gspn/GSPN.cpp
  17. 183
      src/storage/gspn/GSPN.h
  18. 90
      src/storage/gspn/GspnBuilder.cpp
  19. 89
      src/storage/gspn/GspnBuilder.h
  20. 43
      src/storage/gspn/ImmediateTransition.h
  21. 59
      src/storage/gspn/Marking.cpp
  22. 80
      src/storage/gspn/Marking.h
  23. 41
      src/storage/gspn/Place.cpp
  24. 87
      src/storage/gspn/Place.h
  25. 36
      src/storage/gspn/TimedTransition.h
  26. 195
      src/storage/gspn/Transition.cpp
  27. 240
      src/storage/gspn/Transition.h
  28. 153
      src/storm-gspn.cpp
  29. 55
      src/utility/constants.cpp
  30. 26
      src/utility/constants.h
  31. 1
      src/utility/storm.cpp
  32. 2
      src/utility/storm.h
  33. 13
      src/utility/vector.h
  34. 2
      storm-config.h.in

1
CMakeLists.txt
View File

@ -37,6 +37,7 @@ option(STORM_PYTHON "Builds the API for Python" OFF)
option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON) option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON)
mark_as_advanced(STORM_COMPILE_WITH_CCACHE) mark_as_advanced(STORM_COMPILE_WITH_CCACHE)
option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF) option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF)
option(STORM_USE_CLN_NUMBERS "Sets whether CLN or GMP numbers should be used" ON)
set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).") set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).")
set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).")
set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).")

41034
examples/gspn/HypercubeGrid/hc3k4p4b12.pnml
File diff suppressed because it is too large
View File

87274
examples/gspn/HypercubeGrid/hc4k3p3b12.pnml
File diff suppressed because it is too large
View File

1
examples/gspn/HypercubeGrid/hc5k3p3b15.pnml.REMOVED.git-id
View File

@ -0,0 +1 @@
1dcc3a0045e4d0f9358f9ee04e70c6f0107929be

5554
examples/gspn/ibm319/IBM319.pnml
File diff suppressed because it is too large
View File

148
examples/gspn/tiny/tiny01.pnml
View File

@ -0,0 +1,148 @@
<pnml>
<net id="tiny1">
<place id="p1">
<initialMarking>
<value>Default,1</value>
</initialMarking>
</place>
<place id="p2">
<initialMarking>
<value>Default,1</value>
</initialMarking>
</place>
<place id="p3">
<initialMarking>
<value>Default,0</value>
</initialMarking>
</place>
<place id="p4">
<initialMarking>
<value>Default,0</value>
</initialMarking>
</place>
<place id="p5">
<initialMarking>
<value>Default,0</value>
</initialMarking>
</place>
<place id="p6">
<initialMarking>
<value>Default,0</value>
</initialMarking>
</place>
<place id="p7">
<initialMarking>
<value>Default,0</value>
</initialMarking>
</place>
<transition id="t1">
<rate>
<value>1</value>
</rate>
<timed>
<value>false</value>
</timed>
</transition>
<transition id="t2">
<rate>
<value>2</value>
</rate>
<timed>
<value>false</value>
</timed>
</transition>
<transition id="t3">
<rate>
<value>3</value>
</rate>
<timed>
<value>false</value>
</timed>
</transition>
<transition id="l1">
<rate>
<value>4</value>
</rate>
<timed>
<value>true</value>
</timed>
</transition>
<transition id="l2">
<rate>
<value>5</value>
</rate>
<timed>
<value>true</value>
</timed>
<priority>
<text>2</text>
</priority>
</transition>
<arc id="arc1" source="p1" target="t1">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc2" source="t1" target="p3">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc3" source="p2" target="t2">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc4" source="t2" target="p5">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc5" source="p2" target="t3">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc6" source="p3" target="t3">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc7" source="t3" target="p4">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc8" source="p4" target="l1">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc9" source="l1" target="p6">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc10" source="p5" target="l2">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc11" source="l2" target="p7">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
</net>
</pnml>

1236
examples/gspn/workflow_cluster/workflow_cluster.pnml
File diff suppressed because it is too large
View File

9
src/CMakeLists.txt
View File

@ -11,7 +11,7 @@ file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp)
file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp)
file(GLOB_RECURSE STORM_DFT_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm-dyftee.cpp) file(GLOB_RECURSE STORM_DFT_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm-dyftee.cpp)
file(GLOB_RECURSE STORM_PGCL_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm-pgcl.cpp) file(GLOB_RECURSE STORM_PGCL_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm-pgcl.cpp)
file(GLOB_RECURSE STORM_GSPN_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm-gspn.cpp)
# Additional include files like the storm-config.h # Additional include files like the storm-config.h
file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h)
@ -23,6 +23,7 @@ list(REMOVE_ITEM STORM_LIB_HEADERS ${STORM_HEADERS_CLI})
set(STORM_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_MAIN_FILE}) set(STORM_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_MAIN_FILE})
set(STORM_DFT_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_DFT_MAIN_FILE}) set(STORM_DFT_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_DFT_MAIN_FILE})
set(STORM_PGCL_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_PGCL_MAIN_FILE}) set(STORM_PGCL_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_PGCL_MAIN_FILE})
set(STORM_GSPN_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_GSPN_MAIN_FILE})
set(STORM_MAIN_HEADERS ${STORM_HEADERS_CLI}) set(STORM_MAIN_HEADERS ${STORM_HEADERS_CLI})
file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/*.h ${PROJECT_SOURCE_DIR}/src/*.cpp) file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/*.h ${PROJECT_SOURCE_DIR}/src/*.cpp)
@ -40,7 +41,7 @@ endif(ADDITIONAL_LINK_DIRS)
############################################################################### ###############################################################################
## # ## #
## Executable Creation #
## Executable Creation #
## # ## #
## All link_directories() calls MUST be made before this point # ## All link_directories() calls MUST be made before this point #
## # ## #
@ -59,6 +60,10 @@ add_executable(storm-pgcl-main ${STORM_PGCL_MAIN_SOURCES} ${STORM_MAIN_HEADERS})
target_link_libraries(storm-pgcl-main storm) target_link_libraries(storm-pgcl-main storm)
set_target_properties(storm-pgcl-main PROPERTIES OUTPUT_NAME "storm-pgcl") set_target_properties(storm-pgcl-main PROPERTIES OUTPUT_NAME "storm-pgcl")
add_executable(storm-gspn-main ${STORM_GSPN_MAIN_SOURCES} ${STORM_MAIN_HEADERS})
target_link_libraries(storm-gspn-main storm) # Adding headers for xcode
set_target_properties(storm-gspn-main PROPERTIES OUTPUT_NAME "storm-gspn")
target_link_libraries(storm ${STORM_LINK_LIBRARIES}) target_link_libraries(storm ${STORM_LINK_LIBRARIES})

14
src/adapters/CarlAdapter.h
View File

@ -6,6 +6,10 @@
#include <boost/multiprecision/gmp.hpp> #include <boost/multiprecision/gmp.hpp>
#ifdef STORM_HAVE_CLN
#include <cln/cln.h>
#endif
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
#include <carl/numbers/numbers.h> #include <carl/numbers/numbers.h>
@ -44,15 +48,23 @@ namespace carl {
} }
inline size_t hash_value(mpq_class const& q) {
std::hash<mpq_class> h;
return h(q);
}
#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_NUMBERS
namespace cln { namespace cln {
inline size_t hash_value(cl_RA const& n) { inline size_t hash_value(cl_RA const& n) {
std::hash<cln::cl_RA> h; std::hash<cln::cl_RA> h;
return h(n); return h(n);
} }
} }
#endif
namespace storm { namespace storm {
#if defined STORM_HAVE_CLN && defined USE_CLN_NUMBERS
#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_NUMBERS
typedef cln::cl_RA RationalNumber; typedef cln::cl_RA RationalNumber;
#else #else
typedef mpq_class RationalNumber; typedef mpq_class RationalNumber;

2
src/builder/ExplicitDFTModelBuilder.cpp
View File

@ -2,7 +2,7 @@
#include <src/models/sparse/MarkovAutomaton.h> #include <src/models/sparse/MarkovAutomaton.h>
#include <src/models/sparse/Ctmc.h> #include <src/models/sparse/Ctmc.h>
#include <src/utility/constants.h> #include <src/utility/constants.h>
#include <src/utility/vector.h>
#include "src/utility/vector.h"
#include <src/exceptions/UnexpectedException.h> #include <src/exceptions/UnexpectedException.h>
#include <map> #include <map>

326
src/builder/ExplicitGspnModelBuilder.cpp
View File

@ -0,0 +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<typename ValueType>
storm::models::sparse::MarkovAutomaton<ValueType> ExplicitGspnModelBuilder<ValueType>::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<uint_fast64_t>(numberOfTotalBits, 100);
builder = storm::storage::SparseMatrixBuilder<double>(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<ValueType> 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<storm::expressions::ExpressionManager>();
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<double> 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<double>(matrix, labeling, markovianStates, exitRates);
}
template<typename ValueType>
void ExplicitGspnModelBuilder<ValueType>::addRowForPartitions(std::vector<std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>> 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<uint_fast64_t , double, storm::builder::ExplicitGspnModelBuilder<ValueType>::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<typename ValueType>
void ExplicitGspnModelBuilder<ValueType>::addRowForTimedTransitions(std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> const& enabledTimedTransitions, storm::gspn::Marking const& currentMarking, double const& accRate) {
std::map<uint_fast64_t , double, storm::builder::ExplicitGspnModelBuilder<ValueType>::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<typename ValueType>
void ExplicitGspnModelBuilder<ValueType>::addValuesToBuilder(std::map<uint_fast64_t , double, storm::builder::ExplicitGspnModelBuilder<ValueType>::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<typename ValueType>
std::vector<std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>> ExplicitGspnModelBuilder<ValueType>::partitonEnabledImmediateTransitions(
storm::gspn::Marking const& marking,
std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> const& enabledImmediateTransitions) {
decltype(partitonEnabledImmediateTransitions(marking, enabledImmediateTransitions)) result;
std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> 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<typename ValueType>
double ExplicitGspnModelBuilder<ValueType>::getAccumulatedWeight(std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> const& vector) const {
double result = 0;
for (auto &trans : vector) {
result += trans->getWeight();
}
return result;
}
template<typename ValueType>
void ExplicitGspnModelBuilder<ValueType>::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<typename ValueType>
std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> ExplicitGspnModelBuilder<ValueType>::getEnabledTimedTransition(
storm::gspn::Marking const& marking) {
std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>>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<typename ValueType>
std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> ExplicitGspnModelBuilder<ValueType>::getEnabledImmediateTransition(
storm::gspn::Marking const& marking) {
std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>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<typename ValueType>
double ExplicitGspnModelBuilder<ValueType>::getAccumulatedRate(std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> const& vector) {
double result = 0;
for (auto trans_ptr : vector) {
result += trans_ptr->getRate();
}
return result;
}
template<typename ValueType>
storm::storage::BitVector ExplicitGspnModelBuilder<ValueType>::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<typename ValueType>
uint_fast64_t ExplicitGspnModelBuilder<ValueType>::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<storm::storage::BitVector>(bitvector));
}
return index;
}
template<typename ValueType>
storm::models::sparse::StateLabeling ExplicitGspnModelBuilder<ValueType>::getStateLabeling() const {
storm::models::sparse::StateLabeling labeling(markings.size());
std::map<uint_fast64_t , std::string> 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<double>;
}
}

172
src/builder/ExplicitGspnModelBuilder.h
View File

@ -0,0 +1,172 @@
#ifndef STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_
#define STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_
#include <string>
#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<typename ValueType=double>
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<ValueType> 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<std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>> 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<std::shared_ptr<storm::gspn::TimedTransition<double>>> 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<uint_fast64_t , double, storm::builder::ExplicitGspnModelBuilder<ValueType>::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<std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>> partitonEnabledImmediateTransitions(storm::gspn::Marking const& marking, std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> 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<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> 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<std::shared_ptr<storm::gspn::TimedTransition<double>>> 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<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> 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<std::shared_ptr<storm::gspn::TimedTransition<double>>> 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<uint_fast64_t, uint_fast64_t> 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<uint_fast64_t> markings = storm::storage::BitVectorHashMap<uint_fast64_t>(64, 1);
// a list of markings for which the outgoing edges need to be computed
std::deque<std::shared_ptr<storm::storage::BitVector>> 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<double> builder;
// contains the current row index during the computation
uint_fast64_t currentRowIndex;
};
}
}
#endif //STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_

573
src/parser/GspnParser.cpp
View File

@ -0,0 +1,573 @@
#include "src/parser/GspnParser.h"
#include <iostream>
#include <xercesc/dom/DOM.hpp>
#include <xercesc/sax/HandlerBase.hpp>
#include <xercesc/util/PlatformUtils.hpp>
#include "src/exceptions/UnexpectedException.h"
#include "src/storage/gspn/Place.h"
#include "src/storage/gspn/ImmediateTransition.h"
#include "src/utility/macros.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
try {
xercesc::XMLPlatformUtils::Initialize();
}
catch (xercesc::XMLException const& toCatch) {
// 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());
}
catch (xercesc::XMLException const& toCatch) {
auto message = xercesc::XMLString::transcode(toCatch.getMessage());
// Error occurred while parsing the file. Abort constructing the gspn since the input file is not valid
// or the parser run into a problem.
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, message);
xercesc::XMLString::release(&message);
}
catch (const xercesc::DOMException& toCatch) {
auto message = xercesc::XMLString::transcode(toCatch.msg);
// Error occurred while parsing the file. Abort constructing the gspn since the input file is not valid
// or the parser run into a problem.
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, message);
xercesc::XMLString::release(&message);
}
catch (...) {
// Error occurred while parsing the file. Abort constructing the gspn since the input file is not valid
// 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 the top-level node is not a "pnml" node, then throw an exception.
STORM_LOG_THROW(getName(elementRoot).compare("pnml") == 0, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n");
traversePnmlElement(elementRoot);
// 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<bool, uint_fast64_t> numberOfInitialTokens(false, defaultNumberOfInitialTokens);
std::pair<bool, int_fast64_t> 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<bool, bool> timed(false, defaultTransitionType);
std::pair<bool, std::string> 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<storm::gspn::GSPN::RateType> 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<storm::gspn::GSPN::WeightType> 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<bool, std::string> source(false, "");
std::pair<bool, std::string> target(false, "");
std::pair<bool, std::string> type(false, defaultArcType);
std::pair<bool, uint_fast64_t> 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;
}
}
}

165
src/parser/GspnParser.h
View File

@ -0,0 +1,165 @@
#ifndef STORM_PARSER_GSPNPARSER_H_
#define STORM_PARSER_GSPNPARSER_H_
#include <string>
#include <xercesc/parsers/XercesDOMParser.hpp>
#include <xercesc/util/XMLString.hpp>
#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);
// 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;
};
}
}
#endif //STORM_PARSER_GSPNPARSER_H_

10
src/solver/stateelimination/EliminatorBase.cpp
View File

@ -49,7 +49,8 @@ namespace storm {
} else if (Mode == ScalingMode::DivideOneMinus) { } else if (Mode == ScalingMode::DivideOneMinus) {
if (hasEntryInColumn) { if (hasEntryInColumn) {
STORM_LOG_ASSERT(columnValue != storm::utility::one<ValueType>(), "The scaling mode 'divide-one-minus' requires a non-one value in the given column."); STORM_LOG_ASSERT(columnValue != storm::utility::one<ValueType>(), "The scaling mode 'divide-one-minus' requires a non-one value in the given column.");
columnValue = storm::utility::simplify(storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - columnValue));
columnValue = storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - columnValue);
columnValue = storm::utility::simplify(columnValue);
} }
} }
@ -57,7 +58,8 @@ namespace storm {
for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); entryIt != entryIte; ++entryIt) { for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); entryIt != entryIte; ++entryIt) {
// Only scale the entries in a different column. // Only scale the entries in a different column.
if (entryIt->getColumn() != column) { if (entryIt->getColumn() != column) {
entryIt->setValue(storm::utility::simplify(entryIt->getValue() * columnValue));
auto tmpVal = entryIt->getValue() * columnValue;
entryIt->setValue(storm::utility::simplify(tmpVal));
} }
} }
updateValue(column, columnValue); updateValue(column, columnValue);
@ -145,7 +147,9 @@ namespace storm {
*result = *first1; *result = *first1;
++first1; ++first1;
} else { } else {
auto probability = storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue()));
ValueType sprod = multiplyFactor * first2->getValue();
ValueType sum = first1->getValue() + storm::utility::simplify(sprod);
auto probability = storm::utility::simplify(sum);
*result = storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type>(first1->getColumn(), probability); *result = storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type>(first1->getColumn(), probability);
newBackwardEntries[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability); newBackwardEntries[successorOffsetInNewBackwardTransitions].emplace_back(predecessor, probability);
++first1; ++first1;

516
src/storage/gspn/GSPN.cpp
View File

@ -0,0 +1,516 @@
#include "src/storage/gspn/GSPN.h"
#include <src/utility/macros.h>
#include <boost/lexical_cast.hpp>
namespace storm {
namespace gspn {
void GSPN::addImmediateTransition(storm::gspn::ImmediateTransition<WeightType> const& transition) {
this->immediateTransitions.push_back(std::make_shared<storm::gspn::ImmediateTransition<WeightType>>(transition));
}
void GSPN::addTimedTransition(storm::gspn::TimedTransition<RateType> const& transition) {
this->timedTransitions.push_back(std::make_shared<storm::gspn::TimedTransition<RateType>>(transition));
}
void GSPN::addPlace(Place const& place) {
this->places.push_back(place);
}
uint_fast64_t GSPN::getNumberOfPlaces() const {
return places.size();
}
std::vector<std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>>> const& GSPN::getTimedTransitions() const {
return this->timedTransitions;
}
std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>>> const& GSPN::getImmediateTransitions() const {
return this->immediateTransitions;
}
std::vector<storm::gspn::Place> const& GSPN::getPlaces() const {
return places;
}
std::shared_ptr<storm::gspn::Marking> GSPN::getInitialMarking(std::map<uint_fast64_t, uint_fast64_t>& numberOfBits, uint_fast64_t const& numberOfTotalBits) const {
auto m = std::make_shared<storm::gspn::Marking>(getNumberOfPlaces(), numberOfBits, numberOfTotalBits);
for (auto& place : getPlaces()) {
m->setNumberOfTokensAt(place.getID(), place.getNumberOfInitialTokens());
}
return m;
}
std::pair<bool, storm::gspn::Place> GSPN::getPlace(std::string const& id) const {
for (auto& place : places) {
if (id.compare(place.getName()) == 0) {
return std::make_pair<bool, storm::gspn::Place const&>(true, place);
}
}
return std::make_pair<bool, storm::gspn::Place>(false, storm::gspn::Place());
}
std::pair<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const> GSPN::getTimedTransition(std::string const& id) const {
for (auto& trans : timedTransitions) {
if (id.compare(trans->getName()) == 0) {
return std::make_pair<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const>(true, static_cast<std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const>(trans));
}
}
return std::make_pair<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const>(false, nullptr);
}
std::pair<bool, std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> const> GSPN::getImmediateTransition(std::string const& id) const {
for (auto& trans : immediateTransitions) {
if (id.compare(trans->getName()) == 0) {
return std::make_pair<bool, std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> const>(true, static_cast<std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> const>(trans));
}
}
return std::make_pair<bool, std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> const>(false, nullptr);
}
std::pair<bool, std::shared_ptr<storm::gspn::Transition> const> GSPN::getTransition(std::string const& id) const {
auto trans = getTimedTransition(id);
if (trans.first == true) {
return trans;
}
return getImmediateTransition(id);
}
void GSPN::writeDotToStream(std::ostream& outStream) {
outStream << "digraph " << this->getName() << " {" << std::endl;
// print places with initial marking (not printed is the capacity)
outStream << "\t" << "node [shape=ellipse]" << std::endl;
for (auto& place : this->getPlaces()) {
outStream << "\t" << place.getName() << " [label=\"" << place.getName() << "(" << place.getNumberOfInitialTokens();
outStream << ")\"];" << std::endl;
}
// print transitions with weight/rate
outStream << "\t" << "node [shape=box]" << std::endl;
for (auto& trans : this->getImmediateTransitions()) {
outStream << "\t" << trans->getName() << " [label=\"" << trans->getName();
outStream << "(immediate:" << trans->getWeight() << ")\"];" << std::endl;
}
for (auto& trans : this->getTimedTransitions()) {
outStream << "\t" << trans->getName() << " [label=\"" << trans->getName();
outStream << "(timed:" << trans->getRate() << ")\"];" << std::endl;
}
// print arcs
for (auto& trans : this->getImmediateTransitions()) {
auto it = trans->getInputPlacesCBegin();
while (it != trans->getInputPlacesCEnd()) {
outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"normal:" <<
trans->getInputArcMultiplicity(**it);
outStream << "\"];" << std::endl;
++it;
}
it = trans->getInhibitionPlacesCBegin();
while (it != trans->getInhibitionPlacesCEnd()) {
outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"inhibition:" <<
trans->getInhibitionArcMultiplicity(**it);
outStream << "\"];" << std::endl;
++it;
}
it = trans->getOutputPlacesCBegin();
while (it != trans->getOutputPlacesCEnd()) {
outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" <<
trans->getOutputArcMultiplicity(**it);
outStream << "\"];" << std::endl;
++it;
}
}
for (auto& trans : this->getTimedTransitions()) {
auto it = trans->getInputPlacesCBegin();
while (it != trans->getInputPlacesCEnd()) {
outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"normal:" <<
trans->getInputArcMultiplicity(**it);
outStream << "\"];" << std::endl;
++it;
}
it = trans->getInhibitionPlacesCBegin();
while (it != trans->getInhibitionPlacesCEnd()) {
outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"inhibition:" <<
trans->getInhibitionArcMultiplicity(**it);
outStream << "\"];" << std::endl;
++it;
}
it = trans->getOutputPlacesCBegin();
while (it != trans->getOutputPlacesCEnd()) {
outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" <<
trans->getOutputArcMultiplicity(**it);
outStream << "\"];" << std::endl;
++it;
}
}
outStream << "}" << std::endl;
}
void GSPN::setName(std::string const& name) {
this->name = name;
}
std::string const& GSPN::getName() const {
return this->name;
}
bool GSPN::isValid() const {
bool result = true;
result |= testPlaces();
result |= testTransitions();
return result;
}
bool GSPN::testPlaces() const {
std::vector<std::string> namesOfPlaces;
std::vector<uint_fast64_t> idsOfPlaces;
bool result = true;
for (auto const& place : this->getPlaces()) {
if (std::find(namesOfPlaces.begin(), namesOfPlaces.end(), place.getName()) != namesOfPlaces.end()) {
STORM_PRINT_AND_LOG("duplicates states with the name \"" + place.getName() + "\"\n")
result = false;
}
if (std::find(idsOfPlaces.begin(), idsOfPlaces.end(), place.getID()) != idsOfPlaces.end()) {
STORM_PRINT_AND_LOG("duplicates states with the id \"" + boost::lexical_cast<std::string>(place.getID()) + "\"\n")
result = false;
}
if (place.getNumberOfInitialTokens() > place.getNumberOfInitialTokens()) {
STORM_PRINT_AND_LOG("number of initial tokens is greater than the capacity for place \"" + place.getName() + "\"\n")
result = false;
}
}
return result;
}
bool GSPN::testTransitions() const {
bool result = true;
for (auto const& transition : this->getImmediateTransitions()) {
if (transition->getInputPlacesCBegin() == transition->getInputPlacesCEnd() &&
transition->getInhibitionPlacesCBegin() == transition->getInhibitionPlacesCEnd()) {
STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n")
result = false;
}
if (transition->getOutputPlacesCBegin() == transition->getOutputPlacesCEnd()) {
STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n")
result = false;
}
}
for (auto const& transition : this->getTimedTransitions()) {
if (transition->getInputPlacesCBegin() == transition->getInputPlacesCEnd() &&
transition->getInhibitionPlacesCBegin() == transition->getInhibitionPlacesCEnd()) {
STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n")
result = false;
}
if (transition->getOutputPlacesCBegin() == transition->getOutputPlacesCEnd()) {
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 it = transition->getInputPlacesCBegin(); it != transition->getInputPlacesCEnd(); ++it) {
bool foundPlace = false;
for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
foundPlace = true;
}
}
if (!foundPlace) {
STORM_PRINT_AND_LOG("input place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
result = false;
}
}
for (auto it = transition->getInhibitionPlacesCBegin(); it != transition->getInhibitionPlacesCEnd(); ++it) {
bool foundPlace = false;
for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
foundPlace = true;
}
}
if (!foundPlace) {
STORM_PRINT_AND_LOG("inhibition place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
result = false;
}
}
for (auto it = transition->getOutputPlacesCBegin(); it != transition->getOutputPlacesCEnd(); ++it) {
bool foundPlace = false;
for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
foundPlace = true;
}
}
if (!foundPlace) {
STORM_PRINT_AND_LOG("output place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
result = false;
}
}
}
for (auto const& transition : this->getTimedTransitions()) {
for (auto it = transition->getInputPlacesCBegin(); it != transition->getInputPlacesCEnd(); ++it) {
bool foundPlace = false;
for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
foundPlace = true;
}
}
if (!foundPlace) {
STORM_PRINT_AND_LOG("input place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
result = false;
}
}
for (auto it = transition->getInhibitionPlacesCBegin(); it != transition->getInhibitionPlacesCEnd(); ++it) {
bool foundPlace = false;
for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
foundPlace = true;
}
}
if (!foundPlace) {
STORM_PRINT_AND_LOG("inhibition place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
result = false;
}
}
for (auto it = transition->getOutputPlacesCBegin(); it != transition->getOutputPlacesCEnd(); ++it) {
bool foundPlace = false;
for (auto const& place : places) {
if (place.getName() == (*it)->getName()) {
foundPlace = true;
}
}
if (!foundPlace) {
STORM_PRINT_AND_LOG("output place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
result = false;
}
}
}
return result;
}
void GSPN::toPnpro(std::ostream &stream) const {
auto space = " ";
auto space2 = " ";
auto space3 = " ";
auto projectName = "storm-export"; // TODO add to args
stream << "<project name=\"" << projectName << "\" version=\"121\">" << std::endl;
stream << space << "<gspn name=\"" << getName() << "\" >" << std::endl;
u_int32_t x = 1;
stream << space2 << "<nodes>" << std::endl;
for (auto& place : places) {
stream << space3 << "<place marking=\"" << place.getNumberOfInitialTokens() <<"\" ";
stream << "name =\"" << place.getName() << "\" ";
stream << "x=\"" << x << "\" ";
stream << "y=\"1\" ";
stream << "/>" << std::endl;
x = x + 3;
}
x = 1;
for (auto& trans : timedTransitions) {
stream << space3 << "<transition name=\"" << trans->getName() << "\" ";
stream << "type=\"EXP\" ";
stream << "nservers-x=\"" << trans->getRate() << "\" ";
stream << "x=\"" << x << "\" ";
stream << "y=\"4\" ";
stream << "/>" << std::endl;
x = x + 3;
}
for (auto& trans : immediateTransitions) {
stream << space3 << "<transition name=\"" << trans->getName() << "\" ";
stream << "type=\"IMM\" ";
stream << "x=\"" << x << "\" ";
stream << "y=\"4\" ";
stream << "/>" << std::endl;
x = x + 3;
}
stream << space2 << "</nodes>" << std::endl;
stream << space2 << "<edges>" << std::endl;
for (auto& trans : timedTransitions) {
for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) {
stream << space3 << "<arc ";
stream << "head=\"" << trans->getName() << "\" ";
stream << "tail=\"" << (*it)->getName() << "\" ";
stream << "kind=\"INPUT\" ";
stream << "mult=\"" << trans->getInputArcMultiplicity(**it) << "\" ";
stream << "/>" << std::endl;
}
for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) {
stream << space3 << "<arc ";
stream << "head=\"" << trans->getName() << "\" ";
stream << "tail=\"" << (*it)->getName() << "\" ";
stream << "kind=\"INHIBITOR\" ";
stream << "mult=\"" << trans->getInhibitionArcMultiplicity(**it) << "\" ";
stream << "/>" << std::endl;
}
for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) {
stream << space3 << "<arc ";
stream << "head=\"" << (*it)->getName() << "\" ";
stream << "tail=\"" << trans->getName() << "\" ";
stream << "kind=\"OUTPUT\" ";
stream << "mult=\"" << trans->getOutputArcMultiplicity(**it) << "\" ";
stream << "/>" << std::endl;
}
}
for (auto& trans : immediateTransitions) {
for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) {
stream << space3 << "<arc ";
stream << "head=\"" << trans->getName() << "\" ";
stream << "tail=\"" << (*it)->getName() << "\" ";
stream << "kind=\"INPUT\" ";
stream << "mult=\"" << trans->getInputArcMultiplicity(**it) << "\" ";
stream << "/>" << std::endl;
}
for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) {
stream << space3 << "<arc ";
stream << "head=\"" << trans->getName() << "\" ";
stream << "tail=\"" << (*it)->getName() << "\" ";
stream << "kind=\"INHIBITOR\" ";
stream << "mult=\"" << trans->getInhibitionArcMultiplicity(**it) << "\" ";
stream << "/>" << std::endl;
}
for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) {
stream << space3 << "<arc ";
stream << "head=\"" << (*it)->getName() << "\" ";
stream << "tail=\"" << trans->getName() << "\" ";
stream << "kind=\"OUTPUT\" ";
stream << "mult=\"" << trans->getOutputArcMultiplicity(**it) << "\" ";
stream << "/>" << std::endl;
}
}
stream << space2 << "</edges>" << std::endl;
stream << space << "</gspn>" << std::endl;
stream << "</project>" << std::endl;
}
void GSPN::toPnml(std::ostream &stream) const {
std::string space = " ";
std::string space2 = " ";
std::string space3 = " ";
std::string space4 = " ";
stream << "<pnml>" << std::endl;
stream << space << "<net id=\"" << getName() << "\">" << std::endl;
// add places
for (const auto &place : places) {
stream << space2 << "<place id=\"" << place.getName() << "\">" << std::endl;
stream << space3 << "<initialMarking>" << std::endl;
stream << space4 << "<value>Default," << place.getNumberOfInitialTokens() << "</value>" << std::endl;
stream << space3 << "</initialMarking>" << std::endl;
stream << space2 << "</place>" << std::endl;
}
// add immediate transitions
for (const auto &trans : immediateTransitions) {
stream << space2 << "<transition id=\"" << trans->getName() << "\">" << std::endl;
stream << space3 << "<rate>" << std::endl;
stream << space4 << "<value>" << trans->getWeight() << "</value>" << std::endl;
stream << space3 << "</rate>" << std::endl;
stream << space3 << "<timed>" << std::endl;
stream << space4 << "<value>false</value>" << std::endl;
stream << space3 << "</timed>" << std::endl;
stream << space2 << "</transition>" << std::endl;
}
// add timed transitions
for (const auto &trans : timedTransitions) {
stream << space2 << "<transition id=\"" << trans->getName() << "\">" << std::endl;
stream << space3 << "<rate>" << std::endl;
stream << space4 << "<value>" << trans->getRate() << "</value>" << std::endl;
stream << space3 << "</rate>" << std::endl;
stream << space3 << "<timed>" << std::endl;
stream << space4 << "<value>true</value>" << std::endl;
stream << space3 << "</timed>" << std::endl;
stream << space2 << "</transition>" << std::endl;
}
uint_fast64_t i = 0;
// add arcs for immediate transitions
for (const auto &trans : immediateTransitions) {
// add input arcs
for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) {
stream << space2 << "<arc ";
stream << "id=\"arc" << i++ << "\" ";
stream << "source=\"" << (*it)->getName() << "\" ";
stream << "target=\"" << trans->getName() << "\" ";
stream << ">" << std::endl;
stream << space3 << "<inscription>" << std::endl;
stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(**it) << "</value>" << std::endl;
stream << space3 << "</inscription>" << std::endl;
stream << space3 << "<type value=\"normal\" />" << std::endl;
stream << space2 << "</arc>" << std::endl;
}
// add inhibition arcs
for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) {
stream << space2 << "<arc ";
stream << "id=\"arc" << i++ << "\" ";
stream << "source=\"" << (*it)->getName() << "\" ";
stream << "target=\"" << trans->getName() << "\" ";
stream << ">" << std::endl;
stream << space3 << "<inscription>" << std::endl;
stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(**it) << "</value>" << std::endl;
stream << space3 << "</inscription>" << std::endl;
stream << space3 << "<type value=\"inhibition\" />" << std::endl;
stream << space2 << "</arc>" << std::endl;
}
// add output arcs
for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) {
stream << space2 << "<arc ";
stream << "id=\"arc" << i++ << "\" ";
stream << "source=\"" << trans->getName() << "\" ";
stream << "target=\"" << (*it)->getName() << "\" ";
stream << ">" << std::endl;
stream << space3 << "<inscription>" << std::endl;
stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(**it) << "</value>" << std::endl;
stream << space3 << "</inscription>" << std::endl;
stream << space3 << "<type value=\"normal\" />" << std::endl;
stream << space2 << "</arc>" << std::endl;
}
}
stream << space << "</net>" << std::endl;
stream << "</pnml>" << std::endl;
}
}
}

183
src/storage/gspn/GSPN.h
View File

@ -0,0 +1,183 @@
#ifndef STORM_STORAGE_GSPN_GSPN_H
#define STORM_STORAGE_GSPN_GSPN_H
#include <iostream>
#include <stdint.h>
#include <vector>
#include <memory>
#include "src/storage/gspn/ImmediateTransition.h"
#include "src/storage/gspn/Marking.h"
#include "src/storage/gspn/Place.h"
#include "src/storage/gspn/TimedTransition.h"
namespace storm {
namespace gspn {
// Stores a GSPN
class GSPN {
public:
// 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<WeightType> const& transition);
/*!
* Adds a timed transition to the gspn.
*
* @param transition The transition which is added to the gspn.
*/
void addTimedTransition(TimedTransition<RateType> const& transition);
/*!
* Adds a place to the gspn.
*
* @param place The place which is added to the gspn.
*/
void addPlace(Place const& place);
/*!
* Returns the number of places in this gspn.
*
* @return The number of places.
*/
uint_fast64_t getNumberOfPlaces() const;
/*!
* Returns the vector of timed transitions in this gspn.
*
* @return The vector of timed transitions.
*/
std::vector<std::shared_ptr<TimedTransition<GSPN::RateType>>> const& getTimedTransitions() const;
/*!
* Returns the vector of immediate transitions in this gspn.
*
* @return The vector of immediate tansitions.
*/
std::vector<std::shared_ptr<ImmediateTransition<GSPN::WeightType>>> const& getImmediateTransitions() const;
/*!
* Returns the places of this gspn
*/
std::vector<storm::gspn::Place> const& getPlaces() const;
/*
* Computes the initial marking of the gspn.
*
* @param map The Map determines the number of bits for each place.
* @return The initial Marking
*/
std::shared_ptr<storm::gspn::Marking> getInitialMarking(std::map<uint_fast64_t, uint_fast64_t>& numberOfBits, uint_fast64_t const& numberOfTotalBits) const;
/*!
* Returns the place with the corresponding id.
*
* @param id The ID of the place.
* @return The first element is true if the place was found.
* If the first element is true, then the second element is the wanted place.
* If the first element is false, then the second element is not defined.
*/
std::pair<bool, storm::gspn::Place> getPlace(std::string const& id) 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<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> 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<bool, std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> 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<storm::gspn::Transition> getTransition(std::string const& id) const;
std::pair<bool, std::shared_ptr<storm::gspn::Transition> const> getTransition(std::string const& id) const;
/*!
* Write the gspn in a dot(graphviz) configuration.
*
* @param outStream The stream to which the output is written to.
*/
void writeDotToStream(std::ostream& outStream);
/*!
* Set the name of the gspn to the given name.
*
* @param name The new name.
*/
void setName(std::string const& name);
/*!
* Returns the name of the gspn.
*
* @return The name.
*/
std::string const& getName() const;
/*!
* Performe some checks
* - testPlaces()
* - testTransitions()
*
* @return true if no errors are found
*/
bool isValid() const;
// TODO doc
void toPnpro(std::ostream &stream) const;
// TODO doc
void toPnml(std::ostream &stream) const;
private:
/*!
* Test
* - if places are unique (ids and names)
* - if the capacity is greater than the number of initial tokens
*
* @return true if no errors found
*/
bool testPlaces() const;
/*!
* Test
* - if transition have at least on input/inhibitor and one output place
*
* @return true if no errors found
*/
bool testTransitions() const;
// set containing all immediate transitions
std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<WeightType>>> immediateTransitions;
// set containing all timed transitions
std::vector<std::shared_ptr<storm::gspn::TimedTransition<RateType>>> timedTransitions;
// set containing all places
std::vector<storm::gspn::Place> places;
// name of the gspn
std::string name;
};
}
}
#endif //STORM_STORAGE_GSPN_GSPN_H

90
src/storage/gspn/GspnBuilder.cpp
View File

@ -0,0 +1,90 @@
#include <src/exceptions/IllegalFunctionCallException.h>
#include "GspnBuilder.h"
#include "src/utility/macros.h"
#include "src/exceptions/IllegalFunctionCallException.h"
#include "Place.h"
namespace storm {
namespace gspn {
void GspnBuilder::addPlace(uint_fast64_t const& id, int_fast64_t const& capacity, uint_fast64_t const& initialTokens) {
addPlace(id, "place_" + std::to_string(id), capacity, initialTokens);
}
void GspnBuilder::addPlace(uint_fast64_t const& id, std::string const& name, int_fast64_t const& capacity, uint_fast64_t const& initialTokens) {
auto place = storm::gspn::Place();
place.setCapacity(capacity);
place.setID(id);
place.setName(name);
place.setNumberOfInitialTokens(initialTokens);
idToPlaceName.insert(std::pair<uint_fast64_t const, std::string const>(id, name));
gspn.addPlace(place);
}
void GspnBuilder::addImmediateTransition(uint_fast64_t const& id, uint_fast64_t const& priority, double const& weight) {
auto trans = storm::gspn::ImmediateTransition<double>();
trans.setName(std::to_string(id));
trans.setPriority(priority);
trans.setWeight(weight);
gspn.addImmediateTransition(trans);
}
void GspnBuilder::addTimedTransition(uint_fast64_t const &id, uint_fast64_t const &priority, double const &rate) {
auto trans = storm::gspn::TimedTransition<double>();
trans.setName(std::to_string(id));
trans.setPriority(priority);
trans.setRate(rate);
gspn.addTimedTransition(trans);
}
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(idToPlaceName.at(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);
}
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.");
}
auto placePair = gspn.getPlace(idToPlaceName.at(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);
}
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.");
}
auto placePair = gspn.getPlace(idToPlaceName.at(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.");
}
std::get<1>(transPair)->setOutputArcMultiplicity(std::get<1>(placePair), multiplicity);
}
storm::gspn::GSPN const& GspnBuilder::buildGspn() const {
return gspn;
}
}
}

89
src/storage/gspn/GspnBuilder.h
View File

@ -0,0 +1,89 @@
#ifndef STORM_STORAGE_GSPN_GSPNBUILDER_H
#define STORM_STORAGE_GSPN_GSPNBUILDER_H
#include <map>
#include <string>
#include <vector>
#include "GSPN.h"
namespace storm {
namespace gspn {
class GspnBuilder {
public:
/**
* Add a place to the gspn.
* @param id The id must be unique for the gspn.
* @param capacity The capacity is the limit of tokens in the place.
* A capacity of -1 indicates an unbounded place.
* @param initialTokens The number of inital tokens in the place.
*/
void addPlace(uint_fast64_t const& id, int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0);
/**
* Add a place to the gspn.
* @param id The id must be unique for the gspn.
* @param name The name must be unique for the gspn.
* @param capacity The capacity is the limit of tokens in the place.
* A capacity of -1 indicates an unbounded place.
* @param initialTokens The number of inital tokens in the place.
*/
void addPlace(uint_fast64_t const& id, std::string const& name, int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0);
/**
* Adds an immediate transition to the gspn.
* @param id The id must be unique for the gspn.
* @param priority The priority for the transtion.
* @param weight The weight for the transition.
*/
void addImmediateTransition(uint_fast64_t const& id, uint_fast64_t const& priority = 0, double const& weight = 0);
/**
* Adds an timed transition to the gspn.
* @param id The name id be unique for the gspn.
* @param priority The priority for the transtion.
* @param weight The weight for the transition.
*/
void addTimedTransition(uint_fast64_t const &id, uint_fast64_t const &priority = 0, double const &rate = 0);
/**
* Adds an new input arc from a place to an transition.
* @param from The place from which the arc is originating.
* @param to The transtion to which the arc goes to.
* @param multiplicity The multiplicity of the arc.
*/
void addInputArc(uint_fast64_t const &from, uint_fast64_t const &to, uint_fast64_t const &multiplicity = 1);
/**
* Adds an new input arc from a place to an transition.
* @param from The place from which the arc is originating.
* @param to The transtion to which the arc goes to.
* @param multiplicity The multiplicity of the arc.
*/
void addInhibitionArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity = 1);
/**
* Adds an new input arc from a place to an transition.
* @param from The place from which the arc is originating.
* @param to The transtion to which the arc goes to.
* @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);
/**
*
* @return The gspn which is constructed by the builder.
*/
storm::gspn::GSPN const& buildGspn() const;
private:
// gspn which is returned
storm::gspn::GSPN gspn;
// map from ids to names (for places)
std::map<uint_fast64_t const, std::string const> idToPlaceName;
};
}
}
#endif //STORM_STORAGE_GSPN_GSPNBUILDER_H

43
src/storage/gspn/ImmediateTransition.h
View File

@ -0,0 +1,43 @@
#ifndef STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_
#define STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_
#include "src/storage/gspn/Transition.h"
#include "src/utility/constants.h"
namespace storm {
namespace gspn {
template <typename WeightType>
class ImmediateTransition : public storm::gspn::Transition {
public:
/*!
* Sets the weight of this transition to the given value.
*
* @param weight The new weight for this transition.
*/
void setWeight(WeightType const& weight) {
this->weight = weight;
}
/*!
* Retrieves the weight of this transition.
*
* @return The weight of this transition.
*/
WeightType getWeight() const {
return this->weight;
}
/**
* True iff no weight is attached.
*/
bool noWeightAttached() {
return storm::utility::isZero(weight);
}
private:
// the weight of the transition. Must be positive, if zero, then no weight is attached.
WeightType weight;
};
}
}
#endif //STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_

59
src/storage/gspn/Marking.cpp
View File

@ -0,0 +1,59 @@
#include <stdint.h>
#include "src/storage/gspn/Marking.h"
namespace storm {
namespace gspn {
Marking::Marking(uint_fast64_t const& numberOfPlaces, std::map<uint_fast64_t, uint_fast64_t> const& numberOfBits, uint_fast64_t const& numberOfTotalBits) {
this->numberOfPlaces = numberOfPlaces;
this->numberOfBits = numberOfBits;
this->marking = storm::storage::BitVector(numberOfTotalBits);
}
Marking::Marking(uint_fast64_t const& numberOfPlaces, std::map<uint_fast64_t, uint_fast64_t> const& numberOfBits, storm::storage::BitVector const& bitvector) {
this->numberOfPlaces = numberOfPlaces;
this->numberOfBits = numberOfBits;
this->marking = bitvector;
}
uint_fast64_t Marking::getNumberOfPlaces() const {
return this->numberOfPlaces;
}
void Marking::setNumberOfTokensAt(uint_fast64_t const& place, uint_fast64_t const& numberOfTokens) {
uint_fast64_t index = 0;
for (uint_fast64_t i=0; i < place; ++i) {
index += numberOfBits[i];
}
marking.setFromInt(index, numberOfBits[place], numberOfTokens);
}
uint_fast64_t Marking::getNumberOfTokensAt(uint_fast64_t const& place) const {
uint_fast64_t index = 0;
for (uint_fast64_t i=0; i < place; ++i) {
index += numberOfBits.at(i);
}
return marking.getAsInt(index, numberOfBits.at(place));
}
std::shared_ptr<storm::storage::BitVector> Marking::getBitVector() const {
auto result = std::make_shared<storm::storage::BitVector>();
*result = storm::storage::BitVector(marking);
return result;
}
bool Marking::operator==(const Marking& other) const {
if (getNumberOfPlaces() != other.getNumberOfPlaces()) {
return false;
}
if (&numberOfBits == &other.numberOfBits) {
return marking == other.marking;
}
for (uint_fast64_t i=0; i < getNumberOfPlaces(); ++i) {
if (getNumberOfTokensAt(i) != other.getNumberOfTokensAt(i)) {
return false;
}
}
return true;
}
}
}

80
src/storage/gspn/Marking.h
View File

@ -0,0 +1,80 @@
#ifndef STORM_STORAGE_GSPN_MARKING_H_
#define STORM_STORAGE_GSPN_MARKING_H_
#include <cmath>
#include <map>
#include <memory>
#include "src/storage/BitVector.h"
namespace storm {
namespace gspn {
class Marking {
public:
/*!
* Creates an empty marking (at all places contain 0 tokens).
*
* @param numberOfPlaces The number of places of the gspn.
* @param numberOfBits The number of bits used to store the number of tokens for each place
* @param numberOfTotalBits The length of the internal bitvector
*/
Marking(uint_fast64_t const& numberOfPlaces, std::map<uint_fast64_t, uint_fast64_t> const& numberOfBits, uint_fast64_t const& numberOfTotalBits);
/*!
* Create the marking described by the bitvector.
*
* @param numberOfPlaces The number of places of the gspn.
* @param numberOfBits The number of bits used to store the number of tokens for each place
* @param bitvector The bitvector encoding the marking.
*/
Marking(uint_fast64_t const&numberOfPlaces, std::map<uint_fast64_t, uint_fast64_t> const& numberOfBits, storm::storage::BitVector const& bitvector);
/*!
* Retrieves the number of places for which the tokens are stored.
*
* @return The number of places.
*/
uint_fast64_t getNumberOfPlaces() const;
/*!
* Set the number of tokens for the given place to the given amount.
*
* @param place Place must be a valid place for which the number of tokens is changed.
* @param numberOfTokens The new number of tokens at the place.
*/
void setNumberOfTokensAt(uint_fast64_t const& place, uint_fast64_t const& numberOfTokens);
/*!
* Get the number of tokens for the given place.
*
* @param place The place from which the tokens are counted.
* @return The number of tokens at the place.
*/
uint_fast64_t getNumberOfTokensAt(uint_fast64_t const& place) const;
/*!
* Returns a copy of the bitvector
*
* @return The bitvector which encodes the marking
*/
std::shared_ptr<storm::storage::BitVector> getBitVector() const;
/*!
* Overload equality operator
*/
bool operator==(const Marking& other) const;
private:
// the maximal number of places in the gspn
uint_fast64_t numberOfPlaces;
// number of bits for each place
std::map<uint_fast64_t, uint_fast64_t> numberOfBits;
// contains the information of the marking
storm::storage::BitVector marking;
};
}
}
#endif //STORM_STORAGE_GSPN_MARKING_H_

41
src/storage/gspn/Place.cpp
View File

@ -0,0 +1,41 @@
#include "Place.h"
#include "src/exceptions/IllegalArgumentValueException.h"
#include "src/utility/macros.h"
namespace storm {
namespace gspn {
void Place::setName(std::string const& name) {
this->name = name;
}
std::string Place::getName() const {
return this->name;
}
void Place::setID(uint_fast64_t const& id) {
this->id = id;
}
uint_fast64_t Place::getID() const {
return this->id;
}
void Place::setNumberOfInitialTokens(uint_fast64_t const& tokens) {
this->numberOfInitialTokens = tokens;
}
uint_fast64_t Place::getNumberOfInitialTokens() const {
return this->numberOfInitialTokens;
}
void Place::setCapacity(int_fast64_t const& capacity) {
STORM_LOG_THROW(capacity >= -1, storm::exceptions::IllegalArgumentValueException, "The capacity cannot be less than -1.");
this->capacity = capacity;
}
int_fast64_t Place::getCapacity() const {
return this->capacity;
}
}
}

87
src/storage/gspn/Place.h
View File

@ -0,0 +1,87 @@
#ifndef STORM_STORAGE_GSPN_PLACE_H_
#define STORM_STORAGE_GSPN_PLACE_H_
#include <string>
namespace storm {
namespace gspn {
/*!
* This class provides methods to store and retrieve data for a place in a gspn.
*/
class Place {
public:
/*!
* Sets the name of this place. The name must be unique for a gspn.
*
* @param name The new name for the place.
*/
void setName(std::string const& name);
/*!
* Returns the name of this place.
*
* @return The name of this place.
*/
std::string getName() const;
/*!
* Sets the id of this place. The id must be unique for a gspn.
*
* @param id The new id of this place.
*/
void setID(uint_fast64_t const& id);
/*!
* Returns the id of this place.
*
* @return The id of this place.
*/
uint_fast64_t getID() const;
/*!
* Sets the number of initial tokens of this place.
*
* @param tokens The number of initial tokens.
*/
void setNumberOfInitialTokens(uint_fast64_t const& tokens);
/*!
* Returns the number of initial tokens of this place.
*
* @return The number of initial tokens of this place.
*/
uint_fast64_t getNumberOfInitialTokens() const;
/*!
* Sets the capacity of tokens of this place.
*
* @param capacity The capacity of this place. A non-negative number represents the capacity.
* The value -1 indicates that the capacity is not set.
*/
void setCapacity(int_fast64_t const& capacity);
/*!
* Returns the capacity of tokens of this place.
*
* @return The capacity of the place. The value -1 indicates that the capacity is not set.
*/
int_fast64_t getCapacity() const;
private:
// contains the number of initial tokens of this place
uint_fast64_t numberOfInitialTokens;
// unique id (is used to refer to a specific place in a bitvector)
uint_fast64_t id;
// name which is used in pnml file
std::string name;
// capacity of this place
// -1 indicates that the capacity is not set
// other non-negative values represents the capacity
int_fast64_t capacity;
};
}
}
#endif //STORM_STORAGE_GSPN_PLACE_H_

36
src/storage/gspn/TimedTransition.h
View File

@ -0,0 +1,36 @@
#ifndef STORM_STORAGE_GSPN_TIMEDTRANSITION_H_
#define STORM_STORAGE_GSPN_TIMEDTRANSITION_H_
#include "src/storage/gspn/Transition.h"
namespace storm {
namespace gspn {
template <typename RateType>
class TimedTransition : public storm::gspn::Transition {
public:
/*!
* Sets the rate of this transition to the given value.
*
* @param rate The new rate for this transition.
*/
void setRate(RateType const& rate) {
this->rate = rate;
}
/*!
* Retrieves the rate of this transition.
*
* @return The rate of this transition.
*/
RateType getRate() const {
return this->rate;
}
private:
// the rate of the transition
RateType rate;
};
}
}
#endif //STORM_STORAGE_GSPN_TIMEDTRANSITION_H_

195
src/storage/gspn/Transition.cpp
View File

@ -0,0 +1,195 @@
#include "src/storage/gspn/Transition.h"
#include "src/utility/macros.h"
namespace storm {
namespace gspn {
void Transition::setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) {
auto ptr = std::make_shared<storm::gspn::Place>(place);
inputMultiplicities[ptr] = multiplicity;
inputPlaces.push_back(ptr);
}
bool Transition::removeInputArc(storm::gspn::Place const& place) {
if (existsInputArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place);
inputMultiplicities.erase(ptr);
inputPlaces.erase(std::find(inputPlaces.begin(), inputPlaces.end(), ptr));
return true;
} else {
return false;
}
}
bool Transition::existsInputArc(storm::gspn::Place const& place) const {
auto ptr = std::make_shared<storm::gspn::Place>(place);
return inputMultiplicities.end() != inputMultiplicities.find(ptr);
}
void Transition::setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) {
auto ptr = std::make_shared<storm::gspn::Place>(place);
outputMultiplicities[ptr] = multiplicity;
outputPlaces.push_back(ptr);
}
bool Transition::removeOutputArc(storm::gspn::Place const& place) {
if (existsOutputArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place);
outputMultiplicities.erase(ptr);
outputPlaces.erase(std::find(outputPlaces.begin(), outputPlaces.end(), ptr));
return true;
} else {
return false;
}
}
bool Transition::existsOutputArc(storm::gspn::Place const& place) const {
auto ptr = std::make_shared<storm::gspn::Place>(place);
return outputMultiplicities.end() != outputMultiplicities.find(ptr);
}
void Transition::setInhibitionArcMultiplicity(storm::gspn::Place const& place,
uint_fast64_t multiplicity) {
auto ptr = std::make_shared<storm::gspn::Place>(place);
inhibitionMultiplicities[ptr] = multiplicity;
inhibitionPlaces.push_back(ptr);
}
bool Transition::removeInhibitionArc(storm::gspn::Place const& place) {
if (existsInhibitionArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place);
inhibitionMultiplicities.erase(ptr);
inhibitionPlaces.erase(std::find(inhibitionPlaces.begin(), inhibitionPlaces.end(), ptr));
return true;
} else {
return false;
}
}
bool Transition::existsInhibitionArc(storm::gspn::Place const& place) const {
auto ptr = std::make_shared<storm::gspn::Place>(place);
return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(ptr);
}
bool Transition::isEnabled(storm::gspn::Marking const& marking) const {
auto inputIterator = inputMultiplicities.cbegin();
while (inputIterator != inputMultiplicities.cend()) {
if (marking.getNumberOfTokensAt(inputIterator->first->getID()) < inputIterator->second) {
return false;
}
++inputIterator;
}
auto inhibitionIterator = inhibitionMultiplicities.cbegin();
while (inhibitionIterator != inhibitionMultiplicities.cend()) {
if (marking.getNumberOfTokensAt(inhibitionIterator->first->getID()) >= inhibitionIterator->second) {
return false;
}
++inhibitionIterator;
}
auto outputIterator = outputMultiplicities.cbegin();
while (outputIterator != outputMultiplicities.cend()) {
if (outputIterator->first->getCapacity() >= 0) {
if (marking.getNumberOfTokensAt(outputIterator->first->getID()) + outputIterator->second > outputIterator->first->getCapacity()) {
return false;
}
}
++outputIterator;
}
return true;
}
storm::gspn::Marking Transition::fire(storm::gspn::Marking const& marking) const {
storm::gspn::Marking newMarking(marking);
auto inputIterator = inputMultiplicities.cbegin();
while (inputIterator != inputMultiplicities.cend()) {
newMarking.setNumberOfTokensAt(inputIterator->first->getID(),
newMarking.getNumberOfTokensAt(inputIterator->first->getID()) - inputIterator->second);
++inputIterator;
}
auto outputIterator = outputMultiplicities.cbegin();
while (outputIterator != outputMultiplicities.cend()) {
newMarking.setNumberOfTokensAt(outputIterator->first->getID(),
newMarking.getNumberOfTokensAt(outputIterator->first->getID()) + outputIterator->second);
++outputIterator;
}
return newMarking;
}
void Transition::setName(std::string const& name) {
this->name = name;
}
std::string const& Transition::getName() const {
return this->name;
}
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInputPlacesCBegin() const {
return this->inputPlaces.cbegin();
}
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInputPlacesCEnd() const {
return this->inputPlaces.cend();
}
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getOutputPlacesCBegin() const {
return this->outputPlaces.cbegin();
}
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getOutputPlacesCEnd() const {
return this->outputPlaces.cend();
}
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInhibitionPlacesCBegin() const {
return this->inhibitionPlaces.cbegin();
}
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInhibitionPlacesCEnd() const {
return this->inhibitionPlaces.cend();
}
uint_fast64_t Transition::getInputArcMultiplicity(storm::gspn::Place const& place) const {
if (existsInputArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place);
return inputMultiplicities.at(ptr);
} else {
return 0;
}
}
uint_fast64_t Transition::getInhibitionArcMultiplicity(storm::gspn::Place const& place) const {
if (existsInhibitionArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place);
return inhibitionMultiplicities.at(ptr);
} else {
return 0;
}
}
uint_fast64_t Transition::getOutputArcMultiplicity(storm::gspn::Place const& place) const {
if (existsOutputArc(place)) {
auto ptr = std::make_shared<storm::gspn::Place>(place);
return outputMultiplicities.at(ptr);
} else {
return 0;
}
}
void Transition::setPriority(uint_fast64_t const& priority) {
this->priority = priority;
}
uint_fast64_t Transition::getPriority() const {
return this->priority;
}
}
}

240
src/storage/gspn/Transition.h
View File

@ -0,0 +1,240 @@
#ifndef STORM_STORAGE_GSPN_TRANSITION_H_
#define STORM_STORAGE_GSPN_TRANSITION_H_
#include <map>
#include <vector>
#include "src/storage/gspn/Marking.h"
#include "src/storage/gspn/Place.h"
namespace storm {
namespace gspn {
/*!
* This class represents a transition in a gspn.
*/
class Transition {
public:
/*!
* Set the multiplicity of the input arc originating from the place.
* If the arc already exists, the former multiplicity is overwritten.
* If the arc does not yet exists, it is created.
*
* @param place The place connected by an input arc.
* @param multiplicity The multiplicity of the specified arc.
*/
void setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity);
/*!
* Removes an input arc connected to a given place.
*
* @param place The place from which the input arc is originating.
* @return True if the arc existed.
*/
bool removeInputArc(storm::gspn::Place const& place);
/*!
* Checks whether the given place is connected to this transition via an input arc.
*
* @param place The place which is going to be checked.
* @return True if the place is connected via an input arc.
*/
bool existsInputArc(storm::gspn::Place const& place) const;
/*!
* Set the multiplicity of the output arc going to the place.
* If the arc already exists, the former multiplicity is overwritten.
* If the arc does not yet exists, it is created.
*
* @param place The place connected by an output arc.
* @param multiplicity The multiplicity of the specified arc.
*/
void setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity);
/*!
* Removes an output arc connected to a given place.
*
* @param place The place from which the output arc is leading to.
* @return True if the arc existed.
*/
bool removeOutputArc(storm::gspn::Place const& place);
/*!
* Checks whether the given place is connected to this transition via an output arc.
*
* @param place The place which is going to be checked.
* @return True if the place is connected via an output arc.
*/
bool existsOutputArc(storm::gspn::Place const& place) const;
/*!
* Set the multiplicity of the inhibition arc originating from the place.
* If the arc already exists, the former multiplicity is overwritten.
* If the arc does not yet exists, it is created.
*
* @param place The place connected by an inhibition arc.
* @param multiplicity The multiplicity of the specified arc.
*/
void setInhibitionArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity);
/*!
* Removes an inhibition arc connected to a given place.
*
* @param place The place from which the inhibition arc is originating.
* @return True if the arc existed.
*/
bool removeInhibitionArc(storm::gspn::Place const& place);
/*!
* Checks whether the given place is connected to this transition via an inhibition arc.
*
* @param place The place which is going to be checked.
* @return True if the place is connected via an inhibition arc.
*/
bool existsInhibitionArc(storm::gspn::Place const& place) const;
/*!
* Checks if the given marking enables the transition.
*
* @return True if the transition is enabled.
*/
bool isEnabled(storm::gspn::Marking const& marking) const;
/*!
* Fire the transition if possible.
*
* @param marking The current marking before the transition is fired.
* @return The marking after the transition was fired.
*/
storm::gspn::Marking fire(storm::gspn::Marking const& marking) const;
/*!
* Set the name of the transition.
*
* @param name New name of the transition.
*/
void setName(std::string const& name);
/*!
* Returns the name of the transition.
*
* @return The name of the transition.
*/
std::string const& getName() const;
/*!
* Returns a constant iterator to the begin of a vector which contains all input places.
*
* @return Returns iterator.
*/
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getInputPlacesCBegin() const;
/*!
* Returns a constant iterator to the end of a vector which contains all input places.
*
* @return Returns iterator.
*/
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getInputPlacesCEnd() const;
/*!
* Returns a constant iterator to the begin of a vector which contains all output places.
*
* @return Returns iterator.
*/
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getOutputPlacesCBegin() const;
/*!
* Returns a constant iterator to the end of a vector which contains all output places.
*
* @return Returns iterator.
*/
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getOutputPlacesCEnd() const;
/*!
* Returns a constant iterator to the begin of a vector which contains all inhibition places.
*
* @return Returns iterator.
*/
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getInhibitionPlacesCBegin() const;
/*!
* Returns a constant iterator to the end of a vector which contains all inhibition places.
*
* @return Returns iterator.
*/
std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getInhibitionPlacesCEnd() const;
/*!
* Returns the corresponding multiplicity.
*
* @param place connected to this transition by an input arc
* @return cardinality or 0 if the arc does not exists
*/
uint_fast64_t getInputArcMultiplicity(storm::gspn::Place const& place) const;
/*!
* Returns the corresponding multiplicity.
*
* @param place connected to this transition by an inhibition arc
* @return cardinality or 0 if the arc does not exists
*/
uint_fast64_t getInhibitionArcMultiplicity(storm::gspn::Place const& place) const;
/*!
* Returns the corresponding multiplicity.
*
* @param place connected to this transition by an output arc
* @return cardinality or 0 if the arc does not exists
*/
uint_fast64_t getOutputArcMultiplicity(storm::gspn::Place const& place) const;
/*!
* Sets the priority of this transtion.
*
* @param priority The new priority.
*/
void setPriority(uint_fast64_t const& priority);
/*!
* Returns the priority of this transition.
*
* @return The priority.
*/
uint_fast64_t getPriority() const;
private:
/*!
* Comparator which defines an total order on places.
* A place is less than another place if the id is less than the id from the other place.
*/
struct PlaceComparator {
bool operator()(std::shared_ptr<storm::gspn::Place> const& lhs, std::shared_ptr<storm::gspn::Place> const& rhs) const {
return lhs->getID() < rhs->getID();
}
};
// maps places connected to this transition with an input arc to the corresponding multiplicity
std::map<std::shared_ptr<storm::gspn::Place>, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inputMultiplicities;
// maps places connected to this transition with an output arc to the corresponding multiplicities
std::map<std::shared_ptr<storm::gspn::Place>, uint_fast64_t, storm::gspn::Transition::PlaceComparator> outputMultiplicities;
// maps places connected to this transition with an inhibition arc to the corresponding multiplicity
std::map<std::shared_ptr<storm::gspn::Place>, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inhibitionMultiplicities;
// name of the transition
std::string name;
// list of all places connected to this transition via an input arc
std::vector<std::shared_ptr<storm::gspn::Place>> inputPlaces;
// list of all places connected to this transition via an output arc
std::vector<std::shared_ptr<storm::gspn::Place>> outputPlaces;
// list of all places connected to this transition via an inhibition arc
std::vector<std::shared_ptr<storm::gspn::Place>> inhibitionPlaces;
// priority of this transition
uint_fast64_t priority;
};
}
}
#endif //STORM_STORAGE_GSPN_TRANSITION_H_

153
src/storm-gspn.cpp
View File

@ -0,0 +1,153 @@
#include "src/builder/ExplicitGspnModelBuilder.h"
#include "src/exceptions/BaseException.h"
#include "src/parser/GspnParser.h"
#include "src/storage/gspn/GSPN.h"
#include "src/storage/gspn/GspnBuilder.h"
#include "src/utility/macros.h"
#include "src/utility/initialize.h"
#include <fstream>
#include <iostream>
#include <string>
// TODO clean-up includes after doing all other todos
/*!
* Parses the arguments to storm-gspn
* The read data is stored in the different arguments (e.g., inputFile, formula, ...)
*
* @param argc number of arguments passed to storm-gspn
* @param argv array of arguments
* @param inputFile the input file is stored in this object
* @param formula the formula is stored in this object
* @param outputFile the output file is stored in this object
* @param outputType the output type is stored in this object
* @return false if the help flag is set or the input file is missing
*/
bool parseArguments(const int argc, const char **argv, std::string &inputFile, std::string &formula,
std::string &outputFile, std::string &outputType) {
auto end = argv + argc;
bool result = false;
for (auto it = argv; it != end; ++it) {
std::string currentArg = *it;
// parse input file argument
if (currentArg == "--input_file" || currentArg == "-i") {
auto next = it + 1;
if (next != end) {
return -1;
} else {
inputFile = *next;
result = true;
}
break;
}
// parse formula argument
if (currentArg == "--formula" || currentArg == "-f") {
auto next = it + 1;
if (next != end) {
return -1;
} else {
formula = *next;
}
break;
}
// parse output file argument
if (currentArg == "--output_file" || currentArg == "-o") {
auto next = it + 1;
if (next != end) {
return -1;
} else {
outputFile = *next;
}
break;
}
// parse output file type argument
if (currentArg == "--output_type" || currentArg == "-ot") {
auto next = it + 1;
if (next != end) {
return -1;
} else {
outputType = *next;
}
break;
}
// parse help argument
if (currentArg == "--help" || currentArg == "-h") {
return false;
}
}
return result;
}
/*!
* Print the manual of storm-gspn
*/
void printHelp() {
std::cout << "storm-gspn -i input_file [-f formula] [-o output_file] [-ot output_type] [-h]" << std::endl;
std::cout << std::endl;
std::cout << "-i, --input_file: file which contains the gspn" << std::endl;
std::cout << "-f, --formula: formula which should be checked on the gspn" << std::endl;
std::cout << "-o, -output_file: file in which the gspn/markov automaton should be stored" << std::endl
<< " requires the option -ot to be set" << std::endl;
std::cout << "-ot, --output_type: possible output types are: pnml, pnpro or ma" << std::endl;
}
int main(const int argc, const char **argv) {
std::string inputFile, formula, outputFile, outputType;
if (!parseArguments(argc, argv, inputFile, formula, outputFile, outputType)) {
printHelp();
return 1;
}
try {
storm::utility::setUp();
// parse GSPN from file
auto parser = storm::parser::GspnParser();
auto gspn = parser.parse(inputFile);
// todo ------[marker]
gspn.isValid();
storm::gspn::GspnBuilder builder2;
builder2.addPlace(2);
//
//std::ofstream file;
//file.open("/Users/thomas/Desktop/storm.dot");
//gspn.writeDotToStream(file);
//file.close();
std::ofstream file;
file.open("/Users/thomas/Desktop/gspn.pnpro");
gspn.toPnpro(file);
file.close();
std::cout << "Parsing complete!" << std::endl;
// Construct MA
auto builder = storm::builder::ExplicitGspnModelBuilder<>();
auto ma = builder.translateGspn(gspn, argv[2]);
std::cout << "Markov Automaton: " << std::endl;
std::cout << "number of states: " << ma.getNumberOfStates() << std::endl;
std::cout << "number of transitions: " << ma.getNumberOfTransitions() << std::endl << std::endl;
// All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp();
return 0;
} catch (storm::exceptions::BaseException const& exception) {
STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is: " << exception.what());
} catch (std::exception const& exception) {
STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM to terminate. The message of this exception is: " << exception.what());
}
}

55
src/utility/constants.cpp
View File

@ -14,27 +14,27 @@ namespace storm {
ValueType one() { ValueType one() {
return ValueType(1); return ValueType(1);
} }
template<typename ValueType> template<typename ValueType>
ValueType zero() { ValueType zero() {
return ValueType(0); return ValueType(0);
} }
template<typename ValueType> template<typename ValueType>
ValueType infinity() { ValueType infinity() {
return std::numeric_limits<ValueType>::infinity(); return std::numeric_limits<ValueType>::infinity();
} }
template<typename ValueType> template<typename ValueType>
bool isOne(ValueType const& a) { bool isOne(ValueType const& a) {
return a == one<ValueType>(); return a == one<ValueType>();
} }
template<typename ValueType> template<typename ValueType>
bool isZero(ValueType const& a) { bool isZero(ValueType const& a) {
return a == zero<ValueType>(); return a == zero<ValueType>();
} }
template<typename ValueType> template<typename ValueType>
bool isConstant(ValueType const& a) { bool isConstant(ValueType const& a) {
return true; return true;
@ -62,42 +62,41 @@ namespace storm {
bool isOne(storm::RationalNumber const& a) { bool isOne(storm::RationalNumber const& a) {
return carl::isOne(a); return carl::isOne(a);
} }
template<> template<>
bool isZero(storm::RationalNumber const& a) { bool isZero(storm::RationalNumber const& a) {
return carl::isZero(a); return carl::isZero(a);
} }
template<> template<>
bool isOne(storm::RationalFunction const& a) { bool isOne(storm::RationalFunction const& a) {
return a.isOne(); return a.isOne();
} }
template<> template<>
bool isZero(storm::RationalFunction const& a) { bool isZero(storm::RationalFunction const& a) {
return a.isZero(); return a.isZero();
} }
template<> template<>
bool isConstant(storm::RationalFunction const& a) { bool isConstant(storm::RationalFunction const& a) {
return a.isConstant(); return a.isConstant();
} }
template<> template<>
bool isOne(storm::Polynomial const& a) { bool isOne(storm::Polynomial const& a) {
return a.isOne(); return a.isOne();
} }
template<> template<>
bool isZero(storm::Polynomial const& a) { bool isZero(storm::Polynomial const& a) {
return a.isZero(); return a.isZero();
} }
template<> template<>
bool isConstant(storm::Polynomial const& a) { bool isConstant(storm::Polynomial const& a) {
return a.isConstant(); return a.isConstant();
} }
template<> template<>
storm::RationalFunction infinity() { storm::RationalFunction infinity() {
// FIXME: this should be treated more properly. // FIXME: this should be treated more properly.
@ -137,7 +136,7 @@ namespace storm {
double convertNumber(double const& number){ double convertNumber(double const& number){
return number; return number;
} }
template<typename ValueType> template<typename ValueType>
ValueType abs(ValueType const& number) { ValueType abs(ValueType const& number) {
return std::fabs(number); return std::fabs(number);
@ -146,7 +145,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template<> template<>
RationalFunction& simplify(RationalFunction& value); RationalFunction& simplify(RationalFunction& value);
template<> template<>
RationalFunction&& simplify(RationalFunction&& value); RationalFunction&& simplify(RationalFunction&& value);
@ -172,7 +171,7 @@ namespace storm {
value.simplify(); value.simplify();
return std::move(value); return std::move(value);
} }
template<> template<>
double convertNumber(RationalNumber const& number){ double convertNumber(RationalNumber const& number){
return carl::toDouble(number); return carl::toDouble(number);
@ -261,6 +260,7 @@ namespace storm {
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
template double abs(double const& number); template double abs(double const& number);
template bool isInteger(double const& number); template bool isInteger(double const& number);
template bool isOne(float const& value); template bool isOne(float const& value);
@ -283,16 +283,17 @@ namespace storm {
template bool isOne(int const& value); template bool isOne(int const& value);
template bool isZero(int const& value); template bool isZero(int const& value);
template bool isConstant(int const& value); template bool isConstant(int const& value);
template int one(); template int one();
template int zero(); template int zero();
template int infinity(); template int infinity();
template int pow(int const& value, uint_fast64_t exponent); template int pow(int const& value, uint_fast64_t exponent);
template bool isInteger(int const& number); template bool isInteger(int const& number);
template int simplify(int value); template int simplify(int value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
@ -304,7 +305,7 @@ namespace storm {
template uint32_t one(); template uint32_t one();
template uint32_t zero(); template uint32_t zero();
template uint32_t infinity(); template uint32_t infinity();
template storm::storage::sparse::state_type one(); template storm::storage::sparse::state_type one();
template storm::storage::sparse::state_type zero(); template storm::storage::sparse::state_type zero();
template storm::storage::sparse::state_type infinity(); template storm::storage::sparse::state_type infinity();
@ -336,7 +337,7 @@ namespace storm {
template storm::RationalNumber abs(storm::RationalNumber const& number); template storm::RationalNumber abs(storm::RationalNumber const& number);
template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent); template storm::RationalNumber pow(storm::RationalNumber const& value, uint_fast64_t exponent);
template storm::RationalNumber simplify(storm::RationalNumber value); template storm::RationalNumber simplify(storm::RationalNumber value);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry);
@ -346,26 +347,26 @@ namespace storm {
template bool isOne(RationalFunction const& value); template bool isOne(RationalFunction const& value);
template bool isZero(RationalFunction const& value); template bool isZero(RationalFunction const& value);
template bool isConstant(RationalFunction const& value); template bool isConstant(RationalFunction const& value);
template RationalFunction one(); template RationalFunction one();
template RationalFunction zero(); template RationalFunction zero();
template storm::RationalFunction infinity(); template storm::RationalFunction infinity();
template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
template RationalFunction simplify(RationalFunction value); template RationalFunction simplify(RationalFunction value);
template RationalFunction& simplify(RationalFunction& value); template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value); template RationalFunction&& simplify(RationalFunction&& value);
template Polynomial one(); template Polynomial one();
template Polynomial zero(); template Polynomial zero();
template bool isOne(Interval const& value); template bool isOne(Interval const& value);
template bool isZero(Interval const& value); template bool isZero(Interval const& value);
template bool isConstant(Interval const& value); template bool isConstant(Interval const& value);
template Interval one(); template Interval one();
template Interval zero(); template Interval zero();
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);

26
src/utility/constants.h
View File

@ -13,47 +13,47 @@
#include <cstdint> #include <cstdint>
namespace storm { namespace storm {
// Forward-declare MatrixEntry class. // Forward-declare MatrixEntry class.
namespace storage { namespace storage {
template<typename IndexType, typename ValueType> class MatrixEntry; template<typename IndexType, typename ValueType> class MatrixEntry;
} }
namespace utility { namespace utility {
template<typename ValueType> template<typename ValueType>
ValueType one(); ValueType one();
template<typename ValueType> template<typename ValueType>
ValueType zero(); ValueType zero();
template<typename ValueType> template<typename ValueType>
ValueType infinity(); ValueType infinity();
template<typename ValueType> template<typename ValueType>
bool isOne(ValueType const& a); bool isOne(ValueType const& a);
template<typename ValueType> template<typename ValueType>
bool isZero(ValueType const& a); bool isZero(ValueType const& a);
template<typename ValueType> template<typename ValueType>
bool isConstant(ValueType const& a); bool isConstant(ValueType const& a);
template<typename ValueType> template<typename ValueType>
ValueType pow(ValueType const& value, uint_fast64_t exponent); ValueType pow(ValueType const& value, uint_fast64_t exponent);
template<typename ValueType> template<typename ValueType>
ValueType simplify(ValueType value); ValueType simplify(ValueType value);
template<typename IndexType, typename ValueType> template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry); storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
template<typename IndexType, typename ValueType> template<typename IndexType, typename ValueType>
storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry); storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
template<typename TargetType, typename SourceType> template<typename TargetType, typename SourceType>
TargetType convertNumber(SourceType const& number); TargetType convertNumber(SourceType const& number);
template<typename ValueType> template<typename ValueType>
ValueType abs(ValueType const& number); ValueType abs(ValueType const& number);

1
src/utility/storm.cpp
View File

@ -12,6 +12,7 @@ namespace storm {
storm::prism::Program parseProgram(std::string const& path) { storm::prism::Program parseProgram(std::string const& path) {
storm::prism::Program program = storm::parser::PrismParser::parse(path).simplify().simplify(); storm::prism::Program program = storm::parser::PrismParser::parse(path).simplify().simplify();
program.checkValidity(); program.checkValidity();
std::cout << program << std::endl;
return program; return program;
} }

2
src/utility/storm.h
View File

@ -271,7 +271,7 @@ namespace storm {
case storm::settings::modules::CoreSettings::Engine::Sparse: { case storm::settings::modules::CoreSettings::Engine::Sparse: {
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>(); std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model"); STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model");
return verifySparseModel(sparseModel, formula, onlyInitialStatesRelevant);
return (sparseModel, formula, onlyInitialStatesRelevant);
} }
case storm::settings::modules::CoreSettings::Engine::Hybrid: { case storm::settings::modules::CoreSettings::Engine::Hybrid: {
std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>(); std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>();

13
src/utility/vector.h
View File

@ -12,7 +12,6 @@
#include <functional> #include <functional>
#include "src/storage/BitVector.h" #include "src/storage/BitVector.h"
#include "src/utility/constants.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/solver/OptimizationDirection.h" #include "src/solver/OptimizationDirection.h"
@ -623,16 +622,18 @@ namespace storm {
* @return True iff the elements are considered equal. * @return True iff the elements are considered equal.
*/ */
template<class T> template<class T>
bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) {
bool equalModuloPrecision(T const& val1, T const& val2, T const& precision, bool relativeError = true) {
if (relativeError) { if (relativeError) {
if (val2 == 0) { if (val2 == 0) {
return (storm::utility::abs(val1) <= precision); return (storm::utility::abs(val1) <= precision);
} }
if (storm::utility::abs((val1 - val2)/val2) > precision) {
T relDiff = (val1 - val2)/val2;
if (storm::utility::abs(relDiff) > precision) {
return false; return false;
} }
} else { } else {
if (storm::utility::abs(val1 - val2) > precision) return false;
T diff = val1 - val2;
if (storm::utility::abs(diff) > precision) return false;
} }
return true; return true;
} }
@ -647,7 +648,7 @@ namespace storm {
* @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms.
*/ */
template<class T> template<class T>
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, T precision, bool relativeError) {
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, T const& precision, bool relativeError) {
STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match."); STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) { for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) {
@ -671,7 +672,7 @@ namespace storm {
* @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms. * @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms.
*/ */
template<class T> template<class T>
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, std::vector<uint_fast64_t> const& positions, T precision, bool relativeError) {
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, std::vector<uint_fast64_t> const& positions, T const& precision, bool relativeError) {
STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match."); STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
for (uint_fast64_t position : positions) { for (uint_fast64_t position : positions) {

2
storm-config.h.in
View File

@ -44,6 +44,8 @@
// Whether carl is available and to be used. // Whether carl is available and to be used.
#cmakedefine STORM_HAVE_CARL #cmakedefine STORM_HAVE_CARL
#cmakedefine STORM_USE_CLN_NUMBERS
// Whether smtrat is available and to be used. // Whether smtrat is available and to be used.
#cmakedefine STORM_HAVE_SMTRAT #cmakedefine STORM_HAVE_SMTRAT

Write Preview
Loading…
Cancel
Save