sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

updated LTL-scheduler

tempestpy_adaptions
hannah 3 years ago
committed by Stefan Pranger
parent
0983f2f564
commit
93c2e92c2a
6 changed files with 278 additions and 74 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 223
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
  2. 17
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
  3. 2
      src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
  4. 8
      src/storm/transformer/Product.h
  5. 9
      src/storm/utility/graph.cpp
  6. 93
      src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

223
src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
View File

@ -16,6 +16,8 @@
#include "storm/environment/modelchecker/ModelCheckerEnvironment.h"
#include "storm/utility/graph.h"
namespace storm {
namespace modelchecker {
namespace helper {
@ -30,9 +32,12 @@ namespace storm {
storm::storage::Scheduler<ValueType> SparseLTLHelper<ValueType, Nondeterministic>::SparseLTLHelper::extractScheduler(storm::models::sparse::Model<ValueType> 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?");
// TODO fails for No accepting states, skipping probability computation.
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<ValueType>::MemoryStructureBuilder memoryBuilder(this->_memoryTransitions.get().size(), model);
@ -44,36 +49,36 @@ namespace storm {
}
}
/*
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.
// Now, 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.
// Create a scheduler (with memory) for the model from the REACH and MEC scheduler of the MDP-DA-product model.
storm::storage::Scheduler<ValueType> 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;
// <s, q, MEC, InfSet> -> choice
storm::storage::sparse::state_type modelState = std::get<0>(choice.first);
storm::storage::sparse::state_type automatonState = std::get<1>(choice.first);
uint_fast64_t mec = std::get<2>(choice.first);
uint_fast64_t infSet = std::get<3>(choice.first);
// Encode as memory state
uint_fast64_t memoryState = (((infSet * _mecStatesInfSets.get().size()) + mec) * _numberOfDaStates.get()) + automatonState;
scheduler.setChoice(choice.second, modelState, memoryState);
}
// TODO set non-reachable (modelState,memoryState)-Pairs (i.e. those that are not contained in _productChoices) to "unreachable", (extend Scheduler by something like std::vector<std::Bitvector>> reachableSchedulerChoices; und isChoiceReachable(..))
// TODO
// set non-reachable (modelState,memoryState)-Pairs (i.e. those that are not contained in _productChoices) to "unreachable", (extend Scheduler by something like std::vector<std::Bitvector>> reachableSchedulerChoices; und isChoiceReachable(..))
// Sanity check for created scheduler.
STORM_LOG_ASSERT(scheduler.isDeterministicScheduler(), "Expected a deterministic scheduler");
return scheduler;
}
template<typename ValueType, bool Nondeterministic>
@ -95,7 +100,7 @@ namespace storm {
template <typename ValueType, bool Nondeterministic>
storm::storage::BitVector SparseLTLHelper<ValueType, Nondeterministic>::computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
storm::storage::BitVector SparseLTLHelper<ValueType, Nondeterministic>::computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, typename transformer::DAProduct<productModelType>::ptr product) {
STORM_LOG_INFO("Computing accepting states for acceptance condition " << *acceptance.getAcceptanceExpression());
if (acceptance.getAcceptanceExpression()->isTRUE()) {
STORM_LOG_INFO(" TRUE -> all states accepting (assumes no deadlock in the model)");
@ -112,6 +117,14 @@ namespace storm {
std::size_t accMECs = 0;
std::size_t allMECs = 0;
std::size_t i = 0;
if (this->isProduceSchedulerSet()) {
_mecStatesInfSets.emplace();
_productChoices.emplace();
}
// Save the states that are already assigned a scheduler (MEC), a state is assigned to the first MEC we find.
storm::storage::BitVector finishedStates(transitionMatrix.getRowGroupCount(), false);
for (auto const& conjunction : dnf) {
// determine the set of states of the subMDP that can satisfy the condition
// => remove all states that would violate Fins in the conjunction
@ -153,12 +166,16 @@ namespace storm {
storm::storage::MaximalEndComponentDecomposition<ValueType> mecs(transitionMatrix, backwardTransitions, allowed);
allMECs += mecs.size();
for (const auto& mec : mecs) {
// Save the accSets that need to be visited inf often to satisfy a specific accepting MEC.
std::vector<storm::storage::BitVector> infSets = std::vector<storm::storage::BitVector>();
STORM_LOG_DEBUG("Inspect MEC: " << mec);
bool accepting = true;
for (auto const& literal : conjunction) {
if (literal->isTRUE()) {
// skip
} else if (literal->isFALSE()) {
accepting = false;
break;
@ -173,6 +190,11 @@ namespace storm {
accepting = false;
break;
}
if (this->isProduceSchedulerSet()) {
infSets.emplace_back(~accSet);
}
} else {
STORM_LOG_DEBUG("Checking against " << accSet);
if (!mec.containsAnyState(accSet)) {
@ -180,7 +202,11 @@ namespace storm {
accepting = false;
break;
}
if (this->isProduceSchedulerSet()) {
infSets.emplace_back(accSet);
}
}
} else if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) {
// do only sanity checks here
STORM_LOG_ASSERT(atom.isNegated() ? !mec.containsAnyState(~accSet) : !mec.containsAnyState(accSet), "MEC contains Fin-states, which should have been removed");
@ -192,14 +218,69 @@ namespace storm {
accMECs++;
STORM_LOG_DEBUG("MEC is accepting");
for (auto const& stateChoicePair : mec) {
for (auto const &stateChoicePair : mec) {
acceptingStates.set(stateChoicePair.first);
}
if (this->isProduceSchedulerSet()) {
storm::storage::BitVector mecStates(transitionMatrix.getRowGroupCount(), false);
for (auto const &stateChoicePair : mec) {
mecStates.set(stateChoicePair.first);
}
// If there are no InfSets (either all TRUE or only FIN in conjunction)
if (infSets.empty()) {
// We want to visit some states of this MEC inf. often
infSets.emplace_back(mecStates);
}
// Save the states of this MEC (that are not contained in any other MEC yet) and the InfSets need to be visited inf. often to sat. the acc. cond.
_mecStatesInfSets.get().insert({accMECs, std::make_pair(mecStates & ~finishedStates, infSets)});
// Define scheduler choices for the states in this MEC (that are not in any other MEC)
for (uint_fast64_t infSet = 0; infSet < infSets.size(); ++infSet) {
// Scheduler that satisfies the MEC acceptance condition (visit each InfSet inf often, or switch to scheduler of another MEC)
storm::storage::Scheduler<ValueType> mecScheduler(
transitionMatrix.getRowGroupCount());
// Compute a scheduler that, with prob=1, reaches the infSet via mecStates starting from states that are not yet in other MEC
storm::utility::graph::computeSchedulerProb1E<ValueType>(_mecStatesInfSets.get()[accMECs].first, transitionMatrix, backwardTransitions, mecStates, _mecStatesInfSets.get()[accMECs].second[infSet], mecScheduler);
// Prob1E sets an arbitrary choice for the psi states, but we want to stay in this accepting mec.
for (auto pState : (_mecStatesInfSets.get()[accMECs].first & _mecStatesInfSets.get()[accMECs].second[infSet])) {
// If we are in the InfSet, we stay in mec-states
// TODO is this correct:
// (*std::next(mec.getChoicesForState(pState).begin(), 0))
mecScheduler.setChoice(storm::storage::SchedulerChoice<ValueType>((*std::next(mec.getChoicesForState(pState).begin()), 0)), pState);
}
// Extract scheduler choices (only for states that are already assigned a scheduler, i.e are in another MEC)
for (auto pState : _mecStatesInfSets.get()[accMECs].first) {
//if (!_mecStatesInfSets.get()[accMECs].second[infSet].get(pState)) {
// We want to reach the InfSet, save choice: <s, q, MEC, InfSet> ---> choice
// TODO find test that fails, when ignoring these:
this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState),product->getAutomatonState(pState), accMECs, infSet), mecScheduler.getChoice(pState)});
}
}
// The states in this MEC will not be reassigned
finishedStates = finishedStates | mecStates;
}
}
}
}
if (this->isProduceSchedulerSet()) {
// Remaining states belong to no mec (REACH scheduler is computed later)
_mecStatesInfSets.get()[0] = std::make_pair(~finishedStates,std::vector<storm::storage::BitVector>(1,~finishedStates));
}
STORM_LOG_DEBUG("Accepting states: " << acceptingStates);
STORM_LOG_INFO("Found " << acceptingStates.getNumberOfSetBits() << " states in " << accMECs << " accepting MECs (considered " << allMECs << " MECs).");
@ -209,7 +290,6 @@ namespace storm {
template <typename ValueType, bool Nondeterministic>
storm::storage::BitVector SparseLTLHelper<ValueType, Nondeterministic>::computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix) {
storm::storage::StronglyConnectedComponentDecomposition<ValueType> bottomSccs(transitionMatrix, storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs());
//storm::storage::BitVector acceptingStates = storm::storage::BitVector(product->getProductModel().getNumberOfStates());
storm::storage::BitVector acceptingStates(transitionMatrix.getRowGroupCount(), false);
std::size_t checkedBSCCs = 0, acceptingBSCCs = 0, acceptingBSCCStates = 0;
@ -275,9 +355,9 @@ namespace storm {
storm::storage::BitVector acceptingStates;
if (Nondeterministic) {
STORM_LOG_INFO("Computing MECs and checking for acceptance...");
acceptingStates = computeAcceptingECs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions());
acceptingStates = computeAcceptingECs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions(), product); //TODO product is only needed for ->getModelState(pState) and DAStates for scheduler creation (maybe lambda instead)
} else {
} else {
STORM_LOG_INFO("Computing BSCCs and checking for acceptance...");
acceptingStates = computeAcceptingBCCs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix());
@ -318,44 +398,101 @@ namespace storm {
);
prodNumericResult = std::move(prodCheckResult.values);
if (this->isProduceSchedulerSet()) {
// Extract the choices of the scheduler for the MDP-DA product: <s,q> -> choice
this->_productChoices.emplace();
if (this->isProduceSchedulerSet()) { // TODO create fct for this
_numberOfDaStates = da.getNumberOfStates();
// TODO asserts _mecStatesInfSets initialized etc.
// Extract the choices of the REACH-scheduler (choices to reach an acc. MEC) for the MDP-DA product: <s,q> -> choice
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)});
// <s,q, NoMec, 0> ---> choice
if(! acceptingStates.get(pState)){
// Do not overwrite choices of states in an accepting MEC
this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), 0, 0), prodCheckResult.scheduler->getChoice(pState)});
}
}
// Prepare the memory structure. For that, we need: transitions, initialMemoryStates (and memoryStateLabeling)
// Prepare the memory structure. For that, we need: transitions, initialMemoryStates (and todo: memoryStateLabeling)
// Compute size of the resulting memory structure: a state corresponds to <q <mec, infSet>> encoded as (((infSet * |mecs|) + mec) * |DAStates|) +q
uint64 numCopies =0;
for (auto const& mec: _mecStatesInfSets.get()) {
numCopies += mec.second.second.size();
}
uint64 numMemoryStates = numCopies * _mecStatesInfSets.get().size() * da.getNumberOfStates() + da.getNumberOfStates(); //TODO is this correct
// The next move function of the memory, will be build based on the transitions of the DA.
this->_memoryTransitions.emplace(da.getNumberOfStates(), std::vector<storm::storage::BitVector>(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)) { //todo remove first parameter
modelStates.set(modelState);
this->_memoryTransitions.emplace(numMemoryStates, std::vector<storm::storage::BitVector>(numMemoryStates, storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), false)));
for (storm::storage::sparse::state_type automatonFrom = 0; automatonFrom < da.getNumberOfStates(); ++automatonFrom) {
for (storm::storage::sparse::state_type automatonTo = 0; automatonTo < da.getNumberOfStates(); ++automatonTo) {
// Find the modelStates that trigger this transition.
for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) {
if(!product->isValidProductState(modelState, automatonTo)) {
// Memory state successor of the modelState-transition emanating <automatonFrom, ?, ? > not defined/reachable.
// TODO save as unreachable in scheduler
// STORM_PRINT("set to unreachable : (" << modelState <<" , " << automatonTo <<")");
} else if (automatonTo == productBuilder.getSuccessor(modelState, automatonFrom, modelState)) { //TODO remove first parameter of getSuccessor
// Add the modelState to one outgoing transition of all states of the form <automatonFrom <mec, InfSet>> (mec=0 equals NoMec)
for (uint_fast64_t mec = 0; mec < _mecStatesInfSets.get().size(); ++mec) {
for (uint_fast64_t infSet = 0; infSet < _mecStatesInfSets.get()[mec].second.size(); ++infSet) {
// Find the goalState <automatonTo <mec', InfSet'>>, where <modelState, automatonTo> is in mec'.
if (_mecStatesInfSets.get()[mec].first.get(product->getProductStateIndex(modelState, automatonTo))) {
// <modelState, automatonTo> in contained in this MEC. Now check if we have reached the current InfSet.
if(_mecStatesInfSets.get()[mec].second[infSet].get(product->getProductStateIndex(modelState, automatonTo))){
// InfSet satisfied: Add modelState to the transition from <automatonFrom <mec, InfSet>> to <automatonTo, <mec, NextInfSet>>.
uint64 from = (((infSet * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonFrom;
uint64 to = ((((infSet+1 < _mecStatesInfSets.get()[mec].second.size() ? infSet+1 : 0) * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonTo;
_memoryTransitions.get()[from][to].set(modelState);
} else {
// InfSet not satisfied: Add modelState to the transition from <automatonFrom <mec, InfSet>> to <automatonTo, <mec, InfSet>>.
uint64 from = (((infSet * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonFrom;
uint64 to = (((infSet * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonTo;
_memoryTransitions.get()[from][to].set(modelState);
}
} else {
// We need to find the unique MEC containing <modelState, automatonTo> and start in InfSet 0.
for (uint_fast64_t nextMec = 0; nextMec < _mecStatesInfSets.get().size(); ++nextMec) {
if (_mecStatesInfSets.get()[nextMec].first.get(product->getProductStateIndex(modelState, automatonTo))) {
// Add modelState to the transition from <automatonFrom <mec, InfSet>> to <automatonTo, nextMec, InfSet>>
uint64 from = (((infSet * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonFrom;
uint64 to = (((0 * _mecStatesInfSets.get().size()) + nextMec) * da.getNumberOfStates()) + automatonTo;
_memoryTransitions.get()[from][to].set(modelState);
break; // Can stop, because the state is only contained in one MEC.
}
}
}
}
}
}
}
// Insert a transition: startState--{modelStates}-->goalState
this->_memoryTransitions.get()[startState][goalState] = std::move(modelStates);
}
}
// Finished creation of transitions.
// Find initial memory states
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);
}
// Save for each relevant model state its initial memory state (get the s-successor of q0)
for (storm::storage::sparse::state_type modelState : statesOfInterest) {
storm::storage::sparse::state_type automatonInit = productBuilder.getInitialState(modelState);
STORM_LOG_ASSERT(product->isValidProductState(modelState, automatonInit), "The memory successor state for the model state "<< modelState << "does not exist in the DA-Model Product.");
// Search mec which contains <automatonInit, modelState>
for (uint_fast64_t mec = 0; mec < _mecStatesInfSets.get().size(); ++mec) {
if (_mecStatesInfSets.get()[mec].first.get(product->getProductStateIndex(modelState, automatonInit))) {
this->_memoryInitialStates.get().at(modelState) = (((0 * _mecStatesInfSets.get().size()) + mec) * da.getNumberOfStates()) + automatonInit;
break;
}
}
// TODO labels (e.g. the accepting set?) for the automaton states
}
// Finished creation of initial states.
}
} else {

17
src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
View File

@ -83,7 +83,7 @@ namespace storm {
* @param the transition matrix of the model
* @param the reversed transition relation
*/
storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, typename transformer::DAProduct<productModelType>::ptr product);
/**
* Compute a set S of states that are contained in BSCCs that satisfy the given acceptance conditon.
@ -96,14 +96,13 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
std::size_t _numberOfStates; //TODO just use _transitionMatrix.getRowGroupCount instead?
// REACH scheduler
boost::optional<std::map<std::pair<uint_fast64_t, uint_fast64_t>, storm::storage::SchedulerChoice<ValueType>>> _productChoices; // <s, q> --> choice
boost::optional<std::vector<std::vector<storm::storage::BitVector>>> _memoryTransitions; // BitVector contains the model states that lead from startState to goalSate of the DA
boost::optional<std::vector<uint_fast64_t>> _memoryInitialStates; // Saves for each modelState which automaton state is reached from the initial state //TODO improve
// MEC scheduler
boost::optional<std::map <std::pair<uint_fast64_t,std::pair<uint_fast64_t, uint_fast64_t>> , storm::storage::SchedulerChoice<ValueType>>> _mecProductChoices; // <#literal, <s, daState>> ---> choice
boost::optional<std::vector<std::vector<storm::storage::BitVector>>> _mecMemoryTransitions; // BitVector contains the model states that lead from #INF(i) to #INF(i+1) of the AccCondition (#INF(1) AND #INF(2) ....) OR (..)
// REACH scheduler and MEC scheduler
boost::optional<std::map <std::tuple<uint_fast64_t, uint_fast64_t, uint_fast64_t, uint_fast64_t>, storm::storage::SchedulerChoice<ValueType>>> _productChoices; // <s, q, MEC, InfSet> ---> ReachChoice and <s, q, MEC, InfSet> ---> MecChoice
boost::optional<std::map <uint_fast64_t, std::pair<storm::storage::BitVector, std::vector<storm::storage::BitVector>>>> _mecStatesInfSets; // Save for each accepting mec, its states <s, q> and the infinity sets that need to be visited inf. often (mec 0 corresponds to NoMec)
// Memory structure
boost::optional<std::vector<std::vector<storm::storage::BitVector>>> _memoryTransitions; // The BitVector contains the model states that lead from startState <q, mec, infSet> to <q', mec', infSet'>. This is deterministic, because each state <s, q> is assigned to a unique MEC (scheduler).
boost::optional<std::vector<uint_fast64_t>> _memoryInitialStates; // Save for each stateOfInterest s its initial memory state (which memory state is reached from the initial state after reading s)
boost::optional<std::size_t> _numberOfDaStates;
};
}

2
src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
View File

@ -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<uint64_t, ValueType> transitions;
for (auto const& choiceIndex : choice.getChoiceAsDistribution()) {

8
src/storm/transformer/Product.h
View File

@ -36,6 +36,14 @@ namespace storm {
return productIndexToProductState.at(productStateIndex).second;
}
state_type getProductStateIndex(state_type modelState, state_type automatonState) const {
return productStateToProductIndex.at(product_state_type(modelState, automatonState)); //TODO does this work?
}
bool isValidProductState(state_type modelState, state_type automatonState) const {
return (productStateToProductIndex.count(product_state_type(modelState, automatonState)) >0); //TODO does this work?
}
storm::storage::BitVector liftFromAutomaton(const storm::storage::BitVector& vector) const {
state_type n = productModel.getNumberOfStates();
storm::storage::BitVector lifted(n, false);

9
src/storm/utility/graph.cpp
View File

@ -1764,7 +1764,7 @@ namespace storm {
template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<double>& scheduler, boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ;
template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
@ -1892,9 +1892,10 @@ namespace storm {
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
// TODO remove?
template void computeSchedulerProb1E(storm::storage::BitVector const& prob1EStates, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::Scheduler<storm::RationalFunction>& scheduler, boost::optional<storm::storage::BitVector> const& rowFilter = boost::none);
template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ;
template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);

93
src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp
View File

@ -203,11 +203,14 @@ namespace {
}
}
TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl) {
typedef typename TestFixture::ValueType ValueType;
std::string formulasString = "Pmax=? [X X \"target\"]; Pmin=? [G F \"target\"]; Pmax=? [(G F s>2) & (F G (!s=3))];";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm", formulasString);
std::string formulasString = "Pmax=? [X X \"target\"]; Pmin=? [G F \"target\"]; Pmax=? [(G F s>2) & (F G !(s=3))];";
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());
@ -221,58 +224,114 @@ namespace {
auto result = checker.check(this->env(), tasks[0]);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
storm::storage::Scheduler<ValueType> const &scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
EXPECT_TRUE(scheduler.isDeterministicScheduler());
EXPECT_TRUE(! scheduler.isMemorylessScheduler());
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<storm::models::sparse::Mdp<ValueType>>(); // TODO DTMC!
auto const &inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>(); // TODO DTMC!
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("9/10"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("9/10"),
inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], //TODO other states, too
storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
{
auto result = checker.check(this->env(), tasks[1]);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
storm::storage::Scheduler<ValueType> const &scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().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<storm::models::sparse::Mdp<ValueType>>();
auto const &inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(
*inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1/2"),
inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
{
auto result = checker.check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("1/2"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1/2"),
result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
storm::storage::Scheduler<ValueType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
storm::storage::Scheduler<ValueType> const &scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().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<storm::models::sparse::Mdp<ValueType>>();
auto const &inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(
*inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[2]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1/2"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(this->parseNumber("1/2"),
inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],
storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
}
TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, ltl2) {
typedef typename TestFixture::ValueType ValueType;
//TODO find noMEC-scheduler-error (need nondet in EC)
// Todo unreachable Product state error
std::string formulasString = "Pmax=? [X X !(x=0)];";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/prism-mec-example1.nm", formulasString);
auto mdp = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(3ull, mdp->getNumberOfStates());
EXPECT_EQ(5ull, mdp->getNumberOfTransitions());
ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
EXPECT_EQ(4ull, mdp->getNumberOfChoices());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
{
auto result = checker.check(this->env(), tasks[0]);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
storm::storage::Scheduler<ValueType> const &scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
EXPECT_TRUE(scheduler.isDeterministicScheduler());
EXPECT_TRUE(!scheduler.isMemorylessScheduler());
EXPECT_TRUE(scheduler.isPartialScheduler());
auto inducedModel = mdp->applyScheduler(scheduler, true);
ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp);
auto const &inducedMdp = inducedModel->template as<storm::models::sparse::Mdp<ValueType>>(); // TODO DTMC!
EXPECT_EQ(inducedMdp->getNumberOfChoices(), inducedMdp->getNumberOfStates());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> inducedChecker(*inducedMdp);
auto inducedResult = inducedChecker.check(this->env(), tasks[0]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
// EXPECT_NEAR(this->parseNumber("todo"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
}
}
}
Write Preview
Loading…
Cancel
Save