%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Situation Formalization of the simple-MCP, i.e, no restrictions on % % leaving a missionary with too many cannibals, but they do use a boat. % % % % Written by Eyal Amir % % 2/27/96 % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% situation2_1_1 % [ parameters ] : THEORY BEGIN % ASSUMING % assuming declarations % ENDASSUMING %%%%%%%%%%%%%%%%%%%%%%% Declarations, etc. %%%%%%%%%%%%%%%%%%%%%%%%%% Person : TYPE p, t1, t2, m1,m2,m3,c1,c2,c3 : VAR Person WaterCrosser : TYPE Boat : WaterCrosser Bank: TYPE = { Rb,Lb } %RightBank, LeftBank bank, bank1, bank2: VAR Bank Action : TYPE a : VAR Action Nulla : Action Situation: TYPE s,s1,s2 : VAR Situation S0: Situation result : [Action, Situation -> Situation] location : [Person, Situation -> Bank] location : [WaterCrosser, Situation -> Bank] opposite(bank): Bank = (IF bank = Lb THEN Rb ELSE Lb ENDIF) can: [Action, Situation -> boolean] % Construction of the theory : Stage B %before applying this, you should do 'M-x load-prelude-library' and specify %/usr/local2/pvs/lib/finite_sets as the library % Notice that sets are represented as predicates, and thus you lose some of % "Set Theory". Persons : TYPE = finite_set[Person] M, C : Persons g,g1,g2,g3,g4,g5,g6,g7,g8,g9: VAR Persons Cross_river : [ Persons,Bank -> Action ] IMPORTING epsilons[Person] miss(s,bank) : Persons = {p| member(p,M) AND location(p,s) = bank} cann(s,bank) : Persons = {p| member(p,C) AND location(p,s) = bank} inhabitants(bank,s) : Persons = {p | location(p,s) = bank} % for the Numbers representation, but usefull anyway. take_two(g): Persons = pick({g1|subset?(g1,g) AND card(g1)=2},2) take_one(g): Persons = singleton(epsilon(g)) %%%%%%%%%%%%%%%%%%%%%%%% Axioms %%%%%%%%%%%%%%%%%%%%%%%%%% Axiom1: AXIOM Forall s, g, p: member(p,g) AND can(Cross_river(g,bank), s) IMPLIES location(p, result(Cross_river(g,bank), s)) = bank %Preconditions for crossing the river Axiom2: AXIOM subset?(g, inhabitants(bank,s)) AND card(g)<=2 AND location(Boat,s)=bank IMPLIES can(Cross_river(g,opposite(bank)),s) % Boat Axioms Axiom3: AXIOM can(Cross_river(g,bank),s) IMPLIES location(Boat, result(Cross_river(g,bank), s)) = bank % Frame Axiom Frame1: AXIOM Forall s, g, p: (NOT member(p,g)) IMPLIES location(p, result(Cross_river(g,bank), s)) = location(p,s) %Initial Situation Initial1: AXIOM member(p,M) OR member(p,C) IMPLIES location(p,S0) = Lb Initial2: AXIOM card(M) = 3 AND card(C) = 3 Initial3: AXIOM location(Boat,S0)=Lb % DNA (Distinct Names Assumption): DNA1: AXIOM C /= M DNA2: AXIOM Rb /= Lb DNA3: AXIOM member(p,M) IFF NOT member(p,C) % We got three birds in one shot here :-) DNA, CWA, and empty intersection % We might want to add that as a different kind of DNA (i.e., the members of % distinct sets are different) % Distinct Action Assumption (for the inertia formalization) DAA: AXIOM g1 /= g2 OR bank1 /= bank2 IMPLIES Cross_river(g1,bank1)/=Cross_river(g2,bank2) % Additionals Eyaldiff1: LEMMA FORALL g1,g2: disjoint?(g2, difference(g1,g2)) Eyalsets1: LEMMA g1(p) IMPLIES add(p,remove(p,g1)) = g1 Eyalsets2: LEMMA subset?(g1,g2) AND subset?(g3,g4) IMPLIES subset?(intersection(g1,g3),intersection(g2,g4)) Eyalcard1: LEMMA g1(p) IMPLIES card(difference(g1, singleton(p))) = card(g1)-1 Eyalepsilon1: LEMMA card(g)>0 IMPLIES g(epsilon(g)) Eyalepsilon1a: LEMMA card(g)>0 AND g1=singleton(epsilon(g)) IMPLIES card(g1)=1 AND subset?(g1,g) Eyalimplies1: LEMMA (FORALL p:g1(p) IMPLIES g2(p)) IFF subset?(g1,g2) %intermediate SimpleDisjoint1: LEMMA disjoint?(cann(s,bank),miss(s,bank)) SimpleDisjoint2: LEMMA disjoint?(cann(s,bank),cann(s,opposite(bank))) SimpleDisjoint3: LEMMA disjoint?(miss(s,bank),miss(s,opposite(bank))) SimpleUnion: LEMMA card(union(M,C))=6 SimpleBank: LEMMA inhabitants(bank,s) = union(cann(s,bank),miss(s,bank)) SimpleInitial: LEMMA cann(S0,Lb)=C AND miss(S0,Lb)=M IncrCard: LEMMA can(Cross_river(g1,bank),s) IMPLIES inhabitants(bank,result(Cross_river(g1,bank),s)) = union(inhabitants(bank,s),g1) % Numbers lemmas CardComplement: LEMMA card(inhabitants(bank,s))=6-card(inhabitants(opposite(bank),s)) SimpleComplement: LEMMA card(cann(s,bank)) = 6-card(cann(s,opposite(bank))) -card(miss(s,bank))-card(miss(s,opposite(bank))) Eyalpick1: LEMMA card(g)>=2 and g1=take_two(g) IMPLIES card(g1)=2 and subset?(g1,g) Eyalcard2: LEMMA FORALL (N:nat): (N=1 IMPLIES location(Boat,result(Cross_river(take_one(inhabitants(Rb,s)),Lb),s)) = Lb AND card(inhabitants(Lb,result(Cross_river(take_one(inhabitants(Rb,s)),Lb),s))) = card(inhabitants(Lb,s))+1 AND card(inhabitants(Rb,result(Cross_river(take_one(inhabitants(Rb,s)),Lb),s))) = card(inhabitants(Rb,s))-1 Lb_to_Rb: LEMMA location(Boat,s)=Lb AND card(inhabitants(Lb,s))>=2 IMPLIES location(Boat,result(Cross_river(take_two(inhabitants(Lb,s)),Rb),s)) = Rb AND card(inhabitants(Rb,result(Cross_river(take_two(inhabitants(Lb,s)),Rb),s))) = card(inhabitants(Rb,s))+2 AND card(inhabitants(Lb,result(Cross_river(take_two(inhabitants(Lb,s)),Rb),s))) = card(inhabitants(Lb,s))-2 % The following are definitions aiding in shortening the proof i: VAR nat AS(i):RECURSIVE [Action,Situation] = (IF i=0 THEN (Nulla,S0) ELSE IF even?(i) THEN (Cross_river(take_one(inhabitants(Rb,proj_2(AS(i-1)))),Lb), result(Cross_river(take_one(inhabitants(Rb, proj_2(AS(i-1)))),Lb),proj_2(AS(i-1)))) ELSE (Cross_river(take_two(inhabitants(Lb,proj_2(AS(i-1)))),Rb), result(Cross_river(take_two(inhabitants(Lb, proj_2(AS(i-1)))),Rb),proj_2(AS(i-1)))) ENDIF ENDIF) MEASURE (LAMBDA i: i) S(i):Situation = proj_2(AS(i)) Slemma: LEMMA S(i+1)= (IF even?(i+1) THEN result(Cross_river(take_one(inhabitants(Rb,S(i))),Lb),S(i)) ELSE result(Cross_river(take_two(inhabitants(Lb,S(i))),Rb),S(i)) ENDIF) % Final Lemmas % Lemma1 is the final lemma, but you should actually prove it using the 'cardinality' properties proved earlier in the theory. % Lb Rb # % % 6 2-> 0 1 % 4 <-1 2 2 % 5 2-> 1 3 % 3 <-1 3 4 % 4 2-> 2 5 % 2 <-1 4 6 % 3 2-> 3 7 % 1 <-1 5 8 % 2 2-> 4 9 % 0 6 % Here I try to prove the same thing with somewhat shorter proof (for the human...). Lemma1: LEMMA s=S(9) IMPLIES card(cann(s,Rb)) = 3 AND card(miss(s,Rb)) = 3 AND card(cann(s,Lb)) = 0 AND card(miss(s,Lb)) = 0 % Just for your knowledge : the following lemma was proved by me after severe problems, and % although I know how to formulate it easier now, I would not want you to go through that % as a plain homework... % % Lemma1a: LEMMA EXISTS g1,g2,g3,g4,g5,g6,g7,g8,g9: % s = result(Cross_river(g9,Rb), % result(Cross_river(g8,Lb), % result(Cross_river(g7,Rb), % result(Cross_river(g6,Lb), % result(Cross_river(g5,Rb), % result(Cross_river(g4,Lb), % result(Cross_river(g3,Rb), % result(Cross_river(g2,Lb), % result(Cross_river(g1,Rb),S0))))))))) % IMPLIES % card(cann(s,Rb)) = 3 AND card(miss(s,Rb)) = 3 AND % card(cann(s,Lb)) = 0 AND card(miss(s,Lb)) = 0 END situation2_1_1