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

Execution Outputs of marcie for RessAllocation/R003C100 (P/T)

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

execution on node 2: quadhexa-2.u-paris10.fr (runId=136978025000174_n_2)
=====================================================================
runnning marcie on RessAllocation-PT-R003C100 (CTLMix)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool marcie:
Test is RessAllocation-PT-R003C100, examination is CTLMix
=====================================================================

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

START 1369785086

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

constant oo registered with value < INFINITY >
parse successfull!


(NrP: 600 NrTr: 400)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m0sec


-> reachability set: #nodes 4156 (4.2e+03) #states 1,419,511,971,601,939,502,357,423,537,093,994,181,923,624,388,856,767,315,968 (57)



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

checking: EF [[p_81_0=p_39_1 & r_97_2=p_20_1]]
normalized: E [true U [p_81_0=p_39_1 & r_97_2=p_20_1]]

-> the formula is FALSE

FORMULA p_1466_mix_eq_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [[r_97_2=p_20_1 | p_81_0=p_39_1]]
normalized: E [true U [r_97_2=p_20_1 | p_81_0=p_39_1]]

-> the formula is FALSE

FORMULA p_1467_mix_eq_or FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[p_81_0=p_39_1 & r_97_2=p_20_1]]
normalized: ~ [EG [~ [[p_81_0=p_39_1 & r_97_2=p_20_1]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1468_mix_eq_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [[r_97_2=p_20_1 | p_81_0=p_39_1]]
normalized: ~ [EG [~ [[r_97_2=p_20_1 | p_81_0=p_39_1]]]]


EG iterations: 0
-> the formula is FALSE

FORMULA p_1469_mix_eq_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [A [EF [p_81_0=p_39_1] U AG [r_97_2=p_20_1]]]
normalized: ~ [EG [~ [[~ [E [~ [E [true U p_81_0=p_39_1]] U [E [true U ~ [r_97_2=p_20_1]] & ~ [E [true U p_81_0=p_39_1]]]]] & ~ [EG [E [true U ~ [r_97_2=p_20_1]]]]]]]]


EG iterations: 0

EG iterations: 0
-> the formula is FALSE

FORMULA p_1470_mix_eq_x FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m1sec

checking: EG [[r_38_0>r_13_1 & "r_43_2" \in [1, oo) && "p_44_1" \in [1, oo) && "r_44_2" \in [1, oo)]]
normalized: EG [[r_38_0>r_13_1 & "r_43_2" \in [1, oo) && "p_44_1" \in [1, oo) && "r_44_2" \in [1, oo)]]

.
EG iterations: 1
-> the formula is FALSE

FORMULA p_1471_mix_full_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [["r_43_2" \in [1, oo) && "p_44_1" \in [1, oo) && "r_44_2" \in [1, oo) | r_38_0>r_13_1]]
normalized: EG [["r_44_2" \in [1, oo) && "r_43_2" \in [1, oo) && "p_44_1" \in [1, oo) | r_38_0>r_13_1]]

...............
before gc: list nodes free: 3407876

after gc: idd nodes used:165976, unused:15834024; list nodes free:74737534
..
before gc: list nodes free: 3439510

after gc: idd nodes used:185814, unused:15814186; list nodes free:74648874
.
before gc: list nodes free: 3434681

after gc: idd nodes used:194714, unused:15805286; list nodes free:74608934
.
before gc: list nodes free: 3430106

after gc: idd nodes used:201037, unused:15798963; list nodes free:74582937
.
before gc: list nodes free: 3425256

after gc: idd nodes used:206651, unused:15793349; list nodes free:74559949

before gc: list nodes free: 3432240

after gc: idd nodes used:249171, unused:15750829; list nodes free:74340261
.
before gc: list nodes free: 3441641

after gc: idd nodes used:240506, unused:15759494; list nodes free:74392109
.
before gc: list nodes free: 3413559

after gc: idd nodes used:239793, unused:15760207; list nodes free:74400985
.
before gc: list nodes free: 3413071

after gc: idd nodes used:237496, unused:15762504; list nodes free:74418676
.
before gc: list nodes free: 3403851

after gc: idd nodes used:241387, unused:15758613; list nodes free:74404542

before gc: list nodes free: 3470269

after gc: idd nodes used:267042, unused:15732958; list nodes free:74272519
.
before gc: list nodes free: 3404198

after gc: idd nodes used:259998, unused:15740002; list nodes free:74314132
.
before gc: list nodes free: 3398040

after gc: idd nodes used:257966, unused:15742034; list nodes free:74329750

before gc: list nodes free: 3463654

after gc: idd nodes used:286187, unused:15713813; list nodes free:74184086
.
before gc: list nodes free: 3397250

after gc: idd nodes used:274943, unused:15725057; list nodes free:74247751
.
before gc: list nodes free: 3387039

after gc: idd nodes used:139617, unused:15860383; list nodes free:74862291

before gc: list nodes free: 3469731

after gc: idd nodes used:296304, unused:15703696; list nodes free:74141549
.
before gc: list nodes free: 3392624

after gc: idd nodes used:284551, unused:15715449; list nodes free:74208413

before gc: list nodes free: 3444816

after gc: idd nodes used:318603, unused:15681397; list nodes free:74031589
.
before gc: list nodes free: 3391296

after gc: idd nodes used:300075, unused:15699925; list nodes free:74133385

before gc: list nodes free: 3386395

after gc: idd nodes used:354416, unused:15645584; list nodes free:73852258
.
before gc: list nodes free: 3430428

after gc: idd nodes used:316398, unused:15683602; list nodes free:74054252
.
before gc: list nodes free: 3379569

after gc: idd nodes used:304325, unused:15695675; list nodes free:74120778

before gc: list nodes free: 3457332

after gc: idd nodes used:332024, unused:15667976; list nodes free:73977687
.
before gc: list nodes free: 3381824

after gc: idd nodes used:313140, unused:15686860; list nodes free:74080098

before gc: list nodes free: 3451910

after gc: idd nodes used:344374, unused:15655626; list nodes free:73918519
.
before gc: list nodes free: 3376389

after gc: idd nodes used:322413, unused:15677587; list nodes free:74036388

before gc: list nodes free: 3442012

after gc: idd nodes used:356039, unused:15643961; list nodes free:73861299
.
before gc: list nodes free: 3376026

after gc: idd nodes used:330494, unused:15669506; list nodes free:73999618

before gc: list nodes free: 3433498

after gc: idd nodes used:366735, unused:15633265; list nodes free:73810558
.
before gc: