Subject: [sv-ac] semantics of match
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Feb 26 2003 - 06:13:56 PST
roy, surrendra,
i am trying to understand the semantics of match as presented on page 20 of
the ova document. let's assume for the moment that a and r are both false.
then we get that
pi, j, c, false, false |= matched (e) if the following two hold:
- pi, j |= c
- there exists i <= k < j s.t. pi,i,k,c \modelstightly e and for all l, k
<= l < j, pi, l |= !c
i don't understand the "<=" in "k <= l < j". i think that if
pi,i,k,c \modelstightly e
then according to page 14, c holds at pi^k. is that correct? if so, then
how can it ever be that "for all l, k <= l < j, pi, l |= !c"? shouldn't it
be "k < l < j" instead?
thanks,
cindy.
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
This archive was generated by hypermail 2b28 : Wed Feb 26 2003 - 06:10:46 PST