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=Vasy2003-PT-none
export BK_EXAMINATION=CTLCardinalityComparison
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1656
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/Vasy2003-PT-none
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is Vasy2003-PT-none, examination is CTLCardinalityComparison'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of marcie for Vasy2003/none (P/T)

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

execution on node 4: quadhexa-2.u-paris10.fr (runId=137107412600160_n_4)
=====================================================================
runnning marcie on Vasy2003-PT-none (CTLCardinalityComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is Vasy2003-PT-none, examination is CTLCardinalityComparison
=====================================================================

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

START 1371144134

Marcie rev. 1103M (build: rohrch on 2013-02-17)
A model checker for Generalized Stochastic Petri nets

authors: Alex Tovchigrechko (IDD package and CTL model checking)

Martin Schwarick (Symbolic numerical analysis and CSL model checking)

Christian Rohr (Simulative and approximative numerical model checking)

marcie@informatik.tu-cottbus.de

called as: marcie --net-file=model.pnml --mem=4 --mcc-file=CTLCardinalityComparison.txt

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 485 NrTr: 776)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 1m31sec


-> reachability set: #nodes 11506 (1.2e+04) #states 9,794,739,147,610,899,087,361 (21)



starting CTL model checker
--------------------------

checking: AG [[p179=p124 & p154=p418]]
normalized: ~ [E [true U ~ [[p179=p124 & p154=p418]]]]

-> the formula is FALSE

FORMULA p_1456_cardinalitycomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m1sec

checking: EF [[p179=p124 | p154=p418]]
normalized: E [true U [p179=p124 | p154=p418]]

-> the formula is FALSE

FORMULA p_1457_cardinalitycomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[p179=p124 & p154=p418]]
normalized: E [true U [p179=p124 & p154=p418]]

-> the formula is FALSE

FORMULA p_1458_cardinalitycomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[p179=p124 | p154=p418]]
normalized: ~ [EG [~ [[p179=p124 | p154=p418]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1459_cardinalitycomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [AG [[p154=p418 -> p179=p124]]]
normalized: E [true U ~ [E [true U ~ [[p179=p124 | ~ [p154=p418]]]]]]

-> the formula is TRUE

FORMULA p_1460_cardinalitycomparison_eq_x TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[p29<=p233 & p408<=p272]]
normalized: ~ [E [true U ~ [[p29<=p233 & p408<=p272]]]]

-> the formula is FALSE

FORMULA p_1461_cardinalitycomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[p29<=p233 | p408<=p272]]
normalized: EG [[p29<=p233 | p408<=p272]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1462_cardinalitycomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[p29<=p233 & p408<=p272]]
normalized: E [true U [p29<=p233 & p408<=p272]]

-> the formula is FALSE

FORMULA p_1463_cardinalitycomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 1m44sec

STOP 1371144238

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

check if there are places and transitions
ok
check if there are transitions without pre-places
ok
check if at least one transition is enabled in m0
ok
check if there are transitions that can never fire
ok


initing FirstDep: 0m0sec

1032 1317 2486 4390 6165 6422 6426 6667 6721 8431 8550 8527 8568 8532 8532 8620 8625 8929 8924 7069 7234 7249 7264 7278 7313 7289 7265 7370 7473 7571 7412 7414 7414 7514 7540 7556 7582 7584 7586 7586 7697 7723 7732 7791 7798 8405 7727 7882 7895 7755 7743 7745 7747 7749 7917 7848 7848 7850 7851 7852 7853 7854 7855 7867 7870 8039 8273 9935 9941 9951 10246 10258 10258 10287 10295 10256 10456 10588 10593 10592 10592 10592 10398 10720 10722 10723 10722 10718 10713 10854 10857 10858 10865 10863 10532 10746 11214 11219 11214 10879 10880 10896 10896 10861 10592 10864 10594 10867 10595 10869 10596 10611 10964 10631 10635 10992 10641 10829 10831 11039 10644 10835 10868 11126 10765 10959 11167 10767 10963 11166 10882 10770 10969 11177 10772 10973 10984 11192 10903 10785 10990 11190 11163 10788 10996 10998 11206 10791 11002 11004 11186 10805 11019 11228 10809 12931 16638 16638 16638 17110 17409 16767 16707 16701 16698 16693 16688 16666 16639 17167 17161 13235 13284 13286 13327 13298 13256 13210 13156 13443 13230 13226 13206 13382 13421 13050 13114 12944 12945 12946 13158 13197 13198 13201 13249 13255 13029 13185 12907 12909 12911 12913 13223 13232 12921 13242 13248 13252 13255 13258 13261 13264 12958 12961 12964 13016 14652 14652 14652 14911 13584 12960 12868 12863 12859 12854 12849 12828 12823 12799 12799 12799 13325 13319 11049 11272 11273 11009 10873 10873 10873 10873 10873 10873 10873 10873 10873 10873 10873 10873 11123 11124 10994 10919 10586 10586 10586 10586 10962 10930 10589 10590 9870 9870 9870 9875 9688 9694 9697 9755 9757 9760 9762 9774 9776 9778 9781 9794 9798 11334 11814 11817 11814 11397 11971 12109 14117 14117 14117 14874 14296 14233 14233 14233 14311 14233 14233 14233 14667 14668 14656 12574 12635 12609 12550 12543 12539 12545 12588 12505 12505 12693 12732 12716 12505 12505 12505 12505 12729 12768 12751 12505 12505 12505 12761 12806 12812 12555 12543 12855 12866 12583 12555 12557 12559 12884 12867 12865 12871 12873 12875 12914 12916 12918 12572 12575 12579 12579 14567 14591 14591 14591 15224 14647 14513 14509 14504 14500 14495 14482 14469 14443 14443 14443 14971 14965 14957 12886 12886 12888 12752 12754 12754 12754 12755 12755 12756 12755 12756 12480 12480 12480 12462 12462 12462 12331 12331 12331 12705 12670 12331 12331 12331 12331 12710 12331 12331 12331 12331 12331 12689 12727 12331 12331 12331 12441 12696 12734 12729 12331 12331 12331 12703 12741 12331 12331 12331 12709 12747 12745 12331 12331 12331 12331 12718 12719 12757 12754 11398 11398 11398 12303 11401 11403 11404 11406 11407 11409 11411 11413 11414 11434 11436 11437 11439 11440 11442 11443 11469 11446 11447 11449 11451 11452 11454 11455 11493 11480 11481 11482 11484 11485 11487 11489 11490 11491 11493 11494 11496 11497 11498 11500 11502 11503 11504 11506
iterations count:476190 (613), effective:6570 (8)

initing FirstDep: 0m0sec


iterations count:776 (1), effective:0 (0)

iterations count:776 (1), effective:0 (0)

iterations count:776 (1), effective:0 (0)

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