fond
Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
ITS-Tools: StateSpace on NeoElection/3 (Colored)
Last Updated
Apr. 26, 2013

Introduction

This page shows the outputs produced by the execution of ITS-Tools on NeoElection/3 (Colored). We provide:

About the Execution

Execution Summary
Memory (MB) CPU (s) End
66.17 1.05 normal

Execution Chart

We display below the execution chart for this examination (boot time has been removed).

Sequence of Actions to be Executed by the VM

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

export BK_INPUT=NeoElection-COL-3
export BK_EXAMINATION=StateSpace
export BK_TOOL=ITS-Tools
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1749
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/NeoElection-COL-3
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool ITS-Tools:'
echo ' Test is NeoElection-COL-3, examination is StateSpace'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of ITS-Tools for NeoElection/3 (Colored)

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.


execution on node 25: cluster1u27.lip6.fr (runId=136959878702144_n_25)
=====================================================================
runnning ITS-Tools on NeoElection-COL-3 (StateSpace)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool ITS-Tools:
Test is NeoElection-COL-3, examination is StateSpace
=====================================================================

--------------------
content from stdout:

START 1370196872
its-reach command run as :

/home/mcc/BenchKit/bin/its-reach -i model.sep.flat.gal -t GAL --quiet
Model ,|S| ,Time ,Mem(kb) ,fin. SDD ,fin. DDD ,peak SDD ,peak DDD ,SDD Hom ,SDD cache peak ,DDD Hom ,DDD cachepeak ,SHom cache
neoelection\_3\_sep\_inst,974325,3.57,32840,2,12489,5,263107,6,0,3224,105899,0
Total reachable state count : 974325

STATE_SPACE 974325 TECHNIQUES DECISION_DIAGRAMS
STOP 1370196876

--------------------
content from stderr:

initial cost 327223
final cost 24493
crashed[0],dead[0],electionFailed[0],masterList[0],masterList[10],masterList[20],masterList[30],masterList[40],negotiation[0],negotiation[30],network[10],network[110],network[130],network[140],network[170],network[190],network[20],network[210],network[230],network[250],network[260],network[290],network[310],network[330],network[350],network[370],network[380],network[50],startNeg__broadcasting[0],electionInit[0],network[70],network[90],poll__networl[0],poll__networl[100],poll__networl[10],poll__networl[110],poll__networl[120],poll__networl[130],poll__networl[140],poll__networl[160],poll__networl[170],poll__networl[180],poll__networl[190],poll__networl[200],poll__networl[20],poll__networl[210],poll__networl[220],poll__networl[230],poll__networl[240],poll__networl[250],poll__networl[260],poll__networl[280],poll__networl[290],poll__networl[300],poll__networl[310],poll__networl[320],poll__networl[330],poll__networl[340],poll__networl[350],poll__networl[360],poll__networl[370],poll__networl[380],poll__networl[40],poll__networl[50],poll__networl[60],poll__networl[70],poll__networl[80],poll__networl[90],crashed[1],dead[1],electionFailed[1],masterList[11],masterList[1],masterList[21],masterList[31],masterList[41],network[111],network[11],network[121],network[131],network[141],network[161],network[171],network[181],network[191],network[1],network[201],network[211],network[21],network[231],network[241],network[251],network[261],network[281],network[291],network[301],network[311],network[321],network[331],network[351],network[361],network[371],network[381],network[41],network[51],network[61],network[71],network[81],network[91],poll__networl[111],poll__networl[11],poll__networl[121],poll__networl[131],poll__networl[141],poll__networl[161],poll__networl[171],poll__networl[181],negotiation[1],negotiation[2],poll__networl[191],poll__networl[1],poll__networl[201],poll__networl[211],poll__networl[21],poll__networl[231],poll__networl[241],poll__networl[251],poll__networl[261],poll__networl[281],poll__networl[291],poll__networl[301],poll__networl[311],poll__networl[321],poll__networl[331],poll__networl[351],poll__networl[361],poll__networl[371],poll__networl[381],poll__networl[41],poll__networl[51],poll__networl[61],poll__networl[71],poll__networl[81],poll__networl[91],sendAnnPs__broadcasting[1],startNeg__broadcasting[1],crashed[2],dead[2],electionFailed[2],masterList[12],masterList[22],masterList[2],masterList[32],masterList[42],negotiation[12],network[122],network[142],network[162],network[182],network[202],network[212],network[22],network[242],network[262],network[282],network[2],network[302],network[322],network[332],network[362],network[382],network[42],network[62],network[82],network[92],poll__networl[112],poll__networl[122],poll__networl[12],poll__networl[132],poll__networl[142],poll__networl[152],poll__networl[162],poll__networl[172],poll__networl[182],poll__networl[192],poll__networl[202],poll__networl[212],poll__networl[22],poll__networl[232],poll__networl[242],poll__networl[252],poll__networl[262],poll__networl[272],poll__networl[282],poll__networl[292],poll__networl[2],poll__networl[302],poll__networl[312],poll__networl[322],poll__networl[32],poll__networl[332],poll__networl[352],poll__networl[362],poll__networl[372],poll__networl[382],poll__networl[42],poll__networl[52],poll__networl[62],poll__networl[72],negotiation[10],negotiation[4],sendAnnPs__broadcasting[0],negotiation[11],negotiation[5],stage[2],electedPrimary[0],electedSecondary[0],poll__waitingMessage[0],stage[0],negotiation[8],negotiation[7],stage[1],poll__networl[82],poll__networl[92],sendAnnPs__broadcasting[2],startNeg__broadcasting[2],network[12],polling[0],network[36],network[16],network[40],network[4],network[64],network[88],network[8],network[60],poll__networl[5],poll__networl[6],poll__networl[7],network[0],poll__networl[29],poll__networl[30],poll__networl[31],network[5],network[6],network[7],network[104],masterState[0],poll__networl[53],poll__networl[54],poll__networl[55],network[100],poll__networl[77],poll__networl[78],poll__networl[79],network[24],masterState[1],masterState[2],masterState[4],masterState[3],poll__handlingMessage[0],poll__pollEnd[0],network[200],masterState[5],masterState[6],masterState[7],network[31],network[29],network[30],network[84],network[108],network[296],network[132],network[48],network[28],network[112],network[136],network[196],network[101],network[102],network[103],network[32],network[53],network[55],network[96],network[124],network[54],poll__networl[101],network[128],poll__networl[103],poll__networl[125],poll__networl[102],network[72],poll__networl[127],poll__networl[126],network[120],network[125],network[127],network[126],masterState[8],poll__networl[149],masterState[9],poll__networl[151],poll__networl[150],poll__networl[173],masterState[12],poll__handlingMessage[1],poll__pollEnd[1],masterState[15],masterState[11],masterState[14],masterState[10],poll__networl[175],poll__networl[174],masterState[13],network[156],network[224],crashed[3],dead[3],electionFailed[3],masterList[13],masterList[23],network[78],network[77],network[79],network[292],masterList[33],network[320],network[180],masterList[3],masterList[43],negotiation[3],network[113],network[149],network[151],network[150],network[123],network[220],network[133],network[13],network[144],network[143],network[153],network[163],network[183],network[193],network[203],network[213],network[233],network[23],network[243],network[253],network[263],network[273],network[283],network[303],network[313],network[323],network[168],network[173],network[174],network[175],network[333],stage[4],network[316],network[33],network[353],network[363],network[373],network[383],stage[3],poll__waitingMessage[1],negotiation[17],negotiation[16],polling[1],network[52],electedSecondary[1],stage[5],network[197],network[198],network[199],network[3],negotiation[20],network[43],network[63],network[73],network[83],network[93],electedPrimary[1],network[192],network[148],network[223],network[222],network[221],negotiation[23],poll__networl[113],poll__networl[123],poll__networl[133],negotiation[13],negotiation[14],network[160],network[204],network[56],network[216],negotiation[19],network[228],network[152],network[184],poll__networl[197],poll__networl[198],poll__networl[199],poll__networl[221],poll__networl[222],poll__networl[223],masterState[23],masterState[21],poll__handlingMessage[2],poll__pollEnd[2],masterState[17],masterState[18],masterState[19],masterState[20],masterState[22],network[247],network[245],network[246],masterState[16],network[240],poll__networl[245],poll__networl[246],poll__networl[247],network[248],poll__networl[269],poll__networl[270],poll__networl[271],network[244],negotiation[18],network[256],negotiation[22],startNeg__broadcasting[5],sendAnnPs__broadcasting[3],negotiation[27],network[344],network[208],sendAnnPs__broadcasting[5],network[252],startNeg__broadcasting[3],startNeg__broadcasting[4],network[232],startNeg__broadcasting[6],network[270],network[269],network[271],network[264],network[276],electionInit[1],network[293],electionInit[2],network[340],network[294],network[76],negotiation[21],network[295],sendAnnPs__broadcasting[6],negotiation[39],sendAnnPs__broadcasting[4],negotiation[28],startNeg__broadcasting[7],polling[2],sendAnnPs__broadcasting[7],network[319],network[317],startNeg__broadcasting[9],network[318],electedPrimary[2],network[172],stage[7],network[280],electionInit[3],network[288],sendAnnPs__broadcasting[10],negotiation[29],poll__waitingMessage[2],stage[6],network[312],sendAnnPs__broadcasting[8],electedSecondary[2],startNeg__broadcasting[10],network[328],startNeg__broadcasting[8],negotiation[32],negotiation[35],stage[8],sendAnnPs__broadcasting[9],negotiation[33],negotiation[31],negotiation[34],network[341],network[343],network[342],network[80],network[352],network[268],network[336],network[176],network[300],masterState[30],masterState[29],negotiation[40],poll__handlingMessage[3],poll__pollEnd[3],masterState[25],masterState[26],negotiation[42],masterState[31],masterState[27],masterState[28],poll__networl[13],poll__networl[293],poll__networl[294],sendAnnPs__broadcasting[11],poll__networl[295],poll__networl[317],poll__networl[318],poll__networl[319],network[272],masterState[24],network[324],poll__networl[341],network[366],network[365],poll__networl[342],network[367],poll__networl[343],network[360],poll__networl[365],poll__networl[366],poll__networl[143],poll__networl[367],startNeg__broadcasting[11],network[368],network[376],network[364],electedPrimary[3],negotiation[43],network[348],polling[3],network[304],negotiation[41],poll__networl[153],stage[10],network[372],negotiation[44],poll__waitingMessage[3],stage[9],poll__networl[163],electedSecondary[3],negotiation[47],stage[11],poll__networl[183],negotiation[46],poll__networl[193],poll__networl[203],poll__networl[213],poll__networl[233],poll__networl[23],poll__networl[243],poll__networl[253],poll__networl[263],poll__networl[273],poll__networl[283],poll__networl[303],poll__networl[313],poll__networl[323],poll__networl[333],poll__networl[33],poll__networl[353],poll__networl[363],poll__networl[373],poll__networl[383],poll__networl[3],poll__networl[43],poll__networl[63],poll__networl[73],poll__networl[83],poll__networl[93],masterList[14],masterList[24],masterList[34],masterList[44],masterList[4],negotiation[24],network[114],network[134],network[14],network[154],network[164],network[194],network[214],network[234],network[254],network[274],network[284],network[314],network[334],network[34],network[354],network[374],network[44],network[74],network[94],poll__networl[104],poll__networl[114],poll__networl[124],poll__networl[134],poll__networl[144],poll__networl[14],poll__networl[154],poll__networl[164],poll__networl[184],poll__networl[194],poll__networl[204],poll__networl[214],poll__networl[224],poll__networl[234],poll__networl[244],poll__networl[24],poll__networl[254],poll__networl[264],poll__networl[274],poll__networl[284],poll__networl[304],poll__networl[314],poll__networl[324],poll__networl[334],poll__networl[344],poll__networl[34],poll__networl[354],poll__networl[364],poll__networl[374],poll__networl[44],poll__networl[4],poll__networl[64],poll__networl[74],poll__networl[84],poll__networl[94],masterList[15],masterList[25],masterList[35],masterList[45],masterList[5],negotiation[15],negotiation[45],network[105],network[115],network[135],network[145],network[155],network[15],network[165],network[185],network[195],network[205],network[215],network[225],network[235],network[255],network[25],network[265],network[275],network[285],network[305],network[315],network[325],network[335],network[345],network[355],network[35],network[375],network[45],network[65],network[75],network[85],network[95],poll__networl[105],poll__networl[115],poll__networl[135],negotiation[25],negotiation[26],poll__networl[145],poll__networl[155],poll__networl[15],poll__networl[165],poll__networl[185],poll__networl[195],poll__networl[205],poll__networl[215],poll__networl[225],poll__networl[235],poll__networl[255],poll__networl[25],poll__networl[265],poll__networl[275],poll__networl[285],poll__networl[305],poll__networl[315],poll__networl[325],poll__networl[335],poll__networl[345],poll__networl[355],poll__networl[35],poll__networl[375],poll__networl[45],poll__networl[65],poll__networl[75],poll__networl[85],poll__networl[95],masterList[16],masterList[26],masterList[36],masterList[46],masterList[6],negotiation[36],negotiation[6],network[106],network[116],network[146],network[166],network[186],network[206],network[226],network[236],network[266],network[26],network[286],network[306],network[326],network[346],network[356],network[46],network[66],network[86],poll__networl[106],poll__networl[116],poll__networl[136],poll__networl[146],poll__networl[156],poll__networl[166],poll__networl[16],poll__networl[176],poll__networl[186],poll__networl[196],poll__networl[206],poll__networl[216],poll__networl[226],poll__networl[236],poll__networl[256],poll__networl[266],poll__networl[26],poll__networl[276],poll__networl[286],poll__networl[296],poll__networl[306],poll__networl[316],poll__networl[326],poll__networl[336],poll__networl[346],poll__networl[356],poll__networl[36],poll__networl[376],poll__networl[46],poll__networl[56],poll__networl[66],poll__networl[76],poll__networl[86],poll__networl[96],masterList[17],masterList[27],masterList[37],masterList[47],masterList[7],network[107],network[117],network[137],network[147],network[157],network[167],network[177],network[17],network[187],network[207],network[217],network[227],network[237],network[257],network[267],network[277],network[27],network[287],network[297],network[307],network[327],network[337],network[347],network[357],network[377],network[37],network[47],network[57],network[67],network[87],network[97],poll__networl[107],poll__networl[117],poll__networl[137],poll__networl[147],negotiation[38],negotiation[37],poll__networl[157],poll__networl[167],poll__networl[177],poll__networl[17],poll__networl[187],poll__networl[207],poll__networl[217],poll__networl[227],poll__networl[237],poll__networl[257],poll__networl[267],poll__networl[277],poll__networl[27],poll__networl[287],poll__networl[297],poll__networl[307],poll__networl[327],poll__networl[337],poll__networl[347],poll__networl[357],poll__networl[377],poll__networl[37],poll__networl[47],poll__networl[57],poll__networl[67],poll__networl[87],poll__networl[97],masterList[18],masterList[28],masterList[38],masterList[8],network[118],network[138],network[158],network[178],network[188],network[18],network[218],network[238],network[258],network[278],network[298],network[308],network[338],network[358],network[378],network[38],network[58],network[68],network[98],poll__networl[108],poll__networl[118],poll__networl[128],poll__networl[138],poll__networl[148],poll__networl[158],poll__networl[168],poll__networl[178],poll__networl[188],poll__networl[18],poll__networl[208],poll__networl[218],poll__networl[228],poll__networl[238],poll__networl[248],poll__networl[258],poll__networl[268],poll__networl[278],poll__networl[288],poll__networl[28],poll__networl[298],poll__networl[308],poll__networl[328],poll__networl[338],poll__networl[348],poll__networl[358],poll__networl[368],poll__networl[378],poll__networl[38],poll__networl[48],poll__networl[58],poll__networl[68],poll__networl[88],poll__networl[8],poll__networl[98],masterList[19],masterList[29],masterList[39],masterList[9],negotiation[9],network[109],network[119],network[129],network[139],network[159],network[169],network[179],network[189],network[19],network[209],network[219],network[229],network[239],network[249],network[259],network[279],network[289],network[299],network[309],network[329],network[339],network[349],network[359],network[369],network[379],network[39],network[49],network[59],network[69],network[89],network[99],network[9],poll__networl[109],poll__networl[119],poll__networl[129],poll__networl[139],poll__networl[159],poll__networl[169],poll__networl[179],poll__networl[189],poll__networl[19],poll__networl[209],poll__networl[219],poll__networl[229],poll__networl[239],poll__networl[249],poll__networl[259],poll__networl[279],poll__networl[289],poll__networl[299],poll__networl[309],poll__networl[329],poll__networl[339],poll__networl[349],poll__networl[359],poll__networl[369],poll__networl[379],poll__networl[39],poll__networl[49],poll__networl[59],poll__networl[69],poll__networl[89],poll__networl[99],poll__networl[9],

--------------------
content from /tmp/BenchKit_head_log_file.1749: