Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : stats XP of model checking on chord example
[simgrid.git] / 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