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-048, examination is CTLCardinality
Time confinement is 3600 seconds
Memory confinement is 6144 MBytes
Run identifier is r21sr-ovh1-140191459800216
=====================================================================

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

BK_START 1401920614548
======================================================
== This is GreatSPN, running for the MCC'2014 ==
======================================================
Running CircularTrains (PT), instance 048
MODEL_DIR = /home/mcc/execution
CONVERT PNML /home/mcc/execution/model.pnml
COMPUTING STRUCTURAL INFO.
CONVERT FORMULAE /home/mcc/execution/CTLCardinality.xml INTO /home/mcc/execution/CTLCardinality.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/CTLCardinality.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 t16_to_17 (0/48).
Encoding transition t46_to_47 (1/48).
Encoding transition t7_to_8 (2/48).
Encoding transition t10_to_11 (3/48).
Encoding transition t13_to_14 (4/48).
Encoding transition t22_to_23 (5/48).
Encoding transition t43_to_44 (6/48).
Encoding transition t18_to_19 (7/48).
Encoding transition t41_to_42 (8/48).
Encoding transition t34_to_35 (9/48).
Encoding transition t4_to_5 (10/48).
Encoding transition t11_to_12 (11/48).
Encoding transition t6_to_7 (12/48).
Encoding transition t45_to_46 (13/48).
Encoding transition t32_to_33 (14/48).
Encoding transition t9_to_10 (15/48).
Encoding transition t29_to_30 (16/48).
Encoding transition t8_to_9 (17/48).
Encoding transition t20_to_21 (18/48).
Encoding transition t30_to_31 (19/48).
Encoding transition t47_to_48 (20/48).
Encoding transition t23_to_24 (21/48).
Encoding transition t15_to_16 (22/48).
Encoding transition t2_to_3 (23/48).
Encoding transition t24_to_25 (24/48).
Encoding transition t48_to_1 (25/48).
Encoding transition t39_to_40 (26/48).
Encoding transition t42_to_43 (27/48).
Encoding transition t33_to_34 (28/48).
Encoding transition t36_to_37 (29/48).
Encoding transition t27_to_28 (30/48).
Encoding transition t19_to_20 (31/48).
Encoding transition t12_to_13 (32/48).
Encoding transition t5_to_6 (33/48).
Encoding transition t44_to_45 (34/48).
Encoding transition t17_to_18 (35/48).
Encoding transition t21_to_22 (36/48).
Encoding transition t3_to_4 (37/48).
Encoding transition t14_to_15 (38/48).
Encoding transition t28_to_29 (39/48).
Encoding transition t40_to_41 (40/48).
Encoding transition t35_to_36 (41/48).
Encoding transition t26_to_27 (42/48).
Encoding transition t37_to_38 (43/48).
Encoding transition t1_to_2 (44/48).
Encoding transition t31_to_32 (45/48).
Encoding transition t25_to_26 (46/48).
Encoding transition t38_to_39 (47/48).
----------------------------------------
End firing rule encoding

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

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

Ok.

BK_STOP 1401921162441

--------------------
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 * 048: value too great for base (error token is "048")
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-048"
export BK_EXAMINATION="CTLCardinality"
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-048.tgz
mv CircularTrains-PT-048 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-048, examination is CTLCardinality"
echo " Time confinement is $BK_TIME_CONFINEMENT seconds"
echo " Memory confinement is 6144 MBytes"
echo " Run identifier is r21sr-ovh1-140191459800216"
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 ;