-
Notifications
You must be signed in to change notification settings - Fork 2
/
things_to_test
76 lines (60 loc) · 2.35 KB
/
things_to_test
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
#RANDOM CRAP.
#ASSAGE.
(x := 3; x = 3) == (x := 3)
(x = 3; y = 4) == (y = 4; x = 3)
(x := 3; y := 4) == (y := 4; x := 3)
(x := 1; y = 2) == (y = 2; x := 1)
(dup; x = 3) == (x = 3; dup)
(x = 3; x:= 3) == (x = 3)
(x := 3; x:=4 ) == (x := 4)
(x = 3; x = 4) == drop
(x = 3 + x != 3) == pass
(x != 3) <= x != 4
(x := 3; x :=4; x := 5) == x:=5
(x := 3; x :=4; x := 2; x := 5) == x:=5
(x := 3; x :=4; x := 2; x := 1; x := 5) == x:=5
(x := 3; x :=4; x := 2; x := 1; x := 0; x := 5) == x:=5
(x := 3; x :=4; x := 2; x := 1; x := 0; x := 6; x := 5) == x:=5
(x := 3; x :=4; x := 2; x := 1; x := 0; x := 6; x := 7; x := 5) == x:=5
(x := 3; y :=4; x := 2; y := 1; x := 0; y := 6; x := 7; x := 5) == x:=5; y := 6
(y := 1; x := 0; y := 6; x := 5) == x:=5; y := 6
x := 0; y := 6; x := 5 == x := 5; y := 6
z := 3; y := 6; x := 5 <= z := 4; x := 5 y := 6
(x = 3 + z = 4) + drop == (x = 3 + z = 4)
(x = 3 + z = 4) + (x = 3 + z = 4) == (x = 3 + z = 4)
pass; (x = 3 + z = 4) == (x = 3 + z = 4)
(x = 3 + z = 4); pass == (x = 3 + z = 4)
(y = 2);(x = 3 + z = 4) == (y = 2);(x = 3) + (y = 2);(z = 4)
(x = 3 + z = 4);(y = 2) == (x = 3);(y = 2) + (z = 4);(y = 2)
x = 3 <= x = 4
drop; (x = 3 + z = 4) == drop
(x = 3 + z = 4); drop == drop
pass + (x = 3 + z = 4); (x = 3 + z = 4)* == (x = 3 + z = 4)*
# this is a trolltastic test. it's true because both sides are equivalent
# to the sum of all tests.
(z = 5) + ((x = 3 + z = 4); (x = 3 + z = 4)*) <= z = 5 + (x = 3 + z = 4)*
#BOOLEAN ALGEBRA TIME!
(x = 4) + ~(x = 4) == pass
(x = 4); ~(x = 4) == drop
#DUP-TACULAR!
dup; x = 5 == x = 5; dup
#PACKET ALGEBRA
x := 4; x = 4 == x:= 4
x = 4; x := 4 == x = 4
x = 3; x = 5 == drop
#from the other project
( switch = 0; (switch := 1))* <= drop
(x := 4; x:= 3; x = 3)* == pass + x := 3
(x := 4; x:= 3; x = 3) <= pass + x := 3
(x := 4; x:= 3; x = 3) == x := 3
#simple hops through the network
sw = 0; sw := 1; dup; sw = 1; sw := 2; dup == sw = 0; sw := 1; dup; sw := 2; dup
sw = 0; sw := 1; dup; sw = 1 == sw = 0; sw := 1; dup
(y = 3 + z = 4;z := 4)*;(y = 4 + z = 5)*== (y = 3 + z = 4; z := 4)*;(y = 4 + z = 5)*
(a=3);(b=4);(c=2;c:=3 + c=3;c:=2)*;(d=1);(e=4);(f=0) <= a = 0
pass + (a=1;b:=2);(c=3;drop) + (c=3;drop) <= c=3;drop
pass <= drop
x = 1; dup <= dup
#This exploits non-canonicity of FDDs, naive implementation gets it wrong
f:=1;g := 2 == f:=1;g:=2 + g=2;f := 1
f=0;g:=0 + f=1;g:=1 + f!=1;g:=0 == f=1;g:=1 + f!=1;g:=0