► |  | Redex: Practical Semantics Engineering

1 | Amb: A Redex Tutorial
2 | Long Tutorial
3 | Extended Exercises
4 | The Redex Reference
5 | Automated Testing Benchmark
| Bibliography
| Index

▼ | 3 | Extended Exercises

3.1 | Problem: Objects
3.2 | Solution: Objects
3.3 | Problem: Types
3.4 | Solution: Types
3.5 | Problem: Missionaries and Cannibals
3.6 | Solution: Missionaries and Cannibals
3.7 | Problem: Towers of Hanoi
3.8 | Solution: Towers of Hanoi
3.9 | Problem: GC
3.10 | Solution: GC
3.11 | Problem: Finite State Machines
3.12 | Solution: Finite State Machines
3.13 | Problem: Threads
3.14 | Solution: Threads
3.15 | Problem: Contracts
3.16 | Solution: Contracts
3.17 | Problem: Binary Addition
3.18 | Solution: Binary Addition

top ← prev up next →

#### 3.6`` Solution: Missionaries and Cannibals

#lang racket
;; solving the missionaries-and-cannibals problem with Redex
(require redex)
;; -----------------------------------------------------------------------------
;; the problem space syntax
(define-language MC
(configuration ::= (population boat population))
(population ::= (mc ...))
(boat ::= L R)
(mc ::= c m))
;; -----------------------------------------------------------------------------
;; constraints
(define-metafunction MC
ok : population -> boolean
[(ok (mc ...))
,(let ((m (for/sum ((mc (term (mc ...))) #:when (eq? 'm mc)) 1))
(c (for/sum ((mc (term (mc ...))) #:when (eq? 'c mc)) 1)))
(or (zero? m) (>= m c)))])
;; a subject reduction test (which sadly failed for the first draft)
(define-metafunction MC
ok-state : configuration -> boolean
[(ok-state ((mc_l ...) any (mc_r ...)))
,(and (term (ok (mc_l ...))) (term (ok (mc_r ...))))])
;; -----------------------------------------------------------------------------
;; a reduction relation that searches the state space
(define mc-->
(reduction-relation
MC
(--> [(mc_l1 ... mc_* mc_l2 ... mc_+ mc_l3 ...) L (mc_r ...)]
;; move two people from left to right
[(mc_l1 ... mc_l2 ... mc_l3 ...) R (mc_* mc_+ mc_r ...)]
(where population_left (mc_l1 ... mc_l2 ... mc_l3 ...))
(where population_right (mc_* mc_+ mc_r ...))
(where #true (ok population_left))
(where #true (ok population_right))
move-2-left-to-right)
(--> [(mc mc_1 ...) R (mc_r1 ... mc_* mc_r2 ...)]
;; move one person from right to left
[(mc_* mc mc_1 ...) L (mc_r1 ... mc_r2 ...)]
(where population_left (mc_* mc mc_1 ...))
(where population_right (mc_r1 ... mc_r2 ...))
(where #true (ok population_left))
(where #true (ok population_right))
move-1-right-to-left)
(--> [(mc mc_1 ...) R (mc_r1 ... mc_* mc_r2 ... mc_+ mc_r3 ...)]
;; move two people from right to left
[(mc_* mc_+ mc mc_1 ...) L (mc_r1 ... mc_r2 ... mc_r3 ...)]
(where population_left (mc_* mc_+ mc mc_1 ...))
(where population_right (mc_r1 ... mc_r2 ... mc_r3 ...))
(where #true (ok population_left))
(where #true (ok population_right))
move-2-right-to-left)))
;; -----------------------------------------------------------------------------
(module+ main
(traces mc--> (term ((m m m c c c) L ()))
#:pred (lambda (e) (term (ok-state ,e)))))

top ← prev up next →