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

switching to recursive synchronization resolution for JANI explicit model exploration

main
dehnert 7 years ago
parent
205ed7f4bf
commit
032d68b9b0
6 changed files with 67 additions and 58 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. 84
      src/storm/generator/JaniNextStateGenerator.cpp
  2. 8
      src/storm/generator/JaniNextStateGenerator.h
  3. 14
      src/storm/storage/jani/Automaton.cpp
  4. 4
      src/storm/storage/jani/Automaton.h
  5. 10
      src/storm/storage/jani/Model.cpp
  6. 5
      src/storm/storage/jani/Model.h

84
src/storm/generator/JaniNextStateGenerator.cpp
View File

@ -173,7 +173,7 @@ namespace storm {
std::vector<StateType> JaniNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
std::vector<StateType> initialStateIndices;
if (this->model.hasNonTrivialInitialStatesRestriction()) {
if (this->model.hasNonTrivialInitialStates()) {
// Prepare an SMT solver to enumerate all initial states.
storm::utility::solver::SmtSolverFactory factory;
std::unique_ptr<storm::solver::SmtSolver> solver = factory.create(model.getExpressionManager());
@ -473,6 +473,33 @@ namespace storm {
return choice;
}
template<typename ValueType, typename StateType>
void JaniNextStateGenerator<ValueType, StateType>::generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, AutomataEdgeSets const& edgeCombination, std::vector<EdgeSetWithIndices::const_iterator> const& iteratorList, storm::builder::jit::Distribution<StateType, ValueType>& distribution, std::vector<ValueType>& stateActionRewards, EdgeIndexSet& edgeIndices, StateToIdCallback stateToIdCallback) {
if (storm::utility::isZero<ValueType>(probability)) {
return;
}
if (position >= iteratorList.size()) {
StateType id = stateToIdCallback(state);
distribution.add(id, probability);
} else {
auto const& indexAndEdge = *iteratorList[position];
auto const& edge = *indexAndEdge.second;
for (auto const& destination : edge.getDestinations()) {
generateSynchronizedDistribution(applyUpdate(state, destination, this->variableInformation.locationVariables[edgeCombination[position].first]), probability * this->evaluator->asRational(destination.getProbability()), position + 1, edgeCombination, iteratorList, distribution, stateActionRewards, edgeIndices, stateToIdCallback);
}
if (this->getOptions().isBuildChoiceOriginsSet()) {
edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[position].first, indexAndEdge.first));
}
auto valueIt = stateActionRewards.begin();
performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
}
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state, StateToIdCallback stateToIdCallback) {
std::vector<Choice<ValueType>> result;
@ -489,57 +516,17 @@ namespace storm {
iteratorList[i] = edgeCombination[i].second.cbegin();
}
storm::builder::jit::Distribution<CompressedState, ValueType> currentDistribution;
storm::builder::jit::Distribution<CompressedState, ValueType> nextDistribution;
storm::builder::jit::Distribution<StateType, ValueType> distribution;
// As long as there is one feasible combination of commands, keep on expanding it.
bool done = false;
while (!done) {
currentDistribution.clear();
nextDistribution.clear();
std::vector<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
currentDistribution.add(state, storm::utility::one<ValueType>());
distribution.clear();
EdgeIndexSet edgeIndices;
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
auto const& indexAndEdge = *iteratorList[i];
if (this->getOptions().isBuildChoiceOriginsSet()) {
edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[i].first, indexAndEdge.first));
}
storm::jani::Edge const& edge = *indexAndEdge.second;
for (auto const& destination : edge.getDestinations()) {
for (auto const& stateProbability : currentDistribution) {
// Compute the new state under the current update and add it to the set of new target states.
CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first]);
// If the new state was already found as a successor state, update the probability
// and otherwise insert it.
ValueType probability = stateProbability.getValue() * this->evaluator->asRational(destination.getProbability());
if (edge.hasRate()) {
probability *= this->evaluator->asRational(edge.getRate());
}
if (probability != storm::utility::zero<ValueType>()) {
nextDistribution.add(newTargetState, probability);
}
}
}
// Create the state-action reward for the newly created choice.
auto valueIt = stateActionRewards.begin();
performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
nextDistribution.compress();
// If there is one more command to come, shift the target states one time step back.
if (i < iteratorList.size() - 1) {
currentDistribution = std::move(nextDistribution);
}
}
std::vector<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
generateSynchronizedDistribution(state, storm::utility::one<ValueType>(), 0, edgeCombination, iteratorList, distribution, stateActionRewards, edgeIndices, stateToIdCallback);
distribution.compress();
// At this point, we applied all commands of the current command combination and newTargetStates
// contains all target states and their respective probabilities. That means we are now ready to
@ -559,9 +546,8 @@ namespace storm {
// Add the probabilities/rates to the newly created choice.
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (auto const& stateProbability : nextDistribution) {
StateType actualIndex = stateToIdCallback(stateProbability.getState());
choice.addProbability(actualIndex, stateProbability.getValue());
for (auto const& stateProbability : distribution) {
choice.addProbability(stateProbability.getState(), stateProbability.getValue());
if (this->options.isExplorationChecksSet()) {
probabilitySum += stateProbability.getValue();

8
src/storm/generator/JaniNextStateGenerator.h
View File

@ -8,6 +8,13 @@
#include "storm/storage/jani/OrderedAssignments.h"
namespace storm {
namespace builder {
namespace jit {
template <typename StateType, typename ValueType>
class Distribution;
}
}
namespace jani {
class Edge;
class EdgeDestination;
@ -93,6 +100,7 @@ namespace storm {
typedef std::vector<AutomatonAndEdgeSet> AutomataEdgeSets;
std::vector<Choice<ValueType>> expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state, StateToIdCallback stateToIdCallback);
void generateSynchronizedDistribution(storm::storage::BitVector const& state, ValueType const& probability, uint64_t position, AutomataEdgeSets const& edgeCombination, std::vector<EdgeSetWithIndices::const_iterator> const& iteratorList, storm::builder::jit::Distribution<StateType, ValueType>& distribution, std::vector<ValueType>& stateActionRewards, EdgeIndexSet& edgeIndices, StateToIdCallback stateToIdCallback);
/*!
* Checks the list of enabled edges for multiple synchronized writes to the same global variable.

14
src/storm/storage/jani/Automaton.cpp
View File

@ -323,8 +323,18 @@ namespace storm {
return initialStatesRestriction.isInitialized();
}
bool Automaton::hasNonTrivialInitialStatesRestriction() const {
return this->hasInitialStatesRestriction() && !this->getInitialStatesRestriction().isTrue();
bool Automaton::hasNonTrivialInitialStates() const {
if (this->hasInitialStatesRestriction() && !this->getInitialStatesRestriction().isTrue()) {
return true;
}
for (auto const& variable : this->getVariables()) {
if (variable.hasInitExpression() && !variable.isTransient()) {
return true;
}
}
return false;
}
storm::expressions::Expression const& Automaton::getInitialStatesRestriction() const {

4
src/storm/storage/jani/Automaton.h
View File

@ -242,9 +242,9 @@ namespace storm {
bool hasInitialStatesRestriction() const;
/*!
* Retrieves whether there is a non-trivial initial states restriction.
* Retrieves whether this automaton has non-trivial initial states.
*/
bool hasNonTrivialInitialStatesRestriction() const;
bool hasNonTrivialInitialStates() const;
/*!
* Gets the expression restricting the legal initial values of the automaton's variables.

10
src/storm/storage/jani/Model.cpp
View File

@ -939,12 +939,18 @@ namespace storm {
return initialStatesRestriction;
}
bool Model::hasNonTrivialInitialStatesRestriction() const {
bool Model::hasNonTrivialInitialStates() const {
if (this->hasInitialStatesRestriction() && !this->getInitialStatesRestriction().isTrue()) {
return true;
} else {
for (auto const& variable : this->getGlobalVariables()) {
if (variable.hasInitExpression() && !variable.isTransient()) {
return true;
}
}
for (auto const& automaton : this->automata) {
if (automaton.hasInitialStatesRestriction() && !automaton.getInitialStatesRestriction().isTrue()) {
if (automaton.hasNonTrivialInitialStates()) {
return true;
}
}

5
src/storm/storage/jani/Model.h
View File

@ -358,10 +358,9 @@ namespace storm {
bool hasInitialStatesRestriction() const;
/*!
* Retrieves whether there is a non-trivial initial states restriction in the model or any of the contained
* automata.
* Retrieves whether there are non-trivial initial states in the model or any of the contained automata.
*/
bool hasNonTrivialInitialStatesRestriction() const;
bool hasNonTrivialInitialStates() const;
/*!
* Sets the expression restricting the legal initial values of the global variables.

Write Preview
Loading…
Cancel
Save