Hi Johan, >> > next[0] p == p (next[0] is needed for the definition of >> eventually[0:x]) >> > next[n] p == next (next[n-1] p) [n>0] >> > >> > and >> > s_next[n] p == not next[n] not p [n>0] >> >> [DB:] The reason next[m] starts from 1, is that we want to reserve >> next[0] as synchronizing operator for multi clock properties. I just saw >> a presentation by Dana Fisman on a similar operator in PSL. I am waiting >> for the proceeding of the conference HVC07, that should be published at >> November 19, to see what she has done. > >How should we define 's_eventually [0:m]' and 'always [0:m]'? It seems >they are ultimately defined in terms of next[0]. Yes that is a problem Maybe 's_eventually [0:m] p = 1[*0:m] #-# p' And 'always [0:m] p = 1[*0:m] |-> p]' Note, that in this case p cannot have a different leading clock. What do you think? Doron --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Mon Oct 29 23:30:49 2007
This archive was generated by hypermail 2.1.8 : Mon Oct 29 2007 - 23:30:55 PDT