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

extended JANI next-state generator to be able to deal with custom system compositions

main
dehnert 8 years ago
parent
5f120fd5bb
commit
b2b692b8ae
4 changed files with 339 additions and 263 deletions
Split View
  1. 499
      src/storm/generator/JaniNextStateGenerator.cpp
  2. 45
      src/storm/generator/JaniNextStateGenerator.h
  3. 50
      src/storm/generator/VariableInformation.cpp
  4. 8
      src/storm/generator/VariableInformation.h

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

@ -34,12 +34,9 @@ namespace storm {
template<typename ValueType, typename StateType>
JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) {
STORM_LOG_THROW(model.hasStandardComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables.");
STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support assignment levels.");
STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidArgumentException, "The jit JANI model builder currently does not support reusing actions in parallel composition");
// Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway).
if (this->model.hasTransientEdgeDestinationAssignments()) {
@ -47,9 +44,12 @@ namespace storm {
}
STORM_LOG_THROW(!this->model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support transient edge destination assignments.");
// Only after checking validity of the program, we initialize the variable information.
// Create all synchronization-related information, e.g. the automata that are put in parallel.
this->createSynchronizationInformation();
// Now we are ready to initialize the variable information.
this->checkValid();
this->variableInformation = VariableInformation(model);
this->variableInformation = VariableInformation(model, this->parallelAutomata);
// Create a proper evalator.
this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(model.getManager());
@ -92,11 +92,6 @@ namespace storm {
// If there are terminal states we need to handle, we now need to translate all labels to expressions.
if (this->options.hasTerminalStates()) {
std::vector<std::reference_wrapper<storm::jani::Automaton const>> composedAutomata;
for (auto const& automaton : this->model.getAutomata()) {
composedAutomata.emplace_back(automaton);
}
for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
if (expressionOrLabelAndBool.first.isExpression()) {
this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
@ -110,7 +105,7 @@ namespace storm {
STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), composedAutomata), expressionOrLabelAndBool.second));
this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata), expressionOrLabelAndBool.second));
}
}
}
@ -177,15 +172,11 @@ namespace storm {
storm::utility::solver::SmtSolverFactory factory;
std::unique_ptr<storm::solver::SmtSolver> solver = factory.create(model.getExpressionManager());
std::vector<std::reference_wrapper<storm::jani::Automaton const>> allAutomata;
for (auto const& automaton : model.getAutomata()) {
allAutomata.push_back(automaton);
}
std::vector<storm::expressions::Expression> rangeExpressions = model.getAllRangeExpressions(allAutomata);
std::vector<storm::expressions::Expression> rangeExpressions = model.getAllRangeExpressions(this->parallelAutomata);
for (auto const& expression : rangeExpressions) {
solver->add(expression);
}
solver->add(model.getInitialStatesExpression(allAutomata));
solver->add(model.getInitialStatesExpression(this->parallelAutomata));
// Proceed as long as the solver can still enumerate initial states.
std::vector<StateType> initialStateIndices;
@ -213,9 +204,10 @@ namespace storm {
// Gather iterators to the initial locations of all the automata.
std::vector<std::set<uint64_t>::const_iterator> initialLocationsIts;
std::vector<std::set<uint64_t>::const_iterator> initialLocationsItes;
for (auto const& automaton : allAutomata) {
initialLocationsIts.push_back(automaton.get().getInitialLocationIndices().cbegin());
initialLocationsItes.push_back(automaton.get().getInitialLocationIndices().cend());
for (auto const& automatonRef : this->parallelAutomata) {
auto const& automaton = automatonRef.get();
initialLocationsIts.push_back(automaton.getInitialLocationIndices().cbegin());
initialLocationsItes.push_back(automaton.getInitialLocationIndices().cend());
}
storm::utility::combinatorics::forEach(initialLocationsIts, initialLocationsItes, [this,&initialState] (uint64_t index, uint64_t value) { setLocation(initialState, this->variableInformation.locationVariables[index], value); }, [&stateToIdCallback,&initialStateIndices,&initialState] () {
// Register initial state.
@ -287,7 +279,8 @@ namespace storm {
// need the state rewards then.
std::vector<ValueType> stateRewards(this->rewardVariables.size(), storm::utility::zero<ValueType>());
uint64_t automatonIndex = 0;
for (auto const& automaton : model.getAutomata()) {
for (auto const& automatonRef : this->parallelAutomata) {
auto const& automaton = automatonRef.get();
uint64_t currentLocationIndex = locations[automatonIndex];
storm::jani::Location const& location = automaton.getLocation(currentLocationIndex);
auto valueIt = stateRewards.begin();
@ -307,12 +300,7 @@ namespace storm {
// Get all choices for the state.
result.setExpanded();
std::vector<Choice<ValueType>> allChoices = getSilentActionChoices(locations, *this->state, stateToIdCallback);
std::vector<Choice<ValueType>> allLabeledChoices = getNonsilentActionChoices(locations, *this->state, stateToIdCallback);
for (auto& choice : allLabeledChoices) {
allChoices.push_back(std::move(choice));
}
std::vector<Choice<ValueType>> allChoices = getActionChoices(locations, *this->state, stateToIdCallback);
std::size_t totalNumberOfChoices = allChoices.size();
// If there is not a single choice, we return immediately, because the state has no behavior (other than
@ -370,239 +358,235 @@ namespace storm {
return result;
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getSilentActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) {
std::vector<Choice<ValueType>> result;
Choice<ValueType> JaniNextStateGenerator<ValueType, StateType>::expandNonSynchronizingEdge(storm::jani::Edge const& edge, uint64_t outputActionIndex, uint64_t automatonIndex, CompressedState const& state, StateToIdCallback stateToIdCallback) {
// Determine the exit rate if it's a Markovian edge.
boost::optional<ValueType> exitRate = boost::none;
if (edge.hasRate()) {
exitRate = this->evaluator->asRational(edge.getRate());
}
// Iterate over all automata.
uint64_t automatonIndex = 0;
Choice<ValueType> choice(edge.getActionIndex(), static_cast<bool>(exitRate));
for (auto const& automaton : model.getAutomata()) {
uint64_t location = locations[automatonIndex];
// Iterate over all updates of the current command.
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (auto const& destination : edge.getDestinations()) {
ValueType probability = this->evaluator->asRational(destination.getProbability());
// Iterate over all edges from the source location.
for (auto const& edge : automaton.getEdgesFromLocation(location)) {
// Skip the edge if it is labeled with a non-silent action.
if (edge.getActionIndex() != storm::jani::Model::SILENT_ACTION_INDEX) {
continue;
}
if (probability != storm::utility::zero<ValueType>()) {
// Obtain target state index and add it to the list of known states. If it has not yet been
// seen, we also add it to the set of states that have yet to be explored.
auto newState = applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]);
// Skip the command, if it is not enabled.
if (!this->evaluator->asBool(edge.getGuard())) {
continue;
}
StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
// Determine the exit rate if it's a Markovian edge.
boost::optional<ValueType> exitRate = boost::none;
if (edge.hasRate()) {
exitRate = this->evaluator->asRational(edge.getRate());
}
// Update the choice by adding the probability/target state to it.
probability = exitRate ? exitRate.get() * probability : probability;
choice.addProbability(stateIndex, probability);
result.push_back(Choice<ValueType>(edge.getActionIndex(), static_cast<bool>(exitRate)));
Choice<ValueType>& choice = result.back();
if (this->options.isExplorationChecksSet()) {
probabilitySum += probability;
}
}
}
// Create the state-action reward for the newly created choice.
performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addReward(value); } );
if (this->options.isExplorationChecksSet()) {
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ").");
}
return choice;
}
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;
if (this->options.isExplorationChecksSet()) {
// Check whether a global variable is written multiple times in any combination.
checkGlobalVariableWritesValid(edgeCombination);
}
std::vector<EdgeSet::const_iterator> iteratorList(edgeCombination.size());
// Initialize the list of iterators.
for (size_t i = 0; i < edgeCombination.size(); ++i) {
iteratorList[i] = edgeCombination[i].second.cbegin();
}
// As long as there is one feasible combination of commands, keep on expanding it.
bool done = false;
while (!done) {
boost::container::flat_map<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
std::vector<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
currentTargetStates->emplace(state, storm::utility::one<ValueType>());
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
storm::jani::Edge const& edge = **iteratorList[i];
// Iterate over all updates of the current command.
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (auto const& destination : edge.getDestinations()) {
ValueType probability = this->evaluator->asRational(destination.getProbability());
if (probability != storm::utility::zero<ValueType>()) {
// Obtain target state index and add it to the list of known states. If it has not yet been
// seen, we also add it to the set of states that have yet to be explored.
StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
// Update the choice by adding the probability/target state to it.
probability = exitRate ? exitRate.get() * probability : probability;
choice.addProbability(stateIndex, probability);
for (auto const& stateProbabilityPair : *currentTargetStates) {
// Compute the new state under the current update and add it to the set of new target states.
CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, destination, this->variableInformation.locationVariables[edgeCombination[i].first]);
if (this->options.isExplorationChecksSet()) {
probabilitySum += probability;
// If the new state was already found as a successor state, update the probability
// and otherwise insert it.
ValueType probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
if (edge.hasRate()) {
probability *= this->evaluator->asRational(edge.getRate());
}
if (probability != storm::utility::zero<ValueType>()) {
auto targetStateIt = newTargetStates->find(newTargetState);
if (targetStateIt != newTargetStates->end()) {
targetStateIt->second += probability;
} else {
newTargetStates->emplace(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; } );
}
// Create the state-action reward for the newly created choice.
performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addReward(value); } );
// If there is one more command to come, shift the target states one time step back.
if (i < iteratorList.size() - 1) {
delete currentTargetStates;
currentTargetStates = newTargetStates;
newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
}
}
// 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
// add the choice to the list of transitions.
result.emplace_back(outputActionIndex);
// Now create the actual distribution.
Choice<ValueType>& choice = result.back();
// Add the rewards to the choice.
choice.addRewards(std::move(stateActionRewards));
// Add the probabilities/rates to the newly created choice.
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (auto const& stateProbabilityPair : *newTargetStates) {
StateType actualIndex = stateToIdCallback(stateProbabilityPair.first);
choice.addProbability(actualIndex, stateProbabilityPair.second);
if (this->options.isExplorationChecksSet()) {
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ").");
probabilitySum += stateProbabilityPair.second;
}
}
++automatonIndex;
if (this->options.isExplorationChecksSet()) {
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ").");
}
// Dispose of the temporary maps.
delete currentTargetStates;
delete newTargetStates;
// Now, check whether there is one more command combination to consider.
bool movedIterator = false;
for (uint64_t j = 0; !movedIterator && j < iteratorList.size(); ++j) {
++iteratorList[j];
if (iteratorList[j] != edgeCombination[j].second.end()) {
movedIterator = true;
} else {
// Reset the iterator to the beginning of the list.
iteratorList[j] = edgeCombination[j].second.begin();
}
}
done = !movedIterator;
}
return result;
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getNonsilentActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) {
std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) {
std::vector<Choice<ValueType>> result;
for (uint64_t actionIndex : model.getNonsilentActionIndices()) {
std::vector<std::vector<storm::jani::Edge const*>> enabledEdges = getEnabledEdges(locations, actionIndex);
// Only process this action, if there is at least one feasible solution.
if (!enabledEdges.empty()) {
if (this->options.isExplorationChecksSet()) {
// Check whether a global variable is written multiple times in any combination.
checkGlobalVariableWritesValid(enabledEdges);
for (auto const& outputAndEdges : edges) {
auto const& edges = outputAndEdges.second;
if (edges.size() == 1) {
// If the synch consists of just one element, it's non-synchronizing.
auto const& nonsychingEdges = edges.front();
uint64_t automatonIndex = nonsychingEdges.first;
auto edgesIt = nonsychingEdges.second.find(locations[automatonIndex]);
if (edgesIt != nonsychingEdges.second.end()) {
for (auto const& edge : edgesIt->second) {
if (!this->evaluator->asBool(edge->getGuard())) {
continue;
}
Choice<ValueType> choice = expandNonSynchronizingEdge(*edge, outputAndEdges.first ? outputAndEdges.first.get() : edge->getActionIndex(), automatonIndex, state, stateToIdCallback);
result.emplace_back(std::move(choice));
}
}
} else {
// If the element has more than one set of edges, we need to perform a synchronization.
STORM_LOG_ASSERT(outputAndEdges.first, "Need output action index for synchronization.");
std::vector<std::vector<storm::jani::Edge const*>::const_iterator> iteratorList(enabledEdges.size());
// Initialize the list of iterators.
for (size_t i = 0; i < enabledEdges.size(); ++i) {
iteratorList[i] = enabledEdges[i].cbegin();
}
AutomataEdgeSets automataEdgeSets;
uint64_t outputActionIndex = outputAndEdges.first.get();
// As long as there is one feasible combination of commands, keep on expanding it.
bool done = false;
while (!done) {
boost::container::flat_map<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
std::vector<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
bool productiveCombination = true;
for (auto const& automatonAndEdges : outputAndEdges.second) {
uint64_t automatonIndex = automatonAndEdges.first;
EdgeSet enabledEdgesOfAutomaton;
currentTargetStates->emplace(state, storm::utility::one<ValueType>());
auto locationVariableIt = this->variableInformation.locationVariables.cbegin();
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
storm::jani::Edge const& edge = **iteratorList[i];
for (auto const& destination : edge.getDestinations()) {
for (auto const& stateProbabilityPair : *currentTargetStates) {
// Compute the new state under the current update and add it to the set of new target states.
CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, destination, *locationVariableIt);
// If the new state was already found as a successor state, update the probability
// and otherwise insert it.
ValueType probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
if (edge.hasRate()) {
probability *= this->evaluator->asRational(edge.getRate());
}
if (probability != storm::utility::zero<ValueType>()) {
auto targetStateIt = newTargetStates->find(newTargetState);
if (targetStateIt != newTargetStates->end()) {
targetStateIt->second += probability;
} else {
newTargetStates->emplace(newTargetState, probability);
}
}
bool atLeastOneEdge = false;
auto edgesIt = automatonAndEdges.second.find(locations[automatonIndex]);
if (edgesIt != automatonAndEdges.second.end()) {
for (auto const& edge : edgesIt->second) {
if (!this->evaluator->asBool(edge->getGuard())) {
continue;
}
// 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; } );
}
// If there is one more command to come, shift the target states one time step back.
if (i < iteratorList.size() - 1) {
delete currentTargetStates;
currentTargetStates = newTargetStates;
newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
}
++locationVariableIt;
}
// 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
// add the choice to the list of transitions.
result.push_back(Choice<ValueType>(actionIndex));
// Now create the actual distribution.
Choice<ValueType>& choice = result.back();
// Add the rewards to the choice.
choice.addRewards(std::move(stateActionRewards));
// Add the probabilities/rates to the newly created choice.
ValueType probabilitySum = storm::utility::zero<ValueType>();
for (auto const& stateProbabilityPair : *newTargetStates) {
StateType actualIndex = stateToIdCallback(stateProbabilityPair.first);
choice.addProbability(actualIndex, stateProbabilityPair.second);
if (this->options.isExplorationChecksSet()) {
probabilitySum += stateProbabilityPair.second;
atLeastOneEdge = true;
enabledEdgesOfAutomaton.emplace_back(edge);
}
}
if (this->options.isExplorationChecksSet()) {
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ").");
}
// Dispose of the temporary maps.
delete currentTargetStates;
delete newTargetStates;
// Now, check whether there is one more command combination to consider.
bool movedIterator = false;
for (uint64_t j = 0; !movedIterator && j < iteratorList.size(); ++j) {
++iteratorList[j];
if (iteratorList[j] != enabledEdges[j].end()) {
movedIterator = true;
} else {
// Reset the iterator to the beginning of the list.
iteratorList[j] = enabledEdges[j].begin();
}
// If there is no enabled edge of this automaton, the whole combination is not productive.
if (!atLeastOneEdge) {
productiveCombination = false;
break;
}
done = !movedIterator;
automataEdgeSets.emplace_back(std::make_pair(automatonIndex, std::move(enabledEdgesOfAutomaton)));
}
}
}
return result;
}
template<typename ValueType, typename StateType>
std::vector<std::vector<storm::jani::Edge const*>> JaniNextStateGenerator<ValueType, StateType>::getEnabledEdges(std::vector<uint64_t> const& locationIndices, uint64_t actionIndex) {
std::vector<std::vector<storm::jani::Edge const*>> result;
// Iterate over all automata.
uint64_t automatonIndex = 0;
for (auto const& automaton : model.getAutomata()) {
// If the automaton has no edge labeled with the given action, we can skip it.
if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) {
continue;
}
auto edges = automaton.getEdgesFromLocation(locationIndices[automatonIndex], actionIndex);
// If the automaton contains the action, but there is no edge available labeled with
// this action, we don't have any feasible command combinations.
if (edges.empty()) {
return std::vector<std::vector<storm::jani::Edge const*>>();
}
std::vector<storm::jani::Edge const*> edgePointers;
for (auto const& edge : edges) {
if (this->evaluator->asBool(edge.getGuard())) {
edgePointers.push_back(&edge);
if (productiveCombination) {
std::vector<Choice<ValueType>> choices = expandSynchronizingEdgeCombination(automataEdgeSets, outputActionIndex, state, stateToIdCallback);
for (auto const& choice : choices) {
result.emplace_back(std::move(choice));
}
}
}
// If there was no enabled edge although the automaton has some edge with the required action, we must
// not return anything.
if (edgePointers.empty()) {
return std::vector<std::vector<storm::jani::Edge const*>>();
}
result.emplace_back(std::move(edgePointers));
++automatonIndex;
}
}
return result;
}
template<typename ValueType, typename StateType>
void JaniNextStateGenerator<ValueType, StateType>::checkGlobalVariableWritesValid(std::vector<std::vector<storm::jani::Edge const*>> const& enabledEdges) const {
void JaniNextStateGenerator<ValueType, StateType>::checkGlobalVariableWritesValid(AutomataEdgeSets const& enabledEdges) const {
std::map<storm::expressions::Variable, uint64_t> writtenGlobalVariables;
for (auto edgeSetIt = enabledEdges.begin(), edgeSetIte = enabledEdges.end(); edgeSetIt != edgeSetIte; ++edgeSetIt) {
for (auto const& edge : *edgeSetIt) {
for (auto const& edge : edgeSetIt->second) {
for (auto const& globalVariable : edge->getWrittenGlobalVariables()) {
auto it = writtenGlobalVariables.find(globalVariable);
@ -629,20 +613,13 @@ namespace storm {
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
// Prepare a mapping from automata names to the location variables.
std::vector<std::reference_wrapper<storm::jani::Automaton const>> composedAutomata;
for (auto const& automaton : model.getAutomata()) {
composedAutomata.emplace_back(automaton);
}
// As in JANI we can use transient boolean variable assignments in locations to identify states, we need to
// create a list of boolean transient variables and the expressions that define them.
std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> transientVariableToExpressionMap;
for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
if (variable.isBooleanVariable()) {
if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) {
transientVariableToExpressionMap[variable.getExpressionVariable()] = model.getLabelExpression(variable.asBooleanVariable(), composedAutomata);
transientVariableToExpressionMap[variable.getExpressionVariable()] = model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata);
}
}
}
@ -691,7 +668,8 @@ namespace storm {
}
// Then fill them.
for (auto const& automaton : model.getAutomata()) {
for (auto const& automatonRef : this->parallelAutomata) {
auto const& automaton = automatonRef.get();
for (auto const& location : automaton.getLocations()) {
auto rewardVariableIt = rewardVariables.begin();
auto rewardVariableIte = rewardVariables.end();
@ -731,6 +709,81 @@ namespace storm {
}
}
template<typename ValueType, typename StateType>
void JaniNextStateGenerator<ValueType, StateType>::createSynchronizationInformation() {
// Create synchronizing edges information.
storm::jani::Composition const& topLevelComposition = this->model.getSystemComposition();
if (topLevelComposition.isAutomatonComposition()) {
auto const& automaton = this->model.getAutomaton(topLevelComposition.asAutomatonComposition().getAutomatonName());
this->parallelAutomata.push_back(automaton);
LocationsAndEdges locationsAndEdges;
for (auto const& edge : automaton.getEdges()) {
locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(&edge);
}
AutomataAndEdges automataAndEdges;
automataAndEdges.emplace_back(std::make_pair(0, std::move(locationsAndEdges)));
this->edges.emplace_back(std::make_pair(boost::none, std::move(automataAndEdges)));
} else {
STORM_LOG_THROW(topLevelComposition.isParallelComposition(), storm::exceptions::WrongFormatException, "Expected parallel composition.");
storm::jani::ParallelComposition const& parallelComposition = topLevelComposition.asParallelComposition();
uint64_t automatonIndex = 0;
for (auto const& composition : parallelComposition.getSubcompositions()) {
STORM_LOG_THROW(composition->isAutomatonComposition(), storm::exceptions::WrongFormatException, "Expected flat parallel composition.");
this->parallelAutomata.push_back(this->model.getAutomaton(composition->asAutomatonComposition().getAutomatonName()));
// Add edges with silent action.
LocationsAndEdges locationsAndEdges;
for (auto const& edge : parallelAutomata.back().get().getEdges()) {
if (edge.getActionIndex() == storm::jani::Model::SILENT_ACTION_INDEX) {
locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(&edge);
}
}
if (!locationsAndEdges.empty()) {
AutomataAndEdges automataAndEdges;
automataAndEdges.emplace_back(std::make_pair(automatonIndex, std::move(locationsAndEdges)));
this->edges.emplace_back(std::make_pair(boost::none, std::move(automataAndEdges)));
}
++automatonIndex;
}
for (auto const& vector : parallelComposition.getSynchronizationVectors()) {
uint64_t outputActionIndex = this->model.getActionIndex(vector.getOutput());
AutomataAndEdges automataAndEdges;
bool atLeastOneEdge = true;
uint64_t automatonIndex = 0;
for (auto const& element : vector.getInput()) {
if (!storm::jani::SynchronizationVector::isNoActionInput(element)) {
LocationsAndEdges locationsAndEdges;
uint64_t actionIndex = this->model.getActionIndex(element);
for (auto const& edge : parallelAutomata[automatonIndex].get().getEdges()) {
if (edge.getActionIndex() == actionIndex) {
locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(&edge);
}
}
if (locationsAndEdges.empty()) {
atLeastOneEdge = false;
break;
}
automataAndEdges.emplace_back(std::make_pair(automatonIndex, std::move(locationsAndEdges)));
}
++automatonIndex;
}
if (atLeastOneEdge) {
this->edges.emplace_back(std::make_pair(outputActionIndex, std::move(automataAndEdges)));
}
}
}
STORM_LOG_TRACE("Number of synchronizations: " << this->edges.size() << ".");
}
template<typename ValueType, typename StateType>
void JaniNextStateGenerator<ValueType, StateType>::checkValid() const {
// If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.

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

@ -66,35 +66,33 @@ namespace storm {
CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update, storm::generator::LocationVariableInformation const& locationVariable);
/*!
* Retrieves all choices labeled with the silent action possible from the given state.
* Retrieves all choices possible from the given state.
*
* @param locations The current locations of all automata.
* @param state The state for which to retrieve the silent choices.
* @return The silent action choices of the state.
* @return The action choices of the state.
*/
std::vector<Choice<ValueType>> getSilentActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback);
std::vector<Choice<ValueType>> getActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback);
/*!
* Retrieves all choices labeled with some non-silent action possible from the given state.
*
* @param locations THe current locations of all automata.
* @param state The state for which to retrieve the non-silent choices.
* @return The non-silent action choices of the state.
* Retrieves the choice generated by the given edge.
*/
std::vector<Choice<ValueType>> getNonsilentActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback);
Choice<ValueType> expandNonSynchronizingEdge(storm::jani::Edge const& edge, uint64_t outputActionIndex, uint64_t automatonIndex, CompressedState const& state, StateToIdCallback stateToIdCallback);
/*!
* Retrieves a list of lists of edges such that the list at index i are all edges of automaton i enabled in
* the current state. If the list is empty, it means there was at least one automaton containing edges with
* the desired action, but none of them were enabled.
*/
std::vector<std::vector<storm::jani::Edge const*>> getEnabledEdges(std::vector<uint64_t> const& locationIndices, uint64_t actionIndex);
typedef std::vector<storm::jani::Edge const*> EdgeSet;
typedef std::unordered_map<uint64_t, EdgeSet> LocationsAndEdges;
typedef std::vector<std::pair<uint64_t, LocationsAndEdges>> AutomataAndEdges;
typedef std::pair<boost::optional<uint64_t>, AutomataAndEdges> OutputAndEdges;
typedef std::pair<uint64_t, EdgeSet> AutomatonAndEdgeSet;
typedef std::vector<AutomatonAndEdgeSet> AutomataEdgeSets;
std::vector<Choice<ValueType>> expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state, StateToIdCallback stateToIdCallback);
/*!
* Checks the list of enabled edges (obtained by a call to <code>getEnabledEdges</code>) for multiple
* synchronized writes to the same global variable.
* Checks the list of enabled edges for multiple synchronized writes to the same global variable.
*/
void checkGlobalVariableWritesValid(std::vector<std::vector<storm::jani::Edge const*>> const& enabledEdges) const;
void checkGlobalVariableWritesValid(AutomataEdgeSets const& enabledEdges) const;
/*!
* Treats the given transient assignments by calling the callback function whenever a transient assignment
@ -107,6 +105,11 @@ namespace storm {
*/
void buildRewardModelInformation();
/*!
* Creates the internal information about synchronizing edges.
*/
void createSynchronizationInformation();
/*!
* Checks the underlying model for validity for this next-state generator.
*/
@ -115,6 +118,12 @@ namespace storm {
/// The model used for the generation of next states.
storm::jani::Model model;
/// The automata that are put into parallel by this generator.
std::vector<std::reference_wrapper<storm::jani::Automaton const>> parallelAutomata;
/// The vector storing the edges that need to be explored (synchronously or asynchronously).
std::vector<OutputAndEdges> edges;
/// The transient variables of reward models that need to be considered.
std::vector<storm::expressions::Variable> rewardVariables;

50
src/storm/generator/VariableInformation.cpp
View File

@ -4,10 +4,13 @@
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/Automaton.h"
#include "storm/storage/jani/AutomatonComposition.h"
#include "storm/storage/jani/ParallelComposition.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/WrongFormatException.h"
#include <cmath>
@ -55,7 +58,7 @@ namespace storm {
sortVariables();
}
VariableInformation::VariableInformation(storm::jani::Model const& model) : totalBitOffset(0) {
VariableInformation::VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata) : totalBitOffset(0) {
// Check that the model does not contain non-transient unbounded integer or non-transient real variables.
STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains global non-transient real variables.");
STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient unbounded integer variables.");
@ -79,29 +82,34 @@ namespace storm {
totalBitOffset += bitwidth;
}
}
for (auto const& automaton : model.getAutomata()) {
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
totalBitOffset += bitwidth;
for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
if (!variable.isTransient()) {
booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
++totalBitOffset;
}
for (auto const& automatonRef : parallelAutomata) {
createVariablesForAutomaton(automatonRef.get());
}
sortVariables();
}
void VariableInformation::createVariablesForAutomaton(storm::jani::Automaton const& automaton) {
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
totalBitOffset += bitwidth;
for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
if (!variable.isTransient()) {
booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
++totalBitOffset;
}
for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
if (!variable.isTransient()) {
int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
totalBitOffset += bitwidth;
}
}
for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
if (!variable.isTransient()) {
int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
totalBitOffset += bitwidth;
}
}
sortVariables();
}
uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const {

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

@ -13,6 +13,7 @@ namespace storm {
namespace jani {
class Model;
class Automaton;
}
namespace generator {
@ -74,7 +75,7 @@ namespace storm {
// A structure storing information about the used variables of the program.
struct VariableInformation {
VariableInformation(storm::prism::Program const& program);
VariableInformation(storm::jani::Model const& model);
VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata);
VariableInformation() = default;
uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;
@ -96,6 +97,11 @@ namespace storm {
* Sorts the variables to establish a known ordering.
*/
void sortVariables();
/*!
* Creates all necessary variables for a JANI automaton.
*/
void createVariablesForAutomaton(storm::jani::Automaton const& automaton);
};
}

Write Preview
|||||||
100:0
Loading…
Cancel
Save