;; The first three lines of this file were inserted by DrRacket. They record metadata
;; about the language level of this file in a form that our tools can easily process.
#reader(lib "htdp-intermediate-lambda-reader.ss" "lang")((modname reachables-tues-2) (read-case-sensitive #t) (teachpacks ()) (htdp-settings #(#t constructor repeating-decimal #f #t none #f ())))
(require rackunit)
(require "extras.rkt")
;; Node = Int
;; Int -> SetOfInt
;; GIVEN: an integer
;; RETURNS: the list of its successors in the implicit graph.
;; For this graph, this is always a set (no repetitions)
(define (successors1 n)
(if (<= n 0)
empty
(local
((define n1 (quotient n 3)))
(list n1 (+ n1 5)))))
(begin-for-test
(check set-equal? (successors1 6) (list 2 7))
(check set-equal? (successors1 2) (list 0 5))
(check set-equal? (successors1 0) empty)
(check set-equal? (successors1 5) (list 1 6))
(check set-equal? (successors1 1) (list 0 5)))
(define (all-successors nodes)
(foldr
(lambda (node ans-for-rest)
(set-union
(successors1 node)
ans-for-rest))
empty
nodes))
(begin-for-test
(check set-equal?
(all-successors (list 2 6))
(list 0 5 2 7)))
#|
A HALTING MEASURE is a quantity that is
(a) always a non-negative integer
(b) that decreases at every recursive call
A TERMINATION ARGUMENT consists of
-- a claimed halting measure
-- an argument that the claimed halting measure really
is a halting measure.
|#
;; reachable : SetOfNode Nat -> SetOfNode
;; GIVEN: A set of nodes and a nonnegint n
;; RETURNS: the set of nodes reachable from the given nodes
;; in n or fewer steps
;; HALTING MEASURE: n
(define (reachable nodes n)
(if (zero? n) nodes
(local
((define new-nodes (reachable nodes (- n 1))))
(set-union
new-nodes
(all-successors new-nodes)))))
#;(begin-for-test
(check set-equal? (reachable (list 30) 0)
(list 30))
(check set-equal? (reachable (list 30) 1)
(list 30 10 15))
(check set-equal? (reachable (list 30) 2)
(list 30 10 15 3 8 5)))
;; all-reachables : Node SetOfNodes -> SetOfNodes
;; GIVEN: a node src and set of nodes seen
;; WHERE:
;; src has a finite number of reachable nodes.
;; seen = (reachable (list src) n) for some n.
;; RETURNS: the set of all nodes reachable from src
;; STRATEGy: General Recursion
;; HALTING MEASURE: (the number of nodes reachable from src)
;; - (the number of nodes in seen)
(define (all-reachables src seen)
(local
((define new-nodes (all-successors seen)))
(cond
[(set-equal? seen new-nodes) seen]
[else (all-reachables src
(set-union
seen
new-nodes))])))
;; initialize with:
(all-reachables src (list src))