Need Help

Whatever is on your mind, whether Lisp related or not.
Post Reply
shoulder

Need Help

Post by shoulder » Thu Nov 19, 2009 10:05 am

This is the question : I don't exactly know what my teacher means by hold ;
The response property is the most commonly used in formal software verification. Response(p; q) is true if every
time p holds, it is followed by q. Formally, Response(p; q) is true iff ∀ moments of time (states) i, if p(i) (meaning p
holds at moment i) then ∃ j ≥ i and q(j).
Write an ACL2 function (response qp) that takes a list of characters and returns T if the above relation is satisfied, and
returns nil if p holds at some moment and is not followed by q at a later moment.
In your modeling of the list, use the notation (a b) to indicate that a and b hold at the same moment. For exam-
ple, in the list ’(a b (c d) e), a holds at moment 1, b at moment 2, c and d at moment 3, and e at moment 4.

Possible cases to test your function against are:
• (response qp (a b c d)) returns T.
• (response qp (a b q d)) returns T.
• (response qp (a b p q)) returns T.
• (response qp (a b (p q) d)) returns T.
• (response qp (a b q q p)) returns Nil.

Here is what I have

Code: Select all

(DEFUN RESPONSE_qp (p q)
    (COND ((consp p)(cdr q))
            ((listp p) (response_qp(car q) p))
            (t (response_qp (p) (response_qp( q))))))
    
Thanks

ramarren
Posts: 613
Joined: Sun Jun 29, 2008 4:02 am
Location: Warsaw, Poland
Contact:

Re: Need Help

Post by ramarren » Wed Nov 25, 2009 12:43 am

shoulder wrote:This is the question : I don't exactly know what my teacher means by hold ;
There are those things called "dictionaries": hold, in this case the meaning 8b is applicable.

In this particular case for this particular model it merely means that if there is p in the list, it must be followed by q. The function you gave isn't even syntactically correct.

I would suggest approaching this problem by first constructing a function to determine a position of a symbol in a list even if it is in a sublist. Using that checking the response condition is trivial.

Post Reply