diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index b785be6c3..8ccdc12be 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -22,6 +22,7 @@ #include "storm-dft/settings/modules/DFTSettings.h" #include "storm-gspn/storage/gspn/GSPN.h" +#include "storm-gspn/storm-gspn.h" #include "storm/settings/modules/GSPNSettings.h" #include "storm/settings/modules/GSPNExportSettings.h" @@ -112,6 +113,7 @@ void initializeSettings() { // For translation into JANI via GSPN. storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); } /*! @@ -140,7 +142,16 @@ int main(const int argc, const char** argv) { if (dftSettings.isTransformToGspn()) { storm::gspn::GSPN* gspn = transformDFT(dftSettings.getDftFilename()); + storm::handleGSPNExportSettings(*gspn); + storm::jani::Model* model = storm::buildJani(*gspn); + + storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule(); + if (janiSettings.isJaniFileSet()) { + storm::exportJaniModel(*model, {}, janiSettings.getJaniFilename()); + } + + delete model; delete gspn; storm::utility::cleanUp(); return 0; diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h index 76517a3a1..305fa0129 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.h +++ b/src/storm-gspn/builder/JaniGSPNBuilder.h @@ -9,17 +9,15 @@ namespace storm { class JaniGSPNBuilder { public: JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr const& expManager) : gspn(gspn), expressionManager(expManager) { - gspn.writeDotToStream(std::cout); + } virtual ~JaniGSPNBuilder() { - for (auto const& varEntry : vars) { - delete varEntry.second; - } + } void setIgnoreWeights(bool ignore = true) { - ignoreWeights = ignore; + //ignoreWeights = ignore; } @@ -46,8 +44,8 @@ namespace storm { } assert(janiVar != nullptr); assert(vars.count(place.getID()) == 0); - vars[place.getID()] = janiVar; - model->addVariable(*janiVar); + vars[place.getID()] = &model->addVariable(*janiVar); + delete janiVar; } } @@ -59,95 +57,76 @@ namespace storm { 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; + 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); + std::vector weightedDestinations; + + 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()) { - guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); - assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second); + destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second); } for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { - guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second); + 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 ); - } - storm::jani::OrderedAssignments oa(assignments); - storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa); - storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, guard, {dest}); - automaton.addEdge(e); + totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0)); + } + totalWeight = totalWeight.simplify(); - } - 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. - for (auto const& partition : gspn.getPartitions()) { - storm::expressions::Expression guard = expressionManager->boolean(false); - std::vector weightedDestinations; - - - assert(lastPriority <= partition.priority); - if (lastPriority < partition.priority) { - priorityGuard = priorityGuard && !lastPriorityGuard; - lastPriority = partition.priority; - } else { - assert(lastPriority == partition.priority); + 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; } - - // 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); + 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); } - totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0)); - } - 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 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) ); + 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; - 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; + 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; } for (auto const& trans : gspn.getTimedTransitions()) { @@ -155,27 +134,33 @@ namespace storm { std::vector assignments; for (auto const& inPlaceEntry : trans.getInputPlaces()) { - guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); - assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) ); + 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); + guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() >= inhibPlaceEntry.second); } for (auto const& outputPlaceEntry : trans.getOutputPlaces()) { - assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) ); + 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)); + } } storm::jani::OrderedAssignments oa(assignments); storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa); storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, 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::map vars; std::shared_ptr expressionManager; }; diff --git a/src/storm-gspn/storm-gspn.h b/src/storm-gspn/storm-gspn.h new file mode 100644 index 000000000..3af59a9c1 --- /dev/null +++ b/src/storm-gspn/storm-gspn.h @@ -0,0 +1,32 @@ +#pragma once + +#include "storm/storage/jani/Model.h" + +#include "storm-gspn/builder/JaniGSPNBuilder.h" +#include "storm-gspn/storage/gspn/Gspn.h" + +#include "storm/settings/modules/GSPNExportSettings.h" + +namespace storm { + /** + * Builds JANI model from GSPN. + */ + storm::jani::Model* buildJani(storm::gspn::GSPN const& gspn) { + std::shared_ptr exprManager(new storm::expressions::ExpressionManager()); + storm::builder::JaniGSPNBuilder builder(gspn, exprManager); + return builder.build(); + } + + void handleGSPNExportSettings(storm::gspn::GSPN const& gspn) { + storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule(); + if (exportSettings.isWriteToDotSet()) { + std::ofstream fs; + fs.open(exportSettings.getWriteToDotFilename()); + gspn.writeDotToStream(std::cout); + gspn.writeDotToStream(fs); + fs.close(); + } + + } + +} \ No newline at end of file diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 7ba6cc09e..cfa8c66d1 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -12,7 +12,7 @@ #include "storm/settings/modules/JaniExportSettings.h" #include "storm/utility/storm-version.h" -#include "storm/storage/jani/JSONExporter.h" + // Includes for the linked libraries and versions header. @@ -253,14 +253,7 @@ namespace storm { } if (model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { - STORM_LOG_TRACE("Exporting JANI model."); - if (storm::settings::getModule().isExportAsStandardJaniSet()) { - storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel()); - normalisedModel.makeStandardJaniCompliant(); - storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), storm::settings::getModule().getJaniFilename()); - } else { - storm::jani::JsonExporter::toFile(model.asJaniModel(), formulasInProperties(properties), storm::settings::getModule().getJaniFilename()); - } + exportJaniModel(model.asJaniModel(), properties, storm::settings::getModule().getJaniFilename()); } if (ioSettings.isNoBuildModelSet()) { diff --git a/src/storm/settings/modules/GSPNExportSettings.h b/src/storm/settings/modules/GSPNExportSettings.h index 3db836cf7..32ae422ba 100644 --- a/src/storm/settings/modules/GSPNExportSettings.h +++ b/src/storm/settings/modules/GSPNExportSettings.h @@ -15,7 +15,7 @@ namespace storm { GSPNExportSettings(); /** - * Retrievew whether the pgcl file option was set + * Retrieve whether the pgcl file option was set */ bool isWriteToDotSet() const; diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index 667952719..18f0aebae 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -141,5 +141,14 @@ namespace storm { return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndVariable()); } + std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments) { + stream << "["; + for(auto const& e : assignments.allAssignments) { + stream << *e << std::endl; + } + stream << "]"; + return stream; + } + } } diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index 789b1014a..999b9d95f 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/src/storm/storage/jani/OrderedAssignments.h @@ -109,6 +109,8 @@ namespace storm { */ void substitute(std::map const& substitution); + friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments); + private: static std::vector>::const_iterator lowerBound(Assignment const& assignment, std::vector> const& assignments); diff --git a/src/storm/utility/storm.cpp b/src/storm/utility/storm.cpp index 40ab41b91..62c499fbd 100644 --- a/src/storm/utility/storm.cpp +++ b/src/storm/utility/storm.cpp @@ -30,6 +30,17 @@ namespace storm{ modelAndFormulae.first.checkValid(); return modelAndFormulae; } + + void exportJaniModel(storm::jani::Model const& model, std::vector const& properties, std::string const& filepath) { + STORM_LOG_TRACE("Exporting JANI model."); + if (storm::settings::getModule().isExportAsStandardJaniSet()) { + storm::jani::Model normalisedModel = model; + normalisedModel.makeStandardJaniCompliant(); + storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), filepath); + } else { + storm::jani::JsonExporter::toFile(model, formulasInProperties(properties), filepath); + } + } /** * Helper diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index cee49998b..6657a7d6d 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -23,6 +23,7 @@ #include "storm/settings/modules/RegionSettings.h" #include "storm/settings/modules/EliminationSettings.h" #include "storm/settings/modules/JitBuilderSettings.h" +#include "storm/settings/modules/JaniExportSettings.h" // Formula headers. #include "storm/logic/Formulas.h" @@ -55,6 +56,7 @@ #include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h" #include "storm/storage/ModelFormulasPair.h" #include "storm/storage/SymbolicModelDescription.h" +#include "storm/storage/jani/JSONExporter.h" // Headers for model checking. #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" @@ -575,7 +577,13 @@ namespace storm { } return result; } - + + + /** + * + */ + void exportJaniModel(storm::jani::Model const& model, std::vector const& properties, std::string const& filepath); + template void exportMatrixToFile(std::shared_ptr> model, std::string const& filepath) { STORM_LOG_THROW(model->getType() != storm::models::ModelType::Ctmc, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." );