1		% farmer, goat, wolf, cabbage puzzle
2		% we need to cross the river with a boat
3		% which just has space for the farmer and one animal/object
4
5
6		start(fluss([bauer,kohl,wolf,ziege],[])). % start with everything on the left
7	?	trans(move(X),A,B) :- kante(A,X,B).
8		prop(X,X).
9		prop(X,unsafe) :- ziel(X).
10		prop(X,h(L)) :- heuristic_function_result(X,L).
11
12		% which animal eats which animal/object if left alone without the farmer (bauer)
13		eats(ziege,kohl).
14		eats(wolf,ziege).
15
16		% check if a list of animals/objects is unsafe without the farmer
17		ko(List) :-
18	?	member(X,List), member(Y,List), eats(X,Y).
19
20		% possible changes of state, by boat changing from one side to the other:
21	?	kante(fluss(L,R),X,fluss(NL,NR)) :- move(L,R,X,NL,NR).
22	?	kante(fluss(L,R),X,fluss(NL,NR)) :- move(R,L,X,NR,NL).
23
24		:- use_module(library(lists)).
25
26		move(L,R,bauer,NewL,NewR) :- % farmer takes the boat alone
27	?	select(bauer,L,NewL), % we need the farmer to take the boat
28	?	\+ ko(NewL), % we can leave the remaining objects alone
29		NewR=[bauer|R].
30		move(L,R,bauer(X),NewL,NewR) :- % farmer takes boat and one object/animal
31	?	select(bauer,L,LL),
32	?	select(X,LL,NewL), % we select another animal/object to travel in the boat
33	?	\+ ko(NewL),
34		sort([bauer,X|R],NewR). % sort to ensure a unique state representation
35
36		ziel(fluss([],[bauer,kohl,wolf,ziege] )).
37
38
39		animation_function_result(fluss(Left,Right),[((1,1),Left),((1,2),'~~'),((1,3),Right)]).
40		% using Unicode symbols seems to crash latest Tk version on macOS, so use this with care:
41		%animation_function_result(fluss(Left,Right),[((1,1),LL),((1,2),'~~'),((1,3),RR)]) :-
42		% translate(Left,LL), translate(Right,RR).
43
44		heuristic_function_active.
45		heuristic_function_result(fluss(L,_),Len) :- length(L,Len).
46
47
48		prob_pragma_string('ASSERT_LTL','G not(deadlock)').
49		prob_pragma_string('ASSERT_LTL','G not(e(move))'). % is FALSE
50		prob_pragma_string('ASSERT_LTL','G not({unsafe})'). % is FALSE
51
52		translate([],[]).
53		translate([H|T],[TH|TT]) :- (translate1(H,TH)->true ; TH=H), translate(T,TT).
54		translate1(wolf,'\x1f43a\').
55		translate1(kohl,'\x1F96C\').
56		translate1(ziege,'\x1F410\').
57
58		% Goat 128016 0x1F410
59		% Cabbage 129388
60		% Wolf 128058 1f43a