fond
Model Checking Contest @ Petri Nets 2014
Tunis, Tunisia, June 24, 2014
Execution Report for Run r21sr-ovh1-140191459800231
Last Updated
Sept. 1, 2014

About the Execution

Execution Summary
Max Memory
Used (MB)
CPU Usage (ms) I/O Wait (ms) Competition Result Execution
Status
182.86 547136 668.5 CC normal

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-1668
Executing tool greatspn
Input is CircularTrains-PT-096, examination is CTLFireability
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r21sr-ovh1-140191459800231
=====================================================================


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

BK_START 1401920655037
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running CircularTrains (PT), instance 096
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/CTLFireability.xml INTO /home/mcc/execution/CTLFireability.rgmedd-ctl
Instance is not an integer.
BUILDING STRUCTURAL INFORMATIONS...
OK.
/home/mcc/BenchKit/bin/bin/RGMEDD model -FORCE-WES1 -h 2000000000 -B 1 -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 t66_to_67 (0/96).
Encoding transition t16_to_17 (1/96).
Encoding transition t59_to_60 (2/96).
Encoding transition t46_to_47 (3/96).
Encoding transition t7_to_8 (4/96).
Encoding transition t10_to_11 (5/96).
Encoding transition t13_to_14 (6/96).
Encoding transition t22_to_23 (7/96).
Encoding transition t43_to_44 (8/96).
Encoding transition t18_to_19 (9/96).
Encoding transition t52_to_53 (10/96).
Encoding transition t80_to_81 (11/96).
Encoding transition t41_to_42 (12/96).
Encoding transition t49_to_50 (13/96).
Encoding transition t34_to_35 (14/96).
Encoding transition t91_to_92 (15/96).
Encoding transition t4_to_5 (16/96).
Encoding transition t11_to_12 (17/96).
Encoding transition t64_to_65 (18/96).
Encoding transition t6_to_7 (19/96).
Encoding transition t82_to_83 (20/96).
Encoding transition t45_to_46 (21/96).
Encoding transition t32_to_33 (22/96).
Encoding transition t9_to_10 (23/96).
Encoding transition t29_to_30 (24/96).
Encoding transition t73_to_74 (25/96).
Encoding transition t89_to_90 (26/96).
Encoding transition t8_to_9 (27/96).
Encoding transition t20_to_21 (28/96).
Encoding transition t30_to_31 (29/96).
Encoding transition t47_to_48 (30/96).
Encoding transition t23_to_24 (31/96).
Encoding transition t15_to_16 (32/96).
Encoding transition t86_to_87 (33/96).
Encoding transition t2_to_3 (34/96).
Encoding transition t87_to_88 (35/96).
Encoding transition t54_to_55 (36/96).
Encoding transition t84_to_85 (37/96).
Encoding transition t50_to_51 (38/96).
Encoding transition t24_to_25 (39/96).
Encoding transition t57_to_58 (40/96).
Encoding transition t78_to_79 (41/96).
Encoding transition t75_to_76 (42/96).
Encoding transition t48_to_49 (43/96).
Encoding transition t60_to_61 (44/96).
Encoding transition t39_to_40 (45/96).
Encoding transition t69_to_70 (46/96).
Encoding transition t63_to_64 (47/96).
Encoding transition t42_to_43 (48/96).
Encoding transition t96_to_1 (49/96).
Encoding transition t33_to_34 (50/96).
Encoding transition t36_to_37 (51/96).
Encoding transition t27_to_28 (52/96).
Encoding transition t65_to_66 (53/96).
Encoding transition t72_to_73 (54/96).
Encoding transition t19_to_20 (55/96).
Encoding transition t58_to_59 (56/96).
Encoding transition t93_to_94 (57/96).
Encoding transition t90_to_91 (58/96).
Encoding transition t12_to_13 (59/96).
Encoding transition t5_to_6 (60/96).
Encoding transition t51_to_52 (61/96).
Encoding transition t81_to_82 (62/96).
Encoding transition t44_to_45 (63/96).
Encoding transition t17_to_18 (64/96).
Encoding transition t21_to_22 (65/96).
Encoding transition t3_to_4 (66/96).
Encoding transition t14_to_15 (67/96).
Encoding transition t76_to_77 (68/96).
Encoding transition t28_to_29 (69/96).
Encoding transition t56_to_57 (70/96).
Encoding transition t53_to_54 (71/96).
Encoding transition t79_to_80 (72/96).
Encoding transition t85_to_86 (73/96).
Encoding transition t67_to_68 (74/96).
Encoding transition t40_to_41 (75/96).
Encoding transition t92_to_93 (76/96).
Encoding transition t35_to_36 (77/96).
Encoding transition t62_to_63 (78/96).
Encoding transition t70_to_71 (79/96).
Encoding transition t26_to_27 (80/96).
Encoding transition t55_to_56 (81/96).
Encoding transition t61_to_62 (82/96).
Encoding transition t77_to_78 (83/96).
Encoding transition t37_to_38 (84/96).
Encoding transition t95_to_96 (85/96).
Encoding transition t1_to_2 (86/96).
Encoding transition t88_to_89 (87/96).
Encoding transition t31_to_32 (88/96).
Encoding transition t68_to_69 (89/96).
Encoding transition t71_to_72 (90/96).
Encoding transition t94_to_95 (91/96).
Encoding transition t83_to_84 (92/96).
Encoding transition t25_to_26 (93/96).
Encoding transition t74_to_75 (94/96).
Encoding transition t38_to_39 (95/96).
----------------------------------------
End firing rule encoding

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

Total Used Memory: 6268KB
RS size: 1 (1)
----------------------------------------
End RS generation
----------------------------------------

Ok.

BK_STOP 1401921203750

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

javax.xml.bind.UnmarshalException: unexpected element (uri:"http://mcc.lip6.fr/", local:"property-set"). Expected elements are <{}all-paths>,<{}before>,<{}boolean-formula>,<{}conjunction>,<{}deadlock>,<{}description>,<{}disjunction>,<{}equivalence>,<{}exclusive-disjunction>,<{}exists-path>,<{}expected-result>,<{}explanation>,<{}false>,<{}finally>,<{}formula>,<{}globally>,<{}id>,<{}if-no-successor>,<{}implication>,<{}impossibility>,<{}integer-constant>,<{}integer-difference>,<{}integer-division>,<{}integer-eq>,<{}integer-expression>,<{}integer-formula>,<{}integer-ge>,<{}integer-gt>,<{}integer-le>,<{}integer-lt>,<{}integer-ne>,<{}integer-product>,<{}integer-sum>,<{}invariant>,<{}is-ctl>,<{}is-fireable>,<{}is-live>,<{}is-ltl>,<{}is-reachability>,<{}is-structural>,<{}level>,<{}negation>,<{}next>,<{}place>,<{}place-bound>,<{}possibility>,<{}property>,<{}property-set>,<{}reach>,<{}steps>,<{}strength>,<{}tags>,<{}tokens-count>,<{}transition>,<{}true>,<{}until>,<{}value>
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallingContext.handleEvent(UnmarshallingContext.java:647)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.Loader.reportError(Loader.java:243)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.Loader.reportError(Loader.java:238)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.Loader.reportUnexpectedChildElement(Loader.java:105)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallingContext$DefaultRootLoader.childElement(UnmarshallingContext.java:1048)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallingContext._startElement(UnmarshallingContext.java:483)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallingContext.startElement(UnmarshallingContext.java:465)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.SAXConnector.startElement(SAXConnector.java:135)
at com.sun.org.apache.xerces.internal.parsers.AbstractSAXParser.startElement(AbstractSAXParser.java:506)
at com.sun.org.apache.xerces.internal.impl.XMLNSDocumentScannerImpl.scanStartElement(XMLNSDocumentScannerImpl.java:376)
at com.sun.org.apache.xerces.internal.impl.XMLNSDocumentScannerImpl$NSContentDriver.scanRootElementHook(XMLNSDocumentScannerImpl.java:602)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl$FragmentContentDriver.next(XMLDocumentFragmentScannerImpl.java:3063)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentScannerImpl$PrologDriver.next(XMLDocumentScannerImpl.java:881)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentScannerImpl.next(XMLDocumentScannerImpl.java:607)
at com.sun.org.apache.xerces.internal.impl.XMLNSDocumentScannerImpl.next(XMLNSDocumentScannerImpl.java:116)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl.scanDocument(XMLDocumentFragmentScannerImpl.java:488)
at com.sun.org.apache.xerces.internal.parsers.XML11Configuration.parse(XML11Configuration.java:835)
at com.sun.org.apache.xerces.internal.parsers.XML11Configuration.parse(XML11Configuration.java:764)
at com.sun.org.apache.xerces.internal.parsers.XMLParser.parse(XMLParser.java:123)
at com.sun.org.apache.xerces.internal.parsers.AbstractSAXParser.parse(AbstractSAXParser.java:1210)
at com.sun.org.apache.xerces.internal.jaxp.SAXParserImpl$JAXPSAXParser.parse(SAXParserImpl.java:568)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallerImpl.unmarshal0(UnmarshallerImpl.java:202)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallerImpl.unmarshal(UnmarshallerImpl.java:174)
at javax.xml.bind.helpers.AbstractUnmarshallerImpl.unmarshal(AbstractUnmarshallerImpl.java:157)
at javax.xml.bind.helpers.AbstractUnmarshallerImpl.unmarshal(AbstractUnmarshallerImpl.java:214)
at Main.convert(Main.java:194)
at Main.main(Main.java:229)
/home/mcc/BenchKit/bin/greatspn_tool.sh: line 133: 3 * 096: value too great for base (error token is "096")
Cannot read input file model.bnd

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="CircularTrains-PT-096"
export BK_EXAMINATION="CTLFireability"
export BK_TOOL="greatspn"
export BK_RESULT_DIR="/srv/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/CircularTrains-PT-096.tgz
mv CircularTrains-PT-096 execution

# this is for BenchKit: explicit launching of the test

cd execution
echo "====================================================================="
echo " Generated by BenchKit 2-1668"
echo " Executing tool greatspn"
echo " Input is CircularTrains-PT-096, examination is CTLFireability"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r21sr-ovh1-140191459800231"
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 ;