source: Deliverables/D5.1/cost-plug-in/wrapper/tests/parity/parity.lus @ 1462

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 834 bytes
Line 
1const size=8;
2
3node XOR(a,b:bool) returns (Xor:bool);
4let
5        Xor = if a then not b else b;
6tel
7
8node P(const n: int; B: bool^n) returns (p:bool);
9let
10 p = with n=1 then B[0]
11      else XOR(B[n-1] , P(n-1,B[0..n-2]));
12tel
13
14node parity (input: bool^size)
15returns (parity,done: bool);
16var b, todo: bool^size;
17let
18   b[0..(size-2)] = input[0..(size-2)] ->
19                              pre(b[1..(size-1)]);
20   b[size-1] = input[size-1] -> false;
21   todo[0..(size-2)] = false^(size-1) ->
22                              pre(todo[1..(size-1)]);
23   todo[size-1] = true -> false;
24   done = todo[0];
25   parity = b[0] -> XOR(pre(parity) , b[0]);
26tel
27
28node verif_parity (input: bool^size)
29returns(ok: bool);
30var comb, seq, done: bool;
31let
32   ok = not done or (comb = seq);
33   comb =  P(size,input) -> pre(comb);
34  (seq,done) = parity(input);
35tel
Note: See TracBrowser for help on using the repository browser.