Project

General

Profile

Download (426 Bytes) Statistics
| Branch: | Tag: | Revision:
1
(*@ contract NLGuidanceSpec (Vt, Vv, Xtarg,   Xv:real^3; r:real; ) returns (r1: real; );
2
let
3
var P1 : bool = 0.0 = Vt[0];
4
guarantee "NLG-007" P1;
5
tel
6
*)
7

    
8
node mynode (Vt, Vv, Xtarg,   Xv:real^3; r:real; ) returns (r1: real; );
9
var P0, P1: bool;
10
let
11
 P0 = [0.1, 0.2] = [0.1, 0.3]; -- Bug: it looks like the output C doesn't check the equality btw values but pointers!
12
 P1 = 0.0 = Vt[0];
13
 r1 = if P1 && P0 then 1.0 else 0.0;
14
tel
(9-9/16)