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
84 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft");
85 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
86 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft");
87 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
88 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft");
89 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
90 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft");
91 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
92
93 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq.dft");
94 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
95 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq2.dft");
96 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
97 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq3.dft");
98 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
99 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq4.dft");
100 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
101 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq5.dft");
102 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
103 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/seq6.dft");
104 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
105
106 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/mutex.dft");
107 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
108 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/mutex2.dft");
109 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
110 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft");
111 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
112 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/mutex4.dft");
113 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
114
115 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/all_be_distributions.dft");
116 EXPECT_EQ(symmetries.nrSymmetries(), 0ul);
117 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/all_gates.dft");
118 EXPECT_EQ(symmetries.nrSymmetries(), 2ul);
119 EXPECT_EQ(symmetries.getSymmetryGroup(21).size(), 2ul);
120 EXPECT_EQ(symmetries.getSymmetryGroup(21)[0].size(), 4ul);
121 EXPECT_EQ(symmetries.getSymmetryGroup(32).size(), 1ul);
122 EXPECT_EQ(symmetries.getSymmetryGroup(32)[0].size(), 2ul);
123}
124
125TEST(SymmetryTest, SymmetricFT) {
126 auto symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/symmetry6.dft");
127 EXPECT_EQ(symmetries.nrSymmetries(), 5ul);
128 EXPECT_EQ(symmetries.getSymmetryGroup(12).size(), 1ul);
129 EXPECT_EQ(symmetries.getSymmetryGroup(12)[0].size(), 2ul);
130 EXPECT_EQ(symmetries.getSymmetryGroup(10).size(), 1ul);
131 EXPECT_EQ(symmetries.getSymmetryGroup(10)[0].size(), 2ul);
132 EXPECT_EQ(symmetries.getSymmetryGroup(14).size(), 5ul);
133 EXPECT_EQ(symmetries.getSymmetryGroup(14)[0].size(), 2ul);
134 EXPECT_EQ(symmetries.getSymmetryGroup(0).size(), 1ul);
135 EXPECT_EQ(symmetries.getSymmetryGroup(0)[0].size(), 2ul);
136 EXPECT_EQ(symmetries.getSymmetryGroup(2).size(), 3ul);
137 EXPECT_EQ(symmetries.getSymmetryGroup(2)[0].size(), 3ul);
138
139 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/symmetry7.dft");
140 EXPECT_EQ(symmetries.nrSymmetries(), 3ul);
141 EXPECT_EQ(symmetries.getSymmetryGroup(0).size(), 1ul);
142 EXPECT_EQ(symmetries.getSymmetryGroup(0)[0].size(), 3ul);
143 EXPECT_EQ(symmetries.getSymmetryGroup(5).size(), 1ul);
144 EXPECT_EQ(symmetries.getSymmetryGroup(5)[0].size(), 2ul);
145 EXPECT_EQ(symmetries.getSymmetryGroup(7).size(), 1ul);
146 EXPECT_EQ(symmetries.getSymmetryGroup(7)[0].size(), 2ul);
147
148 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft/pdep_symmetry.dft");
149 EXPECT_EQ(symmetries.nrSymmetries(), 2ul);
150 EXPECT_EQ(symmetries.getSymmetryGroup(2).size(), 4ul);
151 EXPECT_EQ(symmetries.getSymmetryGroup(2)[0].size(), 2ul);
152 EXPECT_EQ(symmetries.getSymmetryGroup(6).size(), 9ul);
153 EXPECT_EQ(symmetries.getSymmetryGroup(6)[0].size(), 2ul);
154
155 symmetries = findSymmetries(STORM_TEST_RESOURCES_DIR "/dft//hecs_2_2.dft");
156 EXPECT_EQ(symmetries.nrSymmetries(), 4ul);
157 EXPECT_EQ(symmetries.getSymmetryGroup(2).size(), 2ul);
158 EXPECT_EQ(symmetries.getSymmetryGroup(2)[0].size(), 2ul);
159 EXPECT_EQ(symmetries.getSymmetryGroup(12).size(), 1ul);
160 EXPECT_EQ(symmetries.getSymmetryGroup(12)[0].size(), 2ul);
161 EXPECT_EQ(symmetries.getSymmetryGroup(6).size(), 1ul);
162 EXPECT_EQ(symmetries.getSymmetryGroup(6)[0].size(), 5ul);
163 EXPECT_EQ(symmetries.getSymmetryGroup(18).size(), 19ul);
164 EXPECT_EQ(symmetries.getSymmetryGroup(18)[0].size(), 2ul);
165}
166
167} // 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