|
|
@ -6,15 +6,13 @@ |
|
|
|
#include "storm/parser/PrismParser.h"
|
|
|
|
#include "storm/storage/SymbolicModelDescription.h"
|
|
|
|
#include "storm/utility/graph.h"
|
|
|
|
#include "storm/utility/shortestPaths.cpp"
|
|
|
|
#include "storm/utility/shortestPaths.h"
|
|
|
|
|
|
|
|
// NOTE: The KSPs / distances of these tests were generated by the
|
|
|
|
// KSP-Generator itself and checked for gross implausibility, but no
|
|
|
|
// more than that.
|
|
|
|
// An independent verification of the values would be really nice ...
|
|
|
|
|
|
|
|
// FIXME: (almost) all of these fail; the question is: is there actually anything wrong or does the new parser yield a different order of states?
|
|
|
|
|
|
|
|
std::shared_ptr<storm::models::sparse::Model<double>> buildExampleModel() { |
|
|
|
std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"; |
|
|
|
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath); |
|
|
@ -61,16 +59,12 @@ TEST(KSPTest, groupTarget) { |
|
|
|
auto groupTarget = std::vector<storm::utility::ksp::state_t>{50, 90}; |
|
|
|
auto spg = storm::utility::ksp::ShortestPathsGenerator<double>(*model, groupTarget); |
|
|
|
|
|
|
|
// FIXME comments are outdated (but does it even matter?)
|
|
|
|
// this path should lead to 90
|
|
|
|
double dist1 = spg.getDistance(8); |
|
|
|
EXPECT_DOUBLE_EQ(0.00018449245583999996, dist1); |
|
|
|
|
|
|
|
// this one to 50
|
|
|
|
double dist2 = spg.getDistance(9); |
|
|
|
EXPECT_DOUBLE_EQ(0.00018449245583999996, dist2); |
|
|
|
|
|
|
|
// this one to 90 again
|
|
|
|
double dist3 = spg.getDistance(12); |
|
|
|
EXPECT_DOUBLE_EQ(7.5303043199999984e-06, dist3); |
|
|
|
} |
|
|
|