From ca9cce5d299d436a70df60ae1809dcc165d3ea1a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 24 Nov 2025 15:49:51 +0100 Subject: [PATCH 01/11] Replaced boost::mt19937 by std::mt19937 for DFT simulator --- src/storm-dft/simulator/DFTTraceSimulator.cpp | 4 ++-- src/storm-dft/simulator/DFTTraceSimulator.h | 6 +++--- src/storm/utility/random.cpp | 4 ++-- src/storm/utility/random.h | 8 +++---- .../storm-dft/simulator/DftSimulatorTest.cpp | 7 +------ .../simulator/DftTraceGeneratorTest.cpp | 21 +++---------------- .../simulator/ImportanceFunction.cpp | 8 +------ src/test/storm-dft/simulator/SamplingTest.cpp | 8 +------ 8 files changed, 17 insertions(+), 49 deletions(-) diff --git a/src/storm-dft/simulator/DFTTraceSimulator.cpp b/src/storm-dft/simulator/DFTTraceSimulator.cpp index f5cbb34015..b8e29f7863 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.cpp +++ b/src/storm-dft/simulator/DFTTraceSimulator.cpp @@ -5,14 +5,14 @@ namespace simulator { template DFTTraceSimulator::DFTTraceSimulator(storm::dft::storage::DFT const& dft, - storm::dft::storage::DFTStateGenerationInfo const& stateGenerationInfo, boost::mt19937& randomGenerator) + storm::dft::storage::DFTStateGenerationInfo const& stateGenerationInfo, std::mt19937& randomGenerator) : dft(dft), stateGenerationInfo(stateGenerationInfo), generator(dft, stateGenerationInfo), randomGenerator(randomGenerator) { // Set initial state resetToInitial(); } template -void DFTTraceSimulator::setRandomNumberGenerator(boost::mt19937& randomNumberGenerator) { +void DFTTraceSimulator::setRandomNumberGenerator(std::mt19937& randomNumberGenerator) { this->randomGenerator = randomNumberGenerator; } diff --git a/src/storm-dft/simulator/DFTTraceSimulator.h b/src/storm-dft/simulator/DFTTraceSimulator.h index 4fa0b92002..c331b128bc 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.h +++ b/src/storm-dft/simulator/DFTTraceSimulator.h @@ -41,14 +41,14 @@ class DFTTraceSimulator { * @param randomGenerator Random number generator. */ DFTTraceSimulator(storm::dft::storage::DFT const& dft, storm::dft::storage::DFTStateGenerationInfo const& stateGenerationInfo, - boost::mt19937& randomGenerator); + std::mt19937& randomGenerator); /*! * Set the random number generator. * * @param randomNumberGenerator Random number generator. */ - void setRandomNumberGenerator(boost::mt19937& randomNumberGenerator); + void setRandomNumberGenerator(std::mt19937& randomNumberGenerator); /*! * Set the current state back to the initial state in order to start a new simulation. @@ -145,7 +145,7 @@ class DFTTraceSimulator { double time; // Random number generator - boost::mt19937& randomGenerator; + std::mt19937& randomGenerator; }; } // namespace simulator diff --git a/src/storm/utility/random.cpp b/src/storm/utility/random.cpp index fbd0f9e2ff..50adf76fd6 100644 --- a/src/storm/utility/random.cpp +++ b/src/storm/utility/random.cpp @@ -36,13 +36,13 @@ uint64_t RandomProbabilityGenerator::random_uint(uint64_t min, u BernoulliDistributionGenerator::BernoulliDistributionGenerator(double prob) : distribution(prob) {} -bool BernoulliDistributionGenerator::random(boost::mt19937& engine) { +bool BernoulliDistributionGenerator::random(std::mt19937& engine) { return distribution(engine); } ExponentialDistributionGenerator::ExponentialDistributionGenerator(double rate) : distribution(rate) {} -double ExponentialDistributionGenerator::random(boost::mt19937& engine) { +double ExponentialDistributionGenerator::random(std::mt19937& engine) { return distribution(engine); } } // namespace utility diff --git a/src/storm/utility/random.h b/src/storm/utility/random.h index fb4f16e774..bbac3b1c3b 100644 --- a/src/storm/utility/random.h +++ b/src/storm/utility/random.h @@ -44,19 +44,19 @@ class RandomProbabilityGenerator { class BernoulliDistributionGenerator { public: BernoulliDistributionGenerator(double prob); - bool random(boost::mt19937& engine); + bool random(std::mt19937& engine); private: - boost::random::bernoulli_distribution<> distribution; + std::bernoulli_distribution distribution; }; class ExponentialDistributionGenerator { public: ExponentialDistributionGenerator(double rate); - double random(boost::mt19937& engine); + double random(std::mt19937& engine); private: - boost::random::exponential_distribution<> distribution; + std::exponential_distribution distribution; }; } // namespace utility diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp index 93beba164c..23a51024ed 100644 --- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -25,7 +25,7 @@ std::pair simulateDft(std::string const& file, double timebound, // Init random number generator // storm::utility::setLogLevel(l3pp::LogLevel::TRACE); - boost::mt19937 gen(5u); + std::mt19937 gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, stateGenerationInfo, gen); size_t count = 0; @@ -69,12 +69,7 @@ TEST(DftSimulatorTest, VotingUnreliability) { result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting3.dft", 1, 10000); EXPECT_NEAR(result, 0.3496529873, 0.01); result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting4.dft", 1, 10000); -#if BOOST_VERSION > 106400 EXPECT_NEAR(result, 0.693568287, 0.01); -#else - // Older Boost versions yield different value - EXPECT_NEAR(result, 0.693568287, 0.015); -#endif } TEST(DftSimulatorTest, PandUnreliability) { diff --git a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp index a0feb68aa4..469cababae 100644 --- a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp +++ b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp @@ -151,7 +151,7 @@ TYPED_TEST(DftTraceGeneratorTest, RandomStepsAnd) { EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, pair.second.hasSymmetries()); // Init random number generator - boost::mt19937 gen(5u); + std::mt19937 gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, pair.second, gen); auto state = simulator.getCurrentState(); @@ -160,19 +160,13 @@ TYPED_TEST(DftTraceGeneratorTest, RandomStepsAnd) { // First random step storm::dft::simulator::SimulationStepResult res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); -#if BOOST_VERSION > 106400 - // Older Boost versions yield different value EXPECT_NEAR(simulator.getCurrentTime(), 0.522079, 1e-6); -#endif state = simulator.getCurrentState(); EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); -#if BOOST_VERSION > 106400 - // Older Boost versions yield different value EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214, 1e-6); -#endif state = simulator.getCurrentState(); EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); } @@ -183,7 +177,7 @@ TYPED_TEST(DftTraceGeneratorTest, Reset) { EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, pair.second.hasSymmetries()); // Init random number generator - boost::mt19937 gen(5u); + std::mt19937 gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, pair.second, gen); auto state = simulator.getCurrentState(); @@ -192,19 +186,13 @@ TYPED_TEST(DftTraceGeneratorTest, Reset) { // First random step storm::dft::simulator::SimulationStepResult res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); -#if BOOST_VERSION > 106400 - // Older Boost versions yield different value EXPECT_NEAR(simulator.getCurrentTime(), 0.522079, 1e-6); -#endif auto stateStep1 = simulator.getCurrentState(); EXPECT_FALSE(stateStep1->hasFailed(dft->getTopLevelIndex())); res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); -#if BOOST_VERSION > 106400 - // Older Boost versions yield different value EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214, 1e-6); -#endif state = simulator.getCurrentState(); EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); @@ -215,10 +203,7 @@ TYPED_TEST(DftTraceGeneratorTest, Reset) { res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); -#if BOOST_VERSION > 106400 - // Older Boost versions yield different value EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214 + 2.4686932, 1e-6); -#endif state = simulator.getCurrentState(); EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); } @@ -228,7 +213,7 @@ TYPED_TEST(DftTraceGeneratorTest, Fdep) { auto dft = pair.first; // Init random number generator. Will not be important as we are choosing the steps deterministically. - boost::mt19937 gen(5u); + std::mt19937 gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, pair.second, gen); // Start with initial state diff --git a/src/test/storm-dft/simulator/ImportanceFunction.cpp b/src/test/storm-dft/simulator/ImportanceFunction.cpp index 8a3ee078cb..a4c250fc3d 100644 --- a/src/test/storm-dft/simulator/ImportanceFunction.cpp +++ b/src/test/storm-dft/simulator/ImportanceFunction.cpp @@ -28,7 +28,7 @@ TEST(ImportanceFunctionTest, RandomStepsAnd) { auto dft = pair.first; // Init random number generator - boost::mt19937 gen(5u); + std::mt19937 gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, pair.second, gen); // Init importance function @@ -44,20 +44,14 @@ TEST(ImportanceFunctionTest, RandomStepsAnd) { // First random step storm::dft::simulator::SimulationStepResult res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); -#if BOOST_VERSION > 106400 - // Older Boost versions yield different value EXPECT_NEAR(simulator.getCurrentTime(), 0.522079, 1e-6); -#endif state = simulator.getCurrentState(); EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); EXPECT_EQ(imp.getImportance(state), 1); res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); -#if BOOST_VERSION > 106400 - // Older Boost versions yield different value EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214, 1e-6); -#endif state = simulator.getCurrentState(); EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); EXPECT_EQ(imp.getImportance(state), 2); diff --git a/src/test/storm-dft/simulator/SamplingTest.cpp b/src/test/storm-dft/simulator/SamplingTest.cpp index 1fb4003fe4..b77f8a0d98 100644 --- a/src/test/storm-dft/simulator/SamplingTest.cpp +++ b/src/test/storm-dft/simulator/SamplingTest.cpp @@ -6,13 +6,7 @@ namespace { TEST(SamplingTest, SampleExponential) { -#if BOOST_VERSION < 106400 - // Boost changed implementation of exponential distribution - // -> different values are returned - GTEST_SKIP(); - return; -#endif - boost::mt19937 gen(5u); + std::mt19937 gen(5u); storm::utility::ExponentialDistributionGenerator dist(5); // Ensure that pseudo random numbers are the same on all machines From e29fae499ac22bbbd99f6701bc655b1aa1c5a658 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 24 Nov 2025 15:50:53 +0100 Subject: [PATCH 02/11] Updated results after changing RNG --- src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp | 10 +++++----- src/test/storm-dft/simulator/ImportanceFunction.cpp | 4 ++-- src/test/storm-dft/simulator/SamplingTest.cpp | 4 ++-- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp index 469cababae..b25b620324 100644 --- a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp +++ b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp @@ -160,13 +160,13 @@ TYPED_TEST(DftTraceGeneratorTest, RandomStepsAnd) { // First random step storm::dft::simulator::SimulationStepResult res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); - EXPECT_NEAR(simulator.getCurrentTime(), 0.522079, 1e-6); + EXPECT_NEAR(simulator.getCurrentTime(), 0.113522, 1e-6); state = simulator.getCurrentState(); EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); - EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214, 1e-6); + EXPECT_NEAR(simulator.getCurrentTime(), 0.113522 + 0.904286, 1e-6); state = simulator.getCurrentState(); EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); } @@ -186,13 +186,13 @@ TYPED_TEST(DftTraceGeneratorTest, Reset) { // First random step storm::dft::simulator::SimulationStepResult res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); - EXPECT_NEAR(simulator.getCurrentTime(), 0.522079, 1e-6); + EXPECT_NEAR(simulator.getCurrentTime(), 0.113522, 1e-6); auto stateStep1 = simulator.getCurrentState(); EXPECT_FALSE(stateStep1->hasFailed(dft->getTopLevelIndex())); res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); - EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214, 1e-6); + EXPECT_NEAR(simulator.getCurrentTime(), 0.113522 + 0.904286, 1e-6); state = simulator.getCurrentState(); EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); @@ -203,7 +203,7 @@ TYPED_TEST(DftTraceGeneratorTest, Reset) { res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); - EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214 + 2.4686932, 1e-6); + EXPECT_NEAR(simulator.getCurrentTime(), 0.113522 + 0.904286 + 7.769302, 1e-6); state = simulator.getCurrentState(); EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); } diff --git a/src/test/storm-dft/simulator/ImportanceFunction.cpp b/src/test/storm-dft/simulator/ImportanceFunction.cpp index a4c250fc3d..c3ac70d9af 100644 --- a/src/test/storm-dft/simulator/ImportanceFunction.cpp +++ b/src/test/storm-dft/simulator/ImportanceFunction.cpp @@ -44,14 +44,14 @@ TEST(ImportanceFunctionTest, RandomStepsAnd) { // First random step storm::dft::simulator::SimulationStepResult res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); - EXPECT_NEAR(simulator.getCurrentTime(), 0.522079, 1e-6); + EXPECT_NEAR(simulator.getCurrentTime(), 0.113522, 1e-6); state = simulator.getCurrentState(); EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex())); EXPECT_EQ(imp.getImportance(state), 1); res = simulator.randomStep(); EXPECT_EQ(res, storm::dft::simulator::SimulationStepResult::SUCCESSFUL); - EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214, 1e-6); + EXPECT_NEAR(simulator.getCurrentTime(), 0.113522 + 0.904286, 1e-6); state = simulator.getCurrentState(); EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex())); EXPECT_EQ(imp.getImportance(state), 2); diff --git a/src/test/storm-dft/simulator/SamplingTest.cpp b/src/test/storm-dft/simulator/SamplingTest.cpp index b77f8a0d98..5697719023 100644 --- a/src/test/storm-dft/simulator/SamplingTest.cpp +++ b/src/test/storm-dft/simulator/SamplingTest.cpp @@ -10,8 +10,8 @@ TEST(SamplingTest, SampleExponential) { storm::utility::ExponentialDistributionGenerator dist(5); // Ensure that pseudo random numbers are the same on all machines - double reference[] = {0.18241937154, 0.0522078772595, 0.0949721368604, 0.246869315378, 0.765000791199, - 0.0177096648877, 0.225167598601, 0.23538530391, 1.01605360643, 0.138846355094}; + double reference[] = {0.011352194735198223, 0.35595966617002761, 0.0904286229501646, 0.77693019063043178, 0.018822806624073801, + 0.10108027454097809, 0.087433897364154994, 0.13335480534208866, 0.93816592681955202, 0.33034562021306652}; for (int i = 0; i < 10; ++i) { EXPECT_NEAR(dist.random(gen), reference[i], 1e-10); } From fc019006aa25a45425691a7b9364c26e050e044f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 24 Nov 2025 15:57:20 +0100 Subject: [PATCH 03/11] Test files end with suffix Test.cpp --- doc/developers.md | 3 +++ .../bdd/{TestBddModularizer.cpp => BddModularizerTest.cpp} | 0 .../bdd/{TestBddVarOrdering.cpp => BddVarOrderingTest.cpp} | 4 ++-- src/test/storm-dft/bdd/{TestBdd.cpp => SftBddTest.cpp} | 0 .../{ImportanceFunction.cpp => ImportanceFunctionTest.cpp} | 0 ...rismProgramSimulator.cpp => PrismProgramSimulatorTest.cpp} | 0 ...niLocalEliminatorTests.cpp => JaniLocalEliminatorTest.cpp} | 0 7 files changed, 5 insertions(+), 2 deletions(-) rename src/test/storm-dft/bdd/{TestBddModularizer.cpp => BddModularizerTest.cpp} (100%) rename src/test/storm-dft/bdd/{TestBddVarOrdering.cpp => BddVarOrderingTest.cpp} (97%) rename src/test/storm-dft/bdd/{TestBdd.cpp => SftBddTest.cpp} (100%) rename src/test/storm-dft/simulator/{ImportanceFunction.cpp => ImportanceFunctionTest.cpp} (100%) rename src/test/storm/simulator/{PrismProgramSimulator.cpp => PrismProgramSimulatorTest.cpp} (100%) rename src/test/storm/storage/{JaniLocalEliminatorTests.cpp => JaniLocalEliminatorTest.cpp} (100%) diff --git a/doc/developers.md b/doc/developers.md index 27bc3b145d..05e8b0af52 100644 --- a/doc/developers.md +++ b/doc/developers.md @@ -59,6 +59,9 @@ The following contains some general guidelines for developers. #include ... ``` +### File structure +- Test files in `src/test/` end with the suffix `*Test.cpp`. + ### Output - We provide custom macros for output and logging. The use of `std::cout` should be avoided and instead, macros such as `STORM_LOG_DEBUG`, `STORM_LOG_INFO` or `STORM_PRINT_AND_LOG` should be used. diff --git a/src/test/storm-dft/bdd/TestBddModularizer.cpp b/src/test/storm-dft/bdd/BddModularizerTest.cpp similarity index 100% rename from src/test/storm-dft/bdd/TestBddModularizer.cpp rename to src/test/storm-dft/bdd/BddModularizerTest.cpp diff --git a/src/test/storm-dft/bdd/TestBddVarOrdering.cpp b/src/test/storm-dft/bdd/BddVarOrderingTest.cpp similarity index 97% rename from src/test/storm-dft/bdd/TestBddVarOrdering.cpp rename to src/test/storm-dft/bdd/BddVarOrderingTest.cpp index aa7720430a..f6e9ee634d 100644 --- a/src/test/storm-dft/bdd/TestBddVarOrdering.cpp +++ b/src/test/storm-dft/bdd/BddVarOrderingTest.cpp @@ -7,7 +7,7 @@ namespace { -TEST(TestBddVarOrdering, VariableOrdering) { +TEST(BddVarOrderingTest, VariableOrdering) { #ifdef STORM_HAVE_SYLVAN auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft"); auto manager{std::make_shared()}; @@ -42,7 +42,7 @@ TEST(TestBddVarOrdering, VariableOrdering) { #endif } -TEST(TestBddVarOrdering, OrderParser) { +TEST(BddVarOrderingTest, OrderParser) { #ifdef STORM_HAVE_SYLVAN auto dft = storm::dft::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft"); diff --git a/src/test/storm-dft/bdd/TestBdd.cpp b/src/test/storm-dft/bdd/SftBddTest.cpp similarity index 100% rename from src/test/storm-dft/bdd/TestBdd.cpp rename to src/test/storm-dft/bdd/SftBddTest.cpp diff --git a/src/test/storm-dft/simulator/ImportanceFunction.cpp b/src/test/storm-dft/simulator/ImportanceFunctionTest.cpp similarity index 100% rename from src/test/storm-dft/simulator/ImportanceFunction.cpp rename to src/test/storm-dft/simulator/ImportanceFunctionTest.cpp diff --git a/src/test/storm/simulator/PrismProgramSimulator.cpp b/src/test/storm/simulator/PrismProgramSimulatorTest.cpp similarity index 100% rename from src/test/storm/simulator/PrismProgramSimulator.cpp rename to src/test/storm/simulator/PrismProgramSimulatorTest.cpp diff --git a/src/test/storm/storage/JaniLocalEliminatorTests.cpp b/src/test/storm/storage/JaniLocalEliminatorTest.cpp similarity index 100% rename from src/test/storm/storage/JaniLocalEliminatorTests.cpp rename to src/test/storm/storage/JaniLocalEliminatorTest.cpp From c7d6dd41346e79a5dcb8799324edd4fd3b670a47 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 25 Nov 2025 22:17:21 +0100 Subject: [PATCH 04/11] Unified RandomGenerator --- src/storm-dft/simulator/DFTTraceSimulator.cpp | 16 +++--- src/storm-dft/simulator/DFTTraceSimulator.h | 11 ++-- .../DiscreteTimeSparseModelSimulator.cpp | 4 +- src/storm/simulator/PrismProgramSimulator.cpp | 2 +- src/storm/utility/random.cpp | 53 +++++++++++-------- src/storm/utility/random.h | 48 +++++++---------- .../storm-dft/simulator/DftSimulatorTest.cpp | 3 +- .../simulator/DftTraceGeneratorTest.cpp | 6 +-- .../simulator/ImportanceFunctionTest.cpp | 2 +- src/test/storm-dft/simulator/SamplingTest.cpp | 5 +- 10 files changed, 74 insertions(+), 76 deletions(-) diff --git a/src/storm-dft/simulator/DFTTraceSimulator.cpp b/src/storm-dft/simulator/DFTTraceSimulator.cpp index b8e29f7863..7c6f94dd88 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.cpp +++ b/src/storm-dft/simulator/DFTTraceSimulator.cpp @@ -5,15 +5,16 @@ namespace simulator { template DFTTraceSimulator::DFTTraceSimulator(storm::dft::storage::DFT const& dft, - storm::dft::storage::DFTStateGenerationInfo const& stateGenerationInfo, std::mt19937& randomGenerator) + storm::dft::storage::DFTStateGenerationInfo const& stateGenerationInfo, + storm::utility::RandomProbabilityGenerator randomGenerator) : dft(dft), stateGenerationInfo(stateGenerationInfo), generator(dft, stateGenerationInfo), randomGenerator(randomGenerator) { // Set initial state resetToInitial(); } template -void DFTTraceSimulator::setRandomNumberGenerator(std::mt19937& randomNumberGenerator) { - this->randomGenerator = randomNumberGenerator; +void DFTTraceSimulator::setRandomGenerator(storm::utility::RandomProbabilityGenerator randomGenerator) { + this->randomGenerator = randomGenerator; } template @@ -65,8 +66,7 @@ std::tuple bool successful = true; if (!dependency->isFDEP()) { // Flip a coin whether the PDEP is successful - storm::utility::BernoulliDistributionGenerator probGenerator(dependency->probability()); - successful = probGenerator.random(randomGenerator); + successful = randomGenerator.randomProbability() <= dependency->probability(); } STORM_LOG_TRACE("Let dependency " << *dependency << " " << (successful ? "successfully" : "unsuccessfully") << " fail"); return std::make_tuple(iterFailable, 0, successful); @@ -75,15 +75,13 @@ std::tuple // Initialize with first BE storm::dft::storage::FailableElements::const_iterator nextFail = iterFailable; double rate = state->getBERate(nextFail.asBE(dft)->id()); - storm::utility::ExponentialDistributionGenerator rateGenerator(rate); - double smallestTimebound = rateGenerator.random(randomGenerator); + double smallestTimebound = randomGenerator.randomExponential(rate); ++iterFailable; // Consider all other BEs and find the one which fails first for (; iterFailable != state->getFailableElements().end(); ++iterFailable) { rate = state->getBERate(iterFailable.asBE(dft)->id()); - rateGenerator = storm::utility::ExponentialDistributionGenerator(rate); - double timebound = rateGenerator.random(randomGenerator); + double timebound = randomGenerator.randomExponential(rate); if (timebound < smallestTimebound) { // BE fails earlier -> use as nextFail nextFail = iterFailable; diff --git a/src/storm-dft/simulator/DFTTraceSimulator.h b/src/storm-dft/simulator/DFTTraceSimulator.h index c331b128bc..f3118871d8 100644 --- a/src/storm-dft/simulator/DFTTraceSimulator.h +++ b/src/storm-dft/simulator/DFTTraceSimulator.h @@ -4,7 +4,6 @@ #include "storm-dft/storage/DFT.h" #include "storm-dft/storage/DFTState.h" #include "storm-dft/storage/FailableElements.h" - #include "storm/utility/random.h" namespace storm::dft { @@ -41,14 +40,14 @@ class DFTTraceSimulator { * @param randomGenerator Random number generator. */ DFTTraceSimulator(storm::dft::storage::DFT const& dft, storm::dft::storage::DFTStateGenerationInfo const& stateGenerationInfo, - std::mt19937& randomGenerator); + storm::utility::RandomProbabilityGenerator randomGenerator); /*! * Set the random number generator. * - * @param randomNumberGenerator Random number generator. + * @param randomGenerator Random number generator. */ - void setRandomNumberGenerator(std::mt19937& randomNumberGenerator); + void setRandomGenerator(storm::utility::RandomProbabilityGenerator randomGenerator); /*! * Set the current state back to the initial state in order to start a new simulation. @@ -144,8 +143,8 @@ class DFTTraceSimulator { // Currently elapsed time double time; - // Random number generator - std::mt19937& randomGenerator; + // Random generator + storm::utility::RandomProbabilityGenerator randomGenerator; }; } // namespace simulator diff --git a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp index d45ce861bd..0381037e68 100644 --- a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp +++ b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp @@ -30,7 +30,7 @@ bool DiscreteTimeSparseModelSimulator::randomStep() if (model.getTransitionMatrix().getRowGroupSize(currentState) == 0) { return false; } - return step(generator.random_uint(0, model.getTransitionMatrix().getRowGroupSize(currentState) - 1)); + return step(generator.randomSelect(0, model.getTransitionMatrix().getRowGroupSize(currentState) - 1)); } template @@ -38,7 +38,7 @@ bool DiscreteTimeSparseModelSimulator::step(uint64_t // TODO lots of optimization potential. // E.g., do not sample random numbers if there is only a single transition lastRewards = zeroRewards; - ValueType probability = generator.random(); + ValueType probability = generator.randomProbability(); STORM_LOG_ASSERT(action < model.getTransitionMatrix().getRowGroupSize(currentState), "Action index higher than number of actions"); uint64_t row = model.getTransitionMatrix().getRowGroupIndices()[currentState] + action; uint64_t i = 0; diff --git a/src/storm/simulator/PrismProgramSimulator.cpp b/src/storm/simulator/PrismProgramSimulator.cpp index fa54f1763f..6207373d48 100644 --- a/src/storm/simulator/PrismProgramSimulator.cpp +++ b/src/storm/simulator/PrismProgramSimulator.cpp @@ -29,7 +29,7 @@ void DiscreteTimePrismProgramSimulator::setSeed(uint64_t newSeed) { template bool DiscreteTimePrismProgramSimulator::step(uint64_t actionNumber) { - uint32_t nextState = behavior.getChoices()[actionNumber].sampleFromDistribution(generator.random()); + uint32_t nextState = behavior.getChoices()[actionNumber].sampleFromDistribution(generator.randomProbability()); lastActionRewards = behavior.getChoices()[actionNumber].getRewards(); STORM_LOG_ASSERT(lastActionRewards.size() == stateGenerator->getNumberOfRewardModels(), "Reward vector should have as many rewards as model."); currentState = idToState[nextState]; diff --git a/src/storm/utility/random.cpp b/src/storm/utility/random.cpp index 50adf76fd6..44d3e93673 100644 --- a/src/storm/utility/random.cpp +++ b/src/storm/utility/random.cpp @@ -2,48 +2,59 @@ #include +#include "storm/exceptions/NotSupportedException.h" +#include "storm/utility/macros.h" + namespace storm { namespace utility { -RandomProbabilityGenerator::RandomProbabilityGenerator() : distribution(0.0, 1.0) { + +RandomProbabilityGenerator::RandomProbabilityGenerator() : probabilityDistribution(0.0, 1.0) { std::random_device rd; engine = std::mt19937(rd()); } -RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) : distribution(0.0, 1.0), engine(seed) {} +RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) : engine(seed), probabilityDistribution(0.0, 1.0) {} + +double RandomProbabilityGenerator::randomProbability() { + return probabilityDistribution(engine); +} -double RandomProbabilityGenerator::random() { - return distribution(engine); +uint64_t RandomProbabilityGenerator::randomSelect(uint64_t min, uint64_t max) { + decltype(uniformDistribution.param()) newInterval(min, max); + uniformDistribution.param(newInterval); + return uniformDistribution(engine); + // return std::uniform_int_distribution(min, max)(engine); } -uint64_t RandomProbabilityGenerator::random_uint(uint64_t min, uint64_t max) { - return std::uniform_int_distribution(min, max)(engine); +double RandomProbabilityGenerator::randomExponential(double rate) { + decltype(exponentialDistribution.param()) newRate(rate); + exponentialDistribution.param(newRate); + return exponentialDistribution(engine); } -RandomProbabilityGenerator::RandomProbabilityGenerator() : distribution(0, std::numeric_limits::max()) { +RandomProbabilityGenerator::RandomProbabilityGenerator() : probabilityDistribution(0, std::numeric_limits::max()) { std::random_device rd; engine = std::mt19937(rd()); } -RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) : distribution(0, std::numeric_limits::max()), engine(seed) {} +RandomProbabilityGenerator::RandomProbabilityGenerator(uint64_t seed) + : engine(seed), probabilityDistribution(0, std::numeric_limits::max()) {} -RationalNumber RandomProbabilityGenerator::random() { - return carl::rationalize(distribution(engine)) / carl::rationalize(std::numeric_limits::max()); +storm::RationalNumber RandomProbabilityGenerator::randomProbability() { + return carl::rationalize(probabilityDistribution(engine)) / + carl::rationalize(std::numeric_limits::max()); } -uint64_t RandomProbabilityGenerator::random_uint(uint64_t min, uint64_t max) { - return std::uniform_int_distribution(min, max)(engine); +uint64_t RandomProbabilityGenerator::randomSelect(uint64_t min, uint64_t max) { + decltype(uniformDistribution.param()) newInterval(min, max); + uniformDistribution.param(newInterval); + return uniformDistribution(engine); + // return std::uniform_int_distribution(min, max)(engine); } -BernoulliDistributionGenerator::BernoulliDistributionGenerator(double prob) : distribution(prob) {} - -bool BernoulliDistributionGenerator::random(std::mt19937& engine) { - return distribution(engine); +storm::RationalNumber RandomProbabilityGenerator::randomExponential(storm::RationalNumber rate) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exponential distribution is not supported for rational numbers"); } -ExponentialDistributionGenerator::ExponentialDistributionGenerator(double rate) : distribution(rate) {} - -double ExponentialDistributionGenerator::random(std::mt19937& engine) { - return distribution(engine); -} } // namespace utility } // namespace storm diff --git a/src/storm/utility/random.h b/src/storm/utility/random.h index bbac3b1c3b..498caf5731 100644 --- a/src/storm/utility/random.h +++ b/src/storm/utility/random.h @@ -1,18 +1,24 @@ #pragma once -#include #include + #include "storm/adapters/RationalNumberAdapter.h" namespace storm { namespace utility { + template class RandomProbabilityGenerator { public: RandomProbabilityGenerator(); RandomProbabilityGenerator(uint64_t seed); - ValueType random() const; - uint64_t random_uint(uint64_t min, uint64_t max); + ValueType randomProbability(); + uint64_t randomSelect(uint64_t min, uint64_t max); + ValueType randomExponential(ValueType rate); + + protected: + std::mt19937 engine; + std::uniform_int_distribution uniformDistribution; }; template<> @@ -20,12 +26,15 @@ class RandomProbabilityGenerator { public: RandomProbabilityGenerator(); RandomProbabilityGenerator(uint64_t seed); - double random(); - uint64_t random_uint(uint64_t min, uint64_t max); + double randomProbability(); + uint64_t randomSelect(uint64_t min, uint64_t max); + double randomExponential(double rate); private: - std::uniform_real_distribution distribution; std::mt19937 engine; + std::uniform_int_distribution uniformDistribution; + std::uniform_real_distribution probabilityDistribution; + std::exponential_distribution exponentialDistribution; }; template<> @@ -33,31 +42,14 @@ class RandomProbabilityGenerator { public: RandomProbabilityGenerator(); RandomProbabilityGenerator(uint64_t seed); - RationalNumber random(); - uint64_t random_uint(uint64_t min, uint64_t max); + storm::RationalNumber randomProbability(); + uint64_t randomSelect(uint64_t min, uint64_t max); + storm::RationalNumber randomExponential(storm::RationalNumber rate); private: - std::uniform_int_distribution distribution; std::mt19937 engine; + std::uniform_int_distribution uniformDistribution; + std::uniform_int_distribution probabilityDistribution; }; - -class BernoulliDistributionGenerator { - public: - BernoulliDistributionGenerator(double prob); - bool random(std::mt19937& engine); - - private: - std::bernoulli_distribution distribution; -}; - -class ExponentialDistributionGenerator { - public: - ExponentialDistributionGenerator(double rate); - double random(std::mt19937& engine); - - private: - std::exponential_distribution distribution; -}; - } // namespace utility } // namespace storm \ No newline at end of file diff --git a/src/test/storm-dft/simulator/DftSimulatorTest.cpp b/src/test/storm-dft/simulator/DftSimulatorTest.cpp index 23a51024ed..f8562c3b99 100644 --- a/src/test/storm-dft/simulator/DftSimulatorTest.cpp +++ b/src/test/storm-dft/simulator/DftSimulatorTest.cpp @@ -24,8 +24,7 @@ std::pair simulateDft(std::string const& file, double timebound, storm::dft::storage::DFTStateGenerationInfo stateGenerationInfo(dft->buildStateGenerationInfo(symmetries)); // Init random number generator - // storm::utility::setLogLevel(l3pp::LogLevel::TRACE); - std::mt19937 gen(5u); + storm::utility::RandomProbabilityGenerator gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, stateGenerationInfo, gen); size_t count = 0; diff --git a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp index b25b620324..fc4a49a7dc 100644 --- a/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp +++ b/src/test/storm-dft/simulator/DftTraceGeneratorTest.cpp @@ -151,7 +151,7 @@ TYPED_TEST(DftTraceGeneratorTest, RandomStepsAnd) { EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, pair.second.hasSymmetries()); // Init random number generator - std::mt19937 gen(5u); + storm::utility::RandomProbabilityGenerator gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, pair.second, gen); auto state = simulator.getCurrentState(); @@ -177,7 +177,7 @@ TYPED_TEST(DftTraceGeneratorTest, Reset) { EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, pair.second.hasSymmetries()); // Init random number generator - std::mt19937 gen(5u); + storm::utility::RandomProbabilityGenerator gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, pair.second, gen); auto state = simulator.getCurrentState(); @@ -213,7 +213,7 @@ TYPED_TEST(DftTraceGeneratorTest, Fdep) { auto dft = pair.first; // Init random number generator. Will not be important as we are choosing the steps deterministically. - std::mt19937 gen(5u); + storm::utility::RandomProbabilityGenerator gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, pair.second, gen); // Start with initial state diff --git a/src/test/storm-dft/simulator/ImportanceFunctionTest.cpp b/src/test/storm-dft/simulator/ImportanceFunctionTest.cpp index c3ac70d9af..3889324a3f 100644 --- a/src/test/storm-dft/simulator/ImportanceFunctionTest.cpp +++ b/src/test/storm-dft/simulator/ImportanceFunctionTest.cpp @@ -28,7 +28,7 @@ TEST(ImportanceFunctionTest, RandomStepsAnd) { auto dft = pair.first; // Init random number generator - std::mt19937 gen(5u); + storm::utility::RandomProbabilityGenerator gen(5u); storm::dft::simulator::DFTTraceSimulator simulator(*dft, pair.second, gen); // Init importance function diff --git a/src/test/storm-dft/simulator/SamplingTest.cpp b/src/test/storm-dft/simulator/SamplingTest.cpp index 5697719023..dfe5c0cdaa 100644 --- a/src/test/storm-dft/simulator/SamplingTest.cpp +++ b/src/test/storm-dft/simulator/SamplingTest.cpp @@ -6,14 +6,13 @@ namespace { TEST(SamplingTest, SampleExponential) { - std::mt19937 gen(5u); - storm::utility::ExponentialDistributionGenerator dist(5); + storm::utility::RandomProbabilityGenerator dist(5u); // Ensure that pseudo random numbers are the same on all machines double reference[] = {0.011352194735198223, 0.35595966617002761, 0.0904286229501646, 0.77693019063043178, 0.018822806624073801, 0.10108027454097809, 0.087433897364154994, 0.13335480534208866, 0.93816592681955202, 0.33034562021306652}; for (int i = 0; i < 10; ++i) { - EXPECT_NEAR(dist.random(gen), reference[i], 1e-10); + EXPECT_NEAR(dist.randomExponential(5), reference[i], 1e-10); } } From debd6227cf66f9c2cabbb91ff1e87647a3d31927 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 25 Nov 2025 23:49:27 +0100 Subject: [PATCH 05/11] Extended SparseModelSimulator to continuous-time models --- .../DiscreteTimeSparseModelSimulator.cpp | 98 ---------- .../DiscreteTimeSparseModelSimulator.h | 35 ---- src/storm/simulator/SparseModelSimulator.cpp | 173 ++++++++++++++++++ src/storm/simulator/SparseModelSimulator.h | 61 ++++++ 4 files changed, 234 insertions(+), 133 deletions(-) delete mode 100644 src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp delete mode 100644 src/storm/simulator/DiscreteTimeSparseModelSimulator.h create mode 100644 src/storm/simulator/SparseModelSimulator.cpp create mode 100644 src/storm/simulator/SparseModelSimulator.h diff --git a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp b/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp deleted file mode 100644 index 0381037e68..0000000000 --- a/src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp +++ /dev/null @@ -1,98 +0,0 @@ -#include "storm/simulator/DiscreteTimeSparseModelSimulator.h" -#include "storm/models/sparse/Model.h" - -namespace storm { -namespace simulator { -template -DiscreteTimeSparseModelSimulator::DiscreteTimeSparseModelSimulator( - storm::models::sparse::Model const& model) - : model(model), currentState(*model.getInitialStates().begin()), zeroRewards(model.getNumberOfRewardModels(), storm::utility::zero()) { - STORM_LOG_WARN_COND(model.getInitialStates().getNumberOfSetBits() == 1, - "The model has multiple initial states. This simulator assumes it starts from the initial state with the lowest index."); - lastRewards = zeroRewards; - uint64_t i = 0; - for (auto const& rewModPair : model.getRewardModels()) { - if (rewModPair.second.hasStateRewards()) { - lastRewards[i] += rewModPair.second.getStateReward(currentState); - } - ++i; - } -} - -template -void DiscreteTimeSparseModelSimulator::setSeed(uint64_t seed) { - generator = storm::utility::RandomProbabilityGenerator(seed); -} - -template -bool DiscreteTimeSparseModelSimulator::randomStep() { - // TODO random_uint is slow - if (model.getTransitionMatrix().getRowGroupSize(currentState) == 0) { - return false; - } - return step(generator.randomSelect(0, model.getTransitionMatrix().getRowGroupSize(currentState) - 1)); -} - -template -bool DiscreteTimeSparseModelSimulator::step(uint64_t action) { - // TODO lots of optimization potential. - // E.g., do not sample random numbers if there is only a single transition - lastRewards = zeroRewards; - ValueType probability = generator.randomProbability(); - STORM_LOG_ASSERT(action < model.getTransitionMatrix().getRowGroupSize(currentState), "Action index higher than number of actions"); - uint64_t row = model.getTransitionMatrix().getRowGroupIndices()[currentState] + action; - uint64_t i = 0; - for (auto const& rewModPair : model.getRewardModels()) { - if (rewModPair.second.hasStateActionRewards()) { - lastRewards[i] += rewModPair.second.getStateActionReward(row); - } - ++i; - } - ValueType sum = storm::utility::zero(); - for (auto const& entry : model.getTransitionMatrix().getRow(row)) { - sum += entry.getValue(); - if (sum >= probability) { - currentState = entry.getColumn(); - i = 0; - for (auto const& rewModPair : model.getRewardModels()) { - if (rewModPair.second.hasStateRewards()) { - lastRewards[i] += rewModPair.second.getStateReward(currentState); - } - ++i; - } - return true; - } - } - // This position should never be reached - return false; -} - -template -uint64_t DiscreteTimeSparseModelSimulator::getCurrentState() const { - return currentState; -} - -template -bool DiscreteTimeSparseModelSimulator::resetToInitial() { - currentState = *model.getInitialStates().begin(); - lastRewards = zeroRewards; - uint64_t i = 0; - for (auto const& rewModPair : model.getRewardModels()) { - if (rewModPair.second.hasStateRewards()) { - lastRewards[i] += rewModPair.second.getStateReward(currentState); - } - ++i; - } - return true; -} - -template -std::vector const& DiscreteTimeSparseModelSimulator::getLastRewards() const { - return lastRewards; -} - -template class DiscreteTimeSparseModelSimulator; -template class DiscreteTimeSparseModelSimulator; - -} // namespace simulator -} // namespace storm diff --git a/src/storm/simulator/DiscreteTimeSparseModelSimulator.h b/src/storm/simulator/DiscreteTimeSparseModelSimulator.h deleted file mode 100644 index 88f291e779..0000000000 --- a/src/storm/simulator/DiscreteTimeSparseModelSimulator.h +++ /dev/null @@ -1,35 +0,0 @@ -#include -#include "storm/models/sparse/Model.h" -#include "storm/utility/random.h" - -namespace storm { -namespace simulator { - -/** - * This class is a low-level interface to quickly sample from Discrete-Time Models - * stored explicitly as a SparseModel. - * Additional information about state, actions, should be obtained via the model itself. - * - * TODO: It may be nice to write a CPP wrapper that does not require to actually obtain such informations yourself. - * @tparam ModelType - */ -template> -class DiscreteTimeSparseModelSimulator { - public: - DiscreteTimeSparseModelSimulator(storm::models::sparse::Model const& model); - void setSeed(uint64_t); - bool step(uint64_t action); - bool randomStep(); - std::vector const& getLastRewards() const; - uint64_t getCurrentState() const; - bool resetToInitial(); - - protected: - storm::models::sparse::Model const& model; - uint64_t currentState; - std::vector lastRewards; - std::vector zeroRewards; - storm::utility::RandomProbabilityGenerator generator; -}; -} // namespace simulator -} // namespace storm \ No newline at end of file diff --git a/src/storm/simulator/SparseModelSimulator.cpp b/src/storm/simulator/SparseModelSimulator.cpp new file mode 100644 index 0000000000..739d8a6d51 --- /dev/null +++ b/src/storm/simulator/SparseModelSimulator.cpp @@ -0,0 +1,173 @@ +#include "storm/simulator/SparseModelSimulator.h" + +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/MarkovAutomaton.h" + +namespace storm { +namespace simulator { +template +SparseModelSimulator::SparseModelSimulator(storm::models::sparse::Model const& model) + : model(model), zeroRewards(model.getNumberOfRewardModels(), storm::utility::zero()), generator() { + resetToInitial(); + + if (!model.isDiscreteTimeModel()) { + if (model.getType() == storm::models::ModelType::Ctmc) { + exitRates = model.template as>()->getExitRateVector(); + } else { + STORM_LOG_ASSERT(model.getType() == storm::models::ModelType::MarkovAutomaton, "Model is not a Markov automaton."); + auto ma = model.template as>(); + exitRates = ma->getExitRates(); +#ifndef NDEBUG + for (size_t i = 0; i < exitRates.size(); ++i) { + STORM_LOG_ASSERT((storm::utility::isZero(exitRates[i]) || ma->isMarkovianState(i)) && + (!storm::utility::isZero(exitRates[i]) || !ma->isMarkovianState(i)), + "Exit rate and Markovian state do not match."); + } +#endif + } + } +} + +template +void SparseModelSimulator::setSeed(uint64_t seed) { + generator = storm::utility::RandomProbabilityGenerator(seed); +} +template +void SparseModelSimulator::resetToInitial() { + STORM_LOG_WARN_COND(model.getInitialStates().getNumberOfSetBits() == 1, + "The model has multiple initial states. This simulator assumes it starts from the initial state with the lowest index."); + currentState = *model.getInitialStates().begin(); + currentTime = storm::utility::zero(); + lastRewards = zeroRewards; + uint64_t i = 0; + for (auto const& rewModPair : model.getRewardModels()) { + if (rewModPair.second.hasStateRewards()) { + lastRewards[i] += rewModPair.second.getStateReward(currentState); + } + ++i; + } +} + +template +uint64_t SparseModelSimulator::choice(uint64_t choice) { + STORM_LOG_ASSERT(choice < model.getTransitionMatrix().getRowGroupSize(currentState), "Action index higher than number of actions"); + lastRewards = zeroRewards; + uint64_t row = model.getTransitionMatrix().getRowGroupIndices()[currentState] + choice; + + // Add state-action reward + uint64_t i = 0; + for (auto const& rewModPair : model.getRewardModels()) { + if (rewModPair.second.hasStateActionRewards()) { + lastRewards[i] += rewModPair.second.getStateActionReward(row); + } + ++i; + } + return row; +} + +template +void SparseModelSimulator::transition(uint64_t row, uint64_t column) { +#ifndef NDEBUG + bool columnExists = false; + for (auto const& entry : model.getTransitionMatrix().getRow(row)) { + if (entry.getColumn() == column) { + columnExists = true; + } + } + STORM_LOG_ASSERT(columnExists, "Column " << column << " does not exist"); +#endif + + currentState = column; + // Add state reward + uint64_t i = 0; + for (auto const& rewModPair : model.getRewardModels()) { + if (rewModPair.second.hasStateRewards()) { + lastRewards[i] += rewModPair.second.getStateReward(currentState); + } + ++i; + } +} + +template +bool SparseModelSimulator::randomStep() { + if (!model.isDiscreteTimeModel()) { + // First choose time when to leave the state + randomTime(); + } + + if (model.getTransitionMatrix().getRowGroupSize(currentState) == 0) { + return false; + } + if (model.getTransitionMatrix().getRowGroupSize(currentState) == 1) { + return step(0); + } + // Select action by uniform distribution + return step(generator.randomSelect(0, model.getTransitionMatrix().getRowGroupSize(currentState) - 1)); +} + +template +bool SparseModelSimulator::step(uint64_t action) { + // Perform action + uint64_t row = choice(action); + + if (model.getTransitionMatrix().getRow(row).getNumberOfEntries() == 1) { + // Select only transition + uint64_t column = model.getTransitionMatrix().getRow(row).begin()->getColumn(); + transition(row, column); + return true; + } + + // Randomly select transition + ValueType probability = generator.randomProbability(); + ValueType sum = storm::utility::zero(); + for (auto const& entry : model.getTransitionMatrix().getRow(row)) { + sum += entry.getValue(); + if (sum >= probability) { + uint64_t column = entry.getColumn(); + transition(row, column); + return true; + } + } + + // This position should never be reached + return false; +} + +template +bool SparseModelSimulator::step(uint64_t action, uint64_t column) { + uint64_t row = choice(action); + transition(row, column); + return true; +} + +template +void SparseModelSimulator::randomTime() { + STORM_LOG_ASSERT(!model.isDiscreteTimeModel(), "Model must be continuous-time model"); + ValueType exitRate = exitRates[currentState]; + if (!storm::utility::isZero(exitRate)) { + STORM_LOG_ASSERT(model.getTransitionMatrix().getRowGroupSize(currentState) == 1, "Markovian state should have a trivial row group."); + ValueType time = generator.randomExponential(exitRate); + currentTime += time; + } +} + +template +uint64_t SparseModelSimulator::getCurrentState() const { + return currentState; +} + +template +ValueType SparseModelSimulator::getCurrentTime() const { + return currentTime; +} + +template +std::vector const& SparseModelSimulator::getLastRewards() const { + return lastRewards; +} + +template class SparseModelSimulator; +template class SparseModelSimulator; + +} // namespace simulator +} // namespace storm diff --git a/src/storm/simulator/SparseModelSimulator.h b/src/storm/simulator/SparseModelSimulator.h new file mode 100644 index 0000000000..7d46981f53 --- /dev/null +++ b/src/storm/simulator/SparseModelSimulator.h @@ -0,0 +1,61 @@ +#include + +#include "storm/models/sparse/Model.h" +#include "storm/utility/random.h" + +namespace storm { +namespace simulator { + +/** + * This class is a low-level interface to quickly sample from sparse models. + * Additional information about state, actions, should be obtained via the model itself. + * + * TODO: It may be nice to write a CPP wrapper that does not require to actually obtain such informations yourself. + */ +template> +class SparseModelSimulator { + public: + SparseModelSimulator(storm::models::sparse::Model const& model); + void setSeed(uint64_t); + void resetToInitial(); + + /** + * For probabilistic states: Randomly select action and then randomly select transition. + * For Markovian states (only in continous-time models): Increase time according to exit rate and then randomly select transition. + */ + bool randomStep(); + /** + * Perform action and then randomly select transition. + */ + bool step(uint64_t action); + /** + * Perform action and then select transition corresponding to column. + */ + bool step(uint64_t action, uint64_t column); + + void randomTime(); + + uint64_t getCurrentState() const; + ValueType getCurrentTime() const; + std::vector const& getLastRewards() const; + + private: + /** + * Select choice, update state-action rewards and return corresponding row. + */ + uint64_t choice(uint64_t choice); + void transition(uint64_t row, uint64_t column); + + storm::models::sparse::Model const& model; + uint64_t currentState; + // Time which has progressed so far. Only relevant for continous-time models + ValueType currentTime; + std::vector lastRewards; + std::vector zeroRewards; + storm::utility::RandomProbabilityGenerator generator; + + // Exit rates for continuous-time models + std::vector exitRates; +}; +} // namespace simulator +} // namespace storm \ No newline at end of file From 17bc805c1b6d0c9a4a3d8399bc16a7c93bb73965 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 26 Nov 2025 18:00:03 +0100 Subject: [PATCH 06/11] Tests for SparseModelSimulator --- src/storm/simulator/SparseModelSimulator.cpp | 11 +- src/storm/simulator/SparseModelSimulator.h | 2 + .../simulator/SparseModelSimulatorTest.cpp | 140 ++++++++++++++++++ 3 files changed, 152 insertions(+), 1 deletion(-) create mode 100644 src/test/storm/simulator/SparseModelSimulatorTest.cpp diff --git a/src/storm/simulator/SparseModelSimulator.cpp b/src/storm/simulator/SparseModelSimulator.cpp index 739d8a6d51..c4499dde02 100644 --- a/src/storm/simulator/SparseModelSimulator.cpp +++ b/src/storm/simulator/SparseModelSimulator.cpp @@ -50,7 +50,7 @@ void SparseModelSimulator::resetToInitial() { template uint64_t SparseModelSimulator::choice(uint64_t choice) { - STORM_LOG_ASSERT(choice < model.getTransitionMatrix().getRowGroupSize(currentState), "Action index higher than number of actions"); + STORM_LOG_ASSERT(choice < getCurrentNumberOfChoices(), "Action index higher than number of actions"); lastRewards = zeroRewards; uint64_t row = model.getTransitionMatrix().getRowGroupIndices()[currentState] + choice; @@ -160,6 +160,15 @@ template ValueType SparseModelSimulator::getCurrentTime() const { return currentTime; } +template +uint64_t SparseModelSimulator::getCurrentNumberOfChoices() const { + return model.getTransitionMatrix().getRowGroupSize(currentState); +} + +template +std::set SparseModelSimulator::getCurrentStateLabelling() const { + return model.getStateLabeling().getLabelsOfState(currentState); +} template std::vector const& SparseModelSimulator::getLastRewards() const { diff --git a/src/storm/simulator/SparseModelSimulator.h b/src/storm/simulator/SparseModelSimulator.h index 7d46981f53..e06acc4d36 100644 --- a/src/storm/simulator/SparseModelSimulator.h +++ b/src/storm/simulator/SparseModelSimulator.h @@ -37,6 +37,8 @@ class SparseModelSimulator { uint64_t getCurrentState() const; ValueType getCurrentTime() const; + uint64_t getCurrentNumberOfChoices() const; + std::set getCurrentStateLabelling() const; std::vector const& getLastRewards() const; private: diff --git a/src/test/storm/simulator/SparseModelSimulatorTest.cpp b/src/test/storm/simulator/SparseModelSimulatorTest.cpp new file mode 100644 index 0000000000..0301e10b82 --- /dev/null +++ b/src/test/storm/simulator/SparseModelSimulatorTest.cpp @@ -0,0 +1,140 @@ +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/parser/PrismParser.h" +#include "storm/api/builder.h" +#include "storm/simulator/SparseModelSimulator.h" + +TEST(SparseModelSimulatorTest, KnuthYaoDieTest) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm"); + storm::builder::BuilderOptions options; + options.setBuildAllRewardModels(); + options.setBuildAllLabels(); + auto model = storm::api::buildSparseModel(program, options)->template as>(); + + storm::simulator::SparseModelSimulator sim(*model); + sim.setSeed(42); + EXPECT_EQ("coin_flips", model->getRewardModels().begin()->first); + EXPECT_EQ(0ul, sim.getCurrentState()); + auto rew = sim.getLastRewards(); + rew = sim.getLastRewards(); + EXPECT_EQ(1ul, rew.size()); + EXPECT_EQ(0.0, rew[0]); + auto labels = sim.getCurrentStateLabelling(); + EXPECT_EQ(1ul, labels.size()); + EXPECT_EQ("init", *labels.begin()); + EXPECT_EQ(2ul, sim.getCurrentNumberOfChoices()); + + sim.step(0); + EXPECT_EQ(2ul, sim.getCurrentState()); + rew = sim.getLastRewards(); + EXPECT_EQ(1ul, rew.size()); + EXPECT_EQ(0.0, rew[0]); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + + sim.randomStep(); + EXPECT_EQ(5ul, sim.getCurrentState()); + rew = sim.getLastRewards(); + EXPECT_EQ(1ul, rew.size()); + EXPECT_EQ(1.0, rew[0]); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + + sim.randomStep(); + EXPECT_EQ(11ul, sim.getCurrentState()); + rew = sim.getLastRewards(); + EXPECT_EQ(1ul, rew.size()); + EXPECT_EQ(1.0, rew[0]); + labels = sim.getCurrentStateLabelling(); + EXPECT_EQ(2ul, labels.size()); + EXPECT_TRUE(std::count(labels.begin(), labels.end(), "done") == 1); + EXPECT_TRUE(std::count(labels.begin(), labels.end(), "five") == 1); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + + sim.randomStep(); + EXPECT_EQ(11ul, sim.getCurrentState()); + rew = sim.getLastRewards(); + EXPECT_EQ(1ul, rew.size()); + EXPECT_EQ(0.0, rew[0]); + labels = sim.getCurrentStateLabelling(); + EXPECT_EQ(2ul, labels.size()); + EXPECT_TRUE(std::count(labels.begin(), labels.end(), "done") == 1); + EXPECT_TRUE(std::count(labels.begin(), labels.end(), "five") == 1); + + EXPECT_EQ(0, sim.getCurrentTime()); +} + +TEST(SparseModelSimulatorTest, SimpleMATest) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma"); + storm::builder::BuilderOptions options; + options.setBuildAllRewardModels(); + options.setBuildAllLabels(); + auto model = storm::api::buildSparseModel(program, options)->template as>(); + + storm::simulator::SparseModelSimulator sim(*model); + sim.setSeed(5); + EXPECT_EQ(0ul, model->getRewardModels().size()); + + // 1st run + EXPECT_EQ(0ul, sim.getCurrentState()); + auto rew = sim.getLastRewards(); + rew = sim.getLastRewards(); + EXPECT_EQ(0ul, rew.size()); + auto labels = sim.getCurrentStateLabelling(); + EXPECT_EQ(1ul, labels.size()); + EXPECT_EQ("init", *labels.begin()); + EXPECT_EQ(2ul, sim.getCurrentNumberOfChoices()); + EXPECT_EQ(0, sim.getCurrentTime()); + + sim.step(1); + EXPECT_EQ(0ul, sim.getCurrentState()); + labels = sim.getCurrentStateLabelling(); + EXPECT_EQ(1ul, labels.size()); + EXPECT_EQ("init", *labels.begin()); + EXPECT_EQ(2ul, sim.getCurrentNumberOfChoices()); + EXPECT_EQ(0, sim.getCurrentTime()); + + sim.step(1); + EXPECT_EQ(2ul, sim.getCurrentState()); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_EQ(0, sim.getCurrentTime()); + + sim.randomStep(); + EXPECT_EQ(4ul, sim.getCurrentState()); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_NEAR(0.037679, sim.getCurrentTime(), 1e-6); + + // 2nd run + sim.resetToInitial(); + EXPECT_EQ(0ul, sim.getCurrentState()); + EXPECT_EQ(0, sim.getCurrentTime()); + sim.step(0); + EXPECT_EQ(1ul, sim.getCurrentState()); + EXPECT_EQ(0, sim.getCurrentTime()); + sim.randomStep(); + EXPECT_EQ(0ul, sim.getCurrentState()); + EXPECT_NEAR(0.388465, sim.getCurrentTime(), 1e-6); + + sim.step(0); + EXPECT_EQ(1ul, sim.getCurrentState()); + EXPECT_NEAR(0.388465, sim.getCurrentTime(), 1e-6); + sim.randomStep(); + EXPECT_EQ(0ul, sim.getCurrentState()); + EXPECT_NEAR(0.388465 + 0.050540, sim.getCurrentTime(), 1e-6); + + sim.step(0); + EXPECT_EQ(1ul, sim.getCurrentState()); + EXPECT_NEAR(0.388465 + 0.050540, sim.getCurrentTime(), 1e-6); + sim.randomStep(); + EXPECT_EQ(3ul, sim.getCurrentState()); + EXPECT_NEAR(0.388465 + 0.050540 + 0.066677, sim.getCurrentTime(), 1e-6); +} From 13960a1e43110d84eaad511b3a20cb4728ebe78b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 27 Nov 2025 09:30:28 +0100 Subject: [PATCH 07/11] Fix for CTMC which uses a rate matrix --- src/storm/simulator/SparseModelSimulator.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/storm/simulator/SparseModelSimulator.cpp b/src/storm/simulator/SparseModelSimulator.cpp index c4499dde02..bf999852fe 100644 --- a/src/storm/simulator/SparseModelSimulator.cpp +++ b/src/storm/simulator/SparseModelSimulator.cpp @@ -121,7 +121,12 @@ bool SparseModelSimulator::step(uint64_t action) { ValueType probability = generator.randomProbability(); ValueType sum = storm::utility::zero(); for (auto const& entry : model.getTransitionMatrix().getRow(row)) { - sum += entry.getValue(); + if (model.getType() == storm::models::ModelType::Ctmc) { + // Scale rates to probabilities + sum += entry.getValue() / exitRates[currentState]; + } else { + sum += entry.getValue(); + } if (sum >= probability) { uint64_t column = entry.getColumn(); transition(row, column); From c9e8d50e1e2b29d6cb1c4b7d838b480b2c783801 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 5 Dec 2025 12:02:00 +0100 Subject: [PATCH 08/11] Use shared_ptr for model in SparseModelSimulator --- src/storm/simulator/SparseModelSimulator.cpp | 52 +++++++++---------- src/storm/simulator/SparseModelSimulator.h | 12 ++--- .../simulator/SparseModelSimulatorTest.cpp | 30 +++++++++-- 3 files changed, 59 insertions(+), 35 deletions(-) diff --git a/src/storm/simulator/SparseModelSimulator.cpp b/src/storm/simulator/SparseModelSimulator.cpp index bf999852fe..58db008070 100644 --- a/src/storm/simulator/SparseModelSimulator.cpp +++ b/src/storm/simulator/SparseModelSimulator.cpp @@ -6,16 +6,16 @@ namespace storm { namespace simulator { template -SparseModelSimulator::SparseModelSimulator(storm::models::sparse::Model const& model) - : model(model), zeroRewards(model.getNumberOfRewardModels(), storm::utility::zero()), generator() { +SparseModelSimulator::SparseModelSimulator(std::shared_ptr const> model) + : model(model), zeroRewards(model->getNumberOfRewardModels(), storm::utility::zero()), generator() { resetToInitial(); - if (!model.isDiscreteTimeModel()) { - if (model.getType() == storm::models::ModelType::Ctmc) { - exitRates = model.template as>()->getExitRateVector(); + if (!model->isDiscreteTimeModel()) { + if (model->getType() == storm::models::ModelType::Ctmc) { + exitRates = model->template as>()->getExitRateVector(); } else { - STORM_LOG_ASSERT(model.getType() == storm::models::ModelType::MarkovAutomaton, "Model is not a Markov automaton."); - auto ma = model.template as>(); + STORM_LOG_ASSERT(model->getType() == storm::models::ModelType::MarkovAutomaton, "Model is not a Markov automaton."); + auto ma = model->template as>(); exitRates = ma->getExitRates(); #ifndef NDEBUG for (size_t i = 0; i < exitRates.size(); ++i) { @@ -34,13 +34,13 @@ void SparseModelSimulator::setSeed(uint64_t seed) { } template void SparseModelSimulator::resetToInitial() { - STORM_LOG_WARN_COND(model.getInitialStates().getNumberOfSetBits() == 1, + STORM_LOG_WARN_COND(model->getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states. This simulator assumes it starts from the initial state with the lowest index."); - currentState = *model.getInitialStates().begin(); + currentState = *model->getInitialStates().begin(); currentTime = storm::utility::zero(); lastRewards = zeroRewards; uint64_t i = 0; - for (auto const& rewModPair : model.getRewardModels()) { + for (auto const& rewModPair : model->getRewardModels()) { if (rewModPair.second.hasStateRewards()) { lastRewards[i] += rewModPair.second.getStateReward(currentState); } @@ -52,11 +52,11 @@ template uint64_t SparseModelSimulator::choice(uint64_t choice) { STORM_LOG_ASSERT(choice < getCurrentNumberOfChoices(), "Action index higher than number of actions"); lastRewards = zeroRewards; - uint64_t row = model.getTransitionMatrix().getRowGroupIndices()[currentState] + choice; + uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[currentState] + choice; // Add state-action reward uint64_t i = 0; - for (auto const& rewModPair : model.getRewardModels()) { + for (auto const& rewModPair : model->getRewardModels()) { if (rewModPair.second.hasStateActionRewards()) { lastRewards[i] += rewModPair.second.getStateActionReward(row); } @@ -69,7 +69,7 @@ template void SparseModelSimulator::transition(uint64_t row, uint64_t column) { #ifndef NDEBUG bool columnExists = false; - for (auto const& entry : model.getTransitionMatrix().getRow(row)) { + for (auto const& entry : model->getTransitionMatrix().getRow(row)) { if (entry.getColumn() == column) { columnExists = true; } @@ -80,7 +80,7 @@ void SparseModelSimulator::transition(uint64_t row, currentState = column; // Add state reward uint64_t i = 0; - for (auto const& rewModPair : model.getRewardModels()) { + for (auto const& rewModPair : model->getRewardModels()) { if (rewModPair.second.hasStateRewards()) { lastRewards[i] += rewModPair.second.getStateReward(currentState); } @@ -90,19 +90,19 @@ void SparseModelSimulator::transition(uint64_t row, template bool SparseModelSimulator::randomStep() { - if (!model.isDiscreteTimeModel()) { + if (!model->isDiscreteTimeModel()) { // First choose time when to leave the state randomTime(); } - if (model.getTransitionMatrix().getRowGroupSize(currentState) == 0) { + if (model->getTransitionMatrix().getRowGroupSize(currentState) == 0) { return false; } - if (model.getTransitionMatrix().getRowGroupSize(currentState) == 1) { + if (model->getTransitionMatrix().getRowGroupSize(currentState) == 1) { return step(0); } // Select action by uniform distribution - return step(generator.randomSelect(0, model.getTransitionMatrix().getRowGroupSize(currentState) - 1)); + return step(generator.randomSelect(0, model->getTransitionMatrix().getRowGroupSize(currentState) - 1)); } template @@ -110,9 +110,9 @@ bool SparseModelSimulator::step(uint64_t action) { // Perform action uint64_t row = choice(action); - if (model.getTransitionMatrix().getRow(row).getNumberOfEntries() == 1) { + if (model->getTransitionMatrix().getRow(row).getNumberOfEntries() == 1) { // Select only transition - uint64_t column = model.getTransitionMatrix().getRow(row).begin()->getColumn(); + uint64_t column = model->getTransitionMatrix().getRow(row).begin()->getColumn(); transition(row, column); return true; } @@ -120,8 +120,8 @@ bool SparseModelSimulator::step(uint64_t action) { // Randomly select transition ValueType probability = generator.randomProbability(); ValueType sum = storm::utility::zero(); - for (auto const& entry : model.getTransitionMatrix().getRow(row)) { - if (model.getType() == storm::models::ModelType::Ctmc) { + for (auto const& entry : model->getTransitionMatrix().getRow(row)) { + if (model->getType() == storm::models::ModelType::Ctmc) { // Scale rates to probabilities sum += entry.getValue() / exitRates[currentState]; } else { @@ -147,10 +147,10 @@ bool SparseModelSimulator::step(uint64_t action, uin template void SparseModelSimulator::randomTime() { - STORM_LOG_ASSERT(!model.isDiscreteTimeModel(), "Model must be continuous-time model"); + STORM_LOG_ASSERT(!model->isDiscreteTimeModel(), "Model must be continuous-time model"); ValueType exitRate = exitRates[currentState]; if (!storm::utility::isZero(exitRate)) { - STORM_LOG_ASSERT(model.getTransitionMatrix().getRowGroupSize(currentState) == 1, "Markovian state should have a trivial row group."); + STORM_LOG_ASSERT(model->getTransitionMatrix().getRowGroupSize(currentState) == 1, "Markovian state should have a trivial row group."); ValueType time = generator.randomExponential(exitRate); currentTime += time; } @@ -167,12 +167,12 @@ ValueType SparseModelSimulator::getCurrentTime() con } template uint64_t SparseModelSimulator::getCurrentNumberOfChoices() const { - return model.getTransitionMatrix().getRowGroupSize(currentState); + return model->getTransitionMatrix().getRowGroupSize(currentState); } template std::set SparseModelSimulator::getCurrentStateLabelling() const { - return model.getStateLabeling().getLabelsOfState(currentState); + return model->getStateLabeling().getLabelsOfState(currentState); } template diff --git a/src/storm/simulator/SparseModelSimulator.h b/src/storm/simulator/SparseModelSimulator.h index e06acc4d36..68d304d692 100644 --- a/src/storm/simulator/SparseModelSimulator.h +++ b/src/storm/simulator/SparseModelSimulator.h @@ -1,4 +1,4 @@ -#include +#pragma once #include "storm/models/sparse/Model.h" #include "storm/utility/random.h" @@ -10,18 +10,18 @@ namespace simulator { * This class is a low-level interface to quickly sample from sparse models. * Additional information about state, actions, should be obtained via the model itself. * - * TODO: It may be nice to write a CPP wrapper that does not require to actually obtain such informations yourself. + * TODO: It may be nice to write a CPP wrapper that does not require to actually obtain such information yourself. */ template> class SparseModelSimulator { public: - SparseModelSimulator(storm::models::sparse::Model const& model); + SparseModelSimulator(std::shared_ptr const> model); void setSeed(uint64_t); void resetToInitial(); /** * For probabilistic states: Randomly select action and then randomly select transition. - * For Markovian states (only in continous-time models): Increase time according to exit rate and then randomly select transition. + * For Markovian states (only in continuous-time models): Increase time according to exit rate and then randomly select transition. */ bool randomStep(); /** @@ -48,9 +48,9 @@ class SparseModelSimulator { uint64_t choice(uint64_t choice); void transition(uint64_t row, uint64_t column); - storm::models::sparse::Model const& model; + std::shared_ptr const> model; uint64_t currentState; - // Time which has progressed so far. Only relevant for continous-time models + // Time which has progressed so far. Only relevant for continuous-time models ValueType currentTime; std::vector lastRewards; std::vector zeroRewards; diff --git a/src/test/storm/simulator/SparseModelSimulatorTest.cpp b/src/test/storm/simulator/SparseModelSimulatorTest.cpp index 0301e10b82..0962ef1f82 100644 --- a/src/test/storm/simulator/SparseModelSimulatorTest.cpp +++ b/src/test/storm/simulator/SparseModelSimulatorTest.cpp @@ -5,7 +5,31 @@ #include "storm/api/builder.h" #include "storm/simulator/SparseModelSimulator.h" -TEST(SparseModelSimulatorTest, KnuthYaoDieTest) { +TEST(SparseModelSimulatorTest, KnuthYaoDieDtmc) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + storm::builder::BuilderOptions options; + options.setBuildAllRewardModels(); + options.setBuildAllLabels(); + auto model = storm::api::buildSparseModel(program, options)->template as>(); + + storm::simulator::SparseModelSimulator sim(model); + sim.setSeed(42); + EXPECT_EQ("coin_flips", model->getRewardModels().begin()->first); + EXPECT_EQ(0ul, sim.getCurrentState()); + auto rew = sim.getLastRewards(); + rew = sim.getLastRewards(); + EXPECT_EQ(1ul, rew.size()); + EXPECT_EQ(0.0, rew[0]); + auto labels = sim.getCurrentStateLabelling(); + EXPECT_EQ(1ul, labels.size()); + EXPECT_EQ("init", *labels.begin()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); +} + +TEST(SparseModelSimulatorTest, KnuthYaoDieMdp) { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; #endif @@ -15,7 +39,7 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieTest) { options.setBuildAllLabels(); auto model = storm::api::buildSparseModel(program, options)->template as>(); - storm::simulator::SparseModelSimulator sim(*model); + storm::simulator::SparseModelSimulator sim(model); sim.setSeed(42); EXPECT_EQ("coin_flips", model->getRewardModels().begin()->first); EXPECT_EQ(0ul, sim.getCurrentState()); @@ -78,7 +102,7 @@ TEST(SparseModelSimulatorTest, SimpleMATest) { options.setBuildAllLabels(); auto model = storm::api::buildSparseModel(program, options)->template as>(); - storm::simulator::SparseModelSimulator sim(*model); + storm::simulator::SparseModelSimulator sim(model); sim.setSeed(5); EXPECT_EQ(0ul, model->getRewardModels().size()); From 9927448a81c2aa5b4f4e5353b26087675dcb11a9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 5 Dec 2025 17:20:42 +0100 Subject: [PATCH 09/11] Monte Carlo simulator + test --- src/storm/simulator/SparseModelSimulator.cpp | 9 +- src/storm/simulator/SparseModelSimulator.h | 2 + src/storm/simulator/TraceSimulator.cpp | 99 +++++++++++++++++++ src/storm/simulator/TraceSimulator.h | 82 +++++++++++++++ .../storm/simulator/TraceSimulatorTest.cpp | 86 ++++++++++++++++ 5 files changed, 276 insertions(+), 2 deletions(-) create mode 100644 src/storm/simulator/TraceSimulator.cpp create mode 100644 src/storm/simulator/TraceSimulator.h create mode 100644 src/test/storm/simulator/TraceSimulatorTest.cpp diff --git a/src/storm/simulator/SparseModelSimulator.cpp b/src/storm/simulator/SparseModelSimulator.cpp index 58db008070..848c0b5464 100644 --- a/src/storm/simulator/SparseModelSimulator.cpp +++ b/src/storm/simulator/SparseModelSimulator.cpp @@ -10,7 +10,7 @@ SparseModelSimulator::SparseModelSimulator(std::shar : model(model), zeroRewards(model->getNumberOfRewardModels(), storm::utility::zero()), generator() { resetToInitial(); - if (!model->isDiscreteTimeModel()) { + if (isContinuousTimeModel()) { if (model->getType() == storm::models::ModelType::Ctmc) { exitRates = model->template as>()->getExitRateVector(); } else { @@ -147,7 +147,7 @@ bool SparseModelSimulator::step(uint64_t action, uin template void SparseModelSimulator::randomTime() { - STORM_LOG_ASSERT(!model->isDiscreteTimeModel(), "Model must be continuous-time model"); + STORM_LOG_ASSERT(isContinuousTimeModel(), "Model must be continuous-time model"); ValueType exitRate = exitRates[currentState]; if (!storm::utility::isZero(exitRate)) { STORM_LOG_ASSERT(model->getTransitionMatrix().getRowGroupSize(currentState) == 1, "Markovian state should have a trivial row group."); @@ -180,6 +180,11 @@ std::vector const& SparseModelSimulator:: return lastRewards; } +template +bool SparseModelSimulator::isContinuousTimeModel() const { + return !model->isDiscreteTimeModel(); +} + template class SparseModelSimulator; template class SparseModelSimulator; diff --git a/src/storm/simulator/SparseModelSimulator.h b/src/storm/simulator/SparseModelSimulator.h index 68d304d692..7e684fdd42 100644 --- a/src/storm/simulator/SparseModelSimulator.h +++ b/src/storm/simulator/SparseModelSimulator.h @@ -41,6 +41,8 @@ class SparseModelSimulator { std::set getCurrentStateLabelling() const; std::vector const& getLastRewards() const; + bool isContinuousTimeModel() const; + private: /** * Select choice, update state-action rewards and return corresponding row. diff --git a/src/storm/simulator/TraceSimulator.cpp b/src/storm/simulator/TraceSimulator.cpp new file mode 100644 index 0000000000..1a42fe7e40 --- /dev/null +++ b/src/storm/simulator/TraceSimulator.cpp @@ -0,0 +1,99 @@ +#include "storm/simulator/TraceSimulator.h" + +#include "storm/exceptions/UnsupportedModelException.h" +#include "storm/simulator/SparseModelSimulator.h" + +namespace storm { +namespace simulator { + +template +TraceSimulator::TraceSimulator(std::shared_ptr> simulator) : simulator(simulator) { + // Intentionally left empty. +} + +template +SimulationTraceResult TraceSimulator::simulateStepBoundedTrace(size_t stepBound, std::optional const& goalLabel) { + simulator->resetToInitial(); + size_t steps = 0; + while (steps <= stepBound) { + if (reachedLabel(goalLabel)) { + return SimulationTraceResult::GOAL_REACHED; + } + if (!simulator->randomStep()) { + return SimulationTraceResult::DEADLOCK; + } + steps++; + } + return SimulationTraceResult::BOUND_REACHED; +} + +template +SimulationTraceResult TraceSimulator::simulateTimeBoundedTrace(ValueType timeBound, std::optional const& goalLabel) { + simulator->resetToInitial(); + + while (simulator->getCurrentTime() <= timeBound) { + if (reachedLabel(goalLabel)) { + return SimulationTraceResult::GOAL_REACHED; + } + if (!simulator->randomStep()) { + return SimulationTraceResult::DEADLOCK; + } + } + return SimulationTraceResult::BOUND_REACHED; +} + +template +ValueType TraceSimulator::simulateStepBoundedReachability(std::string const& label, uint64_t stepBound, uint64_t numberRuns) { + STORM_LOG_WARN_COND(!simulator->isContinuousTimeModel(), "Simulating step-bounded reachability on a continuous-time model."); + uint64_t numberGoal = 0; + storm::simulator::SimulationTraceResult res; + for (size_t i = 0; i < numberRuns; ++i) { + res = simulateStepBoundedTrace(stepBound, label); + if (res == storm::simulator::SimulationTraceResult::GOAL_REACHED) { + ++numberGoal; + } else { + if (res == storm::simulator::SimulationTraceResult::DEADLOCK) { + STORM_LOG_WARN("Simulation reached a deadlock state."); + } + } + } + return storm::utility::convertNumber(numberGoal) / storm::utility::convertNumber(numberRuns); +} + +template +ValueType TraceSimulator::simulateTimeBoundedReachability(std::string const& label, ValueType timebound, uint64_t numberRuns) { + STORM_LOG_THROW(simulator->isContinuousTimeModel(), storm::exceptions::UnsupportedModelException, + "Time-bounded reachability can only be simulated on continuous-time models."); + uint64_t numberGoal = 0; + storm::simulator::SimulationTraceResult res; + for (size_t i = 0; i < numberRuns; ++i) { + res = simulateTimeBoundedTrace(timebound, label); + if (res == storm::simulator::SimulationTraceResult::GOAL_REACHED) { + ++numberGoal; + } else { + if (res == storm::simulator::SimulationTraceResult::DEADLOCK) { + STORM_LOG_WARN("Simulation reached a deadlock state."); + } + } + } + return storm::utility::convertNumber(numberGoal) / storm::utility::convertNumber(numberRuns); +} + +template +bool TraceSimulator::reachedLabel(std::optional const& goalLabel) const { + if (!goalLabel.has_value()) { + return false; + } + return simulator->getCurrentStateLabelling().contains(goalLabel.value()); +} + +template +std::shared_ptr const> TraceSimulator::getSimulator() const { + return simulator; +} + +template class TraceSimulator; +template class TraceSimulator; + +} // namespace simulator +} // namespace storm diff --git a/src/storm/simulator/TraceSimulator.h b/src/storm/simulator/TraceSimulator.h new file mode 100644 index 0000000000..2cc8d5a915 --- /dev/null +++ b/src/storm/simulator/TraceSimulator.h @@ -0,0 +1,82 @@ +#pragma once + +#include "storm/simulator/SparseModelSimulator.h" + +namespace storm { +namespace simulator { + +/*! + * The result of simulating a trace can be either that + * - the goal label was reached + * - the step/time bound was reached + * - or a deadlock was encountered. + */ +enum class SimulationTraceResult { GOAL_REACHED, BOUND_REACHED, DEADLOCK }; + +/** + * Perform simulation runs of a model. + */ +template +class TraceSimulator { + public: + /*! + * Constructor. + * @param simulator Underlying simulator. + */ + TraceSimulator(std::shared_ptr> simulator); + + /*! + * Simulate a single (untimed) trace until either the goal label or the step bound is reached. + * @param stepBound Step bound. + * @param goalLabel Label to reach. + * @return Result of trace (step bound reached, goal reached or deadlock). + */ + SimulationTraceResult simulateStepBoundedTrace(size_t stepBound, std::optional const& goalLabel); + + /*! + * Simulate a single (timed) trace until either the goal label or the time bound is reached. + * @param timeBound Time bound. + * @param goalLabel Label to reach. + * @return Result of trace (time bound reached, goal reached or deadlock). + */ + SimulationTraceResult simulateTimeBoundedTrace(ValueType timeBound, std::optional const& goalLabel); + + /*! + * Perform Monte Carlo simulation of a step-bounded reachability property. + * Approximates P=? [F<=stepBound label]. + * @param label Goal label to reach. + * @param stepBound Step bound. + * @param numberRuns Number of simulation runs to perform. + * @return Probability of satisfying the property. Calculated as the ratio of runs reaching the label within stepBound / numberRuns. + */ + ValueType simulateStepBoundedReachability(std::string const& label, uint64_t stepBound, uint64_t numberRuns); + + /*! + * Perform Monte Carlo simulation of a time-bounded reachability property (for continuous-time models). + * Approximates P=? [F<=timeBound label]. + * @param label Goal label to reach. + * @param timebound Time bound. + * @param numberRuns Number of simulation runs to perform. + * @return Probability of satisfying the property. Calculated as the ratio of runs reaching the label within timeBound / numberRuns. + */ + ValueType simulateTimeBoundedReachability(std::string const& label, ValueType timebound, uint64_t numberRuns); + + /*! + * Return the underlying simulator. + * @return Simulator. + */ + std::shared_ptr const> getSimulator() const; + + private: + /*! + * Check whether the current state of the simulator contains the given label. + * @param goalLabel Label to reach. + * @return True if current state contains goal label. Always returns false if no goal label was provided. + */ + bool reachedLabel(std::optional const& goalLabel) const; + + /// The underlying simulator + std::shared_ptr> simulator; +}; +} // namespace simulator +} // namespace storm \ No newline at end of file diff --git a/src/test/storm/simulator/TraceSimulatorTest.cpp b/src/test/storm/simulator/TraceSimulatorTest.cpp new file mode 100644 index 0000000000..3a831f8425 --- /dev/null +++ b/src/test/storm/simulator/TraceSimulatorTest.cpp @@ -0,0 +1,86 @@ +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/api/storm-parsers.h" +#include "storm/api/builder.h" +#include "storm/simulator/SparseModelSimulator.h" +#include "storm/simulator/TraceSimulator.h" + +// Helper functions +template +std::shared_ptr> createModelSimulator(std::string const& file) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::api::parseProgram(file, true); + storm::builder::BuilderOptions options; + options.setBuildAllLabels(); + auto model = storm::api::buildSparseModel(program, options); + + auto sparseModelSimulator = std::make_shared>(model); + sparseModelSimulator->setSeed(5); + return sparseModelSimulator; +} + +template +ValueType parseNumber(std::string const& input) { + return storm::utility::convertNumber(input); +} + +TEST(TraceSimulatorTest, KnuthYaoDieDtmc) { + auto modelSimulator = createModelSimulator(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); + storm::simulator::TraceSimulator simulator(modelSimulator); + + double result = simulator.simulateStepBoundedReachability("one", 100, 10000); + EXPECT_NEAR(parseNumber("1/6"), result, 0.01); + + result = simulator.simulateStepBoundedReachability("init", 100, 10000); + EXPECT_NEAR(parseNumber("1"), result, 0.01); + + result = simulator.simulateStepBoundedReachability("two", 100, 10000); + EXPECT_NEAR(parseNumber("1/6"), result, 0.01); +} + +TEST(TraceSimulatorTest, KnuthYaoDiceMdp) { + auto modelSimulator = createModelSimulator(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); + storm::simulator::TraceSimulator simulator(modelSimulator); + + double result = simulator.simulateStepBoundedReachability("two", 100, 10000); + EXPECT_NEAR(parseNumber("1/32"), result, 0.01); + + result = simulator.simulateStepBoundedReachability("three", 100, 10000); + EXPECT_NEAR(parseNumber("2/32"), result, 0.01); + + result = simulator.simulateStepBoundedReachability("four", 100, 20000); + EXPECT_NEAR(parseNumber("3/32"), result, 0.01); +} + +TEST(TraceSimulatorTest, EmbeddedCtmc) { + auto modelSimulator = createModelSimulator(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); + storm::simulator::TraceSimulator simulator(modelSimulator); + + double result = simulator.simulateTimeBoundedReachability("network_full", 10000, 10000); + EXPECT_NEAR(0.0019216435246119591, result, 0.01); + + result = simulator.simulateTimeBoundedReachability("fail_io", 10000, 10000); + EXPECT_NEAR(0.001911229643, result, 0.01); +} + +TEST(TraceSimulatorTest, TandemCtmc) { + auto modelSimulator = createModelSimulator(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); + storm::simulator::TraceSimulator simulator(modelSimulator); + + double result = simulator.simulateTimeBoundedReachability("network_full", 10, 10000); + EXPECT_NEAR(0.015446370562428037, result, 0.01); + + result = simulator.simulateTimeBoundedReachability("first_queue_full", 10, 10000); + EXPECT_NEAR(0.999999837225515, result, 0.01); +} + +TEST(TraceSimulatorTest, ServerMA) { + auto modelSimulator = createModelSimulator(STORM_TEST_RESOURCES_DIR "/ma/server.ma"); + storm::simulator::TraceSimulator simulator(modelSimulator); + + double result = simulator.simulateTimeBoundedReachability("error", 1, 10000); + EXPECT_TRUE(storm::utility::isBetween(0.382120908, result, 0.455504)); +} From f4ebeeb5a2f344fd167c758a00dbd3f8f08ca9c0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 8 Dec 2025 10:40:12 +0100 Subject: [PATCH 10/11] Introduced general (abstract) class ModelSimulator --- src/storm/simulator/ModelSimulator.cpp | 61 +++++++++ src/storm/simulator/ModelSimulator.h | 128 ++++++++++++++++++ src/storm/simulator/SparseModelSimulator.cpp | 88 +++++------- src/storm/simulator/SparseModelSimulator.h | 72 ++++++---- src/storm/simulator/TraceSimulator.cpp | 7 +- src/storm/simulator/TraceSimulator.h | 10 +- .../simulator/SparseModelSimulatorTest.cpp | 20 +-- .../storm/simulator/TraceSimulatorTest.cpp | 112 ++++++++------- 8 files changed, 346 insertions(+), 152 deletions(-) create mode 100644 src/storm/simulator/ModelSimulator.cpp create mode 100644 src/storm/simulator/ModelSimulator.h diff --git a/src/storm/simulator/ModelSimulator.cpp b/src/storm/simulator/ModelSimulator.cpp new file mode 100644 index 0000000000..5c17a54949 --- /dev/null +++ b/src/storm/simulator/ModelSimulator.cpp @@ -0,0 +1,61 @@ +#include "storm/simulator/ModelSimulator.h" + +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" + +namespace storm { +namespace simulator { + +template +ModelSimulator::ModelSimulator() : currentTime(storm::utility::zero()), randomGenerator() { + // Intentionally left empty +} + +template +void ModelSimulator::setSeed(uint64_t newSeed) { + randomGenerator = storm::utility::RandomProbabilityGenerator(newSeed); +} + +template +bool ModelSimulator::randomStep() { + if (isContinuousTimeModel()) { + // First choose time when to leave the state + randomTime(); + } + + if (isCurrentStateDeadlock()) { + return false; + } + if (getCurrentNumberOfChoices() == 1) { + return step(0); + } + // Select action by uniform distribution + return step(this->randomGenerator.randomSelect(0, getCurrentNumberOfChoices() - 1)); +} + +template +void ModelSimulator::randomTime() { + STORM_LOG_ASSERT(isContinuousTimeModel(), "Model must be continuous-time model"); + ValueType exitRate = getCurrentExitRate(); + if (!storm::utility::isZero(exitRate)) { + STORM_LOG_ASSERT(getCurrentNumberOfChoices() == 1, "Markovian state should have a trivial row group."); + ValueType time = this->randomGenerator.randomExponential(exitRate); + this->currentTime += time; + } +} + +template +ValueType ModelSimulator::getCurrentTime() const { + return currentTime; +} + +template +std::vector const& ModelSimulator::getCurrentRewards() const { + return currentRewards; +} + +template class ModelSimulator; +template class ModelSimulator; + +} // namespace simulator +} // namespace storm diff --git a/src/storm/simulator/ModelSimulator.h b/src/storm/simulator/ModelSimulator.h new file mode 100644 index 0000000000..7be755097e --- /dev/null +++ b/src/storm/simulator/ModelSimulator.h @@ -0,0 +1,128 @@ +#pragma once + +#include "storm/utility/random.h" + +namespace storm { +namespace simulator { + +/*! + * Abstract class for simulator of model. + */ +template +class ModelSimulator { + public: + /*! + * Constructor. + */ + ModelSimulator(); + + /*! + * Destructor. + */ + virtual ~ModelSimulator() = default; + + /*! + * Set specific seed for random number generator. + * Useful to obtain deterministic behaviour of the simulator. + * + * @param seed Seed. + */ + void setSeed(uint64_t seed); + + /*! + * Reset the simulator to the initial state. + */ + virtual void resetToInitial() = 0; + + /*! + * Perform a random step from the current state. + * For probabilistic states: Randomly select an action and then randomly select a transition. + * For Markovian states (only in continuous-time models): Increase the time according to exit rate and then randomly select a transition. + * + * @return Whether the step was successful or not (e.g. deadlock). + */ + bool randomStep(); + + /* + * Increase the current time according to the exit rate in the current state (if continuous-time model). + * Nothing happens if for discrete-time models. + */ + void randomTime(); + + /*! + * Perform the given action and then randomly select a transition. + * + * @param action Action index. + * @return True iff step was successful. + */ + virtual bool step(uint64_t action) = 0; + + /*! + * Time progressed so far. + * Is 0 for discrete-time models. + * + * @return Progressed time. + */ + ValueType getCurrentTime() const; + + /*! + * Return the number of choices for the current state. + * + * @return Number of current choices. + */ + virtual uint64_t getCurrentNumberOfChoices() const = 0; + + /*! + * Return all labels for the current state. + * @return State labels. + */ + virtual std::set getCurrentStateLabelling() const = 0; + + /*! + * Get the rewards for the current state. + * + * @return The current rewards (in the order from getRewardNames()). + */ + std::vector const& getCurrentRewards() const; + + /*! + * The names of the rewards that are returned. + * @return Names of reward models. + */ + virtual std::vector getRewardNames() const = 0; + + /*! + * Get the current exit rate of the state. + * @return State exit rate (if Markovian state in a continuous-time model) or 0 (if probabilistic state or a discrete-time model). + */ + virtual ValueType getCurrentExitRate() const = 0; + + /*! + * Whether the current state is a deadlock. + * + * @return True if the current state has no outgoing transitions. + */ + virtual bool isCurrentStateDeadlock() const = 0; + + /*! + * Whether the model is a continuous-time model. + * + * @return True if the model is continuous-time. + */ + virtual bool isContinuousTimeModel() const = 0; + + protected: + /// Time which has progressed so far. Only relevant for continuous-time models + ValueType currentTime; + + /// The current rewards + std::vector currentRewards; + + /// Used to reinitialize the reward vector to all 0. + std::vector zeroRewards; + + /// Random number generator + storm::utility::RandomProbabilityGenerator randomGenerator; +}; +} // namespace simulator +} // namespace storm \ No newline at end of file diff --git a/src/storm/simulator/SparseModelSimulator.cpp b/src/storm/simulator/SparseModelSimulator.cpp index 848c0b5464..a0783b069a 100644 --- a/src/storm/simulator/SparseModelSimulator.cpp +++ b/src/storm/simulator/SparseModelSimulator.cpp @@ -7,10 +7,11 @@ namespace storm { namespace simulator { template SparseModelSimulator::SparseModelSimulator(std::shared_ptr const> model) - : model(model), zeroRewards(model->getNumberOfRewardModels(), storm::utility::zero()), generator() { - resetToInitial(); + : storm::simulator::ModelSimulator(), model(model) { + this->zeroRewards = std::vector(model->getNumberOfRewardModels(), storm::utility::zero()); + this->resetToInitial(); - if (isContinuousTimeModel()) { + if (this->isContinuousTimeModel()) { if (model->getType() == storm::models::ModelType::Ctmc) { exitRates = model->template as>()->getExitRateVector(); } else { @@ -28,21 +29,18 @@ SparseModelSimulator::SparseModelSimulator(std::shar } } -template -void SparseModelSimulator::setSeed(uint64_t seed) { - generator = storm::utility::RandomProbabilityGenerator(seed); -} template void SparseModelSimulator::resetToInitial() { STORM_LOG_WARN_COND(model->getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states. This simulator assumes it starts from the initial state with the lowest index."); currentState = *model->getInitialStates().begin(); - currentTime = storm::utility::zero(); - lastRewards = zeroRewards; + this->currentTime = storm::utility::zero(); + // Set state rewards + this->currentRewards = this->zeroRewards; uint64_t i = 0; for (auto const& rewModPair : model->getRewardModels()) { if (rewModPair.second.hasStateRewards()) { - lastRewards[i] += rewModPair.second.getStateReward(currentState); + this->currentRewards[i] += rewModPair.second.getStateReward(currentState); } ++i; } @@ -51,14 +49,14 @@ void SparseModelSimulator::resetToInitial() { template uint64_t SparseModelSimulator::choice(uint64_t choice) { STORM_LOG_ASSERT(choice < getCurrentNumberOfChoices(), "Action index higher than number of actions"); - lastRewards = zeroRewards; uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[currentState] + choice; - // Add state-action reward + // Set state-action reward + this->currentRewards = this->zeroRewards; uint64_t i = 0; for (auto const& rewModPair : model->getRewardModels()) { if (rewModPair.second.hasStateActionRewards()) { - lastRewards[i] += rewModPair.second.getStateActionReward(row); + this->currentRewards[i] += rewModPair.second.getStateActionReward(row); } ++i; } @@ -82,59 +80,40 @@ void SparseModelSimulator::transition(uint64_t row, uint64_t i = 0; for (auto const& rewModPair : model->getRewardModels()) { if (rewModPair.second.hasStateRewards()) { - lastRewards[i] += rewModPair.second.getStateReward(currentState); + this->currentRewards[i] += rewModPair.second.getStateReward(currentState); } ++i; } } -template -bool SparseModelSimulator::randomStep() { - if (!model->isDiscreteTimeModel()) { - // First choose time when to leave the state - randomTime(); - } - - if (model->getTransitionMatrix().getRowGroupSize(currentState) == 0) { - return false; - } - if (model->getTransitionMatrix().getRowGroupSize(currentState) == 1) { - return step(0); - } - // Select action by uniform distribution - return step(generator.randomSelect(0, model->getTransitionMatrix().getRowGroupSize(currentState) - 1)); -} - template bool SparseModelSimulator::step(uint64_t action) { // Perform action uint64_t row = choice(action); if (model->getTransitionMatrix().getRow(row).getNumberOfEntries() == 1) { - // Select only transition + // Select the only transition uint64_t column = model->getTransitionMatrix().getRow(row).begin()->getColumn(); transition(row, column); return true; } // Randomly select transition - ValueType probability = generator.randomProbability(); + ValueType probability = this->randomGenerator.randomProbability(); + if (model->getType() == storm::models::ModelType::Ctmc) { + // Scale probability to exit rate + probability *= getCurrentExitRate(); + } ValueType sum = storm::utility::zero(); for (auto const& entry : model->getTransitionMatrix().getRow(row)) { - if (model->getType() == storm::models::ModelType::Ctmc) { - // Scale rates to probabilities - sum += entry.getValue() / exitRates[currentState]; - } else { - sum += entry.getValue(); - } + sum += entry.getValue(); if (sum >= probability) { - uint64_t column = entry.getColumn(); - transition(row, column); + transition(row, entry.getColumn()); return true; } } - // This position should never be reached + STORM_LOG_ASSERT(false, "This line should not be reached."); return false; } @@ -146,25 +125,24 @@ bool SparseModelSimulator::step(uint64_t action, uin } template -void SparseModelSimulator::randomTime() { - STORM_LOG_ASSERT(isContinuousTimeModel(), "Model must be continuous-time model"); - ValueType exitRate = exitRates[currentState]; - if (!storm::utility::isZero(exitRate)) { - STORM_LOG_ASSERT(model->getTransitionMatrix().getRowGroupSize(currentState) == 1, "Markovian state should have a trivial row group."); - ValueType time = generator.randomExponential(exitRate); - currentTime += time; +std::vector SparseModelSimulator::getRewardNames() const { + std::vector names; + for (auto name : model->getRewardModels()) { + names.push_back(name.first); } + return names; } template -uint64_t SparseModelSimulator::getCurrentState() const { - return currentState; +ValueType SparseModelSimulator::getCurrentExitRate() const { + return exitRates[currentState]; } template -ValueType SparseModelSimulator::getCurrentTime() const { - return currentTime; +uint64_t SparseModelSimulator::getCurrentState() const { + return currentState; } + template uint64_t SparseModelSimulator::getCurrentNumberOfChoices() const { return model->getTransitionMatrix().getRowGroupSize(currentState); @@ -176,8 +154,8 @@ std::set SparseModelSimulator::getCurre } template -std::vector const& SparseModelSimulator::getLastRewards() const { - return lastRewards; +bool SparseModelSimulator::isCurrentStateDeadlock() const { + return model->getTransitionMatrix().getRowGroupSize(currentState) == 0; } template diff --git a/src/storm/simulator/SparseModelSimulator.h b/src/storm/simulator/SparseModelSimulator.h index 7e684fdd42..71bbb685c6 100644 --- a/src/storm/simulator/SparseModelSimulator.h +++ b/src/storm/simulator/SparseModelSimulator.h @@ -1,65 +1,77 @@ #pragma once #include "storm/models/sparse/Model.h" -#include "storm/utility/random.h" +#include "storm/simulator/ModelSimulator.h" namespace storm { namespace simulator { -/** +/*! * This class is a low-level interface to quickly sample from sparse models. * Additional information about state, actions, should be obtained via the model itself. * * TODO: It may be nice to write a CPP wrapper that does not require to actually obtain such information yourself. */ template> -class SparseModelSimulator { +class SparseModelSimulator : public storm::simulator::ModelSimulator { public: + /*! + * Constructor. + * @param model Sparse model. + */ SparseModelSimulator(std::shared_ptr const> model); - void setSeed(uint64_t); - void resetToInitial(); - /** - * For probabilistic states: Randomly select action and then randomly select transition. - * For Markovian states (only in continuous-time models): Increase time according to exit rate and then randomly select transition. - */ - bool randomStep(); - /** - * Perform action and then randomly select transition. - */ - bool step(uint64_t action); - /** + void resetToInitial() override; + + bool step(uint64_t action) override; + + /*! * Perform action and then select transition corresponding to column. */ bool step(uint64_t action, uint64_t column); - void randomTime(); - + /*! + * Get current state id. + * @return Current state id. + */ uint64_t getCurrentState() const; - ValueType getCurrentTime() const; - uint64_t getCurrentNumberOfChoices() const; - std::set getCurrentStateLabelling() const; - std::vector const& getLastRewards() const; - bool isContinuousTimeModel() const; + uint64_t getCurrentNumberOfChoices() const override; + + std::set getCurrentStateLabelling() const override; + + std::vector getRewardNames() const override; + + ValueType getCurrentExitRate() const override; + + bool isCurrentStateDeadlock() const override; + + bool isContinuousTimeModel() const override; private: - /** + /*! * Select choice, update state-action rewards and return corresponding row. + * + * @param choice Choice index. + * @return Row in sparse matrix corresponding to chosen state-action. */ uint64_t choice(uint64_t choice); + + /*! + * Perform transition from selected row to given column. + * @param row Row in sparse matrix corresponding to chosen state-action. + * @param column Successor state. + */ void transition(uint64_t row, uint64_t column); + /// The underlying sparse model std::shared_ptr const> model; + + /// The current state id uint64_t currentState; - // Time which has progressed so far. Only relevant for continuous-time models - ValueType currentTime; - std::vector lastRewards; - std::vector zeroRewards; - storm::utility::RandomProbabilityGenerator generator; - // Exit rates for continuous-time models + /// Exit rates for continuous-time models std::vector exitRates; }; } // namespace simulator -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/storm/simulator/TraceSimulator.cpp b/src/storm/simulator/TraceSimulator.cpp index 1a42fe7e40..39a197df1a 100644 --- a/src/storm/simulator/TraceSimulator.cpp +++ b/src/storm/simulator/TraceSimulator.cpp @@ -1,13 +1,14 @@ #include "storm/simulator/TraceSimulator.h" #include "storm/exceptions/UnsupportedModelException.h" -#include "storm/simulator/SparseModelSimulator.h" +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" namespace storm { namespace simulator { template -TraceSimulator::TraceSimulator(std::shared_ptr> simulator) : simulator(simulator) { +TraceSimulator::TraceSimulator(std::shared_ptr> simulator) : simulator(simulator) { // Intentionally left empty. } @@ -88,7 +89,7 @@ bool TraceSimulator::reachedLabel(std::optional const& g } template -std::shared_ptr const> TraceSimulator::getSimulator() const { +std::shared_ptr const> TraceSimulator::getSimulator() const { return simulator; } diff --git a/src/storm/simulator/TraceSimulator.h b/src/storm/simulator/TraceSimulator.h index 2cc8d5a915..60cb22d2f5 100644 --- a/src/storm/simulator/TraceSimulator.h +++ b/src/storm/simulator/TraceSimulator.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/simulator/SparseModelSimulator.h" +#include "storm/simulator/ModelSimulator.h" namespace storm { namespace simulator { @@ -13,7 +13,7 @@ namespace simulator { */ enum class SimulationTraceResult { GOAL_REACHED, BOUND_REACHED, DEADLOCK }; -/** +/*! * Perform simulation runs of a model. */ template @@ -23,7 +23,7 @@ class TraceSimulator { * Constructor. * @param simulator Underlying simulator. */ - TraceSimulator(std::shared_ptr> simulator); + TraceSimulator(std::shared_ptr> simulator); /*! * Simulate a single (untimed) trace until either the goal label or the step bound is reached. @@ -65,7 +65,7 @@ class TraceSimulator { * Return the underlying simulator. * @return Simulator. */ - std::shared_ptr const> getSimulator() const; + std::shared_ptr const> getSimulator() const; private: /*! @@ -76,7 +76,7 @@ class TraceSimulator { bool reachedLabel(std::optional const& goalLabel) const; /// The underlying simulator - std::shared_ptr> simulator; + std::shared_ptr> simulator; }; } // namespace simulator } // namespace storm \ No newline at end of file diff --git a/src/test/storm/simulator/SparseModelSimulatorTest.cpp b/src/test/storm/simulator/SparseModelSimulatorTest.cpp index 0962ef1f82..cdb6cb7936 100644 --- a/src/test/storm/simulator/SparseModelSimulatorTest.cpp +++ b/src/test/storm/simulator/SparseModelSimulatorTest.cpp @@ -19,8 +19,8 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieDtmc) { sim.setSeed(42); EXPECT_EQ("coin_flips", model->getRewardModels().begin()->first); EXPECT_EQ(0ul, sim.getCurrentState()); - auto rew = sim.getLastRewards(); - rew = sim.getLastRewards(); + auto rew = sim.getCurrentRewards(); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(0.0, rew[0]); auto labels = sim.getCurrentStateLabelling(); @@ -43,8 +43,8 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieMdp) { sim.setSeed(42); EXPECT_EQ("coin_flips", model->getRewardModels().begin()->first); EXPECT_EQ(0ul, sim.getCurrentState()); - auto rew = sim.getLastRewards(); - rew = sim.getLastRewards(); + auto rew = sim.getCurrentRewards(); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(0.0, rew[0]); auto labels = sim.getCurrentStateLabelling(); @@ -54,7 +54,7 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieMdp) { sim.step(0); EXPECT_EQ(2ul, sim.getCurrentState()); - rew = sim.getLastRewards(); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(0.0, rew[0]); EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); @@ -62,7 +62,7 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieMdp) { sim.randomStep(); EXPECT_EQ(5ul, sim.getCurrentState()); - rew = sim.getLastRewards(); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(1.0, rew[0]); EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); @@ -70,7 +70,7 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieMdp) { sim.randomStep(); EXPECT_EQ(11ul, sim.getCurrentState()); - rew = sim.getLastRewards(); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(1.0, rew[0]); labels = sim.getCurrentStateLabelling(); @@ -81,7 +81,7 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieMdp) { sim.randomStep(); EXPECT_EQ(11ul, sim.getCurrentState()); - rew = sim.getLastRewards(); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(0.0, rew[0]); labels = sim.getCurrentStateLabelling(); @@ -108,8 +108,8 @@ TEST(SparseModelSimulatorTest, SimpleMATest) { // 1st run EXPECT_EQ(0ul, sim.getCurrentState()); - auto rew = sim.getLastRewards(); - rew = sim.getLastRewards(); + auto rew = sim.getCurrentRewards(); + rew = sim.getCurrentRewards(); EXPECT_EQ(0ul, rew.size()); auto labels = sim.getCurrentStateLabelling(); EXPECT_EQ(1ul, labels.size()); diff --git a/src/test/storm/simulator/TraceSimulatorTest.cpp b/src/test/storm/simulator/TraceSimulatorTest.cpp index 3a831f8425..fb7dd06b33 100644 --- a/src/test/storm/simulator/TraceSimulatorTest.cpp +++ b/src/test/storm/simulator/TraceSimulatorTest.cpp @@ -6,81 +6,95 @@ #include "storm/simulator/SparseModelSimulator.h" #include "storm/simulator/TraceSimulator.h" -// Helper functions -template -std::shared_ptr> createModelSimulator(std::string const& file) { +template +class SparseModelSimulator { + public: + typedef CValueType ValueType; + + static std::shared_ptr> createSimulator(std::string const& file, uint64_t seed) { + storm::prism::Program program = storm::api::parseProgram(file, true); + storm::builder::BuilderOptions options; + options.setBuildAllLabels(); + auto model = storm::api::buildSparseModel(program, options); + + auto sparseModelSimulator = std::make_shared>(model); + sparseModelSimulator->setSeed(seed); + return std::make_shared>(sparseModelSimulator); + } +}; + +template +class TraceSimulatorTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + + TraceSimulatorTest() {} + + void SetUp() override { #ifndef STORM_HAVE_Z3 - GTEST_SKIP() << "Z3 not available."; + GTEST_SKIP() << "Z3 not available."; #endif - storm::prism::Program program = storm::api::parseProgram(file, true); - storm::builder::BuilderOptions options; - options.setBuildAllLabels(); - auto model = storm::api::buildSparseModel(program, options); - - auto sparseModelSimulator = std::make_shared>(model); - sparseModelSimulator->setSeed(5); - return sparseModelSimulator; -} + } -template -ValueType parseNumber(std::string const& input) { - return storm::utility::convertNumber(input); -} + std::shared_ptr> createSimulator(std::string const& file) { + return TestType::createSimulator(file, 5); + } + + ValueType parseNumber(std::string const& input) { + return storm::utility::convertNumber(input); + } +}; + +typedef ::testing::Types> TestingTypes; -TEST(TraceSimulatorTest, KnuthYaoDieDtmc) { - auto modelSimulator = createModelSimulator(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - storm::simulator::TraceSimulator simulator(modelSimulator); +TYPED_TEST_SUITE(TraceSimulatorTest, TestingTypes, ); - double result = simulator.simulateStepBoundedReachability("one", 100, 10000); - EXPECT_NEAR(parseNumber("1/6"), result, 0.01); +TYPED_TEST(TraceSimulatorTest, KnuthYaoDieDtmc) { + auto simulator = this->createSimulator(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); - result = simulator.simulateStepBoundedReachability("init", 100, 10000); - EXPECT_NEAR(parseNumber("1"), result, 0.01); + double result = simulator->simulateStepBoundedReachability("one", 100, 10000); + EXPECT_NEAR(this->parseNumber("1/6"), result, 0.01); - result = simulator.simulateStepBoundedReachability("two", 100, 10000); - EXPECT_NEAR(parseNumber("1/6"), result, 0.01); + result = simulator->simulateStepBoundedReachability("two", 100, 10000); + EXPECT_NEAR(this->parseNumber("1/6"), result, 0.01); } -TEST(TraceSimulatorTest, KnuthYaoDiceMdp) { - auto modelSimulator = createModelSimulator(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - storm::simulator::TraceSimulator simulator(modelSimulator); +TYPED_TEST(TraceSimulatorTest, KnuthYaoDiceMdp) { + auto simulator = this->createSimulator(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); - double result = simulator.simulateStepBoundedReachability("two", 100, 10000); - EXPECT_NEAR(parseNumber("1/32"), result, 0.01); + double result = simulator->simulateStepBoundedReachability("two", 100, 10000); + EXPECT_NEAR(this->parseNumber("1/32"), result, 0.01); - result = simulator.simulateStepBoundedReachability("three", 100, 10000); - EXPECT_NEAR(parseNumber("2/32"), result, 0.01); + result = simulator->simulateStepBoundedReachability("three", 100, 10000); + EXPECT_NEAR(this->parseNumber("2/32"), result, 0.01); - result = simulator.simulateStepBoundedReachability("four", 100, 20000); - EXPECT_NEAR(parseNumber("3/32"), result, 0.01); + result = simulator->simulateStepBoundedReachability("four", 100, 2 * 10000); + EXPECT_NEAR(this->parseNumber("3/32"), result, 0.01); } -TEST(TraceSimulatorTest, EmbeddedCtmc) { - auto modelSimulator = createModelSimulator(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); - storm::simulator::TraceSimulator simulator(modelSimulator); +TYPED_TEST(TraceSimulatorTest, EmbeddedCtmc) { + auto simulator = this->createSimulator(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); - double result = simulator.simulateTimeBoundedReachability("network_full", 10000, 10000); + double result = simulator->simulateTimeBoundedReachability("network_full", 10000, 10000); EXPECT_NEAR(0.0019216435246119591, result, 0.01); - result = simulator.simulateTimeBoundedReachability("fail_io", 10000, 10000); + result = simulator->simulateTimeBoundedReachability("fail_io", 10000, 10000); EXPECT_NEAR(0.001911229643, result, 0.01); } -TEST(TraceSimulatorTest, TandemCtmc) { - auto modelSimulator = createModelSimulator(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); - storm::simulator::TraceSimulator simulator(modelSimulator); +TYPED_TEST(TraceSimulatorTest, TandemCtmc) { + auto simulator = this->createSimulator(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); - double result = simulator.simulateTimeBoundedReachability("network_full", 10, 10000); + double result = simulator->simulateTimeBoundedReachability("network_full", 10, 10000); EXPECT_NEAR(0.015446370562428037, result, 0.01); - result = simulator.simulateTimeBoundedReachability("first_queue_full", 10, 10000); + result = simulator->simulateTimeBoundedReachability("first_queue_full", 10, 10000); EXPECT_NEAR(0.999999837225515, result, 0.01); } -TEST(TraceSimulatorTest, ServerMA) { - auto modelSimulator = createModelSimulator(STORM_TEST_RESOURCES_DIR "/ma/server.ma"); - storm::simulator::TraceSimulator simulator(modelSimulator); +TYPED_TEST(TraceSimulatorTest, ServerMA) { + auto simulator = this->createSimulator(STORM_TEST_RESOURCES_DIR "/ma/server.ma"); - double result = simulator.simulateTimeBoundedReachability("error", 1, 10000); + double result = simulator->simulateTimeBoundedReachability("error", 1, 10000); EXPECT_TRUE(storm::utility::isBetween(0.382120908, result, 0.455504)); } From 8f442f1085efa708f52f6de38226c0cf84cdb411 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 8 Dec 2025 14:07:39 +0100 Subject: [PATCH 11/11] Revised PrismProgramSimulator and added tests --- src/storm/simulator/PrismProgramSimulator.cpp | 156 +++++++++----- src/storm/simulator/PrismProgramSimulator.h | 136 +++++++----- .../simulator/PrismProgramSimulatorTest.cpp | 197 ++++++++++++++++-- .../simulator/SparseModelSimulatorTest.cpp | 67 +++++- .../storm/simulator/TraceSimulatorTest.cpp | 21 +- 5 files changed, 439 insertions(+), 138 deletions(-) diff --git a/src/storm/simulator/PrismProgramSimulator.cpp b/src/storm/simulator/PrismProgramSimulator.cpp index 6207373d48..f7f230a445 100644 --- a/src/storm/simulator/PrismProgramSimulator.cpp +++ b/src/storm/simulator/PrismProgramSimulator.cpp @@ -1,6 +1,6 @@ #include "storm/simulator/PrismProgramSimulator.h" + #include "storm/adapters/JsonAdapter.h" -#include "storm/exceptions/NotSupportedException.h" #include "storm/storage/expressions/ExpressionEvaluator.h" using namespace storm::generator; @@ -9,29 +9,48 @@ namespace storm { namespace simulator { template -DiscreteTimePrismProgramSimulator::DiscreteTimePrismProgramSimulator(storm::prism::Program const& program, - storm::generator::NextStateGeneratorOptions const& options) - : program(program), +PrismProgramSimulator::PrismProgramSimulator(storm::prism::Program program, storm::generator::NextStateGeneratorOptions const& options) + : storm::simulator::ModelSimulator(), + program(program), currentState(), stateGenerator(std::make_shared>(program, options)), - zeroRewards(stateGenerator->getNumberOfRewardModels(), storm::utility::zero()), - lastActionRewards(zeroRewards), stateToId(stateGenerator->getStateSize()), idToState() { + this->zeroRewards = std::vector(stateGenerator->getNumberOfRewardModels(), storm::utility::zero()); // Current state needs to be overwritten to actual initial state. - resetToInitial(); + this->resetToInitial(); } template -void DiscreteTimePrismProgramSimulator::setSeed(uint64_t newSeed) { - generator = storm::utility::RandomProbabilityGenerator(newSeed); -} +bool PrismProgramSimulator::step(uint64_t actionNumber) { + STORM_LOG_ASSERT(actionNumber < getCurrentNumberOfChoices(), "Action index higher than number of actions"); + auto choice = getChoices()[actionNumber]; + + // Set state-action reward + this->currentRewards = this->zeroRewards; + if (!isContinuousTimeModel()) { + this->currentRewards = choice.getRewards(); + STORM_LOG_ASSERT(this->currentRewards.size() == stateGenerator->getNumberOfRewardModels(), "Reward vector should have as many rewards as model."); + } else { + // TODO add support + STORM_LOG_WARN("State-action rewards are currently not supported for continuous-time models."); + } + + uint64_t nextState; + if (choice.size() == 1) { + // Select only transition + nextState = choice.begin()->first; + } else { + // Randomly select transition + ValueType probability = this->randomGenerator.randomProbability(); + if (program.getModelType() == storm::prism::Program::ModelType::CTMC || + (program.getModelType() == storm::prism::Program::ModelType::MA && choice.isMarkovian())) { + // Scale probability to exit rate + probability *= getCurrentExitRate(); + } + nextState = choice.sampleFromDistribution(probability); + } -template -bool DiscreteTimePrismProgramSimulator::step(uint64_t actionNumber) { - uint32_t nextState = behavior.getChoices()[actionNumber].sampleFromDistribution(generator.randomProbability()); - lastActionRewards = behavior.getChoices()[actionNumber].getRewards(); - STORM_LOG_ASSERT(lastActionRewards.size() == stateGenerator->getNumberOfRewardModels(), "Reward vector should have as many rewards as model."); currentState = idToState[nextState]; // TODO we do not need to do this in every step! clearStateCaches(); @@ -40,24 +59,29 @@ bool DiscreteTimePrismProgramSimulator::step(uint64_t actionNumber) { } template -bool DiscreteTimePrismProgramSimulator::explore() { +void PrismProgramSimulator::explore() { // Load the current state into the next state generator. stateGenerator->load(currentState); // TODO: This low-level code currently expands all actions, while this is not necessary. - // However, using the next state generator ensures compatibliity with the model generator. + // However, using the next state generator ensures compatibility with the model generator. behavior = stateGenerator->expand(stateToIdCallback); - STORM_LOG_ASSERT(behavior.getStateRewards().size() == lastActionRewards.size(), "Reward vectors should have same length."); + STORM_LOG_ASSERT(behavior.getStateRewards().size() == this->currentRewards.size(), "Reward vectors should have same length."); for (uint64_t i = 0; i < behavior.getStateRewards().size(); i++) { - lastActionRewards[i] += behavior.getStateRewards()[i]; + this->currentRewards[i] += behavior.getStateRewards()[i]; } - return true; } template -bool DiscreteTimePrismProgramSimulator::isSinkState() const { - if (behavior.empty()) { +bool PrismProgramSimulator::isCurrentStateDeadlock() const { + return behavior.empty(); +} + +template +bool PrismProgramSimulator::isSinkState() const { + if (isCurrentStateDeadlock()) { return true; } + std::set successorIds; for (Choice const& choice : behavior.getChoices()) { for (auto it = choice.begin(); it != choice.end(); ++it) { @@ -74,76 +98,106 @@ bool DiscreteTimePrismProgramSimulator::isSinkState() const { } template -std::vector DiscreteTimePrismProgramSimulator::getCurrentStateLabelling() const { - std::vector labels; +std::set PrismProgramSimulator::getCurrentStateLabelling() const { + std::set labels; for (auto const& label : program.getLabels()) { if (stateGenerator->evaluateBooleanExpressionInCurrentState(label.getStatePredicateExpression())) { - labels.push_back(label.getName()); + labels.insert(label.getName()); } } return labels; } template -std::vector> const& DiscreteTimePrismProgramSimulator::getChoices() const { +std::vector> const& PrismProgramSimulator::getChoices() const { return behavior.getChoices(); } template -std::vector const& DiscreteTimePrismProgramSimulator::getLastRewards() const { - return lastActionRewards; +uint64_t PrismProgramSimulator::getCurrentNumberOfChoices() const { + return getChoices().size(); } template -CompressedState const& DiscreteTimePrismProgramSimulator::getCurrentState() const { +ValueType PrismProgramSimulator::getCurrentExitRate() const { + if (!isContinuousTimeModel()) { + // Discrete-time models have no exit rate + return storm::utility::zero(); + } + + if (isCurrentStateDeadlock()) { + return storm::utility::zero(); + } + if (getCurrentNumberOfChoices() > 1) { + // Probabilistic state + return storm::utility::zero(); + } + + STORM_LOG_ASSERT(getCurrentNumberOfChoices() == 1, "Expected deterministic state."); + auto choice = getChoices().front(); + ValueType totalMass = choice.getTotalMass(); + // CTMC or (MA and Markovian) => totalMass > 0 + STORM_LOG_ASSERT(!(program.getModelType() == storm::prism::Program::ModelType::CTMC || + (program.getModelType() == storm::prism::Program::ModelType::MA && choice.isMarkovian())) || + storm::utility::isPositive(totalMass), + "Expected positive exit rate."); + // MA and not Markovian => totalMass = 1 + STORM_LOG_ASSERT(!(program.getModelType() == storm::prism::Program::ModelType::MA && !choice.isMarkovian()) || storm::utility::isOne(totalMass), + "Probabilities should sum up to one."); + return totalMass; +} + +template +CompressedState const& PrismProgramSimulator::getCurrentState() const { return currentState; } template -expressions::SimpleValuation DiscreteTimePrismProgramSimulator::getCurrentStateAsValuation() const { +expressions::SimpleValuation PrismProgramSimulator::getCurrentStateAsValuation() const { return unpackStateIntoValuation(currentState, stateGenerator->getVariableInformation(), program.getManager()); } template -std::string DiscreteTimePrismProgramSimulator::getCurrentStateString() const { +std::string PrismProgramSimulator::getCurrentStateString() const { return stateGenerator->stateToString(currentState); } template -storm::json DiscreteTimePrismProgramSimulator::getStateAsJson() const { +storm::json PrismProgramSimulator::getStateAsJson() const { return stateGenerator->currentStateToJson(false); } template -storm::json DiscreteTimePrismProgramSimulator::getObservationAsJson() const { +storm::json PrismProgramSimulator::getObservationAsJson() const { return stateGenerator->currentStateToJson(true); } template -bool DiscreteTimePrismProgramSimulator::resetToInitial() { - lastActionRewards = zeroRewards; +void PrismProgramSimulator::resetToInitial() { auto indices = stateGenerator->getInitialStates(stateToIdCallback); - STORM_LOG_THROW(indices.size() == 1, storm::exceptions::NotSupportedException, "Program must have a unique initial state"); - currentState = idToState[indices[0]]; - return explore(); + STORM_LOG_WARN_COND(indices.size() == 1, + "The model has multiple initial states. This simulator assumes it starts from the initial state with the lowest index."); + resetToState(idToState[indices[0]], storm::utility::zero()); } template -bool DiscreteTimePrismProgramSimulator::resetToState(generator::CompressedState const& newState) { - lastActionRewards = zeroRewards; +void PrismProgramSimulator::resetToState(generator::CompressedState const& newState, ValueType time) { + this->currentRewards = this->zeroRewards; + this->currentTime = time; currentState = newState; - return explore(); + explore(); } template -bool DiscreteTimePrismProgramSimulator::resetToState(expressions::SimpleValuation const& valuation) { - lastActionRewards = zeroRewards; +void PrismProgramSimulator::resetToState(expressions::SimpleValuation const& valuation, ValueType time) { + this->currentRewards = this->zeroRewards; + this->currentTime = time; currentState = generator::packStateFromValuation(valuation, stateGenerator->getVariableInformation(), true); - return explore(); + explore(); } template -std::vector DiscreteTimePrismProgramSimulator::getRewardNames() const { +std::vector PrismProgramSimulator::getRewardNames() const { std::vector names; for (uint64_t i = 0; i < stateGenerator->getNumberOfRewardModels(); ++i) { names.push_back(stateGenerator->getRewardModelInformation(i).getName()); @@ -152,7 +206,12 @@ std::vector DiscreteTimePrismProgramSimulator::getReward } template -uint32_t DiscreteTimePrismProgramSimulator::getOrAddStateIndex(generator::CompressedState const& state) { +bool PrismProgramSimulator::isContinuousTimeModel() const { + return !program.isDiscreteTimeModel(); +} + +template +uint32_t PrismProgramSimulator::getOrAddStateIndex(generator::CompressedState const& state) { uint32_t newIndex = static_cast(stateToId.size()); // Check, if the state was already registered. @@ -166,11 +225,12 @@ uint32_t DiscreteTimePrismProgramSimulator::getOrAddStateIndex(genera } template -void DiscreteTimePrismProgramSimulator::clearStateCaches() { +void PrismProgramSimulator::clearStateCaches() { idToState.clear(); stateToId = storm::storage::BitVectorHashMap(stateGenerator->getStateSize()); } -template class DiscreteTimePrismProgramSimulator; +template class PrismProgramSimulator; +template class PrismProgramSimulator; } // namespace simulator } // namespace storm diff --git a/src/storm/simulator/PrismProgramSimulator.h b/src/storm/simulator/PrismProgramSimulator.h index ef8473a923..d7fad35dc3 100644 --- a/src/storm/simulator/PrismProgramSimulator.h +++ b/src/storm/simulator/PrismProgramSimulator.h @@ -1,14 +1,15 @@ #pragma once +#include "storm/simulator/ModelSimulator.h" + #include "storm/generator/PrismNextStateGenerator.h" #include "storm/storage/expressions/SimpleValuation.h" #include "storm/storage/prism/Program.h" -#include "storm/utility/random.h" namespace storm { namespace simulator { -/** +/*! * This class provides a simulator interface on the prism program, * and uses the next state generator. While the next state generator has been tuned, * it is not targeted for simulation purposes. In particular, we (as of now) @@ -18,101 +19,126 @@ namespace simulator { * On the other hand, this simulator is convenient for stepping through the model * as it potentially allows considering the next states. * Thus, while a performant alternative would be great, this simulator has its own merits. - * - * @tparam ValueType */ template -class DiscreteTimePrismProgramSimulator { +class PrismProgramSimulator : public ModelSimulator { public: - /** + /*! * Initialize the simulator for a given prism program. * * @param program The prism program. Should have a unique initial state. * @param options The generator options that are used to generate successor states. */ - DiscreteTimePrismProgramSimulator(storm::prism::Program const& program, storm::generator::NextStateGeneratorOptions const& options); - /** - * Set the simulation seed. + PrismProgramSimulator(storm::prism::Program program, storm::generator::NextStateGeneratorOptions const& options); + + void resetToInitial() override; + + /*! + * Reset the current state to the given state. + * @param compressedState State to reset to. + * @param time Time to reset to. */ - void setSeed(uint64_t); - /** - * + void resetToState(generator::CompressedState const& compressedState, ValueType time); + + /*! + * Reset the current state to the given state. + * @param valuationState State to reset to. + * @param time Time to reset to. + */ + void resetToState(expressions::SimpleValuation const& valuationState, ValueType time); + + bool step(uint64_t actionNumber) override; + + /*! + * Get choices in current state. * @return A list of choices that encode the possibilities in the current state. - * @note successor states are encoded using state indices that will potentially be invalidated as soon as the internal state of the simulator changes + * @note Successor states are encoded using state indices that will potentially be invalidated as soon as the internal state of the simulator changes. */ std::vector> const& getChoices() const; - bool isSinkState() const; + uint64_t getCurrentNumberOfChoices() const override; - /** - * Make a step and randomly select the successor. The action is given as an argument, the index reflects the index of the getChoices vector that can be - * accessed. - * - * @param actionNumber The action to select. - * @return true, if this action can be taken. + /*! + * Get current state. + * @return Current state. */ - bool step(uint64_t actionNumber); - /** - * Accessor for the last state action reward and the current state reward, added together. - * @return A vector with te number of rewards. - */ - std::vector const& getLastRewards() const; generator::CompressedState const& getCurrentState() const; + + /*! + * Get valuation of current state. + * @return Valuation. + */ expressions::SimpleValuation getCurrentStateAsValuation() const; - std::vector getCurrentStateLabelling() const; + /*! + * Get string representation of current state. + * @return String representation of current state. + */ + std::string getCurrentStateString() const; + + /*! + * Get json representation of current state. + * @return Json representation of current state. + */ storm::json getStateAsJson() const; - storm::json getObservationAsJson() const; + std::set getCurrentStateLabelling() const override; - std::string getCurrentStateString() const; - /** - * Reset to the (unique) initial state. - * - * @return + /*! + * Get json representation of observations. + * @return Json representation of observations. */ - bool resetToInitial(); + storm::json getObservationAsJson() const; + + std::vector getRewardNames() const override; + + ValueType getCurrentExitRate() const override; + + bool isCurrentStateDeadlock() const override; - bool resetToState(generator::CompressedState const& compressedState); + /*! + * Whether the current state is an absorbing state. + * @return True if current state is absorbing. + */ + bool isSinkState() const; - bool resetToState(expressions::SimpleValuation const& valuationState); + bool isContinuousTimeModel() const override; - /** - * The names of the rewards that are returned. + private: + /*! + * Explore the current state and create choices and distribution over successor states. */ - std::vector getRewardNames() const; + void explore(); - protected: - bool explore(); + /*! + * Clear all state caches. + */ void clearStateCaches(); - /** + + /*! * Helper function for (temp) storing states. + * + * @param state State. + * @return Index of state. */ - uint32_t getOrAddStateIndex(generator::CompressedState const&); + uint32_t getOrAddStateIndex(generator::CompressedState const& state); /// The program that we are simulating. - storm::prism::Program const& program; + storm::prism::Program program; /// The current state in the program, in its compressed form. generator::CompressedState currentState; /// Generator for the next states std::shared_ptr> stateGenerator; /// Obtained behavior of a state generator::StateBehavior behavior; - /// Helper for last action reward construction - std::vector zeroRewards; - /// Stores the action rewards from the last action. - std::vector lastActionRewards; - /// Random number generator - storm::utility::RandomProbabilityGenerator generator; - /// Data structure to temp store states. + /// Data structure to temporarily store states. storm::storage::BitVectorHashMap stateToId; - + /// Data structure to temporarily store ids to states. std::unordered_map idToState; - private: - // Create a callback for the next-state generator to enable it to request the index of states. + /// Create a callback for the next-state generator to enable it to request the index of states. std::function stateToIdCallback = - std::bind(&DiscreteTimePrismProgramSimulator::getOrAddStateIndex, this, std::placeholders::_1); + std::bind(&PrismProgramSimulator::getOrAddStateIndex, this, std::placeholders::_1); }; } // namespace simulator } // namespace storm diff --git a/src/test/storm/simulator/PrismProgramSimulatorTest.cpp b/src/test/storm/simulator/PrismProgramSimulatorTest.cpp index 50e0b0929f..c16a6b0f42 100644 --- a/src/test/storm/simulator/PrismProgramSimulatorTest.cpp +++ b/src/test/storm/simulator/PrismProgramSimulatorTest.cpp @@ -2,54 +2,205 @@ #include "test/storm_gtest.h" #include "storm-parsers/parser/PrismParser.h" -#include "storm/environment/Environment.h" +#include "storm/adapters/JsonAdapter.h" #include "storm/simulator/PrismProgramSimulator.h" -TEST(PrismProgramSimulatorTest, KnuthYaoDieTest) { +TEST(PrismProgramSimulatorTest, KnuthYaoDieDtmc) { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; #endif - storm::Environment env; - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); storm::builder::BuilderOptions options; options.setBuildAllRewardModels(); + options.setBuildAllLabels(); - storm::simulator::DiscreteTimePrismProgramSimulator sim(program, options); + storm::simulator::PrismProgramSimulator sim(program, options); sim.setSeed(42); + EXPECT_FALSE(sim.isContinuousTimeModel()); EXPECT_EQ("coin_flips", sim.getRewardNames()[0]); - auto rew = sim.getLastRewards(); - rew = sim.getLastRewards(); + + EXPECT_EQ(0ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0ul, sim.getStateAsJson()["d"]); + auto rew = sim.getCurrentRewards(); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(0.0, rew[0]); auto labels = sim.getCurrentStateLabelling(); EXPECT_EQ(0ul, labels.size()); - EXPECT_EQ(2ul, sim.getChoices().size()); - sim.step(0); - rew = sim.getLastRewards(); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_EQ(0, sim.getCurrentTime()); +} + +TEST(PrismProgramSimulatorTest, KnuthYaoDieMdp) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm"); + storm::builder::BuilderOptions options; + options.setBuildAllRewardModels(); + options.setBuildAllLabels(); + + storm::simulator::PrismProgramSimulator sim(program, options); + sim.setSeed(42); + EXPECT_FALSE(sim.isContinuousTimeModel()); + EXPECT_EQ("coin_flips", sim.getRewardNames()[0]); + + EXPECT_EQ(0ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0ul, sim.getStateAsJson()["d"]); + auto rew = sim.getCurrentRewards(); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(0.0, rew[0]); - labels = sim.getCurrentStateLabelling(); + auto labels = sim.getCurrentStateLabelling(); EXPECT_EQ(0ul, labels.size()); - EXPECT_EQ(1ul, sim.getChoices().size()); + EXPECT_EQ(2ul, sim.getCurrentNumberOfChoices()); + sim.step(0); - rew = sim.getLastRewards(); + EXPECT_EQ(02ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0ul, sim.getStateAsJson()["d"]); + rew = sim.getCurrentRewards(); + EXPECT_EQ(1ul, rew.size()); + EXPECT_EQ(0.0, rew[0]); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + + sim.randomStep(); + EXPECT_EQ(5ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0ul, sim.getStateAsJson()["d"]); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(1.0, rew[0]); - labels = sim.getCurrentStateLabelling(); - EXPECT_EQ(0ul, labels.size()); - sim.step(0); - rew = sim.getLastRewards(); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + + sim.randomStep(); + EXPECT_EQ(7ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(5ul, sim.getStateAsJson()["d"]); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(1.0, rew[0]); labels = sim.getCurrentStateLabelling(); EXPECT_EQ(2ul, labels.size()); - EXPECT_TRUE(std::count(labels.begin(), labels.end(), "done") == 1); - EXPECT_TRUE(std::count(labels.begin(), labels.end(), "five") == 1); - sim.step(0); - rew = sim.getLastRewards(); + EXPECT_TRUE(labels.contains("done")); + EXPECT_TRUE(labels.contains("five")); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + + sim.randomStep(); + EXPECT_EQ(7ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(5ul, sim.getStateAsJson()["d"]); + rew = sim.getCurrentRewards(); EXPECT_EQ(1ul, rew.size()); EXPECT_EQ(0.0, rew[0]); labels = sim.getCurrentStateLabelling(); - EXPECT_TRUE(std::count(labels.begin(), labels.end(), "done") == 1); - EXPECT_TRUE(std::count(labels.begin(), labels.end(), "five") == 1); + EXPECT_EQ(2ul, labels.size()); + EXPECT_TRUE(labels.contains("done")); + EXPECT_TRUE(labels.contains("five")); + + EXPECT_EQ(0, sim.getCurrentTime()); +} + +TEST(PrismProgramSimulatorTest, SimpleCtmc) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/simple2.sm"); + storm::builder::BuilderOptions options; + options.setBuildAllRewardModels(); + options.setBuildAllLabels(); + + storm::simulator::PrismProgramSimulator sim(program, options); + sim.setSeed(5); + EXPECT_TRUE(sim.isContinuousTimeModel()); + EXPECT_EQ(2ul, sim.getRewardNames().size()); + + EXPECT_EQ(0ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(2ul, sim.getCurrentRewards().size()); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_EQ(0, sim.getCurrentTime()); + + sim.randomStep(); + EXPECT_EQ(2ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_NEAR(0.007095, sim.getCurrentTime(), 1e-6); + + sim.randomStep(); + EXPECT_EQ(3ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_NEAR(0.007095 + 0.452143, sim.getCurrentTime(), 1e-6); + + sim.randomStep(); + EXPECT_EQ(4ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_NEAR(0.007095 + 0.452143 + 0.094114, sim.getCurrentTime(), 1e-6); +} + +TEST(PrismProgramSimulatorTest, SimpleMA) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma"); + storm::builder::BuilderOptions options; + options.setBuildAllRewardModels(); + options.setBuildAllLabels(); + + storm::simulator::PrismProgramSimulator sim(program, options); + sim.setSeed(5); + EXPECT_TRUE(sim.isContinuousTimeModel()); + EXPECT_EQ(0ul, sim.getRewardNames().size()); + + // 1st run + EXPECT_EQ(0ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0ul, sim.getCurrentRewards().size()); + auto labels = sim.getCurrentStateLabelling(); + EXPECT_EQ(0ul, labels.size()); + EXPECT_EQ(2ul, sim.getCurrentNumberOfChoices()); + EXPECT_EQ(0, sim.getCurrentTime()); + + sim.step(1); + EXPECT_EQ(0ul, sim.getStateAsJson()["s"]); + labels = sim.getCurrentStateLabelling(); + EXPECT_EQ(0ul, labels.size()); + EXPECT_EQ(2ul, sim.getCurrentNumberOfChoices()); + EXPECT_EQ(0, sim.getCurrentTime()); + + sim.step(1); + EXPECT_EQ(2ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_EQ(0, sim.getCurrentTime()); + + sim.randomStep(); + EXPECT_EQ(4ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_NEAR(0.037679, sim.getCurrentTime(), 1e-6); + + // 2nd run + sim.resetToInitial(); + EXPECT_EQ(0ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0, sim.getCurrentTime()); + sim.step(0); + EXPECT_EQ(1ul, sim.getStateAsJson()["s"]); + EXPECT_EQ(0, sim.getCurrentTime()); + sim.randomStep(); + EXPECT_EQ(0ul, sim.getStateAsJson()["s"]); + EXPECT_NEAR(0.388465, sim.getCurrentTime(), 1e-6); + + sim.step(0); + EXPECT_EQ(1ul, sim.getStateAsJson()["s"]); + EXPECT_NEAR(0.388465, sim.getCurrentTime(), 1e-6); + sim.randomStep(); + EXPECT_EQ(0ul, sim.getStateAsJson()["s"]); + EXPECT_NEAR(0.388465 + 0.050540, sim.getCurrentTime(), 1e-6); + + sim.step(0); + EXPECT_EQ(1ul, sim.getStateAsJson()["s"]); + EXPECT_NEAR(0.388465 + 0.050540, sim.getCurrentTime(), 1e-6); + sim.randomStep(); + EXPECT_EQ(3ul, sim.getStateAsJson()["s"]); + EXPECT_NEAR(0.388465 + 0.050540 + 0.066677, sim.getCurrentTime(), 1e-6); } diff --git a/src/test/storm/simulator/SparseModelSimulatorTest.cpp b/src/test/storm/simulator/SparseModelSimulatorTest.cpp index cdb6cb7936..651bd6eaef 100644 --- a/src/test/storm/simulator/SparseModelSimulatorTest.cpp +++ b/src/test/storm/simulator/SparseModelSimulatorTest.cpp @@ -17,7 +17,9 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieDtmc) { storm::simulator::SparseModelSimulator sim(model); sim.setSeed(42); - EXPECT_EQ("coin_flips", model->getRewardModels().begin()->first); + EXPECT_FALSE(sim.isContinuousTimeModel()); + EXPECT_EQ("coin_flips", sim.getRewardNames()[0]); + EXPECT_EQ(0ul, sim.getCurrentState()); auto rew = sim.getCurrentRewards(); rew = sim.getCurrentRewards(); @@ -27,6 +29,7 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieDtmc) { EXPECT_EQ(1ul, labels.size()); EXPECT_EQ("init", *labels.begin()); EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_EQ(0, sim.getCurrentTime()); } TEST(SparseModelSimulatorTest, KnuthYaoDieMdp) { @@ -41,7 +44,8 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieMdp) { storm::simulator::SparseModelSimulator sim(model); sim.setSeed(42); - EXPECT_EQ("coin_flips", model->getRewardModels().begin()->first); + EXPECT_FALSE(sim.isContinuousTimeModel()); + EXPECT_EQ("coin_flips", sim.getRewardNames()[0]); EXPECT_EQ(0ul, sim.getCurrentState()); auto rew = sim.getCurrentRewards(); rew = sim.getCurrentRewards(); @@ -75,8 +79,8 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieMdp) { EXPECT_EQ(1.0, rew[0]); labels = sim.getCurrentStateLabelling(); EXPECT_EQ(2ul, labels.size()); - EXPECT_TRUE(std::count(labels.begin(), labels.end(), "done") == 1); - EXPECT_TRUE(std::count(labels.begin(), labels.end(), "five") == 1); + EXPECT_TRUE(labels.contains("done")); + EXPECT_TRUE(labels.contains("five")); EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); sim.randomStep(); @@ -86,13 +90,55 @@ TEST(SparseModelSimulatorTest, KnuthYaoDieMdp) { EXPECT_EQ(0.0, rew[0]); labels = sim.getCurrentStateLabelling(); EXPECT_EQ(2ul, labels.size()); - EXPECT_TRUE(std::count(labels.begin(), labels.end(), "done") == 1); - EXPECT_TRUE(std::count(labels.begin(), labels.end(), "five") == 1); + EXPECT_TRUE(labels.contains("done")); + EXPECT_TRUE(labels.contains("five")); EXPECT_EQ(0, sim.getCurrentTime()); } -TEST(SparseModelSimulatorTest, SimpleMATest) { +TEST(SparseModelSimulatorTest, SimpleCtmc) { +#ifndef STORM_HAVE_Z3 + GTEST_SKIP() << "Z3 not available."; +#endif + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/simple2.sm"); + storm::builder::BuilderOptions options; + options.setBuildAllRewardModels(); + options.setBuildAllLabels(); + auto model = storm::api::buildSparseModel(program, options)->template as>(); + + storm::simulator::SparseModelSimulator sim(model); + sim.setSeed(5); + EXPECT_TRUE(sim.isContinuousTimeModel()); + EXPECT_EQ(2ul, sim.getRewardNames().size()); + + EXPECT_EQ(0ul, sim.getCurrentState()); + EXPECT_EQ(2ul, sim.getCurrentRewards().size()); + auto labels = sim.getCurrentStateLabelling(); + EXPECT_EQ(1ul, labels.size()); + EXPECT_EQ("init", *labels.begin()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_EQ(0, sim.getCurrentTime()); + + sim.randomStep(); + EXPECT_EQ(2ul, sim.getCurrentState()); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_NEAR(0.007095, sim.getCurrentTime(), 1e-6); + + sim.randomStep(); + EXPECT_EQ(3ul, sim.getCurrentState()); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_NEAR(0.007095 + 0.452143, sim.getCurrentTime(), 1e-6); + + sim.randomStep(); + EXPECT_EQ(4ul, sim.getCurrentState()); + EXPECT_EQ(0ul, sim.getCurrentStateLabelling().size()); + EXPECT_EQ(1ul, sim.getCurrentNumberOfChoices()); + EXPECT_NEAR(0.007095 + 0.452143 + 0.094114, sim.getCurrentTime(), 1e-6); +} + +TEST(SparseModelSimulatorTest, SimpleMA) { #ifndef STORM_HAVE_Z3 GTEST_SKIP() << "Z3 not available."; #endif @@ -104,13 +150,12 @@ TEST(SparseModelSimulatorTest, SimpleMATest) { storm::simulator::SparseModelSimulator sim(model); sim.setSeed(5); - EXPECT_EQ(0ul, model->getRewardModels().size()); + EXPECT_TRUE(sim.isContinuousTimeModel()); + EXPECT_EQ(0ul, sim.getRewardNames().size()); // 1st run EXPECT_EQ(0ul, sim.getCurrentState()); - auto rew = sim.getCurrentRewards(); - rew = sim.getCurrentRewards(); - EXPECT_EQ(0ul, rew.size()); + EXPECT_EQ(0ul, sim.getCurrentRewards().size()); auto labels = sim.getCurrentStateLabelling(); EXPECT_EQ(1ul, labels.size()); EXPECT_EQ("init", *labels.begin()); diff --git a/src/test/storm/simulator/TraceSimulatorTest.cpp b/src/test/storm/simulator/TraceSimulatorTest.cpp index fb7dd06b33..10566f7bd8 100644 --- a/src/test/storm/simulator/TraceSimulatorTest.cpp +++ b/src/test/storm/simulator/TraceSimulatorTest.cpp @@ -3,9 +3,28 @@ #include "storm-parsers/api/storm-parsers.h" #include "storm/api/builder.h" +#include "storm/simulator/PrismProgramSimulator.h" #include "storm/simulator/SparseModelSimulator.h" #include "storm/simulator/TraceSimulator.h" +template +class PrismProgramSimulator { + public: + typedef CValueType ValueType; + + static std::shared_ptr> createSimulator(std::string const& file, uint64_t seed) { + storm::prism::Program program = storm::api::parseProgram(file, true); + program = storm::utility::prism::preprocess(program, ""); // Needed for Tandem for some reason + storm::builder::BuilderOptions options; + options.setBuildAllRewardModels(); + options.setBuildAllLabels(); + + auto prismProgramSimulator = std::make_shared>(program, options); + prismProgramSimulator->setSeed(seed); + return std::make_shared>(prismProgramSimulator); + } +}; + template class SparseModelSimulator { public: @@ -45,7 +64,7 @@ class TraceSimulatorTest : public ::testing::Test { } }; -typedef ::testing::Types> TestingTypes; +typedef ::testing::Types, SparseModelSimulator> TestingTypes; TYPED_TEST_SUITE(TraceSimulatorTest, TestingTypes, );