Model: Path: . URL: svn+ssh://secsvn@svn-sem.cl.cam.ac.uk/WeakMemory/ppc-abstract-machine Repository Root: svn+ssh://secsvn@svn-sem.cl.cam.ac.uk Repository UUID: 0227817e-5e02-0410-83b2-89653b220fac Revision: 8605 Node Kind: directory Schedule: normal Last Changed Author: so294 Last Changed Rev: 8603 Last Changed Date: 2011-11-02 17:20:48 +0000 (Wed, 02 Nov 2011) Name: MachineDefUtils.lem Revision: 8605 Last Changed Author: so294 Last Changed Rev: 8345 Last Changed Date: 2011-08-05 12:52:50 +0100 (Fri, 05 Aug 2011) Text Last Updated: 2011-08-23 12:47:53 +0100 (Tue, 23 Aug 2011) Checksum: 093f06a9a327d1379cf23078896b7b72 Name: MachineDefFreshIds.lem Revision: 8605 Last Changed Author: pes20 Last Changed Rev: 8251 Last Changed Date: 2011-07-01 16:14:46 +0100 (Fri, 01 Jul 2011) Text Last Updated: 2011-08-23 12:47:53 +0100 (Tue, 23 Aug 2011) Checksum: 987ca7ba14acfe76c1ab8236371977f8 Name: MachineDefValue.lem Revision: 8605 Last Changed Author: so294 Last Changed Rev: 8345 Last Changed Date: 2011-08-05 12:52:50 +0100 (Fri, 05 Aug 2011) Text Last Updated: 2011-08-23 12:47:53 +0100 (Tue, 23 Aug 2011) Checksum: 3f0dc34931d5785c77ca202b8a0bcab1 Name: MachineDefTypes.lem Revision: 8605 Last Changed Author: ss726 Last Changed Rev: 8513 Last Changed Date: 2011-10-24 14:31:45 +0100 (Mon, 24 Oct 2011) Text Last Updated: 2011-10-26 22:50:20 +0100 (Wed, 26 Oct 2011) Checksum: dc9de17cd636781e731bd039b23b6441 Name: MachineDefInstructionSemantics.lem Revision: 8605 Last Changed Author: ss726 Last Changed Rev: 8512 Last Changed Date: 2011-10-23 15:50:30 +0100 (Sun, 23 Oct 2011) Text Last Updated: 2011-10-23 15:49:24 +0100 (Sun, 23 Oct 2011) Checksum: 8e9df1b4be01131c894bbde643ececd9 Name: MachineDefStorageSubsystem.lem Revision: 8605 Last Changed Author: pes20 Last Changed Rev: 8514 Last Changed Date: 2011-10-24 14:37:42 +0100 (Mon, 24 Oct 2011) Text Last Updated: 2011-10-26 22:50:20 +0100 (Wed, 26 Oct 2011) Checksum: 09968a0e2edaf045ea53f988caaaf1d1 Name: MachineDefThreadSubsystem.lem Revision: 8605 Last Changed Author: so294 Last Changed Rev: 8603 Last Changed Date: 2011-11-02 17:20:48 +0000 (Wed, 02 Nov 2011) Text Last Updated: 2011-11-02 23:39:52 +0000 (Wed, 02 Nov 2011) Checksum: 3c43a04bc59bbcf978107cba1124a613 Name: MachineDefSystem.lem Revision: 8605 Last Changed Author: pes20 Last Changed Rev: 8507 Last Changed Date: 2011-10-23 11:29:38 +0100 (Sun, 23 Oct 2011) Text Last Updated: 2011-10-23 12:34:37 +0100 (Sun, 23 Oct 2011) Checksum: 11c9e6d828a90b062a9d877e1d14fa58 Lem run: Thu Nov 3 15:20:19 GMT 2011 -e Revision: 6 Last Changed Author: ss726 Last Changed Rev: 6 Last Changed Date: 2011-05-12 15:02:21 +0200 (Thu, 12 May 2011) M src/version.ml Build: Thu May 19 11:29:12 CEST 2011 -e -e Trying LB+addrs \iN{LB+addrs} LOC: [x]LOC: [y]LOC: [z]TOP init write ids <1000:1000>W x 0,<1000:1000>W y 0,<1000:1000>W z 0 Found 1 : Prune count= 0 seen_succs= 18 19 states Found 2 : Prune count= 1 seen_succs= 23 24 states Found 3 : Prune count= 25 seen_succs= 46 47 states Found 4 : Prune count= 35 seen_succs= 59 60 states Found 5 : Prune count= 36 seen_succs= 64 65 states Found 6 : Prune count= 41 seen_succs= 73 74 states Found 7 : Prune count= 42 seen_succs= 77 78 states Found 8 : Prune count= 116 seen_succs= 129 130 states Found 9 : Prune count= 120 seen_succs= 135 136 states Found 10 : Prune count= 429 seen_succs= 298 299 states Found 11 : Prune count= 430 seen_succs= 303 304 states Found 12 : Prune count= 454 seen_succs= 326 327 states Found 13 : Prune count= 463 seen_succs= 339 340 states Found 14 : Prune count= 464 seen_succs= 344 345 states Found 15 : Prune count= 470 seen_succs= 353 354 states Found 16 : Prune count= 471 seen_succs= 357 358 states Found 17 : Prune count= 545 seen_succs= 409 410 states Found 18 : Prune count= 548 seen_succs= 415 416 states Found 19 : Prune count= 858 seen_succs= 578 579 states Found 20 : Prune count= 860 seen_succs= 583 584 states Found 21 : Prune count= 879 seen_succs= 602 603 states Found 22 : Prune count= 880 seen_succs= 607 608 states Found 23 : Prune count= 1758 seen_succs= 1035 1036 states Found 24 : Prune count= 1759 seen_succs= 1040 1041 states Found 25 : Prune count= 1783 seen_succs= 1063 1064 states Found 26 : Prune count= 1817 seen_succs= 1097 1098 states Found 27 : Prune count= 2012 seen_succs= 1213 1214 states Found 28 : Prune count= 2028 seen_succs= 1235 1236 states Found 29 : Prune count= 2031 seen_succs= 1242 1243 states Found 30 : Prune count= 2768 seen_succs= 1591 1592 states Found 31 : Prune count= 2770 seen_succs= 1596 1597 states Found 32 : Prune count= 2789 seen_succs= 1615 1616 states Found 33 : Prune count= 2790 seen_succs= 1620 1621 states Test LB+addrs Allowed States 3 0:r1=0; 1:r1=0; 0:r1=0; 1:r1=1; 0:r1=1; 1:r1=0; No (allowed not found) Condition exists (0:r1=1 /\ 1:r1=1) Hash=eeec3489170ccce04d88173ca1bf6df8 Observation LB+addrs Never 0 3