-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcannibals.rkt
92 lines (78 loc) · 3.99 KB
/
cannibals.rkt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
#lang racket
(require redex)
(define-language Cannibals
(person ::= missionary cannibal)
(boat ::=
(person person)
(person)
())
(river ::= (boat water) (water boat))
(state ::= ((person ...) river (person ...))))
(define startstate
(term (() (water ()) (missionary missionary missionary cannibal cannibal cannibal))))
(module+ test
(define (test-#t v)
(test-equal v #true))
(test-#t (redex-match? Cannibals state startstate)))
(define -->boat
(reduction-relation
Cannibals
#:domain state
(--> [(person_1 ...) (boat water) (person_i person_2 ...)]
[(person_1 ...) (water boat) (person_i person_2 ...)] ;; don't boat towards empty RHS shore
(side-condition (not (eq? (term boat) (term ())))) ;; boat not empty!
boat→)
(--> [(person_1 ...) (water boat) (person_2 ...)]
[(person_1 ...) (boat water) (person_2 ...)]
(side-condition (not (eq? (term boat) (term ())))) ;; boat not empty!
boat←)
(--> [(person_1 ...) (water ( person_b ...)) (person_2 ... person_i person_n ...)]
[(person_1 ...) (water (person_i person_b ...)) (person_2 ... person_n ...)]
(side-condition (< (length (term (person_b ...))) 2))
(side-condition (or (eq? 0 (missionaries (term (person_2 ... person_n ...))))
(>= (missionaries (term (person_2 ... person_n ...)))
(cannibals (term (person_2 ... person_n ...))))))
embark-right)
(--> [(person_1 ... person_i person_n ...) (( person_b ...) water) (person_2 ...)]
[(person_1 ... person_n ...) ((person_i person_b ...) water) (person_2 ...)]
(side-condition (< (length (term (person_b ...))) 2))
(side-condition (not (empty? (term (person_2 ...))))) ;; don't embark once everyone's accross!
(side-condition (or (eq? 0 (missionaries (term (person_1 ... person_n ...))))
(>= (missionaries (term (person_1 ... person_n ...)))
(cannibals (term (person_1 ... person_n ...))))))
embark-left)
(--> [(person_1 ...) (water (person_a ... person_i person_b ...)) ( person_n ...) ]
[(person_1 ...) (water (person_a ... person_b ...)) (order (person_i person_n ...))]
(side-condition (or (eq? 0 (missionaries (term (person_i person_n ...))))
(>= (missionaries (term (person_i person_n ...)))
(cannibals (term (person_i person_n ...))))))
disembark-right)
(--> [( person_2 ... ) ((person_a ... person_i person_b ...) water) (person_1 ...)]
[(order (person_2 ... person_i)) ((person_a ... person_b ...) water) (person_1 ...)]
(side-condition (or (eq? 0 (missionaries (term (person_i person_2 ...))))
(>= (missionaries (term (person_i person_2 ...)))
(cannibals (term (person_i person_2 ...))))))
disembark-left)
))
(define-metafunction Cannibals
order : (person ...) -> (person ...)
[(order (person ...))
,(sort (term (person ...)) (lambda (x y) (string<=? (symbol->string x)
(symbol->string y))))])
(define (cannibals l)
(length (remove* '(missionary) l)))
(define (missionaries l)
(length (remove* '(cannibal) l)))
(module+ test
;; we manage to embark one cannibal from right.
(test-->>∃ -->boat startstate (term (() (water (cannibal))
(cannibal cannibal
missionary missionary missionary))))
;; we manage to transfer everybody.
(test-->>∃ -->boat startstate (term ((cannibal cannibal cannibal
missionary missionary missionary
(() water) ()))))
)
(module+ test
(stepper -->boat startstate)
(test-results))