--- a/semantics/checker.pl	Thu Jan 31 17:03:10 2013 +0000
+++ b/semantics/checker.pl	Thu Jan 31 19:19:07 2013 +0000
@@ -6,15 +6,17 @@
 multimember(A,B,[A|L]) :- member(B,L).
 multimember(A,B,[_|L]) :- multimember(A,B,L).
 
-ensure(A,I,J) :- \+(member(A,I)),  J = [A|I].
+ensure(A,I,J) :- \+((member(B,I), A==B)),  J = [A|I].
 
 % helper for influence 15
 inferInfluence(Id,X,Y,Attrs1,I,J) :-
 	member(wasInfluencedBy(Id,X,Y,Attrs2),I)
-	-> (append(Attrs1,Attrs2,Attrs),
-	    remove(wasInfluencedBy(Id,X,Y,Attrs2),I,J1),
-	    J = [wasInfluencedBy(Id,X,Y,Attrs)|J1])
-	; J = [wasInfluencedBy(Id,X,Y,Attrs)|I].
+	-> (subset(Attrs1,Attrs2)
+	   -> fail
+	   ; (append(Attrs1,Attrs2,Attrs),
+	      remove(wasInfluencedBy(Id,X,Y,Attrs2),I,J1),
+	      J = [wasInfluencedBy(Id,X,Y,Attrs)|J1]))
+	; J = [wasInfluencedBy(Id,X,Y,Attrs1)|I].
 
 
 
@@ -61,12 +63,12 @@
               J = [wasGeneratedBy(_,E1,A1,_,[])|I].
 
 % inference 11a
-infer(I,J) :- member(wasDerivedFrom(_ID,E1,_E2,A,Gen2,Use1,_Attrs),I),
+infer(I,J) :- member(wasDerivedFrom(_ID,_E2,E1,A,Gen2,Use1,_Attrs),I),
 	      A \== null, Gen2 \== null, Use1 \== null,
               \+(member(used(Use1,A,E1,_,_),I)),
               J = [used(Use1,A,E1,_,[])|I].
 % inference 11b
-infer(I,J) :- member(wasDerivedFrom(_ID,_E1,E2,A,Gen2,Use1,_Attrs),I),
+infer(I,J) :- member(wasDerivedFrom(_ID,E2,_E1,A,Gen2,Use1,_Attrs),I),
 	      A \== null, Gen2 \== null, Use1 \== null,
               \+(member(wasGeneratedBy(Gen2,E2,A,_,_),I)),
               J = [wasGeneratedBy(Gen2,E2,A,_,[])|I].
@@ -207,7 +209,7 @@
 	  remove(activity(ID2,ST2,ET2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [activity(ID1,ST1,ET1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 
 % Constraint 22.3: key constraint: agent
@@ -230,7 +232,7 @@
 	  remove(wasGeneratedBy(ID2,E2,A2,T2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [wasGeneratedBy(ID1,E1,A1,T1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 % Constraint 23.2: 
 infer(I,J) :- multimember(used(ID1,A1,E1,T1,Attrs1),
@@ -243,7 +245,7 @@
 	  remove(used(ID2,A2,E2,T2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [used(ID1,A1,E1,T1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 % Constraint 23.3: 
 infer(I,J) :- multimember(wasInformedBy(ID1,A12,A11,Attrs1),
@@ -256,7 +258,7 @@
 	  remove(wasInformedBy(ID2,A22,A21,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [wasInformedBy(ID1,A12,A11,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 % Constraint 23.4: 
 infer(I,J) :- multimember(wasStartedBy(ID1,A12,E1,A11,T1,Attrs1),
@@ -269,7 +271,7 @@
 	  remove(wasStartedBy(ID2,A22,E2,A21,T2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [wasStartedBy(ID1,A12,E1,A11,T1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 % Constraint 23.5: 
 infer(I,J) :- multimember(wasEndedBy(ID1,A12,E1,A11,T1,Attrs1),
@@ -282,7 +284,7 @@
 	  remove(wasEndedBy(ID2,A22,E2,A21,T2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [wasEndedBy(ID1,A12,E1,A11,T1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 % Constraint 23.6: 
 infer(I,J) :- multimember(wasInvalidatedBy(ID1,E1,A1,T1,Attrs1),
@@ -295,7 +297,7 @@
 	  remove(wasInvalidatedBy(ID2,E2,A2,T2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [wasInvalidatedBy(ID1,E1,A1,T1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 % Constraint 23.7: 
 infer(I,J) :- multimember(wasDerivedFrom(ID1,E12,E11,A1,G1,U1,Attrs1),
@@ -308,7 +310,7 @@
 	  remove(wasDerivedFrom(ID2,E22,E21,A2,G2,U2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [wasDerivedFrom(ID1,E12,E11,A1,G1,U1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 % Constraint 23.8:
 infer(I,J) :- multimember(wasAttributedTo(ID1,E1,Ag1,Attrs1),
@@ -321,7 +323,7 @@
 	  remove(wasAttributedTo(ID2,E2,Ag2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [wasAttributedTo(ID1,E1,Ag1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 % Constraint 23.9:
 infer(I,J) :- multimember(wasAssociatedWith(ID1,A1,Ag1,Pl1,Attrs1),
@@ -334,7 +336,7 @@
 	  remove(wasAssociatedWith(ID2,A2,Ag2,Pl2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [wasAssociatedWith(ID1,A1,Ag1,Pl1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 % Constraint 23.10:
 infer(I,J) :- multimember(actedOnBehalfOf(ID1,Ag12,Ag11,A1,Attrs1),
@@ -347,7 +349,7 @@
 	  remove(actedOnBehalfOf(ID2,Ag22,Ag21,A2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [actedOnBehalfOf(ID1,Ag12,Ag11,A1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 % Constraint 23.11:
 infer(I,J) :- multimember(wasInfluencedBy(ID1,Y1,X1,Attrs1),
@@ -360,7 +362,7 @@
 	  remove(wasInfluencedBy(ID2,Y2,X2,Attrs2),J1,J2),
 	  append(Attrs1,Attrs2,Attrs),
 	  J = [wasInfluencedBy(ID1,Y1,X1,Attrs)|J2])
-	; J = invalid).
+	; J = invalid(I)).
 
 
 
@@ -372,7 +374,7 @@
 	A1 == A2,
 	((Gen1 = Gen2)
 	-> (J = I) % And the ids unify, then done.  Key constraint will do the rest.
-	; J = invalid).	% Otherwise invalid.
+	; J = invalid(I)).	% Otherwise invalid.
 
 % Constraint 25: unique-invalidation
 infer(I,J) :- multimember(wasInvalidatedBy(Inv1,E1,A1,_T1,_Attrs1),
@@ -381,7 +383,7 @@
 	A1 == A2,
 	((Inv1 = Inv2)
 	-> (J = I) % And the ids unify, then done.  Key constraint will do the rest.
-	; J = invalid).	% Otherwise invalid.
+	; J = invalid(I)).	% Otherwise invalid.
 
 
 % Constraint 26: unique-wasStartedBy
@@ -391,7 +393,7 @@
 	A11 == A12,
 	((ID1 = ID2)
 	-> (J = I) % And the ids unify, then done.  Key constraint will do the rest.
-	; J = invalid).	% Otherwise invalid.
+	; J = invalid(I)).	% Otherwise invalid.
 
 % Constraint 27: unique-wasEndedBy
 infer(I,J) :- multimember(wasEndedBy(ID1,A1,_E1,A11,_T1,_Attrs1),
@@ -400,7 +402,7 @@
 	A11 == A12,
 	((ID1 = ID2)
 	-> (J = I) % And the ids unify, then done.  Key constraint will do the rest.
-	; J = invalid).	% Otherwise invalid.
+	; J = invalid(I)).	% Otherwise invalid.
 
 % Constraint 28: unique-startTime
 infer(I,J) :- member(activity(A,T1,_T2,_Attrs),I),
@@ -409,7 +411,7 @@
               T1 \== T,
               ((T1=T) 
 	       -> (J = I)
-	       ; J = invalid).
+	       ; J = invalid(I)).
 
 % Constraint 29: unique-endTime
 infer(I,J) :- member(activity(A,_T1,T2,_Attrs),I),
@@ -418,16 +420,19 @@
               T2 \== T,
               ((T2=T) 
 	       -> (J = I)
-	       ; J = invalid).
+	       ; J = invalid(I)).
 
 normalize(I,I) :- \+(infer(I,_)), !.
 normalize(I,K) :- infer(I,J), !, normalize(J,K).
 
 
-constrain(P,O1,O2) :- \+(member(P,O1)),
-	O2 = [P|O1].
 
 
+%% From this point onward we can be more relaxed about uification because
+%% all the free variables have been frozen
+
+constrain(P,O1,O2) :- \+((member(P,O1))),
+	O2 = [P|O1].
 
 % Constraint 30
 ordering_step(I,O1,O2) :-
@@ -520,7 +525,7 @@
 	member(wasDerivedFrom(_ID, E2,E1,_A,_Gen,_Use,_Attrs),I),
 	member(wasGeneratedBy(Gen1, E1,_A1,_T1,_Attrs1),I),  
 	member(wasGeneratedBy(Gen2, E2,_A2,_T2,_Attrs2),I),  
-	constrain(precedes(Gen1,Gen2),O1,O2).
+	constrain(strictlyPrecedes(Gen1,Gen2),O1,O2).
 
 %Constraint 43.1
 ordering_step(I,O1,O2) :-
@@ -617,8 +622,28 @@
 	constrain(precedes(Start1,End2),O1,O2).
 
 
+% Find all existentially quantified vars and freeze them to fresh constants
 
-% TODO: Lots more ordering constraints following this pattern.
+fresh(A,I,J) :- J is I+1, atom_concat('fresh:id',I,A).
+
+freeze([],[]) --> [].
+freeze([T|L],[U|M]) --> freeze_term(T,U), freeze(L,M).
+
+freeze_term(T,U) --> {T =.. [Name|Args]},
+                     freeze_list(Args,Args2),
+		     {U =.. [Name|Args2]}.
+
+freeze_list([],[]) --> [].
+freeze_list([Attrs],[Attrs2]) --> {nonvar(Attrs),(Attrs=[]; Attrs=[_|_])},
+	freeze_attrs(Attrs,Attrs2).
+freeze_list([A|Xs],[B|Ys]) --> freeze_arg(A,B), freeze_list(Xs,Ys).
+
+freeze_arg(A,B) --> {atom(A),A=B}.
+freeze_arg(X,Y) --> {var(X)}, fresh(Y), {Y=X}.
+
+freeze_attrs([],[]) --> [].
+freeze_attrs([A=X|AXs],[A=Y|AYs]) --> freeze_arg(X,Y), freeze_attrs(AXs,AYs).
+
 
 ordering_saturate(I,O,O) :- \+(ordering_step(I,O,_)),!.
 ordering_saturate(I,O1,O3) :-
@@ -734,8 +759,7 @@
 
 % Constraint 50.14.
 typing_step(I) -->
-	{member(wasAssociatedWith(_Id,A,Ag,Pl,_Attrs),I),
-	 Pl == null},
+	{member(wasAssociatedWith(_Id,A,Ag,null,_Attrs),I)},
 	(ensure(typeOf(A,activity)) ;
 	 ensure(typeOf(Ag,agent)) ).
 
@@ -800,51 +824,49 @@
 relation(actedOnBehalfOf).
 
 % Constraint 51
-impos(I,_T) :- member(wasDerivedFrom(_Id,_E2,_E1,null,G,null,_Attrs),I),
-	G \== null.
-impos(I,_T) :- member(wasDerivedFrom(_Id,_E2,_E1,null,null,U,_Attrs),I),
-	U \== null.
-impos(I,_T) :- member(wasDerivedFrom(_Id,_E2,_E1,null,G,U,_Attrs),I),
-	G \== null, U \== null.
+impos(I,_T,c51_1) :- member(wasDerivedFrom(_Id,_E2,_E1,A,G,U,_Attrs),I),
+	A == null, G \== null, U == null.
+impos(I,_T,c51_2) :- member(wasDerivedFrom(_Id,_E2,_E1,A,G,U,_Attrs),I),
+	A == null, G == null, U \== null.
+impos(I,_T,c51_3) :- member(wasDerivedFrom(_Id,_E2,_E1,A,G,U,_Attrs),I),
+	A == null, G \== null, U \== null.
 
 
 
 % Constraint 52.  Have to be careful not to unify.
-impos(I,_T) :- member(specializationOf(E1,E2),I), E1 == E2.
+impos(I,_T,c52) :- member(specializationOf(E,E),I).
 
 % Constraint 53.  
-impos(I,_T) :- member(T1,I),
+impos(I,_T,c53) :- member(T1,I),
 	member(T2,I),
-	T1 =.. [R,Id1|_],
-	T2 =.. [S,Id2|_],
-	Id1 == Id2,
+	T1 =.. [R,Id|_],
+	T2 =.. [S,Id|_],
 	relation(R),
 	relation(S),
 	R \== S.
 
 %Constraint 54
-impos(I,_T) :- member(T1,I),
+impos(I,_T,c54) :- member(T1,I),
 	member(T2,I),
-	T1 =.. [P,Id1|_],
-	T2 =.. [R,Id2|_],
-	Id1 == Id2,
+	T1 =.. [P,Id|_],
+	T2 =.. [R,Id|_],
 	object(P),
 	relation(R).
 
 % Constraint 55
-impos(_I,T) :- member(typeOf(Id1,entity),T),
-	member(typeOf(Id2,activity),T),
-	Id1 == Id2.
+impos(_I,T,c55) :- member(typeOf(Id,entity),T),
+	member(typeOf(Id,activity),T).
 
 % Constraint 56
-impos(I,T) :- member(hadMember(C1,_E1),I),
-	member(typeOf(C2,'prov:EmptyCollection'),T),
-	C1 == C2.
+impos(I,T,c56) :- member(hadMember(C,_E1),I),
+	member(typeOf(C,'prov:EmptyCollection'),T).
 		     
 
-impos_check(I,T) :- \+(impos(I,T)).
+impos_check(I,T) :- \+(impos(I,T,_)).
 
 valid(I) :- normalize(I,J),
-	ordering_check(J),
+	J \= invalid(_),
+	freeze(J,K,0,_),
+	ordering_check(K),
 	typing(J,T),
 	impos_check(J,T).

--- a/semantics/prov_xml.pl	Thu Jan 31 17:03:10 2013 +0000
+++ b/semantics/prov_xml.pl	Thu Jan 31 19:19:07 2013 +0000
@@ -19,9 +19,10 @@
 % Read XML from Filename and
 % bind J to a list of Prolog terms like
 %  [activity('ex:a1',_,_,[]), ... ]
-provx_load(Filename,J):-
+provx_load(Filename,K):-
 	load_structure(Filename,X,[dialect(xmlns),space(remove)]),
-	provx(X,J).
+	provx(X,J),
+	postprocess(J,K).
 
 provx([],_).
 provx([element(Prov:document,_,Contents)|Elements],J):-
@@ -30,6 +31,9 @@
 	provx(Elements,J).
 
 provx_expressions([],[]):-!.
+
+% This doesn't handle the case of alternate and specialization correctly,
+% since they don't have an id or attributes
 provx_expressions([element(Prov:Name,Attrs,Contents)|Elements],[Expression|J]):-
 	ns(prov,Prov),
 	template(Name,TArgs),
@@ -62,6 +66,16 @@
 	% optional argument absent
 	!,
 	provx_args(TArgs,Elements,Args).
+provx_args([-Name|TArgs],[element(Prov:Name,Attrs,Contents)|Elements],[Value|Values]):-
+	% optional argument present
+	ns(prov,Prov),
+	!,
+	arg_value(Attrs,Contents,Value),
+	provx_args(TArgs,Elements,Values).
+provx_args([-_|TArgs],Elements,[null|Args]):-
+	% optional argument absent
+	!,
+	provx_args(TArgs,Elements,Args).
 provx_args(TArgs,Elements,_):-
 	write('Failing on args'),write(Elements),nl,
 	write('Expected '),write(TArgs),nl,
@@ -102,10 +116,30 @@
 template(wasEndedBy,[activity,+trigger,+ender,+time]).
 template(wasInvalidatedBy,[entity,+activity,+time]).
 
-template(wasDerivedFrom,[generatedEntity,usedEntity,+activity,+generation,+usage]).
+template(wasDerivedFrom,[generatedEntity,usedEntity,-activity,-generation,-usage]).
 template(wasAttributedTo,[entity,agent]).
-template(wasAssociatedWith,[activity,+agent]).
+template(wasAssociatedWith,[activity,+agent,-plan]).
 template(actedOnBehalfOf,[delegate,responsible,+activity]).
 template(wasInfluencedBy,[influencee,influencer]).
 template(specializationOf,[specificEntity,generalEntity]).
-template(alternate,[alternate1,alternate2]).
+template(alternateOf,[alternate1,alternate2]).
+
+expand(X,Y) :- (X == null -> Y = _; Y = X).
+
+postprocess([],[]).
+postprocess([specializationOf(_,E1,E2,_)|J],
+	    [specializationOf(E1,E2)|K]) :-
+	!,postprocess(J,K).
+postprocess([alternateOf(_,E1,E2,_)|J],
+	    [alternateOf(E1,E2)|K]) :-
+	!,postprocess(J,K).
+postprocess([wasDerivedFrom(ID,E2,E1,A,G1,U1,Attrs)|J],
+	    [wasDerivedFrom(ID,E2,E1,A,G2,U2,Attrs)|K]) :-
+	!,
+	(A == null
+	-> (G2 = G1, U2 = U1)
+	; (expand(G1,G2),expand(U1,U2))),
+	postprocess(J,K).
+    
+postprocess([A|J],[A|K]) :- postprocess(J,K).
+	    
\ No newline at end of file

--- a/semantics/prov_xml_test.pl	Thu Jan 31 17:03:10 2013 +0000
+++ b/semantics/prov_xml_test.pl	Thu Jan 31 19:19:07 2013 +0000
@@ -1,3 +1,6 @@
+% depends on checker and prov_xml
+:- consult(checker).
+:- consult(prov_xml).
 
 test1(J):-
 	provx_load('constraint_test_provx/unification-usage-s2-PASS-c23.provx',J).
@@ -5,7 +8,7 @@
 % Test and report on directory of .provx files
 % - only tests whether the mapping completes, 
 %  not whether result is correct,
-test2(File,Files,J):-
+test2(File,Files,J,PassOrFail):-
 	Dir='constraint_test_provx',
 	directory_files(Dir,Files),
 	sort(Files,Files1),
@@ -14,13 +17,26 @@
 	absolute_file_name(File,AbsFile,[relative_to(Dir)]),
 	exists_file(AbsFile),
 	succeeds(provx_load(AbsFile,J),PassOrFail),
-	write(PassOrFail),write(' '),write(File),nl,nl.
+	write(PassOrFail),write('\t'),write(File),nl,nl.
 
 test_all:-
-	test2(_,_,_),
+	test2(_,_,_,_),
 	fail.
 test_all.
-	
+
+validate_all:-
+	test2(File,_,J,pass),
+	(valid(J)
+	-> ( write('valid\t'),write(File), nl,nl)
+	; (write('invalid\t'),write(File), nl,nl)),
+	fail.
+validate_all.
+
+test3(File,J,K) :- Dir='constraint_test_provx',
+	absolute_file_name(File,AbsFile,[relative_to(Dir)]),
+	succeeds(provx_load(AbsFile,J),_),
+	normalize(J,K).
+
 succeeds(Goal,pass):-
 	call(Goal),
 	!.