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 MP+lwsync+addr \iN{MP+lwsync+addr}
LOC: [x]LOC: [y]TOP init write ids <1000:1000>W x 0,<1000:1000>W y 0
Found      1 : Prune count=     0  seen_succs=    19     20 states 
Found      2 : Prune count=    17  seen_succs=    42     43 states 
Found      3 : Prune count=    24  seen_succs=    55     56 states 
Found      4 : Prune count=    25  seen_succs=    60     61 states 
Found      5 : Prune count=   261  seen_succs=   207    208 states 
Found      6 : Prune count=   262  seen_succs=   212    213 states 
Found      7 : Prune count=   286  seen_succs=   235    236 states 
Found      8 : Prune count=   295  seen_succs=   248    249 states 
Found      9 : Prune count=   296  seen_succs=   253    254 states 
Found     10 : Prune count=   348  seen_succs=   295    296 states 
Found     11 : Prune count=   989  seen_succs=   637    638 states 
Found     12 : Prune count=   990  seen_succs=   642    643 states 
Found     13 : Prune count=  1014  seen_succs=   665    666 states 
Found     14 : Prune count=  1023  seen_succs=   678    679 states 
Found     15 : Prune count=  1024  seen_succs=   683    684 states 
Found     16 : Prune count=  1076  seen_succs=   725    726 states 
Found     17 : Prune count=  1887  seen_succs=  1134   1135 states 
Test MP+lwsync+addr Allowed
States 3
1:r1=0; 1:r4=0;
1:r1=0; 1:r4=1;
1:r1=1; 1:r4=1;
No (allowed not found)
Condition exists (1:r1=1 /\ 1:r4=0)
Hash=0c3a42ea89d14eb1fcf45b6f16e3b110
Observation MP+lwsync+addr Never 0 3