From 83e911a557fb4eea7da085cfb40872026091f7f0 Mon Sep 17 00:00:00 2001 From: Gonzalo Brito Gadeschi Date: Tue, 27 May 2025 14:17:59 +0200 Subject: [PATCH] Test impact of cpp2w --- tests/dat3m/auto/arfna.litmus.expected | 10 ++++------ tests/dat3m/auto/arfna2.litmus.expected | 10 ++++------ tests/dat3m/auto/b+acq+rel.litmus.expected | 9 ++++----- tests/dat3m/auto/b+acq+rlx.litmus.expected | 9 ++++----- tests/dat3m/auto/b+acq+sc.litmus.expected | 9 ++++----- tests/dat3m/auto/b+rlx+rel.litmus.expected | 9 ++++----- tests/dat3m/auto/b+rlx+rlx.litmus.expected | 9 ++++----- tests/dat3m/auto/b+rlx+sc.litmus.expected | 9 ++++----- tests/dat3m/auto/b+sc+rel.litmus.expected | 9 ++++----- tests/dat3m/auto/b+sc+rlx.litmus.expected | 9 ++++----- tests/dat3m/auto/b+sc+sc.litmus.expected | 9 ++++----- tests/dat3m/auto/b.litmus.expected | 9 ++++----- tests/dat3m/auto/c.litmus.expected | 10 ++++------ tests/dat3m/auto/c_p.litmus.expected | 10 ++++------ tests/dat3m/auto/c_p_reorder.litmus.expected | 10 ++++------ tests/dat3m/auto/c_pq.litmus.expected | 10 ++++------ tests/dat3m/auto/c_pq_reorder.litmus.expected | 10 ++++------ tests/dat3m/auto/c_q.litmus.expected | 10 ++++------ tests/dat3m/auto/c_q_reorder.litmus.expected | 10 ++++------ tests/dat3m/auto/c_reorder.litmus.expected | 10 ++++------ tests/dat3m/auto/cyc.litmus.expected | 9 ++++----- tests/dat3m/auto/cyc_na.litmus.expected | 10 ++++------ tests/dat3m/auto/fig1.litmus.expected | 4 ++-- tests/dat3m/auto/lb.litmus.expected | 9 ++++----- tests/dat3m/auto/linearisation.litmus.expected | 10 ++++------ .../dat3m/auto/linearisation2.litmus.expected | 9 ++++----- tests/dat3m/auto/roachmotel.litmus.expected | 10 ++++------ tests/dat3m/auto/roachmotel2.litmus.expected | 10 ++++------ tests/dat3m/auto/seq.litmus.expected | 10 ++++------ tests/dat3m/auto/seq2.litmus.expected | 9 ++++----- tests/dat3m/auto/strengthen.litmus.expected | 10 ++++------ tests/dat3m/auto/strengthen2.litmus.expected | 10 ++++------ .../IRIW-sc-sc-acq-sc-acq-sc.litmus.expected | 9 ++++----- .../manual/RWC-sc-acq-sc-sc-sc.litmus.expected | 9 ++++----- .../manual/cppmem_iriw_relacq.litmus.expected | 9 ++++----- tests/dat3m/manual/imm-E3.10.litmus.expected | 7 +++---- tests/dat3m/manual/imm-E3.3.litmus.expected | 9 ++++----- tests/dat3m/manual/imm-E3.6.litmus.expected | 9 ++++----- .../dat3m/manual/imm-E3.8-alt.litmus.expected | 9 ++++----- tests/dat3m/manual/imm-E3.9.litmus.expected | 7 +++---- tests/dat3m/manual/imm-R2-alt.litmus.expected | 9 ++++----- tests/dat3m/manual/imm-R2.litmus.expected | 9 ++++----- .../amp-lna-lna-sna-sna.racy.litmus.expected | 7 +++---- .../amp-lna-srel-lrlx-sna.racy.litmus.expected | 7 +++---- ...na-srel-srlx-lacq-sna.cpp11.litmus.expected | 7 +++---- ...el-srlx-lacq-sna.cpp17.racy.litmus.expected | 7 +++---- .../amp-lna-srlx-lacq-sna.racy.litmus.expected | 7 +++---- .../amp-lna-srlx-lrlx-sna.racy.litmus.expected | 7 +++---- .../amp-lrlx-srel-lrlx-srlx.litmus.expected | 9 ++++----- .../amp-lrlx-srlx-lacq-srlx.litmus.expected | 9 ++++----- .../amp-lrlx-srlx-lrlx-lrlx.litmus.expected | 9 ++++----- ...oRR-srlx-lacq-na.cpp11.racy.litmus.expected | 3 +-- ...oRR-srlx-lrlx-na.cpp11.racy.litmus.expected | 3 +-- ...rlx-srlx-lrlx-na.cpp11.racy.litmus.expected | 3 +-- ...frel-srlx-lacq-lna-lna.racy.litmus.expected | 3 +-- ...mp-srlx-srel-lrlx-lacq-lrlx.litmus.expected | 9 ++++----- .../mp/mp-srlx-srel-lrlx-lrlx.litmus.expected | 9 ++++----- .../mp/mp-srlx-srlx-lacq-lrlx.litmus.expected | 9 ++++----- .../mp/mp-srlx-srlx-lrlx-lrlx.litmus.expected | 9 ++++----- .../rs/mp-rs-add-est-atomic.litmus.expected | 9 ++++----- ...mp-rs-st-eadd-atomics.cpp11.litmus.expected | 10 ++++------ ...mp-rs-st-eadd-atomics.cpp17.litmus.expected | 8 +++----- .../rs/mp-rs-st-est-atomics.litmus.expected | 10 ++++------ tests/herdrc11/C13.litmus.expected | 9 ++++----- ...B+fetch.addrlxrlx-porlxrlxs.litmus.expected | 9 ++++----- ...lx+fetch.addrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...orlxrlx+posWrlxrlx-porlxrlx.litmus.expected | 10 ++++------ ...porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...lx+fetch.addrlxrlx-porlxrlx.litmus.expected | 10 ++++------ ...lx+fetch.addrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...lx+fetch.addrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...orlxrlx+posWrlxrlx-porlxrlx.litmus.expected | 10 ++++------ ...porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...orlxrlx+posWrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...W+fetch.addrlxrlx-porlxrlxs.litmus.expected | 9 ++++----- ...lx+fetch.addrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...orlxrlx+posWrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...addrlxrlx-porlxrlx+porlxrlx.litmus.expected | 9 ++++----- ...osWrlxrlx-porlxrlx+porlxrlx.litmus.expected | 9 ++++----- ...rmwrlxrlx-porlxrlx+porlxrlx.litmus.expected | 9 ++++----- ...addrlxrlx-porlxrlx+porlxrlx.litmus.expected | 9 ++++----- ...osWrlxrlx-porlxrlx+porlxrlx.litmus.expected | 9 ++++----- ...rmwrlxrlx-porlxrlx+porlxrlx.litmus.expected | 9 ++++----- ...lx+fetch.addrlxrlx-porlxrlx.litmus.expected | 9 ++++----- ...orlxrlx+posWrlxrlx-porlxrlx.litmus.expected | 10 ++++------ ...porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected | 9 ++++----- .../oota-3-2-proc-opt.litmus.expected | 7 +++---- tests/paul_oota/oota-3-2-proc.litmus.expected | 7 +++---- tests/paul_oota/oota-3proc.litmus.expected | 7 +++---- .../paul_oota/oota-causality-1.litmus.expected | 9 ++++----- .../oota-causality-10.litmus.expected | 9 ++++----- .../oota-causality-11.litmus.expected | 11 ++++------- .../oota-causality-13.litmus.expected | 9 ++++----- .../oota-causality-14.litmus.expected | 9 ++++----- .../oota-causality-15.litmus.expected | 9 ++++----- .../oota-causality-17.litmus.expected | 7 +++---- .../oota-causality-18.litmus.expected | 7 +++---- .../oota-causality-19.litmus.expected | 7 +++---- .../paul_oota/oota-causality-2.litmus.expected | 9 ++++----- .../oota-causality-20.litmus.expected | 7 +++---- .../paul_oota/oota-causality-3.litmus.expected | 9 ++++----- .../paul_oota/oota-causality-4.litmus.expected | 7 +++---- .../paul_oota/oota-causality-5.litmus.expected | 8 +++----- .../paul_oota/oota-causality-6.litmus.expected | 9 ++++----- .../paul_oota/oota-causality-7.litmus.expected | 10 ++++------ .../paul_oota/oota-causality-9.litmus.expected | 4 ++-- .../oota-causality-9a.litmus.expected | 4 ++-- tests/paul_oota/oota-ctrl.litmus.expected | 9 ++++----- tests/paul_oota/oota-dg-1.litmus.expected | 9 ++++----- .../oota-invent-int-load.litmus.expected | 9 ++++----- .../paul_oota/oota-two-source.litmus.expected | 18 +++--------------- .../simple-reordering.litmus.expected | 9 ++++----- tests/pldi17/iriw-acq-sc.litmus.expected | 9 ++++----- tests/pldi17/lb.litmus.expected | 7 +++---- tests/pldi17/sb+rfis.litmus.expected | 9 ++++----- tests/pldi17/wwmerge.litmus.expected | 11 ++++------- tests/pldi17/z6.u.litmus.expected | 9 ++++----- .../auto/a7_reorder+Cacq.litmus.expected | 4 ++-- .../auto/a7_reorder+Crel-acq.litmus.expected | 4 ++-- .../auto/a7_reorder+Crel.litmus.expected | 4 ++-- .../auto/a7_reorder+Crlx.litmus.expected | 4 ++-- .../popl15/auto/a7_reorder+Csc.litmus.expected | 4 ++-- .../auto/a7_reorder+Racq.litmus.expected | 4 ++-- .../popl15/auto/a7_reorder+Rna.litmus.expected | 4 ++-- .../auto/a7_reorder+Rrel.litmus.expected | 4 ++-- .../auto/a7_reorder+Rrlx.litmus.expected | 4 ++-- .../popl15/auto/a7_reorder+Rsc.litmus.expected | 4 ++-- tests/popl15/auto/b+acq+rel.litmus.expected | 9 ++++----- tests/popl15/auto/b+acq+rlx.litmus.expected | 9 ++++----- tests/popl15/auto/b+acq+sc.litmus.expected | 9 ++++----- tests/popl15/auto/b+rlx+rel.litmus.expected | 9 ++++----- tests/popl15/auto/b+rlx+rlx.litmus.expected | 9 ++++----- tests/popl15/auto/b+rlx+sc.litmus.expected | 9 ++++----- tests/popl15/auto/b+sc+rel.litmus.expected | 9 ++++----- tests/popl15/auto/b+sc+rlx.litmus.expected | 9 ++++----- tests/popl15/auto/b+sc+sc.litmus.expected | 9 ++++----- tests/popl15/manual/a7_reorder.litmus.expected | 4 ++-- tests/popl15/manual/arfna.litmus.expected | 10 ++++------ tests/popl15/manual/arfna2.litmus.expected | 10 ++++------ tests/popl15/manual/b.litmus.expected | 9 ++++----- tests/popl15/manual/c.litmus.expected | 10 ++++------ tests/popl15/manual/c_p.litmus.expected | 10 ++++------ .../popl15/manual/c_p_reorder.litmus.expected | 10 ++++------ tests/popl15/manual/c_pq.litmus.expected | 10 ++++------ .../popl15/manual/c_pq_reorder.litmus.expected | 10 ++++------ tests/popl15/manual/c_q.litmus.expected | 10 ++++------ .../popl15/manual/c_q_reorder.litmus.expected | 10 ++++------ tests/popl15/manual/c_reorder.litmus.expected | 10 ++++------ tests/popl15/manual/cyc.litmus.expected | 9 ++++----- tests/popl15/manual/cyc_na.litmus.expected | 10 ++++------ tests/popl15/manual/fig1.litmus.expected | 4 ++-- tests/popl15/manual/lb.litmus.expected | 9 ++++----- .../manual/linearisation.litmus.expected | 10 ++++------ .../manual/linearisation2.litmus.expected | 9 ++++----- tests/popl15/manual/roachmotel.litmus.expected | 10 ++++------ .../popl15/manual/roachmotel2.litmus.expected | 10 ++++------ tests/popl15/manual/seq.litmus.expected | 10 ++++------ tests/popl15/manual/seq2.litmus.expected | 9 ++++----- tests/popl15/manual/strengthen.litmus.expected | 10 ++++------ .../popl15/manual/strengthen2.litmus.expected | 10 ++++------ 162 files changed, 586 insertions(+), 791 deletions(-) diff --git a/tests/dat3m/auto/arfna.litmus.expected b/tests/dat3m/auto/arfna.litmus.expected index 4a4b75a8..710526a6 100644 --- a/tests/dat3m/auto/arfna.litmus.expected +++ b/tests/dat3m/auto/arfna.litmus.expected @@ -1,12 +1,10 @@ Test arfna Allowed -States 2 +States 1 [x]=0; [y]=0; -[x]=1; [y]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([x]=1 /\ [y]=1) -Observation arfna Sometimes 1 1 +Observation arfna Never 0 1 Hash=c69a80006463884aeaf6958f9e74807a diff --git a/tests/dat3m/auto/arfna2.litmus.expected b/tests/dat3m/auto/arfna2.litmus.expected index 5346b328..f392f3d2 100644 --- a/tests/dat3m/auto/arfna2.litmus.expected +++ b/tests/dat3m/auto/arfna2.litmus.expected @@ -1,12 +1,10 @@ Test arfna_transformed Allowed -States 2 +States 1 [x]=0; [y]=0; -[x]=1; [y]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([x]=1 /\ [y]=1) -Observation arfna_transformed Sometimes 1 1 +Observation arfna_transformed Never 0 1 Hash=fbb437dbcdc8a88611a71fe92622c1d5 diff --git a/tests/dat3m/auto/b+acq+rel.litmus.expected b/tests/dat3m/auto/b+acq+rel.litmus.expected index efb7c5a7..7610c0a2 100644 --- a/tests/dat3m/auto/b+acq+rel.litmus.expected +++ b/tests/dat3m/auto/b+acq+rel.litmus.expected @@ -1,13 +1,12 @@ Test b+acq+rel Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+acq+rel Sometimes 1 3 +Observation b+acq+rel Never 0 3 Hash=0f7142d4a35f9e4a34d811105d759b25 diff --git a/tests/dat3m/auto/b+acq+rlx.litmus.expected b/tests/dat3m/auto/b+acq+rlx.litmus.expected index 6fb51991..a26aa3f6 100644 --- a/tests/dat3m/auto/b+acq+rlx.litmus.expected +++ b/tests/dat3m/auto/b+acq+rlx.litmus.expected @@ -1,13 +1,12 @@ Test b+acq+rlx Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+acq+rlx Sometimes 1 3 +Observation b+acq+rlx Never 0 3 Hash=a6ddbce34f4ed83e7398a60863004d24 diff --git a/tests/dat3m/auto/b+acq+sc.litmus.expected b/tests/dat3m/auto/b+acq+sc.litmus.expected index 8a5bb5d7..2cb2e03a 100644 --- a/tests/dat3m/auto/b+acq+sc.litmus.expected +++ b/tests/dat3m/auto/b+acq+sc.litmus.expected @@ -1,13 +1,12 @@ Test b+acq+sc Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+acq+sc Sometimes 1 3 +Observation b+acq+sc Never 0 3 Hash=f4c9acce455da0095bd9a81f9398dda3 diff --git a/tests/dat3m/auto/b+rlx+rel.litmus.expected b/tests/dat3m/auto/b+rlx+rel.litmus.expected index 6babdf0b..c2cf93e9 100644 --- a/tests/dat3m/auto/b+rlx+rel.litmus.expected +++ b/tests/dat3m/auto/b+rlx+rel.litmus.expected @@ -1,13 +1,12 @@ Test b+rlx+rel Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+rlx+rel Sometimes 1 3 +Observation b+rlx+rel Never 0 3 Hash=f4364386d981d551de45022ce1bd6389 diff --git a/tests/dat3m/auto/b+rlx+rlx.litmus.expected b/tests/dat3m/auto/b+rlx+rlx.litmus.expected index ff5c790e..f35da7f4 100644 --- a/tests/dat3m/auto/b+rlx+rlx.litmus.expected +++ b/tests/dat3m/auto/b+rlx+rlx.litmus.expected @@ -1,13 +1,12 @@ Test b+rlx+rlx Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+rlx+rlx Sometimes 1 3 +Observation b+rlx+rlx Never 0 3 Hash=263307ea63cba772b35ffa9562467a92 diff --git a/tests/dat3m/auto/b+rlx+sc.litmus.expected b/tests/dat3m/auto/b+rlx+sc.litmus.expected index b736e58b..4685e70f 100644 --- a/tests/dat3m/auto/b+rlx+sc.litmus.expected +++ b/tests/dat3m/auto/b+rlx+sc.litmus.expected @@ -1,13 +1,12 @@ Test b+rlx+sc Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+rlx+sc Sometimes 1 3 +Observation b+rlx+sc Never 0 3 Hash=fd321ba779c3afaa5a5f39644ed84c62 diff --git a/tests/dat3m/auto/b+sc+rel.litmus.expected b/tests/dat3m/auto/b+sc+rel.litmus.expected index beca87ea..c843368d 100644 --- a/tests/dat3m/auto/b+sc+rel.litmus.expected +++ b/tests/dat3m/auto/b+sc+rel.litmus.expected @@ -1,13 +1,12 @@ Test b+sc+rel Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+sc+rel Sometimes 1 3 +Observation b+sc+rel Never 0 3 Hash=f88964bb60588f8339ee6ec8fc43c303 diff --git a/tests/dat3m/auto/b+sc+rlx.litmus.expected b/tests/dat3m/auto/b+sc+rlx.litmus.expected index abe5d880..810a6c81 100644 --- a/tests/dat3m/auto/b+sc+rlx.litmus.expected +++ b/tests/dat3m/auto/b+sc+rlx.litmus.expected @@ -1,13 +1,12 @@ Test b+sc+rlx Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+sc+rlx Sometimes 1 3 +Observation b+sc+rlx Never 0 3 Hash=307b4f4af7807a1e790f80e56e464e74 diff --git a/tests/dat3m/auto/b+sc+sc.litmus.expected b/tests/dat3m/auto/b+sc+sc.litmus.expected index f5cb8835..01f39492 100644 --- a/tests/dat3m/auto/b+sc+sc.litmus.expected +++ b/tests/dat3m/auto/b+sc+sc.litmus.expected @@ -1,13 +1,12 @@ Test b+sc+sc Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+sc+sc Sometimes 1 3 +Observation b+sc+sc Never 0 3 Hash=1b961ffe905698d0e34c2f492e2f63ed diff --git a/tests/dat3m/auto/b.litmus.expected b/tests/dat3m/auto/b.litmus.expected index 9844f293..8f9faf76 100644 --- a/tests/dat3m/auto/b.litmus.expected +++ b/tests/dat3m/auto/b.litmus.expected @@ -1,13 +1,12 @@ Test b Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b Sometimes 1 3 +Observation b Never 0 3 Hash=263307ea63cba772b35ffa9562467a92 diff --git a/tests/dat3m/auto/c.litmus.expected b/tests/dat3m/auto/c.litmus.expected index 66b46131..89e8b77e 100644 --- a/tests/dat3m/auto/c.litmus.expected +++ b/tests/dat3m/auto/c.litmus.expected @@ -1,12 +1,10 @@ Test c Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=1; [q]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c Sometimes 1 1 +Observation c Never 0 1 Hash=0ff4377802cdc23062bd3f44362c7fac diff --git a/tests/dat3m/auto/c_p.litmus.expected b/tests/dat3m/auto/c_p.litmus.expected index d8146dc6..667b7ff4 100644 --- a/tests/dat3m/auto/c_p.litmus.expected +++ b/tests/dat3m/auto/c_p.litmus.expected @@ -1,12 +1,10 @@ Test c_p Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=2; [q]=1; -Undef +No Witnesses -Positive: 0 Negative: 2 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_p Never 0 2 +Observation c_p Never 0 1 Hash=6b0ea2e4212c129f4929f58e34375feb diff --git a/tests/dat3m/auto/c_p_reorder.litmus.expected b/tests/dat3m/auto/c_p_reorder.litmus.expected index c5a1ef48..095b8e00 100644 --- a/tests/dat3m/auto/c_p_reorder.litmus.expected +++ b/tests/dat3m/auto/c_p_reorder.litmus.expected @@ -1,12 +1,10 @@ Test c_p_reorder Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=2; [q]=1; -Undef +No Witnesses -Positive: 0 Negative: 2 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_p_reorder Never 0 2 +Observation c_p_reorder Never 0 1 Hash=c67c1c81fada13c17a7e8ef2e1944b35 diff --git a/tests/dat3m/auto/c_pq.litmus.expected b/tests/dat3m/auto/c_pq.litmus.expected index 4dec50fc..9e2d88dd 100644 --- a/tests/dat3m/auto/c_pq.litmus.expected +++ b/tests/dat3m/auto/c_pq.litmus.expected @@ -1,12 +1,10 @@ Test c_pq Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=2; [q]=1; -Undef +No Witnesses -Positive: 0 Negative: 2 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_pq Never 0 2 +Observation c_pq Never 0 1 Hash=86e3436a379bae81d0e2f1d960cfd7cd diff --git a/tests/dat3m/auto/c_pq_reorder.litmus.expected b/tests/dat3m/auto/c_pq_reorder.litmus.expected index 1d1e6071..cdc442e8 100644 --- a/tests/dat3m/auto/c_pq_reorder.litmus.expected +++ b/tests/dat3m/auto/c_pq_reorder.litmus.expected @@ -1,12 +1,10 @@ Test c_pq_reorder Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=2; [q]=1; -Undef +No Witnesses -Positive: 0 Negative: 2 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_pq_reorder Never 0 2 +Observation c_pq_reorder Never 0 1 Hash=63b97be159ec65f84ff3c70d2e4e40e2 diff --git a/tests/dat3m/auto/c_q.litmus.expected b/tests/dat3m/auto/c_q.litmus.expected index 88cbf919..0faf9b90 100644 --- a/tests/dat3m/auto/c_q.litmus.expected +++ b/tests/dat3m/auto/c_q.litmus.expected @@ -1,12 +1,10 @@ Test c_q Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=1; [q]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_q Sometimes 1 1 +Observation c_q Never 0 1 Hash=bd2094625f1ee93e2689abfeb1c12d02 diff --git a/tests/dat3m/auto/c_q_reorder.litmus.expected b/tests/dat3m/auto/c_q_reorder.litmus.expected index acb4a111..f190782e 100644 --- a/tests/dat3m/auto/c_q_reorder.litmus.expected +++ b/tests/dat3m/auto/c_q_reorder.litmus.expected @@ -1,12 +1,10 @@ Test c_q_reorder Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=1; [q]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_q_reorder Sometimes 1 1 +Observation c_q_reorder Never 0 1 Hash=abda1ea76cc8deea5b2c8ca2ddb27a04 diff --git a/tests/dat3m/auto/c_reorder.litmus.expected b/tests/dat3m/auto/c_reorder.litmus.expected index 511606b4..400208ab 100644 --- a/tests/dat3m/auto/c_reorder.litmus.expected +++ b/tests/dat3m/auto/c_reorder.litmus.expected @@ -1,12 +1,10 @@ Test c_reorder Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=1; [q]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_reorder Sometimes 1 1 +Observation c_reorder Never 0 1 Hash=c6e61b3cc4e99d188768c792a17890f8 diff --git a/tests/dat3m/auto/cyc.litmus.expected b/tests/dat3m/auto/cyc.litmus.expected index 75c9506f..95b832aa 100644 --- a/tests/dat3m/auto/cyc.litmus.expected +++ b/tests/dat3m/auto/cyc.litmus.expected @@ -1,11 +1,10 @@ Test cyc Allowed -States 2 +States 1 0:r0=0; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 1 +Positive: 0 Negative: 1 Condition exists (0:r0=1 /\ 1:r1=1) -Observation cyc Sometimes 1 1 +Observation cyc Never 0 1 Hash=d16e1b2160f9a55f0bb557046b596103 diff --git a/tests/dat3m/auto/cyc_na.litmus.expected b/tests/dat3m/auto/cyc_na.litmus.expected index b7c3f5e5..633089cf 100644 --- a/tests/dat3m/auto/cyc_na.litmus.expected +++ b/tests/dat3m/auto/cyc_na.litmus.expected @@ -1,12 +1,10 @@ Test cyc_na Allowed -States 2 +States 1 0:r0=0; 1:r1=0; -0:r0=1; 1:r1=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists (0:r0=1 /\ 1:r1=1) -Observation cyc_na Sometimes 1 1 +Observation cyc_na Never 0 1 Hash=592962ab016c17f023c60a22e9365300 diff --git a/tests/dat3m/auto/fig1.litmus.expected b/tests/dat3m/auto/fig1.litmus.expected index 47a64c45..3975e1e3 100644 --- a/tests/dat3m/auto/fig1.litmus.expected +++ b/tests/dat3m/auto/fig1.litmus.expected @@ -3,8 +3,8 @@ States 1 [a]=1; [x]=1; [y]=1; Ok Witnesses -Positive: 4 Negative: 0 +Positive: 3 Negative: 0 Condition exists ([a]=1 /\ [x]=1 /\ [y]=1) -Observation fig1 Always 4 0 +Observation fig1 Always 3 0 Hash=1f61ce15fe6a88e6d904d414bf4b4d44 diff --git a/tests/dat3m/auto/lb.litmus.expected b/tests/dat3m/auto/lb.litmus.expected index 324d9fbc..0f0b2f98 100644 --- a/tests/dat3m/auto/lb.litmus.expected +++ b/tests/dat3m/auto/lb.litmus.expected @@ -1,13 +1,12 @@ Test lb Allowed -States 4 +States 3 0:r1=0; 1:r2=0; 0:r1=0; 1:r2=1; 0:r1=1; 1:r2=0; -0:r1=1; 1:r2=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r1=1 /\ 1:r2=1) -Observation lb Sometimes 1 3 +Observation lb Never 0 3 Hash=4cf90e2fdfda0174409e5fd545b6f19d diff --git a/tests/dat3m/auto/linearisation.litmus.expected b/tests/dat3m/auto/linearisation.litmus.expected index 2aff7ca5..2c2cc8ec 100644 --- a/tests/dat3m/auto/linearisation.litmus.expected +++ b/tests/dat3m/auto/linearisation.litmus.expected @@ -1,12 +1,10 @@ Test linearisation Allowed -States 2 +States 1 0:t=0; [w]=0; [x]=0; [y]=0; [z]=0; -0:t=2; [w]=1; [x]=1; [y]=1; [z]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists (0:t=2 /\ [w]=1 /\ [x]=1 /\ [y]=1 /\ [z]=1) -Observation linearisation Sometimes 1 1 +Observation linearisation Never 0 1 Hash=543d660acf26c106140b9ad29f6b4ccd diff --git a/tests/dat3m/auto/linearisation2.litmus.expected b/tests/dat3m/auto/linearisation2.litmus.expected index d4e36262..d793a177 100644 --- a/tests/dat3m/auto/linearisation2.litmus.expected +++ b/tests/dat3m/auto/linearisation2.litmus.expected @@ -1,11 +1,10 @@ Test linearisation2 Allowed -States 2 +States 1 0:t=0; [w]=0; [x]=0; [y]=0; [z]=0; -0:t=2; [w]=1; [x]=1; [y]=1; [z]=1; -Ok +No Witnesses -Positive: 1 Negative: 1 +Positive: 0 Negative: 1 Condition exists (0:t=2 /\ [w]=1 /\ [x]=1 /\ [y]=1 /\ [z]=1) -Observation linearisation2 Sometimes 1 1 +Observation linearisation2 Never 0 1 Hash=51e2c04a509c2f8d763f65266f14f3d5 diff --git a/tests/dat3m/auto/roachmotel.litmus.expected b/tests/dat3m/auto/roachmotel.litmus.expected index bf0b0372..2ca37fc8 100644 --- a/tests/dat3m/auto/roachmotel.litmus.expected +++ b/tests/dat3m/auto/roachmotel.litmus.expected @@ -1,12 +1,10 @@ Test roachmotel Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; [z]=1; -[a]=1; [x]=1; [y]=1; [z]=1; -Undef +No Witnesses -Positive: 2 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [z]=1 /\ [x]=1 /\ [y]=1) -Observation roachmotel Sometimes 2 1 +Observation roachmotel Never 0 1 Hash=89a4c1ec939981e0b843da41078b910c diff --git a/tests/dat3m/auto/roachmotel2.litmus.expected b/tests/dat3m/auto/roachmotel2.litmus.expected index 7cddcbf2..dd8fafd0 100644 --- a/tests/dat3m/auto/roachmotel2.litmus.expected +++ b/tests/dat3m/auto/roachmotel2.litmus.expected @@ -1,12 +1,10 @@ Test roachmotel2 Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; [z]=1; -[a]=1; [x]=1; [y]=1; [z]=1; -Undef +No Witnesses -Positive: 2 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [z]=1 /\ [x]=1 /\ [y]=1) -Observation roachmotel2 Sometimes 2 1 +Observation roachmotel2 Never 0 1 Hash=6d27da9e3c6dcde00c4db99dd97e6e43 diff --git a/tests/dat3m/auto/seq.litmus.expected b/tests/dat3m/auto/seq.litmus.expected index bd2fa071..4657ad50 100644 --- a/tests/dat3m/auto/seq.litmus.expected +++ b/tests/dat3m/auto/seq.litmus.expected @@ -1,12 +1,10 @@ Test seq Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; -[a]=1; [x]=1; [y]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [x]=1 /\ [y]=1) -Observation seq Sometimes 1 1 +Observation seq Never 0 1 Hash=0559dd8eb63cce8637b7d0e9945d646d diff --git a/tests/dat3m/auto/seq2.litmus.expected b/tests/dat3m/auto/seq2.litmus.expected index 329b8452..34cb0535 100644 --- a/tests/dat3m/auto/seq2.litmus.expected +++ b/tests/dat3m/auto/seq2.litmus.expected @@ -1,11 +1,10 @@ Test seq2 Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; -[a]=1; [x]=1; [y]=1; -Ok +No Witnesses -Positive: 1 Negative: 1 +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [x]=1 /\ [y]=1) -Observation seq2 Sometimes 1 1 +Observation seq2 Never 0 1 Hash=e37262f71f5106920e496da6fd1dee2a diff --git a/tests/dat3m/auto/strengthen.litmus.expected b/tests/dat3m/auto/strengthen.litmus.expected index 00df6915..5ad598ac 100644 --- a/tests/dat3m/auto/strengthen.litmus.expected +++ b/tests/dat3m/auto/strengthen.litmus.expected @@ -1,12 +1,10 @@ Test strengthen Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; [z]=1; -[a]=1; [x]=1; [y]=1; [z]=1; -Undef +No Witnesses -Positive: 2 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [z]=1 /\ [x]=1 /\ [y]=1) -Observation strengthen Sometimes 2 1 +Observation strengthen Never 0 1 Hash=936f17c1670a38b94c845fd21682daa3 diff --git a/tests/dat3m/auto/strengthen2.litmus.expected b/tests/dat3m/auto/strengthen2.litmus.expected index 96592fe9..60cb71f4 100644 --- a/tests/dat3m/auto/strengthen2.litmus.expected +++ b/tests/dat3m/auto/strengthen2.litmus.expected @@ -1,12 +1,10 @@ Test strengthen2 Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; [z]=1; -[a]=1; [x]=1; [y]=1; [z]=1; -Undef +No Witnesses -Positive: 2 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [z]=1 /\ [x]=1 /\ [y]=1) -Observation strengthen2 Sometimes 2 1 +Observation strengthen2 Never 0 1 Hash=6d27da9e3c6dcde00c4db99dd97e6e43 diff --git a/tests/dat3m/manual/IRIW-sc-sc-acq-sc-acq-sc.litmus.expected b/tests/dat3m/manual/IRIW-sc-sc-acq-sc-acq-sc.litmus.expected index 0e426046..c8957fbd 100644 --- a/tests/dat3m/manual/IRIW-sc-sc-acq-sc-acq-sc.litmus.expected +++ b/tests/dat3m/manual/IRIW-sc-sc-acq-sc-acq-sc.litmus.expected @@ -1,5 +1,5 @@ Test IRIW-sc-sc-acq-sc-acq-sc Allowed -States 16 +States 15 2:r1=0; 2:r2=0; 3:r3=0; 3:r4=0; 2:r1=0; 2:r2=0; 3:r3=0; 3:r4=1; 2:r1=0; 2:r2=0; 3:r3=1; 3:r4=0; @@ -10,16 +10,15 @@ States 16 2:r1=0; 2:r2=1; 3:r3=1; 3:r4=1; 2:r1=1; 2:r2=0; 3:r3=0; 3:r4=0; 2:r1=1; 2:r2=0; 3:r3=0; 3:r4=1; -2:r1=1; 2:r2=0; 3:r3=1; 3:r4=0; 2:r1=1; 2:r2=0; 3:r3=1; 3:r4=1; 2:r1=1; 2:r2=1; 3:r3=0; 3:r4=0; 2:r1=1; 2:r2=1; 3:r3=0; 3:r4=1; 2:r1=1; 2:r2=1; 3:r3=1; 3:r4=0; 2:r1=1; 2:r2=1; 3:r3=1; 3:r4=1; -Ok +No Witnesses -Positive: 1 Negative: 15 +Positive: 0 Negative: 15 Condition exists (2:r1=1 /\ 2:r2=0 /\ 3:r3=1 /\ 3:r4=0) -Observation IRIW-sc-sc-acq-sc-acq-sc Sometimes 1 15 +Observation IRIW-sc-sc-acq-sc-acq-sc Never 0 15 Hash=7e79dc44fc68f3a00e9daea47435e3bc diff --git a/tests/dat3m/manual/RWC-sc-acq-sc-sc-sc.litmus.expected b/tests/dat3m/manual/RWC-sc-acq-sc-sc-sc.litmus.expected index 1ea2415a..dba9fb1e 100644 --- a/tests/dat3m/manual/RWC-sc-acq-sc-sc-sc.litmus.expected +++ b/tests/dat3m/manual/RWC-sc-acq-sc-sc-sc.litmus.expected @@ -1,17 +1,16 @@ Test RWC-sc-acq-sc-sc-sc Allowed -States 8 +States 7 1:r1=0; 1:r2=0; 2:r3=0; 1:r1=0; 1:r2=0; 2:r3=1; 1:r1=0; 1:r2=1; 2:r3=0; 1:r1=0; 1:r2=1; 2:r3=1; -1:r1=1; 1:r2=0; 2:r3=0; 1:r1=1; 1:r2=0; 2:r3=1; 1:r1=1; 1:r2=1; 2:r3=0; 1:r1=1; 1:r2=1; 2:r3=1; -Ok +No Witnesses -Positive: 1 Negative: 7 +Positive: 0 Negative: 7 Condition exists (1:r1=1 /\ 1:r2=0 /\ 2:r3=0) -Observation RWC-sc-acq-sc-sc-sc Sometimes 1 7 +Observation RWC-sc-acq-sc-sc-sc Never 0 7 Hash=c0b295c0c45ee2e0c26a42986307cc8a diff --git a/tests/dat3m/manual/cppmem_iriw_relacq.litmus.expected b/tests/dat3m/manual/cppmem_iriw_relacq.litmus.expected index 69158187..7f2149ce 100644 --- a/tests/dat3m/manual/cppmem_iriw_relacq.litmus.expected +++ b/tests/dat3m/manual/cppmem_iriw_relacq.litmus.expected @@ -1,5 +1,5 @@ Test cppmem_iriw_relacq Allowed -States 16 +States 15 2:r1=0; 2:r2=0; 3:r3=0; 3:r4=0; 2:r1=0; 2:r2=0; 3:r3=0; 3:r4=1; 2:r1=0; 2:r2=0; 3:r3=1; 3:r4=0; @@ -10,16 +10,15 @@ States 16 2:r1=0; 2:r2=1; 3:r3=1; 3:r4=1; 2:r1=1; 2:r2=0; 3:r3=0; 3:r4=0; 2:r1=1; 2:r2=0; 3:r3=0; 3:r4=1; -2:r1=1; 2:r2=0; 3:r3=1; 3:r4=0; 2:r1=1; 2:r2=0; 3:r3=1; 3:r4=1; 2:r1=1; 2:r2=1; 3:r3=0; 3:r4=0; 2:r1=1; 2:r2=1; 3:r3=0; 3:r4=1; 2:r1=1; 2:r2=1; 3:r3=1; 3:r4=0; 2:r1=1; 2:r2=1; 3:r3=1; 3:r4=1; -Ok +No Witnesses -Positive: 1 Negative: 15 +Positive: 0 Negative: 15 Condition exists (2:r1=1 /\ 2:r2=0 /\ 3:r3=1 /\ 3:r4=0) -Observation cppmem_iriw_relacq Sometimes 1 15 +Observation cppmem_iriw_relacq Never 0 15 Hash=ea7782bc9661e6b768418d27aa0c6ce1 diff --git a/tests/dat3m/manual/imm-E3.10.litmus.expected b/tests/dat3m/manual/imm-E3.10.litmus.expected index 0c3aeb88..3d6ca9f2 100644 --- a/tests/dat3m/manual/imm-E3.10.litmus.expected +++ b/tests/dat3m/manual/imm-E3.10.litmus.expected @@ -1,12 +1,11 @@ Test imm-E3.10 Allowed -States 3 +States 2 0:r0=0; 1:r0=0; 1:r1=0; 0:r0=1; 1:r0=0; 1:r1=0; -0:r0=1; 1:r0=1; 1:r1=0; No Witnesses -Positive: 0 Negative: 4 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r0=1 /\ 1:r1=1) -Observation imm-E3.10 Never 0 4 +Observation imm-E3.10 Never 0 3 Hash=b3d5989372c098c9386d365ad7fd8046 diff --git a/tests/dat3m/manual/imm-E3.3.litmus.expected b/tests/dat3m/manual/imm-E3.3.litmus.expected index 5a64b4bb..66d75b9a 100644 --- a/tests/dat3m/manual/imm-E3.3.litmus.expected +++ b/tests/dat3m/manual/imm-E3.3.litmus.expected @@ -1,13 +1,12 @@ Test imm-E3.3 Allowed -States 4 +States 3 0:r0=0; 1:r0=0; 0:r0=0; 1:r0=1; 0:r0=1; 1:r0=0; -0:r0=1; 1:r0=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r0=1) -Observation imm-E3.3 Sometimes 1 3 +Observation imm-E3.3 Never 0 3 Hash=6b7647248ac98f6bcb2e873ac120954f diff --git a/tests/dat3m/manual/imm-E3.6.litmus.expected b/tests/dat3m/manual/imm-E3.6.litmus.expected index afef1294..0fa797d4 100644 --- a/tests/dat3m/manual/imm-E3.6.litmus.expected +++ b/tests/dat3m/manual/imm-E3.6.litmus.expected @@ -1,12 +1,11 @@ Test imm-E3.6 Allowed -States 3 +States 2 0:r0=0; 0:r1=1; 1:r0=0; 0:r0=0; 0:r1=1; 1:r0=1; -0:r0=1; 0:r1=1; 1:r0=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 0:r1=1 /\ 1:r0=1) -Observation imm-E3.6 Sometimes 1 3 +Observation imm-E3.6 Never 0 3 Hash=1489b81baf8f31ab9771ffd568a211a6 diff --git a/tests/dat3m/manual/imm-E3.8-alt.litmus.expected b/tests/dat3m/manual/imm-E3.8-alt.litmus.expected index c8fec067..3f7b41c1 100644 --- a/tests/dat3m/manual/imm-E3.8-alt.litmus.expected +++ b/tests/dat3m/manual/imm-E3.8-alt.litmus.expected @@ -1,5 +1,5 @@ Test imm-E3.8 Allowed -States 16 +States 15 0:r0=0; 0:r1=0; 3:r0=0; 3:r1=0; 0:r0=0; 0:r1=0; 3:r0=0; 3:r1=1; 0:r0=0; 0:r1=0; 3:r0=1; 3:r1=0; @@ -10,16 +10,15 @@ States 16 0:r0=0; 0:r1=1; 3:r0=1; 3:r1=1; 0:r0=1; 0:r1=0; 3:r0=0; 3:r1=0; 0:r0=1; 0:r1=0; 3:r0=0; 3:r1=1; -0:r0=1; 0:r1=0; 3:r0=1; 3:r1=0; 0:r0=1; 0:r1=0; 3:r0=1; 3:r1=1; 0:r0=1; 0:r1=1; 3:r0=0; 3:r1=0; 0:r0=1; 0:r1=1; 3:r0=0; 3:r1=1; 0:r0=1; 0:r1=1; 3:r0=1; 3:r1=0; 0:r0=1; 0:r1=1; 3:r0=1; 3:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 15 +Positive: 0 Negative: 15 Condition exists (0:r0=1 /\ 0:r1=0 /\ 3:r0=1 /\ 3:r1=0) -Observation imm-E3.8 Sometimes 1 15 +Observation imm-E3.8 Never 0 15 Hash=e45f4ff3f976b46709142875a8084e44 diff --git a/tests/dat3m/manual/imm-E3.9.litmus.expected b/tests/dat3m/manual/imm-E3.9.litmus.expected index 9d36c5bf..151e18a0 100644 --- a/tests/dat3m/manual/imm-E3.9.litmus.expected +++ b/tests/dat3m/manual/imm-E3.9.litmus.expected @@ -1,15 +1,14 @@ Test imm-E3.9 Allowed -States 6 +States 5 0:r0=0; 0:r1=0; 2:r0=0; 0:r0=0; 0:r1=0; 2:r0=1; 0:r0=0; 0:r1=1; 2:r0=0; 0:r0=0; 0:r1=1; 2:r0=1; -0:r0=1; 0:r1=0; 2:r0=1; 0:r0=1; 0:r1=1; 2:r0=1; No Witnesses -Positive: 0 Negative: 6 +Positive: 0 Negative: 5 Condition exists (0:r0=1 /\ 0:r1=0 /\ 2:r0=10) -Observation imm-E3.9 Never 0 6 +Observation imm-E3.9 Never 0 5 Hash=cd46d948530c7e5b60a4863eea633a6e diff --git a/tests/dat3m/manual/imm-R2-alt.litmus.expected b/tests/dat3m/manual/imm-R2-alt.litmus.expected index d74c834a..c718b486 100644 --- a/tests/dat3m/manual/imm-R2-alt.litmus.expected +++ b/tests/dat3m/manual/imm-R2-alt.litmus.expected @@ -1,5 +1,5 @@ Test imm-R2 Allowed -States 12 +States 11 1:r0=0; 2:r0=0; 2:r1=0; 1:r0=0; 2:r0=0; 2:r1=1; 1:r0=0; 2:r0=1; 2:r1=0; @@ -10,12 +10,11 @@ States 12 1:r0=1; 2:r0=0; 2:r1=1; 1:r0=1; 2:r0=1; 2:r1=1; 1:r0=1; 2:r0=2; 2:r1=1; -1:r0=1; 2:r0=3; 2:r1=0; 1:r0=1; 2:r0=3; 2:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 19 +Positive: 0 Negative: 18 Condition exists (1:r0=1 /\ 2:r0=3 /\ 2:r1=0) -Observation imm-R2 Sometimes 1 19 +Observation imm-R2 Never 0 18 Hash=b8de6be26d0f5d1448eabb9da8eab3e7 diff --git a/tests/dat3m/manual/imm-R2.litmus.expected b/tests/dat3m/manual/imm-R2.litmus.expected index ae357443..f78e844c 100644 --- a/tests/dat3m/manual/imm-R2.litmus.expected +++ b/tests/dat3m/manual/imm-R2.litmus.expected @@ -1,5 +1,5 @@ Test imm-R2 Allowed -States 12 +States 11 1:r0=0; 2:r0=0; 2:r1=0; 1:r0=0; 2:r0=0; 2:r1=1; 1:r0=0; 2:r0=1; 2:r1=0; @@ -10,12 +10,11 @@ States 12 1:r0=1; 2:r0=0; 2:r1=1; 1:r0=1; 2:r0=1; 2:r1=1; 1:r0=1; 2:r0=2; 2:r1=1; -1:r0=1; 2:r0=3; 2:r1=0; 1:r0=1; 2:r0=3; 2:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 19 +Positive: 0 Negative: 18 Condition exists (1:r0=1 /\ 2:r0=3 /\ 2:r1=0) -Observation imm-R2 Sometimes 1 19 +Observation imm-R2 Never 0 18 Hash=c6192045f2875fbebecbaab8cc3b41e8 diff --git a/tests/gonzalo/amp/amp-lna-lna-sna-sna.racy.litmus.expected b/tests/gonzalo/amp/amp-lna-lna-sna-sna.racy.litmus.expected index 8ef8b68c..d667a5eb 100644 --- a/tests/gonzalo/amp/amp-lna-lna-sna-sna.racy.litmus.expected +++ b/tests/gonzalo/amp/amp-lna-lna-sna-sna.racy.litmus.expected @@ -1,12 +1,11 @@ Test amp-lna-lna-sna-sna-racy Allowed -States 2 +States 1 0:b=0; -0:b=1; Undef Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Flag *undef* Condition exists (0:b=1) -Observation amp-lna-lna-sna-sna-racy Sometimes 1 2 +Observation amp-lna-lna-sna-sna-racy Never 0 2 Hash=55daeeb489d5ca8db572521189892efe diff --git a/tests/gonzalo/amp/amp-lna-srel-lrlx-sna.racy.litmus.expected b/tests/gonzalo/amp/amp-lna-srel-lrlx-sna.racy.litmus.expected index ced317cd..c54cf1a3 100644 --- a/tests/gonzalo/amp/amp-lna-srel-lrlx-sna.racy.litmus.expected +++ b/tests/gonzalo/amp/amp-lna-srel-lrlx-sna.racy.litmus.expected @@ -1,12 +1,11 @@ Test amp-lna-srel-lrx-sna-racy Allowed -States 2 +States 1 0:b=0; -0:b=1; Undef Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Flag *undef* Condition exists (0:b=1) -Observation amp-lna-srel-lrx-sna-racy Sometimes 1 2 +Observation amp-lna-srel-lrx-sna-racy Never 0 2 Hash=4155374d6754d0345b1c8b2ba6d2cc57 diff --git a/tests/gonzalo/amp/amp-lna-srel-srlx-lacq-sna.cpp11.litmus.expected b/tests/gonzalo/amp/amp-lna-srel-srlx-lacq-sna.cpp11.litmus.expected index df3575e4..82c891e9 100644 --- a/tests/gonzalo/amp/amp-lna-srel-srlx-lacq-sna.cpp11.litmus.expected +++ b/tests/gonzalo/amp/amp-lna-srel-srlx-lacq-sna.cpp11.litmus.expected @@ -1,12 +1,11 @@ Test amp-lna-srel-srlx-lacq-sna-cpp11 Forbidden -States 2 +States 1 0:b=0; -0:b=1; Undef Witnesses -Positive: 3 Negative: 1 +Positive: 3 Negative: 0 Flag *undef* Condition ~exists (0:b=1) -Observation amp-lna-srel-srlx-lacq-sna-cpp11 Sometimes 1 3 +Observation amp-lna-srel-srlx-lacq-sna-cpp11 Never 0 3 Hash=78c514ef749aac258a20c6b6de292c3b diff --git a/tests/gonzalo/amp/amp-lna-srel-srlx-lacq-sna.cpp17.racy.litmus.expected b/tests/gonzalo/amp/amp-lna-srel-srlx-lacq-sna.cpp17.racy.litmus.expected index 3fe628cb..87ec5a3e 100644 --- a/tests/gonzalo/amp/amp-lna-srel-srlx-lacq-sna.cpp17.racy.litmus.expected +++ b/tests/gonzalo/amp/amp-lna-srel-srlx-lacq-sna.cpp17.racy.litmus.expected @@ -1,12 +1,11 @@ Test amp-lna-srel-srlx-lacq-sna-cpp17-racy Allowed -States 2 +States 1 0:b=0; -0:b=1; Undef Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Flag *undef* Condition exists (0:b=1) -Observation amp-lna-srel-srlx-lacq-sna-cpp17-racy Sometimes 1 3 +Observation amp-lna-srel-srlx-lacq-sna-cpp17-racy Never 0 3 Hash=78c514ef749aac258a20c6b6de292c3b diff --git a/tests/gonzalo/amp/amp-lna-srlx-lacq-sna.racy.litmus.expected b/tests/gonzalo/amp/amp-lna-srlx-lacq-sna.racy.litmus.expected index 938b0ed1..b1a7a237 100644 --- a/tests/gonzalo/amp/amp-lna-srlx-lacq-sna.racy.litmus.expected +++ b/tests/gonzalo/amp/amp-lna-srlx-lacq-sna.racy.litmus.expected @@ -1,12 +1,11 @@ Test amp-lna-srlx-lacq-sna-racy Allowed -States 2 +States 1 0:b=0; -0:b=1; Undef Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Flag *undef* Condition exists (0:b=1) -Observation amp-lna-srlx-lacq-sna-racy Sometimes 1 2 +Observation amp-lna-srlx-lacq-sna-racy Never 0 2 Hash=eb3092f507698e3d519fe637991156f8 diff --git a/tests/gonzalo/amp/amp-lna-srlx-lrlx-sna.racy.litmus.expected b/tests/gonzalo/amp/amp-lna-srlx-lrlx-sna.racy.litmus.expected index d0c53887..afbdf779 100644 --- a/tests/gonzalo/amp/amp-lna-srlx-lrlx-sna.racy.litmus.expected +++ b/tests/gonzalo/amp/amp-lna-srlx-lrlx-sna.racy.litmus.expected @@ -1,12 +1,11 @@ Test amp-lna-srlx-lrlx-sna-racy Allowed -States 2 +States 1 0:b=0; -0:b=1; Undef Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Flag *undef* Condition exists (0:b=1) -Observation amp-lna-srlx-lrlx-sna-racy Sometimes 1 2 +Observation amp-lna-srlx-lrlx-sna-racy Never 0 2 Hash=93816ed123d14e5c2ec4c09da5ea61c8 diff --git a/tests/gonzalo/amp/amp-lrlx-srel-lrlx-srlx.litmus.expected b/tests/gonzalo/amp/amp-lrlx-srel-lrlx-srlx.litmus.expected index 72b2d1d1..ef781732 100644 --- a/tests/gonzalo/amp/amp-lrlx-srel-lrlx-srlx.litmus.expected +++ b/tests/gonzalo/amp/amp-lrlx-srel-lrlx-srlx.litmus.expected @@ -1,11 +1,10 @@ Test amp-lrlx-srel-lrlx-srlx Allowed -States 2 +States 1 0:b=0; -0:b=1; -Ok +No Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Condition exists (0:b=1) -Observation amp-lrlx-srel-lrlx-srlx Sometimes 1 2 +Observation amp-lrlx-srel-lrlx-srlx Never 0 2 Hash=5153bd136cbf9ff87707b18ca97354c7 diff --git a/tests/gonzalo/amp/amp-lrlx-srlx-lacq-srlx.litmus.expected b/tests/gonzalo/amp/amp-lrlx-srlx-lacq-srlx.litmus.expected index e657e22f..a2c36b3f 100644 --- a/tests/gonzalo/amp/amp-lrlx-srlx-lacq-srlx.litmus.expected +++ b/tests/gonzalo/amp/amp-lrlx-srlx-lacq-srlx.litmus.expected @@ -1,11 +1,10 @@ Test amp-lrlx-srlx-lacq-srlx Allowed -States 2 +States 1 0:b=0; -0:b=1; -Ok +No Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Condition exists (0:b=1) -Observation amp-lrlx-srlx-lacq-srlx Sometimes 1 2 +Observation amp-lrlx-srlx-lacq-srlx Never 0 2 Hash=38635d3d7e6361bb816facfb30d1b0f0 diff --git a/tests/gonzalo/amp/amp-lrlx-srlx-lrlx-lrlx.litmus.expected b/tests/gonzalo/amp/amp-lrlx-srlx-lrlx-lrlx.litmus.expected index b1f1b9fd..4b6d72ee 100644 --- a/tests/gonzalo/amp/amp-lrlx-srlx-lrlx-lrlx.litmus.expected +++ b/tests/gonzalo/amp/amp-lrlx-srlx-lrlx-lrlx.litmus.expected @@ -1,11 +1,10 @@ Test amp-lrlx-srlx-lrlx-srlx Allowed -States 2 +States 1 0:b=0; -0:b=1; -Ok +No Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Condition exists (0:b=1) -Observation amp-lrlx-srlx-lrlx-srlx Sometimes 1 2 +Observation amp-lrlx-srlx-lrlx-srlx Never 0 2 Hash=c5c22f6a48ddc56d95b295071b73fcec diff --git a/tests/gonzalo/coRR/coRR-srlx-lacq-na.cpp11.racy.litmus.expected b/tests/gonzalo/coRR/coRR-srlx-lacq-na.cpp11.racy.litmus.expected index 06595ced..ec3c5f9f 100644 --- a/tests/gonzalo/coRR/coRR-srlx-lacq-na.cpp11.racy.litmus.expected +++ b/tests/gonzalo/coRR/coRR-srlx-lacq-na.cpp11.racy.litmus.expected @@ -2,10 +2,9 @@ Test coRR-srlx-lacq-na-cpp11-racy Allowed States 2 1:a=0; 1:b=0; 1:a=1; 1:b=1; -Undef +No Witnesses Positive: 0 Negative: 2 -Flag *undef* Condition exists (1:a=1 /\ 1:b=0) Observation coRR-srlx-lacq-na-cpp11-racy Never 0 2 Hash=c72e2c53e2ea649a92d87f6613d9bebf diff --git a/tests/gonzalo/coRR/coRR-srlx-lrlx-na.cpp11.racy.litmus.expected b/tests/gonzalo/coRR/coRR-srlx-lrlx-na.cpp11.racy.litmus.expected index 69c7b695..0448d370 100644 --- a/tests/gonzalo/coRR/coRR-srlx-lrlx-na.cpp11.racy.litmus.expected +++ b/tests/gonzalo/coRR/coRR-srlx-lrlx-na.cpp11.racy.litmus.expected @@ -2,10 +2,9 @@ Test coRR-srlx-lrlx-na Allowed States 2 1:a=0; 1:b=0; 1:a=1; 1:b=1; -Undef +No Witnesses Positive: 0 Negative: 2 -Flag *undef* Condition exists (1:a=1 /\ 1:b=0) Observation coRR-srlx-lrlx-na Never 0 2 Hash=68078820c90f7b739c3aacdc2878a4ec diff --git a/tests/gonzalo/lmp/lmp-srlx-srlx-lrlx-na.cpp11.racy.litmus.expected b/tests/gonzalo/lmp/lmp-srlx-srlx-lrlx-na.cpp11.racy.litmus.expected index cffec0f5..eb217856 100644 --- a/tests/gonzalo/lmp/lmp-srlx-srlx-lrlx-na.cpp11.racy.litmus.expected +++ b/tests/gonzalo/lmp/lmp-srlx-srlx-lrlx-na.cpp11.racy.litmus.expected @@ -3,10 +3,9 @@ States 3 1:a=0; 1:b=0; 1:a=1; 1:b=0; 1:a=2; 1:b=2; -Undef +Ok Witnesses Positive: 3 Negative: 0 -Flag *undef* Condition ~exists (1:a=2 /\ not (1:b=2)) Observation lmp-srlx-srlx-lrx-na Never 0 3 Hash=b0128071add54a2cfb1a12a444be40a9 diff --git a/tests/gonzalo/mp/mp-sna-frel-srlx-lacq-lna-lna.racy.litmus.expected b/tests/gonzalo/mp/mp-sna-frel-srlx-lacq-lna-lna.racy.litmus.expected index ff661d7e..5fd61487 100644 --- a/tests/gonzalo/mp/mp-sna-frel-srlx-lacq-lna-lna.racy.litmus.expected +++ b/tests/gonzalo/mp/mp-sna-frel-srlx-lacq-lna-lna.racy.litmus.expected @@ -2,10 +2,9 @@ Test mp-sna-frel-srlx-lacq-lna-lna-racy Allowed States 2 1:a=0; 1:b=0; 1:c=0; 1:a=1; 1:b=1; 1:c=1; -Undef +No Witnesses Positive: 0 Negative: 2 -Flag *undef* Condition exists (1:a=1 /\ 1:b=0 /\ not (1:c=1)) Observation mp-sna-frel-srlx-lacq-lna-lna-racy Never 0 2 Hash=7dcec2340fda9d72eca193bc94e25290 diff --git a/tests/gonzalo/mp/mp-srlx-srel-lrlx-lacq-lrlx.litmus.expected b/tests/gonzalo/mp/mp-srlx-srel-lrlx-lacq-lrlx.litmus.expected index cf79d0db..063cf579 100644 --- a/tests/gonzalo/mp/mp-srlx-srel-lrlx-lacq-lrlx.litmus.expected +++ b/tests/gonzalo/mp/mp-srlx-srel-lrlx-lacq-lrlx.litmus.expected @@ -1,17 +1,16 @@ Test mp-srlx-srel-lrlx-lacq-lrlx Allowed -States 8 +States 7 1:a=0; 1:b=0; 1:c=0; 1:a=0; 1:b=0; 1:c=1; 1:a=0; 1:b=0; 1:c=2; -1:a=1; 1:b=0; 1:c=2; 1:a=1; 1:b=1; 1:c=1; 1:a=1; 1:b=1; 1:c=2; 1:a=2; 1:b=0; 1:c=1; 1:a=2; 1:b=0; 1:c=2; -Ok +No Witnesses -Positive: 1 Negative: 12 +Positive: 0 Negative: 12 Condition exists (1:a=1 /\ 1:b=0 /\ not (1:c=1)) -Observation mp-srlx-srel-lrlx-lacq-lrlx Sometimes 1 12 +Observation mp-srlx-srel-lrlx-lacq-lrlx Never 0 12 Hash=756d1bff5ee22b5dcf2b7129a43fb6a4 diff --git a/tests/gonzalo/mp/mp-srlx-srel-lrlx-lrlx.litmus.expected b/tests/gonzalo/mp/mp-srlx-srel-lrlx-lrlx.litmus.expected index 23304e46..933d1241 100644 --- a/tests/gonzalo/mp/mp-srlx-srel-lrlx-lrlx.litmus.expected +++ b/tests/gonzalo/mp/mp-srlx-srel-lrlx-lrlx.litmus.expected @@ -1,12 +1,11 @@ Test mp-srlx-srel-lrlx-lrlx Allowed -States 3 +States 2 1:a=0; 1:b=0; -1:a=1; 1:b=0; 1:a=1; 1:b=1; -Ok +No Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Condition exists (1:a=1 /\ 1:b=0) -Observation mp-srlx-srel-lrlx-lrlx Sometimes 1 2 +Observation mp-srlx-srel-lrlx-lrlx Never 0 2 Hash=57dd88436ff37a55207a60cd86beb3cc diff --git a/tests/gonzalo/mp/mp-srlx-srlx-lacq-lrlx.litmus.expected b/tests/gonzalo/mp/mp-srlx-srlx-lacq-lrlx.litmus.expected index 30ca4a82..0435a7fa 100644 --- a/tests/gonzalo/mp/mp-srlx-srlx-lacq-lrlx.litmus.expected +++ b/tests/gonzalo/mp/mp-srlx-srlx-lacq-lrlx.litmus.expected @@ -1,12 +1,11 @@ Test mp-srlx-srlx-lacq-lrlx Allowed -States 3 +States 2 1:a=0; 1:b=0; -1:a=1; 1:b=0; 1:a=1; 1:b=1; -Ok +No Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Condition exists (1:a=1 /\ 1:b=0) -Observation mp-srlx-srlx-lacq-lrlx Sometimes 1 2 +Observation mp-srlx-srlx-lacq-lrlx Never 0 2 Hash=1eabf8f013cba9be20759ba7202d9a38 diff --git a/tests/gonzalo/mp/mp-srlx-srlx-lrlx-lrlx.litmus.expected b/tests/gonzalo/mp/mp-srlx-srlx-lrlx-lrlx.litmus.expected index 1c0bdb7a..3e873381 100644 --- a/tests/gonzalo/mp/mp-srlx-srlx-lrlx-lrlx.litmus.expected +++ b/tests/gonzalo/mp/mp-srlx-srlx-lrlx-lrlx.litmus.expected @@ -1,12 +1,11 @@ Test mp-srlx-srlx-lrlx-lrlx Allowed -States 3 +States 2 1:a=0; 1:b=0; -1:a=1; 1:b=0; 1:a=1; 1:b=1; -Ok +No Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Condition exists (1:a=1 /\ 1:b=0) -Observation mp-srlx-srlx-lrlx-lrlx Sometimes 1 2 +Observation mp-srlx-srlx-lrlx-lrlx Never 0 2 Hash=08cce0931b85a75fbda999537bfd2f54 diff --git a/tests/gonzalo/rs/mp-rs-add-est-atomic.litmus.expected b/tests/gonzalo/rs/mp-rs-add-est-atomic.litmus.expected index 9a65890f..96e40816 100644 --- a/tests/gonzalo/rs/mp-rs-add-est-atomic.litmus.expected +++ b/tests/gonzalo/rs/mp-rs-add-est-atomic.litmus.expected @@ -1,17 +1,16 @@ Test mp-rs-add-est Allowed -States 8 +States 7 1:a=0; 1:b=0; [x]=2; 1:a=0; 1:b=0; [x]=3; 1:a=1; 1:b=0; [x]=2; 1:a=1; 1:b=0; [x]=3; 1:a=2; 1:b=0; [x]=2; 1:a=2; 1:b=0; [x]=3; -1:a=3; 1:b=0; [x]=3; 1:a=3; 1:b=1; [x]=3; -Ok +No Witnesses -Positive: 1 Negative: 12 +Positive: 0 Negative: 12 Condition exists ([x]=3 /\ 1:a=3 /\ 1:b=0) -Observation mp-rs-add-est Sometimes 1 12 +Observation mp-rs-add-est Never 0 12 Hash=d9e5b0ee0a001a2f442e4d081a17d0df diff --git a/tests/gonzalo/rs/mp-rs-st-eadd-atomics.cpp11.litmus.expected b/tests/gonzalo/rs/mp-rs-st-eadd-atomics.cpp11.litmus.expected index 15e21b38..74e685ba 100644 --- a/tests/gonzalo/rs/mp-rs-st-eadd-atomics.cpp11.litmus.expected +++ b/tests/gonzalo/rs/mp-rs-st-eadd-atomics.cpp11.litmus.expected @@ -1,16 +1,14 @@ Test mp-rs-st-eadd-atomics Forbidden -States 7 +States 5 1:a=0; 1:b=0; 1:a=1; 1:b=0; 1:a=2; 1:b=1; -1:a=3; 1:b=0; 1:a=3; 1:b=1; -1:a=4; 1:b=0; 1:a=4; 1:b=1; -No +Ok Witnesses -Positive: 15 Negative: 1 +Positive: 12 Negative: 0 Condition ~exists ((1:a=2 \/ 1:a=4) /\ 1:b=0) -Observation mp-rs-st-eadd-atomics Sometimes 1 15 +Observation mp-rs-st-eadd-atomics Never 0 12 Hash=7be42b6d808fe9ea4f6e0865ff19afd1 diff --git a/tests/gonzalo/rs/mp-rs-st-eadd-atomics.cpp17.litmus.expected b/tests/gonzalo/rs/mp-rs-st-eadd-atomics.cpp17.litmus.expected index 433bb61d..d8d6961b 100644 --- a/tests/gonzalo/rs/mp-rs-st-eadd-atomics.cpp17.litmus.expected +++ b/tests/gonzalo/rs/mp-rs-st-eadd-atomics.cpp17.litmus.expected @@ -1,16 +1,14 @@ Test mp-rs-st-eadd-atomics Forbidden -States 7 +States 5 1:a=0; 1:b=0; 1:a=1; 1:b=0; 1:a=2; 1:b=1; -1:a=3; 1:b=0; 1:a=3; 1:b=1; -1:a=4; 1:b=0; 1:a=4; 1:b=1; Ok Witnesses -Positive: 16 Negative: 0 +Positive: 12 Negative: 0 Condition ~exists (1:a=2 /\ 1:b=0) -Observation mp-rs-st-eadd-atomics Never 0 16 +Observation mp-rs-st-eadd-atomics Never 0 12 Hash=7be42b6d808fe9ea4f6e0865ff19afd1 diff --git a/tests/gonzalo/rs/mp-rs-st-est-atomics.litmus.expected b/tests/gonzalo/rs/mp-rs-st-est-atomics.litmus.expected index 40087449..2af5f55b 100644 --- a/tests/gonzalo/rs/mp-rs-st-est-atomics.litmus.expected +++ b/tests/gonzalo/rs/mp-rs-st-est-atomics.litmus.expected @@ -1,19 +1,17 @@ Test mp-rs-st-est-atomics-cpp11 Allowed -States 10 +States 8 1:a=0; 1:b=0; [x]=2; 1:a=0; 1:b=0; [x]=3; 1:a=1; 1:b=0; [x]=2; 1:a=1; 1:b=0; [x]=3; 1:a=2; 1:b=0; [x]=2; 1:a=2; 1:b=0; [x]=3; -1:a=3; 1:b=0; [x]=2; -1:a=3; 1:b=0; [x]=3; 1:a=3; 1:b=1; [x]=2; 1:a=3; 1:b=1; [x]=3; -Ok +No Witnesses -Positive: 2 Negative: 13 +Positive: 0 Negative: 12 Condition exists ([x]=3 /\ 1:a=3 /\ 1:b=0) -Observation mp-rs-st-est-atomics-cpp11 Sometimes 2 13 +Observation mp-rs-st-est-atomics-cpp11 Never 0 12 Hash=983f457abc7f45248268738be602ed44 diff --git a/tests/herdrc11/C13.litmus.expected b/tests/herdrc11/C13.litmus.expected index 67f85c4f..204c234c 100644 --- a/tests/herdrc11/C13.litmus.expected +++ b/tests/herdrc11/C13.litmus.expected @@ -1,11 +1,10 @@ Test C13 Allowed -States 2 -0:r1=S13; 0:r2=S13; 1:r4=S13; +States 1 0:r1=0; 0:r2=0; 1:r4=0; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (not (0:r1=0)) -Observation C13 Sometimes 1 3 +Observation C13 Never 0 3 Hash=70ddc011bf3f6c58e4434450a8a3440c diff --git a/tests/herdrc11/LB+fetch.addrlxrlx-porlxrlxs.litmus.expected b/tests/herdrc11/LB+fetch.addrlxrlx-porlxrlxs.litmus.expected index 047d0646..629db4b3 100644 --- a/tests/herdrc11/LB+fetch.addrlxrlx-porlxrlxs.litmus.expected +++ b/tests/herdrc11/LB+fetch.addrlxrlx-porlxrlxs.litmus.expected @@ -1,13 +1,12 @@ Test LB+fetch.addrlxrlx-porlxrlxs Allowed -States 4 +States 3 0:r0=0; 1:r0=0; [x]=1; [y]=1; 0:r0=0; 1:r0=1; [x]=1; [y]=3; 0:r0=1; 1:r0=0; [x]=3; [y]=1; -0:r0=1; 1:r0=1; [x]=3; [y]=3; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([x]=3 /\ [y]=3 /\ 0:r0=1 /\ 1:r0=1) -Observation LB+fetch.addrlxrlx-porlxrlxs Sometimes 1 3 +Observation LB+fetch.addrlxrlx-porlxrlxs Never 0 3 Hash=fb877ab1d7ccabbf69d82e26f8f61fc4 diff --git a/tests/herdrc11/LB+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/LB+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected index 839ce7d0..32155a05 100644 --- a/tests/herdrc11/LB+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/LB+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test LB+porlxrlx+fetch.addrlxrlx-porlxrlx Allowed -States 4 +States 3 0:r0=0; 1:r0=0; [y]=1; 0:r0=0; 1:r0=1; [y]=3; 0:r0=1; 1:r0=0; [y]=1; -0:r0=1; 1:r0=1; [y]=3; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([y]=3 /\ 0:r0=1 /\ 1:r0=1) -Observation LB+porlxrlx+fetch.addrlxrlx-porlxrlx Sometimes 1 3 +Observation LB+porlxrlx+fetch.addrlxrlx-porlxrlx Never 0 3 Hash=095157b6a99d75813323481e22106ded diff --git a/tests/herdrc11/LB+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/LB+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected index b4949877..9614e653 100644 --- a/tests/herdrc11/LB+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/LB+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected @@ -1,15 +1,13 @@ Test LB+porlxrlx+posWrlxrlx-porlxrlx Allowed -States 6 +States 4 0:r0=0; 1:r0=0; [y]=1; 0:r0=0; 1:r0=0; [y]=2; 0:r0=0; 1:r0=1; [y]=2; 0:r0=1; 1:r0=0; [y]=1; -0:r0=1; 1:r0=0; [y]=2; -0:r0=1; 1:r0=1; [y]=2; -Ok +No Witnesses -Positive: 1 Negative: 5 +Positive: 0 Negative: 4 Condition exists ([y]=2 /\ 0:r0=1 /\ 1:r0=1) -Observation LB+porlxrlx+posWrlxrlx-porlxrlx Sometimes 1 5 +Observation LB+porlxrlx+posWrlxrlx-porlxrlx Never 0 4 Hash=954cb7c63bfe70e606c50d5305ac6df5 diff --git a/tests/herdrc11/LB+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/LB+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected index 91f74781..59463b9f 100644 --- a/tests/herdrc11/LB+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/LB+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test LB+porlxrlx+rmwrlxrlx-porlxrlx Allowed -States 4 +States 3 0:r0=0; 1:r0=0; [y]=1; 0:r0=0; 1:r0=1; [y]=2; 0:r0=1; 1:r0=0; [y]=1; -0:r0=1; 1:r0=1; [y]=2; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([y]=2 /\ 0:r0=1 /\ 1:r0=1) -Observation LB+porlxrlx+rmwrlxrlx-porlxrlx Sometimes 1 3 +Observation LB+porlxrlx+rmwrlxrlx-porlxrlx Never 0 3 Hash=51f4294d4f63b641172fc47ef0f55991 diff --git a/tests/herdrc11/LB+posWrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/LB+posWrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected index e0d984dd..c1d865a1 100644 --- a/tests/herdrc11/LB+posWrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/LB+posWrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected @@ -1,15 +1,13 @@ Test LB+posWrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx Allowed -States 6 +States 4 0:r0=0; 1:r0=0; [x]=1; [y]=1; 0:r0=0; 1:r0=0; [x]=2; [y]=1; 0:r0=0; 1:r0=1; [x]=1; [y]=3; -0:r0=0; 1:r0=1; [x]=2; [y]=3; 0:r0=1; 1:r0=0; [x]=2; [y]=1; -0:r0=1; 1:r0=1; [x]=2; [y]=3; -Ok +No Witnesses -Positive: 1 Negative: 5 +Positive: 0 Negative: 4 Condition exists ([x]=2 /\ [y]=3 /\ 0:r0=1 /\ 1:r0=1) -Observation LB+posWrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx Sometimes 1 5 +Observation LB+posWrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx Never 0 4 Hash=3434bde812dcb79b54c89d1e6b43a938 diff --git a/tests/herdrc11/LB+rmwrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/LB+rmwrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected index 03d78abc..562dd7d5 100644 --- a/tests/herdrc11/LB+rmwrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/LB+rmwrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test LB+rmwrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx Allowed -States 4 +States 3 0:r0=0; 1:r0=0; [x]=1; [y]=1; 0:r0=0; 1:r0=1; [x]=1; [y]=3; 0:r0=1; 1:r0=0; [x]=2; [y]=1; -0:r0=1; 1:r0=1; [x]=2; [y]=3; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([x]=2 /\ [y]=3 /\ 0:r0=1 /\ 1:r0=1) -Observation LB+rmwrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx Sometimes 1 3 +Observation LB+rmwrlxrlx-porlxrlx+fetch.addrlxrlx-porlxrlx Never 0 3 Hash=a2334b8b69de678db5ed52d56260ce83 diff --git a/tests/herdrc11/MP+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/MP+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected index c387849c..bea7f05b 100644 --- a/tests/herdrc11/MP+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/MP+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test MP+porlxrlx+fetch.addrlxrlx-porlxrlx Allowed -States 4 +States 3 1:r0=0; 1:r1=0; [y]=1; 1:r0=0; 1:r1=1; [y]=1; -1:r0=1; 1:r1=0; [y]=3; 1:r0=1; 1:r1=1; [y]=3; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([y]=3 /\ 1:r0=1 /\ 1:r1=0) -Observation MP+porlxrlx+fetch.addrlxrlx-porlxrlx Sometimes 1 3 +Observation MP+porlxrlx+fetch.addrlxrlx-porlxrlx Never 0 3 Hash=379da3f357ed0c736fc0bd638f0828df diff --git a/tests/herdrc11/MP+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/MP+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected index 6bb7d6d1..3efcbf1c 100644 --- a/tests/herdrc11/MP+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/MP+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected @@ -1,15 +1,13 @@ Test MP+porlxrlx+posWrlxrlx-porlxrlx Allowed -States 6 +States 4 1:r0=0; 1:r1=0; [y]=1; -1:r0=0; 1:r1=0; [y]=2; 1:r0=0; 1:r1=1; [y]=1; 1:r0=0; 1:r1=1; [y]=2; -1:r0=1; 1:r1=0; [y]=2; 1:r0=1; 1:r1=1; [y]=2; -Ok +No Witnesses -Positive: 1 Negative: 5 +Positive: 0 Negative: 4 Condition exists ([y]=2 /\ 1:r0=1 /\ 1:r1=0) -Observation MP+porlxrlx+posWrlxrlx-porlxrlx Sometimes 1 5 +Observation MP+porlxrlx+posWrlxrlx-porlxrlx Never 0 4 Hash=6a3417f2a5afc5eafded86840739d1a3 diff --git a/tests/herdrc11/MP+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/MP+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected index 5a2702bf..bb397cc1 100644 --- a/tests/herdrc11/MP+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/MP+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test MP+porlxrlx+rmwrlxrlx-porlxrlx Allowed -States 4 +States 3 1:r0=0; 1:r1=0; [y]=1; 1:r0=0; 1:r1=1; [y]=1; -1:r0=1; 1:r1=0; [y]=2; 1:r0=1; 1:r1=1; [y]=2; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([y]=2 /\ 1:r0=1 /\ 1:r1=0) -Observation MP+porlxrlx+rmwrlxrlx-porlxrlx Sometimes 1 3 +Observation MP+porlxrlx+rmwrlxrlx-porlxrlx Never 0 3 Hash=30b4a0be14a338a4f581e5d56c7e0111 diff --git a/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlx+posWrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlx+posWrlxrlx-porlxrlx.litmus.expected index c6f72659..dc36ef7a 100644 --- a/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlx+posWrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlx+posWrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RR+RW+fetch.addrlxrlx-porlxrlx+posWrlxrlx-porlxrlx Allowed -States 4 +States 3 0:r0=0; 0:r1=0; 1:r0=0; [x]=1; 0:r0=0; 0:r1=1; 1:r0=0; [x]=1; -0:r0=1; 0:r1=0; 1:r0=0; [x]=3; 0:r0=1; 0:r1=1; 1:r0=0; [x]=3; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([x]=3 /\ 0:r0=1 /\ 0:r1=0 /\ 1:r0=0) -Observation RR+RW+fetch.addrlxrlx-porlxrlx+posWrlxrlx-porlxrlx Sometimes 1 3 +Observation RR+RW+fetch.addrlxrlx-porlxrlx+posWrlxrlx-porlxrlx Never 0 3 Hash=ecc7b1f20cbc1fce2e7fdcb2944da236 diff --git a/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected index 24c2d660..63433e9a 100644 --- a/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RR+RW+fetch.addrlxrlx-porlxrlx+rmwrlxrlx-porlxrlx Allowed -States 4 +States 3 0:r0=0; 0:r1=0; 1:r0=0; [x]=1; 0:r0=0; 0:r1=1; 1:r0=0; [x]=1; -0:r0=1; 0:r1=0; 1:r0=0; [x]=3; 0:r0=1; 0:r1=1; 1:r0=0; [x]=3; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([x]=3 /\ 0:r0=1 /\ 0:r1=0 /\ 1:r0=0) -Observation RR+RW+fetch.addrlxrlx-porlxrlx+rmwrlxrlx-porlxrlx Sometimes 1 3 +Observation RR+RW+fetch.addrlxrlx-porlxrlx+rmwrlxrlx-porlxrlx Never 0 3 Hash=33b5853c7fdcc46af20a75fc31dc8174 diff --git a/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlxs.litmus.expected b/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlxs.litmus.expected index 6dcfaa54..1646a42e 100644 --- a/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlxs.litmus.expected +++ b/tests/herdrc11/RR+RW+fetch.addrlxrlx-porlxrlxs.litmus.expected @@ -1,13 +1,12 @@ Test RR+RW+fetch.addrlxrlx-porlxrlxs Allowed -States 4 +States 3 0:r0=0; 0:r1=0; 1:r0=0; [x]=1; 0:r0=0; 0:r1=1; 1:r0=0; [x]=1; -0:r0=1; 0:r1=0; 1:r0=0; [x]=3; 0:r0=1; 0:r1=1; 1:r0=0; [x]=3; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([x]=3 /\ 0:r0=1 /\ 0:r1=0 /\ 1:r0=0) -Observation RR+RW+fetch.addrlxrlx-porlxrlxs Sometimes 1 3 +Observation RR+RW+fetch.addrlxrlx-porlxrlxs Never 0 3 Hash=dd657c21da96ea89798f07d66e87d3d5 diff --git a/tests/herdrc11/RR+RW+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/RR+RW+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected index e7f6cfd2..8314520b 100644 --- a/tests/herdrc11/RR+RW+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/RR+RW+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RR+RW+porlxrlx+fetch.addrlxrlx-porlxrlx Allowed -States 4 +States 3 0:r0=0; 0:r1=0; 1:r0=0; 0:r0=0; 0:r1=1; 1:r0=0; -0:r0=1; 0:r1=0; 1:r0=0; 0:r0=1; 0:r1=1; 1:r0=0; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 0:r1=0 /\ 1:r0=0) -Observation RR+RW+porlxrlx+fetch.addrlxrlx-porlxrlx Sometimes 1 3 +Observation RR+RW+porlxrlx+fetch.addrlxrlx-porlxrlx Never 0 3 Hash=bfbf6d8ba0bf34568e27bc49586c6279 diff --git a/tests/herdrc11/RR+RW+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/RR+RW+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected index 1de5fffc..c5b37d90 100644 --- a/tests/herdrc11/RR+RW+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/RR+RW+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RR+RW+porlxrlx+posWrlxrlx-porlxrlx Allowed -States 4 +States 3 0:r0=0; 0:r1=0; 1:r0=0; 0:r0=0; 0:r1=1; 1:r0=0; -0:r0=1; 0:r1=0; 1:r0=0; 0:r0=1; 0:r1=1; 1:r0=0; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 0:r1=0 /\ 1:r0=0) -Observation RR+RW+porlxrlx+posWrlxrlx-porlxrlx Sometimes 1 3 +Observation RR+RW+porlxrlx+posWrlxrlx-porlxrlx Never 0 3 Hash=152375f25e465f1c4e0f508899f6ad0d diff --git a/tests/herdrc11/RR+RW+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/RR+RW+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected index 68751542..9193bf6c 100644 --- a/tests/herdrc11/RR+RW+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/RR+RW+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RR+RW+porlxrlx+rmwrlxrlx-porlxrlx Allowed -States 4 +States 3 0:r0=0; 0:r1=0; 1:r0=0; 0:r0=0; 0:r1=1; 1:r0=0; -0:r0=1; 0:r1=0; 1:r0=0; 0:r0=1; 0:r1=1; 1:r0=0; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 0:r1=0 /\ 1:r0=0) -Observation RR+RW+porlxrlx+rmwrlxrlx-porlxrlx Sometimes 1 3 +Observation RR+RW+porlxrlx+rmwrlxrlx-porlxrlx Never 0 3 Hash=df57a194bfa4f8bdde5a765eaa959f00 diff --git a/tests/herdrc11/RR+WR+fetch.addrlxrlx-porlxrlx+porlxrlx.litmus.expected b/tests/herdrc11/RR+WR+fetch.addrlxrlx-porlxrlx+porlxrlx.litmus.expected index 2fa75846..2efc542a 100644 --- a/tests/herdrc11/RR+WR+fetch.addrlxrlx-porlxrlx+porlxrlx.litmus.expected +++ b/tests/herdrc11/RR+WR+fetch.addrlxrlx-porlxrlx+porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RR+WR+fetch.addrlxrlx-porlxrlx+porlxrlx Allowed -States 4 -0:r0=0; 0:r1=0; 1:r0=0; +States 3 0:r0=0; 0:r1=0; 1:r0=1; 0:r0=0; 0:r1=1; 1:r0=0; 0:r0=0; 0:r1=1; 1:r0=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=0 /\ 0:r1=0 /\ 1:r0=0) -Observation RR+WR+fetch.addrlxrlx-porlxrlx+porlxrlx Sometimes 1 3 +Observation RR+WR+fetch.addrlxrlx-porlxrlx+porlxrlx Never 0 3 Hash=56df17a81ffdcebaa55c904a6906838d diff --git a/tests/herdrc11/RR+WR+posWrlxrlx-porlxrlx+porlxrlx.litmus.expected b/tests/herdrc11/RR+WR+posWrlxrlx-porlxrlx+porlxrlx.litmus.expected index 5e3da281..fc43211e 100644 --- a/tests/herdrc11/RR+WR+posWrlxrlx-porlxrlx+porlxrlx.litmus.expected +++ b/tests/herdrc11/RR+WR+posWrlxrlx-porlxrlx+porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RR+WR+posWrlxrlx-porlxrlx+porlxrlx Allowed -States 4 -0:r0=0; 0:r1=0; 1:r0=0; +States 3 0:r0=0; 0:r1=0; 1:r0=1; 0:r0=0; 0:r1=1; 1:r0=0; 0:r0=0; 0:r1=1; 1:r0=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=0 /\ 0:r1=0 /\ 1:r0=0) -Observation RR+WR+posWrlxrlx-porlxrlx+porlxrlx Sometimes 1 3 +Observation RR+WR+posWrlxrlx-porlxrlx+porlxrlx Never 0 3 Hash=736a73a8cb0be038527c1908e0155387 diff --git a/tests/herdrc11/RR+WR+rmwrlxrlx-porlxrlx+porlxrlx.litmus.expected b/tests/herdrc11/RR+WR+rmwrlxrlx-porlxrlx+porlxrlx.litmus.expected index 7e69a68d..815275ae 100644 --- a/tests/herdrc11/RR+WR+rmwrlxrlx-porlxrlx+porlxrlx.litmus.expected +++ b/tests/herdrc11/RR+WR+rmwrlxrlx-porlxrlx+porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RR+WR+rmwrlxrlx-porlxrlx+porlxrlx Allowed -States 4 -0:r0=0; 0:r1=0; 1:r0=0; +States 3 0:r0=0; 0:r1=0; 1:r0=1; 0:r0=0; 0:r1=1; 1:r0=0; 0:r0=0; 0:r1=1; 1:r0=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=0 /\ 0:r1=0 /\ 1:r0=0) -Observation RR+WR+rmwrlxrlx-porlxrlx+porlxrlx Sometimes 1 3 +Observation RR+WR+rmwrlxrlx-porlxrlx+porlxrlx Never 0 3 Hash=90333f04c20e6fd3c22e75f4602772c6 diff --git a/tests/herdrc11/RW+WR+fetch.addrlxrlx-porlxrlx+porlxrlx.litmus.expected b/tests/herdrc11/RW+WR+fetch.addrlxrlx-porlxrlx+porlxrlx.litmus.expected index 303fb48b..2eba9f84 100644 --- a/tests/herdrc11/RW+WR+fetch.addrlxrlx-porlxrlx+porlxrlx.litmus.expected +++ b/tests/herdrc11/RW+WR+fetch.addrlxrlx-porlxrlx+porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RW+WR+fetch.addrlxrlx-porlxrlx+porlxrlx Allowed -States 4 +States 3 0:r0=0; 1:r0=0; [y]=1; -0:r0=0; 1:r0=0; [y]=2; 0:r0=0; 1:r0=1; [y]=1; 0:r0=0; 1:r0=1; [y]=2; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([y]=2 /\ 0:r0=0 /\ 1:r0=0) -Observation RW+WR+fetch.addrlxrlx-porlxrlx+porlxrlx Sometimes 1 3 +Observation RW+WR+fetch.addrlxrlx-porlxrlx+porlxrlx Never 0 3 Hash=41476d3497c984d232240dc7f4d8bded diff --git a/tests/herdrc11/RW+WR+posWrlxrlx-porlxrlx+porlxrlx.litmus.expected b/tests/herdrc11/RW+WR+posWrlxrlx-porlxrlx+porlxrlx.litmus.expected index 33fe586f..375ae88d 100644 --- a/tests/herdrc11/RW+WR+posWrlxrlx-porlxrlx+porlxrlx.litmus.expected +++ b/tests/herdrc11/RW+WR+posWrlxrlx-porlxrlx+porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RW+WR+posWrlxrlx-porlxrlx+porlxrlx Allowed -States 4 +States 3 0:r0=0; 1:r0=0; [y]=1; -0:r0=0; 1:r0=0; [y]=2; 0:r0=0; 1:r0=1; [y]=1; 0:r0=0; 1:r0=1; [y]=2; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([y]=2 /\ 0:r0=0 /\ 1:r0=0) -Observation RW+WR+posWrlxrlx-porlxrlx+porlxrlx Sometimes 1 3 +Observation RW+WR+posWrlxrlx-porlxrlx+porlxrlx Never 0 3 Hash=6dc4e80b0dcf4153051df0335e825a9d diff --git a/tests/herdrc11/RW+WR+rmwrlxrlx-porlxrlx+porlxrlx.litmus.expected b/tests/herdrc11/RW+WR+rmwrlxrlx-porlxrlx+porlxrlx.litmus.expected index d4676f91..1d17e433 100644 --- a/tests/herdrc11/RW+WR+rmwrlxrlx-porlxrlx+porlxrlx.litmus.expected +++ b/tests/herdrc11/RW+WR+rmwrlxrlx-porlxrlx+porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test RW+WR+rmwrlxrlx-porlxrlx+porlxrlx Allowed -States 4 +States 3 0:r0=0; 1:r0=0; [y]=1; -0:r0=0; 1:r0=0; [y]=2; 0:r0=0; 1:r0=1; [y]=1; 0:r0=0; 1:r0=1; [y]=2; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([y]=2 /\ 0:r0=0 /\ 1:r0=0) -Observation RW+WR+rmwrlxrlx-porlxrlx+porlxrlx Sometimes 1 3 +Observation RW+WR+rmwrlxrlx-porlxrlx+porlxrlx Never 0 3 Hash=e503fc6683ba63e28e505a0550527dfb diff --git a/tests/herdrc11/S+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/S+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected index 5f923a70..e3766545 100644 --- a/tests/herdrc11/S+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/S+porlxrlx+fetch.addrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test S+porlxrlx+fetch.addrlxrlx-porlxrlx Allowed -States 4 +States 3 1:r0=0; [x]=1; [y]=1; 1:r0=0; [x]=2; [y]=1; 1:r0=1; [x]=1; [y]=3; -1:r0=1; [x]=2; [y]=3; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([x]=2 /\ [y]=3 /\ 1:r0=1) -Observation S+porlxrlx+fetch.addrlxrlx-porlxrlx Sometimes 1 3 +Observation S+porlxrlx+fetch.addrlxrlx-porlxrlx Never 0 3 Hash=6870c9182179bd4307a7f354aa779909 diff --git a/tests/herdrc11/S+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/S+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected index 0f663a91..7b257d83 100644 --- a/tests/herdrc11/S+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/S+porlxrlx+posWrlxrlx-porlxrlx.litmus.expected @@ -1,15 +1,13 @@ Test S+porlxrlx+posWrlxrlx-porlxrlx Allowed -States 6 +States 4 1:r0=0; [x]=1; [y]=1; 1:r0=0; [x]=1; [y]=2; 1:r0=0; [x]=2; [y]=1; -1:r0=0; [x]=2; [y]=2; 1:r0=1; [x]=1; [y]=2; -1:r0=1; [x]=2; [y]=2; -Ok +No Witnesses -Positive: 1 Negative: 5 +Positive: 0 Negative: 4 Condition exists ([x]=2 /\ [y]=2 /\ 1:r0=1) -Observation S+porlxrlx+posWrlxrlx-porlxrlx Sometimes 1 5 +Observation S+porlxrlx+posWrlxrlx-porlxrlx Never 0 4 Hash=a211f660b76160058740f64509dc37a8 diff --git a/tests/herdrc11/S+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected b/tests/herdrc11/S+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected index ba1874ba..19cf6d4d 100644 --- a/tests/herdrc11/S+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected +++ b/tests/herdrc11/S+porlxrlx+rmwrlxrlx-porlxrlx.litmus.expected @@ -1,13 +1,12 @@ Test S+porlxrlx+rmwrlxrlx-porlxrlx Allowed -States 4 +States 3 1:r0=0; [x]=1; [y]=1; 1:r0=0; [x]=2; [y]=1; 1:r0=1; [x]=1; [y]=2; -1:r0=1; [x]=2; [y]=2; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists ([x]=2 /\ [y]=2 /\ 1:r0=1) -Observation S+porlxrlx+rmwrlxrlx-porlxrlx Sometimes 1 3 +Observation S+porlxrlx+rmwrlxrlx-porlxrlx Never 0 3 Hash=7c286bb63932784e00556ba4c6378b43 diff --git a/tests/paul_oota/oota-3-2-proc-opt.litmus.expected b/tests/paul_oota/oota-3-2-proc-opt.litmus.expected index d03aec17..4069d265 100644 --- a/tests/paul_oota/oota-3-2-proc-opt.litmus.expected +++ b/tests/paul_oota/oota-3-2-proc-opt.litmus.expected @@ -1,11 +1,10 @@ Test oota-3-2-proc-opt Allowed -States 2 -0:r1=S10; 1:r2=S10; 1:r3=0; [x]=S10; [y]=S10; [z]=S10; +States 1 0:r1=0; 1:r2=0; 1:r3=0; [x]=0; [y]=0; [z]=0; No Witnesses -Positive: 0 Negative: 4 +Positive: 0 Negative: 3 Condition exists (0:r1=17 /\ 1:r2=17 /\ 1:r3=17) -Observation oota-3-2-proc-opt Never 0 4 +Observation oota-3-2-proc-opt Never 0 3 Hash=f95c908abe0279a163f888cdfe675da9 diff --git a/tests/paul_oota/oota-3-2-proc.litmus.expected b/tests/paul_oota/oota-3-2-proc.litmus.expected index cd45a680..aa1a42de 100644 --- a/tests/paul_oota/oota-3-2-proc.litmus.expected +++ b/tests/paul_oota/oota-3-2-proc.litmus.expected @@ -1,11 +1,10 @@ Test oota-3-2-proc Allowed -States 2 -0:r1=S12; 1:r2=S12; 1:r3=S12; [x]=S12; [y]=S12; [z]=S12; +States 1 0:r1=0; 1:r2=0; 1:r3=0; [x]=0; [y]=0; [z]=0; No Witnesses -Positive: 0 Negative: 4 +Positive: 0 Negative: 3 Condition exists (0:r1=17 /\ 1:r2=17 /\ 1:r3=17) -Observation oota-3-2-proc Never 0 4 +Observation oota-3-2-proc Never 0 3 Hash=58048660bab55de61d7af73c9952f22f diff --git a/tests/paul_oota/oota-3proc.litmus.expected b/tests/paul_oota/oota-3proc.litmus.expected index e98c4211..e1ff266e 100644 --- a/tests/paul_oota/oota-3proc.litmus.expected +++ b/tests/paul_oota/oota-3proc.litmus.expected @@ -1,11 +1,10 @@ Test oota-3proc Allowed -States 2 -0:r1=S12; 1:r2=S12; 2:r3=S12; [x]=S12; [y]=S12; [z]=S12; +States 1 0:r1=0; 1:r2=0; 2:r3=0; [x]=0; [y]=0; [z]=0; No Witnesses -Positive: 0 Negative: 8 +Positive: 0 Negative: 7 Condition exists (0:r1=17 /\ 1:r2=17 /\ 2:r3=17) -Observation oota-3proc Never 0 8 +Observation oota-3proc Never 0 7 Hash=7b60f7bf272b1c0a2eebb75833119402 diff --git a/tests/paul_oota/oota-causality-1.litmus.expected b/tests/paul_oota/oota-causality-1.litmus.expected index 538bc676..55cadc76 100644 --- a/tests/paul_oota/oota-causality-1.litmus.expected +++ b/tests/paul_oota/oota-causality-1.litmus.expected @@ -1,12 +1,11 @@ Test oota-causality-1 Allowed -States 3 +States 2 0:r1=0; 1:r2=0; 0:r1=0; 1:r2=1; -0:r1=1; 1:r2=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r1=1 /\ 1:r2=1) -Observation oota-causality-1 Sometimes 1 3 +Observation oota-causality-1 Never 0 3 Hash=baf587541b236f633c0abc0092380c8f diff --git a/tests/paul_oota/oota-causality-10.litmus.expected b/tests/paul_oota/oota-causality-10.litmus.expected index 7a5482b7..a7d5e371 100644 --- a/tests/paul_oota/oota-causality-10.litmus.expected +++ b/tests/paul_oota/oota-causality-10.litmus.expected @@ -1,14 +1,13 @@ Test oota-causality-10 Allowed -States 5 +States 4 0:r1=0; 1:r2=0; 3:r3=0; 0:r1=0; 1:r2=0; 3:r3=1; 0:r1=1; 1:r2=0; 3:r3=1; -0:r1=1; 1:r2=1; 3:r3=0; 0:r1=1; 1:r2=1; 3:r3=1; -Ok +No Witnesses -Positive: 1 Negative: 7 +Positive: 0 Negative: 4 Condition exists (0:r1=1 /\ 1:r2=1 /\ 3:r3=0) -Observation oota-causality-10 Sometimes 1 7 +Observation oota-causality-10 Never 0 4 Hash=3f211656cb207d53e98926c46aabe41c diff --git a/tests/paul_oota/oota-causality-11.litmus.expected b/tests/paul_oota/oota-causality-11.litmus.expected index 20748827..74223db6 100644 --- a/tests/paul_oota/oota-causality-11.litmus.expected +++ b/tests/paul_oota/oota-causality-11.litmus.expected @@ -1,14 +1,11 @@ Test oota-causality-11 Allowed -States 5 +States 2 0:r1=0; 0:r2=0; 1:r3=0; 1:r4=0; [w]=0; [x]=1; [y]=0; [z]=0; 0:r1=0; 0:r2=1; 1:r3=0; 1:r4=0; [w]=0; [x]=1; [y]=1; [z]=0; -0:r1=0; 0:r2=1; 1:r3=1; 1:r4=0; [w]=0; [x]=1; [y]=1; [z]=1; -0:r1=1; 0:r2=1; 1:r3=1; 1:r4=0; [w]=1; [x]=1; [y]=1; [z]=1; -0:r1=1; 0:r2=1; 1:r3=1; 1:r4=1; [w]=1; [x]=1; [y]=1; [z]=1; -Ok +No Witnesses -Positive: 1 Negative: 15 +Positive: 0 Negative: 8 Condition exists (0:r1=1 /\ 0:r2=1 /\ 1:r3=1 /\ 1:r4=1) -Observation oota-causality-11 Sometimes 1 15 +Observation oota-causality-11 Never 0 8 Hash=74157e54f115173bab1a3c70e23ff896 diff --git a/tests/paul_oota/oota-causality-13.litmus.expected b/tests/paul_oota/oota-causality-13.litmus.expected index 9545a0f1..d1909c9d 100644 --- a/tests/paul_oota/oota-causality-13.litmus.expected +++ b/tests/paul_oota/oota-causality-13.litmus.expected @@ -1,11 +1,10 @@ Test oota-causality-13 Allowed -States 2 +States 1 0:r1=0; 1:r2=0; -0:r1=1; 1:r2=1; -Ok +No Witnesses -Positive: 1 Negative: 1 +Positive: 0 Negative: 1 Condition exists (0:r1=1 /\ 1:r2=1) -Observation oota-causality-13 Sometimes 1 1 +Observation oota-causality-13 Never 0 1 Hash=b983d5c34539df8266a0eaef071e3026 diff --git a/tests/paul_oota/oota-causality-14.litmus.expected b/tests/paul_oota/oota-causality-14.litmus.expected index 235c9d74..d50f8008 100644 --- a/tests/paul_oota/oota-causality-14.litmus.expected +++ b/tests/paul_oota/oota-causality-14.litmus.expected @@ -1,12 +1,11 @@ Test oota-causality-14 Allowed -States 3 +States 2 0:r1=0; 1:r2=0; 1:r3=0; 1:r4=0; 0:r1=0; 1:r2=1; 1:r3=0; 1:r4=1; -0:r1=1; 1:r2=0; 1:r3=1; 1:r4=1; -Ok +No Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Condition exists (0:r1=1 /\ 1:r2=0 /\ 1:r3=1 /\ not (1:r4=0)) -Observation oota-causality-14 Sometimes 1 2 +Observation oota-causality-14 Never 0 2 Hash=05b444c5ddc8d6a11236476bc35a0d02 diff --git a/tests/paul_oota/oota-causality-15.litmus.expected b/tests/paul_oota/oota-causality-15.litmus.expected index 0ad11862..a0d9037f 100644 --- a/tests/paul_oota/oota-causality-15.litmus.expected +++ b/tests/paul_oota/oota-causality-15.litmus.expected @@ -1,14 +1,13 @@ Test oota-causality-15 Allowed -States 5 +States 4 0:r0=0; 0:r1=0; 1:r2=0; 1:r3=0; 1:r4=0; 0:r0=0; 0:r1=0; 1:r2=1; 1:r3=0; 1:r4=1; 0:r0=1; 0:r1=0; 1:r2=0; 1:r3=0; 1:r4=0; 0:r0=1; 0:r1=0; 1:r2=1; 1:r3=0; 1:r4=1; -0:r0=1; 0:r1=1; 1:r2=0; 1:r3=1; 1:r4=1; -Ok +No Witnesses -Positive: 1 Negative: 4 +Positive: 0 Negative: 4 Condition exists (0:r0=1 /\ 0:r1=1 /\ 1:r2=0 /\ 1:r3=1 /\ not (1:r4=0)) -Observation oota-causality-15 Sometimes 1 4 +Observation oota-causality-15 Never 0 4 Hash=b69e202206e02ebc10da9ebce1ef54d3 diff --git a/tests/paul_oota/oota-causality-17.litmus.expected b/tests/paul_oota/oota-causality-17.litmus.expected index 7dda2f4e..d100645c 100644 --- a/tests/paul_oota/oota-causality-17.litmus.expected +++ b/tests/paul_oota/oota-causality-17.litmus.expected @@ -1,13 +1,12 @@ Test oota-causality-17 Allowed -States 4 -0:r1=S17; 0:r3=0; 1:r2=S17; +States 3 0:r1=0; 0:r3=0; 1:r2=0; 0:r1=42; 0:r3=0; 1:r2=0; 0:r1=42; 0:r3=0; 1:r2=42; No Witnesses -Positive: 0 Negative: 7 +Positive: 0 Negative: 5 Condition exists (0:r1=42 /\ 1:r2=42 /\ 0:r3=42) -Observation oota-causality-17 Never 0 7 +Observation oota-causality-17 Never 0 5 Hash=0d90d1171b8dcbdadfa1603f0121c36f diff --git a/tests/paul_oota/oota-causality-18.litmus.expected b/tests/paul_oota/oota-causality-18.litmus.expected index 080976fd..51d7a381 100644 --- a/tests/paul_oota/oota-causality-18.litmus.expected +++ b/tests/paul_oota/oota-causality-18.litmus.expected @@ -1,13 +1,12 @@ Test oota-causality-18 Allowed -States 4 -0:r1=S17; 0:r3=0; 1:r2=S17; +States 3 0:r1=0; 0:r3=0; 1:r2=0; 0:r1=42; 0:r3=0; 1:r2=0; 0:r1=42; 0:r3=0; 1:r2=42; No Witnesses -Positive: 0 Negative: 7 +Positive: 0 Negative: 5 Condition exists (0:r1=42 /\ 1:r2=42 /\ 0:r3=42) -Observation oota-causality-18 Never 0 7 +Observation oota-causality-18 Never 0 5 Hash=2759147e8d11b616583b2e98df0c1b49 diff --git a/tests/paul_oota/oota-causality-19.litmus.expected b/tests/paul_oota/oota-causality-19.litmus.expected index 3de59941..da76ad8f 100644 --- a/tests/paul_oota/oota-causality-19.litmus.expected +++ b/tests/paul_oota/oota-causality-19.litmus.expected @@ -1,13 +1,12 @@ Test oota-causality-19 Allowed -States 4 -0:r1=S8; 1:r2=S8; 2:r3=0; +States 3 0:r1=0; 1:r2=0; 2:r3=0; 0:r1=42; 1:r2=0; 2:r3=0; 0:r1=42; 1:r2=42; 2:r3=0; No Witnesses -Positive: 0 Negative: 16 +Positive: 0 Negative: 13 Condition exists (0:r1=42 /\ 1:r2=42 /\ 2:r3=42) -Observation oota-causality-19 Never 0 16 +Observation oota-causality-19 Never 0 13 Hash=a00d2318a7905329fe1db5988cdf896d diff --git a/tests/paul_oota/oota-causality-2.litmus.expected b/tests/paul_oota/oota-causality-2.litmus.expected index c81b6dfa..5ce4bb3c 100644 --- a/tests/paul_oota/oota-causality-2.litmus.expected +++ b/tests/paul_oota/oota-causality-2.litmus.expected @@ -1,12 +1,11 @@ Test oota-causality-2 Allowed -States 3 +States 2 0:r1=0; 0:r2=0; 1:r3=0; 0:r1=0; 0:r2=0; 1:r3=1; -0:r1=1; 0:r2=1; 1:r3=1; -Ok +No Witnesses -Positive: 1 Negative: 4 +Positive: 0 Negative: 4 Condition exists (0:r1=1 /\ 0:r2=1 /\ 1:r3=1) -Observation oota-causality-2 Sometimes 1 4 +Observation oota-causality-2 Never 0 4 Hash=92940f8168048f73e8d8b06dc7ddd874 diff --git a/tests/paul_oota/oota-causality-20.litmus.expected b/tests/paul_oota/oota-causality-20.litmus.expected index 789815a2..907419d2 100644 --- a/tests/paul_oota/oota-causality-20.litmus.expected +++ b/tests/paul_oota/oota-causality-20.litmus.expected @@ -1,13 +1,12 @@ Test oota-causality-20 Allowed -States 4 -0:r1=S8; 1:r2=S8; 2:r3=0; +States 3 0:r1=0; 1:r2=0; 2:r3=0; 0:r1=42; 1:r2=0; 2:r3=0; 0:r1=42; 1:r2=42; 2:r3=0; No Witnesses -Positive: 0 Negative: 16 +Positive: 0 Negative: 13 Condition exists (0:r1=42 /\ 1:r2=42 /\ 2:r3=42) -Observation oota-causality-20 Never 0 16 +Observation oota-causality-20 Never 0 13 Hash=4280adb1137a16d1eb21f939f679e417 diff --git a/tests/paul_oota/oota-causality-3.litmus.expected b/tests/paul_oota/oota-causality-3.litmus.expected index fdf3c409..be27d444 100644 --- a/tests/paul_oota/oota-causality-3.litmus.expected +++ b/tests/paul_oota/oota-causality-3.litmus.expected @@ -1,16 +1,15 @@ Test oota-causality-3 Allowed -States 7 +States 6 0:r1=0; 0:r2=0; 1:r3=0; 0:r1=0; 0:r2=0; 1:r3=1; 0:r1=0; 0:r2=2; 1:r3=0; -0:r1=1; 0:r2=1; 1:r3=1; 0:r1=2; 0:r2=0; 1:r3=0; 0:r1=2; 0:r2=2; 1:r3=0; 0:r1=2; 0:r2=2; 1:r3=1; -Ok +No Witnesses -Positive: 2 Negative: 16 +Positive: 0 Negative: 15 Condition exists (0:r1=1 /\ 0:r2=1 /\ 1:r3=1) -Observation oota-causality-3 Sometimes 2 16 +Observation oota-causality-3 Never 0 15 Hash=9c951a4f024af759d19cdf71db576307 diff --git a/tests/paul_oota/oota-causality-4.litmus.expected b/tests/paul_oota/oota-causality-4.litmus.expected index 06db9033..9c62034d 100644 --- a/tests/paul_oota/oota-causality-4.litmus.expected +++ b/tests/paul_oota/oota-causality-4.litmus.expected @@ -1,11 +1,10 @@ Test oota-causality-4 Allowed -States 2 -0:r1=S8; 1:r2=S8; +States 1 0:r1=0; 1:r2=0; No Witnesses -Positive: 0 Negative: 4 +Positive: 0 Negative: 3 Condition exists (0:r1=1 /\ 1:r2=1) -Observation oota-causality-4 Never 0 4 +Observation oota-causality-4 Never 0 3 Hash=3bd84f5edcd4ab49a7c5432ef988e26f diff --git a/tests/paul_oota/oota-causality-5.litmus.expected b/tests/paul_oota/oota-causality-5.litmus.expected index 050661e4..26f1754b 100644 --- a/tests/paul_oota/oota-causality-5.litmus.expected +++ b/tests/paul_oota/oota-causality-5.litmus.expected @@ -1,15 +1,13 @@ Test oota-causality-5 Allowed -States 6 -0:r1=S8; 1:r2=S8; 3:r3=0; -0:r1=S8; 1:r2=S8; 3:r3=1; +States 4 0:r1=0; 1:r2=0; 3:r3=0; 0:r1=0; 1:r2=0; 3:r3=1; 0:r1=1; 1:r2=0; 3:r3=1; 0:r1=1; 1:r2=1; 3:r3=1; No Witnesses -Positive: 0 Negative: 24 +Positive: 0 Negative: 18 Condition exists (0:r1=1 /\ 1:r2=1 /\ 3:r3=0) -Observation oota-causality-5 Never 0 24 +Observation oota-causality-5 Never 0 18 Hash=b445fc296da343a561126ca8be9641b1 diff --git a/tests/paul_oota/oota-causality-6.litmus.expected b/tests/paul_oota/oota-causality-6.litmus.expected index c024236c..7aba878f 100644 --- a/tests/paul_oota/oota-causality-6.litmus.expected +++ b/tests/paul_oota/oota-causality-6.litmus.expected @@ -1,12 +1,11 @@ Test oota-causality-6 Allowed -States 3 +States 2 0:r1=0; 1:r2=0; 0:r1=1; 1:r2=0; -0:r1=1; 1:r2=1; -Ok +No Witnesses -Positive: 1 Negative: 2 +Positive: 0 Negative: 2 Condition exists (0:r1=1 /\ 1:r2=1) -Observation oota-causality-6 Sometimes 1 2 +Observation oota-causality-6 Never 0 2 Hash=4fe4c86136f4068fbc7a66c1b94fc3a7 diff --git a/tests/paul_oota/oota-causality-7.litmus.expected b/tests/paul_oota/oota-causality-7.litmus.expected index ad4daebe..12d06d45 100644 --- a/tests/paul_oota/oota-causality-7.litmus.expected +++ b/tests/paul_oota/oota-causality-7.litmus.expected @@ -1,13 +1,11 @@ Test oota-causality-7 Allowed -States 4 +States 2 0:r1=0; 0:r2=0; 1:r3=0; 0:r1=0; 0:r2=1; 1:r3=0; -0:r1=0; 0:r2=1; 1:r3=1; -0:r1=1; 0:r2=1; 1:r3=1; -Ok +No Witnesses -Positive: 1 Negative: 7 +Positive: 0 Negative: 5 Condition exists (0:r1=1 /\ 0:r2=1 /\ 1:r3=1) -Observation oota-causality-7 Sometimes 1 7 +Observation oota-causality-7 Never 0 5 Hash=740f05f1945c1e87a858adc3746b688d diff --git a/tests/paul_oota/oota-causality-9.litmus.expected b/tests/paul_oota/oota-causality-9.litmus.expected index 8495a099..027901b7 100644 --- a/tests/paul_oota/oota-causality-9.litmus.expected +++ b/tests/paul_oota/oota-causality-9.litmus.expected @@ -6,8 +6,8 @@ States 4 0:r1=2; 0:r2=3; 1:r3=3; No Witnesses -Positive: 0 Negative: 10 +Positive: 0 Negative: 9 Condition exists (0:r1=1 /\ 0:r2=1) -Observation oota-causality-9 Never 0 10 +Observation oota-causality-9 Never 0 9 Hash=13118599aee16fff56561ba501927d6a diff --git a/tests/paul_oota/oota-causality-9a.litmus.expected b/tests/paul_oota/oota-causality-9a.litmus.expected index 07a43e78..bff0767d 100644 --- a/tests/paul_oota/oota-causality-9a.litmus.expected +++ b/tests/paul_oota/oota-causality-9a.litmus.expected @@ -6,8 +6,8 @@ States 4 0:r1=2; 0:r2=3; 1:r3=3; No Witnesses -Positive: 0 Negative: 10 +Positive: 0 Negative: 9 Condition exists (0:r1=1 /\ 0:r2=1) -Observation oota-causality-9a Never 0 10 +Observation oota-causality-9a Never 0 9 Hash=b4c68c21b957c06e7214fae53c084a37 diff --git a/tests/paul_oota/oota-ctrl.litmus.expected b/tests/paul_oota/oota-ctrl.litmus.expected index 12221c1e..df8e45b5 100644 --- a/tests/paul_oota/oota-ctrl.litmus.expected +++ b/tests/paul_oota/oota-ctrl.litmus.expected @@ -1,11 +1,10 @@ Test oota-ctrl Allowed -States 2 +States 1 0:r0=0; 1:r1=0; [x]=0; [y]=0; -0:r0=42; 1:r1=42; [x]=42; [y]=42; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=42 /\ 1:r1=42) -Observation oota-ctrl Sometimes 1 3 +Observation oota-ctrl Never 0 3 Hash=52fd9dd2c577bed91a2f7b071fd0d511 diff --git a/tests/paul_oota/oota-dg-1.litmus.expected b/tests/paul_oota/oota-dg-1.litmus.expected index 944b8bcc..9339e76e 100644 --- a/tests/paul_oota/oota-dg-1.litmus.expected +++ b/tests/paul_oota/oota-dg-1.litmus.expected @@ -1,14 +1,13 @@ Test oota-dg-1 Allowed -States 5 +States 4 1:r1=0; 1:r2=0; 2:r3=0; [x]=42; [y]=0; [z]=42; 1:r1=0; 1:r2=0; 2:r3=42; [x]=42; [y]=1; [z]=42; 1:r1=42; 1:r2=0; 2:r3=0; [x]=42; [y]=0; [z]=42; 1:r1=42; 1:r2=0; 2:r3=42; [x]=42; [y]=1; [z]=42; -1:r1=42; 1:r2=1; 2:r3=42; [x]=42; [y]=1; [z]=42; -Ok +No Witnesses -Positive: 1 Negative: 4 +Positive: 0 Negative: 4 Condition exists (1:r2=1 /\ [y]=1) -Observation oota-dg-1 Sometimes 1 4 +Observation oota-dg-1 Never 0 4 Hash=91e2fce7a1e61a6bb1544c2f310fde8f diff --git a/tests/paul_oota/oota-invent-int-load.litmus.expected b/tests/paul_oota/oota-invent-int-load.litmus.expected index ea4fd278..7835c31b 100644 --- a/tests/paul_oota/oota-invent-int-load.litmus.expected +++ b/tests/paul_oota/oota-invent-int-load.litmus.expected @@ -1,11 +1,10 @@ Test oota-invent-int-load Allowed -States 2 +States 1 0:r0=0; 1:r1=0; -0:r0=42; 1:r1=42; -Ok +No Witnesses -Positive: 3 Negative: 5 +Positive: 0 Negative: 5 Condition exists (0:r0=42 /\ 1:r1=42) -Observation oota-invent-int-load Sometimes 3 5 +Observation oota-invent-int-load Never 0 5 Hash=7d0246add471f86db0ece7949830873f diff --git a/tests/paul_oota/oota-two-source.litmus.expected b/tests/paul_oota/oota-two-source.litmus.expected index 6cbf3475..7f0dca2f 100644 --- a/tests/paul_oota/oota-two-source.litmus.expected +++ b/tests/paul_oota/oota-two-source.litmus.expected @@ -1,22 +1,10 @@ Test oota-two-source Allowed -States 13 -0:r1=S8; 1:r2=S8; 2:r3=S16; 3:r4=S16; -0:r1=S8; 1:r2=S8; 2:r3=0; 3:r4=0; -0:r1=S12; 1:r2=S12; 2:r3=S12; 3:r4=S12; -0:r1=S12; 1:r2=S12; 2:r3=S12; 3:r4=0; -0:r1=S16; 1:r2=S12; 2:r3=S12; 3:r4=S16; -0:r1=S16; 1:r2=S16; 2:r3=S16; 3:r4=S16; -0:r1=S16; 1:r2=S16; 2:r3=0; 3:r4=S16; -0:r1=S16; 1:r2=0; 2:r3=S16; 3:r4=S16; -0:r1=S16; 1:r2=0; 2:r3=0; 3:r4=S16; -0:r1=0; 1:r2=S12; 2:r3=S12; 3:r4=0; -0:r1=0; 1:r2=S16; 2:r3=S16; 3:r4=S16; -0:r1=0; 1:r2=0; 2:r3=S16; 3:r4=S16; +States 1 0:r1=0; 1:r2=0; 2:r3=0; 3:r4=0; No Witnesses -Positive: 0 Negative: 316 +Positive: 0 Negative: 120 Condition exists (0:r1=1 /\ 1:r2=1 \/ 2:r3=1 \/ 3:r4=1) -Observation oota-two-source Never 0 316 +Observation oota-two-source Never 0 120 Hash=c1dd393529dc4341a3641b1681f97cfc diff --git a/tests/paul_oota/simple-reordering.litmus.expected b/tests/paul_oota/simple-reordering.litmus.expected index feb351f5..995de03a 100644 --- a/tests/paul_oota/simple-reordering.litmus.expected +++ b/tests/paul_oota/simple-reordering.litmus.expected @@ -1,12 +1,11 @@ Test simple-reordering Allowed -States 3 +States 2 0:r1=0; 1:r2=0; 0:r1=42; 1:r2=0; -0:r1=42; 1:r2=42; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r1=42 /\ 1:r2=42) -Observation simple-reordering Sometimes 1 3 +Observation simple-reordering Never 0 3 Hash=7e0c5c12d2fd48415d57c268ee2e9ce6 diff --git a/tests/pldi17/iriw-acq-sc.litmus.expected b/tests/pldi17/iriw-acq-sc.litmus.expected index fb9b9b10..910adff6 100644 --- a/tests/pldi17/iriw-acq-sc.litmus.expected +++ b/tests/pldi17/iriw-acq-sc.litmus.expected @@ -1,5 +1,5 @@ Test iriw-acq-sc Allowed -States 16 +States 15 1:a=0; 1:c=0; 2:b=0; 2:d=0; 1:a=0; 1:c=0; 2:b=0; 2:d=1; 1:a=0; 1:c=0; 2:b=1; 2:d=0; @@ -10,16 +10,15 @@ States 16 1:a=0; 1:c=1; 2:b=1; 2:d=1; 1:a=1; 1:c=0; 2:b=0; 2:d=0; 1:a=1; 1:c=0; 2:b=0; 2:d=1; -1:a=1; 1:c=0; 2:b=1; 2:d=0; 1:a=1; 1:c=0; 2:b=1; 2:d=1; 1:a=1; 1:c=1; 2:b=0; 2:d=0; 1:a=1; 1:c=1; 2:b=0; 2:d=1; 1:a=1; 1:c=1; 2:b=1; 2:d=0; 1:a=1; 1:c=1; 2:b=1; 2:d=1; -Ok +No Witnesses -Positive: 1 Negative: 15 +Positive: 0 Negative: 15 Condition exists (1:a=1 /\ 2:b=1 /\ 1:c=0 /\ 2:d=0) -Observation iriw-acq-sc Sometimes 1 15 +Observation iriw-acq-sc Never 0 15 Hash=4d114d7795fbcbbfdbcf4d86833bd7b9 diff --git a/tests/pldi17/lb.litmus.expected b/tests/pldi17/lb.litmus.expected index 64789761..8990aa47 100644 --- a/tests/pldi17/lb.litmus.expected +++ b/tests/pldi17/lb.litmus.expected @@ -1,11 +1,10 @@ Test lb Allowed -States 2 -0:a=S8; 1:b=S8; +States 1 0:a=0; 1:b=0; No Witnesses -Positive: 0 Negative: 4 +Positive: 0 Negative: 3 Condition exists (0:a=1 /\ 1:b=1) -Observation lb Never 0 4 +Observation lb Never 0 3 Hash=6e4edbf1846c2f8c7db21476455d2309 diff --git a/tests/pldi17/sb+rfis.litmus.expected b/tests/pldi17/sb+rfis.litmus.expected index 27777cb4..edffd98f 100644 --- a/tests/pldi17/sb+rfis.litmus.expected +++ b/tests/pldi17/sb+rfis.litmus.expected @@ -1,13 +1,12 @@ Test sb+rfis Allowed -States 4 -0:a=1; 0:b=0; 1:c=1; 1:d=0; +States 3 0:a=1; 0:b=0; 1:c=1; 1:d=1; 0:a=1; 0:b=1; 1:c=1; 1:d=0; 0:a=1; 0:b=1; 1:c=1; 1:d=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:a=1 /\ 0:b=0 /\ 1:c=1 /\ 1:d=0) -Observation sb+rfis Sometimes 1 3 +Observation sb+rfis Never 0 3 Hash=d9dde076d62f77046dc4c807cd3ef0c6 diff --git a/tests/pldi17/wwmerge.litmus.expected b/tests/pldi17/wwmerge.litmus.expected index 60b52edd..f476eab1 100644 --- a/tests/pldi17/wwmerge.litmus.expected +++ b/tests/pldi17/wwmerge.litmus.expected @@ -1,27 +1,24 @@ Test wwmerge Allowed -States 18 +States 15 0:a=0; 0:b=0; 2:c=0; 0:a=0; 0:b=0; 2:c=1; 0:a=0; 0:b=0; 2:c=2; 0:a=0; 0:b=1; 2:c=0; 0:a=0; 0:b=1; 2:c=1; 0:a=0; 0:b=1; 2:c=2; -0:a=1; 0:b=0; 2:c=0; 0:a=1; 0:b=0; 2:c=1; 0:a=1; 0:b=0; 2:c=2; 0:a=1; 0:b=1; 2:c=0; 0:a=1; 0:b=1; 2:c=1; 0:a=1; 0:b=1; 2:c=2; -0:a=2; 0:b=0; 2:c=0; -0:a=2; 0:b=0; 2:c=1; 0:a=2; 0:b=0; 2:c=2; 0:a=2; 0:b=1; 2:c=0; 0:a=2; 0:b=1; 2:c=1; 0:a=2; 0:b=1; 2:c=2; -Ok +No Witnesses -Positive: 1 Negative: 17 +Positive: 0 Negative: 15 Condition exists (0:a=2 /\ 0:b=0 /\ 2:c=0) -Observation wwmerge Sometimes 1 17 +Observation wwmerge Never 0 15 Hash=046503ad81d4790aa63534888b9ce164 diff --git a/tests/pldi17/z6.u.litmus.expected b/tests/pldi17/z6.u.litmus.expected index 09558762..1495d9db 100644 --- a/tests/pldi17/z6.u.litmus.expected +++ b/tests/pldi17/z6.u.litmus.expected @@ -1,21 +1,20 @@ Test z6.u Allowed -States 12 +States 11 1:b=0; 1:c=1; 2:a=0; 1:b=0; 1:c=1; 2:a=1; 1:b=0; 1:c=3; 2:a=0; 1:b=0; 1:c=3; 2:a=1; 1:b=1; 1:c=2; 2:a=0; 1:b=1; 1:c=2; 2:a=1; -1:b=1; 1:c=3; 2:a=0; 1:b=1; 1:c=3; 2:a=1; 1:b=3; 1:c=1; 2:a=0; 1:b=3; 1:c=1; 2:a=1; 1:b=3; 1:c=4; 2:a=0; 1:b=3; 1:c=4; 2:a=1; -Ok +No Witnesses -Positive: 1 Negative: 23 +Positive: 0 Negative: 18 Condition exists (2:a=0 /\ 1:b=1 /\ 1:c=3) -Observation z6.u Sometimes 1 23 +Observation z6.u Never 0 18 Hash=cfc62c1993d060f8d29b77b3762a8440 diff --git a/tests/popl15/auto/a7_reorder+Cacq.litmus.expected b/tests/popl15/auto/a7_reorder+Cacq.litmus.expected index d45539b9..bbca8ad0 100644 --- a/tests/popl15/auto/a7_reorder+Cacq.litmus.expected +++ b/tests/popl15/auto/a7_reorder+Cacq.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder+Cacq Always 3 0 +Observation a7_reorder+Cacq Always 2 0 Hash=b8a4e3fd229d579141375032ff44856f diff --git a/tests/popl15/auto/a7_reorder+Crel-acq.litmus.expected b/tests/popl15/auto/a7_reorder+Crel-acq.litmus.expected index 9cb8d77e..adbeb393 100644 --- a/tests/popl15/auto/a7_reorder+Crel-acq.litmus.expected +++ b/tests/popl15/auto/a7_reorder+Crel-acq.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder+Crel-acq Always 3 0 +Observation a7_reorder+Crel-acq Always 2 0 Hash=12c814d44b8e027cb0828b517436812f diff --git a/tests/popl15/auto/a7_reorder+Crel.litmus.expected b/tests/popl15/auto/a7_reorder+Crel.litmus.expected index 0b7217ea..7f1d937c 100644 --- a/tests/popl15/auto/a7_reorder+Crel.litmus.expected +++ b/tests/popl15/auto/a7_reorder+Crel.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder+Crel Always 3 0 +Observation a7_reorder+Crel Always 2 0 Hash=29907f686b7c390219e7ba423b91ed29 diff --git a/tests/popl15/auto/a7_reorder+Crlx.litmus.expected b/tests/popl15/auto/a7_reorder+Crlx.litmus.expected index 1fb25a3e..b835b035 100644 --- a/tests/popl15/auto/a7_reorder+Crlx.litmus.expected +++ b/tests/popl15/auto/a7_reorder+Crlx.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder+Crlx Always 3 0 +Observation a7_reorder+Crlx Always 2 0 Hash=4404e262c7e4ad32331dba6bafe0ad10 diff --git a/tests/popl15/auto/a7_reorder+Csc.litmus.expected b/tests/popl15/auto/a7_reorder+Csc.litmus.expected index 8cfa323f..4da82d94 100644 --- a/tests/popl15/auto/a7_reorder+Csc.litmus.expected +++ b/tests/popl15/auto/a7_reorder+Csc.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder+Csc Always 3 0 +Observation a7_reorder+Csc Always 2 0 Hash=89f89c035df20e08fb11320bb9d39092 diff --git a/tests/popl15/auto/a7_reorder+Racq.litmus.expected b/tests/popl15/auto/a7_reorder+Racq.litmus.expected index 3d65b0df..fe72bfb6 100644 --- a/tests/popl15/auto/a7_reorder+Racq.litmus.expected +++ b/tests/popl15/auto/a7_reorder+Racq.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder+Racq Always 3 0 +Observation a7_reorder+Racq Always 2 0 Hash=d1879c5871f363dc27ed103c00f44678 diff --git a/tests/popl15/auto/a7_reorder+Rna.litmus.expected b/tests/popl15/auto/a7_reorder+Rna.litmus.expected index 59c885a6..ac280917 100644 --- a/tests/popl15/auto/a7_reorder+Rna.litmus.expected +++ b/tests/popl15/auto/a7_reorder+Rna.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder+Rna Always 3 0 +Observation a7_reorder+Rna Always 2 0 Hash=228f9b0c6ad343ae9edc3afcb2ad6593 diff --git a/tests/popl15/auto/a7_reorder+Rrel.litmus.expected b/tests/popl15/auto/a7_reorder+Rrel.litmus.expected index 6666b2ae..2e36336e 100644 --- a/tests/popl15/auto/a7_reorder+Rrel.litmus.expected +++ b/tests/popl15/auto/a7_reorder+Rrel.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder+Rrel Always 3 0 +Observation a7_reorder+Rrel Always 2 0 Hash=5751406f7035d55313555799bb17e20c diff --git a/tests/popl15/auto/a7_reorder+Rrlx.litmus.expected b/tests/popl15/auto/a7_reorder+Rrlx.litmus.expected index 7a4cecde..d750fbc6 100644 --- a/tests/popl15/auto/a7_reorder+Rrlx.litmus.expected +++ b/tests/popl15/auto/a7_reorder+Rrlx.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder+Rrlx Always 3 0 +Observation a7_reorder+Rrlx Always 2 0 Hash=9ba05091d47de88b5218d1319af039fb diff --git a/tests/popl15/auto/a7_reorder+Rsc.litmus.expected b/tests/popl15/auto/a7_reorder+Rsc.litmus.expected index 64e7c975..fc22bc66 100644 --- a/tests/popl15/auto/a7_reorder+Rsc.litmus.expected +++ b/tests/popl15/auto/a7_reorder+Rsc.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder+Rsc Always 3 0 +Observation a7_reorder+Rsc Always 2 0 Hash=fb6c6f6fb59f3c8e529d3f7efb246937 diff --git a/tests/popl15/auto/b+acq+rel.litmus.expected b/tests/popl15/auto/b+acq+rel.litmus.expected index efb7c5a7..7610c0a2 100644 --- a/tests/popl15/auto/b+acq+rel.litmus.expected +++ b/tests/popl15/auto/b+acq+rel.litmus.expected @@ -1,13 +1,12 @@ Test b+acq+rel Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+acq+rel Sometimes 1 3 +Observation b+acq+rel Never 0 3 Hash=0f7142d4a35f9e4a34d811105d759b25 diff --git a/tests/popl15/auto/b+acq+rlx.litmus.expected b/tests/popl15/auto/b+acq+rlx.litmus.expected index 6fb51991..a26aa3f6 100644 --- a/tests/popl15/auto/b+acq+rlx.litmus.expected +++ b/tests/popl15/auto/b+acq+rlx.litmus.expected @@ -1,13 +1,12 @@ Test b+acq+rlx Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+acq+rlx Sometimes 1 3 +Observation b+acq+rlx Never 0 3 Hash=a6ddbce34f4ed83e7398a60863004d24 diff --git a/tests/popl15/auto/b+acq+sc.litmus.expected b/tests/popl15/auto/b+acq+sc.litmus.expected index 8a5bb5d7..2cb2e03a 100644 --- a/tests/popl15/auto/b+acq+sc.litmus.expected +++ b/tests/popl15/auto/b+acq+sc.litmus.expected @@ -1,13 +1,12 @@ Test b+acq+sc Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+acq+sc Sometimes 1 3 +Observation b+acq+sc Never 0 3 Hash=f4c9acce455da0095bd9a81f9398dda3 diff --git a/tests/popl15/auto/b+rlx+rel.litmus.expected b/tests/popl15/auto/b+rlx+rel.litmus.expected index 6babdf0b..c2cf93e9 100644 --- a/tests/popl15/auto/b+rlx+rel.litmus.expected +++ b/tests/popl15/auto/b+rlx+rel.litmus.expected @@ -1,13 +1,12 @@ Test b+rlx+rel Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+rlx+rel Sometimes 1 3 +Observation b+rlx+rel Never 0 3 Hash=f4364386d981d551de45022ce1bd6389 diff --git a/tests/popl15/auto/b+rlx+rlx.litmus.expected b/tests/popl15/auto/b+rlx+rlx.litmus.expected index ff5c790e..f35da7f4 100644 --- a/tests/popl15/auto/b+rlx+rlx.litmus.expected +++ b/tests/popl15/auto/b+rlx+rlx.litmus.expected @@ -1,13 +1,12 @@ Test b+rlx+rlx Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+rlx+rlx Sometimes 1 3 +Observation b+rlx+rlx Never 0 3 Hash=263307ea63cba772b35ffa9562467a92 diff --git a/tests/popl15/auto/b+rlx+sc.litmus.expected b/tests/popl15/auto/b+rlx+sc.litmus.expected index b736e58b..4685e70f 100644 --- a/tests/popl15/auto/b+rlx+sc.litmus.expected +++ b/tests/popl15/auto/b+rlx+sc.litmus.expected @@ -1,13 +1,12 @@ Test b+rlx+sc Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+rlx+sc Sometimes 1 3 +Observation b+rlx+sc Never 0 3 Hash=fd321ba779c3afaa5a5f39644ed84c62 diff --git a/tests/popl15/auto/b+sc+rel.litmus.expected b/tests/popl15/auto/b+sc+rel.litmus.expected index beca87ea..c843368d 100644 --- a/tests/popl15/auto/b+sc+rel.litmus.expected +++ b/tests/popl15/auto/b+sc+rel.litmus.expected @@ -1,13 +1,12 @@ Test b+sc+rel Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+sc+rel Sometimes 1 3 +Observation b+sc+rel Never 0 3 Hash=f88964bb60588f8339ee6ec8fc43c303 diff --git a/tests/popl15/auto/b+sc+rlx.litmus.expected b/tests/popl15/auto/b+sc+rlx.litmus.expected index abe5d880..810a6c81 100644 --- a/tests/popl15/auto/b+sc+rlx.litmus.expected +++ b/tests/popl15/auto/b+sc+rlx.litmus.expected @@ -1,13 +1,12 @@ Test b+sc+rlx Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+sc+rlx Sometimes 1 3 +Observation b+sc+rlx Never 0 3 Hash=307b4f4af7807a1e790f80e56e464e74 diff --git a/tests/popl15/auto/b+sc+sc.litmus.expected b/tests/popl15/auto/b+sc+sc.litmus.expected index f5cb8835..01f39492 100644 --- a/tests/popl15/auto/b+sc+sc.litmus.expected +++ b/tests/popl15/auto/b+sc+sc.litmus.expected @@ -1,13 +1,12 @@ Test b+sc+sc Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b+sc+sc Sometimes 1 3 +Observation b+sc+sc Never 0 3 Hash=1b961ffe905698d0e34c2f492e2f63ed diff --git a/tests/popl15/manual/a7_reorder.litmus.expected b/tests/popl15/manual/a7_reorder.litmus.expected index 003d7cef..a2d8a041 100644 --- a/tests/popl15/manual/a7_reorder.litmus.expected +++ b/tests/popl15/manual/a7_reorder.litmus.expected @@ -3,9 +3,9 @@ States 1 Undef Witnesses -Positive: 3 Negative: 0 +Positive: 2 Negative: 0 Flag *undef* Condition forall (true) -Observation a7_reorder Always 3 0 +Observation a7_reorder Always 2 0 Hash=a4b9057736f07ef51c637e0ac38494b6 diff --git a/tests/popl15/manual/arfna.litmus.expected b/tests/popl15/manual/arfna.litmus.expected index 4a4b75a8..710526a6 100644 --- a/tests/popl15/manual/arfna.litmus.expected +++ b/tests/popl15/manual/arfna.litmus.expected @@ -1,12 +1,10 @@ Test arfna Allowed -States 2 +States 1 [x]=0; [y]=0; -[x]=1; [y]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([x]=1 /\ [y]=1) -Observation arfna Sometimes 1 1 +Observation arfna Never 0 1 Hash=c69a80006463884aeaf6958f9e74807a diff --git a/tests/popl15/manual/arfna2.litmus.expected b/tests/popl15/manual/arfna2.litmus.expected index 5346b328..f392f3d2 100644 --- a/tests/popl15/manual/arfna2.litmus.expected +++ b/tests/popl15/manual/arfna2.litmus.expected @@ -1,12 +1,10 @@ Test arfna_transformed Allowed -States 2 +States 1 [x]=0; [y]=0; -[x]=1; [y]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([x]=1 /\ [y]=1) -Observation arfna_transformed Sometimes 1 1 +Observation arfna_transformed Never 0 1 Hash=fbb437dbcdc8a88611a71fe92622c1d5 diff --git a/tests/popl15/manual/b.litmus.expected b/tests/popl15/manual/b.litmus.expected index 9844f293..8f9faf76 100644 --- a/tests/popl15/manual/b.litmus.expected +++ b/tests/popl15/manual/b.litmus.expected @@ -1,13 +1,12 @@ Test b Allowed -States 4 +States 3 0:r0=0; 1:r1=0; 0:r0=0; 1:r1=1; 0:r0=1; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r0=1 /\ 1:r1=1) -Observation b Sometimes 1 3 +Observation b Never 0 3 Hash=263307ea63cba772b35ffa9562467a92 diff --git a/tests/popl15/manual/c.litmus.expected b/tests/popl15/manual/c.litmus.expected index 66b46131..89e8b77e 100644 --- a/tests/popl15/manual/c.litmus.expected +++ b/tests/popl15/manual/c.litmus.expected @@ -1,12 +1,10 @@ Test c Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=1; [q]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c Sometimes 1 1 +Observation c Never 0 1 Hash=0ff4377802cdc23062bd3f44362c7fac diff --git a/tests/popl15/manual/c_p.litmus.expected b/tests/popl15/manual/c_p.litmus.expected index d8146dc6..667b7ff4 100644 --- a/tests/popl15/manual/c_p.litmus.expected +++ b/tests/popl15/manual/c_p.litmus.expected @@ -1,12 +1,10 @@ Test c_p Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=2; [q]=1; -Undef +No Witnesses -Positive: 0 Negative: 2 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_p Never 0 2 +Observation c_p Never 0 1 Hash=6b0ea2e4212c129f4929f58e34375feb diff --git a/tests/popl15/manual/c_p_reorder.litmus.expected b/tests/popl15/manual/c_p_reorder.litmus.expected index c5a1ef48..095b8e00 100644 --- a/tests/popl15/manual/c_p_reorder.litmus.expected +++ b/tests/popl15/manual/c_p_reorder.litmus.expected @@ -1,12 +1,10 @@ Test c_p_reorder Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=2; [q]=1; -Undef +No Witnesses -Positive: 0 Negative: 2 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_p_reorder Never 0 2 +Observation c_p_reorder Never 0 1 Hash=c67c1c81fada13c17a7e8ef2e1944b35 diff --git a/tests/popl15/manual/c_pq.litmus.expected b/tests/popl15/manual/c_pq.litmus.expected index 4dec50fc..9e2d88dd 100644 --- a/tests/popl15/manual/c_pq.litmus.expected +++ b/tests/popl15/manual/c_pq.litmus.expected @@ -1,12 +1,10 @@ Test c_pq Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=2; [q]=1; -Undef +No Witnesses -Positive: 0 Negative: 2 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_pq Never 0 2 +Observation c_pq Never 0 1 Hash=86e3436a379bae81d0e2f1d960cfd7cd diff --git a/tests/popl15/manual/c_pq_reorder.litmus.expected b/tests/popl15/manual/c_pq_reorder.litmus.expected index 1d1e6071..cdc442e8 100644 --- a/tests/popl15/manual/c_pq_reorder.litmus.expected +++ b/tests/popl15/manual/c_pq_reorder.litmus.expected @@ -1,12 +1,10 @@ Test c_pq_reorder Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=2; [q]=1; -Undef +No Witnesses -Positive: 0 Negative: 2 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_pq_reorder Never 0 2 +Observation c_pq_reorder Never 0 1 Hash=63b97be159ec65f84ff3c70d2e4e40e2 diff --git a/tests/popl15/manual/c_q.litmus.expected b/tests/popl15/manual/c_q.litmus.expected index 88cbf919..0faf9b90 100644 --- a/tests/popl15/manual/c_q.litmus.expected +++ b/tests/popl15/manual/c_q.litmus.expected @@ -1,12 +1,10 @@ Test c_q Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=1; [q]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_q Sometimes 1 1 +Observation c_q Never 0 1 Hash=bd2094625f1ee93e2689abfeb1c12d02 diff --git a/tests/popl15/manual/c_q_reorder.litmus.expected b/tests/popl15/manual/c_q_reorder.litmus.expected index acb4a111..f190782e 100644 --- a/tests/popl15/manual/c_q_reorder.litmus.expected +++ b/tests/popl15/manual/c_q_reorder.litmus.expected @@ -1,12 +1,10 @@ Test c_q_reorder Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=1; [q]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_q_reorder Sometimes 1 1 +Observation c_q_reorder Never 0 1 Hash=abda1ea76cc8deea5b2c8ca2ddb27a04 diff --git a/tests/popl15/manual/c_reorder.litmus.expected b/tests/popl15/manual/c_reorder.litmus.expected index 511606b4..400208ab 100644 --- a/tests/popl15/manual/c_reorder.litmus.expected +++ b/tests/popl15/manual/c_reorder.litmus.expected @@ -1,12 +1,10 @@ Test c_reorder Allowed -States 2 +States 1 [p]=0; [q]=0; -[p]=1; [q]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([p]=1 /\ [q]=1) -Observation c_reorder Sometimes 1 1 +Observation c_reorder Never 0 1 Hash=c6e61b3cc4e99d188768c792a17890f8 diff --git a/tests/popl15/manual/cyc.litmus.expected b/tests/popl15/manual/cyc.litmus.expected index 75c9506f..95b832aa 100644 --- a/tests/popl15/manual/cyc.litmus.expected +++ b/tests/popl15/manual/cyc.litmus.expected @@ -1,11 +1,10 @@ Test cyc Allowed -States 2 +States 1 0:r0=0; 1:r1=0; -0:r0=1; 1:r1=1; -Ok +No Witnesses -Positive: 1 Negative: 1 +Positive: 0 Negative: 1 Condition exists (0:r0=1 /\ 1:r1=1) -Observation cyc Sometimes 1 1 +Observation cyc Never 0 1 Hash=d16e1b2160f9a55f0bb557046b596103 diff --git a/tests/popl15/manual/cyc_na.litmus.expected b/tests/popl15/manual/cyc_na.litmus.expected index b7c3f5e5..633089cf 100644 --- a/tests/popl15/manual/cyc_na.litmus.expected +++ b/tests/popl15/manual/cyc_na.litmus.expected @@ -1,12 +1,10 @@ Test cyc_na Allowed -States 2 +States 1 0:r0=0; 1:r1=0; -0:r0=1; 1:r1=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists (0:r0=1 /\ 1:r1=1) -Observation cyc_na Sometimes 1 1 +Observation cyc_na Never 0 1 Hash=592962ab016c17f023c60a22e9365300 diff --git a/tests/popl15/manual/fig1.litmus.expected b/tests/popl15/manual/fig1.litmus.expected index 47a64c45..3975e1e3 100644 --- a/tests/popl15/manual/fig1.litmus.expected +++ b/tests/popl15/manual/fig1.litmus.expected @@ -3,8 +3,8 @@ States 1 [a]=1; [x]=1; [y]=1; Ok Witnesses -Positive: 4 Negative: 0 +Positive: 3 Negative: 0 Condition exists ([a]=1 /\ [x]=1 /\ [y]=1) -Observation fig1 Always 4 0 +Observation fig1 Always 3 0 Hash=1f61ce15fe6a88e6d904d414bf4b4d44 diff --git a/tests/popl15/manual/lb.litmus.expected b/tests/popl15/manual/lb.litmus.expected index 324d9fbc..0f0b2f98 100644 --- a/tests/popl15/manual/lb.litmus.expected +++ b/tests/popl15/manual/lb.litmus.expected @@ -1,13 +1,12 @@ Test lb Allowed -States 4 +States 3 0:r1=0; 1:r2=0; 0:r1=0; 1:r2=1; 0:r1=1; 1:r2=0; -0:r1=1; 1:r2=1; -Ok +No Witnesses -Positive: 1 Negative: 3 +Positive: 0 Negative: 3 Condition exists (0:r1=1 /\ 1:r2=1) -Observation lb Sometimes 1 3 +Observation lb Never 0 3 Hash=4cf90e2fdfda0174409e5fd545b6f19d diff --git a/tests/popl15/manual/linearisation.litmus.expected b/tests/popl15/manual/linearisation.litmus.expected index 2aff7ca5..2c2cc8ec 100644 --- a/tests/popl15/manual/linearisation.litmus.expected +++ b/tests/popl15/manual/linearisation.litmus.expected @@ -1,12 +1,10 @@ Test linearisation Allowed -States 2 +States 1 0:t=0; [w]=0; [x]=0; [y]=0; [z]=0; -0:t=2; [w]=1; [x]=1; [y]=1; [z]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists (0:t=2 /\ [w]=1 /\ [x]=1 /\ [y]=1 /\ [z]=1) -Observation linearisation Sometimes 1 1 +Observation linearisation Never 0 1 Hash=543d660acf26c106140b9ad29f6b4ccd diff --git a/tests/popl15/manual/linearisation2.litmus.expected b/tests/popl15/manual/linearisation2.litmus.expected index d4e36262..d793a177 100644 --- a/tests/popl15/manual/linearisation2.litmus.expected +++ b/tests/popl15/manual/linearisation2.litmus.expected @@ -1,11 +1,10 @@ Test linearisation2 Allowed -States 2 +States 1 0:t=0; [w]=0; [x]=0; [y]=0; [z]=0; -0:t=2; [w]=1; [x]=1; [y]=1; [z]=1; -Ok +No Witnesses -Positive: 1 Negative: 1 +Positive: 0 Negative: 1 Condition exists (0:t=2 /\ [w]=1 /\ [x]=1 /\ [y]=1 /\ [z]=1) -Observation linearisation2 Sometimes 1 1 +Observation linearisation2 Never 0 1 Hash=51e2c04a509c2f8d763f65266f14f3d5 diff --git a/tests/popl15/manual/roachmotel.litmus.expected b/tests/popl15/manual/roachmotel.litmus.expected index bf0b0372..2ca37fc8 100644 --- a/tests/popl15/manual/roachmotel.litmus.expected +++ b/tests/popl15/manual/roachmotel.litmus.expected @@ -1,12 +1,10 @@ Test roachmotel Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; [z]=1; -[a]=1; [x]=1; [y]=1; [z]=1; -Undef +No Witnesses -Positive: 2 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [z]=1 /\ [x]=1 /\ [y]=1) -Observation roachmotel Sometimes 2 1 +Observation roachmotel Never 0 1 Hash=89a4c1ec939981e0b843da41078b910c diff --git a/tests/popl15/manual/roachmotel2.litmus.expected b/tests/popl15/manual/roachmotel2.litmus.expected index 7cddcbf2..dd8fafd0 100644 --- a/tests/popl15/manual/roachmotel2.litmus.expected +++ b/tests/popl15/manual/roachmotel2.litmus.expected @@ -1,12 +1,10 @@ Test roachmotel2 Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; [z]=1; -[a]=1; [x]=1; [y]=1; [z]=1; -Undef +No Witnesses -Positive: 2 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [z]=1 /\ [x]=1 /\ [y]=1) -Observation roachmotel2 Sometimes 2 1 +Observation roachmotel2 Never 0 1 Hash=6d27da9e3c6dcde00c4db99dd97e6e43 diff --git a/tests/popl15/manual/seq.litmus.expected b/tests/popl15/manual/seq.litmus.expected index bd2fa071..4657ad50 100644 --- a/tests/popl15/manual/seq.litmus.expected +++ b/tests/popl15/manual/seq.litmus.expected @@ -1,12 +1,10 @@ Test seq Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; -[a]=1; [x]=1; [y]=1; -Undef +No Witnesses -Positive: 1 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [x]=1 /\ [y]=1) -Observation seq Sometimes 1 1 +Observation seq Never 0 1 Hash=0559dd8eb63cce8637b7d0e9945d646d diff --git a/tests/popl15/manual/seq2.litmus.expected b/tests/popl15/manual/seq2.litmus.expected index 329b8452..34cb0535 100644 --- a/tests/popl15/manual/seq2.litmus.expected +++ b/tests/popl15/manual/seq2.litmus.expected @@ -1,11 +1,10 @@ Test seq2 Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; -[a]=1; [x]=1; [y]=1; -Ok +No Witnesses -Positive: 1 Negative: 1 +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [x]=1 /\ [y]=1) -Observation seq2 Sometimes 1 1 +Observation seq2 Never 0 1 Hash=e37262f71f5106920e496da6fd1dee2a diff --git a/tests/popl15/manual/strengthen.litmus.expected b/tests/popl15/manual/strengthen.litmus.expected index 00df6915..5ad598ac 100644 --- a/tests/popl15/manual/strengthen.litmus.expected +++ b/tests/popl15/manual/strengthen.litmus.expected @@ -1,12 +1,10 @@ Test strengthen Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; [z]=1; -[a]=1; [x]=1; [y]=1; [z]=1; -Undef +No Witnesses -Positive: 2 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [z]=1 /\ [x]=1 /\ [y]=1) -Observation strengthen Sometimes 2 1 +Observation strengthen Never 0 1 Hash=936f17c1670a38b94c845fd21682daa3 diff --git a/tests/popl15/manual/strengthen2.litmus.expected b/tests/popl15/manual/strengthen2.litmus.expected index 96592fe9..60cb71f4 100644 --- a/tests/popl15/manual/strengthen2.litmus.expected +++ b/tests/popl15/manual/strengthen2.litmus.expected @@ -1,12 +1,10 @@ Test strengthen2 Allowed -States 2 +States 1 [a]=1; [x]=0; [y]=0; [z]=1; -[a]=1; [x]=1; [y]=1; [z]=1; -Undef +No Witnesses -Positive: 2 Negative: 1 -Flag *undef* +Positive: 0 Negative: 1 Condition exists ([a]=1 /\ [z]=1 /\ [x]=1 /\ [y]=1) -Observation strengthen2 Sometimes 2 1 +Observation strengthen2 Never 0 1 Hash=6d27da9e3c6dcde00c4db99dd97e6e43