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

Execution Outputs of marcie for PermAdmissibility/01 (P/T)

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

execution on node 3: quadhexa-2.u-paris10.fr (runId=136959888100067_n_3)
=====================================================================
runnning marcie on PermAdmissibility-PT-01 (ReachabilityMarkingComparison)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is PermAdmissibility-PT-01, examination is ReachabilityMarkingComparison
=====================================================================

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

START 1369618380

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 168 NrTr: 592)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m53sec


-> reachability set: #nodes 66994 (6.7e+04) #states 52,537 (4)



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

checking: AG [[[aux8_7=0.000000000000000 & [aux8_2=0.000000000000000 & [aux8_3=0.000000000000000 & [1.000000000000000=aux8_6 & true]]]] & [out8_3=0.000000000000000 & [out8_2=0.000000000000000 & [out8_4=0.000000000000000 & [out8_5=0.000000000000000 & [out8_0=0.000000000000000 & [out8_1=0.000000000000000 & [out8_7=0.000000000000000 & [1.000000000000000=out8_6 & true]]]]]]]]]]
normalized: ~ [E [true U ~ [[[[[out8_4=0.000000000000000 & [out8_5=0.000000000000000 & [out8_0=0.000000000000000 & [out8_1=0.000000000000000 & [out8_7=0.000000000000000 & [1.000000000000000=out8_6 & true]]]]]] & out8_2=0.000000000000000] & out8_3=0.000000000000000] & [[[[true & 1.000000000000000=aux8_6] & aux8_3=0.000000000000000] & aux8_2=0.000000000000000] & aux8_7=0.000000000000000]]]]]

-> the formula is FALSE

FORMULA p_27_markingcomparison_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m22sec

checking: AG [[[aux8_7=0.000000000000000 & [aux8_2=0.000000000000000 & [aux8_3=0.000000000000000 & [1.000000000000000=aux8_6 & true]]]] | [out8_3=0.000000000000000 & [out8_2=0.000000000000000 & [out8_4=0.000000000000000 & [out8_5=0.000000000000000 & [out8_0=0.000000000000000 & [out8_1=0.000000000000000 & [out8_7=0.000000000000000 & [1.000000000000000=out8_6 & true]]]]]]]]]]
normalized: ~ [E [true U ~ [[[[[[[[[[true & 1.000000000000000=out8_6] & out8_7=0.000000000000000] & out8_1=0.000000000000000] & out8_0=0.000000000000000] & out8_5=0.000000000000000] & out8_4=0.000000000000000] & out8_2=0.000000000000000] & out8_3=0.000000000000000] | [[[[true & 1.000000000000000=aux8_6] & aux8_3=0.000000000000000] & aux8_2=0.000000000000000] & aux8_7=0.000000000000000]]]]]

-> the formula is FALSE

FORMULA p_28_markingcomparison_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[aux8_7=0.000000000000000 & [aux8_2=0.000000000000000 & [aux8_3=0.000000000000000 & [1.000000000000000=aux8_6 & true]]]] & [out8_3=0.000000000000000 & [out8_2=0.000000000000000 & [out8_4=0.000000000000000 & [out8_5=0.000000000000000 & [out8_0=0.000000000000000 & [out8_1=0.000000000000000 & [out8_7=0.000000000000000 & [1.000000000000000=out8_6 & true]]]]]]]]]]
normalized: ~ [E [true U ~ [[[[[[true & 1.000000000000000=aux8_6] & aux8_3=0.000000000000000] & aux8_2=0.000000000000000] & aux8_7=0.000000000000000] & [[[[[[out8_1=0.000000000000000 & [out8_7=0.000000000000000 & [true & 1.000000000000000=out8_6]]] & out8_0=0.000000000000000] & out8_5=0.000000000000000] & out8_4=0.000000000000000] & out8_2=0.000000000000000] & out8_3=0.000000000000000]]]]]

-> the formula is FALSE

FORMULA p_29_markingcomparison_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[aux8_7=0.000000000000000 & [aux8_2=0.000000000000000 & [aux8_3=0.000000000000000 & [1.000000000000000=aux8_6 & true]]]] | [out8_3=0.000000000000000 & [out8_2=0.000000000000000 & [out8_4=0.000000000000000 & [out8_5=0.000000000000000 & [out8_0=0.000000000000000 & [out8_1=0.000000000000000 & [out8_7=0.000000000000000 & [1.000000000000000=out8_6 & true]]]]]]]]]]
normalized: ~ [E [true U ~ [[[aux8_7=0.000000000000000 & [aux8_2=0.000000000000000 & [aux8_3=0.000000000000000 & [1.000000000000000=aux8_6 & true]]]] | [out8_3=0.000000000000000 & [out8_2=0.000000000000000 & [out8_4=0.000000000000000 & [out8_5=0.000000000000000 & [out8_0=0.000000000000000 & [out8_1=0.000000000000000 & [out8_7=0.000000000000000 & [1.000000000000000=out8_6 & true]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_30_markingcomparison_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[aux8_7=0.000000000000000 & [aux8_2=0.000000000000000 & [aux8_3=0.000000000000000 & [1.000000000000000=aux8_6 & true]]]] & [out8_3=0.000000000000000 & [out8_2=0.000000000000000 & [out8_4=0.000000000000000 & [out8_5=0.000000000000000 & [out8_0=0.000000000000000 & [out8_1=0.000000000000000 & [out8_7=0.000000000000000 & [1.000000000000000=out8_6 & true]]]]]]]]]]
normalized: ~ [E [true U ~ [[[aux8_7=0.000000000000000 & [aux8_2=0.000000000000000 & [aux8_3=0.000000000000000 & [1.000000000000000=aux8_6 & true]]]] & [out8_3=0.000000000000000 & [out8_2=0.000000000000000 & [out8_4=0.000000000000000 & [out8_5=0.000000000000000 & [out8_0=0.000000000000000 & [out8_1=0.000000000000000 & [out8_7=0.000000000000000 & [1.000000000000000=out8_6 & true]]]]]]]]]]]]

-> the formula is FALSE

FORMULA p_31_markingcomparison_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[1.000000000000000<=in4_6 & true] & true] & [[1.000000000000000>c8 & true] & true]]]
normalized: ~ [E [true U ~ [[[[1.000000000000000<=in4_6 & true] & true] & [[1.000000000000000>c8 & true] & true]]]]]

-> the formula is FALSE

FORMULA p_32_markingcomparison_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[[[1.000000000000000<=in4_6 & true] & true] | [[1.000000000000000>c8 & true] & true]]]
normalized: ~ [E [true U ~ [[[[true & 1.000000000000000<=in4_6] & true] | [[1.000000000000000>c8 & true] & true]]]]]

-> the formula is FALSE

FORMULA p_33_markingcomparison_full_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[~ [[[1.000000000000000<=in4_6 & true] & true]] & [[1.000000000000000>c8 & true] & true]]]
normalized: ~ [E [true U ~ [[~ [[[true & 1.000000000000000<=in4_6] & true]] & [[true & 1.000000000000000>c8] & true]]]]]

-> the formula is FALSE

FORMULA p_34_markingcomparison_full_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 1m57sec

STOP 1369618499

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

1291 1594 1676 1980 2045 2212 2283 2396 2427 2752 2823 3015 3075 3237 3308 3443 3451 3648 3719 3848 3938 4042 4090 4097 4378 4404 4563 4626 4644 4839 4860 5015 5070 5150 5215 5220 5370 5449 5505 5544 5592 5715 5761 5818 5863 5929 5970 6032 6157 6170 6179 6320 6320 6315 6482 6467 6471 6659 6658 6655 6775 6771 6764 6867 6858 6848 6964 6945 6929 7004 7015 7063 7106 7134 7129 7171 7223 7262 7311 7370 7383 7392 7441 7479 7505 7492 7536 7586 7623 7662 7730 7744 7737 7741 7771 7781 7808 7840 7864 7846 7955 8001 8033 8075 8098 8131 8152 8199 8239 8250 8294 8407 8411 8399 8461 8506 8549 8590 8596 8607 8653 8660 8767 8772 8755 8793 8804 8845 8855 8887 8898 8933 9005 9011 9014 9042 9069 9083 9093 9088 9115 9128 9157 9907 10817 11422 11914 12251 12538 12794 13196 13421 13610 13742 13965 14151 14317 14609 14958 15323 15621 15817 15870 15980 16095 16147 16232 16385 16421 16475 16636 16782 16938 17027 17072 17285 17476 17561 17836 17956 18159 18202 18214 18351 18398 18709 18842 18990 19067 19182 19196 19237 19326 19365 19624 19632 19844 19991 20062 20206 20296 20345 20359 20491 20590 20744 20837 20896 21002 21067 21160 21306 21492 21542 21569 21572 21702 21848 21910 21963 22005 22013 22136 22195 22257 22292 22302 22414 22439 22444 22443 22525 22634 22665 22679 22721 22796 22808 23006 23109 23157 23214 23323 23486 23607 23716 23766 23798 23877 24013 24107 24161 24209 24362 24524 24556 24641 24703 24769 24834 24909 25247 25388 25537 25570 25620 25657 25800 25877 25927 25969 26014 26084 26124 26145 26173 26220 26351 26481 26626 26694 26694 26718 26851 26910 26932 27077 27147 27241 27248 27241 27274 27332 27383 27521 27550 27588 27611 27614 27657 27676 27740 27770 27785 27784 27958 28006 28047 28114 28116 28166 28195 28252 28281 28334 28334 28514 28588 28655 28688 28831 28870 28875 28895 28943 28995 29037 29071 29127 29162 29169 29174 29263 29386 29433 29490 29500 29528 29602 29675 29724 29756 29767 29764 29901 29983 30091 30118 30148 30159 30159 30164 30177 30218 30246 30291 30301 30312 30310 30313 30454 30552 30646 30733 30771 30813 30860 30969 31014 31059 31115 31195 31229 31291 31331 31370 31494 31611 31715 31818 31886 31946 32002 32022 32075 32145 32245 32320 32349 32384 32465 32485 32517 32620 32668 32689 32732 32742 32799 32840 32851 32861 32892 32912 33095 33136 33200 33314 33351 33376 33400 33424 33463 33523 33595 33632 33670 33704 33707 33732 33725 33872 33973 34042 34082 34127 34168 34181 34247 34300 34374 34435 34476 34493 34533 34569 34609 34730 34771 34809 34854 34864 34872 34908 34927 34935 34968 34988 35133 35217 35283 35319 35348 35373 35415 35516 35537 35585 35622 35624 35639 35666 35714 35744 35795 35991 36061 36079 36096 36133 36142 36152 36194 36248 36296 36304 36320 36355 36350 36391 36391 36465 36489 36500 36517 36530 36536 36552 36574 36565 36564 36577 36688 36767 36788 36814 36865 36948 36985 37008 37073 37119 37127 37168 37211 37273 37334 37357 37402 37544 37609 37635 37661 37704 37778 37801 37836 37866 37908 37913 37912 37945 37996 38029 38064 38180 38209 38260 38284 38307 38316 38350 38377 38376 38418 38433 38509 38551 38570 38578 38603 38632 38665 38667 38664 38679 38714 38723 42336 43193 44896 45444 45487 47666 48286 48752 49470 49760 50514 51161 51476 51691 51971 52951 53416 53493 54161 54324 55953 58654 60302 61778 62412 62719 63594 63955 64113 64597 64846 65188 65491 65733 65903 66033 66176 66251 66400 66496 66561 66679 66817 66938
iterations count:592874 (1001), effective:3245 (5)

initing FirstDep: 0m0sec


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

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

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

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

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

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

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

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

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