Due date: 10/05 @ at the beginning of class
Purpose: One goal of this problem set is to prove simple
conjectures. The other goal is to acquire some familiarity with relational
This problem set requires the definition of TOP from
problem 1 on Problem Set 3 and some of your
solutions to the same problem.
Develop a Redex relation that simulates the pattern matching process when an
FSM is "applied" to a sequence of keystrokes:
Thus, the relation relates relates pairs of FSMs and keystroke
sequences extended with three tokens indicating the outcome of the
if a prefix of the sequence of keystrokes drives the given FSM
into a final state, the transition sequence ends in ACCEPTED;
if the sequence of keystrokes is exhausted satisfies the FSM,
the transition sequence ends in SHORT;
if the sequence of keystrokes drives the FSM into a stuck
state, the transition sequence ends in REJECTED.
Your solution should include a (subset of a) test suite that reveals the
non-deterministic nature of FSM specifications.
Hints Think of the initial state of the given
FSM as the current state. If you follow this advice,
stuck? requires some modifications, including the option of not
providing a current key (because there is none). You may uses
traces to debug your solution but your solution may not spawn a
Constraint Your solution must use the Redex
programming language. The relations and functions may escape to the Racket
programming language only for non-recursive tasks like consing an item
onto a list.
Prove the following claim
where xfsm-2-fsm and fsm-2-xfsm are your (fixed)
solutions to Problem 1 on Problem Set 3. Include these solutions with your
homework and make sure that the above redex check does not find a
x-2-f : XFSM -> #t or #f
[(x-2-f XFSM) ,(equal? (term (fsm-2-xfsm (xfsm-2-fsm XFSM))) (term XFSM))])
(redex-check TOP XFSM (term (x-2-f XFSM)))
It is best to formulate the proof in DrRacket's definition window and to
comment it out afterward. Hint Do not think all swans are
white just because all the swans you have seen are white. There are black
swans in Australia.
In the given context, run the following expression in DrRacket's
It generates 10 instances of FSM from TOP, which are
then supplied to the "conjecture" (displayln (term FSM)). Inspect
(redex-check TOP FSM (displayln (term FSM)) #:attempts 10)
Explain in 20 words (or less) a fundamental flaw of all FSMs generated.
In Redex, you could read in an XFSM with the following
You could then run your simulation relation from Problem 1
for some fixed sequence of keys. In other words, you could use the
model to check whether the XFSM in the file is a
read-an-xfsm : string -> XFSM
,(let* ([file (term string_filename)]
[elim (eliminate-whitespace '() (lambda (_) #t))])
(xml->xexpr (elim (with-input-from-file file read-xml/element))))])
Develop run. The meta-function consumes a filename (as a string),
reads an XFSM from the specified file, and traces its execution
on the key sequence ("a" "b" "c" "d"). -- Your solution may
assume that your program will be run in the presence of a file "1.xml",
which contains an XFSM as an XML specification.
Conversely, you could use the following function to generate
XFSMs with redex-check and run a solution to
Problem Set 1 on the randomly generated fsm:
In other words, you could use the model to check whether
program is a implementation that copes with random finite state machines.
(define (run-1 t)
(display-xml/content (xexpr->xml t))
(define fl "1-temp.xml")
(with-output-to-file #:exists 'truncate fl
(lambda () (write-xml/content (xexpr->xml t))))
; for non-Racket solutions (system (format "./1.rkt ~a" fl))
(define r (main fl))
(redex-check FSM-L FSM (run-1 (term FSM)) #:attempts 3)
Explain in 40 words (or less) how the fundamental flaw discussed above
affects this connection between the model of finite state machines and
your "real world" program.
Send in a single Racket file. Its name should
consist of the two last names in alphabetical order separated with a
hyphen; its suffix must be .rkt.
Your file must start with the following two lines:
appropriately instantiated of course. Also separate problems with lines of
the shape ";; " followed by 77 "-". That gives you a width of 80 chars. Try
to stick to this width for all of your code; it ensures basic readability.
;; NameOfPartner1, NameOfPartner2
;; firstname.lastname@example.org, email@example.com