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

one step more 

Former-commit-id: 95773b13c3 [formerly 28ca90f221]
Former-commit-id: 51d197d2b5
tempestpy_adaptions
dehnert 8 years ago
parent
2471036df4
commit
c4f8c1fbcb
5 changed files with 127 additions and 43 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. 5
      src/builder/jit/Choice.cpp
  2. 1
      src/builder/jit/Choice.h
  3. 5
      src/builder/jit/Distribution.cpp
  4. 139
      src/builder/jit/ExplicitJitJaniModelBuilder.cpp
  5. 2
      src/builder/jit/StateBehaviour.cpp

5
src/builder/jit/Choice.cpp
View File

@ -7,7 +7,7 @@ namespace storm {
namespace jit { namespace jit {
template <typename IndexType, typename ValueType> template <typename IndexType, typename ValueType>
Choice<IndexType, ValueType>::Choice() : compressed(true) {
Choice<IndexType, ValueType>::Choice() {
// Intentionally left empty. // Intentionally left empty.
} }
@ -38,10 +38,7 @@ namespace storm {
template <typename IndexType, typename ValueType> template <typename IndexType, typename ValueType>
void Choice<IndexType, ValueType>::compress() { void Choice<IndexType, ValueType>::compress() {
if (!compressed) {
distribution.compress(); distribution.compress();
compressed = true;
}
} }
template <typename IndexType, typename ValueType> template <typename IndexType, typename ValueType>

1
src/builder/jit/Choice.h
View File

@ -24,7 +24,6 @@ namespace storm {
Distribution<IndexType, ValueType>& getDistribution(); Distribution<IndexType, ValueType>& getDistribution();
Distribution<IndexType, ValueType> distribution; Distribution<IndexType, ValueType> distribution;
bool compressed;
}; };
} }

5
src/builder/jit/Distribution.cpp
View File

@ -14,13 +14,13 @@ namespace storm {
template <typename IndexType, typename ValueType> template <typename IndexType, typename ValueType>
void Distribution<IndexType, ValueType>::add(DistributionEntry<IndexType, ValueType> const& entry) { void Distribution<IndexType, ValueType>::add(DistributionEntry<IndexType, ValueType> const& entry) {
storage.push_back(entry); storage.push_back(entry);
compressed = storage.back().getIndex() < entry.getIndex();
compressed &= storage.back().getIndex() < entry.getIndex();
} }
template <typename IndexType, typename ValueType> template <typename IndexType, typename ValueType>
void Distribution<IndexType, ValueType>::add(IndexType const& index, ValueType const& value) { void Distribution<IndexType, ValueType>::add(IndexType const& index, ValueType const& value) {
storage.emplace_back(index, value); storage.emplace_back(index, value);
compressed = storage.back().getIndex() < index;
compressed &= storage.back().getIndex() < index;
} }
template <typename IndexType, typename ValueType> template <typename IndexType, typename ValueType>
@ -57,6 +57,7 @@ namespace storm {
storage.resize(std::distance(storage.begin(), result)); storage.resize(std::distance(storage.begin(), result));
} }
compressed = true;
} }
} }

139
src/builder/jit/ExplicitJitJaniModelBuilder.cpp
View File

@ -159,56 +159,113 @@ namespace storm {
std::queue<StateType> storage; std::queue<StateType> storage;
}; };
{% for edge in nonSynchronizingEdges %}static bool enabled_{$edge.name}(StateType const& state) {
{% for edge in nonSynchronizingEdges %}static bool edge_enabled_{$edge.name}(StateType const& state) {
if ({$edge.guard}) { if ({$edge.guard}) {
return true; return true;
} }
return false; return false;
} }
static void perform_{$edge.name}(StateType const& state) {
{% for destination in edge.destinations %}
static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType& state) {
{% for level in destination.levels %}if (level == {$level.index}) {
{% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value};{% endfor %}
} }
static void lowestLevel_{$edge.name}() {
return {$edge.lowestLevel};
{% endfor %}
} }
static void highestLevel_{$edge.name}() {
return {$edge.highestLevel};
static void destination_perform_{$edge.name}_{$destination.name}(StateType& state) {
{% for level in destination.levels %}
{% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value};
{% endfor %}
{% endfor %}
} }
{% endfor %} {% endfor %}
{% endfor %}
typedef void (*DestinationLevelFunctionPtr)(int_fast64_t, StateType&);
typedef void (*DestinationFunctionPtr)(StateType&);
{% for edge in nonSynchronizingEdges %}class Edge_{$edge.name} {
class Destination {
public: public:
bool isEnabled(StateType const& state) {
if ({$edge.guard}) {
return true;
Destination() : mLowestLevel(0), mHighestLevel(0), mValue(), destinationLevelFunction(nullptr), destinationFunction(nullptr) {
// Intentionally left empty.
} }
return false;
Destination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction) : mLowestLevel(lowestLevel), mHighestLevel(highestLevel), mValue(value), destinationLevelFunction(destinationLevelFunction), destinationFunction(destinationFunction) {
// Intentionally left empty.
} }
{% for destination in edge.destinations %}class Destination_{$destination.name} {
public:
int_fast64_t lowestLevel() const { int_fast64_t lowestLevel() const {
return {$destination.lowestLevel};
return mLowestLevel;
} }
int_fast64_t highestLevel() const { int_fast64_t highestLevel() const {
return {$destination.highestLevel};
return mHighestLevel;
} }
void performAssignments(int_fast64_t level, StateType& state) {
{% for level in destination.levels %}if (level == {$level.index}) {
{% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value};
{% endfor %}
}{% endfor %}
ValueType const& value() const {
return mValue;
}
void performLevel(int_fast64_t level, StateType& state) const {
destinationLevelFunction(level, state);
} }
void perform(StateType& state) const {
destinationFunction(state);
}
private:
int_fast64_t mLowestLevel;
int_fast64_t mHighestLevel;
ValueType mValue;
DestinationLevelFunctionPtr destinationLevelFunction;
DestinationFunctionPtr destinationFunction;
}; };
{% endfor %}
typedef bool (*EdgeEnabledFunctionPtr)(StateType const&);
class Edge {
public:
typedef std::vector<Destination> ContainerType;
Edge() : edgeEnabledFunction(nullptr) {
// Intentionally left empty.
}
Edge(EdgeEnabledFunctionPtr edgeEnabledFunction) : edgeEnabledFunction(edgeEnabledFunction) {
// Intentionally left empty.
}
bool isEnabled(StateType const& state) const {
return edgeEnabledFunction(state);
}
void addDestination(Destination const& destination) {
destinations.push_back(destination);
}
void addDestination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction) {
destinations.emplace_back(lowestLevel, highestLevel, value, destinationLevelFunction, destinationFunction);
}
std::vector<Destination> const& getDestinations() const {
return destinations;
}
ContainerType::const_iterator begin() const {
return destinations.begin();
}
ContainerType::const_iterator end() const {
return destinations.end();
}
private:
EdgeEnabledFunctionPtr edgeEnabledFunction;
ContainerType destinations;
}; };
{% endfor %}
class JitBuilder : public JitModelBuilderInterface<IndexType, ValueType> { class JitBuilder : public JitModelBuilderInterface<IndexType, ValueType> {
public: public:
@ -216,8 +273,15 @@ namespace storm {
{% for state in initialStates %}{ {% for state in initialStates %}{
StateType state; StateType state;
{% for assignment in state %}state.{$assignment.variable} = {$assignment.value}; {% for assignment in state %}state.{$assignment.variable} = {$assignment.value};
{% endfor %}initialStates.push_back(state);
{% endfor %}
initialStates.push_back(state);
}{% endfor %} }{% endfor %}
{% for edge in nonSynchronizingEdges %}{
edge_{$edge.name} = Edge(&edge_enabled_{$edge.name});
{% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name});
{% endfor %}
}
{% endfor %}
} }
virtual storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>* build() override { virtual storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>* build() override {
@ -297,8 +361,25 @@ namespace storm {
return false; return false;
} }
void exploreNonSynchronizingEdges(StateType const& sourceState, IndexType const& currentIndex, StateBehaviour<IndexType, ValueType>& behaviour, StateSet& statesToExplore) {
void exploreNonSynchronizingEdges(StateType const& state, IndexType const& currentIndex, StateBehaviour<IndexType, ValueType>& behaviour, StateSet& statesToExplore) {
{% for edge in nonSynchronizingEdges %}{
{% for destination in edge.destinations %}{
if ({$edge.guard}) {
Choice<IndexType, ValueType>& choice = behaviour.addChoice();
{% for destination in edge.destinations %}{
StateType targetState(state);
destination_perform_{$edge.name}_{$destination.name}(targetState);
//for (auto const& destination : edge_{$edge.name}) {
//destination.perform(targetState);
IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore);
choice.add(targetStateIndex, {$destination.value});
//}
}{% endfor %}
}
}
{% endfor %}
}
{% endfor %}
} }
IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) { IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) {
@ -341,6 +422,9 @@ namespace storm {
spp::sparse_hash_map<StateType, IndexType> stateIds; spp::sparse_hash_map<StateType, IndexType> stateIds;
std::vector<StateType> initialStates; std::vector<StateType> initialStates;
std::vector<IndexType> deadlockStates; std::vector<IndexType> deadlockStates;
{% for edge in nonSynchronizingEdges %}Edge edge_{$edge.name};
{% endfor %}
}; };
BOOST_DLL_ALIAS(storm::builder::jit::JitBuilder::create, create_builder) BOOST_DLL_ALIAS(storm::builder::jit::JitBuilder::create, create_builder)
@ -635,6 +719,7 @@ namespace storm {
cpptempl::data_list levels = generateLevels(destination.getOrderedAssignments()); cpptempl::data_list levels = generateLevels(destination.getOrderedAssignments());
destinationData["name"] = asString(destinationIndex); destinationData["name"] = asString(destinationIndex);
destinationData["levels"] = cpptempl::make_data(levels); destinationData["levels"] = cpptempl::make_data(levels);
destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(destination.getProbability()), storm::expressions::ToCppTranslationOptions("state.", "double"));
destinationData["lowestLevel"] = asString(destination.getOrderedAssignments().getLowestLevel()); destinationData["lowestLevel"] = asString(destination.getOrderedAssignments().getLowestLevel());
destinationData["highestLevel"] = asString(destination.getOrderedAssignments().getHighestLevel()); destinationData["highestLevel"] = asString(destination.getOrderedAssignments().getHighestLevel());

2
src/builder/jit/StateBehaviour.cpp
View File

@ -43,6 +43,8 @@ namespace storm {
choices.front().divideDistribution(static_cast<ValueType>(totalCount)); choices.front().divideDistribution(static_cast<ValueType>(totalCount));
} }
} }
} else if (choices.size() == 1) {
choices.front().compress();
} }
} }

Write Preview
Loading…
Cancel
Save