1#include "storm-config.h"
13struct DftTracesConfig {
18class NoOptimizationsConfig {
22 static DftTracesConfig createConfig() {
23 return DftTracesConfig{
false,
false};
31 static DftTracesConfig createConfig() {
32 return DftTracesConfig{
true,
false};
36class SymmetryReductionConfig {
40 static DftTracesConfig createConfig() {
41 return DftTracesConfig{
false,
true};
45class AllOptimizationsConfig {
49 static DftTracesConfig createConfig() {
50 return DftTracesConfig{
true,
true};
55template<
typename TestType>
56class DftTraceGeneratorTest :
public ::testing::Test {
58 typedef typename TestType::ValueType
ValueType;
60 DftTraceGeneratorTest() : config(TestType::createConfig()) {}
62 DftTracesConfig
const& getConfig()
const {
68 std::shared_ptr<storm::dft::storage::DFT<double>> dft =
69 storm::dft::api::prepareForMarkovAnalysis<double>(*(storm::dft::api::loadDFTGalileoFile<double>(file)));
73 std::vector<std::string> relevantNames;
75 relevantNames.push_back(
"all");
78 dft->setRelevantEvents(relevantEvents,
false);
86 return std::make_pair(dft, stateGenerationInfo);
90 DftTracesConfig config;
93typedef ::testing::Types<NoOptimizationsConfig, DontCareConfig, SymmetryReductionConfig, AllOptimizationsConfig>
TestingTypes;
98 auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR
"/dft/and.dft");
99 auto dft = pair.first;
100 EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, pair.second.hasSymmetries());
104 auto state = generator.createInitialState();
105 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
107 bool changed = state->orderBySymmetry();
108 EXPECT_FALSE(changed);
111 auto iterFailable = state->getFailableElements().begin();
112 ASSERT_NE(iterFailable, state->getFailableElements().end());
114 ASSERT_NE(iterFailable, state->getFailableElements().end());
115 EXPECT_FALSE(iterFailable.isFailureDueToDependency());
117 auto nextBE = iterFailable.asBE(*dft);
118 EXPECT_EQ(nextBE->name(),
"C");
119 state = generator.createSuccessorState(state, nextBE);
120 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
121 changed = state->orderBySymmetry();
122 EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, changed);
123 if (this->getConfig().useSR && this->getConfig().useDC) {
124 EXPECT_TRUE(state->hasFailed(0));
126 EXPECT_TRUE(state->hasFailed(1));
130 iterFailable = state->getFailableElements().begin();
131 ASSERT_NE(iterFailable, state->getFailableElements().end());
132 EXPECT_FALSE(iterFailable.isFailureDueToDependency());
134 nextBE = iterFailable.asBE(*dft);
135 if (this->getConfig().useSR && this->getConfig().useDC) {
138 EXPECT_EQ(nextBE->name(),
"C");
140 EXPECT_EQ(nextBE->name(),
"B");
142 state = generator.createSuccessorState(state, nextBE);
143 changed = state->orderBySymmetry();
144 EXPECT_FALSE(changed);
145 EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex()));
148TYPED_TEST(DftTraceGeneratorTest, RandomStepsAnd) {
149 auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR
"/dft/and.dft");
150 auto dft = pair.first;
151 EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, pair.second.hasSymmetries());
154 boost::mt19937 gen(5u);
157 auto state = simulator.getCurrentState();
158 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
163#if BOOST_VERSION > 106400
165 EXPECT_NEAR(simulator.getCurrentTime(), 0.522079, 1e-6);
167 state = simulator.getCurrentState();
168 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
170 res = simulator.randomStep();
172#if BOOST_VERSION > 106400
174 EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214, 1e-6);
176 state = simulator.getCurrentState();
177 EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex()));
181 auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR
"/dft/and.dft");
182 auto dft = pair.first;
183 EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, pair.second.hasSymmetries());
186 boost::mt19937 gen(5u);
189 auto state = simulator.getCurrentState();
190 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
195#if BOOST_VERSION > 106400
197 EXPECT_NEAR(simulator.getCurrentTime(), 0.522079, 1e-6);
199 auto stateStep1 = simulator.getCurrentState();
200 EXPECT_FALSE(stateStep1->hasFailed(dft->getTopLevelIndex()));
202 res = simulator.randomStep();
204#if BOOST_VERSION > 106400
206 EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214, 1e-6);
208 state = simulator.getCurrentState();
209 EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex()));
212 simulator.resetToState(stateStep1);
213 state = simulator.getCurrentState();
214 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
216 res = simulator.randomStep();
218#if BOOST_VERSION > 106400
220 EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214 + 2.4686932, 1e-6);
222 state = simulator.getCurrentState();
223 EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex()));
227 auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR
"/dft/fdep.dft");
228 auto dft = pair.first;
231 boost::mt19937 gen(5u);
235 auto state = simulator.getCurrentState();
236 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
239 auto iterFailable = state->getFailableElements().begin();
240 ASSERT_NE(iterFailable, state->getFailableElements().end());
242 ASSERT_NE(iterFailable, state->getFailableElements().end());
244 ASSERT_NE(iterFailable, state->getFailableElements().end());
246 EXPECT_FALSE(iterFailable.isFailureDueToDependency());
247 auto nextBE = iterFailable.asBE(*dft);
248 EXPECT_EQ(nextBE->name(),
"B_Power");
252 state = simulator.getCurrentState();
253 EXPECT_TRUE(state->hasFailed(4));
256 iterFailable = state->getFailableElements().begin();
257 ASSERT_NE(iterFailable, state->getFailableElements().end());
259 ASSERT_NE(iterFailable, state->getFailableElements().end());
261 EXPECT_TRUE(iterFailable.isFailureDueToDependency());
262 auto dependency = iterFailable.asDependency(*dft);
263 EXPECT_EQ(dependency->dependentEvents().front()->name(),
"B");
265 res = simulator.step(iterFailable);
267 state = simulator.getCurrentState();
268 EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex()));
Next state generator for DFTs.
static storm::dft::storage::DftSymmetries findSymmetries(storm::dft::storage::DFT< ValueType > const &dft)
Find symmetries in the given DFT.
std::pair< bool, std::string > isWellFormed(storm::dft::storage::DFT< ValueType > const &dft, bool validForMarkovianAnalysis=true)
Check whether the DFT is well-formed.
storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector< std::shared_ptr< storm::logic::Formula const > > const &properties, std::vector< std::string > const &additionalRelevantEventNames)
Get relevant event ids from given relevant event names and labels in properties.
SFTBDDChecker::ValueType ValueType
SimulationStepResult
Result of a single simulation step.
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes