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

Added D5.1: FramaC plugin and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size:
834 bytes

Line  

1  const size=8; 

2  

3  node XOR(a,b:bool) returns (Xor:bool); 

4  let 

5  Xor = if a then not b else b; 

6  tel 

7  

8  node P(const n: int; B: bool^n) returns (p:bool); 

9  let 

10  p = with n=1 then B[0] 

11  else XOR(B[n1] , P(n1,B[0..n2])); 

12  tel 

13  

14  node parity (input: bool^size) 

15  returns (parity,done: bool); 

16  var b, todo: bool^size; 

17  let 

18  b[0..(size2)] = input[0..(size2)] > 

19  pre(b[1..(size1)]); 

20  b[size1] = input[size1] > false; 

21  todo[0..(size2)] = false^(size1) > 

22  pre(todo[1..(size1)]); 

23  todo[size1] = true > false; 

24  done = todo[0]; 

25  parity = b[0] > XOR(pre(parity) , b[0]); 

26  tel 

27  

28  node verif_parity (input: bool^size) 

29  returns(ok: bool); 

30  var comb, seq, done: bool; 

31  let 

32  ok = not done or (comb = seq); 

33  comb = P(size,input) > pre(comb); 

34  (seq,done) = parity(input); 

35  tel 

Note: See
TracBrowser
for help on using the repository browser.