-
Erwan Jahier authored
For instance, do not launch tests that perform result comparison (via lurette) on files that contains extern nodes (as they cannot be executed) or package. Package do not work because appending the tested lustre file with the generated oracle as I do is wrong in presence of package. Moreover, my current test process is not able to test programs which main node IOs are not all on the base clock. I have fixed this by patching the examples. # of expected passes 1508 -> 1512 # of unexpected failures 130 -> 84
Erwan Jahier authoredFor instance, do not launch tests that perform result comparison (via lurette) on files that contains extern nodes (as they cannot be executed) or package. Package do not work because appending the tested lustre file with the generated oracle as I do is wrong in presence of package. Moreover, my current test process is not able to test programs which main node IOs are not all on the base clock. I have fixed this by patching the examples. # of expected passes 1508 -> 1512 # of unexpected failures 130 -> 84
PCOND1.lus 853 B
node PCOND1(h0:bool; hA,hB,hC:bool ;
A:int ; B:int ; C:bool;
hD:bool; D:bool)
returns (hX:bool);
var
hX_on_h0: bool when h0;
hA_on_h0: bool when h0;
hB_on_h0: bool when h0;
hC_on_h0: bool when h0;
hD_on_hC_on_h0: bool when hC_on_h0;
let
hX = current(hX_on_h0);
hA_on_h0 = hA when h0;
hB_on_h0 = hB when h0;
hC_on_h0 = hC when h0;
hD_on_hC_on_h0 = hD when hC_on_h0;
hX_on_h0 = PCOND1_clk(h0,hA when h0,hB when h0,
hC when h0,A when hA_on_h0,B when hB_on_h0,C when hC_on_h0,
hD when hC_on_h0,D when hD_on_hC_on_h0);
tel
node PCOND1_clk(h0:bool; hA,hB,hC:bool when h0;
A:int when hA; B:int when hB; C:bool when hC;
hD:bool when hC; D:bool when hD)
returns (hX:bool when h0);
let
hX = hC and current(hD) and h0 when h0;
tel