diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 6de3d079d..641882d27 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -144,7 +144,7 @@ namespace storm { modelDot.close(); } - storm::modelchecker::helper::SparseLTLHelper helper(embeddedMdp.getTransitionMatrix(), this->getModel().getNumberOfStates()); + storm::modelchecker::helper::SparseLTLHelper helper(embeddedMdp.getTransitionMatrix(), embeddedMdp.getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, embeddedMdp); // Compute Satisfaction sets for APs diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index d80f4a64f..8a59e5252 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -1,8 +1,5 @@ -#include -#include #include "SparseLTLHelper.h" -#include "storm/transformer/DAProductBuilder.h" #include "storm/automata/LTL2DeterministicAutomaton.h" #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" @@ -10,6 +7,8 @@ #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/storage/MaximalEndComponentDecomposition.h" +#include "storm/storage/memorystructure/MemoryStructure.h" +#include "storm/storage/memorystructure/MemoryStructureBuilder.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/DebugSettings.h" @@ -22,10 +21,59 @@ namespace storm { namespace helper { template - SparseLTLHelper::SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix, std::size_t numberOfStates) : _transitionMatrix(transitionMatrix), _numberOfStates(numberOfStates) { + SparseLTLHelper::SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix, std::size_t numberOfStates) : _transitionMatrix(transitionMatrix), _numberOfStates(numberOfStates){ // Intentionally left empty. } + + template + storm::storage::Scheduler SparseLTLHelper::SparseLTLHelper::extractScheduler(storm::models::sparse::Model const& model) { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); + STORM_LOG_ASSERT(this->_productChoices.is_initialized(), "Trying to extract the produced scheduler but none is available. Was there a computation call before?"); + STORM_LOG_ASSERT(this->_memoryTransitions.is_initialized(), "Trying to extract the DA transition structure but none is available. Was there a computation call before?"); + STORM_LOG_ASSERT(this->_memoryInitialStates.is_initialized(), "Trying to extract the initial states of the DA but there are none available. Was there a computation call before?"); + + // Create a memory structure for the MDP scheduler with memory. + typename storm::storage::MemoryStructureBuilder::MemoryStructureBuilder memoryBuilder(this->_memoryTransitions.get().size(), model); + + // Build the transitions between the memory states: startState--- modelStates (transitionVector) --->goalState + for (storm::storage::sparse::state_type startState = 0; startState < this->_memoryTransitions.get().size(); ++startState) { + for (storm::storage::sparse::state_type goalState = 0; goalState < this->_memoryTransitions.get().size(); ++goalState) { + // Bitvector that represents modelStates the model states that trigger this transition. + memoryBuilder.setTransition(startState, goalState, this->_memoryTransitions.get()[startState][goalState]); + } + } + + /* + memoryStateLabeling: Label the memory states to specify, e.g., accepting states // TODO where are these labels used? + for (storm::storage::sparse::state_type q : set) { + memoryBuilder.setLabel(q,//todo); + } + */ + + // initialMemoryStates: Assign an initial memory state to each initial state of the model. + for (uint_fast64_t s0 : model.getInitialStates()) { + // Label the state as initial TODO unnecessary? + //memoryBuilder.setLabel(q, "Initial for model state " s0) + memoryBuilder.setInitialMemoryState(s0, this->_memoryInitialStates.get()[s0]); + } + + + // Finally, we can build the memoryStructure. + storm::storage::MemoryStructure memoryStructure = memoryBuilder.build(); + + // Create a scheduler (with memory of size DA) for the model from the scheduler of the MDP-DA-product model. + storm::storage::Scheduler scheduler(this->_transitionMatrix.getRowGroupCount(), memoryStructure); + + // Use choices in the product model to create a choice based on model state and memory state + for (const auto &choice : this->_productChoices.get()) { + uint_fast64_t modelState = choice.first.first; + uint_fast64_t memoryState = choice.first.second; + scheduler.setChoice(choice.second, modelState, memoryState); + } + + return scheduler; + } template std::map SparseLTLHelper::computeApSets(std::map> const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker){ std::map apSets; @@ -141,7 +189,10 @@ namespace storm { if (accepting) { accMECs++; STORM_LOG_DEBUG("MEC is accepting"); + for (auto const& stateChoicePair : mec) { + // TODO extend scheduler by mec choices (which?) + // need adversary which forces (to remain in mec and) to visit all states of the mec inf. often with prob. 1 acceptingStates.set(stateChoicePair.first); } } @@ -180,12 +231,13 @@ namespace storm { std::vector SparseLTLHelper::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets) { const storm::automata::APSet& apSet = da.getAPSet(); - std::vector apLabels; + + std::vector statesForAP; for (const std::string& ap : apSet.getAPs()) { auto it = apSatSets.find(ap); STORM_LOG_THROW(it != apSatSets.end(), storm::exceptions::InvalidOperationException, "Deterministic automaton has AP " << ap << ", does not appear in formula"); - apLabels.push_back(std::move(it->second)); + statesForAP.push_back(std::move(it->second)); } storm::storage::BitVector statesOfInterest; @@ -199,9 +251,10 @@ namespace storm { STORM_LOG_INFO("Building "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +"product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states..."); - storm::transformer::DAProductBuilder productBuilder(da, apLabels); + transformer::DAProductBuilder productBuilder(da, statesForAP); + + typename transformer::DAProduct::ptr product = productBuilder.build(this->_transitionMatrix, statesOfInterest); - auto product = productBuilder.build(this->_transitionMatrix, statesOfInterest); STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +" has " << product->getProductModel().getNumberOfStates() << " states and " << product->getProductModel().getNumberOfTransitions() << " transitions."); @@ -254,15 +307,56 @@ namespace storm { if (Nondeterministic) { - prodNumericResult = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, - std::move(solveGoalProduct), - product->getProductModel().getTransitionMatrix(), - product->getProductModel().getBackwardTransitions(), - bvTrue, - acceptingStates, - this->isQualitativeSet(), - false // no schedulers (at the moment) - ).values); + MDPSparseModelCheckingHelperReturnType prodCheckResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, + std::move(solveGoalProduct), + product->getProductModel().getTransitionMatrix(), + product->getProductModel().getBackwardTransitions(), + bvTrue, + acceptingStates, + this->isQualitativeSet(), + this->isProduceSchedulerSet() // Whether to create memoryless scheduler for the Model-DA Product. + ); + prodNumericResult = std::move(prodCheckResult.values); + + if (this->isProduceSchedulerSet()) { + // Extract the choices of the scheduler for the MDP-DA product: -> choice + this->_productChoices.emplace(); + for (storm::storage::sparse::state_type pState = 0; + pState < product->getProductModel().getNumberOfStates(); ++pState) { + this->_productChoices.get().insert({std::make_pair(product->getModelState(pState), product->getAutomatonState(pState)), prodCheckResult.scheduler->getChoice(pState)}); + } + + + // Prepare the memory structure. For that, we need: transitions, initialMemoryStates (and todo: memoryStateLabeling) + + // The next move function of the memory, will be build based on the transitions of the DA. + this->_memoryTransitions.emplace(da.getNumberOfStates(), std::vector(da.getNumberOfStates())); + + for (storm::storage::sparse::state_type startState = 0; startState < da.getNumberOfStates(); ++startState) { + for (storm::storage::sparse::state_type goalState = 0; + goalState < da.getNumberOfStates(); ++goalState) { + // Bitvector that represents modelStates the model states that trigger this transition. + storm::storage::BitVector modelStates(this->_transitionMatrix.getRowGroupCount(), false); + for (storm::storage::sparse::state_type modelState = 0; + modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { + if (goalState == productBuilder.getSuccessor(modelState, startState, modelState)) { + modelStates.set(modelState); + } + } + // Insert a transition: startState--{modelStates}-->goalState + this->_memoryTransitions.get()[startState][goalState] = std::move(modelStates); + } + } + + this->_memoryInitialStates.emplace(); + this->_memoryInitialStates->resize(this->_transitionMatrix.getRowGroupCount()); + // Save for each automaton state for which model state it is initial. + for (storm::storage::sparse::state_type modelState = 0; modelState< this->_transitionMatrix.getRowGroupCount(); ++modelState) { + this->_memoryInitialStates.get().at(modelState) = productBuilder.getInitialState(modelState); + } + + // TODO labels (e.g. the accepting set?) for the automaton states + } } else { prodNumericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(env, @@ -275,6 +369,7 @@ namespace storm { } std::vector numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult); + return numericResult; } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index c5e2a9c33..3df887979 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -1,10 +1,12 @@ #include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/automata/DeterministicAutomaton.h" #include "storm/storage/SparseMatrix.h" #include "storm/solver/SolveGoal.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/logic/ExtractMaximalStateFormulasVisitor.h" +#include "storm/transformer/DAProductBuilder.h" namespace storm { @@ -34,6 +36,14 @@ namespace storm { */ SparseLTLHelper(storm::storage::SparseMatrix const& transitionMatrix, std::size_t numberOfSates); + + /*! + * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. + * @param TODO + * @return a new scheduler containing optimal choices for each state that yield the long run average values of the most recent call. + */ + storm::storage::Scheduler extractScheduler(storm::models::sparse::Model const& model); + /*! * todo computes Sat sets of AP * @param @@ -73,18 +83,23 @@ namespace storm { * @param the transition matrix of the model * @param the reversed transition relation */ - static storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions); + storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions); /** * Compute a set S of states that are contained in BSCCs that satisfy the given acceptance conditon. * @tparam the acceptance condition * @tparam the transition matrix of the model */ - static storm::storage::BitVector computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix); + storm::storage::BitVector computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix); storm::storage::SparseMatrix const& _transitionMatrix; - std::size_t _numberOfStates; + std::size_t _numberOfStates; //TODO just use _transitionMatrix.getRowGroupCount instead? + + // scheduler + boost::optional, storm::storage::SchedulerChoice>> _productChoices; // --> choice + boost::optional>> _memoryTransitions; // BitVector contains the model states that lead from startState to goalSate of teh DA + boost::optional> _memoryInitialStates; // Saves for each modelState which automaton state is reached from the initial state //TODO improve }; } diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index cd2422f2b..2e14c8fdb 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -164,7 +164,7 @@ namespace storm { modelDot.close(); } - storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates()); + storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix(), dtmc.getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); // Compute Satisfaction sets for APs diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 934517663..1d68b1d1f 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -14,9 +14,7 @@ #include "storm/logic/FragmentSpecification.h" -#include "storm/transformer/DAProductBuilder.h" #include "storm/logic/ExtractMaximalStateFormulasVisitor.h" -#include "storm/automata/LTL2DeterministicAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -199,6 +197,7 @@ namespace storm { modelDot.close(); } + storm::modelchecker::helper::SparseLTLHelper helper(mdp.getTransitionMatrix(), mdp.getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, mdp); @@ -208,7 +207,13 @@ namespace storm { std::vector numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + //TODO for MA too + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler(mdp))); + } + + return result; } template diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index aaea5b7c1..97741d709 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -19,10 +19,6 @@ namespace storm { // fwd class Environment; - namespace automata { - class DeterministicAutomaton; - } - namespace models { namespace sparse { template class Dtmc; diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 0582fdd76..1c3d6c895 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -224,6 +224,10 @@ namespace storm { out << "Skipped " << numOfSkippedStatesWithUniqueChoice << " deterministic states with unique choice." << std::endl; } out << "___________________________________________________________________" << std::endl; + + // TODO only for tests: + out << memoryStructure->toString(); + out << std::endl; } template <> diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 029387288..31708544d 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -288,7 +288,7 @@ namespace storm { uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); - } + } //TODO successor MemoryState is a problem here 8382838738483264 oder so } else { std::map transitions; for (auto const& choiceIndex : choice.getChoiceAsDistribution()) { diff --git a/src/storm/transformer/DAProductBuilder.h b/src/storm/transformer/DAProductBuilder.h index a6a53f9bd..7c882b3e8 100644 --- a/src/storm/transformer/DAProductBuilder.h +++ b/src/storm/transformer/DAProductBuilder.h @@ -35,7 +35,7 @@ namespace storm { return da.getSuccessor(da.getInitialState(), getLabelForState(modelState)); } - storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type modelFrom, + storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type modelFrom, //TODO delete modelFrom? storm::storage::sparse::state_type automatonFrom, storm::storage::sparse::state_type modelTo) const { return da.getSuccessor(automatonFrom, getLabelForState(modelTo)); diff --git a/src/storm/transformer/ProductBuilder.h b/src/storm/transformer/ProductBuilder.h index a82bd2839..a398a1811 100644 --- a/src/storm/transformer/ProductBuilder.h +++ b/src/storm/transformer/ProductBuilder.h @@ -33,7 +33,6 @@ namespace storm { // use of the SparseMatrixBuilder that can only handle linear addNextValue // calls std::deque todo; - for (state_type s_0 : statesOfInterest) { state_type q_0 = prodOp.getInitialState(s_0); diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index dbea6504d..a1844888b 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -173,6 +173,7 @@ namespace { EXPECT_TRUE(scheduler.isDeterministicScheduler()); EXPECT_TRUE(scheduler.isMemorylessScheduler()); EXPECT_TRUE(!scheduler.isPartialScheduler()); + auto inducedModel = mdp->applyScheduler(scheduler); ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); auto const& inducedMdp = inducedModel->template as>(); @@ -201,5 +202,57 @@ namespace { EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], this->env().solver().lra().getPrecision()); } } + + TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl) { + typedef typename TestFixture::ValueType ValueType; + + std::string formulasString = "Pmax=? [X X \"target\"]; Pmin=? [G F \"target\"];"; + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString); + auto mdp = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(4ull, mdp->getNumberOfStates()); + EXPECT_EQ(11ull, mdp->getNumberOfTransitions()); + ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp); + EXPECT_EQ(7ull, mdp->getNumberOfChoices()); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); + + { + auto result = checker.check(this->env(), tasks[0]); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + + EXPECT_TRUE(scheduler.isDeterministicScheduler()); + EXPECT_TRUE(! scheduler.isMemorylessScheduler()); + EXPECT_TRUE(scheduler.isPartialScheduler()); + auto inducedModel = mdp->applyScheduler(scheduler); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); + auto const& inducedMdp = inducedModel->template as>(); + EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + auto inducedResult = inducedChecker.check(this->env(), tasks[0]); + ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("9/10"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + } + { + auto result = checker.check(this->env(), tasks[1]); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + + EXPECT_TRUE(scheduler.isDeterministicScheduler()); + EXPECT_TRUE(!scheduler.isMemorylessScheduler()); + EXPECT_TRUE(scheduler.isPartialScheduler()); + auto inducedModel = mdp->applyScheduler(scheduler); + ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); + auto const& inducedMdp = inducedModel->template as>(); + EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates()); + storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); + auto inducedResult = inducedChecker.check(this->env(), tasks[1]); + ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::settings::getModule().getPrecision()); + } + } } \ No newline at end of file