The source code and dockerfile for the GSW2024 AI Lab.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
This repo is archived. You can view files and clone it, but cannot push or open issues/pull-requests.

60 lines
1.5 KiB

4 weeks ago
  1. // COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90]
  2. // gxn/dxp 20/11/00
  3. mdp
  4. // constants
  5. const int N=2;
  6. const int K=2;
  7. const int range = 2*(K+1)*N;
  8. const int counter_init = (K+1)*N;
  9. const int left = N;
  10. const int right = 2*(K+1)*N - N;
  11. // shared coin
  12. global counter : [0..range] init counter_init;
  13. module process1
  14. // program counter
  15. pc1 : [0..3];
  16. // 0 - flip
  17. // 1 - write
  18. // 2 - check
  19. // 3 - finished
  20. // local coin
  21. coin1 : [0..1];
  22. // flip coin
  23. [] (pc1=0) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
  24. // write tails -1 (reset coin to add regularity)
  25. [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0);
  26. // write heads +1 (reset coin to add regularity)
  27. [] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0);
  28. // check
  29. // decide tails
  30. [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0);
  31. // decide heads
  32. [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1);
  33. // flip again
  34. [] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0);
  35. // loop (all loop together when done)
  36. [done] (pc1=3) -> 1 : (pc1'=3);
  37. endmodule
  38. // construct remaining processes through renaming
  39. module process2 = process1[pc1=pc2,coin1=coin2] endmodule
  40. // labels
  41. label "finished" = pc1=3 & pc2=3 ;
  42. label "all_coins_equal_0" = coin1=0 & coin2=0 ;
  43. label "all_coins_equal_1" = coin1=1 & coin2=1 ;
  44. label "agree" = coin1=coin2 ;
  45. // rewards
  46. rewards "steps"
  47. true : 1;
  48. endrewards