** Step 0 ** Testing: {[Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], Rfe, ACSyncdRW, ABCSyncdRW, ACSyncdRR, ACLwSyncdRW, ABCLwSyncdRW, ACLwSyncdRR, PodWW, PodWR, PodRW, PodRR, SyncdWW, BCSyncdWW, SyncdWR, SyncdRW, BCSyncdRW, SyncdRR, LwSyncdWW, BCLwSyncdWW, LwSyncdWR, LwSyncdRW, BCLwSyncdRW, LwSyncdRR, ISyncdWW, ISyncdWR, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR} Relaxed: {} Safe : {Fre, Wse} Phase 1 in A (34 tests) Actually tested: {[Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], ACSyncdRW, ACSyncdRR, ACLwSyncdRW, ACLwSyncdRR, PodWW, PodWR, SyncdWW, SyncdWR, LwSyncdWW, LwSyncdWR, ISyncdWW, ISyncdWR} Added relax: {[Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], PodWW, PodWR, LwSyncdWR, ISyncdWW, ISyncdWR} Added safe: {ACSyncdRW, ACSyncdRR, ACLwSyncdRW, ACLwSyncdRR, SyncdWW, SyncdWR, LwSyncdWW} Phase 2 in B (99 tests) Removed safe: {ACLwSyncdRR} Added relax: {ACLwSyncdRR} ** Step 1 ** Testing: {Rfe, ABCSyncdRW, ABCLwSyncdRW, PodRW, PodRR, BCSyncdWW, SyncdRW, BCSyncdRW, SyncdRR, BCLwSyncdWW, LwSyncdRW, BCLwSyncdRW, LwSyncdRR, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR} Relaxed: {[Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], ACLwSyncdRR, PodWW, PodWR, LwSyncdWR, ISyncdWW, ISyncdWR} Safe : {ACSyncdRW, ACSyncdRR, ACLwSyncdRW, Fre, Wse, SyncdWW, SyncdWR, LwSyncdWW} Phase 1 in C (1021 tests) Actually tested: {Rfe, ABCSyncdRW, ABCLwSyncdRW, PodRW, PodRR, BCSyncdWW, BCLwSyncdWW, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR} Added safe: {Rfe, ABCSyncdRW, ABCLwSyncdRW, PodRW, PodRR, BCSyncdWW, BCLwSyncdWW, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR} Phase 2 in D (8090 tests) Removed safe: {Rfe, BCLwSyncdWW} Added relax: {Rfe, BCLwSyncdWW} ** Step 2 ** Testing: {SyncdRW, BCSyncdRW, SyncdRR, LwSyncdRW, BCLwSyncdRW, LwSyncdRR} Relaxed: {[Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], Rfe, ACLwSyncdRR, PodWW, PodWR, BCLwSyncdWW, LwSyncdWR, ISyncdWW, ISyncdWR} Safe : {ACSyncdRW, ABCSyncdRW, ACSyncdRR, ACLwSyncdRW, ABCLwSyncdRW, Fre, Wse, PodRW, PodRR, SyncdWW, BCSyncdWW, SyncdWR, LwSyncdWW, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR} Phase 1 in E (0 tests) Phase 2 in F (834 tests) ** Step 3 ** Testing: {SyncdRW, BCSyncdRW, SyncdRR, LwSyncdRW, BCLwSyncdRW, LwSyncdRR} Relaxed: {[Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], Rfe, ACLwSyncdRR, PodWW, PodWR, BCLwSyncdWW, LwSyncdWR, ISyncdWW, ISyncdWR} Safe : {ACSyncdRW, ABCSyncdRW, ACSyncdRR, ACLwSyncdRW, ABCLwSyncdRW, Fre, Wse, PodRW, PodRR, SyncdWW, BCSyncdWW, SyncdWR, LwSyncdWW, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR} Phase 1 in E (0 tests) Phase 2 in F (834 tests) ** Step 4 ** Testing: {SyncdRW, BCSyncdRW, SyncdRR, LwSyncdRW, BCLwSyncdRW, LwSyncdRR} Relaxed: {[Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], Rfe, ACLwSyncdRR, PodWW, PodWR, BCLwSyncdWW, LwSyncdWR, ISyncdWW, ISyncdWR} Safe : {ACSyncdRW, ABCSyncdRW, ACSyncdRR, ACLwSyncdRW, ABCLwSyncdRW, Fre, Wse, PodRW, PodRR, SyncdWW, BCSyncdWW, SyncdWR, LwSyncdWW, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR} Phase 1 in E (0 tests) Phase 2 in F (834 tests) ** Step 5 ** Testing: {SyncdRW, BCSyncdRW, SyncdRR, LwSyncdRW, BCLwSyncdRW, LwSyncdRR} Relaxed: {[Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], Rfe, ACLwSyncdRR, PodWW, PodWR, BCLwSyncdWW, LwSyncdWR, ISyncdWW, ISyncdWR} Safe : {ACSyncdRW, ABCSyncdRW, ACSyncdRR, ACLwSyncdRW, ABCLwSyncdRW, Fre, Wse, PodRW, PodRR, SyncdWW, BCSyncdWW, SyncdWR, LwSyncdWW, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR} Phase 1 in E (0 tests) Phase 2 in F (834 tests) ** Step 6 ** Testing: {SyncdRW, BCSyncdRW, SyncdRR, LwSyncdRW, BCLwSyncdRW, LwSyncdRR} Relaxed: {[Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], Rfe, ACLwSyncdRR, PodWW, PodWR, BCLwSyncdWW, LwSyncdWR, ISyncdWW, ISyncdWR} Safe : {ACSyncdRW, ABCSyncdRW, ACSyncdRR, ACLwSyncdRW, ABCLwSyncdRW, Fre, Wse, PodRW, PodRR, SyncdWW, BCSyncdWW, SyncdWR, LwSyncdWW, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR} Phase 1 in E (0 tests) Phase 2 in F (834 tests) Previous run answer is: all ++ Witness(es) for relaxed [Rfi,DpAddrdR] ++ A000: 'Rfi DpAddrdR Fre Rfi DpAddrdR Fre' {[Rfi,DpAddrdR], Fre} A001: 'Rfi DpAddrdR Fre Rfi DpAddrdR Fre Rfi DpAddrdR Fre' {[Rfi,DpAddrdR], Fre} A002: 'Rfi DpAddrdR Fre Rfi DpAddrdR Fre Rfi DpAddrdR Fre Rfi DpAddrdR Fre' {[Rfi,DpAddrdR], Fre} ++++++++ ++ Witness(es) for relaxed [Rfi,DpCtrlIsyncdR] ++ A003: 'Rfi DpCtrlIsyncdR Fre Rfi DpCtrlIsyncdR Fre' {[Rfi,DpCtrlIsyncdR], Fre} A004: 'Rfi DpCtrlIsyncdR Fre Rfi DpCtrlIsyncdR Fre Rfi DpCtrlIsyncdR Fre' {[Rfi,DpCtrlIsyncdR], Fre} A005: 'Rfi DpCtrlIsyncdR Fre Rfi DpCtrlIsyncdR Fre Rfi DpCtrlIsyncdR Fre Rfi DpCtrlIsyncdR Fre' {[Rfi,DpCtrlIsyncdR], Fre} ++++++++ ++ Witness(es) for relaxed Rfe ++ C075: 'Rfe DpAddrdR Fre Rfe DpAddrdR Fre' {Rfe, Fre, DpAddrdR} D523: 'Rfe DpAddrdR Fre Rfe DpDatadW Wsi' {Rfe, Fre, DpAddrdR, [DpDatadW,Wsi]} D505: 'Rfe DpAddrdR Fri Rfe DpAddrdR Fre' {Rfe, Fre, DpAddrdR, [DpAddrdR,Fri]} D734: 'Rfe DpAddrdR Fri Rfe DpCtrlIsyncdR Fre' {Rfe, Fre, [DpAddrdR,Fri], DpCtrlIsyncdR} D620: 'Rfe DpAddrdR Fri Rfe DpCtrldR Fre' {Rfe, Fre, [DpAddrdR,Fri], DpCtrldR} D1741: 'Rfe DpAddrdR Fri Rfe DpCtrldW Wse' {Rfe, Wse, [DpAddrdR,Fri], DpCtrldW} C028: 'Rfe DpAddrdW Rfe DpAddrdW Wse' {Rfe, Wse, DpAddrdW} D602: 'Rfe DpAddrdW Rfe DpCtrldR Fre' {Rfe, Fre, DpAddrdW, DpCtrldR} D1131: 'Rfe DpAddrdW Rfe DpCtrldR Fre SyncdWW Wse' {Rfe, Fre, Wse, SyncdWW, DpAddrdW, DpCtrldR} D764: 'Rfe DpAddrdW Rfe DpCtrldW Rfe DpCtrlIsyncdR Fre' {Rfe, Fre, DpAddrdW, DpCtrldW, DpCtrlIsyncdR} D1723: 'Rfe DpAddrdW Rfe DpCtrldW Wse' {Rfe, Wse, DpAddrdW, DpCtrldW} D1618: 'Rfe DpAddrdW Rfe DpDatadW Wse Rfe DpAddrdW Wsi' {Rfe, Wse, DpAddrdW, [DpAddrdW,Wsi], DpDatadW} D1344: 'Rfe DpAddrdW Wse LwSyncdWW Wse' {Rfe, Wse, LwSyncdWW, DpAddrdW} D466: 'Rfe DpAddrdW Wse Rfe DpAddrdR Fre' {Rfe, Fre, Wse, DpAddrdW, DpAddrdR} D1531: 'Rfe DpAddrdW Wse Rfe DpDatadW' {Rfe, Wse, DpAddrdW, DpDatadW} D725: 'Rfe DpAddrdW Wsi Rfe DpCtrlIsyncdR Fre' {Rfe, Fre, [DpAddrdW,Wsi], DpCtrlIsyncdR} D1281: 'Rfe DpCtrlIsyncdR Fre LwSyncdWW Wse' {Rfe, Fre, Wse, LwSyncdWW, DpCtrlIsyncdR} C077: 'Rfe DpCtrlIsyncdR Fre Rfe DpCtrlIsyncdR Fre' {Rfe, Fre, DpCtrlIsyncdR} D254: 'Rfe DpCtrlIsyncdR Fre SyncdWR Fre' {Rfe, Fre, SyncdWR, DpCtrlIsyncdR} C268: 'Rfe DpCtrldR Fre LwSyncdWW Wse' {Rfe, Fre, Wse, LwSyncdWW, DpCtrldR} D245: 'Rfe DpCtrldR Fre SyncdWR Fre' {Rfe, Fre, SyncdWR, DpCtrldR} D761: 'Rfe DpCtrldW Rfe DpCtrlIsyncdR Fre' {Rfe, Fre, DpCtrldW, DpCtrlIsyncdR} D647: 'Rfe DpCtrldW Rfe DpCtrldR Fre' {Rfe, Fre, DpCtrldW, DpCtrldR} C068: 'Rfe DpCtrldW Rfe DpCtrldW Wse' {Rfe, Wse, DpCtrldW} C292: 'Rfe DpCtrldW Wse LwSyncdWW Wse' {Rfe, Wse, LwSyncdWW, DpCtrldW} D335: 'Rfe DpCtrldW Wse SyncdWR Fre' {Rfe, Fre, Wse, SyncdWR, DpCtrldW} D1218: 'Rfe DpCtrldW Wse SyncdWW Wse' {Rfe, Wse, SyncdWW, DpCtrldW} D629: 'Rfe DpDatadW Rfe DpCtrldR Fre' {Rfe, Fre, DpDatadW, DpCtrldR} D637: 'Rfe DpDatadW Rfe DpCtrldR Fre Rfe DpCtrldW' {Rfe, Fre, DpDatadW, DpCtrldW, DpCtrldR} D251: 'Rfe DpDatadW Rfe DpCtrldR Fre SyncdWR Fre' {Rfe, Fre, SyncdWR, DpDatadW, DpCtrldR} C051: 'Rfe DpDatadW Rfe DpDatadW Wse' {Rfe, Wse, DpDatadW} C050: 'Rfe DpDatadW Rfe DpDatadW Wse SyncdWR Fre' {Rfe, Fre, Wse, SyncdWR, DpDatadW} C054: 'Rfe DpDatadW Rfe DpDatadW Wse SyncdWW Wse' {Rfe, Wse, SyncdWW, DpDatadW} D638: 'Rfe DpDatadW Wsi Rfe DpCtrldR Fre' {Rfe, Fre, [DpDatadW,Wsi], DpCtrldR} C266: 'Rfe ISyncdRR Fre LwSyncdWW Wse' {Rfe, Fre, Wse, LwSyncdWW, ISyncdRR} D389: 'Rfe ISyncdRR Fre Rfe DpAddrdR Fri' {Rfe, Fre, ISyncdRR, [DpAddrdR,Fri]} D376: 'Rfe ISyncdRR Fre Rfe DpAddrdR Fri Rfe DpAddrdW' {Rfe, Fre, ISyncdRR, DpAddrdW, [DpAddrdR,Fri]} D371: 'Rfe ISyncdRR Fre Rfe DpAddrdW' {Rfe, Fre, ISyncdRR, DpAddrdW} D380: 'Rfe ISyncdRR Fre Rfe DpAddrdW Wsi' {Rfe, Fre, ISyncdRR, [DpAddrdW,Wsi]} D416: 'Rfe ISyncdRR Fre Rfe DpCtrldW' {Rfe, Fre, ISyncdRR, DpCtrldW} D424: 'Rfe ISyncdRR Fre Rfe DpCtrldW Rfe DpCtrldW' {Rfe, Fre, ISyncdRR, DpCtrldW} D351: 'Rfe ISyncdRR Fre Rfe DpDatadW Wse' {Rfe, Fre, Wse, ISyncdRR, DpDatadW} D407: 'Rfe ISyncdRR Fre Rfe DpDatadW Wsi' {Rfe, Fre, ISyncdRR, [DpDatadW,Wsi]} D478: 'Rfe ISyncdRW Rfe DpAddrdR Fre' {Rfe, Fre, ISyncdRW, DpAddrdR} D1734: 'Rfe ISyncdRW Rfe DpAddrdW Wsi Rfe DpCtrldW Wse' {Rfe, Wse, ISyncdRW, [DpAddrdW,Wsi], DpCtrldW} D707: 'Rfe ISyncdRW Rfe DpCtrlIsyncdR Fre' {Rfe, Fre, ISyncdRW, DpCtrlIsyncdR} D593: 'Rfe ISyncdRW Rfe DpCtrldR Fre' {Rfe, Fre, ISyncdRW, DpCtrldR} D1612: 'Rfe ISyncdRW Rfe DpDatadW Wse Rfe DpDatadW Wsi' {Rfe, Wse, ISyncdRW, DpDatadW, [DpDatadW,Wsi]} D362: 'Rfe ISyncdRW Rfe ISyncdRR Fre' {Rfe, Fre, ISyncdRW, ISyncdRR} D1443: 'Rfe ISyncdRW Wse Rfe DpAddrdR Fri Rfe DpCtrldW' {Rfe, Wse, ISyncdRW, [DpAddrdR,Fri], DpCtrldW} D1399: 'Rfe ISyncdRW Wse Rfe DpDatadW Rfe DpAddrdW' {Rfe, Wse, ISyncdRW, DpAddrdW, DpDatadW} C187: 'Rfe LwSyncdRW Wse Rfe DpAddrdR Fri' {Rfe, ACLwSyncdRW, Wse, [DpAddrdR,Fri]} D925: 'Rfe LwSyncdRW Wse Rfe DpAddrdW Wsi' {Rfe, ACLwSyncdRW, Wse, [DpAddrdW,Wsi]} D943: 'Rfe LwSyncdRW Wse Rfe DpDatadW' {Rfe, ACLwSyncdRW, Wse, DpDatadW} D909: 'Rfe LwSyncdRW Wse Rfe ISyncdRW Rfe ISyncdRW' {Rfe, ACLwSyncdRW, Wse, ISyncdRW} D128: 'Rfe PodRR Fre Rfe DpAddrdR Fri' {Rfe, Fre, PodRR, [DpAddrdR,Fri]} D110: 'Rfe PodRR Fre Rfe DpAddrdW' {Rfe, Fre, PodRR, DpAddrdW} D184: 'Rfe PodRR Fre Rfe DpCtrlIsyncdR Fre SyncdWW' {Rfe, Fre, PodRR, BCSyncdWW, DpCtrlIsyncdR} D137: 'Rfe PodRR Fre Rfe DpDatadW' {Rfe, Fre, PodRR, DpDatadW} D146: 'Rfe PodRR Fre Rfe DpDatadW Wsi' {Rfe, Fre, PodRR, [DpDatadW,Wsi]} D101: 'Rfe PodRR Fre Rfe ISyncdRW' {Rfe, Fre, PodRR, ISyncdRW} D1093: 'Rfe PodRR Fre SyncdWW Wse Rfe ISyncdRW' {Rfe, Fre, Wse, PodRR, SyncdWW, ISyncdRW} D469: 'Rfe PodRW Rfe DpAddrdR Fre' {Rfe, Fre, PodRW, DpAddrdR} D1724: 'Rfe PodRW Rfe DpAddrdW Rfe DpCtrldW Wse' {Rfe, Wse, PodRW, DpAddrdW, DpCtrldW} D584: 'Rfe PodRW Rfe DpCtrldR Fre' {Rfe, Fre, PodRW, DpCtrldR} D589: 'Rfe PodRW Rfe DpCtrldR Fre Rfe DpAddrdR Fri' {Rfe, Fre, PodRW, [DpAddrdR,Fri], DpCtrldR} D1711: 'Rfe PodRW Rfe DpCtrldW Wse Rfe DpDatadW' {Rfe, Wse, PodRW, DpDatadW, DpCtrldW} D1707: 'Rfe PodRW Rfe DpCtrldW Wse Rfe ISyncdRW' {Rfe, Wse, PodRW, ISyncdRW, DpCtrldW} D399: 'Rfe PodRW Rfe DpDatadW Rfe ISyncdRR Fre' {Rfe, Fre, PodRW, ISyncdRR, DpDatadW} D092: 'Rfe PodRW Rfe PodRR Fre' {Rfe, Fre, PodRW, PodRR} C004: 'Rfe PodRW Rfe PodRW Rfe SyncdRR Fre' {Rfe, ACSyncdRR, Fre, PodRW} C007: 'Rfe PodRW Rfe PodRW Rfe SyncdRW Wse' {Rfe, ACSyncdRW, Wse, PodRW} C006: 'Rfe PodRW Rfe PodRW Wse' {Rfe, Wse, PodRW} C288: 'Rfe PodRW Wse LwSyncdWW Wse' {Rfe, Wse, PodRW, LwSyncdWW} D1312: 'Rfe PodRW Wse LwSyncdWW Wse Rfe DpDatadW' {Rfe, Wse, PodRW, LwSyncdWW, DpDatadW} D984: 'Rfe PodRW Wse Rfe ISyncdRW' {Rfe, Wse, PodRW, ISyncdRW} C160: 'Rfe PodRW Wse Rfe PodRW Wse' {Rfe, Wse, PodRW} D1162: 'Rfe PodRW Wse SyncdWW Wse' {Rfe, Wse, PodRW, SyncdWW} C081: 'Rfe SyncdRR Fre Rfe DpAddrdW Wsi' {Rfe, ACSyncdRR, Fre, [DpAddrdW,Wsi]} C083: 'Rfe SyncdRR Fre Rfe DpDatadW' {Rfe, ACSyncdRR, Fre, DpDatadW} D079: 'Rfe SyncdRR Fre Rfe DpDatadW Rfe DpCtrldW' {Rfe, ACSyncdRR, Fre, DpDatadW, DpCtrldW} C049: 'Rfe SyncdRR Fre Rfe DpDatadW Rfe DpDatadW' {Rfe, ACSyncdRR, Fre, DpDatadW} C084: 'Rfe SyncdRR Fre Rfe DpDatadW Wsi' {Rfe, ACSyncdRR, Fre, [DpDatadW,Wsi]} C015: 'Rfe SyncdRR Fre Rfe ISyncdRW Rfe ISyncdRW' {Rfe, ACSyncdRR, Fre, ISyncdRW} D542: 'Rfe SyncdRW Rfe DpAddrdR Fre Rfe ISyncdRW' {Rfe, ABCSyncdRW, Fre, ISyncdRW, DpAddrdR} C167: 'Rfe SyncdRW Wse Rfe DpAddrdW' {Rfe, ACSyncdRW, Wse, DpAddrdW} C029: 'Rfe SyncdRW Wse Rfe DpAddrdW Rfe DpAddrdW' {Rfe, ACSyncdRW, Wse, DpAddrdW} C168: 'Rfe SyncdRW Wse Rfe DpAddrdW Wsi' {Rfe, ACSyncdRW, Wse, [DpAddrdW,Wsi]} D883: 'Rfe SyncdRW Wse Rfe DpAddrdW Wsi Rfe DpCtrldW' {Rfe, ACSyncdRW, Wse, [DpAddrdW,Wsi], DpCtrldW} C172: 'Rfe SyncdRW Wse Rfe DpCtrldW' {Rfe, ACSyncdRW, Wse, DpCtrldW} C060: 'Rfe SyncdRW Wse Rfe DpDatadW Wsi Rfe DpDatadW Wsi' {Rfe, ACSyncdRW, Wse, [DpDatadW,Wsi]} ++++++++ ++ Witness(es) for relaxed ACLwSyncdRR ++ B054: 'Rfe LwSyncdRR Fre LwSyncdWW Wse' {ACLwSyncdRR, Fre, Wse, LwSyncdWW} B050: 'Rfe LwSyncdRR Fre SyncdWW Wse' {ACLwSyncdRR, Fre, Wse, SyncdWW} ++++++++ ++ Witness(es) for relaxed PodWW ++ A010: 'Wse PodWW Wse PodWW' {Wse, PodWW} A011: 'Wse PodWW Wse PodWW Wse PodWW' {Wse, PodWW} A012: 'Wse PodWW Wse PodWW Wse PodWW Wse PodWW' {Wse, PodWW} ++++++++ ++ Witness(es) for relaxed PodWR ++ A013: 'Fre PodWR Fre PodWR' {Fre, PodWR} A014: 'Fre PodWR Fre PodWR Fre PodWR' {Fre, PodWR} A015: 'Fre PodWR Fre PodWR Fre PodWR Fre PodWR' {Fre, PodWR} ++++++++ ++ Witness(es) for relaxed BCLwSyncdWW ++ D7863: 'Rfe DpAddrdR Fre LwSyncdWW Wse LwSyncdWW' {Fre, Wse, LwSyncdWW, BCLwSyncdWW, DpAddrdR} D7735: 'Rfe DpAddrdR Fre LwSyncdWW Wse SyncdWR Fre LwSyncdWW' {Fre, Wse, SyncdWR, LwSyncdWW, BCLwSyncdWW, DpAddrdR} D7682: 'Rfe DpAddrdR Fre SyncdWR Fre LwSyncdWW' {Fre, SyncdWR, BCLwSyncdWW, DpAddrdR} D7694: 'Rfe DpCtrlIsyncdR Fre SyncdWR Fre LwSyncdWW' {Fre, SyncdWR, BCLwSyncdWW, DpCtrlIsyncdR} D7896: 'Rfe DpCtrldR Fre LwSyncdWW Rfe DpCtrldR Fre LwSyncdWW' {Fre, BCLwSyncdWW, DpCtrldR} D7688: 'Rfe DpCtrldR Fre SyncdWR Fre LwSyncdWW' {Fre, SyncdWR, BCLwSyncdWW, DpCtrldR} D7901: 'Rfe DpCtrldR Fre SyncdWW Wse LwSyncdWW' {Fre, Wse, SyncdWW, BCLwSyncdWW, DpCtrldR} D7810: 'Rfe ISyncdRR Fre LwSyncdWW Rfe DpCtrldR Fre LwSyncdWW' {Fre, BCLwSyncdWW, ISyncdRR, DpCtrldR} D7806: 'Rfe ISyncdRR Fre LwSyncdWW Rfe ISyncdRR Fre LwSyncdWW' {Fre, BCLwSyncdWW, ISyncdRR} C968: 'Rfe ISyncdRR Fre LwSyncdWW Wse LwSyncdWW' {Fre, Wse, LwSyncdWW, BCLwSyncdWW, ISyncdRR} D7676: 'Rfe ISyncdRR Fre SyncdWR Fre LwSyncdWW' {Fre, SyncdWR, BCLwSyncdWW, ISyncdRR} D7623: 'Rfe PodRR Fre LwSyncdWW Rfe DpCtrldR Fre LwSyncdWW' {Fre, PodRR, BCLwSyncdWW, DpCtrldR} C577: 'Rfe PodRR Fre LwSyncdWW Wse LwSyncdWW' {Fre, Wse, PodRR, LwSyncdWW, BCLwSyncdWW} D7126: 'Rfe PodRR Fre Rfe SyncdRR Fre LwSyncdWW' {ACSyncdRR, Fre, PodRR, BCLwSyncdWW} C571: 'Rfe PodRR Fre Rfe SyncdRW Wse LwSyncdWW' {ACSyncdRW, Fre, Wse, PodRR, BCLwSyncdWW} C567: 'Rfe PodRR Fre SyncdWR Fre LwSyncdWW' {Fre, PodRR, SyncdWR, BCLwSyncdWW} C573: 'Rfe PodRR Fre SyncdWW Wse LwSyncdWW' {Fre, Wse, PodRR, SyncdWW, BCLwSyncdWW} D7132: 'Rfe SyncdRR Fre LwSyncdWW Rfe ISyncdRR Fre' {ACSyncdRR, Fre, BCLwSyncdWW, ISyncdRR} C895: 'Rfe SyncdRW Wse LwSyncdWW Rfe DpCtrlIsyncdR Fre' {ACSyncdRW, Fre, Wse, BCLwSyncdWW, DpCtrlIsyncdR} D6697: 'Rfe SyncdRW Wse LwSyncdWW Rfe DpCtrldR Fre' {ACSyncdRW, Fre, Wse, BCLwSyncdWW, DpCtrldR} D6693: 'Rfe SyncdRW Wse LwSyncdWW Rfe ISyncdRR Fre' {ACSyncdRW, Fre, Wse, BCLwSyncdWW, ISyncdRR} ++++++++ ++ Witness(es) for relaxed LwSyncdWR ++ A025: 'Fre LwSyncdWR Fre LwSyncdWR' {Fre, LwSyncdWR} A026: 'Fre LwSyncdWR Fre LwSyncdWR Fre LwSyncdWR' {Fre, LwSyncdWR} A027: 'Fre LwSyncdWR Fre LwSyncdWR Fre LwSyncdWR Fre LwSyncdWR' {Fre, LwSyncdWR} ++++++++ ++ Witness(es) for relaxed ISyncdWW ++ A028: 'Wse ISyncdWW Wse ISyncdWW' {Wse, ISyncdWW} A029: 'Wse ISyncdWW Wse ISyncdWW Wse ISyncdWW' {Wse, ISyncdWW} A030: 'Wse ISyncdWW Wse ISyncdWW Wse ISyncdWW Wse ISyncdWW' {Wse, ISyncdWW} ++++++++ ++ Witness(es) for relaxed ISyncdWR ++ A031: 'Fre ISyncdWR Fre ISyncdWR' {Fre, ISyncdWR} A032: 'Fre ISyncdWR Fre ISyncdWR Fre ISyncdWR' {Fre, ISyncdWR} A033: 'Fre ISyncdWR Fre ISyncdWR Fre ISyncdWR Fre ISyncdWR' {Fre, ISyncdWR} ++++++++ Observed relaxed: {Rfi, [Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], Rfe, ACLwSyncdRR, PodWW, PodWR, BCLwSyncdWW, LwSyncdWR, ISyncdWW, ISyncdWR} Observed safe: {ACSyncdRW, ABCSyncdRW, ACSyncdRR, ACLwSyncdRW, ABCLwSyncdRW, Fri, Fre, Wsi, Wse, PodRW, PodRR, SyncdWW, BCSyncdWW, SyncdWR, SyncdRW, BCSyncdRW, SyncdRR, LwSyncdWW, LwSyncdRW, BCLwSyncdRW, LwSyncdRR, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR} ** Now checking safe set conformance ** ** Step 7 ** Phase 2 in G (1737 tests) ** Step 8 ** Phase 2 in G (1737 tests) ** Step 9 ** Phase 2 in G (1737 tests) ** Step 10 ** Phase 2 in G (1737 tests) ** Step 11 ** Phase 2 in G (1737 tests) ** Step 12 ** Observed relaxed: {Rfi, [Rfi,DpAddrdR], [Rfi,DpCtrlIsyncdR], Rfe, ACLwSyncdRR, PodWW, PodWR, BCLwSyncdWW, LwSyncdWR, ISyncdWW, ISyncdWR} Observed safe: {ACSyncdRW, ABCSyncdRW, ACSyncdRR, ACLwSyncdRW, ABCLwSyncdRW, Fri, Fre, Wsi, Wse, PodRW, PodRR, SyncdWW, BCSyncdWW, SyncdWR, SyncdRW, BCSyncdRW, SyncdRR, LwSyncdWW, LwSyncdRW, BCLwSyncdRW, LwSyncdRR, ISyncdRW, ISyncdRR, DpAddrdW, [DpAddrdW,Wsi], DpAddrdR, [DpAddrdR,Fri], DpDatadW, [DpDatadW,Wsi], DpCtrldW, DpCtrldR, DpCtrlIsyncdR}