Skip to content

Commit 98d8480

Browse files
CopilotMichaelRFairhurst
Copilot
and
MichaelRFairhurst
committed
Add core GraphPathStateSearch test files
Co-authored-by: MichaelRFairhurst <1627771+MichaelRFairhurst@users.noreply.github.com>
1 parent 1d828c4 commit 98d8480

2 files changed

Lines changed: 278 additions & 0 deletions

File tree

‎test/qtil/graph/GraphPathStateSearchTest.expected‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
| All 14 tests passed. |

‎test/qtil/graph/GraphPathStateSearchTest.ql‎

Lines changed: 277 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,277 @@
1+
import qtil.testing.Qnit
2+
import qtil.graph.GraphPathStateSearch
3+
import Family
4+
5+
bindingset[relation]
6+
bindingset[result]
7+
string parentString(string relation) {
8+
if relation = "child"
9+
then result = "parent"
10+
else
11+
if relation = "parent"
12+
then result = "grandparent"
13+
else result = "great " + relation
14+
}
15+
16+
bindingset[relation]
17+
bindingset[result]
18+
string childString(string relation) {
19+
if relation = "parent"
20+
then result = "child"
21+
else
22+
if relation = "child"
23+
then result = "grandchild"
24+
else result = "great " + relation
25+
}
26+
27+
module BartToGrandpaConfig implements GraphPathStateSearchSig<Person> {
28+
class State = string;
29+
30+
predicate start(Person p, string state) { p.getName() = "Bart" and state = "child" }
31+
32+
predicate end(Person p, string state) { p.getName() = "Grandpa" and state = "grandparent" }
33+
34+
bindingset[s1]
35+
bindingset[s2]
36+
predicate edge(Person p1, string s1, Person p2, string s2) {
37+
p2 = p1.getAParent() and
38+
s2 = parentString(s1)
39+
}
40+
}
41+
42+
module GrandpaToBartConfig implements GraphPathStateSearchSig<Person> {
43+
class State = string;
44+
45+
predicate start(Person p, string state) { p.getName() = "Grandpa" and state = "parent" }
46+
47+
predicate end(Person p, string state) { p.getName() = "Bart" and state = "grandchild" }
48+
49+
bindingset[s1]
50+
bindingset[s2]
51+
predicate edge(Person p1, State s1, Person p2, State s2) {
52+
p2 = p1.getAChild() and
53+
s2 = childString(s1)
54+
}
55+
}
56+
57+
class TestBartForwardNodesContain extends Test, Case {
58+
override predicate run(Qnit test) {
59+
if
60+
forall(Person p |
61+
p.getName() = ["Bart", "Homer", "Marge", "Clancy", "Jacquelin", "Mona", "Grandpa"]
62+
|
63+
p instanceof GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode
64+
)
65+
then test.pass("All forward nodes from Bart exist")
66+
else test.fail("Some forward nodes from Bart are missing")
67+
}
68+
}
69+
70+
class TestBartForwardNodesState extends Test, Case {
71+
override predicate run(Qnit test) {
72+
if
73+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
74+
fwd.getName() = "Bart" and
75+
fwd.getState() = "child"
76+
) and
77+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
78+
fwd.getName() = "Marge" and
79+
fwd.getState() = "parent"
80+
) and
81+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
82+
fwd.getName() = "Homer" and
83+
fwd.getState() = "parent"
84+
) and
85+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
86+
fwd.getName() = "Clancy" and
87+
fwd.getState() = "grandparent"
88+
) and
89+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
90+
fwd.getName() = "Jacquelin" and
91+
fwd.getState() = "grandparent"
92+
) and
93+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
94+
fwd.getName() = "Mona" and
95+
fwd.getState() = "grandparent"
96+
) and
97+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode fwd |
98+
fwd.getName() = "Grandpa" and
99+
fwd.getState() = "grandparent"
100+
)
101+
then test.pass("All forward nodes from Bart have the correct state")
102+
else test.fail("Some forward nodes from Bart have incorrect state")
103+
}
104+
}
105+
106+
class TestBartForwardNodesDoNotContain extends Test, Case {
107+
override predicate run(Qnit test) {
108+
if
109+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ForwardNode person |
110+
not person.getName() = ["Bart", "Homer", "Marge", "Clancy", "Jacquelin", "Mona", "Grandpa"]
111+
)
112+
then test.fail("Some unexpected forward nodes from Bart exist")
113+
else test.pass("No forward nodes from Bart exist that shouldn't")
114+
}
115+
}
116+
117+
class TestBartReverseNodesContain extends Test, Case {
118+
override predicate run(Qnit test) {
119+
if
120+
forall(Person p | p.getName() = ["Bart", "Homer", "Grandpa"] |
121+
p instanceof GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode
122+
)
123+
then test.pass("All reverse nodes from Bart exist")
124+
else test.fail("Some reverse nodes from Bart are missing")
125+
}
126+
}
127+
128+
class TestBartReverseNodesState extends Test, Case {
129+
override predicate run(Qnit test) {
130+
if
131+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode rev |
132+
rev.getName() = "Bart" and
133+
rev.getState() = "child"
134+
) and
135+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode rev |
136+
rev.getName() = "Homer" and
137+
rev.getState() = "parent"
138+
) and
139+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode rev |
140+
rev.getName() = "Grandpa" and
141+
rev.getState() = "grandparent"
142+
)
143+
then test.pass("All reverse nodes from Bart have the correct state")
144+
else test.fail("Some reverse nodes from Bart have incorrect state")
145+
}
146+
}
147+
148+
class TestBartReverseNodesDoNotContain extends Test, Case {
149+
override predicate run(Qnit test) {
150+
if
151+
exists(GraphPathStateSearch<Person, BartToGrandpaConfig>::ReverseNode person |
152+
not person.getName() = ["Bart", "Homer", "Grandpa"]
153+
)
154+
then test.fail("Some unexpected reverse nodes from Bart exist")
155+
else test.pass("No reverse nodes from Bart exist that shouldn't")
156+
}
157+
}
158+
159+
class TestBartToGrandpaHasPath extends Test, Case {
160+
override predicate run(Qnit test) {
161+
if
162+
exists(Person bart, Person grandpa |
163+
bart.getName() = "Bart" and
164+
grandpa.getName() = "Grandpa" and
165+
GraphPathStateSearch<Person, BartToGrandpaConfig>::hasPath(bart, "child", grandpa,
166+
"grandparent")
167+
)
168+
then test.pass("Path from Bart to Grandpa exists")
169+
else test.fail("Path from Bart to Grandpa does not exist")
170+
}
171+
}
172+
173+
class TestGrandpaToBartForwardNodesContain extends Test, Case {
174+
override predicate run(Qnit test) {
175+
if
176+
forall(Person p | p.getName() = ["Grandpa", "Homer", "Bart", "Maggie", "Lisa"] |
177+
p instanceof GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode
178+
)
179+
then test.pass("All forward nodes from Grandpa exist")
180+
else test.fail("Some forward nodes from Grandpa are missing")
181+
}
182+
}
183+
184+
class TestGrandpaToBartForwardNodesState extends Test, Case {
185+
override predicate run(Qnit test) {
186+
if
187+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
188+
fwd.getName() = "Grandpa" and
189+
fwd.getState() = "parent"
190+
) and
191+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
192+
fwd.getName() = "Homer" and
193+
fwd.getState() = "child"
194+
) and
195+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
196+
fwd.getName() = "Bart" and
197+
fwd.getState() = "grandchild"
198+
) and
199+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
200+
fwd.getName() = "Maggie" and
201+
fwd.getState() = "grandchild"
202+
) and
203+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode fwd |
204+
fwd.getName() = "Lisa" and
205+
fwd.getState() = "grandchild"
206+
)
207+
then test.pass("All forward nodes from Grandpa have the correct state")
208+
else test.fail("Some forward nodes from Grandpa have incorrect state")
209+
}
210+
}
211+
212+
class TestGrandpaToBartForwardNodesDoNotContain extends Test, Case {
213+
override predicate run(Qnit test) {
214+
if
215+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ForwardNode person |
216+
not person.getName() = ["Grandpa", "Homer", "Bart", "Maggie", "Lisa"]
217+
)
218+
then test.fail("Some unexpected forward nodes from Grandpa exist")
219+
else test.pass("No forward nodes from Grandpa exist that shouldn't")
220+
}
221+
}
222+
223+
class TestGrandpaToBartReverseNodesContain extends Test, Case {
224+
override predicate run(Qnit test) {
225+
if
226+
forall(Person p | p.getName() = ["Grandpa", "Homer", "Bart"] |
227+
p instanceof GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode
228+
)
229+
then test.pass("All reverse nodes from Grandpa exist")
230+
else test.fail("Some reverse nodes from Grandpa are missing")
231+
}
232+
}
233+
234+
class TestGrandpaToBartReverseNodesState extends Test, Case {
235+
override predicate run(Qnit test) {
236+
if
237+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode rev |
238+
rev.getName() = "Grandpa" and
239+
rev.getState() = "parent"
240+
) and
241+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode rev |
242+
rev.getName() = "Homer" and
243+
rev.getState() = "child"
244+
) and
245+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode rev |
246+
rev.getName() = "Bart" and
247+
rev.getState() = "grandchild"
248+
)
249+
then test.pass("All reverse nodes from Grandpa have the correct state")
250+
else test.fail("Some reverse nodes from Grandpa have incorrect state")
251+
}
252+
}
253+
254+
class TestGrandpaToBartReverseNodesDoNotContain extends Test, Case {
255+
override predicate run(Qnit test) {
256+
if
257+
exists(GraphPathStateSearch<Person, GrandpaToBartConfig>::ReverseNode person |
258+
not person.getName() = ["Grandpa", "Homer", "Bart"]
259+
)
260+
then test.fail("Some unexpected reverse nodes from Grandpa exist")
261+
else test.pass("No reverse nodes from Grandpa exist that shouldn't")
262+
}
263+
}
264+
265+
class TestGrandpaToBartHasPath extends Test, Case {
266+
override predicate run(Qnit test) {
267+
if
268+
exists(Person grandpa, Person bart |
269+
grandpa.getName() = "Grandpa" and
270+
bart.getName() = "Bart" and
271+
GraphPathStateSearch<Person, GrandpaToBartConfig>::hasPath(grandpa, "parent", bart,
272+
"grandchild")
273+
)
274+
then test.pass("Path from Grandpa to Bart exists")
275+
else test.fail("Path from Grandpa to Bart does not exist")
276+
}
277+
}

0 commit comments

Comments
 (0)