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 programming.

---

Context:

This problem set requires the definition of TOP from problem 1 on Problem Set 3 and some of your solutions to the same problem.

Problem 1:

Develop a Redex relation that simulates the pattern matching process when an FSM is "applied" to a sequence of keystrokes:

1. if a prefix of the sequence of keystrokes drives the given FSM into a final state, the transition sequence ends in ACCEPTED;
2. if the sequence of keystrokes is exhausted satisfies the FSM, the transition sequence ends in SHORT;
3. if the sequence of keystrokes drives the FSM into a stuck state, the transition sequence ends in REJECTED.

Thus, the relation relates relates pairs of FSMs and keystroke sequences extended with three tokens indicating the outcome of the process.

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 trace window.

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.

Problem 2:

Prove the following claim

  (define-metafunction TOP
    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)))
   

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 counter-example.

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.

Problem 3:

In the given context, run the following expression in DrRacket's interactions area:

  (redex-check TOP FSM (displayln (term FSM)) #:attempts 10)
   

It generates 10 instances of FSM from TOP, which are then supplied to the "conjecture" (displayln (term FSM)). Inspect the outputs.

Explain in 20 words (or less) a fundamental flaw of all FSMs generated.

In Redex, you could read in an XFSM with the following function:

  (define-metafunction TOP
    read-an-xfsm : string -> XFSM
    [(read-an-xfsm string_filename)
     ,(let* ([file (term string_filename)]
	     [elim (eliminate-whitespace '() (lambda (_) #t))])
	(xml->xexpr (elim (with-input-from-file file read-xml/element))))])
   

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 good specification.

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: function:

  (define (run-1 t)
    (display-xml/content (xexpr->xml t))
    (newline)
    (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))
    (displayln r)
    r)

   (redex-check FSM-L FSM (run-1 (term FSM)) #:attempts 3)
   

In other words, you could use the model to check whether program is a implementation that copes with random finite state machines.

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.

Deliverable:

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:

  ;; NameOfPartner1, NameOfPartner2 
  ;; email@of.partner1.com, email@of.partner2.com

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.