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

initial support for partitions in translation from gspn to jani

main
Sebastian Junges 9 years ago
parent
a8b6e6e188
commit
f8986fe613
4 changed files with 72 additions and 41 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 101
      src/storm-gspn/builder/JaniGSPNBuilder.h
  2. 4
      src/storm-gspn/storage/gspn/GSPN.cpp
  3. 7
      src/storm-gspn/storage/gspn/GSPN.h
  4. 1
      src/storm-gspn/storage/gspn/GspnBuilder.cpp

101
src/storm-gspn/builder/JaniGSPNBuilder.h
View File

@ -81,53 +81,74 @@ namespace storm {
}
if(!ignoreWeights) {
uint64_t lastPriority;
storm::expressions::Expression lastPriorityGuard = expressionManager->boolean(false);
storm::expressions::Expression priorityGuard = expressionManager->boolean(true);
// TODO here there is something to fix if we add transition partitions.
storm::expressions::Expression guard = expressionManager->boolean(false);
std::vector<storm::jani::EdgeDestination> weightedDestinations;
// Compute enabled weight expression.
storm::expressions::Expression totalWeight = expressionManager->rational(0.0);
for (auto const& trans : gspn.getImmediateTransitions()) {
if (trans.noWeightAttached()) {
continue;
}
storm::expressions::Expression destguard = expressionManager->boolean(true);
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
}
totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0));
for (auto const& partition : gspn.getPartitions()) {
storm::expressions::Expression guard = expressionManager->boolean(false);
std::vector<storm::jani::EdgeDestination> weightedDestinations;
}
totalWeight = totalWeight.simplify();
for (auto const& trans : gspn.getImmediateTransitions()) {
if (trans.noWeightAttached()) {
continue;
}
storm::expressions::Expression destguard = expressionManager->boolean(true);
std::vector<storm::jani::Assignment> assignments;
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) );
assert(lastPriority <= partition.priority);
if (lastPriority < partition.priority) {
priorityGuard = priorityGuard && !lastPriorityGuard;
lastPriority = partition.priority;
} else {
assert(lastPriority == partition.priority);
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
// Compute enabled weight expression.
storm::expressions::Expression totalWeight = expressionManager->rational(0.0);
for (auto const& transId : partition.transitions) {
auto const& trans = gspn.getImmediateTransitions()[transId];
if (trans.noWeightAttached()) {
continue;
}
storm::expressions::Expression destguard = expressionManager->boolean(true);
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
}
totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0));
}
for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) );
totalWeight = totalWeight.simplify();
for (auto const& transId : partition.transitions) {
auto const& trans = gspn.getImmediateTransitions()[transId];
if (trans.noWeightAttached()) {
continue;
}
storm::expressions::Expression destguard = expressionManager->boolean(true);
std::vector<storm::jani::Assignment> assignments;
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) );
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
}
for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) );
}
destguard = destguard.simplify();
guard = guard || destguard;
storm::jani::OrderedAssignments oa(assignments);
storm::jani::EdgeDestination dest(locId, storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)), oa);
weightedDestinations.push_back(dest);
}
destguard = destguard.simplify();
guard = guard || destguard;
storm::jani::OrderedAssignments oa(assignments);
storm::jani::EdgeDestination dest(locId, storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)), oa);
weightedDestinations.push_back(dest);
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, (priorityGuard && guard).simplify(), weightedDestinations);
automaton.addEdge(e);
lastPriorityGuard = lastPriorityGuard || guard;
}
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, guard.simplify(), weightedDestinations);
automaton.addEdge(e);
}
for (auto const& trans : gspn.getTimedTransitions()) {
storm::expressions::Expression guard = expressionManager->boolean(true);

4
src/storm-gspn/storage/gspn/GSPN.cpp
View File

@ -57,6 +57,10 @@ namespace storm {
return m;
}
std::vector<TransitionPartition> const& GSPN::getPartitions() const {
return partitions;
}
storm::gspn::Place const* GSPN::getPlace(uint64_t id) const {
if(id < places.size()) {

7
src/storm-gspn/storage/gspn/GSPN.h
View File

@ -38,6 +38,11 @@ namespace storm {
*/
uint64_t getNumberOfPlaces() const;
/*!
*
*/
std::vector<TransitionPartition> const& getPartitions() const;
/*!
* Returns the vector of timed transitions in this gspn.
*
@ -65,7 +70,6 @@ namespace storm {
*/
std::shared_ptr<storm::gspn::Marking> getInitialMarking(std::map<uint64_t, uint64_t>& numberOfBits, uint64_t const& numberOfTotalBits) const;
/*!
* Returns the place with the corresponding id.
*
@ -86,6 +90,7 @@ namespace storm {
* Returns the timed transition with the corresponding name.
*
* @param name The ID of the timed transition.
* @return A pointer to the transition, and nullptr otherwise
*/
storm::gspn::TimedTransition<GSPN::RateType> const* getTimedTransition(std::string const& name) const;

1
src/storm-gspn/storage/gspn/GspnBuilder.cpp
View File

@ -162,6 +162,7 @@ namespace storm {
}
}
std::reverse(orderedPartitions.begin(), orderedPartitions.end());
return new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions);
}

Write Preview
Loading…
Cancel
Save