Execution Chart

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

Trace from the execution

Waiting for the VM to be ready (probing ssh)
............................................................................
=====================================================================
Generated by BenchKit 2-1667
Executing tool greatspn
Input is QuasiCertifProtocol-PT-06, examination is CTLFireability
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r04kn-qhx2-140043541601167
=====================================================================

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

BK_START 1400445148233
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running QuasiCertifProtocol (PT), instance 06
MODEL_DIR = /home/mcc/execution
CONVERT FORMULAE /home/mcc/execution/CTLFireability.xml INTO /home/mcc/execution/CTLFireability.rgmedd-ctl
BUILDING STRUCTURAL INFORMATIONS...
OK.
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-WES1 -h 2000000000 -B 10 -C -f /home/mcc/execution/CTLFireability.rgmedd-ctl
Using FORCE Heuristic for the variable ordering.
Setting MEDDLY cache to 2000000000 bytes.
Opening file: model.bnd
----------------------------------------
Start firing rule encoding
----------------------------------------
Encoding transition malC1_2 (0/116).
Encoding transition malC1_1 (1/116).
Encoding transition malC1_0 (2/116).
Encoding transition malC1_6 (3/116).
Encoding transition malC1_5 (4/116).
Encoding transition malC1_4 (5/116).
Encoding transition malC1_3 (6/116).
Encoding transition malS6_3 (7/116).
Encoding transition malS6_2 (8/116).
Encoding transition malS6_1 (9/116).
Encoding transition malS6_0 (10/116).
Encoding transition malS5_0 (11/116).
Encoding transition malS6_6 (12/116).
Encoding transition malS6_5 (13/116).
Encoding transition malS6_4 (14/116).
Encoding transition AgetTS (15/116).
Encoding transition AreqCS (16/116).
Encoding transition AackCS (17/116).
Encoding transition AstartCS (18/116).
Encoding transition AreqTS (19/116).
Encoding transition malS3_4 (20/116).
Encoding transition malS3_3 (21/116).
Encoding transition malS3_6 (22/116).
Encoding transition malS3_5 (23/116).
Encoding transition malS2_1 (24/116).
Encoding transition malS2_0 (25/116).
Encoding transition malS2_3 (26/116).
Encoding transition malS2_2 (27/116).
Encoding transition malS2_5 (28/116).
Encoding transition malS2_4 (29/116).
Encoding transition malS1_0 (30/116).
Encoding transition malS2_6 (31/116).
Encoding transition malS1_2 (32/116).
Encoding transition malS1_1 (33/116).
Encoding transition malS1_4 (34/116).
Encoding transition malS1_3 (35/116).
Encoding transition malS5_1 (36/116).
Encoding transition malS5_2 (37/116).
Encoding transition malS5_3 (38/116).
Encoding transition malS5_4 (39/116).
Encoding transition malS5_5 (40/116).
Encoding transition malS5_6 (41/116).
Encoding transition malS4_0 (42/116).
Encoding transition malS4_1 (43/116).
Encoding transition malS4_2 (44/116).
Encoding transition malS4_3 (45/116).
Encoding transition malS4_4 (46/116).
Encoding transition malS4_5 (47/116).
Encoding transition malS4_6 (48/116).
Encoding transition malS3_0 (49/116).
Encoding transition malS3_1 (50/116).
Encoding transition malS3_2 (51/116).
Encoding transition SsendTS_2 (52/116).
Encoding transition SsendTS_1 (53/116).
Encoding transition SsendTS_0 (54/116).
Encoding transition CsendTS1_6 (55/116).
Encoding transition CsendTS1_5 (56/116).
Encoding transition CsendTS1_4 (57/116).
Encoding transition CsendTS1_3 (58/116).
Encoding transition CsendTS1_2 (59/116).
Encoding transition SackCS_3 (60/116).
Encoding transition SackCS_2 (61/116).
Encoding transition SackCS_1 (62/116).
Encoding transition SackCS_0 (63/116).
Encoding transition SsendTS_6 (64/116).
Encoding transition SsendTS_5 (65/116).
Encoding transition SsendTS_4 (66/116).
Encoding transition SsendTS_3 (67/116).
Encoding transition malA1 (68/116).
Encoding transition CgenCertif_0 (69/116).
Encoding transition malA4 (70/116).
Encoding transition malA2 (71/116).
Encoding transition malA5 (72/116).
Encoding transition malA3 (73/116).
Encoding transition malS1_5 (74/116).
Encoding transition malS1_6 (75/116).
Encoding transition CsendTS1_0 (76/116).
Encoding transition CsendTS1_1 (77/116).
Encoding transition CgenCertif_5 (78/116).
Encoding transition CgenCertif_6 (79/116).
Encoding transition CgenCertif_3 (80/116).
Encoding transition CgenCertif_4 (81/116).
Encoding transition CgenCertif_1 (82/116).
Encoding transition CgenCertif_2 (83/116).
Encoding transition SgetTS_4 (84/116).
Encoding transition SgetTS_3 (85/116).
Encoding transition SgetTS_6 (86/116).
Encoding transition SgetTS_5 (87/116).
Encoding transition SgetTS_0 (88/116).
Encoding transition SreqTS_6 (89/116).
Encoding transition SgetTS_2 (90/116).
Encoding transition SgetTS_1 (91/116).
Encoding transition ScertCS_5 (92/116).
Encoding transition ScertCS_4 (93/116).
Encoding transition AendCS (94/116).
Encoding transition ScertCS_6 (95/116).
Encoding transition ScertCS_1 (96/116).
Encoding transition ScertCS_0 (97/116).
Encoding transition ScertCS_3 (98/116).
Encoding transition ScertCS_2 (99/116).
Encoding transition Sperform_1 (100/116).
Encoding transition Sperform_2 (101/116).
Encoding transition Sperform_3 (102/116).
Encoding transition Sperform_4 (103/116).
Encoding transition SackCS_4 (104/116).
Encoding transition SackCS_5 (105/116).
Encoding transition SackCS_6 (106/116).
Encoding transition Sperform_0 (107/116).
Encoding transition SreqTS_2 (108/116).
Encoding transition SreqTS_3 (109/116).
Encoding transition SreqTS_4 (110/116).
Encoding transition SreqTS_5 (111/116).
Encoding transition Sperform_5 (112/116).
Encoding transition Sperform_6 (113/116).
Encoding transition SreqTS_0 (114/116).
Encoding transition SreqTS_1 (115/116).
----------------------------------------
End firing rule encoding

----------------------------------------
----------------------------------------
Start RS generation
----------------------------------------

Total Used Memory: 29540KB
RS size: 2271960 (2.27196e+06)
----------------------------------------
End RS generation
----------------------------------------

FORMULA QuasiCertifProtocol-COL-06-CTLFireability-1 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA QuasiCertifProtocol-COL-06-CTLFireability-2 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA QuasiCertifProtocol-COL-06-CTLFireability-3 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA QuasiCertifProtocol-COL-06-CTLFireability-4 FALSE TECHNIQUES DECISION_DIAGRAMS
FORMULA QuasiCertifProtocol-COL-06-CTLFireability-5 FALSE TECHNIQUES DECISION_DIAGRAMS

BK_STOP 1400446606678

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

Cannot read input file model.bnd
createEGMDD: MEDDLY Error: Insufficient memory
Assertion failed at WN/SOURCE/CTL/CTL.cpp:1657
terminate called after throwing an instance of 'int'
/home/mcc/BenchKit/bin/greatspn_tool.sh: line 167: 1713 Aborted ~/BenchKit/bin/bin/RGMEDD model ${PLACE_ORDER} ${MEDDLY_CACHE} ${BOUND} -C -f ${NEW_FRM}

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.

set -x
# this is for BenchKit: configuration of major elements for the test
export BK_INPUT="QuasiCertifProtocol-PT-06"
export BK_EXAMINATION="CTLFireability"
export BK_TOOL="greatspn"
export BK_RESULT_DIR="/home/fko/BK_RESULTS/OUTPUTS"
export BK_TIME_CONFINEMENT="3600"

# this is specific to your benchmark or test

export BIN_DIR="$HOME/BenchKit/bin"

# remove the execution directoty if it exists (to avoid increse of .vmdk images)
if [ -d execution ] ; then
rm -rf execution
fi

tar xzf /home/mcc/BenchKit/INPUTS/QuasiCertifProtocol-PT-06.tgz
mv QuasiCertifProtocol-PT-06 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1667"
echo " Executing tool greatspn"
echo " Input is QuasiCertifProtocol-PT-06, examination is CTLFireability"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r04kn-qhx2-140043541601167"
echo "====================================================================="
echo
echo "--------------------"
echo "content from stdout:"
echo
echo -n "BK_START "
date -u +%s%3N
timeout -s 9 $BK_TIME_CONFINEMENT bash -c "/home/mcc/BenchKit/BenchKit_head.sh 2> STDERR ; echo ; echo -n \"BK_STOP \" ; date -u +%s%3N"
if [ $? -eq 137 ] ; then
echo
echo "BK_TIME_CONFINEMENT_REACHED"
fi
echo
echo "--------------------"
echo "content from stderr:"
echo
cat STDERR ;