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

refactoring gspn code (moved stuff to cpp) and check all options via helper function now

tempestpy_adaptions
sjunges 8 years ago
parent
d84d202a0c
commit
5b811a916c
3 changed files with 166 additions and 155 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. 13
      src/storm-gspn-cli/storm-gspn.cpp
  2. 149
      src/storm-gspn/builder/JaniGSPNBuilder.cpp
  3. 159
      src/storm-gspn/builder/JaniGSPNBuilder.h

13
src/storm-gspn-cli/storm-gspn.cpp
View File

@ -96,21 +96,16 @@ int main(const int argc, const char **argv) {
auto capacities = parseCapacitiesList(storm::settings::getModule<storm::settings::modules::GSPNSettings>().getCapacitiesFilename());
gspn->setCapacities(capacities);
}
if(storm::settings::getModule<storm::settings::modules::GSPNExportSettings>().isWriteToDotSet()) {
std::ofstream file;
file.open(storm::settings::getModule<storm::settings::modules::GSPNExportSettings>().getWriteToDotFilename());
gspn->writeDotToStream(file);
}
storm::handleGSPNExportSettings(*gspn);
if(storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
storm::jani::Model* model = storm::buildJani(*gspn);
storm::exportJaniModel(*model, {}, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
delete model;
}
delete gspn;
return 0;
//

149
src/storm-gspn/builder/JaniGSPNBuilder.cpp
View File

@ -1 +1,150 @@
#include "JaniGSPNBuilder.h"
namespace storm {
namespace builder {
storm::jani::Model* JaniGSPNBuilder::build(std::string const& automatonName) {
storm::jani::Model* model = new storm::jani::Model(gspn.getName(), storm::jani::ModelType::MA, janiVersion, expressionManager);
storm::jani::Automaton mainAutomaton(automatonName, expressionManager->declareIntegerVariable("loc"));
addVariables(model);
uint64_t locId = addLocation(mainAutomaton);
addEdges(mainAutomaton, locId);
model->addAutomaton(mainAutomaton);
model->setStandardSystemComposition();
return model;
}
void JaniGSPNBuilder::addVariables(storm::jani::Model* model) {
for (auto const& place : gspn.getPlaces()) {
storm::jani::Variable* janiVar = nullptr;
if (!place.hasRestrictedCapacity()) {
// Effectively no capacity limit known
janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()));
} else {
assert(place.hasRestrictedCapacity());
janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity()));
}
assert(janiVar != nullptr);
assert(vars.count(place.getID()) == 0);
vars[place.getID()] = &model->addVariable(*janiVar);
delete janiVar;
}
}
uint64_t JaniGSPNBuilder::addLocation(storm::jani::Automaton& automaton) {
uint64_t janiLoc = automaton.addLocation(storm::jani::Location("loc"));
automaton.addInitialLocation("loc");
return janiLoc;
}
void JaniGSPNBuilder::addEdges(storm::jani::Automaton& automaton, uint64_t locId) {
uint64_t lastPriority = -1;
storm::expressions::Expression lastPriorityGuard = expressionManager->boolean(false);
storm::expressions::Expression priorityGuard = expressionManager->boolean(true);
for (auto const& partition : gspn.getPartitions()) {
storm::expressions::Expression guard = expressionManager->boolean(false);
assert(lastPriority >= partition.priority);
if (lastPriority > partition.priority) {
priorityGuard = priorityGuard && !lastPriorityGuard;
lastPriority = partition.priority;
} else {
assert(lastPriority == partition.priority);
}
// 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));
}
totalWeight = totalWeight.simplify();
std::vector<storm::jani::OrderedAssignments> oas;
std::vector<storm::expressions::Expression> probabilities;
std::vector<uint64_t> destinationLocations;
for (auto const& transId : partition.transitions) {
auto const& trans = gspn.getImmediateTransitions()[transId];
if (trans.noWeightAttached()) {
std::cout << "ERROR -- no weights attached at transition" << std::endl;
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);
if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
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()) {
if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
} else {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first));
}
}
destguard = destguard.simplify();
guard = guard || destguard;
oas.emplace_back(assignments);
destinationLocations.emplace_back(locId);
probabilities.emplace_back(storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)));
}
std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge((priorityGuard && guard).simplify());
for (auto const& oa : oas) {
templateEdge->addDestination(storm::jani::TemplateEdgeDestination(oa));
}
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, destinationLocations, probabilities);
automaton.addEdge(e);
lastPriorityGuard = lastPriorityGuard || guard;
}
for (auto const& trans : gspn.getTimedTransitions()) {
storm::expressions::Expression guard = expressionManager->boolean(true);
std::vector<storm::jani::Assignment> assignments;
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
}
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
}
for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
} else {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first));
}
}
std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(guard);
templateEdge->addDestination(assignments);
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans.getRate()), templateEdge, {locId}, {expressionManager->integer(1)});
automaton.addEdge(e);
}
}
}
}

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

@ -8,165 +8,32 @@ namespace storm {
namespace builder {
class JaniGSPNBuilder {
public:
JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr<storm::expressions::ExpressionManager> const& expManager) : gspn(gspn), expressionManager(expManager) {
JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr<storm::expressions::ExpressionManager> const& expManager)
: gspn(gspn), expressionManager(expManager) {
}
virtual ~JaniGSPNBuilder() {
// Intentionally left empty.
}
storm::jani::Model* build() {
storm::jani::Model* model = new storm::jani::Model(gspn.getName(), storm::jani::ModelType::MA, janiVersion, expressionManager);
storm::jani::Automaton mainAutomaton("immediate", expressionManager->declareIntegerVariable("loc"));
addVariables(model);
uint64_t locId = addLocation(mainAutomaton);
addEdges(mainAutomaton, locId);
model->addAutomaton(mainAutomaton);
model->setStandardSystemComposition();
return model;
}
storm::jani::Model* build(std::string const& automatonName = "gspn_automaton");
storm::jani::Variable const& getPlaceVariable(uint64_t placeId) {
return *vars.at(placeId);
}
void addVariables(storm::jani::Model* model) {
for (auto const& place : gspn.getPlaces()) {
storm::jani::Variable* janiVar = nullptr;
if (!place.hasRestrictedCapacity()) {
// Effectively no capacity limit known
janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()));
} else {
assert(place.hasRestrictedCapacity());
janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity()));
}
assert(janiVar != nullptr);
assert(vars.count(place.getID()) == 0);
vars[place.getID()] = &model->addVariable(*janiVar);
delete janiVar;
}
}
uint64_t addLocation(storm::jani::Automaton& automaton) {
uint64_t janiLoc = automaton.addLocation(storm::jani::Location("loc"));
automaton.addInitialLocation("loc");
return janiLoc;
}
void addEdges(storm::jani::Automaton& automaton, uint64_t locId) {
uint64_t lastPriority = -1;
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.
for (auto const& partition : gspn.getPartitions()) {
storm::expressions::Expression guard = expressionManager->boolean(false);
assert(lastPriority >= partition.priority);
if (lastPriority > partition.priority) {
priorityGuard = priorityGuard && !lastPriorityGuard;
lastPriority = partition.priority;
} else {
assert(lastPriority == partition.priority);
}
// 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));
}
totalWeight = totalWeight.simplify();
std::vector<storm::jani::OrderedAssignments> oas;
std::vector<storm::expressions::Expression> probabilities;
std::vector<uint64_t> destinationLocations;
for (auto const& transId : partition.transitions) {
auto const& trans = gspn.getImmediateTransitions()[transId];
if (trans.noWeightAttached()) {
std::cout << "ERROR -- no weights attached at transition" << std::endl;
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);
if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
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()) {
if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
} else {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first));
}
}
destguard = destguard.simplify();
guard = guard || destguard;
oas.emplace_back(assignments);
destinationLocations.emplace_back(locId);
probabilities.emplace_back(storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)));
}
std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge((priorityGuard && guard).simplify());
for (auto const& oa : oas) {
templateEdge->addDestination(storm::jani::TemplateEdgeDestination(oa));
}
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, destinationLocations, probabilities);
automaton.addEdge(e);
lastPriorityGuard = lastPriorityGuard || guard;
}
for (auto const& trans : gspn.getTimedTransitions()) {
storm::expressions::Expression guard = expressionManager->boolean(true);
std::vector<storm::jani::Assignment> assignments;
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
}
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
}
for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
} else {
assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first));
}
}
std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(guard);
templateEdge->addDestination(assignments);
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans.getRate()), templateEdge, {locId}, {expressionManager->integer(1)});
automaton.addEdge(e);
}
}
private:
void addVariables(storm::jani::Model* model);
uint64_t addLocation(storm::jani::Automaton& automaton);
void addEdges(storm::jani::Automaton& automaton, uint64_t locId);
const uint64_t janiVersion = 1;
storm::gspn::GSPN const& gspn;
std::map<uint64_t, storm::jani::Variable const*> vars;

Write Preview
Loading…
Cancel
Save