Introduction

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=Peterson-COL-5
export BK_EXAMINATION=StateSpace
export BK_TOOL=ITS-Tools
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1750
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/Peterson-COL-5
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool ITS-Tools:'
echo ' Test is Peterson-COL-5, examination is StateSpace'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of ITS-Tools for Peterson/5 (Colored)

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

execution on node 27: cluster1u29.lip6.fr (runId=136966894901840_n_27)
=====================================================================
runnning ITS-Tools on Peterson-COL-5 (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 Peterson-COL-5, examination is StateSpace
=====================================================================

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

START 1370199379
its-reach command run as :

/home/mcc/BenchKit/bin/its-reach -i model.sep.flat.gal -t GAL --quiet
STATE_SPACE TECHNIQUES DECISION_DIAGRAMS
STOP 1370199823

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

initial cost 244803
final cost 101529
TestIdentity[31],TestIdentity[37],TestIdentity[43],BeginLoop[31],TestIdentity[49],BeginLoop[1],BeginLoop[37],BeginLoop[43],BeginLoop[61],BeginLoop[151],BeginLoop[121],BeginLoop[49],BeginLoop[91],BeginLoop[127],BeginLoop[157],TestIdentity[1],BeginLoop[7],BeginLoop[67],TestIdentity[61],BeginLoop[97],TestIdentity[121],TestIdentity[151],BeginLoop[62],TestIdentity[91],BeginLoop[32],IsEndLoop[31],BeginLoop[73],TestIdentity[127],BeginLoop[133],TestIdentity[7],TestIdentity[157],BeginLoop[163],BeginLoop[103],IsEndLoop[37],BeginLoop[122],TestIdentity[67],IsEndLoop[61],TestIdentity[97],BeginLoop[13],BeginLoop[2],BeginLoop[92],IsEndLoop[121],TestIdentity[55],IsEndLoop[1],TestIdentity[73],IsEndLoop[43],IsEndLoop[91],BeginLoop[38],BeginLoop[152],TestIdentity[133],BeginLoop[79],IsEndLoop[151],TestIdentity[163],BeginLoop[55],TestIdentity[103],TestIdentity[13],BeginLoop[139],IsEndLoop[127],IsEndLoop[49],BeginLoop[128],IsEndLoop[7],BeginLoop[74],IsEndLoop[0],BeginLoop[8],IsEndLoop[73],IsEndLoop[157],IsEndLoop[30],IsEndLoop[67],BeginLoop[109],BeginLoop[68],BeginLoop[44],BeginLoop[158],IsEndLoop[60],TestIdentity[79],IsEndLoop[150],BeginLoop[169],IsEndLoop[120],IsEndLoop[90],IsEndLoop[36],TestIdentity[139],IsEndLoop[126],IsEndLoop[156],IsEndLoop[66],IsEndLoop[97],IsEndLoop[96],IsEndLoop[42],TestIdentity[0],TestIdentity[62],IsEndLoop[6],IsEndLoop[13],TestIdentity[109],IsEndLoop[79],IsEndLoop[72],IsEndLoop[48],TestIdentity[169],IsEndLoop[132],IsEndLoop[133],BeginLoop[50],IsEndLoop[162],IsEndLoop[102],BeginLoop[80],BeginLoop[98],IsEndLoop[55],IsEndLoop[163],IsEndLoop[103],BeginLoop[14],TestIdentity[32],IsEndLoop[78],WantSection[2],IsEndLoop[12],TestAlone[1],IsEndLoop[138],TestAlone[61],TestIdentity[122],BeginLoop[134],TestAlone[121],IsEndLoop[139],TestAlone[151],TestAlone[91],BeginLoop[19],BeginLoop[145],TestIdentity[2],IsEndLoop[108],TestIdentity[92],IsEndLoop[169],TestIdentity[19],IsEndLoop[109],IsEndLoop[168],TestAlone[127],IsEndLoop[54],BeginLoop[164],TestAlone[7],TestIdentity[152],BeginLoop[115],TestAlone[157],IsEndLoop[19],TestIdentity[6],TestAlone[67],BeginLoop[104],TestIdentity[74],BeginLoop[175],TestIdentity[145],TestAlone[97],TestIdentity[38],TestIdentity[128],TestIdentity[68],TestAlone[73],BeginLoop[85],TestIdentity[8],IsEndLoop[145],BeginLoop[140],TestIdentity[115],TestAlone[13],IsEndLoop[175],TestAlone[133],TestIdentity[175],TestIdentity[158],TestAlone[163],TestAlone[103],IsEndLoop[115],BeginLoop[170],BeginLoop[56],IsEndLoop[144],BeginLoop[110],WantSection[0],TestIdentity[85],IsEndLoop[25],TestAlone[31],BeginLoop[20],TestAlone[79],IsEndLoop[114],TestIdentity[44],IsEndLoop[174],TestIdentity[12],IsEndLoop[18],TestAlone[139],TestIdentity[80],IsEndLoop[85],IsEndLoop[84],TestAlone[37],TestAlone[109],TestAlone[169],BeginLoop[146],TestIdentity[98],TestIdentity[30],TestAlone[30],BeginLoop[25],BeginLoop[176],TestIdentity[25],TestAlone[60],BeginLoop[0],TestAlone[19],TestIdentity[60],TestIdentity[14],TestAlone[43],TestAlone[150],TestAlone[0],BeginLoop[116],TestAlone[120],TestIdentity[134],TestIdentity[150],TestAlone[90],TestIdentity[50],BeginLoop[26],Idle[1],TestIdentity[120],TestIdentity[90],TestAlone[49],TestAlone[126],TestAlone[156],TestAlone[145],TestAlone[36],TestIdentity[164],TestAlone[66],TestAlone[6],TestAlone[96],TestAlone[115],TestAlone[175],TestIdentity[126],IsEndLoop[24],TestIdentity[156],TestAlone[85],TestIdentity[66],TestIdentity[104],TestIdentity[36],IsEndLoop[62],TestAlone[25],TestIdentity[96],TestAlone[72],BeginLoop[86],TestIdentity[140],TestAlone[42],TestAlone[132],TestAlone[12],TestAlone[55],TestAlone[162],TestAlone[102],AskForSection[5],TestIdentity[170],BeginLoop[30],Idle[0],TestIdentity[20],TestIdentity[110],BeginLoop[6],BeginLoop[60],TestIdentity[18],TestAlone[138],TestAlone[78],TestAlone[48],BeginLoop[150],TestAlone[108],AskForSection[0],TestIdentity[56],TestIdentity[72],TestAlone[168],BeginLoop[120],TestAlone[18],BeginLoop[90],TestIdentity[132],TestIdentity[42],TestIdentity[146],TestIdentity[162],TestIdentity[102],TestAlone[32],TestIdentity[176],TestAlone[122],TestAlone[2],WantSection[3],IsEndLoop[74],IsEndLoop[68],TestIdentity[26],TestAlone[152],TestAlone[92],TestIdentity[116],BeginLoop[126],TestAlone[24],BeginLoop[156],BeginLoop[66],TestAlone[54],BeginLoop[36],TestAlone[128],BeginLoop[96],TestAlone[8],BeginLoop[12],TestIdentity[138],BeginLoop[63],TestAlone[144],TestIdentity[78],Turn[0],TestAlone[38],TestAlone[158],TestAlone[114],Turn[1],TestAlone[174],IsEndLoop[80],TestIdentity[108],TestIdentity[48],TestAlone[84],Turn[2],WantSection[1],TestIdentity[168],TestAlone[62],CS[1],TestIdentity[24],TestIdentity[86],EndTurn[0],Turn[5],EndTurn[5],TestAlone[44],AskForSection[1],EndTurn[10],EndTurn[20],Turn[3],Turn[4],EndTurn[15],TestAlone[98],AskForSection[21],TestAlone[14],EndTurn[25],AskForSection[11],AskForSection[6],TestAlone[134],BeginLoop[72],AskForSection[26],TestTurn[0],AskForSection[10],AskForSection[16],TestAlone[68],BeginLoop[132],TestAlone[164],BeginLoop[42],TestTurn[5],BeginLoop[162],BeginLoop[102],TestTurn[10],CS[0],IsEndLoop[122],TestAlone[74],TestAlone[50],TestTurn[25],IsEndLoop[2],IsEndLoop[32],TestTurn[20],TestAlone[140],TestTurn[15],TestAlone[104],Turn[6],IsEndLoop[152],Turn[10],Turn[11],TestAlone[20],Turn[8],Turn[7],Turn[9],TestAlone[170],BeginLoop[18],WantSection[4],TestAlone[80],TestAlone[110],Idle[2],EndTurn[1],IsEndLoop[128],WantSection[5],EndTurn[21],TestTurn[1],IsEndLoop[8],IsEndLoop[92],BeginLoop[69],TestIdentity[54],TestIdentity[144],TestTurn[21],EndTurn[11],BeginLoop[75],EndTurn[6],TestTurn[26],TestTurn[11],TestAlone[56],TestAlone[146],BeginLoop[138],EndTurn[16],TestTurn[6],TestIdentity[114],TestTurn[16],TestAlone[176],BeginLoop[78],EndTurn[26],TestAlone[26],AskForSection[2],TestIdentity[174],AskForSection[22],BeginLoop[108],IsEndLoop[158],AskForSection[12],BeginLoop[48],TestIdentity[84],BeginLoop[168],IsEndLoop[38],AskForSection[7],TestAlone[116],AskForSection[17],AskForSection[27],TestIdentity[63],Turn[12],BeginLoop[81],Turn[14],Turn[16],Turn[17],BeginLoop[123],Turn[13],Turn[15],TestAlone[86],TestTurn[12],TestTurn[2],BeginLoop[3],TestTurn[22],IsEndLoop[44],IsEndLoop[86],TestTurn[27],TestTurn[7],TestTurn[17],BeginLoop[33],IsEndLoop[14],EndTurn[12],BeginLoop[153],EndTurn[2],EndTurn[22],EndTurn[17],BeginLoop[24],EndTurn[7],IsEndLoop[134],AskForSection[25],IsEndLoop[164],IsEndLoop[5],IsEndLoop[35],IsEndLoop[65],CS[2],EndTurn[27],IsEndLoop[125],IsEndLoop[95],IsEndLoop[140],AskForSection[13],AskForSection[23],AskForSection[3],AskForSection[18],AskForSection[8],IsEndLoop[50],TestTurn[23],IsEndLoop[20],BeginLoop[129],AskForSection[28],TestTurn[13],BeginLoop[9],TestTurn[3],IsEndLoop[170],TestTurn[18],TestTurn[28],TestTurn[8],IsEndLoop[98],Turn[18],Turn[22],Turn[20],BeginLoop[144],Turn[21],Turn[19],BeginLoop[54],Turn[23],IsEndLoop[146],IsEndLoop[11],BeginLoop[114],BeginLoop[93],TestAlone[155],BeginLoop[174],IsEndLoop[176],IsEndLoop[26],IsEndLoop[131],IsEndLoop[71],IsEndLoop[56],BeginLoop[159],EndTurn[23],BeginLoop[84],IsEndLoop[41],TestIdentity[69],IsEndLoop[101],EndTurn[13],EndTurn[3],AskForSection[15],IsEndLoop[155],EndTurn[18],EndTurn[8],BeginLoop[39],IsEndLoop[104],TestIdentity[75],EndTurn[28],IsEndLoop[110],TestIdentity[3],TestIdentity[123],TestAlone[161],TestTurn[4],WantSection[11],TestTurn[9],TestIdentity[33],TestIdentity[153],TestAlone[5],TestAlone[35],TestAlone[65],TestTurn[24],TestAlone[95],TestTurn[14],IsEndLoop[77],TestTurn[29],AskForSection[20],EndTurn[9],TestTurn[19],IsEndLoop[17],TestAlone[125],AskForSection[24],IsEndLoop[107],AskForSection[4],EndTurn[4],IsEndLoop[137],IsEndLoop[47],TestIdentity[81],AskForSection[14],AskForSection[9],AskForSection[19],TestAlone[167],BeginLoop[45],IsEndLoop[116],Idle[5],AskForSection[29],TestAlone[63],IsEndLoop[161],BeginLoop[15],Turn[28],Turn[24],TestAlone[11],Turn[27],Turn[29],WantSection[7],Turn[26],Turn[25],TestIdentity[9],TestIdentity[129],EndTurn[14],BeginLoop[135],TestAlone[71],TestAlone[41],BeginLoop[165],TestAlone[131],TestAlone[101],TestAlone[173],IsEndLoop[143],IsEndLoop[83],TestIdentity[159],IsEndLoop[23],WantSection[10],BeginLoop[87],IsEndLoop[113],BeginLoop[141],TestAlone[3],IsEndLoop[53],CS[5],TestAlone[33],TestAlone[77],TestIdentity[39],EndTurn[29],TestAlone[153],EndTurn[19],BeginLoop[21],TestAlone[17],EndTurn[24],TestAlone[123],TestAlone[107],BeginLoop[51],TestAlone[47],TestAlone[93],TestAlone[69],BeginLoop[171],TestAlone[179],WantSection[9],IsEndLoop[59],TestIdentity[93],TestAlone[137],IsEndLoop[29],IsEndLoop[167],TestAlone[75],BeginLoop[147],TestAlone[9],IsEndLoop[89],TestAlone[159],TestAlone[83],BeginLoop[27],TestAlone[113],TestAlone[23],TestAlone[129],BeginLoop[177],TestAlone[143],TestAlone[53],TestIdentity[155],TestAlone[39],BeginLoop[57],TestIdentity[45],TestIdentity[15],IsEndLoop[119],TestAlone[81],IsEndLoop[149],TestAlone[99],BeginLoop[99],Idle[3],TestIdentity[135],TestIdentity[165],TestIdentity[5],CS[3],TestIdentity[95],TestAlone[29],TestAlone[59],TestIdentity[65],TestIdentity[35],TestAlone[15],TestAlone[45],IsEndLoop[173],TestAlone[89],TestAlone[105],TestIdentity[141],TestAlone[165],TestAlone[124],TestAlone[135],TestAlone[119],TestAlone[149],TestIdentity[21],TestIdentity[125],TestAlone[111],TestAlone[94],TestIdentity[51],TestIdentity[87],TestAlone[4],TestAlone[141],TestIdentity[171],TestAlone[21],TestIdentity[161],TestAlone[154],TestAlone[64],TestAlone[171],TestAlone[51],BeginLoop[105],TestAlone[130],CS[4],TestAlone[34],TestIdentity[11],BeginLoop[111],TestIdentity[147],IsEndLoop[93],Idle[4],TestIdentity[27],TestAlone[87],TestAlone[117],TestAlone[27],TestAlone[147],TestIdentity[71],TestAlone[136],TestIdentity[177],IsEndLoop[179],TestAlone[57],TestIdentity[57],TestIdentity[41],TestAlone[177],TestAlone[160],TestAlone[10],TestIdentity[101],TestAlone[70],TestAlone[142],BeginLoop[155],IsEndLoop[63],TestAlone[40],TestIdentity[94],BeginLoop[95],BeginLoop[5],TestAlone[100],IsEndLoop[3],BeginLoop[94],BeginLoop[65],TestIdentity[77],BeginLoop[117],TestAlone[148],BeginLoop[35],TestIdentity[131],IsEndLoop[153],TestAlone[76],TestIdentity[17],WantSection[6],TestAlone[16],IsEndLoop[33],TestIdentity[107],TestAlone[46],TestIdentity[4],TestIdentity[47],TestAlone[166],TestAlone[106],TestIdentity[64],TestIdentity[99],IsEndLoop[154],IsEndLoop[94],TestIdentity[154],IsEndLoop[4],BeginLoop[161],IsEndLoop[64],TestAlone[82],TestIdentity[167],BeginLoop[64],IsEndLoop[69],BeginLoop[4],IsEndLoop[34],BeginLoop[125],TestAlone[112],TestAlone[22],BeginLoop[11],IsEndLoop[9],IsEndLoop[159],TestAlone[52],TestIdentity[34],TestAlone[172],BeginLoop[154],IsEndLoop[123],TestIdentity[83],TestIdentity[137],BeginLoop[71],TestIdentity[113],IsEndLoop[160],BeginLoop[41],TestIdentity[23],IsEndLoop[75],TestAlone[28],IsEndLoop[39],TestAlone[58],IsEndLoop[10],BeginLoop[34],TestIdentity[53],TestAlone[88],BeginLoop[101],TestIdentity[105],TestAlone[118],TestAlone[178],IsEndLoop[70],IsEndLoop[99],IsEndLoop[40],WantSection[8],TestIdentity[143],TestIdentity[111],TestIdentity[160],IsEndLoop[100],TestIdentity[70],TestIdentity[10],IsEndLoop[15],IsEndLoop[81],IsEndLoop[45],BeginLoop[77],TestIdentity[29],IsEndLoop[124],IsEndLoop[129],IsEndLoop[165],TestIdentity[59],BeginLoop[17],TestIdentity[173],IsEndLoop[76],TestIdentity[89],BeginLoop[70],IsEndLoop[16],IsEndLoop[105],BeginLoop[160],BeginLoop[10],TestIdentity[119],TestIdentity[40],BeginLoop[107],IsEndLoop[21],IsEndLoop[135],BeginLoop[47],IsEndLoop[171],IsEndLoop[106],IsEndLoop[46],IsEndLoop[51],IsEndLoop[111],TestIdentity[149],IsEndLoop[141],TestIdentity[76],BeginLoop[131],IsEndLoop[27],IsEndLoop[87],IsEndLoop[166],TestIdentity[100],IsEndLoop[57],TestIdentity[117],BeginLoop[167],IsEndLoop[147],IsEndLoop[177],BeginLoop[40],IsEndLoop[82],TestIdentity[16],TestIdentity[179],IsEndLoop[112],BeginLoop[76],IsEndLoop[22],TestIdentity[46],IsEndLoop[117],BeginLoop[83],BeginLoop[124],IsEndLoop[52],TestIdentity[166],BeginLoop[113],IsEndLoop[130],BeginLoop[23],BeginLoop[100],TestIdentity[106],TestIdentity[82],IsEndLoop[172],BeginLoop[53],BeginLoop[137],TestIdentity[124],IsEndLoop[28],IsEndLoop[58],BeginLoop[16],IsEndLoop[88],IsEndLoop[118],IsEndLoop[136],BeginLoop[46],TestIdentity[112],TestIdentity[22],BeginLoop[166],IsEndLoop[178],TestIdentity[52],BeginLoop[82],TestIdentity[172],IsEndLoop[142],BeginLoop[29],BeginLoop[173],BeginLoop[143],BeginLoop[59],BeginLoop[106],TestIdentity[28],BeginLoop[89],TestIdentity[58],IsEndLoop[148],TestIdentity[88],BeginLoop[119],TestIdentity[178],TestIdentity[118],BeginLoop[22],BeginLoop[112],BeginLoop[172],BeginLoop[52],BeginLoop[130],BeginLoop[149],BeginLoop[28],BeginLoop[179],BeginLoop[58],BeginLoop[88],BeginLoop[136],BeginLoop[178],BeginLoop[142],BeginLoop[118],TestIdentity[130],BeginLoop[148],TestIdentity[136],TestIdentity[142],TestIdentity[148],
sparsehash FATAL ERROR: failed to allocate 41 groups

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