diff --git a/alloy/tests/PC-bar-acq-rel-atom.test b/alloy/tests/PC-bar-acq-rel-atom.test
new file mode 100644
index 0000000..f305282
--- /dev/null
+++ b/alloy/tests/PC-bar-acq-rel-atom.test
@@ -0,0 +1,13 @@
+// Producer-Consumer pattern using named barriers. 
+// Atomic operations are non-private and thus the load and store are in locord. 
+// Barriers are acq_rel and thus they are in sw.
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.scopewg.sc0 x = 1
+cbar.acq.rel.scopewg.semsc0 0
+NEWTHREAD
+cbar.acq.rel.scopewg.semsc0 0
+st.atom.scopewg.sc0 x = 1
+NOSOLUTION consistent[X] && #dr=0
+NOSOLUTION #dr>0
\ No newline at end of file
diff --git a/alloy/tests/PC-bar-acq-rel-nonpriv.test b/alloy/tests/PC-bar-acq-rel-nonpriv.test
new file mode 100644
index 0000000..9de9764
--- /dev/null
+++ b/alloy/tests/PC-bar-acq-rel-nonpriv.test
@@ -0,0 +1,13 @@
+// Producer-Consumer pattern using named barriers. 
+// Load and store are non-private and thus in locord. 
+// Barriers are acq_rel and thus they are in sw.
+NEWWG
+NEWSG
+NEWTHREAD
+ld.nonpriv.sc0 x = 1
+cbar.acq.rel.scopewg.semsc0 0
+NEWTHREAD
+cbar.acq.rel.scopewg.semsc0 0
+st.nonpriv.sc0 x = 1
+NOSOLUTION consistent[X] && #dr=0
+NOSOLUTION #dr>0
\ No newline at end of file
diff --git a/alloy/tests/PC-bar-acq-rel-priv.test b/alloy/tests/PC-bar-acq-rel-priv.test
new file mode 100644
index 0000000..86dcbb0
--- /dev/null
+++ b/alloy/tests/PC-bar-acq-rel-priv.test
@@ -0,0 +1,13 @@
+// Producer-Consumer pattern using named barriers. 
+// Load and store are private and thus not in locord. 
+// Barriers are acq_rel and thus they are in sw.
+NEWWG
+NEWSG
+NEWTHREAD
+ld.sc0 x = 1
+cbar.acq.rel.scopewg.semsc0 0
+NEWTHREAD
+cbar.acq.rel.scopewg.semsc0 0
+st.sc0 x = 1
+SATISFIABLE consistent[X]
+SATISFIABLE #dr>0
\ No newline at end of file
diff --git a/alloy/tests/PC-bar-atom.test b/alloy/tests/PC-bar-atom.test
new file mode 100644
index 0000000..5d357cf
--- /dev/null
+++ b/alloy/tests/PC-bar-atom.test
@@ -0,0 +1,13 @@
+// Producer-Consumer pattern using named barriers. 
+// Atomic operations are non-private and thus the load and store are in locord. 
+// Barriers are not acq_rel and thus they are not in sw.
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.scopewg.sc0 x = 1
+cbar.scopewg 0
+NEWTHREAD
+cbar.scopewg 0
+st.atom.scopewg.sc0 x = 1
+SATISFIABLE consistent[X] && #dr=0
+NOSOLUTION #dr>0
diff --git a/alloy/tests/PC-bar-nonpriv.test b/alloy/tests/PC-bar-nonpriv.test
new file mode 100644
index 0000000..6b65818
--- /dev/null
+++ b/alloy/tests/PC-bar-nonpriv.test
@@ -0,0 +1,13 @@
+// Producer-Consumer pattern using named barriers. 
+// Load and store are non-private and thus in locord. 
+// Barriers are not acq_rel and thus they are not in sw.
+NEWWG
+NEWSG
+NEWTHREAD
+ld.nonpriv.sc0 x = 1
+cbar.scopewg 0
+NEWTHREAD
+cbar.scopewg 0
+st.nonpriv.sc0 x = 1
+SATISFIABLE consistent[X]
+SATISFIABLE #dr>0
\ No newline at end of file
diff --git a/alloy/tests/asmo-weak.test b/alloy/tests/asmo-weak.test
new file mode 100644
index 0000000..b59e267
--- /dev/null
+++ b/alloy/tests/asmo-weak.test
@@ -0,0 +1,21 @@
+// Test if thread 3 and thread 4 can read updates to x in conflicting order
+NEWWG
+NEWSG
+NEWTHREAD
+st.sc0 x = 1
+NEWWG
+NEWSG
+NEWTHREAD
+st.sc0 x = 2
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.scopedev.sc0 x = 1
+ld.atom.scopedev.sc0 x = 2
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.scopedev.sc0 x = 2
+ld.atom.scopedev.sc0 x = 1
+SATISFIABLE consistent[X] && #dr>0
+SATISFIABLE consistent[X]
\ No newline at end of file
diff --git a/alloy/tests/coww-rr.test b/alloy/tests/coww-rr.test
new file mode 100644
index 0000000..6700e65
--- /dev/null
+++ b/alloy/tests/coww-rr.test
@@ -0,0 +1,13 @@
+// Non-atomic memory operations may be observed by one thread in a different order than they were written by another thread
+NEWWG
+NEWSG
+NEWTHREAD
+st.sc0 x = 1
+st.sc0 x = 2
+NEWWG
+NEWSG
+NEWTHREAD
+ld.sc0 x = 2
+ld.sc0 x = 1
+SATISFIABLE consistent[X]
+NOSOLUTION consistent[X] && #dr=0
\ No newline at end of file
diff --git a/alloy/tests/mp-avvis.test b/alloy/tests/mp-avvis.test
new file mode 100644
index 0000000..aeb94e8
--- /dev/null
+++ b/alloy/tests/mp-avvis.test
@@ -0,0 +1,12 @@
+// Av/Vis + Rel/Acq forbids the behavior
+NEWWG
+NEWSG
+NEWTHREAD
+st.av.scopedev.sc0 x = 1
+st.atom.rel.scopewg.sc0.semsc0 y = 1
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopewg.sc0.semsc0 y = 1
+ld.vis.scopedev.sc0 x = 0
+NOSOLUTION consistent[X]
+NOSOLUTION consistent[X] && #dr=0
\ No newline at end of file
diff --git a/alloy/tests/mp-no-avvis.test b/alloy/tests/mp-no-avvis.test
new file mode 100644
index 0000000..b26c081
--- /dev/null
+++ b/alloy/tests/mp-no-avvis.test
@@ -0,0 +1,12 @@
+// Rel/Acq alone is not enough to forbid the behavior
+NEWWG
+NEWSG
+NEWTHREAD
+st.sc0 x = 1
+st.atom.rel.scopewg.sc0.semsc0 y = 1
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopewg.sc0.semsc0 y = 1
+ld.sc0 x = 0
+SATISFIABLE consistent[X]
+NOSOLUTION consistent[X] && #dr=0
\ No newline at end of file
diff --git a/alloy/tests/sb2dv.test b/alloy/tests/sb2dv.test
new file mode 100644
index 0000000..3f46e61
--- /dev/null
+++ b/alloy/tests/sb2dv.test
@@ -0,0 +1,13 @@
+// Adapted from Figure 5 of paper: Heterogeneous-race-free Memory Models
+NEWWG
+NEWSG
+NEWTHREAD
+st.atom.rel.scopewg.sc0.semsc0 x = 1
+ld.atom.acq.scopedev.sc0.semsc0 y = 0
+NEWWG
+NEWSG
+NEWTHREAD
+st.atom.rel.scopewg.sc0.semsc0 y = 1
+ld.atom.acq.scopedev.sc0.semsc0 x = 0
+SATISFIABLE consistent[X] && #dr>0
+NOSOLUTION consistent[X] && #dr=0
\ No newline at end of file
diff --git a/alloy/tests/sb2wg.test b/alloy/tests/sb2wg.test
new file mode 100644
index 0000000..d012425
--- /dev/null
+++ b/alloy/tests/sb2wg.test
@@ -0,0 +1,11 @@
+// Adapted from Figure 5 of paper: Heterogeneous-race-free Memory Models
+NEWWG
+NEWSG
+NEWTHREAD
+st.atom.rel.scopewg.sc0.semsc0 x = 1
+ld.atom.acq.scopedev.sc0.semsc0 y = 0
+NEWSG
+NEWTHREAD
+st.atom.rel.scopewg.sc0.semsc0 y = 1
+ld.atom.acq.scopedev.sc0.semsc0 x = 0
+SATISFIABLE consistent[X] && #dr=0
\ No newline at end of file