-
Notifications
You must be signed in to change notification settings - Fork 1
/
test_theme.thm
90 lines (71 loc) · 2.63 KB
/
test_theme.thm
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
<?xml version="1.0"?>
<alloy>
<view>
<defaultnode/>
<defaultedge/>
<node>
<type name="ATOMIC_EXCH_BRANCH"/>
<type name="END"/>
<type name="Int"/>
<type name="ONE"/>
<type name="START"/>
<type name="String"/>
<type name="univ"/>
<type name="ZERO"/>
<type name="seq/Int"/>
<set name="$interesting_a" type="A"/>
</node>
<node shape="Dbl Octagon" color="Red">
<type name="G_memory"/>
</node>
<node shape="Egg" color="Yellow">
<type name="Thread"/>
</node>
<node shape="Ellipse" color="Blue">
<type name="S"/>
</node>
<node shape="Octagon" color="White">
<type name="Instruction"/>
</node>
<node visible="no">
<type name="V"/>
<type name="X"/>
</node>
<node visible="yes" color="Green">
<type name="A"/>
</node>
<node visible="yes" hideunconnected="no" numberatoms="yes" shape="Octagon" color="Gray">
<type name="L_state"/>
</node>
<edge attribute="no" constraint="yes">
<relation name="po"> <type name="Instruction"/> <type name="Instruction"/> </relation>
</edge>
<edge attribute="yes">
<relation name="check_val"> <type name="ATOMIC_EXCH_BRANCH"/> <type name="V"/> </relation>
<relation name="exch_val"> <type name="ATOMIC_EXCH_BRANCH"/> <type name="V"/> </relation>
</edge>
<edge merge="no">
<relation name="branch_target"> <type name="ATOMIC_EXCH_BRANCH"/> <type name="Instruction"/> </relation>
</edge>
<edge visible="no">
<relation name="$ao"> <type name="A"/> <type name="A"/> </relation>
<relation name="$next"> <type name="A"/> <type name="A"/> </relation>
<relation name="$next_in_thd"> <type name="A"/> <type name="A"/> </relation>
<relation name="$to"> <type name="S"/> <type name="S"/> </relation>
<relation name="$to_run_a"> <type name="Thread"/> <type name="A"/> </relation>
<relation name="t_order"> <type name="Thread"/> <type name="Thread"/> </relation>
</edge>
<edge visible="no" attribute="yes">
<relation name="check_loc"> <type name="ATOMIC_EXCH_BRANCH"/> <type name="X"/> </relation>
<relation name="G_state"> <type name="S"/> <type name="G_memory"/> </relation>
<relation name="ins"> <type name="A"/> <type name="Instruction"/> </relation>
<relation name="mem"> <type name="G_memory"/> <type name="X"/> <type name="V"/> </relation>
<relation name="next_ins"> <type name="L_state"/> <type name="Instruction"/> </relation>
<relation name="T_state"> <type name="S"/> <type name="Thread"/> <type name="L_state"/> </relation>
<relation name="thd"> <type name="Instruction"/> <type name="Thread"/> </relation>
</edge>
<edge visible="no" constraint="no">
<relation name="pre"> <type name="A"/> <type name="S"/> </relation>
</edge>
</view>
</alloy>