[SAL-HELP] Suspicious results

[Lee Pike]

Richard,

I'm confused by why you have a temporal specification with no  
transitions in your state machine.  In any event, I believe the  
following formula is invalid, given your definitions of the constants  
BIG and LITTLE:

(BIG = LITTLE * (BIG div LITTLE))

Perhaps you're expecting division to return a REAL?

Lee

On Sep 26, 2006, at 2:59 PM, <rmbradfo at rockwellcollins.com>  
<rmbradfo at rockwellcollins.com> wrote:

>
> In the attached file, I can't figure out why I would get a counter- 
> example with F=201.  To me it seems like F should equal 200.  I've  
> counted parentheses again and again, but I can't spot my error.
>
> Thanks,
> --Richard Bradford
>
>
>
> <RBshort1.sal>