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

Added possibility to set (un)reachable states for scheduler 

Conflicts:
	src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

 It looks like you may be committing a cherry-pick.
tempestpy_adaptions
hannah 3 years ago
committed by Stefan Pranger
parent
214d586d10
commit
412489a57f
7 changed files with 159 additions and 57 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 82
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
  2. 2
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
  3. 15
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  4. 88
      src/storm/storage/Scheduler.cpp
  5. 21
      src/storm/storage/Scheduler.h
  6. 2
      src/storm/transformer/DAProductBuilder.h
  7. 6
      src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

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

@ -86,18 +86,25 @@ namespace storm {
uint_fast64_t infSet = std::get<2>(choice.first); uint_fast64_t infSet = std::get<2>(choice.first);
scheduler.setChoice(choice.second, modelState, (automatonState*(_infSets.get().size()+1))+ infSet); scheduler.setChoice(choice.second, modelState, (automatonState*(_infSets.get().size()+1))+ infSet);
// TODO: shouldn't happen?
//STORM_LOG_ASSERT(!this->_unreachableStates.get()[(automatonState*(_infSets.get().size()+1))+ infSet].get(modelState), "Tried to set choice for unreachable state.");
}
/*
for (uint_fast64_t memoryState = 0; this->_unreachableStates.get().size(); ++memoryState) {
for (auto state : this->_unreachableStates.get()[memoryState]) {
// todo fails, memory state = 9
scheduler.setStateUnreachable(state, memoryState);
}
} }
// TODO
// set non-reachable (modelState,memoryState)-Pairs (i.e. those that are not contained in _productChoices) to "unreachable",
// also: states that are never reached using the scheduler
// (extend Scheduler by something like std::vector<std::Bitvector>>
// + reachableSchedulerChoices; isChoiceReachable(..))
// + change definition of partialScheduler/undefinedstates (true if there are undefined states (undefined states are always reachable))
// + maybe states in trueUpsi are unreachable
//
*/
// Sanity check for created scheduler. // Sanity check for created scheduler.
STORM_LOG_ASSERT(scheduler.isDeterministicScheduler(), "Expected a deterministic scheduler"); STORM_LOG_ASSERT(scheduler.isDeterministicScheduler(), "Expected a deterministic scheduler");
STORM_LOG_ASSERT(!scheduler.isPartialScheduler(), "Expected a fully defined scheduler");
return scheduler; return scheduler;
} }
@ -290,7 +297,6 @@ namespace storm {
} }
// Define scheduler choices for the states in this MEC (that are not in any other MEC) // Define scheduler choices for the states in this MEC (that are not in any other MEC)
for (uint_fast64_t id : infSetIds) { for (uint_fast64_t id : infSetIds) {
// Scheduler that satisfies the MEC acceptance condition (visit each InfSet inf often, or switch to scheduler of another MEC) // Scheduler that satisfies the MEC acceptance condition (visit each InfSet inf often, or switch to scheduler of another MEC)
@ -311,7 +317,6 @@ namespace storm {
// We want to reach the InfSet, save choice: <s, q, InfSetID> ---> choice // We want to reach the InfSet, save choice: <s, q, InfSetID> ---> choice
this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), id), mecScheduler.getChoice(pState)}); this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), id), mecScheduler.getChoice(pState)});
} }
} }
} }
} }
@ -441,68 +446,87 @@ namespace storm {
// TODO asserts _mecStatesInfSets initialized etc. // TODO asserts _mecStatesInfSets initialized etc.
// Compute size of the resulting memory structure: a state corresponds to <q, infSet>> encoded as (q* (|infSets|+1))+infSet
uint64 numMemoryStates = (da.getNumberOfStates() * (_infSets.get().size()+1)) + _infSets.get().size()+1; //+1 for states outside accECs
_unreachableStates.emplace(numMemoryStates, storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), false));
// Extract the choices of the REACH-scheduler (choices to reach an acc. MEC) for the MDP-DA product: <s,q> -> choice // 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 : ~acceptingStates) { for (storm::storage::sparse::state_type pState : ~acceptingStates) {
// for state <s,q> not in any accEC <s,q, REACH> ---> choice
// Do not overwrite choices of states in an accepting MEC
this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), _infSets.get().size()), prodCheckResult.scheduler->getChoice(pState)});
// For non-accepting states that are not in any accepting EC we use the 'last' copy of the DA // For non-accepting states that are not in any accepting EC we use the 'last' copy of the DA
this->_accInfSets.get()[pState] = {this->_infSets.get().size()};
this->_accInfSets.get()[pState] = {_infSets.get().size()};
// For state <s,q> not in any accEC <s,q, REACH> ---> choice. Do not overwrite choices of states in an accepting MEC.
this->_productChoices.get().insert({std::make_tuple(product->getModelState(pState), product->getAutomatonState(pState), _infSets.get().size()), prodCheckResult.scheduler->getChoice(pState)});
if (!prodCheckResult.scheduler->isStateReachable(pState)) {
//TODO
this->_unreachableStates.get()[(product->getAutomatonState(pState)) * (_infSets.get().size()+1) + _infSets.get().size()].set(product->getModelState(pState));
}
} }
// Prepare the memory structure. For that, we need: transitions, initialMemoryStates (and memoryStateLabeling) // Prepare the memory structure. For that, we need: transitions, initialMemoryStates (and memoryStateLabeling)
// Compute size of the resulting memory structure: a state corresponds to <q, infSet>> encoded as (q* (|infSets|+1))+infSet
uint64 numMemoryStates = (da.getNumberOfStates() * (_infSets.get().size()+1)) + _infSets.get().size()+1; //+1 for states outside accECs
// The next move function of the memory, will be build based on the transitions of the DA and jumps between InfSets. // The next move function of the memory, will be build based on the transitions of the DA and jumps between InfSets.
this->_memoryTransitions.emplace(numMemoryStates, std::vector<storm::storage::BitVector>(numMemoryStates, storm::storage::BitVector(this->_transitionMatrix.getRowGroupCount(), false))); 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 automatonFrom = 0; automatonFrom < da.getNumberOfStates(); ++automatonFrom) {
for (storm::storage::sparse::state_type automatonTo = 0; automatonTo < da.getNumberOfStates(); ++automatonTo) { for (storm::storage::sparse::state_type automatonTo = 0; automatonTo < da.getNumberOfStates(); ++automatonTo) {
// Find the modelStates that trigger this transition. // Find the modelStates that trigger this transition.
for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) { for (storm::storage::sparse::state_type modelState = 0; modelState < this->_transitionMatrix.getRowGroupCount(); ++modelState) {
if(!product->isValidProductState(modelState, automatonTo)) { 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 <<">");
// <modelState, automatonTo> is not defined in the Product. Thus, considered not reachable for the scheduler.
for (uint_fast64_t infSet = 0; infSet < _infSets.get().size(); ++infSet) {
this->_unreachableStates.get()[ (automatonTo* (_infSets.get().size()+1)) + infSet].set(modelState);
}
} else if (automatonTo == productBuilder.getSuccessor(modelState, automatonFrom, modelState)) { //TODO remove first parameter of getSuccessor } 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, InfSet> (Inf=lenInfSet equals not in MEC)
// Add the modelState to one outgoing transition of all states of the form <automatonFrom, InfSet> (Inf=lenInfSet equals not in MEC)
// For non-accepting states that are not in any accepting EC we use the 'last' copy of the DA // For non-accepting states that are not in any accepting EC we use the 'last' copy of the DA
// For the accepting states we jump through copies of the DA wrt. the infinity sets.
// and for the accepting states we jump through copies of the DA wrt. the infinity sets.
for (uint_fast64_t infSet = 0; infSet < _infSets.get().size()+1; ++infSet) { for (uint_fast64_t infSet = 0; infSet < _infSets.get().size()+1; ++infSet) {
// Check if we need to switch the acceptance condition // Check if we need to switch the acceptance condition
if (_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().count(infSet) == 0) { if (_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().count(infSet) == 0) {
// the state is is in a different accepting MEC with a different accepting conjunction of InfSets. // the state is is in a different accepting MEC with a different accepting conjunction of InfSets.
auto newInfSet = _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin(); auto newInfSet = _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin();
_memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *newInfSet].set(modelState); _memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *newInfSet].set(modelState);
// TODO problem other inf set combis may not be reachable?
// this->_reachableStates.get()[(automatonTo * (_infSets.get().size()+1)) + *newInfSet].set(modelState, true);
} else { } else {
// The state is either not in an accepting EC or in an accepting EC that needs to satisfy the infSet. // The state is either not in an accepting EC or in an accepting EC that needs to satisfy the infSet.
if (infSet == _infSets.get().size() || !(_infSets.get()[infSet].get(product->getProductStateIndex(modelState, automatonTo)))) { if (infSet == _infSets.get().size() || !(_infSets.get()[infSet].get(product->getProductStateIndex(modelState, automatonTo)))) {
// <modelState, automatonTo> is not in any accepting EC or does not satisfy the InfSet, we stay there. // <modelState, automatonTo> is not in any accepting EC or does not satisfy the InfSet, we stay there.
// Add modelState to the transition from <automatonFrom, InfSet> to <automatonTo, InfSet> // Add modelState to the transition from <automatonFrom, InfSet> to <automatonTo, InfSet>
_memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + infSet].set(modelState); _memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + infSet].set(modelState);
// TODO problem other inf set combis may not be reachable?
//this->_reachableStates.get()[(automatonTo * (_infSets.get().size()+1)) + infSet].set(modelState, true);
} else { } else {
STORM_LOG_ASSERT(_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)] != boost::none, "The list of InfSets for the product state <" <<modelState<< ", " << automatonTo<<"> is undefined."); STORM_LOG_ASSERT(_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)] != boost::none, "The list of InfSets for the product state <" <<modelState<< ", " << automatonTo<<"> is undefined.");
// <modelState, automatonTo> satisfies the InfSet, find the next one // <modelState, automatonTo> satisfies the InfSet, find the next one
auto it = std::find(_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin(), _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end(), infSet);
STORM_LOG_ASSERT(it != _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end(), "The list of InfSets for the product state <" <<modelState<< ", " << automatonTo<<"> does not contain the infSet " << infSet);
it++;
if (it == _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end()) {
auto nextInfSet = std::find(_accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin(), _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end(), infSet);
STORM_LOG_ASSERT(nextInfSet != _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end(), "The list of InfSets for the product state <" <<modelState<< ", " << automatonTo<<"> does not contain the infSet " << infSet);
nextInfSet++;
if (nextInfSet == _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().end()) {
// Start again. // Start again.
it = _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin();
nextInfSet = _accInfSets.get()[product->getProductStateIndex(modelState, automatonTo)].get().begin();
} }
// Add modelState to the transition from <automatonFrom <mec, InfSet>> to <automatonTo, <mec, NextInfSet>>. // Add modelState to the transition from <automatonFrom <mec, InfSet>> to <automatonTo, <mec, NextInfSet>>.
_memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *it].set(modelState);
_memoryTransitions.get()[(automatonFrom * (_infSets.get().size()+1)) + infSet][(automatonTo * (_infSets.get().size()+1)) + *nextInfSet].set(modelState);
// TODO problem other inf set combis may not be reachable?
// this->_reachableStates.get()[(automatonTo * (_infSets.get().size()+1)) + *nextInfSet].set(modelState, true);
} }
} }
} }

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

@ -70,7 +70,6 @@ namespace storm {
std::vector<ValueType> computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map<std::string, storm::storage::BitVector>& apSatSets); std::vector<ValueType> computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map<std::string, storm::storage::BitVector>& apSatSets);
private: private:
/*! /*!
* Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance condition (in DNF). * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance condition (in DNF).
* More precisely, let * More precisely, let
@ -99,6 +98,7 @@ namespace storm {
// scheduler // scheduler
bool _randomScheduler = false; bool _randomScheduler = false;
boost::optional<std::map <std::tuple<uint_fast64_t, uint_fast64_t, uint_fast64_t>, storm::storage::SchedulerChoice<ValueType>>> _productChoices; // <s, q, len(_infSets)> ---> ReachChoice and <s, q, InfSet> ---> MecChoice boost::optional<std::map <std::tuple<uint_fast64_t, uint_fast64_t, uint_fast64_t>, storm::storage::SchedulerChoice<ValueType>>> _productChoices; // <s, q, len(_infSets)> ---> ReachChoice and <s, q, InfSet> ---> MecChoice
boost::optional<std::vector<storm::storage::BitVector>> _unreachableStates; // unreachable memory state and model state combinations
boost::optional<std::vector<storm::storage::BitVector>> _infSets; // Save the InfSets of the Acceptance condition. boost::optional<std::vector<storm::storage::BitVector>> _infSets; // Save the InfSets of the Acceptance condition.
boost::optional<std::vector<boost::optional<std::set<uint_fast64_t>>>> _accInfSets; // Save for each product state (which is assigned to an acceptingMEC), the infSets that need to be visited inf often to satisfy the acceptance condition. Remaining states belonging to no accepting EC, are assigned len(_infSets) (REACH scheduler) boost::optional<std::vector<boost::optional<std::set<uint_fast64_t>>>> _accInfSets; // Save for each product state (which is assigned to an acceptingMEC), the infSets that need to be visited inf often to satisfy the acceptance condition. Remaining states belonging to no accepting EC, are assigned len(_infSets) (REACH scheduler)

15
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -609,14 +609,21 @@ namespace storm {
// Set values of resulting vector that are known exactly. // Set values of resulting vector that are known exactly.
storm::utility::vector::setVectorValues<ValueType>(result, qualitativeStateSets.statesWithProbability1, storm::utility::one<ValueType>()); storm::utility::vector::setVectorValues<ValueType>(result, qualitativeStateSets.statesWithProbability1, storm::utility::one<ValueType>());
// Check if the values of the maybe states are relevant for the SolveGoal
bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates);
// If requested, we will produce a scheduler. // If requested, we will produce a scheduler.
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler; std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
if (produceScheduler) { if (produceScheduler) {
scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(transitionMatrix.getRowGroupCount()); scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(transitionMatrix.getRowGroupCount());
}
// If maybeStatesNotRelevant is true, we have to set the scheduler for maybe states as "unreachable"
if (maybeStatesNotRelevant) {
for (auto state : qualitativeStateSets.maybeStates) {
scheduler->setStateUnreachable(state);
}
// Check if the values of the maybe states are relevant for the SolveGoal
bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates);
}
}
// create multiplier and execute the calculation for 1 additional step // create multiplier and execute the calculation for 1 additional step
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix); auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
@ -628,8 +635,6 @@ namespace storm {
} }
} }
std::vector<ValueType> maybeStateChoiceValues = std::vector<ValueType>(sizeMaybeStateChoiceValues, storm::utility::zero<ValueType>());
// TODO: if a scheduler is to be produced and maybestatesNotRelevant is true, we have to set the scheduler for maybsetsates as "unreachable" TODO
// Check whether we need to compute exact probabilities for some states. // Check whether we need to compute exact probabilities for some states.
if ((qualitative || maybeStatesNotRelevant) && !goal.isShieldingTask()) { if ((qualitative || maybeStatesNotRelevant) && !goal.isShieldingTask()) {
// Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.

88
src/storm/storage/Scheduler.cpp
View File

@ -13,41 +13,48 @@ namespace storm {
Scheduler<ValueType>::Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure> const& memoryStructure) : memoryStructure(memoryStructure) { Scheduler<ValueType>::Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure> const& memoryStructure) : memoryStructure(memoryStructure) {
uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1; uint_fast64_t numOfMemoryStates = memoryStructure ? memoryStructure->getNumberOfStates() : 1;
schedulerChoices = std::vector<std::vector<SchedulerChoice<ValueType>>>(numOfMemoryStates, std::vector<SchedulerChoice<ValueType>>(numberOfModelStates)); schedulerChoices = std::vector<std::vector<SchedulerChoice<ValueType>>>(numOfMemoryStates, std::vector<SchedulerChoice<ValueType>>(numberOfModelStates));
reachableStates = std::vector<storm::storage::BitVector>(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, true));
numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates;
numOfDeterministicChoices = 0; numOfDeterministicChoices = 0;
numOfUnreachableStates = 0;
} }
template <typename ValueType> template <typename ValueType>
Scheduler<ValueType>::Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure>&& memoryStructure) : memoryStructure(std::move(memoryStructure)) { Scheduler<ValueType>::Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure>&& memoryStructure) : memoryStructure(std::move(memoryStructure)) {
uint_fast64_t numOfMemoryStates = this->memoryStructure ? this->memoryStructure->getNumberOfStates() : 1; uint_fast64_t numOfMemoryStates = this->memoryStructure ? this->memoryStructure->getNumberOfStates() : 1;
schedulerChoices = std::vector<std::vector<SchedulerChoice<ValueType>>>(numOfMemoryStates, std::vector<SchedulerChoice<ValueType>>(numberOfModelStates)); schedulerChoices = std::vector<std::vector<SchedulerChoice<ValueType>>>(numOfMemoryStates, std::vector<SchedulerChoice<ValueType>>(numberOfModelStates));
reachableStates = std::vector<storm::storage::BitVector>(numOfMemoryStates, storm::storage::BitVector(numberOfModelStates, true));
numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates; numOfUndefinedChoices = numOfMemoryStates * numberOfModelStates;
numOfDeterministicChoices = 0; numOfDeterministicChoices = 0;
numOfUnreachableStates = 0;
} }
template <typename ValueType> template <typename ValueType>
void Scheduler<ValueType>::setChoice(SchedulerChoice<ValueType> const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) { void Scheduler<ValueType>::setChoice(SchedulerChoice<ValueType> const& choice, uint_fast64_t modelState, uint_fast64_t memoryState) {
STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index");
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
auto& schedulerChoice = schedulerChoices[memoryState][modelState]; auto& schedulerChoice = schedulerChoices[memoryState][modelState];
if (schedulerChoice.isDefined()) {
if (!choice.isDefined()) {
++numOfUndefinedChoices;
}
} else {
if (choice.isDefined()) {
assert(numOfUndefinedChoices > 0);
--numOfUndefinedChoices;
}
}
if (schedulerChoice.isDeterministic()) {
if (!choice.isDeterministic()) {
assert(numOfDeterministicChoices > 0);
--numOfDeterministicChoices;
if (reachableStates[memoryState].get(modelState)) {
if (schedulerChoice.isDefined()) {
if (!choice.isDefined()) {
++numOfUndefinedChoices;
}
} else {
if (choice.isDefined()) {
assert(numOfUndefinedChoices > 0);
--numOfUndefinedChoices;
}
} }
} else {
if (choice.isDeterministic()) {
++numOfDeterministicChoices;
if (schedulerChoice.isDeterministic()) {
if (!choice.isDeterministic()) {
assert(numOfDeterministicChoices > 0);
--numOfDeterministicChoices;
}
} else {
if (choice.isDeterministic()) {
++numOfDeterministicChoices;
}
} }
} }
@ -79,6 +86,49 @@ namespace storm {
return schedulerChoices[memoryState][modelState]; return schedulerChoices[memoryState][modelState];
} }
template <typename ValueType>
void Scheduler<ValueType>::setStateUnreachable(uint_fast64_t modelState, uint_fast64_t memoryState) {
STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index");
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
auto& schedulerChoice = schedulerChoices[memoryState][modelState];
if (reachableStates[memoryState].get(modelState)) {
reachableStates[memoryState].set(modelState, false);
++numOfUnreachableStates;
// Choices for unreachable states are not considered undefined or deterministic
if (!schedulerChoice.isDefined()) {
--numOfUndefinedChoices;
} else if (schedulerChoice.isDeterministic()) {
--numOfDeterministicChoices;
}
}
}
template <typename ValueType>
void Scheduler<ValueType>::setStateReachable(uint_fast64_t modelState, uint_fast64_t memoryState) {
STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index");
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
auto& schedulerChoice = schedulerChoices[memoryState][modelState];
if (!reachableStates[memoryState].get(modelState)) {
reachableStates[memoryState].set(modelState, true);
--numOfUnreachableStates;
// Choices for unreachable states are not considered undefined or deterministic
if (!schedulerChoice.isDefined()) {
++numOfUndefinedChoices;
} else if (schedulerChoice.isDeterministic()) {
++numOfDeterministicChoices;
}
}
}
template <typename ValueType>
bool Scheduler<ValueType>::isStateReachable(uint_fast64_t modelState, uint64_t memoryState) const {
return reachableStates[memoryState].get(modelState);
}
template<typename ValueType> template<typename ValueType>
storm::storage::BitVector Scheduler<ValueType>::computeActionSupport(std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const { storm::storage::BitVector Scheduler<ValueType>::computeActionSupport(std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const {
auto nrActions = nondeterministicChoiceIndices.back(); auto nrActions = nondeterministicChoiceIndices.back();
@ -104,7 +154,7 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
bool Scheduler<ValueType>::isDeterministicScheduler() const { bool Scheduler<ValueType>::isDeterministicScheduler() const {
return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices;
return numOfDeterministicChoices == (schedulerChoices.size() * schedulerChoices.begin()->size()) - numOfUndefinedChoices - numOfUnreachableStates;
} }
template <typename ValueType> template <typename ValueType>
@ -124,6 +174,7 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
void Scheduler<ValueType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const { void Scheduler<ValueType>::printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const {
// TODO ignore unreachable states
STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler.");
bool const stateValuationsGiven = model != nullptr && model->hasStateValuations(); bool const stateValuationsGiven = model != nullptr && model->hasStateValuations();
@ -260,6 +311,7 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
void Scheduler<ValueType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const { void Scheduler<ValueType>::printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices) const {
//TODO not defined for memory and unreachable states are not considered
STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); 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_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_LOG_THROW(isMemorylessScheduler(), storm::exceptions::NotImplementedException, "Json export of schedulers with memory not implemented.");

21
src/storm/storage/Scheduler.h
View File

@ -60,6 +60,27 @@ namespace storm {
*/ */
SchedulerChoice<ValueType> const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const; SchedulerChoice<ValueType> const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const;
/*!
* Set the combination of model state and memoryStructure state to unreachable.
*
* @param modelState The state of the model.
* @param memoryState The state of the memoryStructure.
*/
void setStateUnreachable(uint_fast64_t modelState, uint_fast64_t memoryState = 0);
/*!
* Set the combination of model state and memoryStructure state to reachable.
*
* @param modelState The state of the model.
* @param memoryState The state of the memoryStructure.
*/
void setStateReachable(uint_fast64_t modelState, uint_fast64_t memoryState = 0);
/*!
* Is the combination of model state and memoryStructure state to reachable?
*/
bool isStateReachable(uint_fast64_t modelState, uint64_t memoryState = 0) const;
/*! /*!
* Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state * Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state
*/ */

2
src/storm/transformer/DAProductBuilder.h
View File

@ -35,7 +35,7 @@ namespace storm {
return da.getSuccessor(da.getInitialState(), getLabelForState(modelState)); return da.getSuccessor(da.getInitialState(), getLabelForState(modelState));
} }
storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type modelFrom, //TODO delete modelFrom?
storm::storage::sparse::state_type getSuccessor(storm::storage::sparse::state_type modelFrom,
storm::storage::sparse::state_type automatonFrom, storm::storage::sparse::state_type automatonFrom,
storm::storage::sparse::state_type modelTo) const { storm::storage::sparse::state_type modelTo) const {
return da.getSuccessor(automatonFrom, getLabelForState(modelTo)); return da.getSuccessor(automatonFrom, getLabelForState(modelTo));

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

@ -221,7 +221,7 @@ namespace {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp); storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
{ {
tasks[0].setOnlyInitialStatesRelevant(true); // TODO for false, but need equivalent inducedModel state for model state
tasks[0].setOnlyInitialStatesRelevant(true);
auto result = checker.check(this->env(), tasks[0]); auto result = checker.check(this->env(), tasks[0]);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("81/100"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); EXPECT_NEAR(this->parseNumber("81/100"), result->template asExplicitQuantitativeCheckResult<ValueType>()[*mdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
@ -244,7 +244,7 @@ namespace {
EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); EXPECT_NEAR(this->parseNumber("81/100"), inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
} }
{ {
tasks[1].setOnlyInitialStatesRelevant(true);
tasks[1].setOnlyInitialStatesRelevant(false);
auto result = checker.check(this->env(), tasks[1]); auto result = checker.check(this->env(), tasks[1]);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
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());
@ -258,7 +258,7 @@ namespace {
ASSERT_EQ(inducedModel->getType(), storm::models::ModelType::Mdp); 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()); 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]); auto inducedResult = inducedChecker.check(this->env(), tasks[1]);
ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult());
EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()); EXPECT_NEAR(this->parseNumber("1/2"),inducedResult->template asExplicitQuantitativeCheckResult<ValueType>()[*inducedMdp->getInitialStates().begin()],storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());

Write Preview
Loading…
Cancel
Save