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

Merge branch 'jani_support' of https://sselab.de/lab9/private/git/storm into jani_support 

Former-commit-id: 21e2240feb [formerly 3690adc628]
Former-commit-id: 3176d0d29f
main
sjunges 9 years ago
parent
1309729150 f2e23a7544
commit
5a64c2b96e
1 changed files with 122 additions and 29 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. 149
      src/builder/DdJaniModelBuilder.cpp

149
src/builder/DdJaniModelBuilder.cpp
View File

@ -530,7 +530,7 @@ namespace storm {
// This structure represents an edge.
struct ActionDd {
ActionDd(storm::dd::Add<Type> const& guard = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitions = storm::dd::Add<Type, ValueType>(), std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments = {}, std::pair<uint64_t, uint64_t> localNondeterminismVariables = std::pair<uint64_t, uint64_t>(0, 0), std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& variableToWritingFragment = {}, storm::dd::Bdd<Type> const& illegalFragment = storm::dd::Bdd<Type>()) : guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), localNondeterminismVariables(localNondeterminismVariables), variableToWritingFragment(variableToWritingFragment), illegalFragment(illegalFragment) {
ActionDd(storm::dd::Add<Type> const& guard = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitions = storm::dd::Add<Type, ValueType>(), std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments = {}, std::pair<uint64_t, uint64_t> localNondeterminismVariables = std::pair<uint64_t, uint64_t>(0, 0), std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& variableToWritingFragment = {}, storm::dd::Bdd<Type> const& illegalFragment = storm::dd::Bdd<Type>()) : guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), localNondeterminismVariables(localNondeterminismVariables), variableToWritingFragment(variableToWritingFragment), illegalFragment(illegalFragment), inputEnabled(false) {
// Intentionally left empty.
}
@ -550,6 +550,14 @@ namespace storm {
return ActionDd(guard, transitions * factor, transientEdgeAssignments, localNondeterminismVariables, variableToWritingFragment, illegalFragment);
}
bool isInputEnabled() const {
return inputEnabled;
}
void setIsInputEnabled() {
inputEnabled = true;
}
// A DD that represents all states that have this edge enabled.
storm::dd::Add<Type, ValueType> guard;
@ -569,6 +577,9 @@ namespace storm {
// A DD characterizing the fragment of the states satisfying the guard that are illegal because
// there are synchronizing edges enabled that write to the same global variable.
storm::dd::Bdd<Type> illegalFragment;
// A flag storing whether this action is input-enabled.
bool inputEnabled;
};
// This structure represents a subcomponent of a composition.
@ -631,7 +642,13 @@ namespace storm {
boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
std::map<uint64_t, uint64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset);
std::set<uint64_t> inputEnabledActionIndices;
for (auto const& actionName : composition.getInputEnabledActions()) {
inputEnabledActionIndices.insert(actionInformation.getActionIndex(actionName));
}
return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset, inputEnabledActionIndices);
}
boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
@ -679,10 +696,15 @@ namespace storm {
private:
AutomatonDd composeInParallel(std::vector<AutomatonDd> const& subautomata, std::vector<storm::jani::SynchronizationVector> const& synchronizationVectors) {
typedef storm::dd::Add<Type, ValueType> IdentityAdd;
typedef std::pair<ActionDd, IdentityAdd> ActionAndAutomatonIdentity;
typedef std::vector<ActionAndAutomatonIdentity> ActionAndAutomatonIdentities;
typedef std::vector<boost::optional<std::pair<ActionAndAutomatonIdentities, IdentityAdd>>> SynchronizationVectorActionsAndIdentities;
AutomatonDd result(this->variables.manager->template getAddOne<ValueType>());
std::map<uint64_t, std::vector<ActionDd>> nonSynchronizingActions;
std::vector<boost::optional<ActionDd>> synchronizationVectorActions(synchronizationVectors.size(), boost::none);
SynchronizationVectorActionsAndIdentities synchronizationVectorActions(synchronizationVectors.size(), boost::none);
for (uint64_t automatonIndex = 0; automatonIndex < subautomata.size(); ++automatonIndex) {
AutomatonDd const& subautomaton = subautomata[automatonIndex];
@ -703,12 +725,12 @@ namespace storm {
if (synchVector.isNoActionInput(synchVector.getInput(automatonIndex))) {
if (automatonIndex == 0) {
// Create a new action that is the identity over the first automaton.
synchronizationVectorActions[synchVectorIndex] = ActionDd(this->variables.manager->template getAddOne<ValueType>(), subautomaton.identity, {}, subautomaton.localNondeterminismVariables, {}, this->variables.manager->getBddZero());
synchronizationVectorActions[synchVectorIndex] = std::make_pair(ActionAndAutomatonIdentities{std::make_pair(ActionDd(this->variables.manager->template getAddOne<ValueType>(), subautomaton.identity, {}, subautomaton.localNondeterminismVariables, {}, this->variables.manager->getBddZero()), subautomaton.identity)}, this->variables.manager->template getAddOne<ValueType>());
} else {
// If there is no action in the output spot, this means that some other subcomposition did
// not provide the action necessary for the synchronization vector to resolve.
if (synchronizationVectorActions[synchVectorIndex]) {
synchronizationVectorActions[synchVectorIndex].get().transitions *= subautomaton.identity;
synchronizationVectorActions[synchVectorIndex].get().second *= subautomaton.identity;
}
}
} else {
@ -721,7 +743,7 @@ namespace storm {
// If the action cannot be found, the particular spot in the output will be left empty.
auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex);
if (inputActionIt != subautomaton.actionIndexToAction.end()) {
synchronizationVectorActions[synchVectorIndex] = inputActionIt->second;
synchronizationVectorActions[synchVectorIndex] = std::make_pair(ActionAndAutomatonIdentities{std::make_pair(inputActionIt->second, subautomaton.identity)}, this->variables.manager->template getAddOne<ValueType>());
}
} else {
// If there is no action in the output spot, this means that some other subcomposition did
@ -729,7 +751,7 @@ namespace storm {
if (synchronizationVectorActions[synchVectorIndex]) {
auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex);
if (inputActionIt != subautomaton.actionIndexToAction.end()) {
synchronizationVectorActions[synchVectorIndex] = combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get(), inputActionIt->second);
synchronizationVectorActions[synchVectorIndex].get().first.push_back(std::make_pair(inputActionIt->second, subautomaton.identity));
} else {
// If the current subcomposition does not provide the required action for the synchronization
// vector, we clear the action.
@ -778,7 +800,7 @@ namespace storm {
// If there is an action resulting from this combination of actions, add it to the output action.
if (synchronizationVectorActions[synchVectorIndex]) {
uint64_t outputActionIndex = actionInformation.getActionIndex(synchVector.getOutput());
nonSynchronizingActions[outputActionIndex].push_back(synchronizationVectorActions[synchVectorIndex].get());
nonSynchronizingActions[outputActionIndex].push_back(combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get().first, synchronizationVectorActions[synchVectorIndex].get().second));
}
}
@ -799,33 +821,101 @@ namespace storm {
return result;
}
ActionDd combineSynchronizingActions(ActionDd action1, ActionDd action2) {
ActionDd combineSynchronizingActions(std::vector<std::pair<ActionDd, storm::dd::Add<Type, ValueType>>> const& actionsAndIdentities, storm::dd::Add<Type, ValueType> const& nonSynchronizingAutomataIdentities) {
// If there is just one action, no need to combine anything.
if (actionsAndIdentities.size() == 1) {
return actionsAndIdentities.front().first;
}
// If there are only input-enabled actions, we also need to build the disjunction of the guards.
bool allActionsInputEnabled = true;
for (auto const& actionIdentityPair : actionsAndIdentities) {
auto const& action = actionIdentityPair.first;
if (!action.isInputEnabled()) {
allActionsInputEnabled = false;
break;
}
}
boost::optional<storm::dd::Bdd<Type>> guardDisjunction;
if (allActionsInputEnabled) {
guardDisjunction = this->variables.manager->getBddZero();
}
// Otherwise, construct the synchronization.
storm::dd::Bdd<Type> illegalFragment = this->variables.manager->getBddZero();
storm::dd::Bdd<Type> guard1 = action1.guard.toBdd();
storm::dd::Bdd<Type> guard2 = action2.guard.toBdd();
storm::dd::Bdd<Type> combinedGuard = guard1 && guard2;
// Cross-multiply the guards to the other fragments that write global variables and check for overlapping
// parts. This finds illegal parts in which a global variable is written multiple times.
std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> globalVariableToWritingFragment;
for (auto& entry : action1.variableToWritingFragment) {
entry.second &= guard2;
globalVariableToWritingFragment[entry.first] = entry.second;
std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> globalVariableToWritingFragmentWithoutNondeterminism;
storm::dd::Bdd<Type> guardConjunction = this->variables.manager->getBddOne();
storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddOne<ValueType>();
std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
uint64_t lowestNondeterminismVariable = actionsAndIdentities.front().first.getLowestLocalNondeterminismVariable();
uint64_t highestNondeterminismVariable = actionsAndIdentities.front().first.getHighestLocalNondeterminismVariable();
storm::dd::Bdd<Type> newIllegalFragment = this->variables.manager->getBddZero();
for (auto const& actionIdentityPair : actionsAndIdentities) {
auto const& action = actionIdentityPair.first;
storm::dd::Bdd<Type> actionGuard = action.guard.toBdd();
if (guardDisjunction) {
guardDisjunction.get() |= actionGuard;
}
for (auto& entry : action2.variableToWritingFragment) {
entry.second &= guard1;
auto it = globalVariableToWritingFragment.find(entry.first);
if (it != globalVariableToWritingFragment.end()) {
auto action1LocalNondeterminismVariableSet = std::set<storm::expressions::Variable>(this->variables.localNondeterminismVariables.begin() + action1.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action1.getHighestLocalNondeterminismVariable());
auto action2LocalNondeterminismVariableSet = std::set<storm::expressions::Variable>(this->variables.localNondeterminismVariables.begin() + action2.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action2.getHighestLocalNondeterminismVariable());
illegalFragment |= it->second.existsAbstract(action1LocalNondeterminismVariableSet) && entry.second.existsAbstract(action2LocalNondeterminismVariableSet);
it->second &= entry.second;
lowestNondeterminismVariable = std::min(lowestNondeterminismVariable, action.getLowestLocalNondeterminismVariable());
highestNondeterminismVariable = std::max(highestNondeterminismVariable, action.getHighestLocalNondeterminismVariable());
transientEdgeAssignments = joinTransientAssignmentMaps(transientEdgeAssignments, action.transientEdgeAssignments);
if (action.isInputEnabled()) {
// If the action is input-enabled, we add self-loops to all states.
transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second);
} else {
transitions *= action.transitions;
}
// Create a set of variables that is used as nondeterminism variables in this action.
auto nondetVariables = std::set<storm::expressions::Variable>(this->variables.localNondeterminismVariables.begin() + action.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action.getHighestLocalNondeterminismVariable());
for (auto const& entry : action.variableToWritingFragment) {
storm::dd::Bdd<Type> guardedWritingFragment = guardConjunction && entry.second;
// Check whether there already is an entry for this variable in the mapping of global variables
// to their writing fragments.
auto globalFragmentIt = globalVariableToWritingFragment.find(entry.first);
if (globalFragmentIt != globalVariableToWritingFragment.end()) {
// If it does, take the conjunction of the entries and also of their versions without nondeterminism
// variables.
globalFragmentIt->second &= guardedWritingFragment;
illegalFragment |= globalVariableToWritingFragmentWithoutNondeterminism[entry.first] && guardedWritingFragment.existsAbstract(nondetVariables);
globalVariableToWritingFragmentWithoutNondeterminism[entry.first] |= guardedWritingFragment.existsAbstract(nondetVariables);
} else {
globalVariableToWritingFragment[entry.first] = entry.second;
// If not, create the entry and also create a version of the entry that abstracts from the
// used nondeterminism variables.
globalVariableToWritingFragment[entry.first] = guardedWritingFragment;
globalVariableToWritingFragmentWithoutNondeterminism[entry.first] = guardedWritingFragment.existsAbstract(nondetVariables);
}
// Join all individual illegal fragments so we can see whether any of these elements lie in the
// conjunction of all guards.
illegalFragment |= action.illegalFragment;
}
// Now go through all fragments that are not written by the current action and join them with the
// guard of the current action.
for (auto& entry : globalVariableToWritingFragment) {
if (action.variableToWritingFragment.find(entry.first) == action.variableToWritingFragment.end()) {
entry.second &= actionGuard;
}
}
return ActionDd(combinedGuard.template toAdd<ValueType>(), action1.transitions * action2.transitions, joinTransientAssignmentMaps(action1.transientEdgeAssignments, action2.transientEdgeAssignments), std::make_pair(std::min(action1.getLowestLocalNondeterminismVariable(), action2.getLowestLocalNondeterminismVariable()), std::max(action1.getHighestLocalNondeterminismVariable(), action2.getHighestLocalNondeterminismVariable())), globalVariableToWritingFragment, illegalFragment);
guardConjunction &= actionGuard;
}
// Cut the union of the illegal fragments to the conjunction of the guards since only these states have
// such a combined transition.
illegalFragment &= guardConjunction;
return ActionDd(guardConjunction.template toAdd<ValueType>(), transitions * nonSynchronizingAutomataIdentities, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment);
}
ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add<Type, ValueType> const& identity1, storm::dd::Add<Type, ValueType> const& identity2) {
@ -1353,7 +1443,7 @@ namespace storm {
}
}
AutomatonDd buildAutomatonDd(std::string const& automatonName, std::map<uint_fast64_t, uint_fast64_t> const& actionIndexToLocalNondeterminismVariableOffset) {
AutomatonDd buildAutomatonDd(std::string const& automatonName, std::map<uint_fast64_t, uint_fast64_t> const& actionIndexToLocalNondeterminismVariableOffset, std::set<uint64_t> const& inputEnabledActionIndices) {
AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName));
storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName);
@ -1363,6 +1453,9 @@ namespace storm {
continue;
}
ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex));
if (inputEnabledActionIndices.find(actionIndex) != inputEnabledActionIndices.end()) {
actionDd.setIsInputEnabled();
}
result.actionIndexToAction[actionIndex] = actionDd;
result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable()));
result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable()));

Write Preview
Loading…
Cancel
Save