diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 7cf58f2f1..fdf2594fc 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -96,21 +96,16 @@ int main(const int argc, const char **argv) { auto capacities = parseCapacitiesList(storm::settings::getModule().getCapacitiesFilename()); gspn->setCapacities(capacities); } - - - if(storm::settings::getModule().isWriteToDotSet()) { - std::ofstream file; - file.open(storm::settings::getModule().getWriteToDotFilename()); - gspn->writeDotToStream(file); - } + + storm::handleGSPNExportSettings(*gspn); if(storm::settings::getModule().isJaniFileSet()) { storm::jani::Model* model = storm::buildJani(*gspn); storm::exportJaniModel(*model, {}, storm::settings::getModule().getJaniFilename()); delete model; } - - + + delete gspn; return 0; // diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index 061e9bd67..386d2b0a2 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -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 oas; + std::vector probabilities; + std::vector 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 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 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 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 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); + + } + } + } +} \ No newline at end of file diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h index 92a7062b6..791989009 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.h +++ b/src/storm-gspn/builder/JaniGSPNBuilder.h @@ -8,165 +8,32 @@ namespace storm { namespace builder { class JaniGSPNBuilder { public: - JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr const& expManager) : gspn(gspn), expressionManager(expManager) { + JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr 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 oas; - std::vector probabilities; - std::vector 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 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 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 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 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 vars;