KSPTest.cpp

Go to the documentation of this file.

#include "storm-config.h"
#include "test/storm_gtest.h"
 
#include "storm-parsers/parser/PrismParser.h"
#include "storm/builder/ExplicitModelBuilder.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/utility/graph.h"
#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 ...
 
class KSPTest : public ::testing::Test {
   protected:
    void SetUp() override {
#ifndef STORM_HAVE_Z3
        GTEST_SKIP() << "Z3 not available.";
#endif
    }
};
 
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);
    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
    return storm::builder::ExplicitModelBuilder<double>(program).build();
}
 
// NOTE: these are hardcoded (obviously), but the model's state indices might change
// (e.g., when the parser or model builder are changed)
// [state 296 seems to be the new index of the old state 300 (checked a few ksps' probs)]
const storm::utility::ksp::state_t testState = 296;
const storm::utility::ksp::state_t stateWithOnlyOnePath = 1;
 
TEST_F(KSPTest, dijkstra) {
    auto model = buildExampleModel();
    storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
 
    double dist = spg.getDistance(1);
    EXPECT_NEAR(0.015859334652581887, dist, 1e-12);
}
 
TEST_F(KSPTest, singleTarget) {
    auto model = buildExampleModel();
    storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
 
    double dist = spg.getDistance(100);
    EXPECT_NEAR(1.5231305000339662e-06, dist, 1e-12);
}
 
TEST_F(KSPTest, reentry) {
    auto model = buildExampleModel();
    storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
 
    double dist = spg.getDistance(100);
    EXPECT_NEAR(1.5231305000339662e-06, dist, 1e-12);
 
    // get another distance to ensure re-entry is no problem
    double dist2 = spg.getDistance(500);
    EXPECT_NEAR(3.0462610000679315e-08, dist2, 1e-12);
}
 
TEST_F(KSPTest, groupTarget) {
    auto model = buildExampleModel();
    auto groupTarget = std::vector<storm::utility::ksp::state_t>{50, 90};
    auto spg = storm::utility::ksp::ShortestPathsGenerator<double>(*model, groupTarget);
 
    double dist1 = spg.getDistance(8);
    EXPECT_NEAR(0.00018449245583999996, dist1, 1e-12);
 
    double dist2 = spg.getDistance(9);
    EXPECT_NEAR(0.00018449245583999996, dist2, 1e-12);
 
    double dist3 = spg.getDistance(12);
    EXPECT_NEAR(7.5303043199999984e-06, dist3, 1e-12);
}
 
TEST_F(KSPTest, kTooLargeException) {
    auto model = buildExampleModel();
    storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, stateWithOnlyOnePath);
 
    STORM_SILENT_ASSERT_THROW(spg.getDistance(2), std::invalid_argument);
}
 
TEST_F(KSPTest, kspStateSet) {
    auto model = buildExampleModel();
    storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
 
    auto bv = spg.getStates(7);
    EXPECT_EQ(50ull, bv.getNumberOfSetBits());
 
    // The result may sadly depend on the compiler/system, so checking a particular outcome is not feasible.
    //    storm::storage::BitVector referenceBV(model->getNumberOfStates(), false);
    //    for (auto s : std::vector<storm::utility::ksp::state_t>{0, 1, 2, 4, 6, 9, 12, 17, 22, 30, 37, 45, 52, 58, 65, 70, 74, 77, 81, 85, 92, 98, 104, 112,
    //    119, 127, 134, 140, 146, 154, 161, 169, 176, 182, 188, 196, 203, 211, 218, 224, 230, 238, 245, 253, 260, 266, 272, 281, 288, 296}) {
    //        referenceBV.set(s, true);
    //    }
    //
    //    EXPECT_EQ(referenceBV, bv);
}
 
TEST_F(KSPTest, kspPathAsList) {
    auto model = buildExampleModel();
    storm::utility::ksp::ShortestPathsGenerator<double> spg(*model, testState);
 
    auto list = spg.getPathAsList(7);
    EXPECT_EQ(50ull, list.size());
 
    // TODO: use path that actually has a loop or something to make this more interesting
    //    auto reference = storm::utility::ksp::OrderedStateList{296, 288, 281, 272, 266, 260, 253, 245, 238, 230, 224, 218, 211, 203, 196, 188, 182, 176, 169,
    //    161, 154, 146, 140, 134, 127, 119, 112, 104, 98, 92, 85, 77, 70, 81, 74, 65, 58, 52, 45, 37, 30, 22, 17, 12, 9, 6, 4, 2, 1, 0}; EXPECT_EQ(reference,
    //    list);
}