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

GSPN to Jani compiles again with updates from gspn branch 

Former-commit-id: f1a1988fe3 [formerly 5003212d39]
Former-commit-id: 71b67f7fc5
tempestpy_adaptions
sjunges 8 years ago
parent
8108c81e63
commit
4f7935342d
2 changed files with 31 additions and 31 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. 56
      src/builder/JaniGSPNBuilder.h
  2. 6
      src/storage/gspn/Transition.h

56
src/builder/JaniGSPNBuilder.h
View File

@ -62,19 +62,19 @@ namespace storm {
for (auto const& trans : gspn.getImmediateTransitions()) {
if (ignoreWeights || trans->noWeightAttached()) {
std::vector<storm::jani::Assignment> assignments;
for (auto inPlaceIt = trans->getInputPlacesCBegin(); inPlaceIt != trans->getInputPlacesCEnd(); ++inPlaceIt) {
guard = guard && (vars[(**inPlaceIt).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(**inPlaceIt));
assignments.emplace_back( *vars[(**inPlaceIt).getID()], (vars[(**inPlaceIt).getID()]->getExpressionVariable() - trans->getInputArcMultiplicity(**inPlaceIt)) );
for (auto const& inPlace : trans->getInputPlaces()) {
guard = guard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(*inPlace));
assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans->getInputArcMultiplicity(*inPlace)) );
}
for (auto inhibPlaceIt = trans->getInhibitionPlacesCBegin(); inhibPlaceIt != trans->getInhibitionPlacesCEnd(); ++inhibPlaceIt) {
guard = guard && (vars[(**inhibPlaceIt).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(**inhibPlaceIt));
for (auto const& inhibPlace : trans->getInhibitionPlaces()) {
guard = guard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(*inhibPlace));
}
for (auto outputPlaceIt = trans->getOutputPlacesCBegin(); outputPlaceIt != trans->getOutputPlacesCEnd(); ++outputPlaceIt) {
assignments.emplace_back( *vars[(**outputPlaceIt).getID()], (vars[(**outputPlaceIt).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(**outputPlaceIt)) );
for (auto const& outputPlace : trans->getOutputPlaces()) {
assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(*outputPlace)) );
}
storm::jani::OrderedAssignments oa(assignments);
storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa);
storm::jani::Edge e(locId, storm::jani::Model::silentActionIndex, boost::none, guard, {dest});
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, guard, {dest});
automaton.addEdge(e);
}
@ -92,11 +92,11 @@ namespace storm {
continue;
}
storm::expressions::Expression destguard = expressionManager->boolean(true);
for (auto inPlaceIt = trans->getInputPlacesCBegin(); inPlaceIt != trans->getInputPlacesCEnd(); ++inPlaceIt) {
destguard = destguard && (vars[(**inPlaceIt).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(**inPlaceIt));
for (auto const& inPlace : trans->getInputPlaces()) {
destguard = destguard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(*inPlace));
}
for (auto inhibPlaceIt = trans->getInhibitionPlacesCBegin(); inhibPlaceIt != trans->getInhibitionPlacesCEnd(); ++inhibPlaceIt) {
destguard = destguard && (vars[(**inhibPlaceIt).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(**inhibPlaceIt));
for (auto const& inhibPlace : trans->getInhibitionPlaces()) {
destguard = destguard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(*inhibPlace));
}
totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans->getWeight()), expressionManager->rational(0.0));
@ -109,15 +109,15 @@ namespace storm {
}
storm::expressions::Expression destguard = expressionManager->boolean(true);
std::vector<storm::jani::Assignment> assignments;
for (auto inPlaceIt = trans->getInputPlacesCBegin(); inPlaceIt != trans->getInputPlacesCEnd(); ++inPlaceIt) {
destguard = destguard && (vars[(**inPlaceIt).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(**inPlaceIt));
assignments.emplace_back( *vars[(**inPlaceIt).getID()], (vars[(**inPlaceIt).getID()]->getExpressionVariable() - trans->getInputArcMultiplicity(**inPlaceIt)) );
for (auto const& inPlace : trans->getInputPlaces()) {
destguard = destguard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(*inPlace));
assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans->getInputArcMultiplicity(*inPlace)) );
}
for (auto inhibPlaceIt = trans->getInhibitionPlacesCBegin(); inhibPlaceIt != trans->getInhibitionPlacesCEnd(); ++inhibPlaceIt) {
destguard = destguard && (vars[(**inhibPlaceIt).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(**inhibPlaceIt));
for (auto const& inhibPlace : trans->getInhibitionPlaces()) {
destguard = destguard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(*inhibPlace));
}
for (auto outputPlaceIt = trans->getOutputPlacesCBegin(); outputPlaceIt != trans->getOutputPlacesCEnd(); ++outputPlaceIt) {
assignments.emplace_back( *vars[(**outputPlaceIt).getID()], (vars[(**outputPlaceIt).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(**outputPlaceIt)) );
for (auto const& outputPlace : trans->getOutputPlaces()) {
assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(*outputPlace)) );
}
destguard = destguard.simplify();
guard = guard || destguard;
@ -125,26 +125,26 @@ namespace storm {
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::silentActionIndex, boost::none, guard.simplify(), weightedDestinations);
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);
std::vector<storm::jani::Assignment> assignments;
for (auto inPlaceIt = trans->getInputPlacesCBegin(); inPlaceIt != trans->getInputPlacesCEnd(); ++inPlaceIt) {
guard = guard && (vars[(**inPlaceIt).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(**inPlaceIt));
assignments.emplace_back( *vars[(**inPlaceIt).getID()], (vars[(**inPlaceIt).getID()]->getExpressionVariable() - trans->getInputArcMultiplicity(**inPlaceIt)) );
for (auto const& inPlace : trans->getInputPlaces()) {
guard = guard && (vars[(*inPlace).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(*inPlace));
assignments.emplace_back( *vars[(*inPlace).getID()], (vars[(*inPlace).getID()]->getExpressionVariable() - trans->getInputArcMultiplicity(*inPlace)) );
}
for (auto inhibPlaceIt = trans->getInhibitionPlacesCBegin(); inhibPlaceIt != trans->getInhibitionPlacesCEnd(); ++inhibPlaceIt) {
guard = guard && (vars[(**inhibPlaceIt).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(**inhibPlaceIt));
for (auto const& inhibPlace : trans->getInhibitionPlaces()) {
guard = guard && (vars[(*inhibPlace).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(*inhibPlace));
}
for (auto outputPlaceIt = trans->getOutputPlacesCBegin(); outputPlaceIt != trans->getOutputPlacesCEnd(); ++outputPlaceIt) {
assignments.emplace_back( *vars[(**outputPlaceIt).getID()], (vars[(**outputPlaceIt).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(**outputPlaceIt)) );
for (auto const& outputPlace : trans->getOutputPlaces()) {
assignments.emplace_back( *vars[(*outputPlace).getID()], (vars[(*outputPlace).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(*outputPlace)) );
}
storm::jani::OrderedAssignments oa(assignments);
storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa);
storm::jani::Edge e(locId, storm::jani::Model::silentActionIndex, expressionManager->rational(trans->getRate()), guard, {dest});
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans->getRate()), guard, {dest});
automaton.addEdge(e);
}
}

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

@ -124,19 +124,19 @@ namespace storm {
* Returns a list of places which are connected via a input arc.
* @return
*/
const std::vector<std::shared_ptr<storm::gspn::Place>> &getInputPlaces() const;
std::vector<std::shared_ptr<storm::gspn::Place>> const& getInputPlaces() const;
/*!
* Returns a list of places which are connected via a output arc.
* @return
*/
const std::vector<std::shared_ptr<storm::gspn::Place>> &getOutputPlaces() const;
std::vector<std::shared_ptr<storm::gspn::Place>> const& getOutputPlaces() const;
/*!
* Returns a list of places which are connected via a inhibition arc.
* @return
*/
const std::vector<std::shared_ptr<storm::gspn::Place>> &getInhibitionPlaces() const;
std::vector<std::shared_ptr<storm::gspn::Place>> const& getInhibitionPlaces() const;
/*!
* Returns the corresponding multiplicity.
Write Preview
Loading…
Cancel
Save