From 03ce4277b4a133fac15543048356a8fc3b93e156 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 22 Sep 2016 12:43:18 +0200 Subject: [PATCH] first version jani export for gspns Former-commit-id: a1bcd24cbe8ded94ccd5b5e0ec9425d55afacaae [formerly 99e3d151d4135ce8dd8d8736fe00d03f5dcef429] Former-commit-id: 31473ed214ed82b9d35d893daa28406db3d61edb --- src/builder/JaniGSPNBuilder.cpp | 1 + src/builder/JaniGSPNBuilder.h | 161 ++++++++++++++++++++++++++++++++ src/storm-gspn.cpp | 38 +++++--- 3 files changed, 188 insertions(+), 12 deletions(-) create mode 100644 src/builder/JaniGSPNBuilder.cpp create mode 100644 src/builder/JaniGSPNBuilder.h diff --git a/src/builder/JaniGSPNBuilder.cpp b/src/builder/JaniGSPNBuilder.cpp new file mode 100644 index 000000000..061e9bd67 --- /dev/null +++ b/src/builder/JaniGSPNBuilder.cpp @@ -0,0 +1 @@ +#include "JaniGSPNBuilder.h" diff --git a/src/builder/JaniGSPNBuilder.h b/src/builder/JaniGSPNBuilder.h new file mode 100644 index 000000000..7985e73eb --- /dev/null +++ b/src/builder/JaniGSPNBuilder.h @@ -0,0 +1,161 @@ +#pragma once + +#include "src/storage/gspn/GSPN.h" +#include "src/storage/jani/Model.h" +#include "src/storage/expressions/ExpressionManager.h" + +namespace storm { + namespace builder { + class JaniGSPNBuilder { + public: + JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr const& expManager) : gspn(gspn), expressionManager(expManager) { + + } + + virtual ~JaniGSPNBuilder() { + for (auto const& varEntry : vars) { + delete varEntry.second; + } + } + + bool setIgnoreWeights(bool ignore = true) { + ignoreWeights = ignore; + } + + + 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"); + addVariables(model); + uint64_t locId = addLocation(mainAutomaton); + addEdges(mainAutomaton, locId); + model->addAutomaton(mainAutomaton); + model->setStandardSystemComposition(); + return model; + } + + void addVariables(storm::jani::Model* model) { + for (auto const& place : gspn.getPlaces()) { + storm::jani::Variable* janiVar = nullptr; + if (place.getCapacity() == -1) { + // Effectively no capacity limit known + janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), false); + } else { + 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()] = janiVar; + model->addVariable(*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) { + + storm::expressions::Expression guard = expressionManager->boolean(true); + for (auto const& trans : gspn.getImmediateTransitions()) { + if (ignoreWeights || trans->noWeightAttached()) { + std::vector 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 inhibPlaceIt = trans->getInhibitionPlacesCBegin(); inhibPlaceIt != trans->getInhibitionPlacesCEnd(); ++inhibPlaceIt) { + guard = guard && (vars[(**inhibPlaceIt).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(**inhibPlaceIt)); + } + for (auto outputPlaceIt = trans->getOutputPlacesCBegin(); outputPlaceIt != trans->getOutputPlacesCEnd(); ++outputPlaceIt) { + assignments.emplace_back( *vars[(**outputPlaceIt).getID()], (vars[(**outputPlaceIt).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(**outputPlaceIt)) ); + } + 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}); + automaton.addEdge(e); + } + + } + if(!ignoreWeights) { + + // TODO here there is something to fix if we add transition partitions. + storm::expressions::Expression guard = expressionManager->boolean(false); + std::vector 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 inPlaceIt = trans->getInputPlacesCBegin(); inPlaceIt != trans->getInputPlacesCEnd(); ++inPlaceIt) { + destguard = destguard && (vars[(**inPlaceIt).getID()]->getExpressionVariable() > trans->getInputArcMultiplicity(**inPlaceIt)); + } + for (auto inhibPlaceIt = trans->getInhibitionPlacesCBegin(); inhibPlaceIt != trans->getInhibitionPlacesCEnd(); ++inhibPlaceIt) { + destguard = destguard && (vars[(**inhibPlaceIt).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(**inhibPlaceIt)); + } + totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans->getWeight()), expressionManager->rational(0.0)); + + } + totalWeight = totalWeight.simplify(); + + for (auto const& trans : gspn.getImmediateTransitions()) { + if (trans->noWeightAttached()) { + continue; + } + storm::expressions::Expression destguard = expressionManager->boolean(true); + std::vector 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 inhibPlaceIt = trans->getInhibitionPlacesCBegin(); inhibPlaceIt != trans->getInhibitionPlacesCEnd(); ++inhibPlaceIt) { + destguard = destguard && (vars[(**inhibPlaceIt).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(**inhibPlaceIt)); + } + for (auto outputPlaceIt = trans->getOutputPlacesCBegin(); outputPlaceIt != trans->getOutputPlacesCEnd(); ++outputPlaceIt) { + assignments.emplace_back( *vars[(**outputPlaceIt).getID()], (vars[(**outputPlaceIt).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(**outputPlaceIt)) ); + } + 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::silentActionIndex, boost::none, guard.simplify(), weightedDestinations); + automaton.addEdge(e); + } + for (auto const& trans : gspn.getTimedTransitions()) { + storm::expressions::Expression guard = expressionManager->boolean(true); + + std::vector 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 inhibPlaceIt = trans->getInhibitionPlacesCBegin(); inhibPlaceIt != trans->getInhibitionPlacesCEnd(); ++inhibPlaceIt) { + guard = guard && (vars[(**inhibPlaceIt).getID()]->getExpressionVariable() > trans->getInhibitionArcMultiplicity(**inhibPlaceIt)); + } + for (auto outputPlaceIt = trans->getOutputPlacesCBegin(); outputPlaceIt != trans->getOutputPlacesCEnd(); ++outputPlaceIt) { + assignments.emplace_back( *vars[(**outputPlaceIt).getID()], (vars[(**outputPlaceIt).getID()]->getExpressionVariable() + trans->getOutputArcMultiplicity(**outputPlaceIt)) ); + } + 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}); + automaton.addEdge(e); + } + } + + private: + bool ignoreWeights; + const uint64_t janiVersion = 1; + storm::gspn::GSPN const& gspn; + std::map vars; + std::shared_ptr expressionManager; + + }; + } +} \ No newline at end of file diff --git a/src/storm-gspn.cpp b/src/storm-gspn.cpp index 40802218e..171d84766 100644 --- a/src/storm-gspn.cpp +++ b/src/storm-gspn.cpp @@ -5,6 +5,11 @@ #include "src/storage/gspn/GspnBuilder.h" #include "src/utility/macros.h" #include "src/utility/initialize.h" + +#include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/jani/Model.h" +#include "src/storage/jani/JsonExporter.h" +#include "src/builder/JaniGSPNBuilder.h" #include #include #include @@ -33,7 +38,7 @@ bool parseArguments(const int argc, const char **argv, std::string &inputFile, s // parse input file argument if (currentArg == "--input_file" || currentArg == "-i") { auto next = it + 1; - if (next != end) { + if (next == end) { return -1; } else { inputFile = *next; @@ -97,6 +102,14 @@ void printHelp() { std::cout << "-ot, --output_type: possible output types are: pnml, pnpro or ma" << std::endl; } +void handleJani(storm::gspn::GSPN const& gspn) { + std::shared_ptr exprManager(new storm::expressions::ExpressionManager()); + storm::builder::JaniGSPNBuilder builder(gspn, exprManager); + storm::jani::Model* model = builder.build(); + storm::jani::JsonExporter::toFile(*model, "gspn.jani"); + delete model; +} + int main(const int argc, const char **argv) { std::string inputFile, formula, outputFile, outputType; if (!parseArguments(argc, argv, inputFile, formula, outputFile, outputType)) { @@ -114,8 +127,9 @@ int main(const int argc, const char **argv) { // todo ------[marker] gspn.isValid(); - storm::gspn::GspnBuilder builder2; - builder2.addPlace(2); + handleJani(gspn); + //storm::gspn::GspnBuilder builder2; + //builder2.addPlace(2); // //std::ofstream file; @@ -123,20 +137,20 @@ int main(const int argc, const char **argv) { //gspn.writeDotToStream(file); //file.close(); - std::ofstream file; - file.open("/Users/thomas/Desktop/gspn.pnpro"); - gspn.toPnpro(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; + //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;