25subsort(position, integer).
26
28sort(location).
29
31subsort(cage, location).
32
34sort(gate).
35
37sort(animal).
38
41subsort(elephant, animal).
42
44subsort(horse, animal).
45
47subsort(dog, animal).
48
50subsort(human, animal).
51
53sort(species).
54
58function(loc(position), location).
59
61function(side1(gate), position).
62
64function(side2(gate), position).
65
67function(species(animal), species).
68
71predicate(accessible(position, position, time)).
72
75predicate(adult(animal)).
76
78predicate(large(animal)).
79
81predicate(largeSpecies(species)).
82
84predicate(neighbor(position, position)).
85
87predicate(sides(position, position, gate)).
88
92event(close(human, gate)).
93
95event(getOff(human, animal)).
96
98event(mount(human, animal)).
99
101event(move(animal, position)).
102
104event(open(human, gate)).
105
107event(throwOff(animal, human)).
108
112fluent(abnormalEncroachment(human)).
113
115noninertial(abnormalEncroachment).
116
118fluent(doneBy(event, animal)).
119
121noninertial(doneBy).
122
124fluent(mounted(human, animal)).
125
128fluent(mountFails(human)).
129
131noninertial(mountFails).
132
134fluent(moves(animal)).
135
137noninertial(moves).
138
140fluent(opened(gate)).
141
143fluent(pos(animal, position)).
144
147fluent(posDeterminingFluent(human, position)).
148
150noninertial(posDeterminingFluent).
151
153fluent(throwOffFails(animal, human)).
154
156noninertial(throwOffFails).
157
160t(species, humanSpecies).
161
162t(species, elephantSpecies).
163
164t(species, horseSpecies).
165
166t(species, dogSpecies).
167
170t(location, outside).
171
174largeSpecies(humanSpecies).
175
178largeSpecies(elephantSpecies).
179
182largeSpecies(horseSpecies).
183
186not(largeSpecies(dogSpecies)).
187
188%
189% examples/AkmanEtAl2004/ZooWorld.e:74
190%
191% examples/AkmanEtAl2004/ZooWorld.e:75
192% [event,animal,time]%
193% HoldsAt(DoneBy(event,animal),time) <->
194% (Happens(event,time) &
195% (({gate} event=Close(animal,gate)) |
196% ({animal1} event=GetOff(animal,animal1))|
197% ({animal1} event=Mount(animal,animal1))|
198% ({position} event=Move(animal,position))|
199% ({gate} event=Open(animal,gate)) |
200% ({human1} event=ThrowOff(animal,human1)))).
201holds_at(doneBy(Event, Animal), Time) <->
202 happens(Event, Time),
203 ( exists([Gate], Event=close(Animal, Gate))
204 ; exists([Animal1],
205 Event=getOff(Animal, Animal1))
206 ; exists([Animal15],
207 Event=mount(Animal, Animal15))
208 ; exists([Position],
209 Event=move(Animal, Position))
210 ; exists([Gate7], Event=open(Animal, Gate7))
211 ; exists([Human1],
212 Event=throwOff(Animal, Human1))
213 ).
214
223holds_at(doneBy(Event1, Animal), Time), holds_at(doneBy(Event2, Animal), Time) ->
224 Event1=Event2.
225
226%
227%
228% examples/AkmanEtAl2004/ZooWorld.e:90
229% [animal] % Large(animal) <-> (Adult(animal) & LargeSpecies(Species(animal))).
230large(Animal) <->
231 adult(Animal),
232 largeSpecies(species(Animal)).
233
240exists([Position1], (Position1\=Position, neighbor(Position, Position1))).
241
246not(neighbor(Position, Position)).
247
254neighbor(Position1, Position2) ->
255 neighbor(Position2, Position1).
256
261Cage\=outside.
262
263%
264%
265% examples/AkmanEtAl2004/ZooWorld.e:102
266% [position1,position2,gate]%
267% Sides(position1,position2,gate) <->
268% ((Side1(gate)=position1 &
269% Side2(gate)=position2) |
270% (Side2(gate)=position1 &
271% Side1(gate)=position2)).
272sides(Position1, Position2, Gate) <->
273 ( side1(Gate)=Position1,
274 side2(Gate)=Position2
275 ; side2(Gate)=Position1,
276 side1(Gate)=Position2
277 ).
278
284loc(side1(Gate))\=loc(side2(Gate)).
285
293sides(Position1, Position2, Gate1), sides(Position1, Position2, Gate2) ->
294 Gate1=Gate2.
295
302sides(Position1, Position2, Gate) ->
303 neighbor(Position1, Position2).
304
313exists([Gate], (loc(Position1)\=loc(Position2), neighbor(Position1, Position2)->sides(Position1, Position2, Gate))).
314
322holds_at(pos(Animal, Position1), Time), holds_at(pos(Animal, Position2), Time) ->
323 Position1=Position2.
324
331exists([Position], holds_at(pos(Animal, Position), Time)).
332
344Animal1\=Animal2, large(Animal1), large(Animal2), holds_at(pos(Animal1, Position), Time), holds_at(pos(Animal2, Position), Time) ->
345 ( exists([Human],
346 (Human=Animal1, holds_at(mounted(Human, Animal2), Time)))
347 ; exists([Human5],
348 (Human5=Animal2, holds_at(mounted(Human5, Animal1), Time)))
349 ).
350
359holds_at(posDeterminingFluent(Human, Position1), Time), holds_at(posDeterminingFluent(Human, Position2), Time) ->
360 Position1=Position2.
361
367initiates(move(Animal, Position), pos(Animal, Position), Time).
368
375holds_at(pos(Animal, Position1), Time) ->
376 terminates(move(Animal, Position2),
377 pos(Animal, Position1),
378 Time).
379
386happens(move(Animal, Position), Time) ->
387 not(holds_at(pos(Animal, Position), Time)).
388
395happens(move(Human, Position), Time) ->
396 not(exists([Animal],
397 holds_at(mounted(Human, Animal), Time))).
398
404initiates(open(Human, Gate), opened(Gate), Time).
405
416happens(open(Human, Gate), Time) ->
417 not(holds_at(opened(Gate), Time)),
418 not(exists([Animal],
419 holds_at(mounted(Human, Animal), Time))),
420 exists([Position],
421 ((side1(Gate)=Position;side2(Gate)=Position), holds_at(pos(Human, Position), Time))).
422
429terminates(close(Human, Gate), opened(Gate), Time).
430
442exists([Position], (happens(close(Human, Gate), Time)->holds_at(opened(Gate), Time), not(exists([Animal], holds_at(mounted(Human, Animal), Time))), (side1(Gate)=Position;side2(Gate)=Position), holds_at(pos(Human, Position), Time))).
443
451holds_at(mounted(Human, Animal), Time), holds_at(pos(Animal, Position), Time) ->
452 holds_at(pos(Human, Position), Time).
453
454%
455%
456% examples/AkmanEtAl2004/ZooWorld.e:189
457% [animal,time]%
458% HoldsAt(Moves(animal),time) <->
459% ({position}
460% HoldsAt(Pos(animal,position),time) &
461% !HoldsAt(Pos(animal,position),time+1)).
462holds_at(moves(Animal), Time) <->
463 exists([Position],
464 (holds_at(pos(Animal, Position), Time), not(holds_at(pos(Animal, Position), Time+1)))).
465
466%
467%
468% examples/AkmanEtAl2004/ZooWorld.e:195
469% [human,time]%
470% HoldsAt(MountFails(human),time) <->
471% ({animal}
472% Happens(Mount(human,animal),time) &
473% HoldsAt(Moves(animal),time)).
474holds_at(mountFails(Human), Time) <->
475 exists([Animal],
476 (happens(mount(Human, Animal), Time), holds_at(moves(Animal), Time))).
477
484not(holds_at(moves(Animal), Time)) ->
485 releases(mount(Human, Animal),
486 pos(Human, Position),
487 Time).
488
495not(holds_at(moves(Animal), Time)) ->
496 initiates(mount(Human, Animal),
497 mounted(Human, Animal),
498 Time).
499
507holds_at(pos(Animal, Position), Time), holds_at(moves(Animal), Time) ->
508 initiates(mount(Human, Animal),
509 pos(Human, Position),
510 Time).
511
519holds_at(pos(Human, Position), Time), holds_at(moves(Animal), Time) ->
520 terminates(mount(Human, Animal),
521 pos(Human, Position),
522 Time).
523
530happens(mount(Human, Animal), Time) ->
531 large(Animal).
532
539holds_at(mounted(Human, Animal), Time) ->
540 large(Animal).
541
548happens(mount(Human1, Human2), Time) ->
549 not(large(Human1)).
550
557holds_at(mounted(Human1, Human2), Time) ->
558 not(large(Human1)).
559
566happens(mount(Human, Animal), Time) ->
567 not(exists([Human1],
568 (Human1\=Human, holds_at(mounted(Human1, Animal), Time)))).
569
577holds_at(mounted(Human1, Animal), Time), holds_at(mounted(Human2, Animal), Time) ->
578 Human1=Human2.
579
586happens(mount(Human, Animal), Time) ->
587 not(exists([Human1],
588 (Human1\=Human, holds_at(mounted(Human1, Human), Time)))).
589
597exists([Animal], (happens(mount(Human1, Human2), Time)->holds_at(mounted(Human2, Animal), Time))).
598
605holds_at(mounted(Human1, Human2), Time) ->
606 not(exists([Animal],
607 holds_at(mounted(Human2, Animal), Time))).
608
615happens(mount(Human, Animal), Time) ->
616 not(exists([Animal1],
617 holds_at(mounted(Human, Animal1), Time))).
618
625not(holds_at(moves(Animal), Time)) ->
626 terminates(getOff(Human, Animal),
627 mounted(Human, Animal),
628 Time).
629
637not(holds_at(moves(Animal), Time)), holds_at(posDeterminingFluent(Human, Position), Time) ->
638 initiates(getOff(Human, Animal),
639 pos(Human, Position),
640 Time).
641
649not(holds_at(moves(Animal), Time)), holds_at(pos(Human, Position), Time) ->
650 terminates(getOff(Human, Animal),
651 pos(Human, Position),
652 Time).
653
662not(holds_at(moves(Animal), Time)), holds_at(pos(Human, Position1), Time), Position1\=Position2 ->
663 terminates(getOff(Human, Animal),
664 pos(Human, Position2),
665 Time).
666
673happens(getOff(Human, Animal), Time) ->
674 holds_at(mounted(Human, Animal), Time).
675
676%
677%
678% examples/AkmanEtAl2004/ZooWorld.e:284
679% [animal1,human,time]%
680% HoldsAt(ThrowOffFails(animal1,human),time) <->
681% ({position,animal2}
682% animal2!=human &
683% HoldsAt(PosDeterminingFluent(human,position),time) &
684% Large(animal2) &
685% HoldsAt(Pos(animal2,position),time+1)).
686holds_at(throwOffFails(Animal1, Human), Time) <->
687 exists([Position, Animal2],
688 (Animal2\=Human, holds_at(posDeterminingFluent(Human, Position), Time), large(Animal2), holds_at(pos(Animal2, Position), Time+1))).
689
698holds_at(posDeterminingFluent(Human, Position), Time), not(holds_at(throwOffFails(Animal, Human), Time)) ->
699 initiates(throwOff(Animal, Human),
700 pos(Human, Position),
701 Time).
702
710holds_at(pos(Human, Position), Time), not(holds_at(throwOffFails(Animal, Human), Time)) ->
711 terminates(throwOff(Animal, Human),
712 pos(Human, Position),
713 Time).
714
724not(holds_at(throwOffFails(Animal, Human), Time)), holds_at(pos(Human, Position1), Time), not(holds_at(posDeterminingFluent(Human, Position2), Time)), Position1\=Position2 ->
725 terminates(throwOff(Animal, Human),
726 pos(Human, Position2),
727 Time).
728
737not(exists([Animal], happens(throwOff(Animal, Human), Time)));happens(getOff(Human, animal), Time) ->
738 holds_at(posDeterminingFluent(Human, 1), Time).
739
748holds_at(posDeterminingFluent(Human, Position), Time), holds_at(throwOffFails(Animal1, Human), Time), holds_at(pos(Animal2, Position), Time) ->
749 initiates(throwOff(Animal1, Human),
750 mounted(Human, Animal2),
751 Time).
752
759not(holds_at(throwOffFails(Animal, Human), Time)) ->
760 terminates(throwOff(Animal, Human),
761 mounted(Human, Animal),
762 Time).
763
770happens(throwOff(Animal, Human), Time) ->
771 holds_at(mounted(Human, Animal), Time).
772
779happens(throwOff(Animal, Human), Time) ->
780 not(happens(getOff(Human, Animal), Time)).
781
788happens(getOff(Human, Animal), Time) ->
789 not(happens(throwOff(Animal, Human), Time)).
790
791%
792%
793% examples/AkmanEtAl2004/ZooWorld.e:336
794% [position1,position2,time]%
795% Accessible(position1,position2,time) <->
796% (Neighbor(position1,position2) &
797% !{gate} Sides(position1,position2,gate) &
798% !HoldsAt(Opened(gate),time)).
799accessible(Position1, Position2, Time) <->
800 thereExists((neighbor(Position1, Position2), not([gate])),
801 (sides(Position1, Position2, gate), not(holds_at(opened(gate), Time)))).
802
811Position1\=Position2, holds_at(pos(Animal, Position1), Time), holds_at(pos(Animal, Position2), Time+1) ->
812 accessible(Position1, Position2, Time).
813
814%
815%
816% examples/AkmanEtAl2004/ZooWorld.e:348
817% [human,time]%
818% HoldsAt(AbnormalEncroachment(human),time) <->
819% (HoldsAt(MountFails(human),time) |
820% ({position,animal1,animal2}
821% HoldsAt(PosDeterminingFluent(human,position),time) &
822% !HoldsAt(ThrowOffFails(animal2,human),time) &
823% Happens(ThrowOff(animal2,human),time) &
824% animal1!=human &
825% Large(animal1) &
826% HoldsAt(Pos(animal1,position),time) &
827% !HoldsAt(Pos(animal1,position),time+1))).
828holds_at(abnormalEncroachment(Human), Time) <->
829 ( holds_at(mountFails(Human), Time)
830 ; exists([Position, Animal1, Animal2],
831 (holds_at(posDeterminingFluent(Human, Position), Time), not(holds_at(throwOffFails(Animal2, Human), Time)), happens(throwOff(Animal2, Human), Time), Animal1\=Human, large(Animal1), holds_at(pos(Animal1, Position), Time), not(holds_at(pos(Animal1, Position), Time+1))))
832 ).
833
846holds_at(pos(Animal1, Position), Time), not(holds_at(pos(Animal1, Position), Time+1)), not(holds_at(pos(Animal2, Position), Time)), holds_at(pos(Animal2, Position), Time+1) ->
847 ( not(large(Animal1))
848 ; not(large(Animal2))
849 ; exists([Human],
850 (Human=Animal2, holds_at(abnormalEncroachment(Human), Time)))
851 ).
852
865Animal1\=Animal2, large(Animal1), large(Animal2), holds_at(pos(Animal1, Position1), Time), holds_at(pos(Animal1, Position2), Time+1), holds_at(pos(Animal2, Position1), Time), holds_at(pos(Animal2, Position2), Time+1) ->
866 not(exists([Gate],
867 sides(Position1, Position2, Gate))).
868
881Animal1\=Animal2, large(Animal1), large(Animal2), holds_at(pos(Animal1, Position1), Time), holds_at(pos(Animal1, Position2), Time+1), holds_at(pos(Animal2, Position2), Time), holds_at(pos(Animal2, Position1), Time+1) ->
882 not(exists([Gate],
883 sides(Position1, Position2, Gate))).
884
896holds_at(opened(Gate), Time), not(holds_at(opened(Gate), Time+1)), sides(Position1, Position2, Gate) ->
897 not(exists([Animal],
898 (holds_at(pos(Animal, Position1), Time), holds_at(pos(Animal, Position2), Time+1)))).
899
904t(gate, gateAO).
905
907t(cage, cageA).
908
911loc(1)=cageA.
912
916loc(2)=cageA.
917
920loc(3)=cageA.
921
924loc(4)=cageA.
925
928loc(5)=outside.
929
932loc(6)=outside.
933
936loc(7)=outside.
937
941loc(8)=outside.
942
943%
944%
945% examples/AkmanEtAl2004/ZooWorld.e:407
946% [position1,position2]%
947% Neighbor(position1,position2) <->
948% ((position1=1 & position2=2) |
949% (position1=1 & position2=3) |
950% (position1=1 & position2=4) |
951% (position1=2 & position2=3) |
952% (position1=2 & position2=4) |
953% (position1=3 & position2=4) |
954% (position1=5 & position2=6) |
955% (position1=5 & position2=7) |
956% (position1=5 & position2=8) |
957% (position1=6 & position2=7) |
958% (position1=6 & position2=8) |
959% (position1=7 & position2=8) |
960% (position2=1 & position1=2) |
961% (position2=1 & position1=3) |
962% (position2=1 & position1=4) |
963% (position2=2 & position1=3) |
964% (position2=2 & position1=4) |
965% (position2=3 & position1=4) |
966% (position2=5 & position1=6) |
967% (position2=5 & position1=7) |
968% (position2=5 & position1=8) |
969% (position2=6 & position1=7) |
970% (position2=6 & position1=8) |
971% (position2=7 & position1=8) |
972% (position1=4 & position2=7) |
973% (position2=4 & position1=7)).
974neighbor(Position1, Position2) <->
975 ( Position1=1,
976 Position2=2
977 ; Position1=1,
978 Position2=3
979 ; Position1=1,
980 Position2=4
981 ; Position1=2,
982 Position2=3
983 ; Position1=2,
984 Position2=4
985 ; Position1=3,
986 Position2=4
987 ; Position1=5,
988 Position2=6
989 ; Position1=5,
990 Position2=7
991 ; Position1=5,
992 Position2=8
993 ; Position1=6,
994 Position2=7
995 ; Position1=6,
996 Position2=8
997 ; Position1=7,
998 Position2=8
999 ; Position2=1,
1000 Position1=2
1001 ; Position2=1,
1002 Position1=3
1003 ; Position2=1,
1004 Position1=4
1005 ; Position2=2,
1006 Position1=3
1007 ; Position2=2,
1008 Position1=4
1009 ; Position2=3,
1010 Position1=4
1011 ; Position2=5,
1012 Position1=6
1013 ; Position2=5,
1014 Position1=7
1015 ; Position2=5,
1016 Position1=8
1017 ; Position2=6,
1018 Position1=7
1019 ; Position2=6,
1020 Position1=8
1021 ; Position2=7,
1022 Position1=8
1023 ; Position1=4,
1024 Position2=7
1025 ; Position2=4,
1026 Position1=7
1027 ).
1028
1033side1(gateAO)=4.
1034
1037side2(gateAO)=7.
1038