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

Execution Outputs of marcie for RwMutex/r0010w1000 (P/T)

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

execution on node 25: cluster1u27.lip6.fr (runId=136980626701424_n_25)
=====================================================================
runnning marcie on RwMutex-PT-r0010w1000 (CTLFireability)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is RwMutex-PT-r0010w1000, examination is CTLFireability
=====================================================================

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

START 1369821744

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=CTLFireability.txt

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 2030 NrTr: 2020)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m6sec

init dd package: 0m1sec


RS generation: 9m34sec


-> reachability set: #nodes 425663 (4.3e+05) #states 2,024 (3)



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

checking: AG [[p1840 \in [1, oo) & p1022 \in [1, oo) && p1023 \in [1, oo) && p1024 \in [1, oo) && p1025 \in [1, oo) && p1026 \in [1, oo) && p1027 \in [1, oo) && p1028 \in [1, oo) && p1029 \in [1, oo) && p1030 \in [1, oo) && p1031 \in [1, oo) && p289 \in [1, oo)]]
normalized: ~ [E [true U ~ [[p1840 \in [1, oo) & p289 \in [1, oo) && p1031 \in [1, oo) && p1030 \in [1, oo) && p1029 \in [1, oo) && p1028 \in [1, oo) && p1027 \in [1, oo) && p1026 \in [1, oo) && p1025 \in [1, oo) && p1024 \in [1, oo) && p1022 \in [1, oo) && p1023 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_1441_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m7sec

checking: AF [[p1840 \in [1, oo) | p1022 \in [1, oo) && p1023 \in [1, oo) && p1024 \in [1, oo) && p1025 \in [1, oo) && p1026 \in [1, oo) && p1027 \in [1, oo) && p1028 \in [1, oo) && p1029 \in [1, oo) && p1030 \in [1, oo) && p1031 \in [1, oo) && p289 \in [1, oo)]]
normalized: ~ [EG [~ [[p1840 \in [1, oo) | p289 \in [1, oo) && p1031 \in [1, oo) && p1030 \in [1, oo) && p1029 \in [1, oo) && p1028 \in [1, oo) && p1027 \in [1, oo) && p1026 \in [1, oo) && p1025 \in [1, oo) && p1024 \in [1, oo) && p1022 \in [1, oo) && p1023 \in [1, oo)]]]]

..
EG iterations: 2
-> the formula is TRUE

FORMULA p_1442_fireability_or TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m7sec

checking: AG [[p1840 \in [1, oo) & p1022 \in [1, oo) && p1023 \in [1, oo) && p1024 \in [1, oo) && p1025 \in [1, oo) && p1026 \in [1, oo) && p1027 \in [1, oo) && p1028 \in [1, oo) && p1029 \in [1, oo) && p1030 \in [1, oo) && p1031 \in [1, oo) && p289 \in [1, oo)]]
normalized: ~ [E [true U ~ [[p1840 \in [1, oo) & p289 \in [1, oo) && p1031 \in [1, oo) && p1030 \in [1, oo) && p1029 \in [1, oo) && p1028 \in [1, oo) && p1027 \in [1, oo) && p1026 \in [1, oo) && p1025 \in [1, oo) && p1024 \in [1, oo) && p1022 \in [1, oo) && p1023 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_1443_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[p1840 \in [1, oo) | p1022 \in [1, oo) && p1023 \in [1, oo) && p1024 \in [1, oo) && p1025 \in [1, oo) && p1026 \in [1, oo) && p1027 \in [1, oo) && p1028 \in [1, oo) && p1029 \in [1, oo) && p1030 \in [1, oo) && p1031 \in [1, oo) && p289 \in [1, oo)]]
normalized: ~ [EG [~ [[p1840 \in [1, oo) | p289 \in [1, oo) && p1031 \in [1, oo) && p1030 \in [1, oo) && p1029 \in [1, oo) && p1028 \in [1, oo) && p1027 \in [1, oo) && p1026 \in [1, oo) && p1025 \in [1, oo) && p1024 \in [1, oo) && p1022 \in [1, oo) && p1023 \in [1, oo)]]]]

..
EG iterations: 2
-> the formula is TRUE

FORMULA p_1444_fireability_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[~ [p1840 \in [1, oo)] & p1022 \in [1, oo) && p1023 \in [1, oo) && p1024 \in [1, oo) && p1025 \in [1, oo) && p1026 \in [1, oo) && p1027 \in [1, oo) && p1028 \in [1, oo) && p1029 \in [1, oo) && p1030 \in [1, oo) && p1031 \in [1, oo) && p289 \in [1, oo)]]
normalized: E [true U [! (p1840 \in [1, oo)) & p289 \in [1, oo) && p1031 \in [1, oo) && p1030 \in [1, oo) && p1029 \in [1, oo) && p1028 \in [1, oo) && p1027 \in [1, oo) && p1026 \in [1, oo) && p1025 \in [1, oo) && p1024 \in [1, oo) && p1022 \in [1, oo) && p1023 \in [1, oo)]]

-> the formula is TRUE

FORMULA p_1445_fireability_x TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 9m12sec

checking: EF [[p1249 \in [1, oo) & p1980 \in [1, oo)]]
normalized: E [true U [p1249 \in [1, oo) & p1980 \in [1, oo)]]

-> the formula is FALSE

FORMULA p_1476_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [[p1249 \in [1, oo) | p1980 \in [1, oo)]]
normalized: EG [[p1249 \in [1, oo) | p1980 \in [1, oo)]]

..
EG iterations: 2
-> the formula is FALSE

FORMULA p_1477_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m2sec

checking: AG [[p1249 \in [1, oo) & p1980 \in [1, oo)]]
normalized: ~ [E [true U ~ [[p1249 \in [1, oo) & p1980 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_1478_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 20m21sec

STOP 1369822966

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

423043 423056 423066 423074 423081 423088 423094 423100 423105 423110 423115 423120 423124 423129 423133 423137 423141 423145 423148 423152 423155 423159 423162 423165 423168 423172 423175 423178 423181 423184 423186 423189 423192 423195 423197 423200 423203 423206 423209 423215 423221 423224 423232 423238 423241 423247 423253 423256 423261 423269 423272 423278 423284 423287 423293 423294 423302 423308 423311 423317 423320 423326 423335 423338 423344 423347 423353 423356 423362 423368 423371 423377 423380 423386 423389 423395 423396 423405 423408 423414 423420 423423 423429 423430 423438 423441 423447 423450 423456 423459 423463 423469 423475 423478 423481 423487 423490 423496 423497 423505 423508 423514 423517 423523 423526 423529 423535 423539 423545 423548 423554 423557 423560 423564 423569 423575 423578 423584 423587 423590 423596 423597 423602 423609 423612 423618 423621 423624 423630 423631 423639 423642 423645 423651 423654 423657 423663 423664 423665 423675 423679 423682 423688 423691 423694 423700 423701 423706 423712 423715 423718 423724 423727 423730 423734 423739 423742 423749 423752 423755 423758 423764 423767 423768 423776 423779 423782 423788 423791 423794 423797 423801 423806 423809 423812 423816 423817 423821 423827 423830 423833 423836 423839 423845 423848 423851 423854 423860 423863 423866 423869 423872 423878 423881 423884 423887 423890 423896 423899 423902 423905 423908 423914 423917 423920 423923 423926 423929 423935 423938 423941 423944 423947 423950 423953 423959 423962 423965 423968 423971 423974 423977 423980 423983 423989 423992 423995 423998 424001 424004 424007 424010 424013 424016 424019 424025 424028 424031 424034 424037 424040 424043 424046 424049 424052 424055 424058 424061 424064 424067 424070 424073 424079 424082 424085 424088 424091 424094 424097 424100 424103 424106 424109 424112 424115 424118 424121 424124 424127 424130 424133 424136 424139 424142 424145 424148 424151 424154 424157 424160 424163 424166 424169 424172 424175 424178 424181 424184 424184 424187 424190 424193 424196 424199 424202 424205 424208 424211 424214 424217 424220 424223 424226 424229 424232 424235 424238 424238 424241 424244 424247 424250 424253 424256 424259 424262 424265 424268 424271 424274 424274 424277 424280 424283 424286 424289 424292 424295 424298 424301 424304 424304 424307 424310 424313 424316 424319 424322 424325 424328 424328 424331 424334 424337 424340 424343 424346 424349 424349 424352 424355 424358 424361 424364 424367 424367 424370 424373 424376 424379 424382 424385 424385 424388 424391 424394 424397 424400 424403 424403 424406 424409 424412 424415 424418 424418 424421 424424 424427 424430 424433 424436 424436 424439 424442 424445 424448 424448 424451 424454 424457 424460 424463 424463 424466 424469 424472 424475 424475 424478 424481 424484 424487 424490 424490 424493 424496 424499 424502 424502 424505 424508 424511 424514 424514 424517 424520 424523 424526 424526 424529 424532 424535 424535 424538 424541 424544 424547 424547 424550 424553 424556 424559 424559 424562 424565 424568 424568 424571 424574 424577 424577 424580 424583 424586 424589 424589 424592 424595 424598 424598 424601 424604 424607 424607 424610 424613 424616 424616 424619 424622 424625 424625 424628 424631 424634 424634 424637 424640 424643 424643 424646 424649 424652 424652 424655 424658 424661 424661 424664 424667 424670 424670 424673 424676 424679 424679 424682 424685 424685 424688 424691 424694 424694 424697 424700 424703 424703 424706 424709 424709 424712 424715 424718 424718 424721 424724 424724 424727 424730 424733 424733 424736 424739 424739 424742 424745 424748 424748 424751 424754 424754 424757 424760 424760 424763 424766 424769 424769 424772 424775 424775 424778 424781 424784 424784 424787 424790 424790 424793 424796 424796 424799 424802 424802 424805 424808 424811 424811 424814 424817 424817 424820 424823 424823 424826 424829 424829 424832 424835 424835 424838 424841 424841 424844 424847 424847 424850 424853 424853 424856 424859 424862 424862 424865 424868 424868 424871 424874 424874 424877 424880 424880 424883 424886 424886 424889 424892 424892 424895 424898 424898 424901 424904 424904 424907 424907 424910 424913 424913 424916 424919 424919 424922 424925 424925 424928 424931 424931 424934 424937 424937 424940 424943 424943 424946 424949 424949 424952 424952 424955 424958 424958 424961 424964 424964 424967 424970 424970 424973 424976 424976 424979 424979 424982 424985 424985 424988 424991 424991 424994 424997 424997 425000 425000 425003 425006 425006 425009 425012 425012 425015 425015 425018 425021 425021 425024 425027 425027 425030 425033 425033 425036 425036 425039 425042 425042 425045 425045 425048 425051 425051 425054 425057 425057 425060 425060 425063 425066 425066 425069 425072 425072 425075 425075 425078 425081 425081 425084 425084 425087 425090 425090 425093 425093 425096 425099 425099 425102 425105 425105 425108 425108 425111 425114 425114 425117 425117 425120 425123 425123 425126 425126 425129 425132 425132 425135 425135 425138 425141 425141 425144 425144 425147 425150 425150 425153 425153 425156 425159 425159 425162 425162 425165 425165 425168 425171 425171 425174 425174 425177 425180 425180 425183 425183 425186 425189 425189 425192 425192 425195 425195 425198 425201 425201 425204 425204 425207 425210 425210 425213 425213 425216 425216 425219 425222 425222 425225 425225 425228 425228 425231 425234 425234 425237 425237 425240 425243 425243 425246 425246 425249 425249 425252 425255 425255 425258 425258 425261 425261 425264 425267 425267 425270 425270 425273 425273 425276 425279 425279 425282 425282 425285 425285 425288 425288 425291 425294 425294 425297 425297 425300 425300 425303 425306 425306 425309 425309 425312 425312 425315 425315 425318 425321 425321 425324 425324 425327 425327 425330 425330 425333 425336 425336 425339 425339 425342 425342 425345 425345 425348 425351 425351 425354 425354 425357 425357 425360 425360 425363 425363 425366 425369 425369 425372 425372 425375 425375 425378 425378 425381 425384 425384 425387 425387 425390 425390 425393 425393 425396 425396 425399 425399 425402 425405 425405 425408 425408 425411 425411 425414 425414 425417 425417 425420 425420 425423 425426 425426 425429 425429 425432 425432 425435 425435 425438 425438 425441 425441 425444 425447 425447 425450 425450 425453 425453 425456 425456 425459 425459 425462 425462 425465 425465 425468 425468 425471 425474 425474 425477 425477 425480 425480 425483 425483 425486 425486 425489 425489 425492 425492 425495 425495 425498 425498 425501 425504 425504 425507 425507 425510 425510 425513 425513 425516 425516 425519 425519 425522 425522 425525 425525 425528 425528 425531 425531 425534 425534 425537 425537 425540 425540 425543 425543 425546 425549 425549 425552 425552 425555 425555 425558 425558 425561 425561 425564 425564 425567 425567 425570 425570 425573 425573 425576 425576 425579 425579 425582 425582 425585 425585 425588 425588 425591 425591 425594 425594 425597 425597 425600 425600 425603 425603 425606 425606 425609 425609 425612 425612 425615 425615 425618 425618 425621 425621 425624 425624 425627 425627 425630 425630 425633 425633 425636 425636 425639 425639 425642 425642 425645 425645 425648 425648 425651 425651 425654 425654 425657 425657 425660 425660 425663 425663
iterations count:1043313 (516), effective:1010 (0)

initing FirstDep: 0m0sec

425663 425663
iterations count:2020 (1), effective:0 (0)
425663 425663
iterations count:2020 (1), effective:0 (0)
423044 423056 423066 423074 423082 423089 423095 423100 423106 423111 423116 423120 423125 423129 423133 423137 423141 423145 423149 423152 423156 423159 423162 423166 423169 423172 423175 423178 423181 423184 423187 423190 423192 423195 423198 423200 423203 423209 423215 423224 423232 423241 423247 423256 423261 423272 423278 423287 423293 423299 423308 423314 423320 423327 423338 423344 423353 423359 423363 423374 423380 423386 423392 423402 423408 423414 423420 423426 423435 423441 423447 423453 423459 423463 423472 423478 423487 423493 423497 423505 423511 423517 423523 423529 423535 423542 423548 423554 423560 423564 423572 423578 423584 423590 423596 423602 423609 423615 423621 423624 423630 423636 423642 423648 423654 423660 423664 423665 423675 423682 423688 423694 423700 423701 423709 423715 423721 423727 423733 423734 423742 423749 423755 423758 423764 423768 423776 423779 423785 423791 423797 423800 423806 423812 423815 423817 423821 423824 423830 423833 423836 423839 423845 423848 423851 423854 423860 423863 423866 423869 423872 423878 423881 423884 423887 423890 423896 423899 423902 423905 423908 423914 423917 423920 423923 423926 423929 423935 423938 423941 423944 423947 423950 423953 423959 423962 423965 423968 423971 423974 423977 423980 423983 423989 423992 423995 423998 424001 424004 424007 424010 424013 424016 424022 424025 424028 424031 424034 424037 424040 424043 424046 424049 424052 424055 424058 424061 424064 424067 424070 424076 424079 424082 424085 424088 424091 424094 424097 424100 424103 424106 424109 424112 424115 424118 424121 424124 424127 424130 424133 424136 424139 424142 424145 424148 424151 424154 424157 424160 424163 424166 424169 424172 424175 424178 424181 424184 424187 424190 424190 424193 424196 424199 424202 424205 424208 424211 424214 424217 424220 424223 424226 424229 424232 424235 424238 424241 424244 424244 424247 424250 424253 424256 424259 424262 424265 424268 424271 424274 424277 424277 424280 424283 424286 424289 424292 424295 424298 424301 424304 424307 424307 424310 424313 424316 424319 424322 424325 424328 424331 424331 424334 424337 424340 424343 424346 424349 424352 424352 424355 424358 424361 424364 424367 424370 424370 424373 424376 424379 424382 424385 424388 424388 424391 424394 424397 424400 424403 424406 424406 424409 424412 424415 424418 424421 424421 424424 424427 424430 424433 424436 424436 424439 424442 424445 424448 424451 424451 424454 424457 424460 424463 424466 424466 424469 424472 424475 424478 424478 424481 424484 424487 424490 424490 424493 424496 424499 424502 424505 424505 424508 424511 424514 424514 424517 424520 424523 424526 424526 424529 424532 424535 424538 424538 424541 424544 424547 424550 424550 424553 424556 424559 424559 424562 424565 424568 424571 424571 424574 424577 424580 424580 424583 424586 424589 424589 424592 424595 424598 424601 424601 424604 424607 424610 424610 424613 424616 424619 424619 424622 424625 424628 424628 424631 424634 424637 424637 424640 424643 424646 424646 424649 424652 424655 424655 424658 424661 424664 424664 424667 424670 424670 424673 424676 424679 424679 424682 424685 424688 424688 424691 424694 424697 424697 424700 424703 424703 424706 424709 424712 424712 424715 424718 424718 424721 424724 424727 424727 424730 424733 424733 424736 424739 424742 424742 424745 424748 424748 424751 424754 424757 424757 424760 424763 424763 424766 424769 424772 424772 424775 424778 424778 424781 424784 424784 424787 424790 424790 424793 424796 424799 424799 424802 424805 424805 424808 424811 424811 424814 424817 424817 424820 424823 424826 424826 424829 424832 424832 424835 424838 424838 424841 424844 424844 424847 424850 424850 424853 424856 424856 424859 424862 424862 424865 424868 424868 424871 424874 424874 424877 424880 424880 424883 424886 424886 424889 424892 424892 424895 424898 424898 424901 424904 424904 424907 424910 424910 424913 424916 424916 424919 424922 424922 424925 424928 424928 424931 424934 424934 424937 424940 424940 424943 424943 424946 424949 424949 424952 424955 424955 424958 424961 424961 424964 424967 424967 424970 424970 424973 424976 424976 424979 424982 424982 424985 424988 424988 424991 424994 424994 424997 424997 425000 425003 425003 425006 425009 425009 425012 425012 425015 425018 425018 425021 425024 425024 425027 425027 425030 425033 425033 425036 425039 425039 425042 425042 425045 425048 425048 425051 425054 425054 425057 425057 425060 425063 425063 425066 425069 425069 425072 425072 425075 425078 425078 425081 425081 425084 425087 425087 425090 425090 425093 425096 425096 425099 425102 425102 425105 425105 425108 425111 425111 425114 425114 425117 425120 425120 425123 425123 425126 425129 425129 425132 425132 425135 425138 425138 425141 425141 425144 425147 425147 425150 425150 425153 425156 425156 425159 425159 425162 425165 425165 425168 425168 425171 425171 425174 425177 425177 425180 425180 425183 425186 425186 425189 425189 425192 425195 425195 425198 425198 425201 425201 425204 425207 425207 425210 425210 425213 425216 425216 425219 425219 425222 425222 425225 425228 425228 425231 425231 425234 425234 425237 425240 425240 425243 425243 425246 425246 425249 425252 425252 425255 425255 425258 425261 425261 425264 425264 425267 425267 425270 425270 425273 425276 425276 425279 425279 425282 425282 425285 425288 425288 425291 425291 425294 425294 425297 425300 425300 425303 425303 425306 425306 425309 425309 425312 425315 425315 425318 425318 425321 425321 425324 425324 425327 425330 425330 425333 425333 425336 425336 425339 425339 425342 425345 425345 425348 425348 425351 425351 425354 425354 425357 425360 425360 425363 425363 425366 425366 425369 425369 425372 425372 425375 425378 425378 425381 425381 425384 425384 425387 425387 425390 425390 425393 425396 425396 425399 425399 425402 425402 425405 425405 425408 425408 425411 425414 425414 425417 425417 425420 425420 425423 425423 425426 425426 425429 425429 425432 425435 425435 425438 425438 425441 425441 425444 425444 425447 425447 425450 425450 425453 425453 425456 425459 425459 425462 425462 425465 425465 425468 425468 425471 425471 425474 425474 425477 425477 425480 425480 425483 425483 425486 425489 425489 425492 425492 425495 425495 425498 425498 425501 425501 425504 425504 425507 425507 425510 425510 425513 425513 425516 425516 425519 425522 425522 425525 425525 425528 425528 425531 425531 425534 425534 425537 425537 425540 425540 425543 425543 425546 425546 425549 425549 425552 425552 425555 425555 425558 425558 425561 425561 425564 425564 425567 425567 425570 425570 425573 425576 425576 425579 425579 425582 425582 425585 425585 425588 425588 425591 425591 425594 425594 425597 425597 425600 425600 425603 425603 425606 425606 425609 425609 425612 425612 425615 425615 425618 425618 425621 425621 425624 425624 425627 425627 425630 425630 425633 425633 425636 425636 425639 425639 425642 425642 425645 425645 425648 425648 425651 425651 425654 425654 425657 425657 425660 425660 425663 425663
iterations count:1001747 (495), effective:1010 (0)
425663 425663
iterations count:2020 (1), effective:0 (0)

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