examples/msg/chord/xp_MC.txt

   1 git revision : d22dbf808ef73d20175495533fe33a47fd2252cb
   2
   3 grid5000 : parapluie-39 (rennes)
   4
   5 *****
   6
   7 chord.c
   8
   9 max_simulation_time = 10;
  10 periodic_stabilize_delay = 8;
  11 periodic_fix_fingers_delay = 8;
  12 periodic_check_predecessor_delay = 8;
  13 periodic_lookup_delay = 8;
  14
  15 chord2.xml
  16
  17 <platform version="3">
  18
  19   <process host="Gatien" function="node">
  20     <argument value="48"/>        <!-- my id -->
  21     <argument value="1"/>         <!-- known id -->
  22     <argument value="2"/>        <!-- time to sleep before it starts-->
  23     <argument value ="9"/>              <!-- deadline -->
  24   </process>
  25
  26   <process host="Jacquelin" function="node">
  27     <argument value="1"/>         <!-- my id -->
  28     <argument value ="9"/>              <!-- deadline -->
  29   </process>
  30
  31 </platform>
  32
  33 * DPOR
  34
  35 ./chord ../msg_platform.xml chord2.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/timeout:1
  36
  37 [0.000000] [mc_global/INFO] Expanded states = 123
  38 [0.000000] [mc_global/INFO] Visited states = 278
  39 [0.000000] [mc_global/INFO] Executed transitions = 262
  40 [0.000000] [mc_global/INFO] Expanded / Visited = 2.260163
  41
  42 real    0m1.691s
  43 user    0m1.612s
  44 sys       0m0.036s
  45
  46 * Both
  47
  48 ./chord ../msg_platform.xml chord2.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/timeout:1 --cfg=model-check/visited:3
  49
  50 [0.000000] [mc_global/INFO] Expanded states = 32
  51 [0.000000] [mc_global/INFO] Visited states = 95
  52 [0.000000] [mc_global/INFO] Executed transitions = 85
  53 [0.000000] [mc_global/INFO] Expanded / Visited = 2.968750
  54
  55 real    0m45.591s
  56 user    0m45.655s
  57 sys       0m0.540s
  58
  59 * State equality
  60
  61 ./chord ../msg_platform.xml chord2.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/timeout:1 --cfg=model-check/visited:3 --cfg=model-check/reduction:none
  62
  63 * None
  64
  65 ./chord ../msg_platform.xml chord2.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/timeout:1 --cfg=model-check/reduction:none
  66
  67 ****
  68
  69 chord.c
  70
  71 max_simulation_time = 20;
  72 periodic_stabilize_delay = 8;
  73 periodic_fix_fingers_delay = 8;
  74 periodic_check_predecessor_delay = 8;
  75 periodic_lookup_delay = 8;
  76
  77 chord2.xml
  78
  79 <platform version="3">
  80
  81   <process host="Gatien" function="node">
  82     <argument value="48"/>        <!-- my id -->
  83     <argument value="1"/>         <!-- known id -->
  84     <argument value="2"/>        <!-- time to sleep before it starts-->
  85     <argument value ="18"/>             <!-- deadline -->
  86   </process>
  87
  88   <process host="Jacquelin" function="node">
  89     <argument value="1"/>         <!-- my id -->
  90     <argument value ="18"/>             <!-- deadline -->
  91   </process>
  92
  93 </platform>
  94
  95
  96 * DPOR
  97
  98 ./chord ../msg_platform.xml chord2.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/timeout:1
  99
 100 [0.000000] [mc_global/INFO] Expanded states = 1103
 101 [0.000000] [mc_global/INFO] Visited states = 2714
 102 [0.000000] [mc_global/INFO] Executed transitions = 2644
 103 [0.000000] [mc_global/INFO] Expanded / Visited = 2.460562
 104
 105 real    0m1.995s
 106 user    0m1.952s
 107 sys       0m0.044s
 108
 109 * Both
 110
 111 ./chord ../msg_platform.xml chord2.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/timeout:1 --cfg=model-check/visited:3
 112
 113 [0.000000] [mc_global/INFO] Expanded states = 28
 114 [0.000000] [mc_global/INFO] Visited states = 91
 115 [0.000000] [mc_global/INFO] Executed transitions = 81
 116 [0.000000] [mc_global/INFO] Expanded / Visited = 3.250000
 117
 118 real    0m47.025s
 119 user    0m47.099s
 120 sys       0m0.516s
 121
 122 * State equality
 123
 124 ./chord ../msg_platform.xml chord2.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/timeout:1 --cfg=model-check/visited:3 --cfg=model-check/reduction:none
 125
 126 * None
 127
 128 ./chord ../msg_platform.xml chord2.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/timeout:1 --cfg=model-check/reduction:none
 129
 130 ****
 131
 132 chord.c
 133
 134 max_simulation_time = 50;
 135 periodic_stabilize_delay = 8;
 136 periodic_fix_fingers_delay = 8;
 137 periodic_check_predecessor_delay = 8;
 138 periodic_lookup_delay = 8;
 139
 140 chord2.xml
 141
 142 <platform version="3">
 143
 144   <process host="Gatien" function="node">
 145     <argument value="48"/>        <!-- my id -->
 146     <argument value="1"/>         <!-- known id -->
 147     <argument value="2"/>        <!-- time to sleep before it starts-->
 148     <argument value ="48"/>             <!-- deadline -->
 149   </process>
 150
 151   <process host="Jacquelin" function="node">
 152     <argument value="1"/>         <!-- my id -->
 153     <argument value ="48"/>             <!-- deadline -->
 154   </process>
 155
 156 </platform>
 157
 158
 159 * DPOR
 160
 161 ./chord ../msg_platform.xml chord2.xml --cfg=model-check:1 --cfg=contexts/factory:ucontext --cfg=model-check/timeout:1