Re: [sv-ac] 1932 LTL_Formal.0701009.pdf partial review.

Hi Doron,


On Tue, Oct 30, 2007 at 08:29:43AM +0200, Bustan, Doron wrote:
> 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


PSL 1850-2005 LRM (B.4.2) defines for example

X[i] P as P preceded by i copies of 'X'

It is stated in the preamble that i>=0.

Will this use of X[0] as a synchronizing operator in PSL thus be non
backwards compatible?

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

Does this mean that '@c1 s_eventually [0:m] @c2 P' will be forbidden?

It certainly would be nice to be able to use next[0].

Otherwise maybe

s_eventually [0:0] P = P
s_eventually [1:1] P = next[1]P
s_eventually [m:n] P = s_eventually[m:n-1] or next[n]P [0<=m<n]

although this is cumbersome.

Regards,

Johan

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

-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.