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

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

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

execution on node 1: quadhexa-2.u-paris10.fr (runId=136978024800113_n_1)
=====================================================================
runnning marcie on RessAllocation-PT-R003C050 (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 RessAllocation-PT-R003C050, examination is CTLFireability
=====================================================================

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

START 1369783609

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: 300 NrTr: 200)

net check time: 0m0sec

parse mcc successfull!

place and transition orderings generation:0m0sec

init dd package: 0m5sec


RS generation: 0m0sec


-> reachability set: #nodes 2056 (2.1e+03) #states 48,717,538,008,124,384,423,924,727,808 (28)



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

checking: AG [["p_6_0" \in [1, oo) && "r_6_1" \in [1, oo) && "r_5_1" \in [1, oo) & "p_21_1" \in [1, oo) && "r_20_0" \in [1, oo) && "r_21_0" \in [1, oo)]]
normalized: ~ [E [true U ~ [["r_21_0" \in [1, oo) && "p_21_1" \in [1, oo) && "r_20_0" \in [1, oo) & "p_6_0" \in [1, oo) && "r_6_1" \in [1, oo) && "r_5_1" \in [1, oo)]]]]

-> the formula is FALSE

FORMULA p_1441_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [["r_20_0" \in [1, oo) && "p_21_1" \in [1, oo) && "r_21_0" \in [1, oo) | "p_6_0" \in [1, oo) && "r_6_1" \in [1, oo) && "r_5_1" \in [1, oo)]]
normalized: E [true U ["r_5_1" \in [1, oo) && "p_6_0" \in [1, oo) && "r_6_1" \in [1, oo) | "r_20_0" \in [1, oo) && "p_21_1" \in [1, oo) && "r_21_0" \in [1, oo)]]

-> the formula is TRUE

FORMULA p_1442_fireability_or TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: AF [["r_21_0" \in [1, oo) && "r_20_0" \in [1, oo) && "p_21_1" \in [1, oo) & ~ ["r_5_1" \in [1, oo) && "p_6_0" \in [1, oo) && "r_6_1" \in [1, oo)]]]
normalized: ~ [EG [~ [[! ("r_5_1" \in [1, oo) && "p_6_0" \in [1, oo) && "r_6_1" \in [1, oo)) & "r_20_0" \in [1, oo) && "p_21_1" \in [1, oo) && "r_21_0" \in [1, oo)]]]]

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

FORMULA p_1443_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m23sec

checking: EF [["r_21_0" \in [1, oo) && "p_21_1" \in [1, oo) && "r_20_0" \in [1, oo) | ~ ["r_5_1" \in [1, oo) && "r_6_1" \in [1, oo) && "p_6_0" \in [1, oo)]]]
normalized: E [true U [! ("r_6_1" \in [1, oo) && "p_6_0" \in [1, oo) && "r_5_1" \in [1, oo)) | "r_21_0" \in [1, oo) && "p_21_1" \in [1, oo) && "r_20_0" \in [1, oo)]]

-> the formula is TRUE

FORMULA p_1444_fireability_or_notx TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EF [EF [["r_21_0" \in [1, oo) && "p_21_1" \in [1, oo) && "r_20_0" \in [1, oo) | AF ["r_5_1" \in [1, oo) && "p_6_0" \in [1, oo) && "r_6_1" \in [1, oo)]]]]
normalized: E [true U E [true U [~ [EG [! ("p_6_0" \in [1, oo) && "r_6_1" \in [1, oo) && "r_5_1" \in [1, oo))]] | "r_21_0" \in [1, oo) && "p_21_1" \in [1, oo) && "r_20_0" \in [1, oo)]]]

.............
before gc: list nodes free: 3258705

after gc: idd nodes used:63746, unused:15936254; list nodes free:75205030
...........................................................
EG iterations: 72
-> the formula is TRUE

FORMULA p_1445_fireability_x TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m31sec

checking: EF [["r_49_2" \in [1, oo) && "r_48_2" \in [1, oo) & "r_16_0" \in [1, oo) && "r_15_0" \in [1, oo)]]
normalized: E [true U ["r_16_0" \in [1, oo) && "r_15_0" \in [1, oo) & "r_49_2" \in [1, oo) && "r_48_2" \in [1, oo)]]

-> the formula is TRUE

FORMULA p_1476_fireability_and TRUE TECHNIQUES DECISION_DIAGRAMS

mc time: 0m0sec

checking: EG [["r_49_2" \in [1, oo) && "r_48_2" \in [1, oo) | "r_15_0" \in [1, oo) && "r_16_0" \in [1, oo)]]
normalized: EG [["r_15_0" \in [1, oo) && "r_16_0" \in [1, oo) | "r_49_2" \in [1, oo) && "r_48_2" \in [1, oo)]]

......
before gc: list nodes free: 3268030

after gc: idd nodes used:70763, unused:15929237; list nodes free:75176320
..........
before gc: list nodes free: 3381995

after gc: idd nodes used:262089, unused:15737911; list nodes free:74311579
..
before gc: list nodes free: 3330208

after gc: idd nodes used:309862, unused:15690138; list nodes free:74086321
.
before gc: list nodes free: 3320654

after gc: idd nodes used:322722, unused:15677278; list nodes free:74029916
.
before gc: list nodes free: 3314506

after gc: idd nodes used:330463, unused:15669537; list nodes free:73997274
.
before gc: list nodes free: 3305055

after gc: idd nodes used:335595, unused:15664405; list nodes free:73982036
.
before gc: list nodes free: 3290807

after gc: idd nodes used:346325, unused:15653675; list nodes free:73935096
.
before gc: list nodes free: 3289816

after gc: idd nodes used:357046, unused:15642954; list nodes free:73888247
.
before gc: list nodes free: 3292276

after gc: idd nodes used:368058, unused:15631942; list nodes free:73839398

before gc: list nodes free: 3407588

after gc: idd nodes used:419834, unused:15580166; list nodes free:73569082
.
before gc: list nodes free: 3315874

after gc: idd nodes used:394047, unused:15605953; list nodes free:73713133
.
before gc: list nodes free: 3252743

after gc: idd nodes used:394008, unused:15605992; list nodes free:73720707
.
before gc: list nodes free: 3255732

after gc: idd nodes used:401497, unused:15598503; list nodes free:73688730

before gc: list nodes free: 3381118

after gc: idd nodes used:463105, unused:15536895; list nodes free:73361414
.
before gc: list nodes free: 3309191

after gc: idd nodes used:419636, unused:15580364; list nodes free:73599124
.
before gc: list nodes free: 3225535

after gc: idd nodes used:421275, unused:15578725; list nodes free:73598802
.
before gc: list nodes free: 3245258

after gc: idd nodes used:419583, unused:15580417; list nodes free:73607507

before gc: list nodes free: 3465091

after gc: idd nodes used:451577, unused:15548423; list nodes free:73440597
.
before gc: list nodes free: 3226347

after gc: idd nodes used:437540, unused:15562460; list nodes free:73524939
.
before gc: list nodes free: 3224345

after gc: idd nodes used:441185, unused:15558815; list nodes free:73510251

before gc: list nodes free: 3445414

after gc: idd nodes used:472417, unused:15527583; list nodes free:73342633
.
before gc: list nodes free: 3224182

after gc: idd nodes used:449855, unused:15550145; list nodes free:73469299
.
before gc: list nodes free: 3210964

after gc: idd nodes used:451291, unused:15548709; list nodes free:73464737

before gc: list nodes free: 3447766

after gc: idd nodes used:477209, unused:15522791; list nodes free:73318995
.
before gc: list nodes free: 3209993

after gc: idd nodes used:457638, unused:15542362; list nodes free:73434581
.
before gc: list nodes free: 3207578

after gc: idd nodes used:459847, unused:15540153; list nodes free:73426225

before gc: list nodes free: 3470950

after gc: idd nodes used:476886, unused:15523114; list nodes free:73329843
.
before gc: list nodes free: 3185933

after gc: idd nodes used:461351, unused:15538649; list nodes free:73418217

before gc: list nodes free: 3245845

after gc: idd nodes used:566929, unused:15433071; list nodes free:72866723
.
before gc: list nodes free: 3373619

after gc: idd nodes used:471309, unused:15528691; list nodes free:73366714
.
before gc: list nodes free: 3176174

after gc: idd nodes used:461739, unused:15538261; list nodes free:73416894

before gc: list nodes free: 3316113

after gc: idd nodes used:535950, unused:15464050; list nodes free:73024100
.
before gc: list nodes free: 3306775

after gc: idd nodes used:465599, unused:15534401; list nodes free:73396310