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=ReachabilityFireability
export BK_TOOL=marcie
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1666
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 ReachabilityFireability'
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=137107412400048_n_4)
=====================================================================
runnning marcie on Vasy2003-PT-none (ReachabilityFireability)
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 ReachabilityFireability
=====================================================================

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

START 1371121755

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=ReachabilityFireability.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: 1m51sec


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



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

checking: ~ [~ [EF [p481 \in [1, oo) && p306 \in [1, oo)]]]
normalized: E [true U p481 \in [1, oo) && p306 \in [1, oo)]

-> the formula is TRUE

FORMULA Property_7_Is_transition_t517_fireable_Result_Unknown TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m51sec

checking: ~ [~ [EF [p483 \in [1, oo) && p248 \in [1, oo)]]]
normalized: E [true U p483 \in [1, oo) && p248 \in [1, oo)]

-> the formula is TRUE

FORMULA Property_8_Is_transition_t550_fireable_Result_Unknown TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m41sec

checking: AG [[p483 \in [1, oo) && p306 \in [1, oo) & p262 \in [1, oo) && p124 \in [1, oo)]]
normalized: ~ [E [true U ~ [[p483 \in [1, oo) && p306 \in [1, oo) & p262 \in [1, oo) && p124 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_4_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[p483 \in [1, oo) && p306 \in [1, oo) | p262 \in [1, oo) && p124 \in [1, oo)]]
normalized: ~ [E [true U ~ [[p483 \in [1, oo) && p306 \in [1, oo) | p262 \in [1, oo) && p124 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_5_fireability_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[p483 \in [1, oo) && p306 \in [1, oo) & p262 \in [1, oo) && p124 \in [1, oo)]]
normalized: ~ [E [true U ~ [[p483 \in [1, oo) && p306 \in [1, oo) & p262 \in [1, oo) && p124 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_6_fireability_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[p465 \in [1, oo) && p194 \in [1, oo) & p261 \in [1, oo)]]]
normalized: ~ [E [true U [p261 \in [1, oo) & p465 \in [1, oo) && p194 \in [1, oo)]]]

-> the formula is TRUE

FORMULA p_38_fireability_and TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[p261 \in [1, oo) | p465 \in [1, oo) && p194 \in [1, oo)]]]
normalized: ~ [E [true U [p261 \in [1, oo) | p465 \in [1, oo) && p194 \in [1, oo)]]]

-> the formula is FALSE

FORMULA p_39_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m32sec

checking: ~ [EF [[~ [p261 \in [1, oo)] & ~ [p465 \in [1, oo) && p194 \in [1, oo)]]]]
normalized: ~ [E [true U [! (p465 \in [1, oo) && p194 \in [1, oo)) & ! (p261 \in [1, oo))]]]

-> the formula is FALSE

FORMULA p_40_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 4m12sec

STOP 1371122008

--------------------
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

6462 8690 8720 10012 9450 9450 10295 10260 11778 12063 10225 10620 10336 10621 10629 10342 10941 10946 10852 11497 11562 10961 10734 10980 10988 10758 10991 10997 10890 10999 10767 11000 11008 10773 11011 11017 10905 11019 10782 11020 11028 10788 11647 11831 11207 12285 11207 12182 11346 11346 11625 11859 11849 11697 11346 11841 11346 11841 11346 11835 11571 11832 11565 11352 11352 11835 11565 11833 11559 11858 11352 11381 11605 11507 12405 12054 11972 12052 11956 11381 12044 11381 12041 11948 12039 11942 11389 11798 11392 11392 11652 11891 11392 11947 11392 11947 11392 11944 11743 11940 11731 11392 11932 11392 11398 11398 11938 11398 11935 11719 11890 11428 11767 11434 11434 11793 11454 11454 11889 11454 11888 11533 11888 11530 11454 11882 11456 11886 11458 11464 11464 11893 11530 11896 11606 11468 11468 11857 11654 11488 11488 11874 11966 11495 11918 11495 11921 11537 11922 11536 11923 11717 11497 11923 11498 11504 11504 11931 11541 11505 11727 11506 11506
iterations count:163609 (210), effective:1298 (1)
6444 8692 8722 10014 10014 9452 10293 9637 11776 12061 10223 10618 10334 10463 10626 10340 10936 10943 10724 11501 11663 10963 10860 10983 10755 10984 10992 10761 10995 11001 10767 11003 10770 11004 11011 10776 11015 11020 10782 11023 10836 10914 11207 11930 11207 12285 12098 12182 11346 11346 11625 11346 11346 11847 11346 11844 11589 11841 11583 11836 11571 11834 11677 11346 11352 11837 11565 11352 11675 11352 11352 11381 11381 11600 12405 11698 11960 11381 12050 11381 12047 11960 12042 11948 11688 11940 11381 11799 11392 11392 11652 11392 11392 11950 11755 11948 11749 11946 11811 11392 11935 11392 11935 11392 11398 11398 11938 11725 11937 11719 11398 11398 11768 11434 11434 11794 11454 11454 11889 11536 11890 11533 11454 11884 11454 11885 11456 11886 11525 11464 11464 11895 11694 11466 11891 11468 11468 11476 11855 11488 11488 11874 11495 11495 11921 11538 11922 11537 11495 11717 11495 11921 11497 11923 11535 11504 11504 11504 11927 11505 11931 11506 11970
iterations count:163910 (211), effective:1298 (1)

iterations count:776 (1), effective:0 (0)
11506
iterations count:1045 (1), effective:2 (0)

iterations count:776 (1), effective:0 (0)
6553 7237 7451 9606 10637 10631 9649 9893 9650 12006 12248 10414 10805 10812 10527 10813 10975 10881 11557 11697 10763 10989 11015 10786 11018 11024 10918 11026 10795 11027 11034 10801 11038 11044 10807 11046 10810 10939 11054 10816 11055 11238 11961 11816 12318 12129 11238 11238 11377 11657 11377 11377 11878 11626 11875 11620 11873 11614 11868 11712 11377 11860 11377 11383 11383 11863 11383 11863 11383 11383 11383 11383 11605 11383 11383 12055 11383 12052 11968 12050 11962 12045 11946 11383 12037 11383 12544 12443 11386 11392 11654 11518 11891 11948 11749 11629 11811 11392 11938 11392 11935 11725 11398 11398 11938 11725 11937 11797 11398 11398 11768 11434 11434 11795 11454 11939 11890 11536 11890 11693 11454 11884 11454 11885 11456 11886 11525 11464 11464 11464 11694 11466 11894 11468 11946 11476 11855 11488 11488 11874 11495 11495 11921 11538 11922 11537 11495 11918 11495 11921 11497 11923 11535 11504 11504 11504 11927 11505 11931 11506 11970
iterations count:161977 (208), effective:1279 (1)
11506
iterations count:1050 (1), effective:3 (0)

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