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

aliased BitVector, used state_t more (cosmetic)

tempestpy_adaptions
tomjanson 9 years ago
committed by Tom Janson
parent
235671d67d
commit
55599b51e7
3 changed files with 13 additions and 12 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. 4
      src/utility/shortestPaths.cpp
  2. 3
      src/utility/shortestPaths.h
  3. 18
      test/functional/utility/KSPTest.cpp

4
src/utility/shortestPaths.cpp
View File

@ -52,9 +52,9 @@ namespace storm {
}
template <typename T>
storage::BitVector ShortestPathsGenerator<T>::getStates(unsigned long k) {
BitVector ShortestPathsGenerator<T>::getStates(unsigned long k) {
computeKSP(k);
storage::BitVector stateSet(numStates - 1, false); // no meta-target
BitVector stateSet(numStates - 1, false); // no meta-target
Path<T> currentPath = kShortestPaths[metaTarget][k - 1];
boost::optional<state_t> maybePredecessor = currentPath.predecessorNode;

3
src/utility/shortestPaths.h
View File

@ -26,6 +26,7 @@ namespace storm {
namespace ksp {
typedef storage::sparse::state_type state_t;
typedef std::vector<state_t> state_list_t;
using BitVector = storage::BitVector;
template <typename T>
struct Path {
@ -100,8 +101,8 @@ namespace storm {
storage::SparseMatrix<T> transitionMatrix;
state_t numStates; // includes meta-target, i.e. states in model + 1
state_t metaTarget;
storage::BitVector initialStates;
state_list_t targets;
BitVector initialStates;
std::unordered_map<state_t, T> targetProbMap;
std::vector<state_list_t> graphPredecessors;

18
test/functional/utility/KSPTest.cpp
View File

@ -25,7 +25,7 @@ std::shared_ptr<storm::models::sparse::Model<double>> buildExampleModel() {
TEST(KSPTest, dijkstra) {
auto model = buildExampleModel();
storm::storage::sparse::state_type testState = 300;
storm::utility::ksp::state_t testState = 300;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
double dist = spg.getDistance(1);
@ -35,7 +35,7 @@ TEST(KSPTest, dijkstra) {
TEST(KSPTest, singleTarget) {
auto model = buildExampleModel();
storm::storage::sparse::state_type testState = 300;
storm::utility::ksp::state_t testState = 300;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
double dist = spg.getDistance(100);
@ -45,7 +45,7 @@ TEST(KSPTest, singleTarget) {
TEST(KSPTest, reentry) {
auto model = buildExampleModel();
storm::storage::sparse::state_type testState = 300;
storm::utility::ksp::state_t testState = 300;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
double dist = spg.getDistance(100);
@ -59,7 +59,7 @@ TEST(KSPTest, reentry) {
TEST(KSPTest, groupTarget) {
auto model = buildExampleModel();
auto groupTarget = storm::utility::ksp::state_list_t{50, 90};
auto groupTarget = std::vector<storm::utility::ksp::state_t>{50, 90};
auto spg = storm::utility::ksp::ShortestPathsGenerator<double>(model, groupTarget);
// this path should lead to 90
@ -78,7 +78,7 @@ TEST(KSPTest, groupTarget) {
TEST(KSPTest, kTooLargeException) {
auto model = buildExampleModel();
storm::storage::sparse::state_type testState = 1;
storm::utility::ksp::state_t testState = 1;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
ASSERT_THROW(spg.getDistance(2), std::invalid_argument);
@ -87,11 +87,11 @@ TEST(KSPTest, kTooLargeException) {
TEST(KSPTest, kspStateSet) {
auto model = buildExampleModel();
storm::storage::sparse::state_type testState = 300;
storm::utility::ksp::state_t testState = 300;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
storm::storage::BitVector referenceBV(model->getNumberOfStates(), false);
for (auto s : storm::utility::ksp::state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}) {
for (auto s : std::vector<storm::utility::ksp::state_t>{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0}) {
referenceBV.set(s, true);
}
@ -103,11 +103,11 @@ TEST(KSPTest, kspStateSet) {
TEST(KSPTest, kspPathAsList) {
auto model = buildExampleModel();
storm::storage::sparse::state_type testState = 300;
storm::utility::ksp::state_t testState = 300;
storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
// TODO: use path that actually has a loop or something to make this more interesting
auto reference = storm::utility::ksp::state_list_t{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0};
auto reference = std::vector<storm::utility::ksp::state_t>{300, 293, 285, 279, 271, 265, 259, 252, 244, 237, 229, 223, 217, 210, 202, 195, 187, 181, 175, 168, 160, 153, 145, 139, 133, 126, 118, 111, 103, 97, 91, 84, 76, 69, 61, 55, 49, 43, 35, 41, 32, 25, 19, 14, 10, 7, 4, 2, 1, 0};
auto list = spg.getPathAsList(7);
EXPECT_EQ(list, reference);

Write Preview
Loading…
Cancel
Save