Hi John, Se my comments below: >> >>* p. 6, F.2.3.2.8. I think that there are some subtleties in defining >> >> (next p) \equiv (1 |=> p) >> >> that make this inequivalent to the PSL X. I don't think it will be >>clear >> which rule for "|=>" should be used. >> >> Consider >> >> @(c) next strong(@(c) a) >> >> The definition says that this is equivalent to >> >> @(c) 1 |=> strong(@(c) a) >> >> Here I am not sure how to get rid of |=>. Strictly speaking, >>strong(@(c) a) >> is clocked, so I should use >> >> @(c) 1 ##1 (@(1) 1) |-> strong(@(c) a) >> >> which is definitely not the same as PSL X. >> >> When I was thinking about 1296, I kept running into dissatisfaction with >> the current definition of |=> in the clocked case, and I think we will >>need >> to make some decision in the future about what we want to do with |=>. >> >> Possibly, next should not be a derived operator at this time. If you >>are >> happy with PSL X semantics for next, then I think it makes sense to >>write the >> semantics for next as a primitive operator like in PSL. >> [[DB:]] I think it is done, need to check in the pdf that I will send by tomorrow. >>* p. 6, F.2.3.2.8. I think that >> >> s_eventually[m:$] p \equiv not(always[m:$] not p) >> >> should be a theorem. Would this make a better definition? [[DB:]] I constructed the definitions this way so that all strong operators are derived using "not". This makes the recursive properties definitions easier, because it does not need to consider strong operators. >> >>* p. 10, F.3.3.3. I have been worried that we may not want to define non- >>vacuity >> for derived operators by applying the primitive definitions to the >>semantic >> definition of the derived operator. I think it is important to check >>these cases. >> >> If next is defined as primitive, then it needs a definition here. >> [[DB:]] I can see clear semantics for "implies", and "if". I guess that for "iff" one shall require at least one of the operands to hold? For "next" I think that "w|= non next p" iff "w^1|= non p", but this may introduce false negatives in case that "next 0" is used to indicate the last letter in the computation e.g. "s_eventually next 0" means that the computation is finite. What do you think? I do not see reasonable definition for "always p". For the bounded range operators, one can require the computation to be long enough? Doron -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Mon Jan 14 00:52:09 2008
This archive was generated by hypermail 2.1.8 : Mon Jan 14 2008 - 00:52:53 PST