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-r0010w0500
export BK_EXAMINATION=ReachabilityFireability
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-r0010w0500
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool marcie:'
echo ' Test is RwMutex-PT-r0010w0500, examination is ReachabilityFireability'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

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

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

execution on node 31: cluster1u33.lip6.fr (runId=136980626601358_n_31)
=====================================================================
runnning marcie on RwMutex-PT-r0010w0500 (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 RwMutex-PT-r0010w0500, examination is ReachabilityFireability
=====================================================================

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

START 1369821011

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: 1030 NrTr: 1020)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m1sec

init dd package: 0m1sec


RS generation: 0m49sec


-> reachability set: #nodes 214541 (2.1e+05) #states 1,524 (3)



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

checking: AG [[p989 \in [1, oo) & p522 \in [1, oo) && p275 \in [1, oo) && p523 \in [1, oo) && p524 \in [1, oo) && p525 \in [1, oo) && p526 \in [1, oo) && p527 \in [1, oo) && p528 \in [1, oo) && p529 \in [1, oo) && p530 \in [1, oo) && p531 \in [1, oo)]]
normalized: ~ [E [true U ~ [[p989 \in [1, oo) & p531 \in [1, oo) && p530 \in [1, oo) && p529 \in [1, oo) && p528 \in [1, oo) && p527 \in [1, oo) && p526 \in [1, oo) && p525 \in [1, oo) && p524 \in [1, oo) && p523 \in [1, oo) && p522 \in [1, oo) && p275 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_2_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[p989 \in [1, oo) | p275 \in [1, oo) && p522 \in [1, oo) && p523 \in [1, oo) && p524 \in [1, oo) && p525 \in [1, oo) && p526 \in [1, oo) && p527 \in [1, oo) && p528 \in [1, oo) && p529 \in [1, oo) && p530 \in [1, oo) && p531 \in [1, oo)]]
normalized: ~ [E [true U ~ [[p989 \in [1, oo) | p531 \in [1, oo) && p530 \in [1, oo) && p529 \in [1, oo) && p528 \in [1, oo) && p527 \in [1, oo) && p526 \in [1, oo) && p525 \in [1, oo) && p524 \in [1, oo) && p523 \in [1, oo) && p275 \in [1, oo) && p522 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_3_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[p989 \in [1, oo) & p530 \in [1, oo) && p523 \in [1, oo) && p275 \in [1, oo) && p522 \in [1, oo) && p524 \in [1, oo) && p525 \in [1, oo) && p526 \in [1, oo) && p527 \in [1, oo) && p528 \in [1, oo) && p529 \in [1, oo) && p531 \in [1, oo)]]
normalized: ~ [E [true U ~ [[p989 \in [1, oo) & p531 \in [1, oo) && p530 \in [1, oo) && p529 \in [1, oo) && p528 \in [1, oo) && p527 \in [1, oo) && p526 \in [1, oo) && p525 \in [1, oo) && p524 \in [1, oo) && p523 \in [1, oo) && p275 \in [1, oo) && p522 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_4_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[p989 \in [1, oo) | p530 \in [1, oo) && p524 \in [1, oo) && p522 \in [1, oo) && p275 \in [1, oo) && p523 \in [1, oo) && p525 \in [1, oo) && p526 \in [1, oo) && p527 \in [1, oo) && p528 \in [1, oo) && p529 \in [1, oo) && p531 \in [1, oo)]]
normalized: ~ [E [true U ~ [[p989 \in [1, oo) | p531 \in [1, oo) && p530 \in [1, oo) && p529 \in [1, oo) && p528 \in [1, oo) && p527 \in [1, oo) && p526 \in [1, oo) && p525 \in [1, oo) && p524 \in [1, oo) && p523 \in [1, oo) && p522 \in [1, oo) && p275 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_5_fireability_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AG [[p531 \in [1, oo) && p530 \in [1, oo) && p529 \in [1, oo) && p528 \in [1, oo) && p527 \in [1, oo) && p524 \in [1, oo) && p522 \in [1, oo) && p275 \in [1, oo) && p523 \in [1, oo) && p525 \in [1, oo) && p526 \in [1, oo) -> p989 \in [1, oo)]]
normalized: ~ [E [true U ~ [[! (p531 \in [1, oo) && p530 \in [1, oo) && p529 \in [1, oo) && p528 \in [1, oo) && p527 \in [1, oo) && p526 \in [1, oo) && p525 \in [1, oo) && p524 \in [1, oo) && p523 \in [1, oo) && p522 \in [1, oo) && p275 \in [1, oo)) | p989 \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_6_fireability_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m47sec

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

-> the formula is TRUE

FORMULA p_38_fireability_and TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: ~ [EF [[p688 \in [1, oo) | p738 \in [1, oo)]]]
normalized: ~ [E [true U [p688 \in [1, oo) | p738 \in [1, oo)]]]

-> the formula is FALSE

FORMULA p_39_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m56sec

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

-> the formula is TRUE

FORMULA p_40_fireability_and_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec


total processing time: 2m54sec

STOP 1369821186

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

213237 213250 213260 213268 213276 213282 213289 213294 213300 213305 213384 213396 213412 213427 213441 213457 213469 213482 213494 213504 213519 213531 213543 213556 213568 213580 213585 213588 213590 213593 213596 213598 213601 213603 213606 213608 213611 213613 213616 213623 213632 213638 213647 213653 213659 213668 213674 213680 213686 213695 213701 213707 213713 213719 213725 213731 213737 213743 213749 213755 213761 213767 213773 213779 213785 213791 213797 213803 213809 213815 213821 213827 213830 213836 213842 213848 213854 213857 213863 213869 213875 213878 213884 213890 213893 213899 213905 213908 213914 213920 213923 213929 213935 213938 213944 213950 213953 213959 213962 213968 213971 213977 213983 213986 213992 213995 214001 214004 214010 214013 214019 214022 214028 214031 214037 214040 214043 214049 214052 214058 214061 214067 214070 214073 214079 214082 214088 214091 214094 214100 214103 214109 214112 214115 214121 214124 214127 214133 214136 214139 214145 214148 214151 214157 214160 214163 214166 214172 214175 214178 214184 214187 214190 214193 214199 214202 214205 214208 214214 214217 214220 214223 214229 214232 214235 214238 214244 214247 214250 214253 214256 214262 214265 214268 214271 214274 214280 214283 214286 214289 214292 214295 214301 214304 214307 214310 214313 214316 214322 214325 214328 214331 214334 214337 214340 214343 214349 214352 214355 214358 214361 214364 214367 214370 214373 214379 214382 214385 214388 214391 214394 214397 214400 214403 214406 214409 214412 214418 214421 214424 214427 214430 214433 214436 214439 214442 214445 214448 214451 214454 214457 214460 214463 214466 214469 214472 214475 214478 214481 214484 214487 214490 214493 214496 214499 214502 214505 214508 214511 214514 214517 214520 214523 214526 214529 214532 214535 214538 214541
iterations count:259134 (254), effective:510 (0)

initing FirstDep: 0m0sec

214541
iterations count:1020 (1), effective:0 (0)
214540 214541
iterations count:2022 (1), effective:2 (0)
214541
iterations count:1020 (1), effective:0 (0)
214540 214541
iterations count:2022 (1), effective:2 (0)
213237 213250 213260 213268 213276 213282 213288 213294 213300 213305 213314 213323 213338 213347 213359 213368 213381 213390 213397 213409 213421 213430 213439 213449 213458 213465 213482 213491 213500 213509 213516 213525 213534 213543 213553 213562 213569 213577 213587 213596 213603 213611 213616 213623 213632 213638 213647 213653 213659 213668 213674 213680 213686 213692 213701 213707 213713 213719 213725 213731 213737 213743 213749 213755 213761 213767 213773 213779 213785 213791 213797 213803 213809 213815 213821 213824 213830 213836 213842 213848 213851 213857 213863 213869 213872 213878 213884 213890 213893 213899 213905 213908 213914 213920 213923 213929 213935 213938 213944 213947 213953 213959 213962 213968 213971 213977 213980 213986 213989 213995 213998 214004 214007 214013 214016 214022 214025 214031 214034 214040 214043 214049 214052 214058 214061 214064 214070 214073 214079 214082 214085 214091 214094 214100 214103 214106 214112 214115 214118 214124 214127 214130 214136 214139 214142 214148 214151 214154 214160 214163 214166 214172 214175 214178 214181 214187 214190 214193 214196 214202 214205 214208 214214 214217 214220 214223 214226 214232 214235 214238 214241 214247 214250 214253 214256 214259 214265 214268 214271 214274 214277 214283 214286 214289 214292 214295 214298 214304 214307 214310 214313 214316 214319 214322 214328 214331 214334 214337 214340 214343 214346 214349 214355 214358 214361 214364 214367 214370 214373 214376 214379 214382 214388 214391 214394 214397 214400 214403 214406 214409 214412 214415 214418 214421 214424 214430 214433 214436 214439 214442 214445 214448 214451 214454 214457 214460 214463 214466 214469 214472 214475 214478 214481 214484 214487 214490 214493 214496 214499 214502 214505 214508 214511 214514 214517 214520 214523 214526 214529 214532 214535 214538 214541
iterations count:263426 (258), effective:510 (0)
213539 213553 213563 213572 213580 213586 213593 213599 213604 213609 213614 213617 213621 213624 213628 213631 213635 213638 213641 213645 213648 213651 213654 213657 213661 213664 213667 213670 213673 213676 213679 213682 213685 213687 213690 213693 213696 213699 213701 213704 213707 213710 213712 213715 213717 213719 213722 213724 213727 213729 213731 213733 213736 213738 213740 213742 213744 213746 213748 213750 213753 213755 213757 213761 213767 213773 213779 213782 213788 213794 213800 213806 213812 213818 213824 213830 213833 213839 213845 213851 213854 213860 213866 213872 213875 213881 213887 213893 213896 213902 213908 213911 213917 213923 213926 213932 213938 213941 213947 213950 213956 213959 213965 213971 213974 213980 213983 213989 213992 213998 214001 214007 214010 214016 214019 214025 214028 214034 214037 214043 214046 214052 214055 214058 214064 214067 214073 214076 214079 214085 214088 214094 214097 214100 214106 214109 214115 214118 214121 214127 214130 214133 214139 214142 214145 214151 214154 214157 214160 214166 214169 214172 214178 214181 214184 214187 214193 214196 214199 214205 214208 214211 214214 214217 214223 214226 214229 214232 214238 214241 214244 214247 214250 214256 214259 214262 214265 214268 214274 214277 214280 214283 214286 214292 214295 214298 214301 214304 214307 214313 214316 214319 214322 214325 214328 214331 214334 214340 214343 214346 214349 214352 214355 214358 214361 214367 214370 214373 214376 214379 214382 214385 214388 214391 214394 214397 214403 214406 214409 214412 214415 214418 214421 214424 214427 214430 214433 214436 214439 214442 214445 214448 214451 214454 214460 214463 214466 214469 214472 214475 214478 214481 214484 214487 214490 214493 214496 214499 214502 214505 214508 214511 214514 214517 214520 214523 214526 214529 214532 214535 214538 214541
iterations count:262826 (257), effective:509 (0)

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