diff --git a/CHANGELOG.md b/CHANGELOG.md index 149861c2e..2c11fea31 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,7 @@ The releases of major and minor versions contain an overview of changes since th Version 1.5.x ------------- ## Version 1.5.x (Under development) +- Scheduler export: Properly handle models with end components. Added export in .json format. - CMake: Search for Gurobi prefers new versions - Tests: Enabled tests for permissive schedulers diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index e6508c190..334480cbf 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -448,6 +448,11 @@ namespace storm { options.setBuildAllLabels(true); options.setBuildAllRewardModels(true); } + + if (buildSettings.isAddOverlappingGuardsLabelSet()) { + options.setAddOverlappingGuardsLabel(true); + } + return storm::api::buildSparseModel(input.model.get(), options, useJit, storm::settings::getModule().isDoctorSet()); } diff --git a/src/storm/api/export.h b/src/storm/api/export.h index 97859520c..792319f31 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -48,7 +48,12 @@ namespace storm { void exportScheduler(std::shared_ptr> const& model, storm::storage::Scheduler const& scheduler, std::string const& filename) { std::ofstream stream; storm::utility::openFile(filename, stream); - scheduler.printToStream(stream, model); + std::string jsonFileExtension = ".json"; + if (filename.size() > 4 && std::equal(jsonFileExtension.rbegin(), jsonFileExtension.rend(), filename.rbegin())) { + scheduler.printJsonToStream(stream, model); + } else { + scheduler.printToStream(stream, model); + } storm::utility::closeFile(stream); } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp index 62dba3778..8db9a6c75 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.cpp @@ -2,6 +2,8 @@ #include "storm/storage/BitVector.h" #include "storm/storage/MaximalEndComponentDecomposition.h" +#include "storm/storage/Scheduler.h" +#include "storm/utility/graph.h" #include "storm/adapters/RationalNumberAdapter.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -11,7 +13,7 @@ namespace storm { namespace helper { template - SparseMdpEndComponentInformation::SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::BitVector const& maybeStates) : NOT_IN_EC(std::numeric_limits::max()), eliminatedEndComponents(false), numberOfMaybeStatesInEc(0), numberOfMaybeStatesNotInEc(0), numberOfEc(endComponentDecomposition.size()) { + SparseMdpEndComponentInformation::SparseMdpEndComponentInformation(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::BitVector const& maybeStates) : NOT_IN_EC(std::numeric_limits::max()), eliminatedEndComponents(!endComponentDecomposition.empty()), numberOfMaybeStatesInEc(0), numberOfMaybeStatesNotInEc(0), numberOfEc(endComponentDecomposition.size()) { // (1) Compute how many maybe states there are before each other maybe state. maybeStatesBefore = maybeStates.getNumberOfSetBitsBeforeIndices(); @@ -90,7 +92,7 @@ namespace storm { } template - SparseMdpEndComponentInformation SparseMdpEndComponentInformation::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector) { + SparseMdpEndComponentInformation SparseMdpEndComponentInformation::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector, bool gatherExitChoices) { SparseMdpEndComponentInformation result(endComponentDecomposition, maybeStates); @@ -163,7 +165,7 @@ namespace storm { // (3) Create the parts of the submatrix and vector b that belong to states contained in ECs. for (auto const& mec : endComponentDecomposition) { builder.newRowGroup(currentRow); - + std::vector exitChoices; for (auto const& stateActions : mec) { uint64_t const& state = stateActions.first; for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { @@ -207,9 +209,16 @@ namespace storm { } } + if (gatherExitChoices) { + exitChoices.push_back(row); + } + ++currentRow; } } + if (gatherExitChoices) { + result.ecToExitChoicesBefore.push_back(std::move(exitChoices)); + } } submatrix = builder.build(currentRow); @@ -217,7 +226,7 @@ namespace storm { } template - SparseMdpEndComponentInformation SparseMdpEndComponentInformation::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector) { + SparseMdpEndComponentInformation SparseMdpEndComponentInformation::eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector, bool gatherExitChoices) { SparseMdpEndComponentInformation result(endComponentDecomposition, maybeStates); @@ -271,7 +280,7 @@ namespace storm { // (3) Create the parts of the submatrix and vector b that belong to states contained in ECs. for (auto const& mec : endComponentDecomposition) { builder.newRowGroup(currentRow); - + std::vector exitChoices; for (auto const& stateActions : mec) { uint64_t const& state = stateActions.first; for (uint64_t row = transitionMatrix.getRowGroupIndices()[state], endRow = transitionMatrix.getRowGroupIndices()[state + 1]; row < endRow; ++row) { @@ -304,9 +313,16 @@ namespace storm { } } + if (gatherExitChoices) { + exitChoices.push_back(row); + } + ++currentRow; } } + if (gatherExitChoices) { + result.ecToExitChoicesBefore.push_back(std::move(exitChoices)); + } } submatrix = builder.build(); @@ -315,23 +331,65 @@ namespace storm { template void SparseMdpEndComponentInformation::setValues(std::vector& result, storm::storage::BitVector const& maybeStates, std::vector const& fromResult) { - auto notInEcResultIt = result.begin(); + // The following assumes that row groups associated to EC states are at the very end. + auto notInEcResultIt = fromResult.begin(); for (auto state : maybeStates) { if (this->isStateInEc(state)) { - result[state] = result[this->getRowGroupAfterElimination(state)]; + STORM_LOG_ASSERT(this->getRowGroupAfterElimination(state) >= this->getNumberOfMaybeStatesNotInEc(), "Expected introduced EC states to be located at the end of the matrix."); + result[state] = fromResult[this->getRowGroupAfterElimination(state)]; } else { result[state] = *notInEcResultIt; ++notInEcResultIt; } } - STORM_LOG_ASSERT(notInEcResultIt == result.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators."); + STORM_LOG_ASSERT(notInEcResultIt == fromResult.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators."); + } + + template + void SparseMdpEndComponentInformation::setScheduler(storm::storage::Scheduler& scheduler, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& fromResult) { + // The following assumes that row groups associated to EC states are at the very end. + storm::storage::BitVector maybeStatesWithoutChoice(maybeStates.size(), false); + storm::storage::BitVector ecStayChoices(transitionMatrix.getRowCount(), false); + auto notInEcResultIt = fromResult.begin(); + for (auto const& state : maybeStates) { + if (this->isStateInEc(state)) { + STORM_LOG_ASSERT(this->getRowGroupAfterElimination(state) >= this->getNumberOfMaybeStatesNotInEc(), "Expected introduced EC states to be located at the end of the matrix."); + STORM_LOG_ASSERT(!ecToExitChoicesBefore.empty(), "No EC exit choices available. End Components have probably been build without."); + uint64_t ec = getEc(state); + auto const& exitChoices = ecToExitChoicesBefore[ec]; + uint64_t afterEliminationChoice = fromResult[this->getRowGroupAfterElimination(state)]; + uint64_t beforeEliminationGlobalChoiceIndex = exitChoices[afterEliminationChoice]; + bool noChoice = true; + for (uint64_t globalChoice = transitionMatrix.getRowGroupIndices()[state]; globalChoice < transitionMatrix.getRowGroupIndices()[state+1]; ++globalChoice) { + // Is this the selected exit choice? + if (globalChoice == beforeEliminationGlobalChoiceIndex) { + scheduler.setChoice(beforeEliminationGlobalChoiceIndex - transitionMatrix.getRowGroupIndices()[state], state); + noChoice = false; + } else { + // Check if this is an exit choice + if (std::find(exitChoices.begin(), exitChoices.end(), globalChoice) == exitChoices.end()) { + ecStayChoices.set(globalChoice, true); + } + } + } + maybeStatesWithoutChoice.set(state, noChoice); + } else { + scheduler.setChoice(*notInEcResultIt, state); + ++notInEcResultIt; + } + } + + STORM_LOG_ASSERT(notInEcResultIt == fromResult.begin() + this->getNumberOfMaybeStatesNotInEc(), "Mismatching iterators."); + // The maybeStates without a choice shall reach maybeStates with a choice with probability 1 + storm::utility::graph::computeSchedulerProb1E(maybeStates, transitionMatrix, backwardTransitions, maybeStatesWithoutChoice, ~maybeStatesWithoutChoice, scheduler, ecStayChoices); + } template class SparseMdpEndComponentInformation; #ifdef STORM_HAVE_CARL template class SparseMdpEndComponentInformation; - template class SparseMdpEndComponentInformation; + //template class SparseMdpEndComponentInformation; #endif } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h index 513ffb49c..f93fb8dce 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h @@ -12,6 +12,9 @@ namespace storm { template class MaximalEndComponentDecomposition; + + template + class Scheduler; } namespace modelchecker { @@ -50,11 +53,12 @@ namespace storm { uint64_t getNotInEcMarker() const; - static SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector); + static SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const* sumColumns, storm::storage::BitVector const* selectedChoices, std::vector const* summand, storm::storage::SparseMatrix& submatrix, std::vector* columnSumVector, std::vector* summandResultVector, bool gatherExitChoices = false); - static SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector); + static SparseMdpEndComponentInformation eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition const& endComponentDecomposition, storm::storage::SparseMatrix const& transitionMatrix, std::vector& rhsVector, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix& submatrix, std::vector& subvector, bool gatherExitChoices = false); void setValues(std::vector& result, storm::storage::BitVector const& maybeStates, std::vector const& fromResult); + void setScheduler(storm::storage::Scheduler& scheduler, storm::storage::BitVector const& maybeStates, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& fromResult); private: // A constant that marks that a state is not contained in any EC. @@ -70,6 +74,7 @@ namespace storm { uint64_t numberOfMaybeStatesNotInEc; uint64_t numberOfEc; std::vector maybeStateToEc; + std::vector> ecToExitChoicesBefore; // Only available, if gatherExitChoices was enabled. Empty otherwise. }; } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 174cf739f..1e9722d7a 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -583,7 +583,7 @@ namespace storm { } template - boost::optional> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix& submatrix, std::vector& b) { + boost::optional> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix& submatrix, std::vector& b, bool produceScheduler) { // Get the set of states that (under some scheduler) can stay in the set of maybestates forever storm::storage::BitVector candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.maybeStates); @@ -599,7 +599,7 @@ namespace storm { // Only do more work if there are actually end-components. if (doDecomposition && !endComponentDecomposition.empty()) { STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " EC(s)."); - SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr); + SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr, submatrix, &b, nullptr, produceScheduler); // If the solve goal has relevant values, we need to adjust them. if (goal.hasRelevantValues()) { @@ -663,10 +663,7 @@ namespace storm { // If the hint information tells us that we have to eliminate MECs, we do so now. boost::optional> ecInformation; if (hintInformation.getEliminateEndComponents()) { - ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, submatrix, b); - - // Make sure we are not supposed to produce a scheduler if we actually eliminate end components. - STORM_LOG_THROW(!ecInformation || !ecInformation.get().getEliminatedEndComponents() || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver."); + ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, submatrix, b, produceScheduler); } else { // Otherwise, we compute the standard equations. computeFixedPointSystemUntilProbabilities(goal, transitionMatrix, qualitativeStateSets, submatrix, b); @@ -678,13 +675,15 @@ namespace storm { // If we eliminated end components, we need to extract the result differently. if (ecInformation && ecInformation.get().getEliminatedEndComponents()) { ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); + if (produceScheduler) { + ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler()); + } } else { // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); - } - - if (produceScheduler) { - extractSchedulerChoices(*scheduler, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates); + if (produceScheduler) { + extractSchedulerChoices(*scheduler, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates); + } } } } @@ -1028,7 +1027,7 @@ namespace storm { } template - boost::optional> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, boost::optional const& selectedChoices, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix& submatrix, std::vector& b, boost::optional>& oneStepTargetProbabilities) { + boost::optional> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, boost::optional const& selectedChoices, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::SparseMatrix& submatrix, std::vector& b, boost::optional>& oneStepTargetProbabilities, bool produceScheduler) { // Start by computing the choices with reward 0, as we only want ECs within this fragment. storm::storage::BitVector zeroRewardChoices(transitionMatrix.getRowCount()); @@ -1075,7 +1074,7 @@ namespace storm { // Only do more work if there are actually end-components. if (doDecomposition && !endComponentDecomposition.empty()) { STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " ECs."); - SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b); + SparseMdpEndComponentInformation result = SparseMdpEndComponentInformation::eliminateEndComponents(endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector, submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b, produceScheduler); // If the solve goal has relevant values, we need to adjust them. if (goal.hasRelevantValues()) { @@ -1163,10 +1162,7 @@ namespace storm { // If the hint information tells us that we have to eliminate MECs, we do so now. boost::optional> ecInformation; if (hintInformation.getEliminateEndComponents()) { - ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities); - - // Make sure we are not supposed to produce a scheduler if we actually eliminate end components. - STORM_LOG_THROW(!ecInformation || !ecInformation.get().getEliminatedEndComponents() || !produceScheduler, storm::exceptions::NotSupportedException, "Producing schedulers is not supported if end-components need to be eliminated for the solver."); + ecInformation = computeFixedPointSystemReachabilityRewardsEliminateEndComponents(goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities, produceScheduler); } else { // Otherwise, we compute the standard equations. computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr); @@ -1184,13 +1180,15 @@ namespace storm { // If we eliminated end components, we need to extract the result differently. if (ecInformation && ecInformation.get().getEliminatedEndComponents()) { ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); + if (produceScheduler) { + ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions, resultForMaybeStates.getScheduler()); + } } else { // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues()); - } - - if (produceScheduler) { - extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates, selectedChoices); + if (produceScheduler) { + extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates, selectedChoices); + } } } } diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 1867978c5..071a45071 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -419,7 +419,16 @@ namespace storm { void Model::setTransitionMatrix(storm::storage::SparseMatrix&& transitionMatrix) { this->transitionMatrix = std::move(transitionMatrix); } - + + template + bool Model::isSinkState(uint64_t state) const { + for (auto const& entry : this->getTransitionMatrix().getRowGroup(state)) { + if (entry.getColumn() != state) { return false; } + if (storm::utility::isOne(entry.getValue())) { return false; } + } + return true; + } + template bool Model::isSparseModel() const { return true; diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index 962fda437..c86a5924f 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -318,6 +318,8 @@ namespace storm { * @param out The stream the information is to be printed to. */ virtual void printModelInformationToStream(std::ostream& out) const override; + + bool isSinkState(uint64_t sink) const; /*! * Exports the model to the dot-format and prints the result to the given stream. diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index 3d1852ba5..7ef3c894c 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -33,6 +33,7 @@ namespace storm { const std::string buildChoiceOriginsOptionName = "buildchoiceorig"; const std::string buildStateValuationsOptionName = "buildstateval"; const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate"; + const std::string buildOverlappingGuardsLabelOptionName = "overlappingguardslabel"; const std::string bitsForUnboundedVariablesOptionName = "int-bits"; BuildSettings::BuildSettings() : ModuleSettings(moduleName) { @@ -51,6 +52,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, buildOutOfBoundsStateOptionName, false, "If set, a state for out-of-bounds valuations is added").setIsAdvanced().build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildOverlappingGuardsLabelOptionName, false, "For states where multiple guards are enabled, we add a label (for debugging DTMCs)").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, bitsForUnboundedVariablesOptionName, false, "Sets the number of bits that is used for unbounded integer variables.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "The number of bits.").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(0,63)).setDefaultValueUnsignedInteger(32).build()).build()); } @@ -99,6 +101,10 @@ namespace storm { return this->getOption(buildOutOfBoundsStateOptionName).getHasOptionBeenSet(); } + bool BuildSettings::isAddOverlappingGuardsLabelSet() const { + return this->getOption(buildOverlappingGuardsLabelOptionName).getHasOptionBeenSet(); + } + storm::builder::ExplorationOrder BuildSettings::getExplorationOrder() const { std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString(); if (explorationOrderAsString == "dfs") { diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h index 3cce0a705..10ae675e3 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/src/storm/settings/modules/BuildSettings.h @@ -99,7 +99,12 @@ namespace storm { * @return */ bool isBuildOutOfBoundsStateSet() const; - + + /*! + * Retrieves whether to build the overlapping label + */ + bool isAddOverlappingGuardsLabelSet() const; + /*! * Retrieves the number of bits that should be used to represent unbounded integer variables * @return diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 7da94b94e..e2ecdf14b 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -59,7 +59,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, false, "If given, the loaded jani model will be written to the specified file in the dot format.").setIsAdvanced() .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportSchedulerOptionName, false, "Exports the choices of an optimal scheduler to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportSchedulerOptionName, false, "Exports the choices of an optimal scheduler to the given file (if supported by engine).").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file. Use file extension '.json' to export in json.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportMonotonicityName, false, "Exports the result of monotonicity checking to the given file.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The output file.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); diff --git a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp new file mode 100644 index 000000000..d8fd4a82a --- /dev/null +++ b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp @@ -0,0 +1,50 @@ +#include "storm/simulator/DiscreteTimeSparseModelSimulator.h" +#include "storm/models/sparse/Model.h" + +namespace storm { + namespace simulator { + template + DiscreteTimeSparseModelSimulator::DiscreteTimeSparseModelSimulator(storm::models::sparse::Model const& model) : model(model), currentState(*model.getInitialStates().begin()) { + STORM_LOG_WARN_COND(model.getInitialStates().getNumberOfSetBits()==1, "The model has multiple initial states. This simulator assumes it starts from the initial state with the lowest index."); + + } + + template + void DiscreteTimeSparseModelSimulator::setSeed(uint64_t seed) { + generator = storm::utility::RandomProbabilityGenerator(seed); + } + + template + bool DiscreteTimeSparseModelSimulator::step(uint64_t action) { + // TODO lots of optimization potential. + // E.g., do not sample random numbers if there is only a single transition + ValueType probability = generator.random(); + STORM_LOG_ASSERT(action < model.getTransitionMatrix().getRowGroupSize(currentState), "Action index higher than number of actions"); + uint64_t row = model.getTransitionMatrix().getRowGroupIndices()[currentState] + action; + ValueType sum = storm::utility::zero(); + for (auto const& entry : model.getTransitionMatrix().getRow(row)) { + sum += entry.getValue(); + if (sum >= probability) { + currentState = entry.getColumn(); + return true; + } + } + return false; + STORM_LOG_ASSERT(false, "This position should never be reached"); + } + + template + uint64_t DiscreteTimeSparseModelSimulator::getCurrentState() const { + return currentState; + } + + template + bool DiscreteTimeSparseModelSimulator::resetToInitial() { + currentState = *model.getInitialStates().begin(); + return true; + } + + + template class DiscreteTimeSparseModelSimulator; + } +} \ No newline at end of file diff --git a/src/storm/simulator/DiscreteTimeSparseModelSimulator.h b/src/storm/simulator/DiscreteTimeSparseModelSimulator.h new file mode 100644 index 000000000..1637bffec --- /dev/null +++ b/src/storm/simulator/DiscreteTimeSparseModelSimulator.h @@ -0,0 +1,30 @@ +#include +#include "storm/models/sparse/Model.h" +#include "storm/utility/random.h" + +namespace storm { + namespace simulator { + + /** + * This class is a low-level interface to quickly sample from Discrete-Time Models + * stored explicitly as a SparseModel. + * Additional information about state, actions, should be obtained via the model itself. + * + * TODO: It may be nice to write a CPP wrapper that does not require to actually obtain such informations yourself. + * @tparam ModelType + */ + template> + class DiscreteTimeSparseModelSimulator { + public: + DiscreteTimeSparseModelSimulator(storm::models::sparse::Model const& model); + void setSeed(uint64_t); + bool step(uint64_t action); + uint64_t getCurrentState() const; + bool resetToInitial(); + protected: + uint64_t currentState; + storm::models::sparse::Model const& model; + storm::utility::RandomProbabilityGenerator generator; + }; + } +} \ No newline at end of file diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index fa40732c6..673a64173 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -1,7 +1,8 @@ -#include +#include "storm/utility/vector.h" #include "storm/storage/Scheduler.h" #include "storm/utility/macros.h" +#include "storm/adapters/JsonAdapter.h" #include "storm/exceptions/NotImplementedException.h" #include @@ -222,6 +223,54 @@ namespace storm { out << "___________________________________________________________________" << std::endl; } + template <> + void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers not implemented for this value type."); + } + + template + void Scheduler::printJsonToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { + STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); + STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given."); + STORM_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers with memory not implemented."); + storm::json output; + for (uint64_t state = 0; state < schedulerChoices.front().size(); ++state) { + // Check whether the state is skipped + if (skipUniqueChoices && model != nullptr && model->getTransitionMatrix().getRowGroupSize(state) == 1) { + continue; + } + storm::json stateChoicesJson; + if (model && model->hasStateValuations()) { + stateChoicesJson["s"] = model->getStateValuations().getStateValuation(state).toJson(); + } else { + stateChoicesJson["s"] = state; + } + auto const& choice = schedulerChoices.front()[state]; + storm::json choicesJson; + if (choice.isDefined()) { + for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) { + uint64_t globalChoiceIndex = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first; + storm::json choiceJson; + if (model && model->hasChoiceOrigins() && model->getChoiceOrigins()->getIdentifier(globalChoiceIndex) != model->getChoiceOrigins()->getIdentifierForChoicesWithNoOrigin()) { + choiceJson["origin"] = model->getChoiceOrigins()->getChoiceAsJson(globalChoiceIndex); + } + if (model && model->hasChoiceLabeling()) { + auto choiceLabels = model->getChoiceLabeling().getLabelsOfChoice(globalChoiceIndex); + choiceJson["labels"] = std::vector(choiceLabels.begin(), choiceLabels.end()); + } + choiceJson["index"] = globalChoiceIndex; + choiceJson["prob"] = storm::utility::convertNumber(choiceProbPair.second); + choicesJson.push_back(std::move(choiceJson)); + } + } else { + choicesJson = "undefined"; + } + stateChoicesJson["c"] = std::move(choicesJson); + output.push_back(std::move(stateChoicesJson)); + } + out << output.dump(4); + } + template class Scheduler; template class Scheduler; template class Scheduler; diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index c6aa30b32..492a7a2f3 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -111,7 +111,12 @@ namespace storm { */ void printToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; - + + /*! + * Prints the scheduler in json format to the given output stream. + */ + void printJsonToStream(std::ostream& out, std::shared_ptr> model = nullptr, bool skipUniqueChoices = false) const; + private: boost::optional memoryStructure; diff --git a/src/storm/storage/expressions/SimpleValuation.cpp b/src/storm/storage/expressions/SimpleValuation.cpp index e60556305..4ed71239a 100644 --- a/src/storm/storage/expressions/SimpleValuation.cpp +++ b/src/storm/storage/expressions/SimpleValuation.cpp @@ -144,6 +144,23 @@ namespace storm { } } + typename SimpleValuation::Json SimpleValuation::toJson() const { + Json result; + for (auto const& variable : getManager()) { + if (variable.second.isBooleanType()) { + result[variable.first.getName()] = this->getBooleanValue(variable.first); + } else if (variable.second.isIntegerType()) { + result[variable.first.getName()] = this->getIntegerValue(variable.first); + } else if (variable.second.isRationalType()) { + result[variable.first.getName()] = this->getRationalValue(variable.first); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); + } + } + return result; + } + + std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation) { out << valuation.toString(false) << std::endl; return out; diff --git a/src/storm/storage/expressions/SimpleValuation.h b/src/storm/storage/expressions/SimpleValuation.h index 3936ed546..c036d4d5c 100644 --- a/src/storm/storage/expressions/SimpleValuation.h +++ b/src/storm/storage/expressions/SimpleValuation.h @@ -6,6 +6,7 @@ #include #include "storm/storage/expressions/Valuation.h" +#include "storm/adapters/JsonAdapter.h" namespace storm { namespace expressions { @@ -17,6 +18,8 @@ namespace storm { public: friend class SimpleValuationPointerHash; friend class SimpleValuationPointerLess; + typedef storm::json Json; + /*! * Creates an empty simple valuation that is associated to no manager and has no variables. @@ -63,6 +66,7 @@ namespace storm { virtual std::string toPrettyString(std::set const& selectedVariables) const; virtual std::string toString(bool pretty = true) const; + Json toJson() const; friend std::ostream& operator<<(std::ostream& out, SimpleValuation const& valuation); diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index e312a7e93..46317c870 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -995,36 +995,39 @@ namespace storm { return destDeclarations; } + ExportJsonType buildEdge(Edge const& edge , std::map const& actionNames, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { + STORM_LOG_THROW(edge.getDestinations().size() > 0, storm::exceptions::InvalidJaniException, "An edge without destinations is not allowed."); + ExportJsonType edgeEntry; + edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex()); + if (!edge.hasSilentAction()) { + edgeEntry["action"] = actionNames.at(edge.getActionIndex()); + } + if (edge.hasRate()) { + edgeEntry["rate"]["exp"] = buildExpression(edge.getRate(), constants, globalVariables, localVariables); + if (commentExpressions) { + edgeEntry["rate"]["comment"] = edge.getRate().toString(); + } + } + if (!edge.getGuard().isTrue()) { + edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard(), constants, globalVariables, localVariables); + if (commentExpressions) { + edgeEntry["guard"]["comment"] = edge.getGuard().toString(); + } + } + edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames, constants, globalVariables, localVariables, commentExpressions); + if (!edge.getAssignments().empty()) { + edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments(), constants, globalVariables, localVariables, commentExpressions); + } + return edgeEntry; + } + ExportJsonType buildEdges(std::vector const& edges , std::map const& actionNames, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { ExportJsonType edgeDeclarations = std::vector(); for(auto const& edge : edges) { if (edge.getGuard().isFalse()) { continue; } - STORM_LOG_THROW(edge.getDestinations().size() > 0, storm::exceptions::InvalidJaniException, "An edge without destinations is not allowed."); - ExportJsonType edgeEntry; - edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex()); - if(!edge.hasSilentAction()) { - edgeEntry["action"] = actionNames.at(edge.getActionIndex()); - } - if(edge.hasRate()) { - edgeEntry["rate"]["exp"] = buildExpression(edge.getRate(), constants, globalVariables, localVariables); - if (commentExpressions) { - edgeEntry["rate"]["comment"] = edge.getRate().toString(); - } - } - if (!edge.getGuard().isTrue()) { - edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard(), constants, globalVariables, localVariables); - if (commentExpressions) { - edgeEntry["guard"]["comment"] = edge.getGuard().toString(); - } - } - edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames, constants, globalVariables, localVariables, commentExpressions); - if (!edge.getAssignments().empty()) { - edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments(), constants, globalVariables, localVariables, commentExpressions); - } - - edgeDeclarations.push_back(std::move(edgeEntry)); + edgeDeclarations.push_back(buildEdge(edge, actionNames, locationNames, constants, globalVariables, localVariables, commentExpressions)); } return edgeDeclarations; } @@ -1065,6 +1068,11 @@ namespace storm { jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition()); } + ExportJsonType JsonExporter::getEdgeAsJson(storm::jani::Model const& janiModel, uint64_t automatonIndex, uint64_t edgeIndex, bool commentExpressions) { + auto const& automaton = janiModel.getAutomaton(automatonIndex); + return buildEdge(automaton.getEdge(edgeIndex), janiModel.getActionIndexToNameMap(), automaton.buildIdToLocationNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), automaton.getVariables(), commentExpressions); + } + std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) { switch(ft) { case storm::modelchecker::FilterType::MIN: diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index d8ba87489..7c11358c6 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -89,7 +89,7 @@ namespace storm { static void toFile(storm::jani::Model const& janiModel, std::vector const& formulas, std::string const& filepath, bool checkValid = true, bool compact = false); static void toStream(storm::jani::Model const& janiModel, std::vector const& formulas, std::ostream& ostream, bool checkValid = false, bool compact = false); - + static ExportJsonType getEdgeAsJson(storm::jani::Model const& janiModel, uint64_t automatonIndex, uint64_t edgeIndex, bool commentExpressions = true); private: void convertModel(storm::jani::Model const& model, bool commentExpressions = true); void convertProperties(std::vector const& formulas, storm::jani::Model const& model); diff --git a/src/storm/storage/sparse/ChoiceOrigins.cpp b/src/storm/storage/sparse/ChoiceOrigins.cpp index 56c512f37..ed3fbb409 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.cpp +++ b/src/storm/storage/sparse/ChoiceOrigins.cpp @@ -66,6 +66,18 @@ namespace storm { std::string const& ChoiceOrigins::getChoiceInfo(uint_fast64_t choiceIndex) const { return getIdentifierInfo(getIdentifier(choiceIndex)); } + + typename ChoiceOrigins::Json const& ChoiceOrigins::getIdentifierAsJson(uint_fast64_t identifier) const { + STORM_LOG_ASSERT(identifier < this->getNumberOfIdentifiers(), "Invalid choice origin identifier: " << identifier); + if (identifierToJson.empty()) { + computeIdentifierJson(); + } + return identifierToJson[identifier]; + } + + typename ChoiceOrigins::Json const& ChoiceOrigins::getChoiceAsJson(uint_fast64_t choiceIndex) const { + return getIdentifierAsJson(getIdentifier(choiceIndex)); + } std::shared_ptr ChoiceOrigins::selectChoices(storm::storage::BitVector const& selectedChoices) const { std::vector indexToIdentifierMapping(selectedChoices.getNumberOfSetBits()); diff --git a/src/storm/storage/sparse/ChoiceOrigins.h b/src/storm/storage/sparse/ChoiceOrigins.h index 902fdd031..afc85faf3 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.h +++ b/src/storm/storage/sparse/ChoiceOrigins.h @@ -5,6 +5,7 @@ #include "storm/storage/BitVector.h" #include "storm/models/sparse/ChoiceLabeling.h" +#include "storm/adapters/JsonAdapter.h" namespace storm { namespace storage { @@ -19,6 +20,7 @@ namespace storm { */ class ChoiceOrigins { public: + typedef storm::json Json; virtual ~ChoiceOrigins() = default; @@ -63,6 +65,16 @@ namespace storm { */ std::string const& getChoiceInfo(uint_fast64_t choiceIndex) const; + /* + * Returns the information for the given choice origin identifier as a (human readable) string + */ + Json const& getIdentifierAsJson(uint_fast64_t identifier) const; + + /* + * Returns the choice origin information as a (human readable) string. + */ + Json const& getChoiceAsJson(uint_fast64_t choiceIndex) const; + /* * Derive new choice origins from this by selecting the given choices. */ @@ -95,10 +107,18 @@ namespace storm { */ virtual void computeIdentifierInfos() const = 0; + /* + * Computes the identifier infos (i.e., human readable strings representing the choice origins). + */ + virtual void computeIdentifierJson() const = 0; + std::vector indexToIdentifier; // cached identifier infos might be empty if identifiers have not been generated yet. mutable std::vector identifierToInfo; + + // cached identifier infos might be empty if identifiers have not been generated yet. + mutable std::vector identifierToJson; }; } diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.cpp b/src/storm/storage/sparse/JaniChoiceOrigins.cpp index c4d1c365b..8063142a7 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.cpp +++ b/src/storm/storage/sparse/JaniChoiceOrigins.cpp @@ -1,6 +1,7 @@ #include "storm/storage/sparse/JaniChoiceOrigins.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/JSONExporter.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -52,6 +53,32 @@ namespace storm { } } + void JaniChoiceOrigins::computeIdentifierJson() const { + this->identifierToJson.clear(); + this->identifierToJson.reserve(this->getNumberOfIdentifiers()); + for (auto const& set : identifierToEdgeIndexSet) { + Json setJson; + if (set.empty()) { + setJson = "No origin"; + } else { + bool first = true; + std::vector edgesJson; + for (auto const& edgeIndex : set) { + auto autAndEdgeOffset = model->decodeAutomatonAndEdgeIndices(edgeIndex); + auto const& automaton = model->getAutomaton(autAndEdgeOffset.first); + auto const& edge = automaton.getEdge(autAndEdgeOffset.second); + if (first) { + setJson["action-label"] = model->getAction(edge.getActionIndex()).getName(); + first = false; + } + edgesJson.push_back(storm::jani::JsonExporter::getEdgeAsJson(*model, autAndEdgeOffset.first, autAndEdgeOffset.second)); + edgesJson.back()["automaton"] = automaton.getName(); + } + setJson["transitions"] = std::move(edgesJson); + } + this->identifierToJson.push_back(std::move(setJson)); + } + } } } } diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.h b/src/storm/storage/sparse/JaniChoiceOrigins.h index 93698a0f0..5ee1aa69b 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.h +++ b/src/storm/storage/sparse/JaniChoiceOrigins.h @@ -59,6 +59,11 @@ namespace storm { */ virtual void computeIdentifierInfos() const override; + /* + * Computes the identifier infos as json (i.e., a machine readable representation of the choice origins). + */ + virtual void computeIdentifierJson() const override; + std::shared_ptr model; std::vector identifierToEdgeIndexSet; }; diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.cpp b/src/storm/storage/sparse/PrismChoiceOrigins.cpp index 69084f8cd..5084b58d7 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.cpp +++ b/src/storm/storage/sparse/PrismChoiceOrigins.cpp @@ -108,6 +108,54 @@ namespace storm { STORM_LOG_DEBUG("Generated the following names for the choice origins: " << storm::utility::vector::toString(this->identifierToInfo)); STORM_LOG_ASSERT(storm::utility::vector::isUnique(this->identifierToInfo), "The generated names for the prism choice origins are not unique."); } + + void PrismChoiceOrigins::computeIdentifierJson() const { + this->identifierToJson.clear(); + this->identifierToJson.reserve(this->getNumberOfIdentifiers()); + for (CommandSet const& set : identifierToCommandSet) { + // Get a string representation of this command set. + Json setJson; + if (set.empty()) { + setJson = "No origin"; + } else { + bool first = true; + std::vector commandsJson; + for (auto const& commandIndex : set) { + Json commandJson; + auto moduleCommandPair = program->getModuleCommandIndexByGlobalCommandIndex(commandIndex); + storm::prism::Module const& module = program->getModule(moduleCommandPair.first); + storm::prism::Command const& command = module.getCommand(moduleCommandPair.second); + if (first) { + setJson["action-label"] = command.getActionName(); + first = false; + } + commandJson["module"] = module.getName(); + commandJson["guard"] = command.getGuardExpression().toString(); + std::vector updatesJson; + for (auto const& update : command.getUpdates()) { + Json updateJson; + updateJson["prob"] = update.getLikelihoodExpression().toString(); + std::stringstream assignmentsString; + bool firstAssignment = true; + for (auto const& a : update.getAssignments()) { + if (firstAssignment) { + firstAssignment = false; + } else { + assignmentsString << " & "; + } + assignmentsString << a; + } + updateJson["result"] = assignmentsString.str(); + updatesJson.push_back(std::move(updateJson)); + } + commandJson["updates"] = updatesJson; + commandsJson.push_back(std::move(commandJson)); + } + setJson["transitions"] = commandsJson; + } + this->identifierToJson.push_back(std::move(setJson)); + } + } } } } diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.h b/src/storm/storage/sparse/PrismChoiceOrigins.h index 06ff3c584..05567a644 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.h +++ b/src/storm/storage/sparse/PrismChoiceOrigins.h @@ -62,6 +62,11 @@ namespace storm { */ virtual void computeIdentifierInfos() const override; + /* + * Computes the identifier infos as json (i.e., a machine readable representation of the choice origins). + */ + virtual void computeIdentifierJson() const override; + std::shared_ptr program; std::vector identifierToCommandSet; }; diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 413e93302..4fd5487c5 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -552,7 +552,9 @@ namespace storm { // set an arbitrary (valid) choice for the psi states. for (auto const& psiState : psiStates) { for (uint_fast64_t memState = 0; memState < scheduler.getNumberOfMemoryStates(); ++memState) { - scheduler.setChoice(0, psiState, memState); + if (!scheduler.getChoice(psiState, memState).isDefined()) { + scheduler.setChoice(0, psiState, memState); + } } } diff --git a/src/storm/utility/random.cpp b/src/storm/utility/random.cpp new file mode 100644 index 000000000..6f3464cdb --- /dev/null +++ b/src/storm/utility/random.cpp @@ -0,0 +1,24 @@ +#include "storm/utility/random.h" + +namespace storm { + namespace utility { + RandomProbabilityGenerator::RandomProbabilityGenerator() + : distribution(0.0, 1.0) + { + std::random_device rd; + engine = std::mt19937(rd()); + } + + RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) + : engine(seed), distribution(0.0, 1.0) + { + + } + + double RandomProbabilityGenerator::random() { + return distribution(engine); + } + + + } +} \ No newline at end of file diff --git a/src/storm/utility/random.h b/src/storm/utility/random.h new file mode 100644 index 000000000..ef5b359df --- /dev/null +++ b/src/storm/utility/random.h @@ -0,0 +1,29 @@ +#include + +namespace storm { + namespace utility { + template + class RandomProbabilityGenerator { + public: + RandomProbabilityGenerator(); + RandomProbabilityGenerator(uint64_t seed); + ValueType random() const; + + }; + + template<> + class RandomProbabilityGenerator { + public: + RandomProbabilityGenerator(); + RandomProbabilityGenerator(uint64_t seed); + double random(); + private: + std::uniform_real_distribution distribution; + std::mt19937 engine; + + }; + + + + } +} \ No newline at end of file