Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SymmetryTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-dft/api/storm-dft.h"
5#include "storm-dft/utility/SymmetryFinder.h"
6
7namespace {
8
9storm::dft::storage::DftSymmetries findSymmetries(std::string const& file) {
10 // Load, and build DFT
11 std::shared_ptr<storm::dft::storage::DFT<double>> dft = storm::dft::api::loadDFTGalileoFile<double>(file);
12 // Find symmetries
13 return storm::dft::utility::SymmetryFinder<double>::findSymmetries(*dft);
14}
15
16TEST(SymmetryTest, SymmetriesStaticFT) {
17 auto symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
18 EXPECT_EQ(symmetries.nrSymmetries(), 1ul);
19 EXPECT_EQ(symmetries.getSymmetryGroup(0).size(), 1ul);
20 EXPECT_EQ(symmetries.getSymmetryGroup(0)[0].size(), 2ul);
21
22 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/or.dft");
23 EXPECT_EQ(symmetries.nrSymmetries(), 1ul);
24 EXPECT_EQ(symmetries.getSymmetryGroup(0).size(), 1ul);
25 EXPECT_EQ(symmetries.getSymmetryGroup(0)[0].size(), 2ul);
26
27 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/voting.dft");
28 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
29 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/voting2.dft");
30 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
31 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/voting3.dft");
32 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
33 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/voting4.dft");
34 EXPECT_EQ(symmetries.nrSymmetries(), 1ul);
35 EXPECT_EQ(symmetries.getSymmetryGroup(0).size(), 1ul);
36 EXPECT_EQ(symmetries.getSymmetryGroup(0)[0].size(), 2ul);
37 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/voting5.dft");
38 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
39}
40
41TEST(SymmetryTest, SymmetriesDynamicFT) {
42 auto symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pand.dft");
43 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
44
45 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/por.dft");
46 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
47
48 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/spare.dft");
49 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
50 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/spare2.dft");
51 EXPECT_EQ(symmetries.nrSymmetries(), 1ul);
52 EXPECT_EQ(symmetries.getSymmetryGroup(2).size(), 2ul);
53 EXPECT_EQ(symmetries.getSymmetryGroup(2)[0].size(), 2ul);
54 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/spare3.dft");
55 EXPECT_EQ(symmetries.nrSymmetries(), 1ul);
56 EXPECT_EQ(symmetries.getSymmetryGroup(2).size(), 2ul);
57 EXPECT_EQ(symmetries.getSymmetryGroup(2)[0].size(), 3ul);
58 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/spare4.dft");
59 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
60 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft");
61 EXPECT_EQ(symmetries.nrSymmetries(), 1ul);
62 EXPECT_EQ(symmetries.getSymmetryGroup(1).size(), 1ul);
63 EXPECT_EQ(symmetries.getSymmetryGroup(1)[0].size(), 2ul);
64 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/spare6.dft");
65 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
66 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/spare7.dft");
67 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
68 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/spare8.dft");
69 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
70
71 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft");
72 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
73 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft");
74 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
75 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/fdep3.dft");
76 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
77 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft");
78 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
79 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft");
80 EXPECT_EQ(symmetries.nrSymmetries(), 1ul);
81 EXPECT_EQ(symmetries.getSymmetryGroup(1).size(), 1ul);
82 EXPECT_EQ(symmetries.getSymmetryGroup(1)[0].size(), 2ul);
83 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/fdep6.dft");
84 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
85 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/fdep7.dft");
86 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
87
88 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft");
89 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
90 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft");
91 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
92 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft");
93 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
94 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft");
95 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
96
97 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq.dft");
98 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
99 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq2.dft");
100 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
101 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq3.dft");
102 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
103 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq4.dft");
104 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
105 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq5.dft");
106 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
107 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq6.dft");
108 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
109
110 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/mutex.dft");
111 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
112 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/mutex2.dft");
113 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
114 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft");
115 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
116 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/mutex4.dft");
117 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
118
119 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/all_be_distributions.dft");
120 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
121 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/all_gates.dft");
122 EXPECT_EQ(symmetries.nrSymmetries(), 2ul);
123 EXPECT_EQ(symmetries.getSymmetryGroup(21).size(), 2ul);
124 EXPECT_EQ(symmetries.getSymmetryGroup(21)[0].size(), 4ul);
125 EXPECT_EQ(symmetries.getSymmetryGroup(32).size(), 1ul);
126 EXPECT_EQ(symmetries.getSymmetryGroup(32)[0].size(), 2ul);
127}
128
129TEST(SymmetryTest, SymmetricFT) {
130 auto symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/symmetry6.dft");
131 EXPECT_EQ(symmetries.nrSymmetries(), 5ul);
132 EXPECT_EQ(symmetries.getSymmetryGroup(12).size(), 1ul);
133 EXPECT_EQ(symmetries.getSymmetryGroup(12)[0].size(), 2ul);
134 EXPECT_EQ(symmetries.getSymmetryGroup(10).size(), 1ul);
135 EXPECT_EQ(symmetries.getSymmetryGroup(10)[0].size(), 2ul);
136 EXPECT_EQ(symmetries.getSymmetryGroup(14).size(), 5ul);
137 EXPECT_EQ(symmetries.getSymmetryGroup(14)[0].size(), 2ul);
138 EXPECT_EQ(symmetries.getSymmetryGroup(0).size(), 1ul);
139 EXPECT_EQ(symmetries.getSymmetryGroup(0)[0].size(), 2ul);
140 EXPECT_EQ(symmetries.getSymmetryGroup(2).size(), 3ul);
141 EXPECT_EQ(symmetries.getSymmetryGroup(2)[0].size(), 3ul);
142
143 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/symmetry7.dft");
144 EXPECT_EQ(symmetries.nrSymmetries(), 3ul);
145 EXPECT_EQ(symmetries.getSymmetryGroup(0).size(), 1ul);
146 EXPECT_EQ(symmetries.getSymmetryGroup(0)[0].size(), 3ul);
147 EXPECT_EQ(symmetries.getSymmetryGroup(5).size(), 1ul);
148 EXPECT_EQ(symmetries.getSymmetryGroup(5)[0].size(), 2ul);
149 EXPECT_EQ(symmetries.getSymmetryGroup(7).size(), 1ul);
150 EXPECT_EQ(symmetries.getSymmetryGroup(7)[0].size(), 2ul);
151
152 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep_symmetry.dft");
153 EXPECT_EQ(symmetries.nrSymmetries(), 2ul);
154 EXPECT_EQ(symmetries.getSymmetryGroup(2).size(), 4ul);
155 EXPECT_EQ(symmetries.getSymmetryGroup(2)[0].size(), 2ul);
156 EXPECT_EQ(symmetries.getSymmetryGroup(6).size(), 9ul);
157 EXPECT_EQ(symmetries.getSymmetryGroup(6)[0].size(), 2ul);
158
159 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft//hecs_2_2.dft");
160 EXPECT_EQ(symmetries.nrSymmetries(), 4ul);
161 EXPECT_EQ(symmetries.getSymmetryGroup(2).size(), 2ul);
162 EXPECT_EQ(symmetries.getSymmetryGroup(2)[0].size(), 2ul);
163 EXPECT_EQ(symmetries.getSymmetryGroup(12).size(), 1ul);
164 EXPECT_EQ(symmetries.getSymmetryGroup(12)[0].size(), 2ul);
165 EXPECT_EQ(symmetries.getSymmetryGroup(6).size(), 1ul);
166 EXPECT_EQ(symmetries.getSymmetryGroup(6)[0].size(), 5ul);
167 EXPECT_EQ(symmetries.getSymmetryGroup(18).size(), 19ul);
168 EXPECT_EQ(symmetries.getSymmetryGroup(18)[0].size(), 2ul);
169}
170
171} // namespace
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:8
storm::dft::utility::SymmetryFinder::findSymmetries
static storm::dft::storage::DftSymmetries findSymmetries(storm::dft::storage::DFT< ValueType > const &dft)
Find symmetries in the given DFT.
Definition SymmetryFinder.cpp:10
storm_gtest.h